Church Numerals

Here is exercise 2.6 from 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)))

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


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

Please review my code:

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

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

  ;; I used an identity function to check the + procedure
  (define (+ a b)
    (lambda (f)
      (lambda (x)
        ((((a f) b) f) x))))

How can I improve this code?

Your function + is not correct.

The definition of the sum of two Church numerals is the following:

(define (plus a b)
  (lambda (f)
    (lambda (x)
      ((a f) ((b f) x)))))

(see for instance wikipedia).

In fact, the Church numeral n can be defined as the functional that applies a given functionf n times to a given value x. So in the above definition, the sum (plus a b) first apply b times f to x, and to that result f is applied a times. In your definition, instead, the types of the applications inside the body of the function are wrong.

How to test for the correctness of Church numerals and functions over them?

You simply apply a Church numeral to the function integer successor (i.e. (lambda(x)(+ x 1))) and the number 0 to find if it produces the corresponding “regular” numeral. So, for instance:

(define (succ x) (+ x 1))   ;; here `+` is the integer addition, not your function!

((zero succ) 0)  ; produces 0
((one succ) 0)   ; produces 1  etc.

So you can test if the sum is correct with:

(((plus one two) succ) 0)  ; produces 3

If you try your function, you will find:

(((+ one two) succ) 0) ; raises an error

StackExchange Code Review Q#141084, answer score: 3