Editing Tree automaton (section)

== Properties ==

=== Recognizability ===

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.

The tree language ''L''(''A'') '''accepted''', or '''recognized''', by a tree automaton ''A'' is the set of all ground terms accepted by ''A''. A set of ground terms is '''recognizable''' if there exists a tree automaton that accepts it.

A linear (that is, arity-preserving) tree homomorphism preserves recognizability.<ref>The notion in {{harvtxt|Comon et al.|2008|loc=sect. 1.4, theorem 1.4.3, p. 31-32}} of tree homomorphism is more general than that of the article "tree homomorphism".</ref>

=== Completeness and reduction ===

A non-deterministic finite tree automaton is '''complete''' if there is at least one transition rule available for every possible symbol-states combination.
A state ''q'' is '''accessible''' if there exists a ground term ''t'' such that there exists a reduction from ''t'' to ''q''(''t'').
An NFTA is '''reduced''' if all its states are accessible.{{sfn|Comon et al.|2008|loc=sect. 1.1, p. 23-24}}

=== Pumping lemma ===

Every sufficiently large<ref>Formally: ''[[Term (logic)#Operations with terms|height]]''(''t'') > ''k'', with ''k'' > 0 depending only on ''L'', not on ''t''</ref> ground term ''t'' in a recognizable tree language ''L'' can be vertically tripartited<ref>Formally: there is a context ''C''[.], a nontrivial context {{math|''C&prime;''[.]}}, and a ground term ''u'' such that {{math|1=''t'' = ''C''[''C&prime;''[''u'']]}}. A "context" ''C''[.] is a tree with one hole (or, correspondingly, a term with one occurrence of one variable). A context is called "trivial" if the tree consists only of the hole node (or, correspondingly, if the term is just the variable). The notation ''C''[''t''] means the result of inserting the tree ''t'' into the hole of ''C''[.] (or, correspondingly, [[Ground instance|instantiating]] the variable to ''t''). {{harvnb|Comon et al.|2008|p=17}}, gives a formal definition.</ref> such that arbitrary repetition ("pumping") of the middle part keeps the resulting term in ''L''.<ref>Formally: {{math|''C''[''C&prime;''<sup>''n''</sup>[''u'']] ∈ ''L''}} for all ''n'' ≥ 0. The notation ''C''<sup>''n''</sup>[.] means the result of stacking ''n'' copies of ''C''[.] one in another, cf. {{harvnb|Comon et al.|2008|p=17}}.</ref>{{sfn|Comon et al.|2008|loc=sect. 1.2, p. 29}}

For the language of all finite lists of boolean values from the above example, all terms beyond the height limit ''k''=2 can be pumped, since they need to contain an occurrence of {{color|#800000|''cons''}}. For example,

:{|
|-
| {{color|#800000|''cons''}}({{color|#800000|''false''}},
| {{color|#800000|''cons''}}({{color|#800000|''true''}},{{color|#800000|''nil''}})
| )
| ,
|-
| {{color|#800000|''cons''}}({{color|#800000|''false''}},{{color|#800000|''cons''}}({{color|#800000|''false''}},
| {{color|#800000|''cons''}}({{color|#800000|''true''}},{{color|#800000|''nil''}})
| ))
| ,
|-
| {{color|#800000|''cons''}}({{color|#800000|''false''}},{{color|#800000|''cons''}}({{color|#800000|''false''}},{{color|#800000|''cons''}}({{color|#800000|''false''}},
| {{color|#800000|''cons''}}({{color|#800000|''true''}},{{color|#800000|''nil''}})
| )))
| , ...
|}

all belong to that language.

=== Closure ===

The class of recognizable tree languages is closed under union, under complementation, and under intersection.{{sfn|Comon et al.|2008|loc=sect. 1.3, theorem 1.3.1, p. 30}}

=== Myhill–Nerode theorem ===

A congruence on the set of all trees over a ranked alphabet ''F'' is an [[equivalence relation]] such that {{math|''u''<sub>1</sub> ≡ ''v''<sub>1</sub>}} and ... and {{math|''u''<sub>''n''</sub> ≡ ''v''<sub>''n''</sub>}} implies {{math|''f''(''u''<sub>1</sub>,...,''u''<sub>''n''</sub>) ≡ ''f''(''v''<sub>1</sub>,...,''v''<sub>''n''</sub>)}}, for every {{math|''f'' ∈ ''F''}}.
It is of finite index if its number of equivalence-classes is finite.

For a given tree-language ''L'', a congruence can be defined by {{math|''u'' ≡<sub>''L''</sub> ''v''}} if {{math|''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:{{sfn|Comon et al.|2008|loc=sect. 1.5, p .36}}

# ''L'' is a recognizable tree language
# ''L'' is the union of some equivalence classes of a congruence of finite index
# the relation {{math|≡<sub>''L''</sub>}} is a congruence of finite index