Exercise 2.6 of SICP

Exercise 2.6: In case representing pairs as procedures wasn’t mind-boggling enough, consider that, in a language that can manipulate procedures, we can get by without numbers (at least insofar as nonnegative integers are concerned) by implementing 0 and the operation of adding 1 as

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

(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. Define one and two directly (not in terms of zero and add-1). (Hint: Use substitution to evaluate (add-1 zero)). Give a direct definition of the addition procedure + (not in terms of repeated application of add-1).

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

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

(add-1 zero)
(add-1 (lambda (f) (lambda (x) x)))
(lambda (f) (lambda (x) (f (((lambda (f) (lambda (x) x)) f) x))))
(lambda (f) (lambda (x) (f ((lambda (x) x) x))))
(lambda (f) (lambda (x) (f x)))

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

(add-1 one)
(add-1 (lambda (f) (lambda (x) (f x))))
(lambda (f) (lambda (x) (f (((lambda (f) (lambda (x) (f x))) f) x))))
(lambda (f) (lambda (x) (f ((lambda (x) (f x)) x))))
(lambda (f) (lambda (x) (f (f x))))

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


In order to check these I will use the fact that Church numerals appear to be repeated function composition. If I use the familiar inc function and pass an argument of 0 I should get the number I am looking for:

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

> ((one inc) 0)
1
> ((two inc) 0)
2
3


Now that I am convinced that my functions work it’s time to move on and create an addition function.

(define (add M N)
(lambda (f)
(lambda (x)
((M f) ((N f) x)))))

(add one one)
(add (lambda (f) (lambda (x) (f x))) (lambda (f) (lambda (x) (f x))))
(lambda (f)
(lambda (x)
(((lambda (f) (lambda (x) (f x))) f) (((lambda (f) (lambda (x) (f x))) f) x))))
(lambda (f)
(lambda (x)
((lambda (x) (f x)) ((lambda (x) (f x)) x))))
(lambda (f)
(lambda (x)
((lambda (x) (f x)) (f x))))
(lambda (f)
(lambda (x)
(f (f x))))


Now to check that it works properly:

>(((add one one) inc) 0)
2

(define (mult m n)