m-chrzan.xyz
aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorMarcin Chrzanowski <mc370754@students.mimuw.edu.pl>2021-08-09 20:49:20 -0400
committerMarcin Chrzanowski <mc370754@students.mimuw.edu.pl>2021-08-09 20:49:20 -0400
commitd8637ef9adee6a033e311ba2b71ad9a6089149a2 (patch)
treed4023e801b8f767fe49cc790f9486195b394209d
parent2646969eaf6d96f6c49a45b6684ae9f2259a1ba3 (diff)
Mention MSO to automata theorem
-rw-r--r--mgr.tex15
1 files changed, 11 insertions, 4 deletions
diff --git a/mgr.tex b/mgr.tex
index b6c18b9..a7bb567 100644
--- a/mgr.tex
+++ b/mgr.tex
@@ -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