In lambda calculus, the only objects we can work with are expressions, which represent functions. So how can we talk about, and perform computations on, more familiar objects like numbers? We'll have to come up with a way to encode numbers, and operations on them, as $λ$ expressions.

Natural numbers

Let's figure out how to express the natural numbers $0, 1, 2, \dots$ in $λ$ calculus. First of all, they shouldn't have any free variables; we don't want numbers to depend on some undefined $x$ . So, like any $λ$ expression with no free variables, they need to start with a $λ$ . That is, they need to be functions.

Say they only take in one input, so they're $λ x . M$ , where $M$ is a $λ$ expression (that varies with the number encoded) containing only the variable $x$ . What could $M$ look like? The obvious things to try look like $x (x (x x))$ and $((x x) x) x$ . To encode $0$ , we would use the simplest version of this: just $x$ . So the examples listed earlier would encode for $3$ .

While it's possible to use one of those definitions for numbers, they don't work that well. What type of object is $x$ supposed to be? Should it be a function, or the input to a function? (Yes, everything in $λ$ calculus can be both, but it can still help to think of those two types differently.) Instead, we'll have each natural number be a function on two inputs, of the form $λ f . λ x . M$ , where we think of $f$ as a "function" and $x$ as an "object."

So what should $0$ be? How about it does nothing to its inputs, and just returns $x$ , so $0 = λ f . λ x . x$ . What about $1$ ? We have a function and an object, so the natural thing to do is apply the one to the other: $1 = λ f . λ x . f x$ . At this point it should be clear how we're going to continue:

$2 = λ f . λ x . f (f x)$
$3 = λ f . λ x . f (f (f x))$
$4 = λ f . λ x . f (f (f (f x)))$

And so on, so $n$ is the function that, on inputs $f$ and $x$ , applies $f$ to $x$ $n$ times. Informally, we could write $n = λ f . λ x . f^{n} (x)$ .

Operations on numbers

We've defined natural numbers, but so far they aren't doing anything. We expect numbers to be able to be added and multiplied, so let's figure out how to express those in $λ$ calculus. We'll start easy: with the successor function $S (n) = n + 1$ .

Successor

On to defining $S$ . It's a function that takes in a number, so let's start with $λ n$ . What should it return? Another number, of course, which starts $λ f . λ x$ . Now we should use $n$ , which applies $f$ to $x$ , $n$ times. But we want $n + 1$ , so we want to apply $f$ to $x$ , $n + 1$ times. If we apply $f$ $n$ times, and then once more, we can achieve this:

$S = λ n . λ f . λ x . f (n f x) .$

Here $(n f x)$ gives us $f^{n} (x)$ , so $f (n f x)$ is $f (f^{n} (x)) = f^{n + 1} (x)$ . We could do these applications in the other order, first taking $f x$ and then applying $f$ to that $n$ times, so

$S^{'} = λ n . λ y . λ x . n f (f x) .$

While $S$ and $S^{'}$ are equivalent when $n$ is a natural number, they aren't equal; if we plug in $λ a . λ b . a$ for $n$ , we have $\begin{matrix} S (λ a . λ b . a) & = λ f . λ x . f ((λ a . λ b . a) f x) = λ f . λ x . f f \end{matrix}$ but $\begin{matrix} S^{'} (λ a . λ b . a) & = λ f . λ x . (λ a . λ b . a) f (f x)) = λ f . λ x . f \end{matrix}$ which is a different function.

To check that $S$ works as we want, let's verify that $S 3 = 4$ . For these worked examples, it's probably much more informative if you work through them yourself; they're provided here so you can check that you did it right.

Worked example: successor

$\begin{matrix} S 3 & = (λ n . λ f . λ x . f (n f x)) (λ f . λ x . f (f (f x))) = (λ f . λ x . f ((λ f . λ x . f (f (f x))) f x)) = (λ f . λ x . f (f (f (f x))) = 4 \end{matrix}$

Addition

Now that we know how to add $1$ , let's figure out how to add arbitrary numbers. Suppose we have two numbers $m$ and $n$ ; remember $m$ means "on inputs $f$ and $x$ , apply $f$ to $x$ $m$ times," and similarly for $n$ . We want $m + n$ to apply $f$ to $x$ $m + n$ times, so how can we accomplish that? If we apply $f$ to $x$ $n$ times, and then $m$ more times, it should have the desired effect. Writing this as a $λ$ term,

$+ = λ m . λ n . λ f . λ x . m f (n f x)$

Again $n f x$ is $f$ of $x$ $n$ times, and the $m f$ in front applies $f$ to the result $m$ more times. We could of course swap $m$ and $n$ , since addition is commutative.

Let's verify that $2 + 3 = 5$ . We have to write $2 + 3$ as $+ 23$ because we haven't defined infixes in $λ$ calculus (though we could define $m + n$ to mean $+ m n$ .

Worked example: addition

$\begin{matrix} + 23 & = (λ m . λ n . λ f . λ x . m f (n f x)) (λ f . λ x . f (f x)) (λ f . λ x . f (f (f x))) = λ f . λ x . (λ f . λ x . f (f x)) f ((λ f . λ x . f (f (f x))) f x) = λ f . λ x . (λ f . λ x . f (f x)) f (f (f (f x))) = λ f . λ x . f (f (f (f (f x)))) = 5 \end{matrix}$

Multiplication

Multiplication might seem a bit harder. Now, given two numbers $m$ and $n$ , we want to apply some function $f$ to $x$ $m \times n$ times. If we take a function that applies $f$ $n$ times, and then apply that function $m$ times, we should get something that applies $f$ $n$ times, $n$ times, which is the same as applying $f$ $m \times n$ times. That is, $(f^{n})^{m} (x) = f^{m \times n} (x)$ . The intermediate function that applies $f$ $n$ times is $λ x . n f x$ , or using $η$ -conversion, simply $n f$ . We just need to apply $n f$ , $m$ times, so we can define

$\times = λ m . λ n . λ f . λ x . m (n f) x$

or, using $η$ -conversion again,

$\times = λ m . λ n . λ f . m (n f) .$

Again multiplication is commutative, so we could swap $m$ and $n$ to get an equally good definition.

We should have $\times 23 = 6$ ; let's check this.

Worked example: multiplication

$\begin{matrix} \times 23 & = (λ m . λ n . λ f . m (n f)) (λ f . λ x . f (f x)) (λ f . λ x . f (f (f x))) = λ f . (λ f . λ x . f (f x)) ((λ f . λ x . f (f (f x))) f) = λ f . (λ f . λ x . f (f x)) (λ x . f (f (f x))) = λ f . λ x . (λ x . f (f (f x))) ((λ x . f (f (f x))) x) = λ f . λ x . (λ x . f (f (f x))) (f (f (f x))) = λ f . λ x . f (f (f (f (f (f x)))))) = 6 \end{matrix}$

(this page is unfinished)

Church encoding