m-chrzan.xyz
aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--mgr.tex16
1 files changed, 8 insertions, 8 deletions
diff --git a/mgr.tex b/mgr.tex
index 8ecbc83..5f8e6ab 100644
--- a/mgr.tex
+++ b/mgr.tex
@@ -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