\begin{frame}{Context-Sensitive Languages are Recursive}
  \begin{goal}{Theorem}
    Context-sensitive languages are recursive.
  \end{goal}
  \pause
  
  \begin{proof}
    Let $G$ be a context-sensitive grammar.
    \pause\medskip

    We argue that there exists a Turing machine $M$ accepting $L(G)$.    
    \pause\medskip

    Let $w \in T^*$ be the input word. 
    \pause\medskip

    The are finitely words over $V \cup T$ of length $\leq |w|$:
    \begin{itemize}
    \pause
      \item $M$ can compute the set $\{\, u \mid S \Rightarrow^* u,\; |u| \le |w| \,\}$
    \pause
      \item $M$ accepts $w$ if $w$ is among these words.\\
        (Otherwise $M$ halts in a non-accepting state.)
    \end{itemize}
    \pause
    Then \alert{$M$ accepts $L(G)$} and \alert{always reaches a halting state}.
  \end{proof}
\end{frame}