Editing Tree automaton (section)

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