\begin{frame}
  \frametitle{Computable Functions in Combinatory Logic}
  
  The class of $\mu$-recursive (found by Kleene) functions is build from:
  \begin{itemize}
    \item \emph{zero}: 0
      \pause\hfill\textcolor{red!50!black}{in CL: $KI$}
    \pause
    \item \emph{successor}: S(n) = n+1
      \pause\hfill\textcolor{red!50!black}{in CL: $[n\,f\,x]\; f\, (n\, f\, x)$}
    \pause
    \item \emph{projection functions}: $\Pi^i_k(n_1,\ldots,n_k) = n_i$
      \pause\hfill\textcolor{red!50!black}{in CL: $\mathsf{pair},\;\mathsf{fst},\mathsf{snd},\ldots$}
    \pause
    \item \emph{composition}: $f(x_1,\ldots,x_n) = g(h_1(\vec{x}),\ldots,h_m(\vec{x}))$\\[.5ex]
      \pause\hfill\textcolor{red!50!black}{in CL: $[\vec{x}]g(h_1\;\vec{x},\ldots,h_m\;\vec{x})$}
    \pause
    \item \emph{primitive recursion}:
      $f(0,\vec{x}) = g(\vec{x})$\\
      \hspace{18ex} $f(S(n),\vec{x}) = h(f(n,\vec{x}),n,\vec{x})$\\[.5ex]
      \pause\hfill\textcolor{red!50!black}{in CL: implicit definition $f\;n\;\vec{x}\;=\;\mathsf{isZero}\; n\;(g\;\vec{x})\;(h\; (f\;(\mathsf{pred}\; n)\;\vec{x})\;n\;\vec{x})$}
      \pause
    \item \emph{unbounded search}:
       $\mu u. [f(u,\vec{x}) = 0]$ is the least $u$ such that $f(u,\vec{x}) = 0$\\
      \pause\hfill\textcolor{red!50!black}{in CL: implicit definition $\mu\;u\;f\;\vec{x}\;=\;\mathsf{isZero}\; (f\;u\;\vec{x})\; u\; (\mu\;(\mathsf{succ}\; u)\;f\;\vec{x})$}
  \end{itemize}
  \pause
  \medskip
  \begin{block}{}
  Every computable function can be computed in combinatory logic.
  \end{block}
\end{frame}