diff options
| -rw-r--r-- | mgr.tex | 15 |
1 files changed, 11 insertions, 4 deletions
@@ -158,10 +158,17 @@ ancestor of itself; $<$ can be used to signify a strict ancestor). Note that in the case of MSO on trees, $\leq$ could be defined using just the edge relation $E$. -\subsection{Query answering problems} -d -\section{Known algorithms we will use} -\subsection{Least Common Ancestor} +We make use of a fundamental theorem tying MSO logic on trees and tree automata: + +\begin{theorem} + 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)$. +\end{theorem} + +We note that the converse of this theorem is also true (i.e. that for every tree +automaton, there is a corresponding MSO formula), however we will use only the +MSO to automata direction in this work. \queryproblem{% Least Common Ancestor (LCA) Queries |