Inmathematics,Church encoding is a way of representing various data types in thelambda 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, byfunctions that are taking functions as their arguments and are returning functions as their results.

TheChurch numerals are a representation of the natural numbers using lambda notation. The method is named forAlonzo 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 thealternative 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.

Church pairs are the Church encoding of thepair (two-tuple) type. The pair is represented as a function that takes a function argument. The pair itself does not decide what to do with the elements of the tuple. When given its argument it will apply the argument to the two components of the pair. The definition of the pair, theselect first element and theselect second element functions inlambda calculus are,

For example,

Church Booleans encode the Boolean valuestrue andfalse. Some programming languages use these as an implementation model for Boolean arithmetic; examples areSmalltalk andPico.

Boolean logic embodies achoice betweentwo alternatives. Thus the Church encodings oftrue andfalse are functions of two parameters:

• true chooses the first parameter ;
• false chooses the second parameter.

The two definitions in lambda calculus are:

These definitions allow predicates (i.e. functions returninglogical values) to directly act asif-test clauses, so thatif operator is just an identity function, and thus can be omitted. Each logical value already acts as anif, performing a choice between its two arguments. A Boolean value applied to two values returns either the first or the second value. The expression

${\displaystyle \mathrm{t}\mathrm{e}\mathrm{s}\mathrm{t}\text{-}\mathrm{c}\mathrm{l}\mathrm{a}\mathrm{u}\mathrm{s}\mathrm{e}\mathrm{t}\mathrm{h}\mathrm{e}\mathrm{n}\text{-}\mathrm{c}\mathrm{l}\mathrm{a}\mathrm{u}\mathrm{s}\mathrm{e}\mathrm{e}\mathrm{l}\mathrm{s}\mathrm{e}\text{-}\mathrm{c}\mathrm{l}\mathrm{a}\mathrm{u}\mathrm{s}\mathrm{e}}$

returnsthen-clause iftest-clause istrue, andelse-clause iftest-clause isfalse.

Because logical values liketrue andfalse choose their first or second argument, they can be combined to provide logical operators. Several implementations are usually possible, whether by directly manipulating parameters or by reducing to the more basic logical values. Here are the definitions, using the shortened notation as mentioned at the start of the article (p,q are predicates;a,b are general values):

Some examples:

Church numerals are the representations ofnatural numbers under Church encoding. Thehigher-order function that represents natural numbern is a function that maps any function${\displaystyle f}$ to itsn-foldcomposition. 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:

${\displaystyle n:f\mapsto f^{\circ n}}$

${\displaystyle f^{\circ n}(x)=(\underset{n\text{ times}}{\underbrace{f\circ f\circ \dots \circ f}})(x)=\underset{n\text{ times}}{\underbrace{f(f(\dots (f}}(x))\dots ))}$

Church encoding is thus aunary encoding of natural numbers,^[1] corresponding to simplecounting. Each Church numeral achieves this by construction.

All Church numerals are functions that take two parameters. Church numerals0,1,2, ..., are defined as follows in thelambda calculus:

Starting with0not applying the function at all, proceed with1applying the function once,2 applying the function twice in a row,3applying the function three times in a row, etc.:

The Church numeral3 is a chain of three applications of any given function in sequence, starting from some value. The supplied function is first applied to a supplied argument and then successively to its own result. The end result is not the number 3 (unless the supplied parameter happens to be 0 and the function is asuccessor function). The function itself, and not its end result, is the Church numeral3. The Church numeral3 means simply to do something three times. It is anostensive demonstration of what is meant by "three times".

Arithmetic operations on numbers produce numbers as their results. In Church encoding, these operations are represented bylambda abstractions which, when applied to Church numerals representing the operands, beta-reduce to the Church numerals representing the results.

Church representation of addition,${\displaystyle \mathrm{plus}(m,n)=m+n}$, uses the identity${\displaystyle f^{\circ (m+n)}(x)=(f^{\circ m}\circ f^{\circ n})(x)=f^{\circ m}(f^{\circ n}(x))}$:

${\displaystyle \mathrm{plus}\equiv \lambda mn.\lambda fx.mf(nfx)}$

The successor operation,${\displaystyle \mathrm{succ}(n)=n+1}$, is obtained byβ-reducing the expression "${\displaystyle \mathrm{plus}1}$":

${\displaystyle \mathrm{succ}\equiv \lambda n.\lambda fx.f(nfx)}$

