Formally show automaton

2 files changed, 84 insertions, 9 deletions

diff --git a/definitions.sty b/definitions.sty
index 829564d..7d06de4 100644
--- a/definitions.sty
+++ b/definitions.sty
@@ -29,6 +29,9 @@
 
 \newcommand{\definedterm}[1]{\emph{#1}}
 
+\newcommand{\leftsymbol}{\mathsf{left}}
+\newcommand{\rightsymbol}{\mathsf{right}}
+
 \newcommand{\data}[1]{\mathsf{#1}}
 \newcommand{\infixtable}{\data{in}}
 \newcommand{\posttable}{\data{post}}
diff --git a/mgr.tex b/mgr.tex
index c2d3405..1c1644b 100644
--- a/mgr.tex
+++ b/mgr.tex
@@ -961,15 +961,87 @@ path from the hole $w$ up to the root $v$. What we claim is that the question
 ``if $A$'s state in $w$ is $q$, is the state in $v$ going to be $q'$?'' can be
 answered with a branch infix regular query.
 
-This is the case because a finite automaton can compute $A$'s states along the
-path from $w$ to $v$ when given access to each of the node's label, state of its
-children in the run of $A$ on the original labeling of $T$, and the information
-whether this node is a left or right child of its parent. Thus the language
-$L_{q, q'}$ over alphabet $Q \times \Sigma \times Q \times \{ left, right \}$ of
-proper semgents of a run of $A$ that start in state $q$ and end in state $q'$ is
-a regular language. Our algorithm for branch infix regular queries dealt with
-top-down queries, but regular languages are reversible. So we preprocess $T$ for
-branch infix regular queries for each language $L_{q, q'}^R$.
+\subsection{Computing the root state of a subtree with a hole}
+
+Consider the subtree of $x$ with hole $y$. It can be divided into the following
+components:
+
+\begin{itemize}
+    \item $y$'s subtree
+    \item A path from $y$ up to $x$, notate it as $x_0 = y, x_1, \ldots, x_p =
+        x$.
+    \item For each $i$ from 1 to $p$, the subtree of $x_i$'s child that doesn't
+        lie on the path from $y$ to $x$. Let $x_i'$ be the child of $x_i$ that
+        doesn't lie on the $y$ to $x$ path.
+\end{itemize}
+
+With our bottom-up computation, we've already computed the new state in $y$.
+There have been no relabelings in the subtrees of the $x_i'$'s, so we can get
+their states from the precomputed run of $A$ on the original tree. Now consider
+how, using all this information, we could easily compute $x$'s new state.
+
+To compute the state in $x_1$, all we need is $x_1$'s label and the states of
+$x_0$ and $x_1'$ -- $x_1$'s children. This is all information we already have.
+So going up the path from $y$ to $x$, we can compute each $x_i$'s new state
+from its label and the states of $x_{i-1}$ and $x_i'$. The computation as just
+described would take time linear in $p$, the length of the path, but the
+computation is simple enough that it could be performed by a finite state word
+automaton, allowing us to use our result from Chapter \ref{branchinfix}. To show
+this formally, consider the alphabet $\Sigma' := Q \times \Sigma \times Q \times
+\{ \leftsymbol, \rightsymbol \}$. A word over this alphabet can be used to
+represent a subtree with a hole. A subtree with hole as described above would be
+represented by word $a_0 a_1 \ldots a_p$ where
+
+\begin{itemize}
+    \item Each $a_i$ is a quadruple from $\Sigma'$, $\langle p_i, b_i, q_i, d_i
+        \rangle$ (with $p_i, q_i \in Q$, $b_i \in \Sigma$, $d_i$ either
+        $\leftsymbol$ or $\rightsymbol$).
+    \item $b_i$ is the original label of $x_i$.
+    \item $p_i$ and $q_i$ are the states of $x_i$'s children in the precomputed
+        run of $A$ over $T$.
+    \item $d_i$ encodes the information of whether $x_i$ is the left or right
+        child of its parent.
+\end{itemize}
+
+Note that this is slightly more information than we previously mentioned: in our
+description of the computation above we only cared about the state of the child
+not on the $y$ to $x$ path. The information about the other child is redundant
+when considering just one subtree with hole and can be ignored when doing
+computation on that particular subtree with hole. But we will keep information
+about both children so that we can handle questions about any subtree with hole.
+
+Now consider the language $L_{q,q'} \subseteq \Sigma'^*$ of words $a_0 \ldots
+a_p$ such that the subtree with hole encoded by such a word, if the hole's state
+were set to $q$, would lead to $A$ arriving at state $q'$ after running up it.
+
+\begin{lemma}
+    $L_{q,q'}$ is a regular language.
+\end{lemma}
+
+Let's explicitly construct the automaton recognizing $L_{q,q'}$. Its state
+space will be $\{ \mathsf{initial} \} \cup Q \times \{ \leftsymbol, \rightsymbol
+\}$, states other than $\mathsf{initial}$ encoding, for the vertex represented
+by the previously read letter, what state we arrived in at it and whether it was
+the current vertex's left or right child. The automaton works as follows:
+
+\begin{enumerate}
+    \item In the initial state $\mathsf{initial}$, read $a_0 = \langle p_0, b_0,
+        q_0, d_0 \rangle$, set the state to $\langle q, d_0 \rangle$.
+    \item Now when reading letter $\langle p_i, b_i, q_i, d_i \rangle$ in state
+        $\langle r, d \rangle$, if $d$ if $\leftsymbol$, use $A$'s transition
+        function $\delta$ to compute the new tree state as $\delta(r, b_i, q_i)$
+        (the previously computed tree state is of our left child's, and our
+        right child's comes from the current letter). If $d$ is $\rightsymbol$,
+        the new tree state will instead be $\delta(p_i, b_i, r)$. Store this and
+        $d_i$ as the new state.
+    \item Accept if the final tree state is $q'$.
+\end{enumerate}
+
+Our algorithm for branch infix regular queries dealt with top-down queries, but
+regular languages are reversible. So we preprocess $T$ for branch infix regular
+queries for each language $L_{q, q'}^R$. Now a query about whether the word on
+the path from $x$ down to $y$ belongs to $L_{q, q'}^R$ is the same as asking if
+the word from $y$ up to $x$ belongs to $L{q,q'}$.
 
 Now to compute $v$'s state after the relabeling of $T$, given we've already
 computed $w$'s new state $q$, take $v'$ -- $v$'s child in the direction of $w$,