nLab Church numeral

Church numerals

Church numerals


The Church numerals are an encoding of the natural numbers into untyped lambda-calculus.


The nnth Church numeral n̲\underline{n} is the operation of “iteration nn times”, sending a function ff to its nnth iterate. Thus 0̲(f)\underline{0}(f) is the identity function, 1̲(f)=f\underline{1}(f) = f, 2̲(f)=ff=λx.f(f(x))\underline{2}(f) = f\circ f = \lambda x. f(f(x)), and so on.

Connection to realizability

The Church numeral n̲\underline{n} can be regarded as a realizer or “proof” that we can do induction up to nn. See this discussion.

Last revised on June 26, 2021 at 16:14:42. See the history of this page for a list of all contributions to it.