Sunday, October 31, 2010

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.

7 comments:

Tyler Breisacher said...

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!

Bill the Lizard said...

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. ;)

Anonymous said...

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

Anonymous said...

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

Anonymous said...

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!

Naomi Kyoto said...

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

Patrick Ryll said...

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).