SICP 2.6: Church numerals

From SICP section 2.1.3 What Is Meant by Data?

Exercise 2.6 introduces us to the idea that in a language that can manipulate procedures, we can get by without integers altogether. The implementation of 0 and the operation of adding 1 are given as

(define zero (lambda (f) (lambda (x) x)))

(define (add-1 n)
   (lambda (f) (lambda (x) (f ((n f) x)))))

This representation is known as Church numerals, after its inventor, Alonzo Church, the logician who invented the λ calculus.

It's important to note that the definition for zero above does not evaluate to the integer 0, it is just a representation for 0.

> zero
#<procedure:zero>

A Church numeral is a procedure that takes one argument, and that argument is itself another procedure that also takes one argument. The procedure zero represents the integer 0 by returning a procedure that applies its input procedure zero times. The Church numeral one should return a procedure that applies its input procedure once, two should return a procedure that applies its input procedure twice, and so on. This is how Church numerals represent integers, by applying their input procedure the exact number of times that the numerals are supposed to represent.

Our job in this exercise is to define one and two directly (not in terms of zero and add-1). We'll do that by using substitution to evaluate (add-1 zero) to see what the resulting procedural definition should be. We also need to give a direct definition for addition of two Church numerals (not in terms of repeated application of add-1).

Before we begin, we'll need some method for testing Church numerals to make sure they do what we expect them to do. We'll need a simple procedure to pass to each Church numeral as an argument so that we can see it gets evaluated the correct number of times. The inc procedure should do nicely. (You can replace inc with any procedure you like, just make it one that's easy to mentally calculate several repetitions of.)

(define (inc n)
   (+ n 1))

We can use inc to show that zero does not call its input parameter, or more precisely, it calls its input procedure zero times.

> ((zero inc) 0)
0
> ((zero inc) 1)
1
> ((zero inc) 2)
2

Now let's define one and two in the way that the book warns us not to, just to make sure they behave as we expect. I'll give the assigned implementations later.

> (define one (add-1 zero))
> (define two (add-1 one))
> ((one inc) 0)
1
> ((one inc) 1)
2
> ((two inc) 0)
2
> ((two inc) 1)
3

So we can see that the procedure returned by one applies inc one time, and the procedure returned by two applies it twice. Now let's use substitution to evaluate (add-1 zero), giving us the direct definition of the Church numeral one.

(add-1 zero)

; retrieve the body of add-1 and substitute zero for its parameter n
(lambda (f) (lambda (x) (f ((zero f) x))))

; retrieve the body of zero and substitute
(lambda (f) (lambda (x) (f ((lambda (x) x) x))))

; simplify
(lambda (f) (lambda (x) (f x)))

So we can define one directly as:

(define one
   (lambda (f) (lambda (x) (f x))))

Next we can define two by evaluating (add-1 one) using exactly the same principles.

(add-1 one)

; retrieve the body of add-1 and substitute one for its parameter n
(lambda (f) (lambda (x) (f ((one f) x))))

; retrieve the body of one and substitute
(lambda (f) (lambda (x) (f ((lambda (x) (f x)) x))))

; simplify
(lambda (f) (lambda (x) (f (f x))))

So two is defined directly as:

(define two
   (lambda (f) (lambda (x) (f (f x)))))

Just as was explained earlier, the Church numeral one takes a procedure as an argument and returns a procedure that applies the input procedure once. The only difference in the Church numeral two is that it applies its input procedure twice.

Add these definitions in the Scheme interpreter and test them out the same as before.

> ((one inc) 0)
1
> ((one inc) 5)
6
> ((two inc) 3)
5
> ((two inc) 7)
9

Now we need to figure out how to add two Church numerals. We can see from the definition of add-1 that all it does is takes a Church numeral, n, and wraps one additional function call around it.

(define (add-1 n)
   (lambda (f) (lambda (x) (f ((n f) x)))))

We can implement Church numeral addition by using the same approach. We'll take two Church numerals m and n. Instead of wrapping n in one extra function call, we'll wrap it in m extra calls.

(define (add-church m n)
   (lambda (f) (lambda (x) ((m f) ((n f) x)))))

We can now use add-church to define several more Church numerals for testing.

> (define three (add-church one two))
> (define four (add-church two two))
> (define seven (add-church three four))
> ((three inc) 0)
3
> ((four inc) 0)
4
> ((seven inc) 0)
7

Related:

For links to all of the SICP lecture notes and exercises that I've done so far, see The SICP Challenge.