From c9fce818e00c50f9623e4a19c75dc447452ff441 Mon Sep 17 00:00:00 2001 From: Marcin Chrzanowski Date: Wed, 13 Oct 2021 15:15:13 +0200 Subject: Add more explicit reduction from MSO to relabling --- mgr.tex | 31 ++++++++++++++++++++++++------- 1 file 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} -- cgit v1.2.3