38/250
\begin{frame}
\small

\begin{example}[Combinatory Logic]
\smallskip
\begin{tabular}{l@{\qquad}lr}
\alert<1>{signature} &
\alert<1>{$\m{S}$ ~ $\m{K}$ ~ $\m{I}$} ~ (constants) \quad
\onslide<2-> \alert<2>{$\cdot$} ~ (application, binary, infix) \\
\onslide<3-> \\
\alert<3>{terms} &
\GREEN{$\m{S}$ \quad $((\m{K} \cdot \m{I}) \cdot \m{I}) \cdot \m{S}$ \quad
$(x \cdot z) \cdot (y \cdot z)$} \\
\onslide<4-> \\
\alert<4>{rewrite rules} &
\GREEN{$\begin{array}[t]{r@{~}c@{~}l@{\qquad\qquad}r@{~}c@{~}l}
\m{I} \cdot x & \to & x \\[.5ex]
(\m{K} \cdot x) \cdot y & \to & x \\[.5ex]
((\m{S} \cdot x) \cdot y) \cdot z & \to & 
(x \cdot z) \cdot (y \cdot z)
\end{array}$} \\
\onslide<5-> \\
\alert<5-7>{rewriting} &
\GREEN{$\begin{array}[t]{@{}r@{~}c@{~}l}
\alert<6>{((\m{S} \cdot \m{K}) \cdot \m{K}) \cdot x}
& \onslide<6->{\to} &
\onslide<6->{\alert<7>{(\m{K} \cdot x) \cdot (\m{K} \cdot x)}} \\
& \onslide<7->{\to} &
\onslide<7->{x}
\end{array}$} \\
\onslide<8-> \\
inventor & \href{http://en.wikipedia.org/wiki/Moses_Schoenfinkel}%
{\alert<8>{Moses Sch\"onfinkel}} (1924) &
\makebox[0mm][l]{\smash{\includegraphics[height=9ex]{../graphics/moses.jpg}}}
\end{tabular}
\end{example}

\end{frame}