diff options
Diffstat (limited to 'mgr.tex')
| -rw-r--r-- | mgr.tex | 36 |
1 files changed, 31 insertions, 5 deletions
@@ -647,11 +647,26 @@ infix regular queries in constant time. \chapter{MSO Query Answering on Trees}\label{mso-query-answering} -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. +Now we have all the pieces necessary to present our main result, which we +can formulate as Theorem \ref{mso-query-answering-theorem}: + +\begin{theorem}\label{mso-query-answering-theorem} + Problem \ref{mso-query-answering-problem} can be solved in time + \qptime{$O(n)$}{$O(m \log m)$}. +\end{theorem} + +First, let's reduce Problem \ref{mso-query-answering-problem} to Problem +\ref{relabel-regular-queries}: + +\begin{lemma} + If Problem \ref{relabel-regular-queries} has an \qptime{$O(n)$}{$O(m \log + m)$} solution, then so does Problem \ref{mso-query-answering-problem}. +\end{lemma} + +Proof: We proceed with several standard linear reductions that transform Problem +\ref{mso-query-answering-problem}, which speaks about MSO formulae with free +variables, to Problem \ref{relabel-regular-queries}, which talks about tree +automata over binary trees. First of all, if $T$ is not binary, we can use a standard encoding to encode it inside of a binary tree $T'$, modifying $\varphi$ to $\varphi'$, such that $T @@ -689,6 +704,17 @@ 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})$. +This concludes the proof of the lemma, and Theorem +\ref{mso-query-answering-theorem} will be proved if we prove: + +\begin{theorem}\label{relabel-regular-queries-theorem} + Problem \ref{relabel-regular-queries} can be solved in time + \qptime{$O(n)$}{$O(m \log m)$} +\end{theorem} + +The rest of this chapter is dedicated to proving Theorem +\ref{relabel-regular-queries-theorem}. + \section{Relabel Regular Queries on Trees} Fix a tree automaton $A$ and take a $\Sigma$-labeled binary tree $T$. |