Church numeral

This article is not detailed enough and needs to be expanded. Please help us by adding some more information.

A Church numeral is a function that can represent a number (specifically, a nonnegative integer) in lambda calculus. The first few numbers are defined as follows:

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 increment function, and then to the second number to be added. If the increment 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.

Subtraction and division are considerably more complicated, but certainly possible. Scott numerals, an alternative to Church numerals, support easier decrementation.