diff options
author | Marcin Chrzanowski <mc370754@students.mimuw.edu.pl> | 2021-10-07 13:08:45 +0200 |
---|---|---|
committer | Marcin Chrzanowski <mc370754@students.mimuw.edu.pl> | 2021-10-07 13:08:45 +0200 |
commit | d772de735c8ac9ac73972c9c775be73a7818f025 (patch) | |
tree | 06b26c537f82295422a969a703f554f7d78a5f7a | |
parent | 9a1dbecbf696e64811d20de2217aa375fe87a2fb (diff) |
Be more precise with relations
-rw-r--r-- | mgr.tex | 6 |
1 files changed, 5 insertions, 1 deletions
@@ -158,10 +158,14 @@ 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$. +In the case of binary trees, the relation $E$ is replaced with two binary +relations $E_l$ and $E_r$, which represent an edge from parent to left child, +and from parent to right child, respectively. + 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 +the case of MSO on trees, $\leq$ can be defined using just the edge relation $E$. We make use of a fundamental theorem tying MSO logic on trees and tree automata: |