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.