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.f`

. The notation ^{n} x`f`

means ^{n}`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.f`

where ^{n} x`n`

is the number represented. `λf.λx.f`

is therefore the representation of ^{0} x`0`

and `f`

means no applications of ^{0}`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.f`

→^{n} x)_{β} `(λf.λx.f`

^{n+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 `f`

is ^{n+1} x`f`

. ^{n} (f x)`succ`

needs to apply two arguments `a`

and `b`

such that

`(λf.λx.f`

→^{n} x) a b_{β} `f`

^{n} (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`

= `succ`

, or ^{n-1} 0`(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 `succ`

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.

I used to be in computer science (programming Culprit for mainframes for the Canadian International Development Agency) and I found your article intense, but interesting. Come visit my blog for occasional technical articles and suchlike. Good to see you there!

— Catxman

http://www.catxman.wordpress.com

LikeLike