Church encoding

In mathematics, Church encoding is a way of representing various data types in the lambda calculus.

In the untyped lambda calculus the only primitive data type are functions, represented by lambda abstraction terms. Types that are usually considered primitive in other notations (such as integers, Booleans, pairs, lists, and tagged unions) are not natively present.

Hence the need arises to have ways to represent the data of these varying types by lambda terms, that is, by functions that are taking functions as their arguments and are returning functions as their results.

The Church numerals are a representation of the natural numbers using lambda notation. The method is named for Alonzo Church, who first encoded data in the lambda calculus this way. It can also be extended to represent other data types in the similar spirit.

This article makes occasional use of the alternative syntax for lambda abstraction terms, where λx.λy.λz.N is abbreviated as λxyz.N, as well as the two standard combinators, ${\displaystyle I\equiv \lambda x.x}$ and ${\displaystyle K\equiv \lambda xy.x}$, as needed.

A straightforward implementation of Church encoding slows some access operations from ${\displaystyle O(1)}$ to ${\displaystyle O(n)}$, where ${\displaystyle n}$ is the size of the data structure, making Church encoding impractical. Research has shown that this can be addressed by targeted optimizations, but most functional programming languages instead expand their intermediate representations to contain algebraic data types. Nonetheless Church encoding is often used in theoretical arguments, as it is a natural representation for partial evaluation and theorem proving. Operations can be typed using higher-ranked types, and primitive recursion is easily accessible. The assumption that functions are the only primitive data types streamlines many proofs.

Church encoding is complete but only representationally. Additional functions are needed to translate the representation into common data types, for display to people. It is not possible in general to decide if two functions are extensionally equal due to the undecidability of equivalence from Church's theorem. The translation may apply the function in some way to retrieve the value it represents, or look up its value as a literal lambda term. Lambda calculus is usually interpreted as using intensional equality. There are potential problems with the interpretation of results because of the difference between the intensional and extensional definition of equality.

Church numerals are the representations of natural numbers under Church encoding. The higher-order function that represents natural number n is a function that maps any function ${\displaystyle f}$ to its n-fold composition. In simpler terms, a numeral represents the number by applying any given function that number of times in sequence, starting from any given starting value: