m-chrzan.xyz
aboutsummaryrefslogtreecommitdiff
path: root/mgr.tex
diff options
context:
space:
mode:
Diffstat (limited to 'mgr.tex')
-rw-r--r--mgr.tex12
1 files changed, 6 insertions, 6 deletions
diff --git a/mgr.tex b/mgr.tex
index cb631e0..c066fe6 100644
--- a/mgr.tex
+++ b/mgr.tex
@@ -512,7 +512,7 @@ before, by looking at $k' := \breaktable[(k+1).q']$, comparing it to $j$, and
either halting if $k' \geq j$, or jumping again otherwise. Because with each
jump we move to a color strictly smaller than before, the number of jumps is
bounded by the number of colors, $|Q|$. Thus the question is answered in time
-constant with respect to $|w|$.
+$O(|Q|)$, which is constant with respect to $|w|$.
\chapter{Branch Infix Regular Questions}\label{branchinfix}
@@ -797,11 +797,11 @@ with unary relation $U_X$ is equivalent to a valuation of $\vec{X}$ in which the
variable $X$ is set to $W$.
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
-$b_1 \ldots b_k$ (where $k = |\vec{X}|$ and each $b_i \in \{ 0, 1 \}$) should be
-interpreted as a bit vector signifying which unary relations $U_X$ a vertex is
-assigned to.
+trees over the alphabet $\Sigma \times \{ 0, 1 \}^{\vec{X}}$ which accepts a
+tree if and only if its labeling corresponds to a model satisfying $\varphi''$.
+Here a label $b_1 \ldots b_k$ (where $k = |\vec{X}|$ and each $b_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 query answering on trees by
solving the relabel regular qeustions problem on trees. Indeed, fix a formula