Multiplication,${\displaystyle \mathrm{mult}(m,n)=m\ast n}$, uses the identity${\displaystyle f^{\circ (m\ast n)}(x)=(f^{\circ n}{)}^{\circ m}(x)}$:

${\displaystyle \mathrm{mult}\equiv \lambda mn.\lambda fx.m(nf)x}$

Thus${\displaystyle b(bf)\equiv (\mathrm{mult}bb)f}$ and${\displaystyle b(b(bf))\equiv (\mathrm{mult}b(\mathrm{mult}bb))f}$, and so by the virtue of Church encoding expressing then-fold composition, the exponentiation operation${\displaystyle \exp (b,n)=b^n}$ is given by

${\displaystyle \exp \equiv \lambda bn.nb\equiv \lambda bnfx.nbfx}$

The predecessor operation${\displaystyle \mathrm{pred}(n)}$ is a little bit more involved. We need to devise an operation that when repeated${\displaystyle n+1}$ times will result in${\displaystyle n}$ applications of the given function${\displaystyle f}$. This is achieved by using the identity function instead, one time only, and then switching back to${\displaystyle f}$:

${\displaystyle \mathrm{pred}\equiv \lambda nfx.n(\lambda ri.i(rf))(\lambda f.x)I}$

As previously mentioned,${\displaystyle I}$ is the identity function,${\displaystyle \lambda x.x}$. See below for a detailed explanation. This suggests implementing e.g. halving and factorial in the similar fashion,

For example,${\displaystyle \mathrm{pred}4fx}$ beta-reduces to${\displaystyle I(f(f(fx)))}$,${\displaystyle \mathrm{half}5fx}$ beta-reduces to${\displaystyle I(f(I(f(Ix))))}$, and${\displaystyle \mathrm{fact}4f}$ beta-reduces to${\displaystyle 1(2(3(4f)))}$.

Subtraction,${\displaystyle minus(m,n)=m-n}$, is expressed by repeated application of the predecessor operation a given number of times, just like addition can be expressed by repeated application of the successor operation a given number of times, etc.:

${\displaystyle \mathrm{tet}}$ is thetetration operation,${\displaystyle \mathrm{tet}m3=m^{(m^{(m^1)})}}$. Similarly to the factorial definition above, it can also be defined by using the intrinsic properties of the Church encoding, creating the "code" expression for it and letting the Church numerals themselves do the rest:

Here${\displaystyle \mathrm{tetr}3a=0aaaa=aaa=a^{(a^a)}}$.

Just as addition as repeated successor has its counterpart in the direct style, so can subtraction be expressed directly and more efficiently as well:

For example,${\displaystyle \mathrm{minus}63fx}$ reduces to an equivalent of${\displaystyle f(2fx)}$.

This also gives another predecessor version, beta-reducing${\displaystyle \lambda m.\mathrm{minus}m1}$ :

Direct definition of division is given quite similarly as

The application to${\displaystyle (\lambda x.x)}$ achieves subtraction by${\displaystyle 1}$ while creating a cycle of actions repeatedly emitting an${\displaystyle f}$ after${\displaystyle n-1}$ steps.

Instead of${\displaystyle \mathrm{Y}}$,${\displaystyle (\lambda q.mqx)}$ can also be used in each of the three definitions above.

Function	Algebra	Identity	Function definition	Lambda expressions
Successor	${\displaystyle n+1}$	${\displaystyle f^{\circ (n+1)}=f\circ f^{\circ n}}$	${\displaystyle \mathrm{succ}nfx=f(nfx)}$	${\displaystyle \lambda nfx.f(nfx)}$	...
Addition	${\displaystyle m+n}$	${\displaystyle f^{\circ (m+n)}=f^{\circ m}\circ f^{\circ n}}$	${\displaystyle \mathrm{plus}mnfx=mf(nfx)}$	${\displaystyle \lambda mnfx.mf(nfx)}$	${\displaystyle \lambda mn.n\mathrm{succ}m}$
Multiplication	${\displaystyle m\ast n}$	${\displaystyle f^{\circ (m\ast n)}=(f^{\circ m}{)}^{\circ n}}$	${\displaystyle \mathrm{multiply}mnfx=m(nf)x}$	${\displaystyle \lambda mnfx.m(nf)x}$	${\displaystyle \lambda mnf.m(nf)}$
Exponentiation	${\displaystyle b^n}$	${\displaystyle b^{\circ n}=(\mathrm{mult}b{)}^{\circ n}}$	${\displaystyle \exp bnfx=nbfx}$	${\displaystyle \lambda bnfx.nbfx}$	${\displaystyle \lambda bn.nb}$
Predecessor[a]	${\displaystyle n-1}$	${\displaystyle first((⟨i,j⟩\mapsto ⟨j,f\circ j⟩{)}^{\circ n}⟨I,I⟩)=f^{\circ (n-1)}}$	${\displaystyle \mathrm{pred}(n+1)fx=I(nfx)}$	${\displaystyle \lambda nfx.n(\lambda ri.i(rf))(\lambda f.x)(\lambda u.u)}$
Subtraction[a] (Monus)	${\displaystyle m-n}$	${\displaystyle m-n=pre{d}^{\circ n}(m)}$	${\displaystyle \mathrm{minus}mn=n\mathrm{pred}m}$	...	${\displaystyle \lambda mn.n\mathrm{pred}m}$

