Editing Tree automaton

{{for|a different notion of tree automaton|tree walking automaton}}

A '''tree automaton''' is a type of [[state machine]]. Tree automata deal with [[tree structure]]s, rather than the [[string (computer science)|strings]] of more conventional state machines.

The following article deals with branching tree automata, which correspond to [[regular tree language|regular languages of trees]].

As with classical automata, finite tree automata (FTA) can be either a [[deterministic automaton]] or not. According to how the automaton processes the input tree, finite tree automata can be of two types: (a) bottom up, (b) top down. This is an important issue, as although non-deterministic (ND) top-down and ND bottom-up tree automata are equivalent in expressive power, deterministic top-down automata are strictly less powerful than their deterministic bottom-up counterparts, because tree properties specified by deterministic top-down tree automata can only depend on path properties. (Deterministic bottom-up tree automata are as powerful as ND tree automata.)

== 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>

== Examples ==

===Bottom-up automaton accepting boolean lists===
Employing coloring to distinguish members of ''F'' and ''Q'', and using the ranked alphabet ''F''={ {{color|#800000|''false''}},{{color|#800000|''true''}},{{color|#800000|''nil''}},{{color|#800000|''cons''}}(.,.) }, with {{color|#800000|''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'', ''Q''<sub>''f''</sub>, Δ) with {{math|1=''Q'' = { {{color|#008000|''Bool''}},{{color|#008000|''BList''}} }, ''Q''<sub>''f''</sub> = { {{color|#008000|''BList''}} },}} and Δ consisting of the rules

<!-- -tabular alignment chosen intentionally - please don't change without understanding the example or without proper reason- -->
:{|
|-
| {{color|#800000|''false''}} || → || {{color|#008000|''Bool''}}({{color|#800000|''false''}}) || (1),
|-
| {{color|#800000|''true''}} || → || {{color|#008000|''Bool''}}({{color|#800000|''true''}}) || (2),
|-
| {{color|#800000|''nil''}} || → || {{color|#008000|''BList''}}({{color|#800000|''nil''}}) || (3), and
|-
| {{color|#800000|''cons''}}({{color|#008000|''Bool''}}(x<sub>1</sub>),{{color|#008000|''BList''}}(x<sub>2</sub>)) || → || {{color|#008000|''BList''}}({{color|#800000|''cons''}}(x<sub>1</sub>,x<sub>2</sub>)) &nbsp; &nbsp; &nbsp; || (4).
|}

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 {{color|#800000|''cons''}}(''x''<sub>1</sub>,''x''<sub>2</sub>) has type {{color|#008000|''BList''}}, provided ''x''<sub>1</sub> and ''x''<sub>2</sub> has type {{color|#008000|''Bool''}} and {{color|#008000|''BList''}}, respectively".
An accepting example run is

<!-- -tabular alignment chosen intentionally - please don't change without understanding the example or without proper reason- -->
:{|
|-
|
| ALIGN=RIGHT | {{color|#800000|''cons''}}(
| ALIGN=RIGHT | {{color|#800000|''false''}},
| ALIGN=RIGHT | {{color|#800000|''cons''}}(
| ALIGN=RIGHT | {{color|#800000|''true''}},
| ALIGN=RIGHT | {{color|#800000|''nil''}}
| ))
|-
| ⇒
| ALIGN=RIGHT | {{color|#800000|''cons''}}(
| ALIGN=RIGHT | {{color|#800000|''false''}},
| ALIGN=RIGHT | {{color|#800000|''cons''}}(
| ALIGN=RIGHT | {{color|#800000|''true''}},
| ALIGN=RIGHT | {{color|#008000|''BList''}}({{color|#800000|''nil''}})
| ))
| by (3)
|-
| ⇒
| ALIGN=RIGHT | {{color|#800000|''cons''}}(
| ALIGN=RIGHT | {{color|#800000|''false''}},
| ALIGN=RIGHT | {{color|#800000|''cons''}}(
| ALIGN=RIGHT | {{color|#008000|''Bool''}}({{color|#800000|''true''}}),
| ALIGN=RIGHT | {{color|#008000|''BList''}}({{color|#800000|''nil''}})
| ))
| by (2)
|-
| ⇒
| ALIGN=RIGHT | {{color|#800000|''cons''}}(
| ALIGN=RIGHT | {{color|#800000|''false''}},
| ALIGN=RIGHT | {{color|#008000|''BList''}}({{color|#800000|''cons''}}(
| ALIGN=RIGHT | {{color|#800000|''true''}},
| ALIGN=RIGHT | {{color|#800000|''nil''}}
| )))
| by (4)
|-
| ⇒
| ALIGN=RIGHT | {{color|#800000|''cons''}}(
| ALIGN=RIGHT | {{color|#008000|''Bool''}}({{color|#800000|''false''}}),
| ALIGN=RIGHT | {{color|#008000|''BList''}}({{color|#800000|''cons''}}(
| ALIGN=RIGHT | {{color|#800000|''true''}},
| ALIGN=RIGHT | {{color|#800000|''nil''}}
| )))
| by (1)
|-
| ⇒
| ALIGN=RIGHT | {{color|#008000|''BList''}}({{color|#800000|''cons''}}(
| ALIGN=RIGHT | {{color|#800000|''false''}},
| ALIGN=RIGHT | {{color|#800000|''cons''}}(
| ALIGN=RIGHT | {{color|#800000|''true''}},
| ALIGN=RIGHT | {{color|#800000|''nil''}}
| ))) &nbsp; &nbsp; &nbsp;
| by (4), accepted.
|}

Cf. the derivation of the same term from a regular tree grammar corresponding to the automaton, shown at [[Regular tree grammar#Examples]].

A rejecting example run is

<!-- -tabular alignment chosen intentionally - please don't change without understanding the example or without proper reason- -->
:{|
|-
|
| ALIGN=RIGHT | {{color|#800000|''cons''}}(
| ALIGN=RIGHT | {{color|#800000|''false''}},
| ALIGN=RIGHT | {{color|#800000|''true''}}
| )
|-
| ⇒
| ALIGN=RIGHT | {{color|#800000|''cons''}}(
| ALIGN=RIGHT | {{color|#800000|''false''}},
| ALIGN=RIGHT | {{color|#008000|''Bool''}}({{color|#800000|''true''}})
| )
| by (1)
|-
| ⇒
| ALIGN=RIGHT | {{color|#800000|''cons''}}(
| ALIGN=RIGHT | {{color|#008000|''Bool''}}({{color|#800000|''false''}}),
| ALIGN=RIGHT | {{color|#008000|''Bool''}}({{color|#800000|''true''}})
| ) &nbsp; &nbsp; &nbsp;
| by (2), no further rule applicable.
|}
Intuitively, this corresponds to the term {{color|#800000|''cons''}}({{color|#800000|''false''}},{{color|#800000|''true''}}) not being well-typed.

===Top-down automaton accepting multiples of 3 in binary notation===

<!-- -tabular alignment chosen intentionally - please don't change without understanding the example or without proper reason- -->
{| class=wikitable style="float:right;"
|-
!
! ALIGN=center | '''(A)'''
! ALIGN=center | '''(B)'''
! ALIGN=center | '''(C)'''
! ALIGN=center | '''(D)'''
|-
!
! ALIGN=center | [[Regular grammar#Strictly regular grammars|'''String'''<BR>'''grammar''']]<BR>'''rules'''
! ALIGN=center | [[Deterministic finite automaton#Formal definition|'''String'''<BR>'''automaton''']]<BR>'''transitions'''
! ALIGN=center | '''Tree'''<BR>'''automaton'''<BR>'''transitions'''
! ALIGN=center | [[Regular tree grammar#Definition|'''Tree'''<BR>'''grammar''']]<BR>'''rules'''
|-
| <!---line numbers--->
{|
|-
! 0
|-
! 1
|-
! 2
|-
! 3
|-
! 4
|-
! 5
|-
! 6
|}
| <!---string grammar--->
{| 
|- 
| {{color|#008000|''S''<sub>0</sub>}} || → || ε
|- 
| {{color|#008000|''S''<sub>0</sub>}} || → || {{color|#800000|0}} {{color|#008000|''S''<sub>0</sub>}}
|- 
| {{color|#008000|''S''<sub>0</sub>}} || → || {{color|#800000|1}} {{color|#008000|''S''<sub>1</sub>}}
|- 
| {{color|#008000|''S''<sub>1</sub>}} || → || {{color|#800000|0}} {{color|#008000|''S''<sub>2</sub>}}
|- 
| {{color|#008000|''S''<sub>1</sub>}} || → || {{color|#800000|1}} {{color|#008000|''S''<sub>0</sub>}}
|- 
| {{color|#008000|''S''<sub>2</sub>}} || → || {{color|#800000|0}} {{color|#008000|''S''<sub>1</sub>}}
|- 
| {{color|#008000|''S''<sub>2</sub>}} || → || {{color|#800000|1}} {{color|#008000|''S''<sub>2</sub>}}
|}
| <!---string automaton--->
{| 
|- 
| &nbsp;
|- 
| δ({{color|#008000|''S''<sub>0</sub>}},{{color|#800000|0}}) || = {{color|#008000|''S''<sub>0</sub>}}
|- 
| δ({{color|#008000|''S''<sub>0</sub>}},{{color|#800000|1}}) || = {{color|#008000|''S''<sub>1</sub>}}
|- 
| δ({{color|#008000|''S''<sub>1</sub>}},{{color|#800000|0}}) || = {{color|#008000|''S''<sub>2</sub>}}
|- 
| δ({{color|#008000|''S''<sub>1</sub>}},{{color|#800000|1}}) || = {{color|#008000|''S''<sub>0</sub>}}
|- 
| δ({{color|#008000|''S''<sub>2</sub>}},{{color|#800000|0}}) || = {{color|#008000|''S''<sub>1</sub>}}
|- 
| δ({{color|#008000|''S''<sub>2</sub>}},{{color|#800000|1}}) || = {{color|#008000|''S''<sub>2</sub>}}
|}
| <!--- tree automaton--->
{|
|- 
| {{color|#008000|''S''<sub>0</sub>}}({{color|#800000|''nil''}}) || → || {{color|#800000|''nil''}}
|- 
| {{color|#008000|''S''<sub>0</sub>}}({{color|#800000|0}}(x)) || → || {{color|#800000|0}}({{color|#008000|''S''<sub>0</sub>}}(x))
|- 
| {{color|#008000|''S''<sub>0</sub>}}({{color|#800000|1}}(x)) || → || {{color|#800000|1}}({{color|#008000|''S''<sub>1</sub>}}(x))
|- 
| {{color|#008000|''S''<sub>1</sub>}}({{color|#800000|0}}(x)) || → || {{color|#800000|0}}({{color|#008000|''S''<sub>2</sub>}}(x))
|- 
| {{color|#008000|''S''<sub>1</sub>}}({{color|#800000|1}}(x)) || → || {{color|#800000|1}}({{color|#008000|''S''<sub>0</sub>}}(x))
|- 
| {{color|#008000|''S''<sub>2</sub>}}({{color|#800000|0}}(x)) || → || {{color|#800000|0}}({{color|#008000|''S''<sub>1</sub>}}(x))
|- 
| {{color|#008000|''S''<sub>2</sub>}}({{color|#800000|1}}(x)) || → || {{color|#800000|1}}({{color|#008000|''S''<sub>2</sub>}}(x))
|}
| <!--- tree grammar--->
{|
|- 
| {{color|#008000|''S''<sub>0</sub>}} || → || {{color|#800000|''nil''}}
|- 
| {{color|#008000|''S''<sub>0</sub>}} || → || {{color|#800000|0}}({{color|#008000|''S''<sub>0</sub>}})
|- 
| {{color|#008000|''S''<sub>0</sub>}} || → || {{color|#800000|1}}({{color|#008000|''S''<sub>1</sub>}})
|- 
| {{color|#008000|''S''<sub>1</sub>}} || → || {{color|#800000|0}}({{color|#008000|''S''<sub>2</sub>}})
|- 
| {{color|#008000|''S''<sub>1</sub>}} || → || {{color|#800000|1}}({{color|#008000|''S''<sub>0</sub>}})
|- 
| {{color|#008000|''S''<sub>2</sub>}} || → || {{color|#800000|0}}({{color|#008000|''S''<sub>1</sub>}})
|- 
| {{color|#008000|''S''<sub>2</sub>}} || → || {{color|#800000|1}}({{color|#008000|''S''<sub>2</sub>}})
|}
|}

{| style="float:right;"
| [[File:DFA example multiplies of 3.svg|thumb|[[Deterministic finite automaton|Deterministic finite (string) automaton]] accepting multiples of 3 in binary notation]]
|}

Using the same colorization as above, this example shows how tree automata generalize ordinary string automata.
The finite deterministic string automaton shown in the picture accepts all strings of binary digits that denote a multiple of 3.
Using the notions from [[Deterministic finite automaton#Formal definition]], it is defined by:
* the set ''Q'' of states being { {{color|#008000|''S''<sub>0</sub>}}, {{color|#008000|''S''<sub>1</sub>}}, {{color|#008000|''S''<sub>2</sub>}} },
* the input alphabet being { {{color|#800000|0}}, {{color|#800000|1}} },
* the initial state being {{color|#008000|''S''<sub>0</sub>}},
* the set of final states being { {{color|#008000|''S''<sub>0</sub>}} }, and
* the transitions being as shown in column (B) of the table.

In the tree automaton setting, the input alphabet is changed such that the symbols {{color|#800000|0}} and {{color|#800000|1}} are both unary, and a nullary symbol, say {{color|#800000|''nil''}} is used for tree leaves.
For example, the binary string "{{color|#800000|110}}" in the string automaton setting corresponds to the term "{{color|#800000|1}}({{color|#800000|1}}({{color|#800000|0}}({{color|#800000|''nil''}})))" in the tree automaton setting; this way, strings can be generalized to trees, or terms.
The top-down finite tree automaton accepting the set of all terms corresponding to multiples of 3 in binary string notation is then defined by:
* the set ''Q'' of states being still { {{color|#008000|''S''<sub>0</sub>}}, {{color|#008000|''S''<sub>1</sub>}}, {{color|#008000|''S''<sub>2</sub>}} },
* the ranked input alphabet being { {{color|#800000|0}}, {{color|#800000|1}}, {{color|#800000|''nil''}} }, with ''Arity''({{color|#800000|0}})=''Arity''({{color|#800000|1}})=1 and ''Arity''({{color|#800000|''nil''}})=0, as explained,
* the set of initial states being { {{color|#008000|''S''<sub>0</sub>}} }, and
* the transitions being as shown in column (C) of the table.
For example, the tree "{{color|#800000|1}}({{color|#800000|1}}({{color|#800000|0}}({{color|#800000|''nil''}})))" is accepted by the following tree automaton run:

<!-- -tabular alignment chosen intentionally - please don't change without understanding the example or without proper reason- -->
{|
|-
|    || {{color|#008000|''S''<sub>0</sub>}}( || {{color|#800000|1}}( ||  || {{color|#800000|1}}( || ||  {{color|#800000|0}}( ||  || {{color|#800000|''nil''}} || ))))
|- 
| ⇒  || || {{color|#800000|1}}( || {{color|#008000|''S''<sub>1</sub>}}( || {{color|#800000|1}}( ||  || {{color|#800000|0}}( ||  || {{color|#800000|''nil''}} || )))) || by 2
|- 
| ⇒  || || {{color|#800000|1}}( ||  || {{color|#800000|1}}( || {{color|#008000|''S''<sub>0</sub>}}( || {{color|#800000|0}}( ||  || {{color|#800000|''nil''}} || )))) || by 4
|- 
| ⇒  || || {{color|#800000|1}}( ||  || {{color|#800000|1}}( ||  || {{color|#800000|0}}( || {{color|#008000|''S''<sub>0</sub>}}( || {{color|#800000|''nil''}} || )))) || by 1
|- 
| ⇒  || || {{color|#800000|1}}( ||  || {{color|#800000|1}}(  ||  || {{color|#800000|0}}( ||  || {{color|#800000|''nil''}} || ))) &nbsp; &nbsp; &nbsp; || by 0
|}

In contrast, the term "{{color|#800000|1}}({{color|#800000|0}}({{color|#800000|''nil''}}))" leads to following non-accepting automaton run:

<!-- -tabular alignment chosen intentionally - please don't change without understanding the example or without proper reason- -->
{|
|- 
| ⇒  {{color|#008000|''S''<sub>0</sub>}}( || {{color|#800000|1}}( ||  || {{color|#800000|0}}( ||  || {{color|#800000|''nil''}} || )))
|- 
| ⇒  || {{color|#800000|1}}( || {{color|#008000|''S''<sub>1</sub>}}( || {{color|#800000|0}}( ||  || {{color|#800000|''nil''}} || )))) || by 2
|- 
| ⇒   || {{color|#800000|1}}( ||  || {{color|#800000|0}}( || {{color|#008000|''S''<sub>2</sub>}}( || {{color|#800000|''nil''}} || )))) &nbsp; &nbsp; &nbsp; || by 3, no further rule applicable
|}

Since there are no other initial states than {{color|#008000|''S''<sub>0</sub>}} to start an automaton run with, the term "{{color|#800000|1}}({{color|#800000|0}}({{color|#800000|''nil''}}))" is not accepted by the tree automaton.

For comparison purposes, the table gives in column (A) and (D) a [[regular grammar#Strictly regular grammars|(right) regular (string) grammar]], and a [[regular tree grammar#Definition|regular tree grammar]], respectively, each accepting the same language as its automaton counterpart.

== 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

== See also ==

* [[Courcelle's theorem]] - an application of tree automata to prove an algorithmic meta-theorem about graphs
* [[Tree transducers]] - extend tree automata in the same way that [[finite-state transducer|word transducer]]s extend [[finite-state automata|word automata]].
* [[Alternating tree automata]]
* [[Infinite-tree automaton|Infinite-tree automata]]

== Notes ==

{{reflist}}

== References ==

* {{cite book| first1=Hubert| last1=Comon| first2=Max| last2=Dauchet| first3=Rémi| last3=Gilleron| first4=Florent| last4=Jacquemard| first5=Denis| last5=Lugiez| first6=Christof| last6=Löding| first7=Sophie| last7=Tison| first8=Marc| last8=Tommasi| title=Tree Automata Techniques and Applications|date=November 2008| url=https://hal.inria.fr/hal-03367725/document| access-date=11 February 2014| ref={{harvid|Comon et al.|2008}}}}
* {{Cite book| publisher = Cambridge University Press| isbn = 978-1-139-49236-2| last = Hosoya| first = Haruo| title = Foundations of XML Processing: The Tree-Automata Approach| date =4 November 2010}}
* {{Cite arXiv| first1=Ferenc| last1=Gécseg| first2=Magnus| last2=Steinby| title=Tree Automata| year=1984 | class=cs.FL|eprint = 1509.06233}}
* {{Cite arXiv| last= Engelfriet| first=Joost| title= Tree Automata and Tree Grammars| year=1975 | class=cs.FL|eprint = 1510.02036}}

== External links ==

=== Implementations ===

* [http://www.grappa.univ-lille3.fr/~filiot/tata/ Grappa]{{dead link|date=March 2025}} ({{webarchive|url=https://web.archive.org/web/20190201065525/http://www.grappa.univ-lille3.fr/~filiot/tata/|date=February 1, 2019}}) - ranked and unranked tree automata libraries (OCaml)
* [https://people.irisa.fr/Thomas.Genet/timbuk Timbuk] - tools for reachability analysis and tree automata calculations (OCaml)
* [http://lethal.sourceforge.net/ LETHAL] - library for working with finite tree and hedge automata (Java)
* [https://www.isa-afp.org/entries/Tree-Automata.html Machine-checked tree automata library] (Isabelle [OCaml, SML, Haskell])
* [http://www.fit.vutbr.cz/research/groups/verifit/tools/libvata/ VATA] - a library for efficient manipulation of non-deterministic tree automata (C++)

{{Formal languages and grammars}}

[[Category:Trees (data structures)]]
[[Category:Automata (computation)]]
[[Category:Formal languages]]
[[Category:Theoretical computer science]]