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 =
- S =
So here are 1,2:
1 = S0
2 = S1
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.
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
Note in particular the first composite church numeral
"IIII" for "4
In fact, wharfie's absolutely right. I should apologise that I make shit up.