Notes:

The predecessor function is given as

${\displaystyle \mathrm{pred}\equiv \lambda nfx.n(\lambda ri.i(rf))(\lambda f.x)(\lambda u.u)}$

This encoding essentially uses the identity

or

The idea here is as follows. The only thing known to the Church numeral${\displaystyle \mathrm{pred}n}$ is the numeral${\displaystyle n}$ itself. Given two arguments${\displaystyle f}$ and${\displaystyle x}$, as usual, the only thing it can do is to apply that numeral to the two arguments, somehow modified so that then-long chain of applications thus created will have one (specifically, leftmost)${\displaystyle f}$ in the chain replaced by the identity function:

Here${\displaystyle Xf}$ is the modified${\displaystyle f}$, and${\displaystyle Zx}$ is the modified${\displaystyle x}$. Since${\displaystyle Xf}$ itself can not be changed, its behavior can only be modified through an additional argument,${\displaystyle A}$.

The goal is achieved, then, by passing that additional argument${\displaystyle A}$ alongfrom the outside in, while modifying it as necessary, with the definitions

Which is exactly what we have in the${\displaystyle \mathrm{pred}}$ definition's lambda expression.

Now it is easy enough to see that

i.e. by eta-contraction and then by induction, it holds that

and so on.

The identityabove may be coded with the explicit use of pairs. It can be done in several ways, for instance,

The expansion for${\displaystyle {\mathrm{pred}}_{2}3}$ is:

This is a simpler definition to devise but leads to a more complex lambda expression,

Pairs in the lambda calculus are essentially just extra arguments, whether passing them inside out like here, or from the outside in as in the original${\displaystyle \mathrm{pred}}$ definition. Another encoding follows the second variant of the predecessor identity directly,

This way it is already quite close to the original, "outside-in"${\displaystyle \mathrm{pred}}$ definition, also creating the chain of${\displaystyle f}$s like it does, only in a bit more wasteful way still. But it is very much less wasteful than the previous,${\displaystyle {\mathrm{pred}}_2}$ definition here. Indeed if we trace its execution we arrive at the new, even more streamlined, yet fully equivalent, definition

which makes it fully clear and apparent that this is all about just argument modification and passing. Its reduction proceeds as

clearly showing what is going on. Still, the original${\displaystyle \mathrm{pred}}$ is much preferable since it's working in the top-down manner and is thus able to stop right away if the user-supplied function${\displaystyle f}$ is short-circuiting. The top-down approach is also used with other definitions like

Division of natural numbers may be implemented by,^[2]

${\displaystyle n/m=\mathrm{if}n\ge m\mathrm{then}1+(n-m)/m\mathrm{else}0}$

Calculating${\displaystyle n-m}$ with${\displaystyle \lambda nm.m\mathrm{pred}n}$ 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 (unless the direct subtraction definition is used, see above). The simplest predicate for testing numbers isIsZero so consider the condition.

${\displaystyle \mathrm{IsZero}(\mathrm{minus}nm)}$

But this condition is equivalent to${\displaystyle n\le m}$, not. If this expression is used then the mathematical definition of division given above is translated into function on Church numerals as,

${\displaystyle \mathrm{divide1}nmfx=(\lambda d.\mathrm{IsZero}d(0fx)(f(\mathrm{divide1}dmfx)))(\mathrm{minus}nm)}$

As desired, this definition has a single call to${\displaystyle \mathrm{minus}nm}$. However the result is that this formula gives the value of${\displaystyle (n-1)/m}$.

This problem may be corrected by adding 1 ton before callingdivide. The definition ofdivide is then,

${\displaystyle \mathrm{divide}n=\mathrm{divide1}(\mathrm{succ}n)}$

