\begin{frame}{From  LBA's to Context-Sensitive Grammars}
  \begin{goal}{Theorem}
    For every LBA $M$, the language $L(M)$ is context-sensitive.
  \end{goal}
  
  \pause
  \vfill
  
  \begin{block}{Proof sketch.}
    As before, build an unrestricted grammar $G$ with $L(G) = L(M)$.
    \pause\medskip
    
    All productions rules are context-sensitive, except for:
    \begin{talign}
      \alert{\Box \to \lambda}
    \end{talign}
    \pause
    However, a linear bounded automaton does not use $\Box$\,!\\
    (It never leaves the borders of the input word.)
    \pause\medskip

    Therefore, we can drop
    \begin{itemize}
      \item the rule $\Box \to \lambda$\pause, and
      \item the rules $S\to V_\Box^\Box S \mid S V_\Box^\Box$.
    \end{itemize}
    \pause
    (In step 1, we derive from $S$ 
    a word $V_{q_0[a_1}^{a_1}V_{a_2}^{a_2}\cdots V_{a_{n-1}}^{a_{n-1}}V_{a_n]}^{a_n}$.)
  \end{block}
\end{frame}