Church numeral

From Esolang
Jump to navigation Jump to search

The natural numbers are initial Church numerals, which is a way of formalizing the intuition that the natural numbers are: do nothing, do it once, do it twice, … ~ C. Simpson, 2023

A Church numeral is a natural number encoded into lambda calculus using Church encoding. Church numerals are one of two popular ways to encode natural numbers as functions, the other being Scott numerals. Church numerals are a weakly initial object in the category of encodings and are often treated as an initial algebra for natural numbers.

Definition

We'll start with simply-typed lambda calculus. A Church numeral is a function with type (X → X) → (X → X), for all types X. This is a polymorphic type signature; in e.g. wikipedia:System F, it would be written as: 

ΛX. (X → X) → (X → X)

We can think of functions with this signature as taking unary operations X → X on some type X, chosen by the caller, and either returning the identity function on X or repeating the unary operation some number of times.

In the untyped lambda calculus, a Church numeral no longer needs to be well-typed as long as it is extensionally equivalent to one of the simply-typed functions. It can be useful, when writing untyped lambda calculus, to write Church numerals and other combinators in simply-typed lambda calculus first.

Examples

The first few numbers can be written with out as: 

0: λfr.r
1: λfr.fr
2: λfr.f(fr)
3: λfr.f(f(fr))

The number n is a function of an endomorphism f and starting value r which applies f to r n times.

Arithmetic

We start with the successor, which merely applies f an additional time: 

succ: λxfr.f(xfr)

Addition of Church numerals is performed by applying the first term to the successor function, and then to the second number to be added. This can be eta-reduced to a single application: 

add: λx.x succ

Multiplication is essentially function composition: 

mul: λxyf.x(yf)

Exponentiation is achieved by simply applying the exponent to the base: 

exp: λxy.yx

There are many ways to define a predecessor function. The following approach uses Church pairs. 

pair: λabx.xab
left: λp.p(λab.a)
right: λp.p(λab.b)
pred: λn.left(n(λp.pair(right p)(succ(right p)))(pair 0 0))

Subtraction is just like addition, but replacing the successor function with the predecessor function. 

sub: λxy.y pred x

We need a fixed-point combinator to define a partial division function. 

fix: (λx.xx)(λfx.x(ffx))
div: fix(λfxy.(succ(sub x y))(λn.succ(f(sub x y)y))0)

Non-standard numerals

There exist models of type theory in which the type [of natural numbers] contains exotic elements that do not correspond to numerals, and moreover, these elements break the [standard] induction principle. ~ A. Bauer, 2015

The polymorphic type of the algebra of natural numbers, as given above, admits terms which don't correspond to any standard natural number. For example, given any fixed-point combinator, the following number iterates infinitely many times: 

omega: fix (λyfx.f(yfx))

Nonetheless it is typeable with e.g. simple typing plus wikipedia:Löb's theorem, witnessed by the fixed-point combinator. We therefore see that lambda terms, even when restricted to reasonable type systems, are an example of a wikipedia:non-standard model of arithmetic. Since lambda terms are countable, we can therefore observe:

Theorem. No countable non-standard model of Peano's first-order axioms is computable. (Tennenbaum, 1959)

Corollary. It is undecidable whether a lambda term for a well-typed Church numeral has a normal form.

Nonetheless many folks working with lambda calculus do not mind the situation, because:

Theorem (Church–Rosser for ULC). In the untyped lambda calculus, every lambda term has at most one normal form. (Schroer, 1965)

Theorem. The above constructions are a model of Peano's first-order axioms. (Kleene)

An informal corollary is that arithmetic over the natural numbers is still correct when carried out by reduction of lambda terms; a computation might diverge, but it cannot converge to an incorrect result.

Thus, the Church numerals are equivalent to the wikipedia:one-point compactification of the natural numbers, giving a version of the wikipedia:extended natural numbers; a Church numeral either reduces to exactly one normal form, or it represents an indefinite computation. A wikipedia:limited principle of omniscience would be required to decide which is the case.

Contrast with Scott numerals

Church numerals are the initial encoding of the natural numbers. Scott numerals are the final encoding.

Fast operations in Church numerals include multiplication and exponentiation, including wikipedia:exponentiation by squaring. In contrast, Scott numerals have fast decrement, including decrement-or-zero tests.

See also

Other approaches to encoding natural numbers in lambda calculus:

References

Retrieved from "https://esolangs.org/w/index.php?title=Church_numeral&oldid=154400"