divide1 is a recursive definition. TheY combinator may be used to implement the recursion. Create a new function calleddiv by;

• In the left hand side${\displaystyle \mathrm{divide1}\to \mathrm{div}c}$
• In the right hand side${\displaystyle \mathrm{divide1}\to c}$

to get,

${\displaystyle \mathrm{div}=\lambda c.\lambda n.\lambda m.\lambda f.\lambda x.(\lambda d.\mathrm{IsZero}d(0fx)(f(cdmfx)))(\mathrm{minus}nm)}$

Then,

${\displaystyle \mathrm{divide}=\lambda n.\mathrm{divide1}(\mathrm{succ}n)}$

where,

Gives,

${\displaystyle \mathrm{divide}=\lambda n.((\lambda f.(\lambda x.xx)(\lambda x.f(xx)))(\lambda c.\lambda n.\lambda m.\lambda f.\lambda x.(\lambda d.(\lambda n.n(\lambda x.(\lambda a.\lambda b.b))(\lambda a.\lambda b.a))d((\lambda f.\lambda x.x)fx)(f(cdmfx)))((\lambda m.\lambda n.n(\lambda n.\lambda f.\lambda x.n(\lambda g.\lambda h.h(gf))(\lambda u.x)(\lambda u.u))m)nm)))((\lambda n.\lambda f.\lambda x.f(nfx))n)}$

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))

For example, 9/3 is represented by

divide (\f.\x.f (f (f (f (f (f (f (f (f x))))))))) (\f.\x.f (f (f x)))

Using a lambda calculus calculator, the above expression reduces to 3, using normal order.

\f.\x.f (f (f (x)))

Apredicate is a function that returns a Boolean value. The most fundamental predicate on Church numerals is${\displaystyle \mathrm{IsZero}}$, which returns${\displaystyle \mathrm{true}}$ if its argument is the Church numeral${\displaystyle 0}$, and${\displaystyle \mathrm{false}}$ otherwise:

${\displaystyle \mathrm{IsZero}=\lambda n.n(\lambda x.\mathrm{false})\mathrm{true}}$

The following predicate tests whether the first argument is less-than-or-equal-to the second:

${\displaystyle \mathrm{LEQ}=\lambda m.\lambda n.\mathrm{IsZero}(\mathrm{minus}mn)}$

Because of the identity

${\displaystyle x=y\equiv (x\le y\wedge y\le x)}$

the test for equality can be implemented as

${\displaystyle \mathrm{EQ}=\lambda m.\lambda n.\mathrm{and}(\mathrm{LEQ}mn)(\mathrm{LEQ}nm)}$

Most real-world languages have support for machine-native integers; thechurch andunchurch functions convert between nonnegative integers and their corresponding Church numerals. The functions are given here inHaskell, where the\ corresponds to the λ of Lambda calculus. Implementations in other languages are similar.

typeChurcha=(a->a)->a->achurch::Integer->ChurchIntegerchurch0=\f->\x->xchurchn=\f->\x->f(church(n-1)fx)unchurch::ChurchInteger->Integerunchurchcn=cn(+1)0

One simple approach for extending Church Numerals tosigned numbers is to use a Church pair, containing Church numerals representing a positive and a negative value.^[3] The integer value is the difference between the two Church numerals.

A natural number is converted to a signed number by,

${\displaystyle {\mathrm{convert}}_s=\lambda x.\mathrm{pair}x0}$

Negation is performed by swapping the values.

${\displaystyle {\mathrm{neg}}_s=\lambda x.\mathrm{pair}(\mathrm{second}x)(\mathrm{first}x)}$

The integer value is more naturally represented if one of the pair is zero. TheOneZero function achieves this condition,

${\displaystyle \mathrm{OneZero}=\lambda x.\mathrm{IsZero}(\mathrm{first}x)x(\mathrm{IsZero}(\mathrm{second}x)x(\mathrm{OneZero}(\mathrm{pair}(\mathrm{pred}(\mathrm{first}x))(\mathrm{pred}(\mathrm{second}x)))))}$

The recursion may be implemented using the Y combinator,

${\displaystyle \mathrm{OneZ}=\lambda c.\lambda x.\mathrm{IsZero}(\mathrm{first}x)x(\mathrm{IsZero}(\mathrm{second}x)x(c(\mathrm{pair}(\mathrm{pred}(\mathrm{first}x))(\mathrm{pred}(\mathrm{second}x)))))}$

${\displaystyle \mathrm{OneZero}=Y\mathrm{OneZ}}$

Addition is defined mathematically on the pair by,

