Church numeral

From Esolang
Jump to: navigation, search

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: λ
2: λfr.f(fr)
3: λfr.f(f(fr))

That is, the number n is 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.


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.

This article is a stub, which means that it is not detailed enough and needs to be expanded. Please help us by adding some more information.