Representation of the natural numbers as higher-order functions
In mathematics, Church encoding is a means of representing data and operators in the lambda calculus. 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.
Terms that are usually considered primitive in other notations (such as integers, booleans, pairs, lists, and tagged unions) are mapped to higher-order functions under Church encoding. The Church-Turing thesis asserts that any computable operator (and its operands) can be represented under Church encoding. In the untyped lambda calculus the only primitive data type is the function.
The Church encoding is not intended as a practical implementation of primitive data types. Its use is to show that other primitive data types are not required to represent any calculation. The completeness is representational. 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 to its n-fold composition. In simpler terms, the "value" of the numeral is equivalent to the number of times the function encapsulates its argument.
All Church numerals are functions that take two parameters. Church numerals 0, 1, 2, ..., are defined as follows in the lambda calculus.
Starting with0not applying the function at all, proceed with1applying the function once, ...:
The Church numeral 3 represents the action of applying any given function three times to a value. The supplied function is first applied to a supplied parameter and then successively to its own result. The end result is not the numeral 3 (unless the supplied parameter happens to be 0 and the function is a successor function). The function itself, and not its end result, is the Church numeral 3. The Church numeral 3 means simply to do anything three times. It is an ostensive demonstration of what is meant by "three times".
The exponentiation function is given by the definition of Church numerals; . In the definition substitute to get and,
which gives the lambda expression,
The function is more difficult to understand.
A Church numeral applies a function n times. The predecessor function must return a function that applies its parameter n - 1 times. This is achieved by building a container around f and x, which is initialized in a way that omits the application of the function the first time. See predecessor for a more detailed explanation.
The subtraction function can be written based on the predecessor function.
The predecessor function used in the Church encoding is,
To build the predecessor we need a way of applying the function 1 fewer time. A numeral n applies the function fn times to x. The predecessor function must use the numeral n to apply the function n-1 times.
Before implementing the predecessor function, here is a scheme that wraps the value in a container function. We will define new functions to use in place of f and x, called inc and init. The container function is called value. The left hand side of the table shows a numeral n applied to inc and init.
The general recurrence rule is,
If there is also a function to retrieve the value from the container (called extract),
Then extract may be used to define the samenum function as,
The samenum function is not intrinsically useful. However, as inc delegates calling of f to its container argument, we can arrange that on the first application inc receives a special container that ignores its argument allowing to skip the first application of f. Call this new initial container const. The right hand side of the above table shows the expansions of nincconst. Then by replacing init with const in the expression for the same function we get the predecessor function,
As explained below the functions inc, init, const, value and extract may be defined as,
Calculating takes many beta reductions. Unless doing the reduction by hand, this doesn't matter that much, but it is preferable to not have to do this calculation twice. The simplest predicate for testing numbers is IsZero so consider the condition.
But this condition is equivalent to , not . If this expression is used then the mathematical definition of division given above is translated into function on Church numerals as,
As desired, this definition has a single call to . However the result is that this formula gives the value of .
This problem may be corrected by adding 1 to n before calling divide. The definition of divide is then,
divide1 is a recursive definition. The Y combinator may be used to implement the recursion. Create a new function called div by;
In the left hand side
In the right hand side
Or as text, using \ for λ,
divide = (\n.((\f.(\x.x x) (\x.f (x x))) (\c.\n.\m.\f.\x.(\d.(\n.n (\x.(\a.\b.b)) (\a.\b.a)) d ((\f.\x.x) f x) (f (c d m f x))) ((\m.\n.n (\n.\f.\x.n (\g.\h.h (g f)) (\u.x) (\u.u)) m) n m))) ((\n.\f.\x. f (n f x)) n))
One simple approach for extending Church Numerals to signed numbers is to use a Church pair, containing Church numerals representing a positive and a negative value. The integer value is the difference between the two Church numerals.
A natural number is converted to a signed number by,
Negation is performed by swapping the values.
The integer value is more naturally represented if one of the pair is zero. The OneZero function achieves this condition,
The recursion may be implemented using the Y combinator,
The last expression is translated into lambda calculus as,
A similar definition is given here for division, except in this definition, one value in each pair must be zero (see OneZero above). The divZ function allows us to ignore the value that has a zero component.
divZ is then used in the following formula, which is the same as for multiplication, but with mult replaced by divZ.
Rational and computable real numbers may also be encoded in lambda calculus. Rational numbers may be encoded as a pair of signed numbers. Computable real numbers may be encoded by a limiting process that guarantees that the difference from the real value differs by a number which may be made as small as we need. The references given describe software that could, in theory, be translated into lambda calculus. Once real numbers are defined, complex numbers are naturally encoded as a pair of real numbers.
The data types and functions described above demonstrate that any data type or calculation may be encoded in lambda calculus. This is the Church-Turing thesis.
Most real-world languages have support for machine-native integers; the church and unchurch functions convert between nonnegative integers and their corresponding Church numerals. The functions are given here in Haskell, where the \ corresponds to the λ of Lambda calculus. Implementations in other languages are similar.
Church Booleans are the Church encoding of the Boolean values true and false. Some programming languages use these as an implementation model for Boolean arithmetic; examples are Smalltalk and Pico.
Boolean logic may be considered as a choice. The Church encoding of true and false are functions of two parameters:
true chooses the first parameter.
false chooses the second parameter.
The two definitions are known as Church Booleans:
This definition allows predicates (i.e. functions returning logical values) to directly act as if-clauses. A function returning a Boolean, which is then applied to two parameters, returns either the first or the second parameter:
evaluates to then-clause if predicatex evaluates to true, and to else-clause if predicatex evaluates to false.
Because true and false choose the first or second parameter they may be combined to provide logic operators. Note that there are two version of not, depending on the evaluation strategy that is chosen.
Church pairs are the Church encoding of the pair (two-tuple) type. The pair is represented as a function that takes a function argument. When given its argument it will apply the argument to the two components of the pair. The definition in lambda calculus is,
As an alternative to the encoding using Church pairs, a list can be encoded by identifying it with its right fold function. For example, a list of three elements x, y and z can be encoded by a higher-order function that when applied to a combinator c and a value n returns c x (c y (c z n)).
This list representation can be given type in System F.
In this approach, we use the fact that list can be observed using pattern matching expression. For example,
using Scala (programming language) notation, if 'list' denotes a value of a list data type with empty list 'Nil' and constructor 'Cons(h,t)' we can inspect the list and compute 'nilCode' in case the list is empty and 'consCode(h,t)' when the list is non-empty:
The 'list' is given by how it acts upon 'nilCode' and 'consCode'. We therefore define a list as a function that accepts such 'nilCode' and 'consCode' as arguments, so that instead of the above pattern match we may simply write:
Let us denote by 'n' the parameter corresponding to 'nilCode' and by 'c' the parameter corresponding to 'consCode'.
The empty list is the one that returns the nil argument:
The non-empty list with head 'h' and tail 't' is given by
More generally, algebraic data type with alternatives becomes a function with parameters. When the th constructor has arguments, the corresponding parameter of the encoding takes arguments as well.
Scott's encoding can be done in untyped lambda calculus, whereas its use with types requires a type system with recursion and type polymorphism. A lists with element type E in this representation that is used to compute values of type C would have the following recursive type definition, where '=>' denotes function type:
typeList=C=>// nil argument(E=>List=>C)=>// cons argumentC// result of pattern matching
A list that can be used to compute arbitrary type would have type that quantifies over C. A list generic in E would also take E as the type argument.