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.
Let's figure out how to express the natural numbers in calculus. First of all, they shouldn't have any free variables; we don't want numbers to depend on some undefined . 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 , where is a expression (that varies with the number encoded) containing only the variable . What could look like? The obvious things to try look like and . To encode , we would use the simplest version of this: just . So the examples listed earlier would encode for .
While it's possible to use one of those definitions for numbers, they don't work that well. What type of object is 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 , where we think of as a "function" and as an "object."
So what should be? How about it does nothing to its inputs, and just returns , so . What about ? We have a function and an object, so the natural thing to do is apply the one to the other: . At this point it should be clear how we're going to continue:
And so on, so is the function that, on inputs and , applies to times. Informally, we could write .
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 .
On to defining . It's a function that takes in a number, so let's start with . What should it return? Another number, of course, which starts . Now we should use , which applies to , times. But we want , so we want to apply to , times. If we apply times, and then once more, we can achieve this:
Here gives us , so is . We could do these applications in the other order, first taking and then applying to that times, so
While and are equivalent when is a natural number, they aren't equal; if we plug in for , we have but which is a different function.
To check that works as we want, let's verify that . 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.
Now that we know how to add , let's figure out how to add arbitrary numbers. Suppose we have two numbers and ; remember means "on inputs and , apply to times," and similarly for . We want to apply to times, so how can we accomplish that? If we apply to times, and then more times, it should have the desired effect. Writing this as a term,
Again is of times, and the in front applies to the result more times. We could of course swap and , since addition is commutative.
Let's verify that . We have to write as because we haven't defined infixes in calculus (though we could define to mean .
Multiplication might seem a bit harder. Now, given two numbers and , we want to apply some function to times. If we take a function that applies times, and then apply that function times, we should get something that applies times, times, which is the same as applying times. That is, . The intermediate function that applies times is , or using -conversion, simply . We just need to apply , times, so we can define
or, using -conversion again,
Again multiplication is commutative, so we could swap and to get an equally good definition.
We should have ; let's check this.