appendix-hk-proofs.tex

\section{Elided proofs from Chapter~3}\label{sec:appendix-hk-proofs}

This appendix contains the proofs for Lemmas~\ref{lemma:03-consistent-yield}
and~\ref{lemma:03-language-partition}. We imply that $\uh = (Q,V,\#,t,e)$ is an
HMM. Moreover, we imply all the definitions introduced in
Section~\ref{sect:03-deriving} to describe $\uh$ in terms of the IO information $\mu_\uh$.
As a prerequisite for both proofs, we shall begin by writing down the languages
of all the grammar states of $H(x)$ and $K$.

\begin{definition}
 Let $\ug = (Q_\ug,q_0,R_\ug)$ be an RTG over $C$. For any grammar state $q\in
 Q_\ug$, the \emph{language of $q$ generated by $\ug$} is given by
 \[
  \lang\ug_q := \pi_C\mbig\kla{D^q(\ug)\cap T_{R_\ug}}.
  \qedhere
 \]
\end{definition}

The mapping $\pi_C\colon T_{R_\ug}(Q_\ug)\to U_C(Q_\ug)$ was introduced as $\pi_\Sigma$ on
page~\pageref{def:02-pi-sigma}. The language $\lang\ug_q$ contains all trees
from $U_C$ that can be generated by applying the grammar's rules, starting from
the state $q$. It especially holds that
\begin{equation}\label{eq:a1}
 \lang\ug = \lang\ug_{q_0}.
\end{equation}
To find $D^q(\ug)\cap T_{R_\ug}$, we first observe that, according to
Definition~\ref{def:02-past}, each $d\in D^q(\ug)$ must have one of two forms,
\[
 d = q \quad\text{or}\quad d = \rho(d_1,\ldots,d_k),
\]
where $\rho=\mbig\kla{q\to c(q_1,\ldots,q_k)}\isin R_\ug$ such that $\rk(c) = k$, and
each $d_i\in D^{q_i}(\ug)$. The first form, $d = q$, is not allowed in
$\lang\ug_q$ since $q\notin T_{R_\ug}$. The second form is admissible, but
because $d\in T_{R_\ug}$, the subtrees $d_i$ may not have positions labeled with
a state $q\in Q_\ug$ either. We therefore have
\[
 D^q(\ug)\cap T_{R_\ug} = \bigcup_{\rho=(q\to c(q_1,\ldots,q_k))\isin R_\ug}
 \mbig\brc{\rho(d_1,\ldots,d_k) \npipe d_1\in D^{q_1}(\ug)\cap T_{R_\ug},\ldots, d_k\in D^{q_k}(\ug)\cap T_{R_\ug}},
\]
from which follows
\begin{equation}
 \label{eq:a2}
 \lang\ug_q = \bigcup_{\rho=(q\to c(q_1,\ldots,q_k))\isin R_\ug}
 \mbig\brc{c(t_1,\ldots,t_k) \npipe t_1\in\lang\ug_{q_1},\ldots, t_k\in\lang\ug_{q_k}},
\end{equation}
when $\pi_C$ is applied on both sides. We can thus describe the languages
$\mbig\lang K$ and $\mbig\lang{H(x)}$ recursively, in terms of the languages
generated from their states.

Let $x\in V^*$. Application of \eqref{eq:a2} to all reachable states in $H(x)$ yields
\begin{align*}
 \mbig\lang{H(x)}_{(T\!,q,x')} &= \bigcup_{q'\in Q}\mbig\brc{\mbig\kla{q',(q,T)}(t_1,t_2) \!\pipe t_1\in\mbig\lang{H(x)}_{(E,q',x')}, t_2\in\mbig\lang{H(x)}_{(T\!,q',\cdr(x'))}}, \\
 \mbig\lang{H(x)}_{(T\!,q,\eps)} &= \mbig\brc{\mbig\kla{\#,(q,T)}} \\
 \intertext{for all $q\in Q_\#$ and $x'\in\suff(x)$, and}
 \mbig\lang{H(x)}_{(E,q,x')} &= \mbig\brc{\mbig\kla{\car(x'),(q,E)}}
\end{align*}
for all $q\in Q$ and $x'\in\suff(x)$. Inserting the last equation into the one above it, we can describe $\mbig\lang{H(x)} = \mbig\lang{H(x)}_{(T\!,\#,x)}$ recursively by
\begin{subequations}\label{eq:a3}\begin{align}
 \mbig\lang{H(x)}_{(T\!,q,x')} &= \bigcup_{q'\in Q}\mBig\brc{\mbig\kla{q',(q,T)}\mBig\kla{\mbig\kla{\car(x'),(q',E)},t} \!\pipe t\in\mbig\lang{H(x)}_{(T\!,q',\cdr(x'))}}, \label{eq:a3a} \\
 \mbig\lang{H(x)}_{(T\!,q,\eps)} &= \mbig\brc{\mbig\kla{\#,(q,T)}} \label{eq:a3b}
\end{align}\end{subequations}
for all $q\in Q_\#$. Analogous application of~\eqref{eq:a2} to all states in
$K$, followed by insertion of the expression for $\lang K_{(E,q)}$ into that of
$\lang K_{(T\!,q)}$, results in
\begin{equation}\label{eq:a4}
 \lang K_{(T\!,q)} = \mbig\brc{\mbig\kla{\#,(q,T)}} \cup \bigcup_{q'\in Q}\bigcup_{v\in V}\mBig\brc{\mbig\kla{q',(q,T)}\mBig\kla{\mbig\kla{v,(q',E)},t} \!\pipe t\in\lang K_{(T\!,q')}}
\end{equation}
for any $q\in Q_\#$. An important observation can be made from the structure of~\eqref{eq:a3}.
\begin{equation}\label{eq:a5}
 \forall x\in V^+, q\in Q\colon\;
 \mbig\lang{H(x)}_{(T,q,\cdr(x))} = \mbig\lang{H\mbig\kla{\cdr(x)}}_{(T,q,\cdr(x))}.
\end{equation}
This equivalence holds because $Q_{\cdr(x)}$ and $R_{\cdr(x)}$ are strict
subsets of $Q_x$ and $R_x$, respectively, and furthermore, because $R_x$ does
not contain any rules not in $R_{\cdr(x)}$ that expand grammar states from
$Q_{\cdr(x)}$. Therefore, we have
\[
 D^q\mbig\kla{H(x)} = D^q\mBig\kla{H\mbig\kla{\cdr(x)}} \quad\forall q\in Q_{\cdr(x)},
\]
from which follows~\eqref{eq:a5}.

\subsection{Proof of Lemma~\ref{lemma:03-consistent-yield}}

\begin{repeatlemma}{\ref{lemma:03-consistent-yield}}
 With the definitions from Section~\ref{sect:03-deriving},
 \[
  \forall x\in X_{\not\bot}\colon\;
  \forall y\in \mbig\lang{H(x)}\colon\;
  \pi_1(y) = x.
 \]
\end{repeatlemma}
\clearpage

\emph{Proof.} Let $x\in X_{\not\bot} = V^*$. We are going to show that
\begin{equation}\label{eq:p11}
 \forall x'\in\suff(x)\cup\brc\eps\colon\;
 \forall q\in Q_\#\colon\;
 \pi_X\mbig\kla{\mbig\lang{H(x)}_{(T,q,x')}} = \brc{x'}.
\end{equation}
by induction over the length of $x'$. The lemma follows from this statement because
\[
 \pi_1\mbig\kla{\mbig\lang{H(x)}}
 = \pi_X\mbig\kla{\mbig\lang{H(x)}}
 = \pi_X\mbig\kla{\mbig\lang{H(x)}_{(T,\#,x)}} \overset{\eqref{eq:p11}}= \brc x.
\]

For the base case, let $x' = \eps$. Then~\eqref{eq:p11} holds because of
\[
 \pi_X\mbig\kla{\mbig\lang{H(x)}_{(T,q,\eps)}}
 \overset{\eqref{eq:a3b}}=
 \mbig\brc{\pi_X\mbig\kla{\#,(q,T)}} = \brc\eps
\]
for any $q\in Q_\#$. For the induction step, let $x'\in\suff(x)$. Since
$\abs{\cdr(x')} < \abs{x'}$, it can be assumed that $\cdr(x')$
satisfies~\eqref{eq:p11} (\emph{induction hypothesis}). Application of $\pi_X$
to both sides of~\eqref{eq:a3a} yields
\begin{align*}
 \pi_X\mbig\kla{\mbig\lang{H(x)}_{(T\!,q,x')}}
 &= \bigcup_{q'\in Q}\mBig\brc{\pi_X\mbig\kla{\car(x'),(q',E)}\pi_X(t) \!\pipe t\in\mbig\lang{H(x)}_{(T\!,q',\cdr(x'))}} \\
 &= \mbig\brc{\car(x')} \cdot \bigcup_{q'\in Q}\mBig\brc{\pi_X(t) \!\pipe t\in\mbig\lang{H(x)}_{(T\!,q',\cdr(x'))}} \\
 &= \mbig\brc{\car(x')} \cdot \bigcup_{q'\in Q}\underbrace{\pi_X\mbig\kla{\mbig\lang{H(x)}_{(T\!,q',\cdr(x'))}}}_{=\brc{\cdr(x')}\text{ by induction hypothesis}} \\
 &= \mbig\brc{\car(x')\cdr(x')} = \mbig\brc{x'}. \tag*{\qed}
\end{align*}

\subsection{Proof of Lemma~\ref{lemma:03-language-partition}}

\begin{repeatlemma}{\ref{lemma:03-language-partition}}
 With the definitions from Section~\ref{sect:03-deriving},
 \[
  \mbig\lang K = \bigcup_{x\in X_{\not\bot}} \mbig\lang{H(x)}.
 \]
\end{repeatlemma}

\emph{Proof.} Let $\pi_Q\colon T_C\to Q_\#$ be the mapping defined by
\[
 \pi_Q(y) := q \text{ such that } y(\eps) = \mbig\kla{a,(q,b)}.
\]
That is, $\pi_Q$ extracts the state $q$ from the label $\mbig\kla{a,(q,b)}$
of the root position of any $y$. As a prerequisite for the actual proof, we are
going to show that
\begin{equation}\label{eq:p21}
 \forall y\in T_C\colon\;
 \mBig\kla{y\in\mbig\lang K_{(T\!,\pi_Q(y))}}
 \text{ iff }
 \mBig\kla{y\in\mbig\lang{H\mbig\kla{\pi_X(y)}}_{(T\!,\pi_Q(y),\pi_X(y))}},
\end{equation}
by structural induction on $y$. According to the definition of the ranked
alphabet $C$, each $y\in T_C$ can have one of three forms,
\begin{align*}
 y_1(v,q) &:= \mbig\kla{v,(q,E)} &&\text{ where } v\in V\text{ and } q\in Q, \\
 y_2(q) &:= \mbig\kla{\#,(q,T)} &&\text{ where } q\in Q_\#, \\
 y_3(q,q',y_e,y_t) &:= \mbig\kla{q',(q,T)}(y_e,y_t) &&\text{ where } q\in Q_\#, q'\in Q, \text{ and } y_e,y_t\in T_C.
\end{align*}
The first two forms are the base cases for the structural induction on $y$,
and the last form represents the inductive step.

\subsubsection*{Base cases}

For any $y=y_1(v,q)$, we have
$\pi_Q(y)=q$ and $\pi_X(y)=v$. We see that~\eqref{eq:p21} holds because
\[
 \mbig\kla{v,(q,E)} \notin \mbig\lang K_{(T\!,q)}
 \quad\text{ and }\quad
 \mbig\kla{v,(q,E)} \notin \mbig\lang{H(v)}_{(T\!,q,v)}.
\]
For any $y=y_2(q)$, we have $\pi_Q(y) = q$ and $\pi_X(y)=\eps$, and \eqref{eq:p21} is
satisfied because
\[
 \mbig\kla{\#,(q,T)} \in \mbig\lang K_{(T\!,q)}
 \quad\text{ and }\quad
 \mbig\kla{\#,(q,T)} \in \mbig\lang{H(\eps)}_{(T\!,q,\eps)}.
\]

\subsubsection*{Induction step: ``$\Rightarrow$'' direction}

Consider any
\[
 y = y_3(q,q',y_e,y_t) = \mbig\kla{q',(q,T)}(y_e,y_t).
\]
such that $y\in\lang K_{(T,q)}$, and let $x:=\pi_X(y)$. Note that $\pi_Q(y) =
q$.  We see from~\eqref{eq:a4} that
\[
 y_t \in \mbig\lang K_{(T\!,q')}
 \quad\text{ and }\quad
 y_e = \mbig\kla{v,(q',E)}
 \quad\text{ where }\quad
 q'\in Q \text{ and } v\in V.
\]
From this follows $x = \pi_X(y) = v\pi_X(y_t)$ and, therefore, $\car(x) = v$
and $\cdr(x)=\pi_X(y_t)$. Since $y_t$ is a substructure of $y$, it can be
assumed to satisfy~\eqref{eq:p21} (\emph{induction hypothesis}). Since
$y_t\in\mbig\lang K_{(T\!,q')}$, we can see from~\eqref{eq:a4} that only
$\pi_Q(y_t) = q'$ is possible. Therefore, by the induction hypothesis,
\[
 y_t
 \in \mbig\lang{H\mbig\kla{\pi_X(y_t)}}_{(T\!,q',\pi_X(y_t))}
 = \mbig\lang{H\mbig\kla{\cdr(x)}}_{(T\!,q',\cdr(x))}.
\]

Because of~\eqref{eq:a5}, this is equivalent to saying that $y_t \in \mbig\lang{H(x)}_{(T\!,q',\cdr(x))}$. We therefore have
\[
 y = \mbig\kla{q',(q,T)}\mBig\kla{\mbig\kla{\car(x),(q',E)},y_t}
\]
with $q\in Q_\#$, $q'\in Q$, and $y_t \in \mbig\lang{H(x)}_{(T\!,q',\cdr(x))}$,
from which follows
\[
 y \in \mbig\lang{H(x)}_{(T\!,q,x)}
\]
because of~\eqref{eq:a3a}.

\subsubsection*{Induction step: ``$\Leftarrow$'' direction}

Consider any $y = y_3(q,q',y_e,y_t)$ such that
$y\in\mbig\lang{H(x)}_{(T\!,\pi_Q(y),x)}$, wherein $x := \pi_X(y)$. Since
$\pi_Q(y) = q$, it follows from~\eqref{eq:a3} that
$y_e = \mbig\kla{\car(x),(q',E)}$ and
$y_t \in \mbig\lang{H(x)}_{(T\!,q',\cdr(x))}$.
Because of~\eqref{eq:a5}, the second statement is equivalent to
\[
 y_t \in \mbig\lang{H\mbig\kla{\cdr(x)}}_{(T\!,q',\cdr(x))}.
\]
From~\eqref{eq:a3}, we see that $\pi_Q(y_t)$ must be $q'$. Since $y_t$ is a
substructure of $y$, it can be assumed to satisfy~\eqref{eq:p21}, from which
follows that $y_t \in \mbig\lang K_{(T\!,q')}$. According to~\eqref{eq:a4}, it
therefore holds that $y\in\mbig\lang K_{(T\!,q)}$. The proof for~\eqref{eq:p21}
is thereby complete.

\subsubsection*{Conclusion of the proof}

To finally derive Lemma~\ref{lemma:03-language-partition}, we first note that
\begin{equation}\label{eq:p22}
 \pi_Q\mbig\kla{\mbig\lang K_{(T\!,\#)}} = \brc\#
 \quad\text{ and }\quad
 \pi_Q\mbig\kla{\mbig\lang{H(x)}_{(T\!,\#,x)}} = \brc\#
\end{equation}
for every $x\in X_{\not\bot}$, which follows from~\eqref{eq:a4} and~\eqref{eq:a3}, respectively.
We can thus expand $\lang K$ into
\begin{align*}
 \mbig\lang K
 = \mbig\lang K_{(T\!,\#)}
 &= \mbig\brc{y\in \pi_Q^{-1}(\#) \npipe y\in\mbig\lang K_{(T\!,\#)}} \\
 &= \mbig\brc{y\in \pi_Q^{-1}(\#) \npipe y\in\mbig\lang K_{(T\!,\pi_Q(y))}}.
\end{align*}
By using~\eqref{eq:p21}, we obtain
\begin{align*}
 \mbig\lang K
 &= \mbig\brc{y\in \pi_Q^{-1}(\#) \npipe y\in\mbig\lang{H\mbig\kla{\pi_X(y)}}_{(T\!,\pi_Q(y),\pi_X(y))}} \\
 &= \mbig\brc{y\in \pi_Q^{-1}(\#) \npipe y\in\mbig\lang{H\mbig\kla{\pi_X(y)}}_{(T\!,\#,\pi_X(y))}}.
\end{align*}

To obtain the desired structure, we split this set into one set per yield $x = \pi_X(y)$.
\begin{align*}
 \mbig\lang K
 &= \bigcup_{x\in X_{\not\bot}} \mbig\brc{y\in \pi_Q^{-1}(\#) \npipe y\in\mbig\lang{H\mbig\kla{\pi_X(y)}}_{(T\!,\#,\pi_X(y))}, x = \pi_X(y)} \\
 &= \bigcup_{x\in X_{\not\bot}} \mbig\brc{y\in \pi_Q^{-1}(\#) \npipe y\in\mbig\lang{H(x)}_{(T\!,\#,x)}, x = \pi_X(y)}.
\end{align*}

Because of~\eqref{eq:p22}, each $H(x)_{(T,\#,x)}$ is a subset of $\pi_Q^{-1}(\#)$. We can therefore simplify this to
\[
 \mbig\lang K
 = \bigcup_{x\in X_{\not\bot}} \mbig\brc{y\in \mbig\lang{H(x)}_{(T\!,\#,x)} \npipe x = \pi_X(y)}
 = \bigcup_{x\in X_{\not\bot}} \mbig\brc{y\in \mbig\lang{H(x)} \npipe x = \pi_X(y)},
\]
which is equivalent to Lemma~\ref{lemma:03-language-partition} because of Lemma~\ref{lemma:03-consistent-yield}.\qed

\endinput
which is equivalent to the desired statement,
\[
 \mbig\lang K = \bigcup_{x\in X_{\not\bot}} \mbig\lang{H(x)},
\]
because of Lemma~\ref{lemma:03-consistent-yield}.\qed