Add more explicit reduction from MSO to relabling

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}