Re-writing church numerals function

Question

In SICP it defines the church numerals for positive numbers as follows:

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

The following is my 'best attempt' to rewrite this for my own understanding, here passing explicit arguments to one function:

(define (church f x n)
  (cond
    ((= n 0) x)                       ; zero case: return x
    (else (f (church f x (- n 1)))))) ; otherwise f(f(f...(x))) n times

(church square 3 2)
81

And then redefining zero I would have:

(define (zero2 f)
  (lambda (x) (church f x 0)))

And add-one as:

(define (add-1 n f)
  (lambda (x) (church f x (+ n 1))))

Or, if we have to defer the f argument then adding a wrapper-lambda:

(define (add-1 n)
  (lambda (f) (lambda (x) (church f x (+ n 1)))))

Do I have a correct understanding of this? if so, why the oh-so-complicated-syntax at the top for the add-1 or zero procedures (note: I'm guessing it's not that complicated and I'm just not fully understanding what it's doing). Any help would be greatly appreciated!

Answer 1

lambda calculus is a sub set of Scheme that does not allow more than one argument and lambda. With combinations of lambdas you can make any construct:

(define false (lambda (true) (lambda (false) false)))
(define true (lambda (true) (lambda (false) true)))
(define if (lambda (pred) (lambda (consequence) (lambda (alternative) ((pred consequence) alternative)))))

You might be wondering why I allow define since it isn't lambda. Well you don;t need it. It is just for convenience since with it you can try it out:

(((if true) 
  'result-true) 
 'result-false) 
; ==> result-true

Instead of using the totally equal version:

((lambda (pred) 
  (lambda (consequence) 
     (lambda (alternative) 
       ((pred consequence) alternative)))) 
 (lambda (true) (lambda (false) true))
  'result-true 
     'result-false)

Your function church is not lambda calculus since it does not return a church number and it takes more than one argument which is a violation. I have seen scheme functions to produce chuck numbers but any chuck number you should be able to do this to get the integer value:

((church-number add1) 0)

eg. zero:

(((lambda (f) (lambda (x) x)) add1) 0) ; ==> 0