Church numeral
A Church numeral is a natural number encoded into lambda calculus using Church encoding. Church numerals are one of two popular ways to encode natural numbers as functions, the other being Scott numerals. Quoting Corbin 2023:
The natural numbers are initial Church numerals, which is a way of formalizing the intuition that the natural numbers are: do nothing, do it once, do it twice, …
Definition
We'll start with simply-typed lambda calculus. A Church numeral is a function with type (X → X) → (X → X), for all types X. This is a polymorphic type signature; in e.g. wikipedia:System F, it would be written as:
ΛX. (X → X) → (X → X)
We can think of this functions with this signature as taking unary operations X → X on some type X, chosen by the caller, and either returning the identity function on X or repeating the unary operation some number of times.
In the untyped lambda calculus, a Church numeral no longer needs to be well-typed as long as it is extensionally equivalent to one of the simply-typed functions. It can be useful, when writing untyped lambda calculus, to write Church numerals and other combinators in simply-typed lambda calculus first.
Examples
The first few numbers can be written with out as:
0: λfr.r 1: λfr.fr 2: λfr.f(fr) 3: λfr.f(f(fr))
That is, the number n is a function of f and r, specifically f applied to r n times. A number can be incremented using λxfr.f(xfr). This works by simulating the number x, but applying f one more time.
Arithmetic
Addition of Church numerals is performed by applying the first term to the successor function, and then to the second number to be added. If the successor function is called +, and Church numerals are notated by the integers they represent, then this resembles standard mathematical notation (adding 3 to 5 can be written as 3+5, which expands to +(+(+5)).
Multiplication is essentially function composition:
mul: λxyf.x(yf)
Exponentiation is achieved by simply applying the exponent to the base:
exp: λxy.yx
There are many ways to define a predecessor function,and the following is one of the ways to use church pairs.
pair: λabx.xab left: λp.p(λab.a) right: λp.p(λab.b) pred: λn.left(n(λp.pair(right p)(succ(right p)))(pair 0 0))
Subtraction just like addition,but replace successor function into predecessor function.
sub: λxy.x pred y
Need a fixed point combinator to define partial division function.
fix: (λx.xx)(λfx.x(ffx)) div: fix(λfxy.(succ(sub x y))(λn.succ(f(sub x y)y))0)
Contrast with Scott numerals
Church numerals are the initial encoding of the natural numbers. Scott numerals are the final encoding.
Fast operations in Church numerals include multiplication and exponentiation, including wikipedia:exponentiation by squaring. In contrast, Scott numerals have fast decrement, including decrement-or-zero tests.
See also
Other approaches to encoding natural numbers in lambda calculus: