Numbers in The Lambda Calculus

God created the natural numbers. All else is the work of man.

Leopold Kronecker

We’ve got lists and with lists we can do pretty much any data structure we like. However, in computing, we also need numbers. Usually, numbers are thought of as fairly basic entities with respect to computing, but, in the Lambda Calculus they are fairly high level concepts, even the natural numbers.

Church Numerals

We could represent numbers as lists. The number 3 might be represented by a list of length three, for example λf.f 1 (λf.f 1 (λf.f 1 (λf.true))) is 3, being a list of three elements, all of which are 1 in this case. The use of 1 as the element is not important, only the length of the list. λf.f apple (λf.f pear (λf.f banana (λf.true))) also represents 3.

We’re not going to do that though, we are going to use Church numerals. The basis of a Church numeral is that it is a function that applies another function n times, where n is the number the Church numeral represents. The Church numeral that represents 3, applies its first argument three times over to its second argument. As an example, 3 (cons x) nil produces a list with three elements, each of which is x. 3 applies cons x three times to its second argument.

3 is defined as  λf.λx.f (f (f x)). In general, the numeral n is defined as λf.λx.fn x. The notation fn means f applied to its argument n times successively, or the composition of f with itself n times. The first few Church numerals are:

let 0 = λf.λx.x

let 1 = λf.λx.f x

let 2 = λf.λx.f (f x)

let 3 = λf.λx.f (f (f x))

Let’s start by considering three basic operations:

• isZero – tests if a numeral is zero: isZero 0 →_β true, isZero n →_β false (n is a Church numeral)
• pred – the predecessor of a numeral: pred 3 →_β 2
• succ – the successor of a numeral: succ 3 →_β 4

isZero

Before we discuss what the function isZero does, what does 0 look like. In general, a Church numeral looks like this: λf.λx.fn x where n is the number represented. λf.λx.f0 x is therefore the representation of 0 and f0 means no applications of f. So 0 is λf.λx.x. ie. a function that ignores its first argument and returns its second unchanged. So, for isZero 0 to be true, it should take 0 and apply it to two arguments, the first is a function we don’t care about and the second is true. e.g.

let isZero1 = λn.n something true

I called it isZero1 because it’s not our final attempt at defining the function. Let’s try it

> isZero1 0
: (λn.n something (true)) (0)
> 
: (0) something (true)
> 
: (λx.x) (true)
> 
: true

What if we apply isZero to some other numeral.

> isZero1 1
: (λn.n something (true)) (1)
> 
: (1) something (true)
> 
: (λx.something x) (true)
> 
: something (true)

in this example, we test isZero1 1. It reduces to something true. It won’t reduce any further because something is a free variable. Let’s try isZero 2.

> isZero1 2
: (λn.n something (true)) (2)
> 
: (2) something (true)
> 
: (λx.something (something x)) (true)
> 
: something (something (true))

This means that, if we replace something with a function that always evaluates to false no matter what its argument is, applying isZero to any non zero numeral will always evaluate to false. The final definition of isZero is thus:

let isZero = λn.n (λx.false) true

> isZero 0
: (λn.n (λx.false) (true)) (0)
> 
: (0) (λx.false) (true)
> 
: (λx.x) (true)
> 
: true

> isZero 2
: (λn.n (λx.false) (true)) (2)
> 
: (2) (λx.false) (true)
> 
: (λx.(λx.false) ((λx.false) x)) (true)
> 
: (λx.false) ((λx.false) (true))
> 
: false

Succ

The successor function applied to a numeral n gives us the next biggest numeral.

succ (λf.λx.fn x) →_β (λf.λx.fn+1 x)

We can take advantage of two things here. The first is the a numeral is a function that takes two arguments: another function f that is applied n times over and and an arbitrary argument to which f is applied n times over. The second is that fn+1 x is fn (f x). succ needs to apply two arguments a and b such that

(λf.λx.fn x) a b →_β fn (f x)

This works if we set a to f and b to f x. f and x are arguments to the numeral n so they need to be arguments to succ n too. This gives us the complete definition of succ:

let succ = λn.λf.λx.n f (f x)

Let’s try it.

