diff options
| -rw-r--r-- | mgr.tex | 23 |
1 files changed, 20 insertions, 3 deletions
@@ -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} |