From 4e6ed4cdb422a672e96e73808327e49b812e662f Mon Sep 17 00:00:00 2001 From: Marcin Chrzanowski Date: Sat, 5 Feb 2022 20:59:53 +0100 Subject: Specify trees as binary --- mgr.tex | 16 ++++++++-------- 1 file 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 -- cgit v1.2.3