> succ 1
: (succ) (1)
> 
: λf.λx.(1) f (f x)
> 
: λf.λx.(λx.f x) (f x)
> 
: λf.λx.f (f x)
> succ 3
: (succ) (3)
> 
: λf.λx.(3) f (f x)
> 
: λf.λx.(λx.f (f (f x))) (f x)
> 
: λf.λx.f (f (f (f x)))
> 
: λf.λx.f (f (f (f x)))
> succ (succ 2)
: (succ) ((succ) (2))
> 
: λf.λx.(succ) (2) f (f x)
> 
: λf.λx.(λf.λx.(2) f (f x)) f (f x)
> 
: λf.λx.(λx.(2) f (f x)) (f x)
> 
: λf.λx.(2) f (f (f x))
> 
: λf.λx.(λx.f (f x)) (f (f x))
> 
: λf.λx.f (f (f (f x)))

In the first case, we get the Church numeral for 2 and in the second two cases we get the church numeral for 4.

Pred

Figuring out the predecessor function is much harder. Undoing an application of a function is pretty hard, not to say impossible. However, we do know that pred n = succn-1 0, or (n-1) succ 0. Now you may not think that helps very much since, to find n-1 we need the predecessor function which is what we are looking for. Or do we.

If you are starting from n and looking for its predecessor you have nothing to go on, but, if you start from 0 and create n by successive applications of succ, you can, if you like, record the result of each application of succ. If you’ve got the history of all your applications of succ, you can reach back into it to find the predecessor of n. We can do this with a list. Each time we apply succ to a numeral, we record it at the head of a list and then when we have applied succ n times, the second element of the list is the predecessor of n.

First of all, we need to make a list containing just zero. That’s easy:

let zeroList = λf.f 0 nil

Now we need a function that will extract the head of a list, apply succ and create a new list with the successor of the head as its head and the entire original list as its tail.

let addSuccHead = λl.cons (succ (head l)) l

Let’s see what that does.

> addSuccHead zeroList
: (λl.cons (succ (head l)) l) (λf.f 0 (λf.true))
> 
: cons (succ (head (λf.f 0 (λf.true)))) (λf.f 0 (λf.true))
> 
: (λt.λf.f (succ (head (λf.f 0 (λf.true)))) t) (λf.f 0 (λf.true))
> 
: λf.f (succ (head (λf.f 0 (λf.true)))) (λf.f 0 (λf.true))
> 
: λf.f (λf.λx.head (λf.f 0 (λf.true)) f (f x)) (λf.f 0 (λf.true))
> 
: λf.f (λf.λx.(λf.f 0 (λf.true)) (λx.λy.x) f (f x)) (λf.f 0 (λf.true))
> 
: λf.f (λf.λx.(λx.λy.x) 0 (λf.true) f (f x)) (λf.f 0 (λf.true))
> 
: λf.f (λf.λx.(λy.0) (λf.true) f (f x)) (λf.f 0 (λf.true))
> 
: λf.f (λf.λx.0 f (f x)) (λf.f 0 (λf.true))
> 
: λf.f (λf.λx.(λx.x) (f x)) (λf.f 0 (λf.true))
> 
: λf.f (λf.λx.f x) (λf.f 0 (λf.true))
> 
: λf.f (λf.λx.f x) (λf.f 0 (λf.true))

That looks promising. We have a list consisting of the Church numeral for 1 and the Church numeral for 0. (Since version 1.3.1 the Lambda Calculator doesn’t expand let definitions until it has to in order to make the expressions more readable). What about multiple applications of addSuccHead? Let’s try it:

> 3 addSuccHead zeroList
: 3 (λl.cons (succ (head l)) l) (λf.f 0 (λf.true))
> 
: (λx.(λl.cons (succ (head l)) l) ((λl.cons (succ (head l)) l) ((λl.cons (succ (head l)) l) x))) (λf.f 0 (λf.true))

This is going to take some time, so we’ll miss out most of the steps.

