diff options
| -rw-r--r-- | mgr.tex | 16 |
1 files changed, 8 insertions, 8 deletions
@@ -285,11 +285,11 @@ with elements of $Q$ such that \end{itemize} A run is \definedterm{accepting} if $T$'s root gets relabeled to an accepting -state, that is a state $q \in F$. The set of all trees accepted by an automaton -$A$ is called the \definedterm{language recognized by $A$}, notated $L(A)$. We -call the class of all languages recognized by tree automata \definedterm{regular -tree languages}, analogously to regular languages recognized by finite state -automata. +state, that is a state $q \in F$. The set of all binary trees accepted by an +automaton $A$ is called the \definedterm{language recognized by $A$}, notated +$L(A)$. We call the class of all languages recognized by tree automata +\definedterm{regular tree languages}, analogously to regular languages +recognized by finite state automata. We note that the expressive power of deterministic bottom-up tree automata is the same as that of nondeterministic (either bottom-up or top-down) tree @@ -316,9 +316,9 @@ $E$. We make use of a fundamental theorem tying MSO logic on trees and tree automata: \begin{theorem}\label{mso-to-automaton} - For every MSO formula $\varphi$ over trees, there exists a tree automaton - $A$ such that for every tree $T$, $T \models \varphi$ if, and only if $T \in - L(A)$. + For every MSO formula $\varphi$ over binary trees, there exists a tree + automaton $A$ such that for every binary tree $T$, $T \models \varphi$ if, + and only if $T \in L(A)$. \end{theorem} We note that the converse of this theorem is also true (i.e. that for every tree |