Editing Tree automaton (section)

== Definitions ==

A '''bottom-up finite tree automaton''' over ''F'' is defined as a tuple
(''Q'', ''F'', ''Q''<sub>''f''</sub>, Δ),
where ''Q'' is a set of states, ''F'' is a [[ranked alphabet]] (i.e., an alphabet whose symbols have an associated [[arity]]), {{math|''Q''<sub>''f''</sub> ⊆ ''Q''}} is a set of final states, and Δ is a set of [[Production (computer science)|transition rules]] of the form ''f''(''q''<sub>1</sub>(''x''<sub>1</sub>),...,''q''<sub>''n''</sub>(''x''<sub>''n''</sub>)) → ''q''(''f''(''x''<sub>1</sub>,...,''x''<sub>''n''</sub>)), for an ''n''-ary {{math|''f'' ∈ ''F'', ''q'', ''q''<sub>''i''</sub> ∈ ''Q''}}, and ''x''<sub>''i''</sub> variables denoting subtrees. That is, members of Δ are rewrite rules from nodes whose childs' roots are states, to nodes whose roots are states. Thus the state of a node is deduced from the states of its children.

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'').
Since these transition rules for constant symbols (leaves) do not require a state, no explicitly defined initial states are needed.
A bottom-up tree automaton is run on a [[ground term]] over ''F'', starting at all its leaves simultaneously and moving upwards, associating a run state from ''Q'' with each subterm.
The term is accepted if its root is associated to an accepting state from {{math|''Q''<sub>''f''</sub>}}.{{sfn|Comon et al.|2008|loc=sect. 1.1, p. 20}}

A '''top-down finite tree automaton''' over ''F'' is defined as a tuple
(''Q'', ''F'', ''Q''<sub>''i''</sub>, Δ),
with two differences with bottom-up tree automata. First, {{math|''Q''<sub>''i''</sub> ⊆ ''Q''}}, the set of its initial states, replaces {{math|''Q''<sub>''f''</sub>}}; second, its transition rules are oriented conversely:
''q''(''f''(''x''<sub>1</sub>,...,''x''<sub>''n''</sub>))  → ''f''(''q''<sub>1</sub>(''x''<sub>1</sub>),...,''q''<sub>''n''</sub>(''x''<sub>''n''</sub>)), for an ''n''-ary {{math|''f'' ∈ ''F'', ''q'', ''q''<sub>''i''</sub> ∈ ''Q''}}, and ''x''<sub>''i''</sub> variables denoting subtrees.
That is, members of Δ are here rewrite rules from nodes whose roots are states to nodes whose children's roots are states.
A top-down automaton starts in some of its initial states at the root and moves downward along branches of the tree, associating along a run a state with each subterm inductively.
A tree is accepted if every branch can be gone through this way.{{sfn|Comon et al.|2008|loc=sect. 1.6, p. 38}}

A tree automaton is called '''deterministic''' (abbreviated '''DFTA''') if no two rules from Δ have the same left hand side; otherwise it is called '''nondeterministic''' ('''NFTA''').{{sfn|Comon et al.|2008|loc=sect. 1.1, p. 23}} Non-deterministic top-down tree automata have the same expressive power as non-deterministic bottom-up ones;{{sfn|Comon et al.|2008|loc=sect. 1.6, theorem 1.6.1, p. 38}} the transition rules are simply reversed, and the final states become the initial states.

In contrast, '''deterministic''' top-down tree automata<ref>In a strict sense, deterministic top-down automata are not defined by {{harvp|Comon et al.|2008}} but they are used there (sect. 1.6, proposition 1.6.2, p. 38). They accept the class of path-closed tree languages (sect. 1.8, exercise 1.6, p. 43-44).</ref> are less powerful than their bottom-up counterparts, because in a deterministic tree automaton no two transition rules have the same left-hand side. For tree automata, transition rules are rewrite rules; and for top-down ones, the left-hand side will be parent nodes. Consequently, a deterministic top-down tree automaton will only be able to test for tree properties that are true in all branches, because the choice of the state to write into each child branch is determined at the parent node, without knowing the child branches contents.

[[Infinite-tree automaton|Infinite-tree automata]] extend top-down automata to infinite trees, and can be used to prove decidability of [[S2S (mathematics) | S2S]], the [[monadic second-order logic | monadic second-order]] theory with two successors.  Finite tree automata (nondeterministic if top-down) suffice for WS2S.<ref>{{Cite book |last1=Morawietz |first1=Frank |last2=Cornell |first2=Tom |chapter=Representing constraints with automata |date=1997-07-07 |title=Proceedings of the 35th annual meeting on Association for Computational Linguistics - |chapter-url=https://dl.acm.org/doi/10.3115/976909.979677 |series=ACL '98/EACL '98 |location=USA |publisher=Association for Computational Linguistics |pages=468–475 |doi=10.3115/976909.979677}}</ref>