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.

## 10 comments:

Before I read this, I had heard of Church numerals, but I didn't really *get it*, and now I think I do.

After letting this concept bubble around in my brain for a while, I decided to try and implement Church numerals in JavaScript, just for fun.

https://github.com/MatrixFrog/church_js

Thanks for the inspiration!

Tyler,

Awesome! There was a time before I started this series when I considered doing all the SICP exercises in JavaScript. I think it was JavaScript: The Good Parts where I first read that it was a fully functional language, so this should be possible. Once I started digging in to SICP I realized that I really wanted to learn Scheme, so I stuck with that as my language.

Maybe someone could reach a wider audience if they took all the solutions and translated them into JavaScript. I know I would be interested in reading that.

Hint hint. ;)

Thanks for this post. Been going through SICP and this helped me a lot.

Hey Bill, I really appreciate you thoroughly explaining the examples in wonderful detail!

I am little confused, however on how you simplified from line 3 to line 4 of:

(add-1 zero)

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

(lambda (f) (lambda (x) (f ((lambda (x) x) x))))

(lambda (f) (lambda (x) (f x)))

I don't understand why it's not:

(lambda (f) (lambda (x) (f (x x))))

Basically, what happens to that last "x"?

(I do understand why the representation of one and two work, but just not the derivation using add-1).

Thanks! Dan

It's Dan again, nevermind I answered my own question...

I see that

(lambda (f) (lambda (x) (f ((lambda (x) x) x))))

the last lambda is the function and then it's applied with the input of x, resulting in x!

Anyway, thanks again!

Bill, thanks for all of your contributions.

The following uses JavaScript's ES6 arrow functions to make this quite readable

const zero = f => x => x

const add1 = x => f => y => f (x (f)) (y);

const one = f => x => f (x);

const two = f => x => f (f (x));

const inc = x => x + 1;

console.log(zero (inc) (0)); // 0

console.log(one (inc) (0)); // 1

console.log(two (inc) (0)); // 2

const add = (x,y) => f => z => x (f) (y (f) (z));

const three = add(one,two);

console.log(three (inc) (0)); // 3

const four = add(two,two);

const seven = add(four,three);

console.log(four (inc) (0)); // 4

console.log(seven (inc) (0)); // 7

Thanks for posting the JS code; really nice. I was trying to learn the same stuff over at http://niltag.net/essays/church.html. However, it seems like the author left out a few steps (namely, the incrementing part) on section 4. Your examples filled in what was presumably implicit in his example(s).

(define one

(lambda (f) f))

It is not required in the exercise, also the product function can be defined with the following code:

(define (product-church m n)

(lambda (f) (lambda (x) ((m (n f)) x))))

I'm totally lost here:

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

(define (add-1 n)

(lambda (f) (lambda (x) (f ((n f) x)))))

(define (inc n)

(+ n 1))

(define one (add-1 zero))

> ((one inc) 0)

1 What?!How?

So add-1 arguments become:

(define (add-1 zero)

(lambda (inc) (lambda (0) (inc ((zero inc) 0)))))

Is that what is going on?I'm so confused

Post a Comment