True when Minimal denotes the same tree as Automaton
using the least possible number of states. States that are
bisimilar are collapsed, and states the start state cannot
reach are dropped:
?- automaton_minimal(automaton(f(2,3), g(1), g(1), a, h(4)), M).
M = automaton(f(2, 2), g(1)).
State 1 of Minimal is still the start state, and the
states are numbered depth first from it, so the answer does not depend
on the order Automaton happened to be written in. Two
automata therefore denote the same tree exactly when their minimal forms
are
=@=/2, and automaton_minimal/2
is idempotent.
Together with term_automaton/2
this is term_minimal/2:
term_minimal(T, M) :-
term_automaton(T, A),
automaton_minimal(A, A1),
term_automaton(M, A1).
The transition relation is a function: a state has exactly one
successor per argument position. Nondeterministic transition systems are
not supported.