> 
: λf.f (λf.λx.f (f (f x))) (λf.f (λf.λx.f (f x)) (λf.f (λf.λx.(λy.0) (λf.true) f (f x)) (λf.f 0 (λf.true))))
> 
: λf.f (λf.λx.f (f (f x))) (λf.f (λf.λx.f (f x)) (λf.f (λf.λx.0 f (f x)) (λf.f 0 (λf.true))))
> 
: λf.f (λf.λx.f (f (f x))) (λf.f (λf.λx.f (f x)) (λf.f (λf.λx.(λx.x) (f x)) (λf.f 0 (λf.true))))
> 
: λf.f (λf.λx.f (f (f x))) (λf.f (λf.λx.f (f x)) (λf.f (λf.λx.f x) (λf.f 0 (λf.true))))

Let’s reformat the last line to be sure of what we’ve got.

λf.
	f 
	(λf.λx.f (f (f x))) 
	(λf.
		f 
		(λf.λx.f (f x)) 
		(λf.
			f 
			(λf.λx.f x) 
			(λf.f 0 (λf.true))))

It should be reasonably obvious that we have here a list consisting of 3, 2, 1, 0 in that order. In order to get the predecessor of 3, we just need head (tail l)) where l is that list. Here, therefore, is our first attempt at pred.

let pred1 = λn.head (tail (n addSuccHead zeroList))

What’s the predecessor of 1?

> pred1 1
: (λn.head (tail (n (λl.cons (succ (head l)) l) (λf.f 0 (λf.true))))) 1
> 
: head (tail (1 (λl.cons (succ (head l)) l) (λf.f 0 (λf.true))))
> 
: tail (1 (λl.cons (succ (head l)) l) (λf.f 0 (λf.true))) (λx.λy.x)
> 
: 1 (λl.cons (succ (head l)) l) (λf.f 0 (λf.true)) (λx.λy.y) (λx.λy.x)
> 
: (λx.(λl.cons (succ (head l)) l) x) (λf.f 0 (λf.true)) (λx.λy.y) (λx.λy.x)
> 
: (λl.cons (succ (head l)) l) (λf.f 0 (λf.true)) (λx.λy.y) (λx.λy.x)
> 
: cons (succ (head (λf.f 0 (λf.true)))) (λf.f 0 (λf.true)) (λx.λy.y) (λx.λy.x)
> 
: (λt.λf.f (succ (head (λf.f 0 (λf.true)))) t) (λf.f 0 (λf.true)) (λx.λy.y) (λx.λy.x)
> 
: (λf.f (succ (head (λf.f 0 (λf.true)))) (λf.f 0 (λf.true))) (λx.λy.y) (λx.λy.x)
> 
: (λx.λy.y) (succ (head (λf.f 0 (λf.true)))) (λf.f 0 (λf.true)) (λx.λy.x)
> 
: (λy.y) (λf.f 0 (λf.true)) (λx.λy.x)
> 
: (λf.f 0 (λf.true)) (λx.λy.x)
> 
: (λx.λy.x) 0 (λf.true)
> 
: (λy.0) (λf.true)
> 
: 0

What about 3? This will be a bit of a roller coaster, so I’ll omit most of the steps.

> pred1 3
: (λn.head (tail (n (λl.cons (succ (head l)) l) (λf.f 0 (λf.true))))) 3
...
: λf.λx.(λf.λx.head (λf.f 0 (λf.true)) f (f x)) f (f x)
> 
: λf.λx.(λx.head (λf.f 0 (λf.true)) f (f x)) (f x)
> 
: λf.λx.head (λf.f 0 (λf.true)) f (f (f x))
> 
: λf.λx.(λf.f 0 (λf.true)) (λx.λy.x) f (f (f x))
> 
: λf.λx.(λx.λy.x) 0 (λf.true) f (f (f x))
> 
: λf.λx.(λy.0) (λf.true) f (f (f x))
> 
: λf.λx.0 f (f (f x))
> 
: λf.λx.(λx.x) (f (f x))
> 
: λf.λx.f (f x)

2 is the answer.

We could leave it at that, but there is another more optimised way to define pred that takes advantage of the fact that you only really need to keep track of the first two items on the list. Instead of using a list to keep track of the history, we use a structure called an ordered pair (or “pair” for short). We have actually already come across an example of an ordered pair: a list is an ordered pair in which the second element is itself a list (or nil). Here’s what a pair looks like:

λp.p a b

It’s a function that applies its argument (that must be a function of two arguments) to a and b. To get the first element apply the pair to true. To get the second element, apply the pair to false.

