Begin tree and MSO definitions

1 files changed, 20 insertions, 3 deletions

diff --git a/mgr.tex b/mgr.tex
index f9ca98f..1310a16 100644
--- a/mgr.tex
+++ b/mgr.tex
@@ -94,11 +94,28 @@
 
 \section{Definitions}
 \subsection{Trees}
-b
+
+We work with finite trees whose vertices are labeled with letters from a finite
+alphabet. More formally, given a finite alphabet $\Sigma$, for each $a \in
+\Sigma$, $a$ is a tree, and if $t_1, \ldots, t_k$ are trees, then
+$a(t_1, \ldots, t_k)$ is also a tree.
+
 \subsection{Tree automata}
 c
-\subsection{Monadic Second Order Logic}
-a
+\subsection{Monadic Second Order (MSO) Logic}
+% def of MSO
+
+From a logical point of view, the trees we work with can be seen as structures
+over a signature with a single binary relation $E$ and unary relations $U_a$ for each $a \in
+\Sigma$. $E(v, w)$ represents a (directed from parent to child) edge from $v$ to
+$w$. $U_a(v)$ signifies that $v$'s label is $a$.
+
+For convenience, we will also make use of the binary relation $\leq$, with $v
+\leq w$ signifying that $v$ is an ancestor of $w$ (with every vertex being an
+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}