In mathematics, Church encoding is a means of representing data and operators in the lambda calculus.
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.
[dubious – discuss] In the untyped lambda calculus the only primitive data type is the function.
A straightforward implementation of Church encoding slows some access operations from
is the size of the data structure, making Church encoding impractical.
[1] 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.
[2] Nonetheless Church encoding is often used in theoretical arguments, as it is a natural representation for partial evaluation and theorem proving.
[1] The assumption that functions are the only primitive data types streamlines many proofs.
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.
There are potential problems with the interpretation of results because of the difference between the intensional and extensional definition of equality.
In simpler terms, the "value" of the numeral is equivalent to the number of times the function encapsulates its argument.
: The Church numeral 3 represents the action of applying any given function three times to a value.
Arithmetic operations on numbers may be represented by functions on Church numerals.
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.
The left-hand side of the table shows a numeral n applied to inc and init.
The simplest predicate for testing numbers is IsZero so consider the condition.
Create a new function called div by; to get, Then, where, Gives, Or as text, using \ for λ, For example, 9/3 is represented by Using a lambda calculus calculator, the above expression reduces to 3, using normal order.
The OneZero function achieves this condition, The recursion may be implemented using the Y combinator, Addition is defined mathematically on the pair by, The last expression is translated into lambda calculus as, Similarly subtraction is defined, giving, Multiplication may be defined by, 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).
Some programming languages use these as an implementation model for Boolean arithmetic; examples are Smalltalk and Pico.
The Church encoding of true and false are functions of two parameters: The two definitions are known as Church Booleans: This definition allows predicates (i.e. functions returning logical values) to directly act as if-clauses.
Because true and false choose the first or second parameter they may be combined to provide logic operators.
To represent null, the pair may be wrapped in another pair, giving three values: Using this idea the basic list operations can be defined like this:[8] In a nil node second is never accessed, provided that head and tail are only applied to nonempty lists.
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)).
Equivalently, it is an application of the chain of functional compositions of partial applications, (c x ∘ c y ∘ c z) n. This list representation can be given type in System F. The evident correspondence to Church numerals is non-coincidental, as that can be seen as a unary encoding, with natural numbers represented by lists of unit (i.e. non-important) values, e.g. [() () ()], with the list's length serving as the representation of the natural number.
An alternative representation is Scott encoding, which uses the idea of continuations and can lead to simpler code.
In this approach, we use the fact that lists can be observed using pattern matching expression.
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.