Tree automaton

A bottom-up finite tree automaton over F is defined as a tuple (Q, F, Qf, Δ), where Q is a set of states, F is a ranked alphabet (i.e., an alphabet whose symbols have an associated arity), Qf ⊆ Q is a set of final states, and Δ is a set of transition rules of the form f(q1(x1),...,qn(xn)) → q(f(x1,...,xn)), for an n-ary f ∈ F, q, qi ∈ Q, and xi variables denoting subtrees.

For n=0, that is, for a constant symbol f, the above transition rule definition reads f() → q(f()); often the empty parentheses are omitted for convenience: f → q(f).

[6] Employing coloring to distinguish members of F and Q, and using the ranked alphabet F={ false,true,nil,cons(.,.)

}, with cons having arity 2 and all other symbols having arity 0, a bottom-up tree automaton accepting the set of all finite lists of boolean values can be defined as (Q, F, Qf, Δ) with Q = { Bool,BList }, Qf = { BList }, and Δ consisting of the rules In this example, the rules can be understood intuitively as assigning to each term its type in a bottom-up manner; e.g. rule (4) can be read as "A term cons(x1,x2) has type BList, provided x1 and x2 has type Bool and BList, respectively".

A rejecting example run is Intuitively, this corresponds to the term cons(false,true) not being well-typed.

Using the notions from Deterministic finite automaton#Formal definition, it is defined by: In the tree automaton setting, the input alphabet is changed such that the symbols 0 and 1 are both unary, and a nullary symbol, say nil is used for tree leaves.

For a bottom-up automaton, a ground term t (that is, a tree) is accepted if there exists a reduction that starts from t and ends with q(t), where q is a final state.

For a top-down automaton, a ground term t is accepted if there exists a reduction that starts from q(t) and ends with t, where q is an initial state.

[7] A non-deterministic finite tree automaton is complete if there is at least one transition rule available for every possible symbol-states combination.

For a given tree-language L, a congruence can be defined by u ≡L v if C[u] ∈ L ⇔ C[v] ∈ L for each context C. The Myhill–Nerode theorem for tree automata states that the following three statements are equivalent:[14]