The Church numerals are an encoding of the natural numbers into untyped lambda-calculus.
The th Church numeral is the operation of “iteration times”, sending a function to its th iterate. Thus is the identity function, , , and so on.
The Church numeral can be regarded as a realizer or “proof” that we can do induction up to . 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.