In
mathematics
Mathematics is an area of knowledge that includes the topics of numbers, formulas and related structures, shapes and the spaces in which they are contained, and quantities and their changes. These topics are represented in modern mathematics ...
, Church encoding is a means of representing data and operators in the
lambda calculus
Lambda calculus (also written as ''λ''-calculus) is a formal system in mathematical logic for expressing computation based on function abstraction and application using variable binding and substitution. It is a universal model of computation ...
. The Church numerals are a representation of the natural numbers using lambda notation. The method is named for
Alonzo Church
Alonzo Church (June 14, 1903 – August 11, 1995) was an American mathematician, computer scientist, logician, philosopher, professor and editor who made major contributions to mathematical logic and the foundations of theoretical computer scienc ...
, 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 function
In mathematics and computer science, a higher-order function (HOF) is a function that does at least one of the following:
* takes one or more functions as arguments (i.e. a procedural parameter, which is a parameter of a procedure that is itself ...
s 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
Lambda calculus (also written as ''λ''-calculus) is a formal system in mathematical logic for expressing computation based on function abstraction and application using variable binding and substitution. It is a universal model of computation t ...
the only primitive data type is the function.
Use
A straightforward implementation of Church encoding slows some access operations from
to
, where
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
In computer science, functional programming is a programming paradigm where programs are constructed by Function application, applying and Function composition (computer science), composing Function (computer science), functions. It is a declar ...
languages instead expand their intermediate representations to contain
algebraic data type
In computer programming, especially functional programming and type theory, an algebraic data type (ADT) is a kind of composite type, i.e., a type formed by combining other types.
Two common classes of algebraic types are product types (i.e., t ...
s. 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 type
In programming languages and type theory, parametric polymorphism allows a single piece of code to be given a "generic" type, using variables in place of actual types, and then instantiated with particular types as needed. Parametrically polymorph ...
s, 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
In mathematics and computer science, the ' (, ) is a challenge posed by David Hilbert and Wilhelm Ackermann in 1928. The problem asks for an algorithm that considers, as input, a statement and answers "Yes" or "No" according to whether the statem ...
. 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
Church numerals are the representations of natural number
In mathematics, the natural numbers are those numbers used for counting (as in "there are ''six'' coins on the table") and ordering (as in "this is the ''third'' largest city in the country").
Numbers used for counting are called ''Cardinal n ...
s under Church encoding. The higher-order function
In mathematics and computer science, a higher-order function (HOF) is a function that does at least one of the following:
* takes one or more functions as arguments (i.e. a procedural parameter, which is a parameter of a procedure that is itself ...
that represents natural number ''n'' is a function that maps any function to its ''n''-fold composition
Composition or Compositions may refer to:
Arts and literature
*Composition (dance), practice and teaching of choreography
*Composition (language), in literature and rhetoric, producing a work in spoken tradition and written discourse, to include v ...
. 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
Lambda calculus (also written as ''λ''-calculus) is a formal system in mathematical logic for expressing computation based on function abstraction and application using variable binding and substitution. It is a universal model of computation ...
.
''Starting with'' 0 ''not applying the function at all, proceed with'' 1 ''applying the function once, 2 ''applying the function twice, 3 ''applying the function three times, etc.'':
:
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
In mathematics, the successor function or successor operation sends a natural number to the next one. The successor function is denoted by ''S'', so ''S''(''n'') = ''n'' +1. For example, ''S''(1) = 2 and ''S''(2) = 3. The successor functio ...
). 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".
Calculation with Church numerals
Arithmetic
Arithmetic () is an elementary part of mathematics that consists of the study of the properties of the traditional operations on numbers— addition, subtraction, multiplication, division, exponentiation, and extraction of roots. In the 19th ...
operations on numbers may be represented by functions on Church numerals. These functions may be defined in lambda calculus
Lambda calculus (also written as ''λ''-calculus) is a formal system in mathematical logic for expressing computation based on function abstraction and application using variable binding and substitution. It is a universal model of computation ...
, or implemented in most functional programming languages (see converting lambda expressions to functions).
The addition function uses the identity .
:
The successor function is β-equivalent to .
:
The multiplication function uses the identity .
:
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.
:
Table of functions on Church numerals
* Note that in the Church encoding,
*
*
Derivation of 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 applies the function times to . The predecessor function must use the numeral to apply the function 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 and , called and . The container function is called . The left hand side of the table shows a numeral applied to and .
:
The general recurrence rule is,
:
If there is also a function to retrieve the value from the container (called ),
:
Then may be used to define the function as,
:
The function is not intrinsically useful. However, as delegates calling of to its container argument, we can arrange that on the first application receives a special container that ignores its argument allowing to skip the first application of . Call this new initial container . The right hand side of the above table shows the expansions of . Then by replacing with in the expression for the function we get the predecessor function,
:
As explained below the functions , , , and may be defined as,
:
Which gives the lambda expression for as,
:
Another way of defining pred
Pred may also be defined using pairs:
:
This is a simpler definition, but leads to a more complex expression for pred.
The expansion for :
:
Division
Division
Division or divider may refer to:
Mathematics
*Division (mathematics), the inverse of multiplication
*Division algorithm, a method for computing the result of mathematical division
Military
*Division (military), a formation typically consisting ...
of natural numbers may be implemented by,
:
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