Church Numeral

lambda-calculus

Definition

Church Numeral

Church numerals are a type of Church encoding for natural numbers.

The general form for a Church numeral $n\in \mathbb{N}$ is:

$$n\equiv \lambda f.\lambda x.f^{n}x$$

where $f^{n}x$ is a shorthand for applying $f$ repeatedly $n$ times.

$$\begin{array}{rl}0& \equiv \lambda f.\lambda x.x\\ 1& \equiv \lambda f.\lambda x.fx\\ 2& \equiv \lambda f.\lambda x.ffx\\ 3& \equiv \lambda f.\lambda x.fffx\\ & ⋮\end{array}$$

Successor

Successor

The successor function $\mathbf{S}$ is a combinator that is used to get the next number of a Church numeral and is defined as:

$$\mathbf{S}\equiv \lambda n.\lambda f.\lambda x.nf(fx)$$

Addition

To add $m$ and $n$, we need to apply $f$ a total of $m+n$ times. We can achieve this by first applying $f$ $n$ times (using the numeral $n$), and then applying $f$ $m$ times (using the numeral $m$) to the result.

$$\mathbf{ADD}\equiv \lambda m.\lambda n.\lambda f.\lambda x.mf(nfx)$$