Understanding church numerals

Question

I'm working my way through SICP, and it gives the following definition for zero for Church Numerals:

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

I have a few questions about that:

1. Why the complicated syntax? It seems to be quite readable by just having the following instead:

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

   where we can see it's a function called zero that takes one (unused) argument f and returns a function-of-one-parameter that will return its parameter. It almost seems like the definition is just intended to be as non-straightforward as possible.

2. What is the x there for? For example doing something like:

   ((zero square) 100)
   

   returns 100. Is x just the default value returned?

Answer 1

There is no x in (lambda (x) x). None.

The x in (lambda (x) x) is bound. It could be named by any name whatever. We can not talk about x in (lambda (x) x) any more than we could talk about y in (lambda (y) y).

There is no y in (lambda (y) y) to speak of. It is just a placeholder, an arbitrary name whose sole purpose in the body is to be the same as in the binder. Same, without regard for which specific name is used there as long as it is used twice -- first time in the binder, and the other time in the body.

And in fact there is this whole 'nother notation for lambda terms, called De Bruijn notation, where the same whole thing is written (lambda 1). With 1 meaning, "I refer to the argument which the binder 1 step above me receives".

So x is unimportant. What's important is (lambda (x) x) which denotes a function which returns its argument as is. The so called "identity" function.

But even this is not important here. The Church encoding of a number is really a binary function, a function expecting two arguments -- the f and the z. The "successor step" unary function f and the "zero" "value" z, whatever that might be, as long as the two go together. Make sense together. Work together.

So how come we see two unary functions there when it is really one binary function in play?

That is the important bit. It is known as currying.

In lambda calculus all functions are unary. And to represent a binary function an unary function is used, such that when given its (first) argument it returns another unary function, which, when given its (now, second) argument, performs whatever thing our intended binary function ought to perform, using those two arguments, the first and the second.

This is all very very simple if we just write it in combinatory (equational) notation instead of the lambda notation:

zero f z = z
one f z = f z
two f z = f (f z) = f (one f z) = succ one f z
succ one f z = f (one f z)

where every juxtaposition denotes an application, and all applications associate on the left, so we imagine the above being a shortcut notation for

zero f = lambda z. z
zero = lambda f. (lambda z. z)
......
......
succ = lambda one. (lambda f. (lambda z. f (one f z) ))
;; such that
succ one f z = (((succ one) f) z)
  = ((((lambda one. (lambda f. (lambda z. f (one f z) ))) one) f) z)
  = .... 
  = (f ((one f) z))
  =  f (one f z)

but it's the same thing. The differences in notation are not important.

And of course there is no one in lambda one. (lambda f. (lambda z. f (one f z) )). It is bound. It could just be named, I dunno, number:

succ number f z = f (number f z) = f ((number f) z)

meaning, (succ number) is such a number, which, given the f and the z, does with them one more f step compared to what number would do.

---

And so, ((zero square) 100) means, use the number zero with the successor step square and the zero value of 100, and have zero perform its number of successor steps for us -- that is to say, 0 steps -- starting from the zero value. Thus returning it unchanged.

Another possible use is ((zero (lambda (x) 0)) 1), or in general

((lambda (n) ((n (lambda (x) 0)) 1)) zero)  

;; or even more generally, abstracting away the 0 and the 1,

((((lambda (n) (lambda (t) (lambda (f) ((n (lambda (x) f)) t)))) zero) 1) 0)

which is just another way of writing

zero (lambda x. 0) 1  ;; or

foo n t f = n (lambda x. f) t   ;; and calling

foo zero 1 0

Hopefully you can see what foo is, easily. And also how to read aloud this t and this f. (Probably the original f would be better named s, for "successor", or something like that).