> (λp.p a b) true
: (λp.p a b) true
> 
: true a b
> 
: (λy.a) b
> 
: a
> (λp.p a b) false
: (λp.p a b) false
> 
: false a b
> 
: (λy.y) b
> 
: b

Our equivalent to addSuccHead is called addSuccFirst and it accepts a pair p as an argument. It creates a new pair whose first element is the successor of its argument’s first element and whose second element is the first element of the argument.

First of all, this is the function to construct a pair:

let pair = λa.λb.λp.p a b

This is the function addSuccFirst

let addSuccFirst = λp.pair (succ (p true)) (p true)

Our starting point is a pair whose first element is 0. We don’t really care about the second element because the only time it will be used is if we do pred 0 which is undefined for the natural numbers (note the, in our previous pred1 list based version, pred 0 would end up trying to take the head of nil which is undefined but actually comes out as true with the definition of nil we have). I’m going to use 0 as the second element so that pred 0 comes out as 0.

> 3 addSuccFirst (pair 0 0)
: 3 (λp.pair (succ (p true)) (p true)) (pair 0 0)
> 
: (λx.(λp.pair (succ (p true)) (p true)) ((λp.pair (succ (p true)) (p true)) ((λp.pair (succ (p true)) (p true)) x))) (pair 0 0)
...
: λp.p (λf.λx.f (f (f x))) (λf.λx.(λy.0) 0 f (f (f x)))
> 
: λp.p (λf.λx.f (f (f x))) (λf.λx.0 f (f (f x)))
> 
: λp.p (λf.λx.f (f (f x))) (λf.λx.(λx.x) (f (f x)))
> 
: λp.p (λf.λx.f (f (f x))) (λf.λx.f (f x))

I’ve snipped a lot of the processing again, but you can see that we end up with a pair containing 3 and 2 as its elements. Applying that pair to false gives us 2 which is the predecessor of 3. The new definition of pred is thus:

let pred = λn.(n addSuccFirst (λp.p 0 0)) false

Note that, in the above, I replaced pair 0 0 with its beta reduction as a small optimisation.

> pred 3
: (λn.n (λp.pair (succ (p true)) (p true)) (λp.p 0 0) false) 3
> 
: 3 (λp.pair (succ (p true)) (p true)) (λp.p 0 0) false
> 
: (λx.(λp.pair (succ (p true)) (p true)) ((λp.pair (succ (p true)) (p true)) ((λp.pair (succ (p true)) (p true)) x))) (λp.p 0 0) false
...
: λf.λx.true 0 0 f (f (f x))
> 
: λf.λx.(λy.0) 0 f (f (f x))
> 
: λf.λx.0 f (f (f x))
> 
: λf.λx.(λx.x) (f (f x))
> 
: λf.λx.f (f x)

The predecessor of 3 is 2. There we go.

Arithmetic

With pred and succ we are ready to define other arithmetic functions. I shall leave most of this for another day, but, to give a flavour, let’s evaluate 3 succ 2.

> 3 succ 2
: 3 succ 2
> 
: (λx.succ (succ (succ x))) 2
> 
: succ (succ (succ 2))
> 
: λf.λx.succ (succ 2) f (f x)
> 
: λf.λx.(λf.λx.succ 2 f (f x)) f (f x)
> 
: λf.λx.(λx.succ 2 f (f x)) (f x)
> 
: λf.λx.succ 2 f (f (f x))
> 
: λf.λx.(λf.λx.2 f (f x)) f (f (f x))
> 
: λf.λx.(λx.2 f (f x)) (f (f x))
> 
: λf.λx.2 f (f (f (f x)))
> 
: λf.λx.(λx.f (f x)) (f (f (f x)))
> 
: λf.λx.f (f (f (f (f x))))

Yes, 3 succ 2 →_β 5. We get addition for free, albeit a grossly inefficient addition. What about this?

2 (3 succ) 0

It beta reduces to

λf.λx.f (f (f (f (f (f x)))))

which is 6. A function for doing multiplication is therefore

λp.λq.p (q succ) 0

I’ll leave it at that for now. With the aid of some comparison functions, we now have all we need to do some fairly powerful computation. In the next episode (which may or may not happen) we’ll use what we’ve got to compute the Fibonacci sequence.