Church encoding

Common card · No. 305164

In mathematics, Church encoding is a method of representing various types of data in the lambda calculus. In the untyped lambda calculus the only primitive data type is the function, 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 present. As such, they must be constructed from lambda terms. Conceptually, they are constructed from higher-order functions. The Church numerals are a representation of the natural numbers using lambda notation. The method is named after Alonzo Church, who first encoded data in the lambda calculus this way. It can also be extended to represent other data types in a 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, I ≡ λ x . x...

Read on Wikipedia