Church numeral

Alonzo Church's representation of natural numbers within the lambda calculus.

People are usually introduced (I known I was) to the lambda calculus as part of some course on programming some (mildly) functional programming language like Scheme, ML/SML/OCaml or Haskell. Of course, all the "trivial" examples of functions involve numbers: for instance, the function square is λx.x*x. Doesn't this mean we have to have numbers before we can have useful functions on them?

Turns out we can represent numbers as functions. To represent natural numbers á la Peano, we have to show how to represent 0 and the function Sn ("add 1 to n"):

• 0 = λf.λx.x
• S = λn.λg.λy.g(ngy)

• 1 = S0 = (λn.λg.λy.g(ngy))(λf.λx.x) = λg.λy.g((λf.λx.x)gy) = λg.λy.gy = λf.λx.fx
• 2 = S1 = (λn.λg.λy.g(ngy))1 = λg.λy.g(1gy) = λg.λy.ggy = λf.λx.ffx

So what does it all mean? Well, "0" takes a function f and an argument x, and applies f to x 0 times, giving just "x". "1" takes a function f and an argument x, and applies f to x 1 time, giving "fx". "2" takes a function f and an argument x, and applies f to x twice, giving "ffx". It's easy to convince yourself that the Church numeral "n" is the abstraction of applying a function f n times to an argument x.

A common tortureexercise is to define addition and multiplication of Church numerals. Hint: think about it in terms of "apply f to x n times"; multiplication is actually easier.

So there you have it. Lambda calculus doesn't need to stand on anything: you can write programs that work on natural numbers, but even those are really just terms of lambda calculus.

NOTE. It is possible to give a slightly shorter definition for S, by avoiding any reference to "y" in the definition above. I feel the description above is somewhat easier to grasp, as it avoids the use of higher order functions in an already confusing situation.

Despite my protestations, wharfinger continues to believe that the term "church" numerals refers to the peculiar practice of mauling Roman numerals on church clocks: the numbers "traditionally" appear there as

I, II, III, IIII, V, VI, VII, VIII, IX, X, XI, XII

In fact, wharfie's absolutely right. I should apologise that I make shit up.