\begin{frame}{Pushdown Automata}
  \begin{block}{}
    A \emph{nondeterministic pushdown automaton} (\emph{NPDA}) is a tuple\vspace{-0.5ex}
    \begin{talign}
      M = (Q,\Sigma,\Gamma,\delta,q_0,z,F)
    \end{talign}
    \vspace{-3.5ex}
    \begin{itemize}\setlength{\itemsep}{-0.5ex}
    \item $Q$ is a finite set of states
    \item $\Sigma$ is a finite input alphabet
    \item \alert{$\Gamma$ is a finite stack alphabet}
    \item \alert{$\delta : Q \times (\Sigma \cup \{\, \lambda \,\}) \times \alert{\Gamma} \to 2^{Q \times \alert{\Gamma^*}}$} 
      
      the transition function, where $\delta(q,\alpha,b)$ is always finite
    \item $q_0 \in Q$ the starting state
    \item \alert{$\alert{z} \in \Gamma$ the stack starting symbol}
    \item $F \subseteq Q$ a set of final states
    \end{itemize}
  \end{block}

  Initially, the stack content is $z$.
  \pause
  
  \begin{goal}{}
    If $(q',v) \in \delta(q,\alpha,b)$, this means that 
    \begin{itemize}
      \vspace{-0.25ex}
      \item from state \alert{$q$} with input \alert{$\alpha w$} and stack $\alert{b}u$ 
      \vspace{-0.5ex}
    \end{itemize}
    the automaton can do a transition to 
    \begin{itemize}
      \vspace{-0.25ex}
      \item state \alert{$q'$} with input \alert{$w$} and stack $\alert{v}u$.
      \vspace{-0.25ex}
    \end{itemize}
  \end{goal}
\end{frame}