\begin{frame} \frametitle{Computation with Church Numerals} \begin{itemize} \item $\mathsf{plus} = [m\, n\, f\, x]\; m\, f\, (n\, f\, x)$ \smallskip \pause \item $\mathsf{succ} = [n\,f\,x]\; f\, (n\, f\, x)$ \smallskip \pause \item $\mathsf{isZero} = [n]\; n \;(K \; \false)\; \true$ \smallskip \pause \item $\mathsf{pred} = [n\, f\, x]\; n\; ([g\, h]\; h\, (g\, f)) \; (K x)\; I$ \smallskip \pause \item \ldots \end{itemize} \begin{exampleblock}{} Idea behind predecessor: \begin{align*} \mathsf{pred} &= \lambda n.\; \mathsf{fst} \;(n \;f \; z) & z &= (0,0) \\ && f\;(x,y) &= (y,y+1) \end{align*} E.g. $\mathsf{pred} \; \overline{3} = \mathsf{fst} \; f(f(f(0,0))) = \mathsf{fst} \; f(f(0,1)) = \mathsf{fst} \; f(1,2) = \mathsf{fst} \; (2,3) = 2$. \end{exampleblock} \end{frame}