From de37067763b58ec29b6deeec2ec1ca7a096f1987 Mon Sep 17 00:00:00 2001 From: Marcin Chrzanowski Date: Sat, 7 Aug 2021 15:38:25 -0400 Subject: Begin tree and MSO definitions --- mgr.tex | 23 ++++++++++++++++++++--- 1 file 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} -- cgit v1.2.3