${\displaystyle x+y=[x_p,x_n]+[y_p,y_n]=x_p-x_n+y_p-y_n=(x_p+y_p)-(x_n+y_n)=[x_p+y_p,x_n+y_n]}$

The last expression is translated into lambda calculus as,

${\displaystyle {\mathrm{plus}}_s=\lambda x.\lambda y.\mathrm{OneZero}(\mathrm{pair}(\mathrm{plus}(\mathrm{first}x)(\mathrm{first}y))(\mathrm{plus}(\mathrm{second}x)(\mathrm{second}y)))}$

Similarly subtraction is defined,

${\displaystyle x-y=[x_p,x_n]-[y_p,y_n]=x_p-x_n-y_p+y_n=(x_p+y_n)-(x_n+y_p)=[x_p+y_n,x_n+y_p]}$

giving,

${\displaystyle {\mathrm{minus}}_s=\lambda x.\lambda y.\mathrm{OneZero}(\mathrm{pair}(\mathrm{plus}(\mathrm{first}x)(\mathrm{second}y))(\mathrm{plus}(\mathrm{second}x)(\mathrm{first}y)))}$

Multiplication may be defined by,

${\displaystyle x\ast y=[x_p,x_n]\ast [y_p,y_n]=(x_p-x_n)\ast (y_p-y_n)=(x_p\ast y_p+x_n\ast y_n)-(x_p\ast y_n+x_n\ast y_p)=[x_p\ast y_p+x_n\ast y_n,x_p\ast y_n+x_n\ast y_p]}$

The last expression is translated into lambda calculus as,

${\displaystyle {\mathrm{mult}}_s=\lambda x.\lambda y.\mathrm{pair}(\mathrm{plus}(\mathrm{mult}(\mathrm{first}x)(\mathrm{first}y))(\mathrm{mult}(\mathrm{second}x)(\mathrm{second}y)))(\mathrm{plus}(\mathrm{mult}(\mathrm{first}x)(\mathrm{second}y))(\mathrm{mult}(\mathrm{second}x)(\mathrm{first}y)))}$

A similar definition is given here for division, except in this definition, one value in each pair must be zero (seeOneZero above). ThedivZ function allows us to ignore the value that has a zero component.

${\displaystyle \mathrm{divZ}=\lambda x.\lambda y.\mathrm{IsZero}y0(\mathrm{divide}xy)}$

divZ is then used in the following formula, which is the same as for multiplication, but withmult replaced bydivZ.

${\displaystyle {\mathrm{divide}}_s=\lambda x.\lambda y.\mathrm{pair}(\mathrm{plus}(\mathrm{divZ}(\mathrm{first}x)(\mathrm{first}y))(\mathrm{divZ}(\mathrm{second}x)(\mathrm{second}y)))(\mathrm{plus}(\mathrm{divZ}(\mathrm{first}x)(\mathrm{second}y))(\mathrm{divZ}(\mathrm{second}x)(\mathrm{first}y)))}$

Rational andcomputable 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.^[4][5] 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 theChurch–Turing thesis.

Alist contains some items in order. The basicoperations on lists are:

A representation of lists should provide ways to implement these operations.

The archetypal lambda calculus representation of lists is Church List encoding. It represents lists asright folds, as functions to return the results of folding over the list with user-supplied arguments.

It follows the paradigm of "a thing is the result of its observation". No matter the concrete implementation, folding a given list of values results in the same result. This provides an abstract view at what a list is. Church List encoding is such a mechanism.

On the other hand, seen more concretely, lists can be represented as a sequence oflinked listnodes.

What follows are four different representations of lists:

• Church lists –right fold representation.
• Two Church pairs for each list node.
• One Church pair for each list node.
• Scott encoding.

This is the original Church encoding for lists. A list is represented by a binary function, that, when supplied with two arguments, – a "combining function" and a "sentinel value", – will perform theright fold of the encoded list using those two arguments.

For an empty list the sentinel value is returned as the folding's result. The result of folding a non-empty list withhead h andtail t is the result of combining, by the supplied function, of thehead h with theresult of folding the tail t with the supplied two arguments. Thus the combining function's two arguments are, conceptually, thecurrent element and theresult of folding therest of the list.

For example, a list of three elements x, y and z is represented by a term that when applied to c and n returns c x (c y (c z n)). Equivalently, it is an application of the chain offunctional compositions (${\displaystyle \circ }$ ) of partial applications, ((c x)${\displaystyle \circ }$ (c y)${\displaystyle \circ }$ (c z)) n.