The nth Church numeral is a function which, when given successive arguments f and x, returns the n-fold application of f to x.
It is just a minor detail of loose ends. Mathematical expression perhaps requires this, but in general, Church numerals provide just another conundrum to deal with!
Named for AlonzoChurch, the creator of LambdaCalculus.
0 := \x.\f.x
1 := \x.\f.(f x)
2 := \x.\f.(f (f x))
...
Terms for comparing two Church numerals for equality or inequality, as well as two realizations of the predecessor are explained OlegKiselyov's pages at
- http://pobox.com/~oleg/ftp/Computation/lambda-calc-opposites.txt (at the end)
- http://pobox.com/~oleg/ftp/Computation/lambda-arithm-neg.scm (at the beginning)
The following site shows how to generalize Church numerals to represent positive and negative integers, and how to add, subtract, compare, multiply and divide these integers:
- http://pobox.com/~oleg/ftp/Scheme/index.html#lambda-calc
- http://pobox.com/~oleg/ftp/Computation/Computation.html#lambda-calc-neg