Lambda Calculus Encodings
Booleans
The pure \(\lambda\)-calculus contains only functions as values. It is not exactly easy to write large or interesting programs in the pure \(\lambda\)-calculus. We can however encode objects, such as booleans, and integers.
Let us start by encoding constants and operators for booleans. That is, we want to define functions TRUE, FALSE, AND, NOT, IF, and other operators that behave as expected. For example:
$$ \begin{aligned} \texttt{AND~TRUE~FALSE}&=\texttt{FALSE}\\ \texttt{NOT~FALSE}&=\mathrm{TRUE}\\ \texttt{IF~TRUE~}e_1e_2&=e_1\\ \texttt{IF~FALSE~}e_1e_2&=e_2 \end{aligned} $$Let’s start by defining TRUE and FALSE:
$$ \begin{aligned} \texttt{TRUE}&\triangleq\lambda x.\lambda y.x\\ \texttt{FALSE}&\triangleq\lambda x.\lambda y.y \end{aligned} $$Thus, both TRUE and FALSE are functions that take two arguments; TRUE returns the first, and FALSE returns the second. We want the function IF to behave like
$$ \lambda b.\lambda t.\lambda f.\texttt{if~}b=\mathtt{TRUE~then~}t\mathtt{~else~}f. $$The definitions for TRUE and FALSE make this very easy.
$$ \mathtt{IF}\triangleq\lambda b.\lambda t.\lambda f.btf $$Definitions of other operators are also straightforward.
$$ \begin{aligned} \texttt{NOT~}\triangleq&\lambda b.b\texttt{~FALSE~TRUE}\\ \texttt{AND~}\triangleq&\lambda b_1.\lambda b_2.b_1b_2\texttt{~FALSE}\\ \texttt{OR~}\triangleq&\lambda b_1.\lambda b_2.b_1\texttt{~TRUE~}b_2 \end{aligned} $$Church numerals
Church numerals encode a number $n$ as a function that takes $f$ and $x$, and applies $f$ to $x$ $n$ times.
$$ \begin{aligned} \overline{0}&\triangleq\lambda f.\lambda x.x\\ \overline{1}&\triangleq\lambda f.\lambda x.fx\\ \overline{2}&\triangleq\lambda f.\lambda x.f(fx)\\\mathtt{SUCC}&\triangleq\lambda n.\lambda f.\lambda x.f(nfx)\end{aligned} $$In the definition for SUCC, the expression $nfx$ applies $f$ to $x$ $n$ times (assuming that variable $n$ is the Church encoding of the natural number $n$). We then apply $f$ to the result, meaning that we apply $f$ to $x$ $n + 1$ times.