The Genius of Alonzo Church: Numbers in Lambda Calculus

So, now, time to move on to doing interesting stuff with lambda calculus. To start with, for convenience, I'll introduce a bit of syntactic sugar to let us name functions. This will make things easier to read as we get to complicated stuff.

To introduce a "global" function (that is a function that we'll use throughout our lambda calculus introduction without including its declaration in every expression), we'll use a "let" expression:

let square = lambda x . x^2

This declares a function named "square", whose definition is lambda x . x^2. If we had an expression "square 4", the "let" above means that it would effectively be treated as if the expression were:

(lambda square . square 4)(lambda x . x^2)

In some of the examples, I used numbers and arithmetic operations. But numbers don't really exist in lambda calculus; all we really have are functions! So we need to invent some way of creating numbers using functions. Fortunately, Alonzo Church, the genius who invented the lambda calculus worked out how to do that. His version of numbers-as-functions are called Church Numerals.

In Church numerals, all numbers are functions with two parameters:

1. Zero is "lambda s z . z".
   
2. One is "lambda s z . s z".
   
3. Two is "lambda s z . s (s z)".
   
4. For any number "n", it's Church numeral is a function which applies its first parameter to its second parameter "n" times.
   

A good way of understanding this is to think of "z" as being a a name for a zero-value, and "s"as a name for a successor function. So zero is a function which just returns the "0" value; one is a function which applies the successor function once to zero; two is a function which applies successor to the successor of zero, etc.

Now - watch this; if we want to do addition, x + y, we need to write a function with four parameters; the two numbers to add; and the "s" and "z" values we want in the resulting number:
let add = lambda s z x y . x s (y s z)

Let's curry that, to separate the two things that are going on. First, it's taking two parameters which are the two values we need to add; second, it needs to normalize things so that the two values being added end up sharing the same binding of the zero and successor values.
let add = lambda x y. (lambda s z . (x s (y s z)))

Look at that for a moment; what that says is, to add x and y: create the church numeral "y" using the parameters "s" and "z". Then apply x to the church numeral y, using the new church numeral "y" defined in "s" and "z". That is: a number is a function which adds itself to another number.

Let's look a tad closer, and run through the evaluation of 2 + 3:

add (lambda s z . s (s z)) (lambda s z . s (s (s z))) news newz

To make things easier, let's alpha 2 and 3, so that "2" uses "s2" and "z2", and 3 uses "s3" and "z3";

add (lambda s2 z2 . s2 (s2 z2)) (lambda s3 z3 . s3 (s3 (s3 z3)))

Now, let's do replace "add" with its definition:

(lambda x y .(lambda s z. (x s y s z))) (lambda s2 z2 . s2 (s2 z2)) (lambda s3 z3 . s3 (s3 (s3 z3)))

Now, let's do a beta on add:

lambda s z . (lambda s2 z2 . s2 (s2 z2)) s (lambda s3 z3 . s3 (s3 (s3 z3)) s z)

And now let's beta the church numberal for three. This basically just "normalizes" three: it replaces the successor and zero function in the definition of three with the successor and zero functions from the parameters to add.

lambda s z . (lambda s2 z2 . s2 (s2 z2)) s (s (s (s z)))

Now.. Here comes the really neat part. Beta again, this time on the lambda for two. Look at what we're going to be doing here: two is a function which takes two parameters: a successor function, and zero function. To add two and three, we're using the successor function from add function; and we're using the result of evaluating three as the value of the zero!:

lambda s z . s (s (s (s (s z))))

And we have our result: the church numeral for five!