m-chrzan.xyz
aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorMarcin Chrzanowski <mc370754@students.mimuw.edu.pl>2021-10-13 15:15:13 +0200
committerMarcin Chrzanowski <mc370754@students.mimuw.edu.pl>2021-10-13 15:15:13 +0200
commitc9fce818e00c50f9623e4a19c75dc447452ff441 (patch)
tree04d74305e2323b5da1ab63667597db242a172632
parent60c5919a62aff1c75e130a8b6be4e26d38592479 (diff)
Add more explicit reduction from MSO to relabling
-rw-r--r--mgr.tex31
1 files changed, 24 insertions, 7 deletions
diff --git a/mgr.tex b/mgr.tex
index 2d015a8..f21bf72 100644
--- a/mgr.tex
+++ b/mgr.tex
@@ -541,8 +541,8 @@ infix regular queries in constant time.
\chapter{MSO Query Answering on Trees}
-We now have all the pieces necessary to present our \qptime{$n$}{$m \log m$}
-algorithm for MSO query answering on trees. We fix an MSO formula
+We now have all the pieces necessary to present our \qptime{$O(n)$}{$O(m \log
+m)$} algorithm for MSO query answering on trees. We fix an MSO formula
$\varphi(\vec{X})$ and take a tree $T$ of size $n$. We proceed with several
reductions so that we end up with needing to solve the relabel regular queries
problem, which we solve in the remainder of this chapter.
@@ -556,15 +556,32 @@ sentence without free variables by adding a unary relation $U_X$ for each
variable $X \in \vec{X}$ and instead of considering the formula $\varphi'$, we
now consider the sentence
+\begin{equation*}
+ \varphi'' = \exists_{X_1} \ldots \exists_{X_k}
+ (\forall{}_x x \in X_i \iff U_{X_i}(x)) \land
+ \varphi'(X_1, \ldots, X_k).
+\end{equation*}
+
Selecting a model in which the vertices in set $W$ are exactly those colored
with unary relation $U_X$ is equivalent to a valuation of $\vec{X}$ in which the
variable $X$ is set to $W$.
-\begin{equation*}
- \varphi'' = \exists_{X_1} \ldots \exists_{X_k}
- (\forall{}_x x \in X_i \implies U_{X_i}(x)) \land
- \varphi'(X_1, \ldots, X_k)
-\end{equation*}
+Now by Theorem \ref{mso-to-automaton}, there is a tree automaton $A$ for binary
+trees over the alphabet $\{ 0, 1 \}^{\vec{X}}$ which accepts a tree if and only
+if its labeling corresponds to a model satisfying $\varphi''$. Here a label
+$a_1 \ldots a_k$ (where $k = |\vec{X}|$ and each $a_i \in \{ 0, 1 \}$) should be
+interpreted as a bit vector signifying which unary relations $U_X$ a vertex is
+assigned to.
+
+By combining the above reductions, we can solve MSO queries on trees by solving
+relabel regular queries on trees. Indeed, fix a formula $\varphi(\vec{X})$ and take
+a tree $T$. Derive automaton $A$ and tree $T'$ as above. Label each vertex of
+$T'$ with $0\ldots0$ (signifying that none of its vertices have yet been
+assigned to any of the variables in $\vec{X}$). Preprocess $A$ and $T'$ for
+relabel regular queries. Now a relabeling of $T'$'s vertices corresponds to
+selecting a specific valuation $\vec{W}$ of $\vec{X}$, thus answering whether or
+not $A$ accepts the relabeled tree is equivalent to answering whether or not $T
+\models \varphi(\vec{W})$.
\section{Relabel Regular Queries on Trees}