\begin{frame}
\small

\begin{example}[Lambda Calculus]
\smallskip
\begin{tabular}{l@{\qquad}lr}
\alert<1>{signature} &
$\alert<1>{\lambda}$ ~ (binds variables) \quad \onslide<2->
$\alert<2>{\cdot}$ ~ (\alert<2>{application}, binary, infix) \\
\onslide<3-> \\
\alert<3>{terms} &
$M ::= x \mid (\lambda x.\,M) \mid (M \cdot M)$ \\
\onslide<4-> \\
\alert<4>{$\alpha$ conversion} & 
$\lambda x.\,x \cdot y \alert<4>{=_{\alpha}} \lambda z.\,z \cdot y$ \\
\onslide<5-> \\
\alert<5,6>{$\beta$ reduction} &
$(\lambda x.\,M) \cdot N \alert<5>{\to_{\beta}} M\alert<6>{[x:=N]}$ \\[1ex]
& \qquad \onslide<6->{replace free occurrences of $x$ in $M$ by $N$} \\
\onslide<7-> \\
\alert<7,8>{rewriting} &
\GREEN{$\begin{array}[t]{@{}r@{~}c@{~}l}
\alert<8>{(\lambda x.\,x \cdot x) \cdot (\lambda x.\,x \cdot x)}
& \onslide<8->{\to} &
\onslide<8->{(\lambda x.\,x \cdot x) \cdot (\lambda x.\,x \cdot x)}
\end{array}$} \\
\onslide<9-> \\
inventor & \href{http://en.wikipedia.org/wiki/Alonzo_Church}%
{\alert<9>{Alonzo Church}} (1936) &
\makebox[0mm][l]{\smash{\includegraphics[height=9ex]{../graphics/church.jpg}}}
\end{tabular}
\end{example}

\end{frame}