diff options
author | Marcin Chrzanowski <mc370754@students.mimuw.edu.pl> | 2021-08-07 15:38:25 -0400 |
---|---|---|
committer | Marcin Chrzanowski <mc370754@students.mimuw.edu.pl> | 2021-08-07 15:38:25 -0400 |
commit | de37067763b58ec29b6deeec2ec1ca7a096f1987 (patch) | |
tree | cab8dcfb16795dbc49408364689dd9a49205ece6 | |
parent | c68fe5a45bcad9cf3bb94bd192bdc2bbbe5a07d1 (diff) |
Begin tree and MSO definitions
-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} |