\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}