Church numerals are an encoding of integers in the lambda calculus

Church numerals are an encoding of natural numbers in the lambda calculus .

In the lambda calculus, the single fundamental object type is functions. The Church encoding of the natural number $n$ is the composition operator: $$c_n = \lambda f. \lambda x. f (\ldots (f \, x) \ldots )$$ where $f$ is applied $n$ times.

The usual arithmetic operations can be encoded as operations on functions, for example: $$ \begin{align} \mathrm{plus} &= \lambda m. \lambda n. \lambda f. \lambda x. m \, f \, (n \, f \, x) && \text{(\(m+n\) maps \(f\) to \(m f\) composed with \(n f\))} \\ \mathrm{mult} &= \lambda m. \lambda n. m \, (n \, f) && \text{(\(m \times n\) composes \((n f)\) \(m\) times)} \\ \end{align} $$

Other data structures can be encoded following similar principles. Church encodings exist for booleans, pairs, etc.

history | excerpt history