Church encoding

Template:Short description Template:Lead too short 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.Template:Dubious In the untyped lambda calculus the only primitive data type is the function.

Use

A straightforward implementation of Church encoding slows some access operations from $O(1)$ to $O(n)$, where $n$ 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 languages instead expand their intermediate representations to contain algebraic data types. 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 types, 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. 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 numbers under Church encoding. The higher-order function that represents natural number n is a function that maps any function $f$ 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.

$f^{\circ n}=\underset{n\text{ times}}{\underbrace{f\circ f\circ \cdots \circ f}}.$

All Church numerals are functions that take two parameters. Church numerals 0, 1, 2, ..., are defined as follows in the lambda calculus.

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.:

$\begin{array}{ccc}\text{Number}& \text{Function definition}& \text{Lambda expression}\\ 0& 0fx=x& 0=\lambda f.\lambda x.x\\ 1& 1fx=fx& 1=\lambda f.\lambda x.fx\\ 2& 2fx=f(fx)& 2=\lambda f.\lambda x.f(fx)\\ 3& 3fx=f(f(fx))& 3=\lambda f.\lambda x.f(f(fx))\\ ⋮& ⋮& ⋮\\ n& nfx=f^{n}x& n=\lambda f.\lambda x.f^{\circ n}x\end{array}$

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".

Calculation with Church numerals

Arithmetic operations on numbers may be represented by functions on Church numerals. These functions may be defined in lambda calculus, or implemented in most functional programming languages (see converting lambda expressions to functions).

The addition function $\mathrm{plus}(m,n)=m+n$ uses the identity $f^{\circ (m+n)}(x)=f^{\circ m}(f^{\circ n}(x))$.

$\mathrm{plus}\equiv \lambda m.\lambda n.\lambda f.\lambda x.mf(nfx)$

The successor function $\mathrm{succ}(n)=n+1$ is β-equivalent to $(\mathrm{plus}1)$.

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

The multiplication function $\mathrm{mult}(m,n)=m*n$ uses the identity $f^{\circ (m*n)}(x)=(f^{\circ n}{)}^{\circ m}(x)$.

$\mathrm{mult}\equiv \lambda m.\lambda n.\lambda f.\lambda x.m(nf)x$

The exponentiation function $\exp (b,n)=b^n$ is given by the definition of Church numerals, $nhx=h^{n}x$. In the definition substitute $h\to b,x\to f$ to get $nbf=b^{n}f$ and,

$\exp bn=b^n=nb$

which gives the lambda expression,

$\exp \equiv \lambda b.\lambda n.nb$

The $\mathrm{pred}(n)$ function is more difficult to understand.

$\mathrm{pred}\equiv \lambda n.\lambda f.\lambda x.n(\lambda g.\lambda h.h(gf))(\lambda u.x)(\lambda u.u)$

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.

$\mathrm{minus}\equiv \lambda m.\lambda n.(n\mathrm{pred})m$

Table of functions on Church numerals

Function	Algebra	Identity	Function definition	Lambda expressions
Successor	$n+1$	$f^{n+1}x=f(f^{n}x)$	$\mathrm{succ}nfx=f(nfx)$	$\lambda n.\lambda f.\lambda x.f(nfx)$	...
Addition	$m+n$	$f^{m+n}x=f^m(f^{n}x)$	$\mathrm{plus}mnfx=mf(nfx)$	$\lambda m.\lambda n.\lambda f.\lambda x.mf(nfx)$	$\lambda m.\lambda n.n\mathrm{succ}m$
Multiplication	$m*n$	$f^{m*n}x=(f^m{)}^{n}x$	$\mathrm{multiply}mnfx=m(nf)x$	$\lambda m.\lambda n.\lambda f.\lambda x.m(nf)x$	$\lambda m.\lambda n.\lambda f.m(nf)$
Exponentiation	$b^n$	$nbf=b^{n}f$Template:Efn	$\exp bnfx=nbfx$	$\lambda b.\lambda n.\lambda f.\lambda x.nbfx$	$\lambda b.\lambda n.nb$
PredecessorTemplate:Efn	$n-1$	${\mathrm{inc}}^n\mathrm{con}=\mathrm{val}(f^{n-1}x)$	$\mathrm{if}(n==0)0\mathrm{else}(n-1)$	$\lambda n.\lambda f.\lambda x.n(\lambda g.\lambda h.h(gf))(\lambda u.x)(\lambda u.u)$
SubtractionTemplate:Efn (Monus)	$m-n$	$f^{m-n}x=(f^{-1}{)}^n(f^{m}x)$	$\mathrm{minus}mn=(n\mathrm{pred})m$	...	$\lambda m.\lambda n.n\mathrm{pred}m$

Notes: Template:Notelist

Derivation of predecessor function

The predecessor function used in the Church encoding is,

$\mathrm{pred}(n)=\{\begin{array}{cc}0& \text{if }n=0,\\ n-1& \text{otherwise}\end{array}$.

We need a way of applying the function 1 fewer times to build the predecessor. A numeral Template:Mvar applies the function Template:Mvar Template:Mvar times to Template:Mvar. The predecessor function must use the numeral Template:Mvar to apply the function Template:Math 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 Template:Mvar and Template:Mvar, called Template:Math and Template:Math. The container function is called Template:Math. The left-hand side of the table shows a numeral Template:Mvar applied to Template:Math and Template:Math.

$\begin{array}{ccc}\text{Number}& \text{Using init}& \text{Using const}\\ 0& \mathrm{init}=\mathrm{value}x& \\ 1& \mathrm{inc}\mathrm{init}=\mathrm{value}(fx)& \mathrm{inc}\mathrm{const}=\mathrm{value}x\\ 2& \mathrm{inc}(\mathrm{inc}\mathrm{init})=\mathrm{value}(f(fx))& \mathrm{inc}(\mathrm{inc}\mathrm{const})=\mathrm{value}(fx)\\ 3& \mathrm{inc}(\mathrm{inc}(\mathrm{inc}\mathrm{init}))=\mathrm{value}(f(f(fx)))& \mathrm{inc}(\mathrm{inc}(\mathrm{inc}\mathrm{const}))=\mathrm{value}(f(fx))\\ ⋮& ⋮& ⋮\\ n& n\mathrm{inc}\mathrm{init}=\mathrm{value}(f^{n}x)=\mathrm{value}(nfx)& n\mathrm{inc}\mathrm{const}=\mathrm{value}(f^{n-1}x)=\mathrm{value}((n-1)fx)\end{array}$

The general recurrence rule is,

$\mathrm{inc}(\mathrm{value}v)=\mathrm{value}(fv)$

If there is also a function to retrieve the value from the container (called Template:Math),

$\mathrm{extract}(\mathrm{value}v)=v$

Then Template:Math may be used to define the Template:Math function as,

$\mathrm{samenum}=\lambda n.\lambda f.\lambda x.\mathrm{extract}(n\mathrm{inc}\mathrm{init})=\lambda n.\lambda f.\lambda x.\mathrm{extract}(\mathrm{value}(nfx))=\lambda n.\lambda f.\lambda x.nfx=\lambda n.n$

The Template:Math function is not intrinsically useful. However, as Template:Math delegates calling of Template:Mvar to its container argument, we can arrange that on the first application Template:Math receives a special container that ignores its argument allowing to skip the first application of Template:Mvar. Call this new initial container Template:Math. The right-hand side of the above table shows the expansions of Template:Mvar Template:Math Template:Math. Then by replacing Template:Math with Template:Math in the expression for the Template:Math function we get the predecessor function,

$\mathrm{pred}=\lambda n.\lambda f.\lambda x.\mathrm{extract}(n\mathrm{inc}\mathrm{const})=\lambda n.\lambda f.\lambda x.\mathrm{extract}(\mathrm{value}((n-1)fx))=\lambda n.\lambda f.\lambda x.(n-1)fx=\lambda n.(n-1)$

As explained below the functions Template:Math, Template:Math, Template:Math, Template:Math and Template:Math may be defined as,

$\begin{array}{cc}\mathrm{value}& =\lambda v.(\lambda h.hv)\\ \mathrm{extract}k& =k\lambda u.u\\ \mathrm{inc}& =\lambda g.\lambda h.h(gf)\\ \mathrm{init}& =\lambda h.hx\\ \mathrm{const}& =\lambda u.x\end{array}$

Which gives the lambda expression for Template:Math as,

$\mathrm{pred}=\lambda n.\lambda f.\lambda x.n(\lambda g.\lambda h.h(gf))(\lambda u.x)(\lambda u.u)$

Value container The value container applies a function to its value. It is defined by, $\mathrm{value}vh=hv$ so, $\mathrm{value}=\lambda v.(\lambda h.hv)$ Inc The Template:Math function should take a value containing Template:Mvar, and return a new value containing Template:Mvar. $\mathrm{inc}(\mathrm{value}v)=\mathrm{value}(fv)$ Letting g be the value container, $g=\mathrm{value}v$ then, $gf=\mathrm{value}vf=fv$ so, $\mathrm{inc}g=\mathrm{value}(gf)$ $\mathrm{inc}=\lambda g.\lambda h.h(gf)$

Extract The value may be extracted by applying the identity function, $I=\lambda u.u$ Using Template:Mvar, $\mathrm{value}vI=v$ so, $\mathrm{extract}k=kI$ Const To implement Template:Math the Template:Math function is replaced with the Template:Math that does not apply Template:Mvar. We need Template:Math to satisfy, $\mathrm{inc}\mathrm{const}=\mathrm{value}x$ $\lambda h.h(\mathrm{const}f)=\lambda h.hx$ Which is satisfied if, $\mathrm{const}f=x$ Or as a lambda expression, $\mathrm{const}=\lambda u.x$

Another explanation of pred

A much simpler presentation is enabled using combinators notation.

$Kxy=x$

$Ix=x$

$Xfri=i(rf)$

$Prednfx=n(Xf)(Kx)I$

Now it is easy enough to see that

$Pred(Succn)fx=Succn(Xf)(Kx)I=Xf(n(Xf)(Kx))I$

$=I(n(Xf)(Kx)f)=...=I(f(f...(f(Kxf))...))=I(nfx)=nfx$

$PredZerofx=Zero(Xf)(Kx)I=KxI=x=Zerofx$

i.e. by eta-contraction, and then by induction,

$Pred(Succn)=n$

$PredZero=Zero$

$Pred(PredZero)=PredZero=Zero$

etc.

Another way of defining pred

Pred may also be defined using pairs:

$\begin{array}{cc}\mathrm{f}=& \lambda p.\mathrm{pair}(\mathrm{second}p)(\mathrm{succ}(\mathrm{second}p))\\ \mathrm{zero}=& (\lambda f.\lambda x.x)\\ \mathrm{pc0}=& \mathrm{pair}\mathrm{zero}\mathrm{zero}\\ \mathrm{pred}=& \lambda n.\mathrm{first}(n\mathrm{f}\mathrm{pc0})\\ \end{array}$

This is a simpler definition but leads to a more complex expression for pred. The expansion for $\mathrm{pred}\mathrm{three}$:

$\begin{array}{cc}\mathrm{pred}\mathrm{three}=& \mathrm{first}(\mathrm{f}(\mathrm{f}(\mathrm{f}(\mathrm{pair}\mathrm{zero}\mathrm{zero}))))\\ =& \mathrm{first}(\mathrm{f}(\mathrm{f}(\mathrm{pair}\mathrm{zero}\mathrm{one})))\\ =& \mathrm{first}(\mathrm{f}(\mathrm{pair}\mathrm{one}\mathrm{two}))\\ =& \mathrm{first}(\mathrm{pair}\mathrm{two}\mathrm{three})\\ =& \mathrm{two}\end{array}$

Division

Division of natural numbers may be implemented by,

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

Calculating $n-m$ 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.

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

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

$\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 $\mathrm{minus}nm$. However the result is that this formula gives the value of $(n-1)/m$.

This problem may be corrected by adding 1 to n before calling divide. The definition of divide is then,

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

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 $\mathrm{divide1}\to \mathrm{div}c$
• In the right hand side $\mathrm{divide1}\to c$

to get,

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

Then,

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

where,

$\begin{array}{cc}\mathrm{divide1}& =Y\mathrm{div}\\ \mathrm{succ}& =\lambda n.\lambda f.\lambda x.f(nfx)\\ Y& =\lambda f.(\lambda x.f(xx))(\lambda x.f(xx))\\ 0& =\lambda f.\lambda x.x\\ \mathrm{IsZero}& =\lambda n.n(\lambda x.\mathrm{false})\mathrm{true}\end{array}$

$\begin{array}{cc}\mathrm{true}& \equiv \lambda a.\lambda b.a\\ \mathrm{false}& \equiv \lambda a.\lambda b.b\end{array}$

$\begin{array}{cc}\mathrm{minus}& =\lambda m.\lambda n.n\mathrm{pred}m\\ \mathrm{pred}& =\lambda n.\lambda f.\lambda x.n(\lambda g.\lambda h.h(gf))(\lambda u.x)(\lambda u.u)\end{array}$

Gives,

$\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 Template:Mvar,

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

Signed numbers

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,

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

Negation is performed by swapping the values.

${\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. The OneZero function achieves this condition,

$\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,

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

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

Plus and minus

Addition is defined mathematically on the pair by,

$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,

${\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,

$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,

${\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)))$

Multiply and divide

Multiplication may be defined by,

$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_n+x_n*y_p)=[x_p*y_p+x_n*y_n,x_p*y_n+x_n*y_p]$

The last expression is translated into lambda calculus as,

${\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 (see OneZero above). The divZ function allows us to ignore the value that has a zero component.

$\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 with mult replaced by divZ.

${\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 and real numbers

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.

Translation with other representations

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.

type Church a = (a -> a) -> a -> a

church :: Integer -> Church Integer
church 0 = \f -> \x -> x
church n = \f -> \x -> f (church (n-1) f x)

unchurch :: Church Integer -> Integer
unchurch cn = cn (+ 1) 0

Church Booleans

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:

$\begin{array}{cc}\mathrm{true}& \equiv \lambda a.\lambda b.a\\ \mathrm{false}& \equiv \lambda a.\lambda b.b\end{array}$

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:

$\mathrm{predicate-}x\mathrm{then-clause}\mathrm{else-clause}$

evaluates to then-clause if predicate-x evaluates to true, and to else-clause if predicate-x 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 multiple possible implementations of not.

$\begin{array}{cc}\mathrm{and}& =\lambda p.\lambda q.pqp\\ \mathrm{or}& =\lambda p.\lambda q.ppq\\ {\mathrm{not}}_1& =\lambda p.\lambda a.\lambda b.pba\\ {\mathrm{not}}_2& =\lambda p.p(\lambda a.\lambda b.b)(\lambda a.\lambda b.a)=\lambda p.p\mathrm{false}\mathrm{true}\\ \mathrm{xor}& =\lambda a.\lambda b.a(\mathrm{not}b)b\\ \mathrm{if}& =\lambda p.\lambda a.\lambda b.pab\end{array}$

Some examples:

$\begin{array}{cc}\mathrm{and}\mathrm{true}\mathrm{false}& =(\lambda p.\lambda q.pqp)\mathrm{true}\mathrm{false}=\mathrm{true}\mathrm{false}\mathrm{true}=(\lambda a.\lambda b.a)\mathrm{false}\mathrm{true}=\mathrm{false}\\ \mathrm{or}\mathrm{true}\mathrm{false}& =(\lambda p.\lambda q.ppq)(\lambda a.\lambda b.a)(\lambda a.\lambda b.b)=(\lambda a.\lambda b.a)(\lambda a.\lambda b.a)(\lambda a.\lambda b.b)=(\lambda a.\lambda b.a)=\mathrm{true}\\ {\mathrm{not}}_1\mathrm{true}& =(\lambda p.\lambda a.\lambda b.pba)(\lambda a.\lambda b.a)=\lambda a.\lambda b.(\lambda a.\lambda b.a)ba=\lambda a.\lambda b.(\lambda c.b)a=\lambda a.\lambda b.b=\mathrm{false}\\ {\mathrm{not}}_2\mathrm{true}& =(\lambda p.p(\lambda a.\lambda b.b)(\lambda a.\lambda b.a))(\lambda a.\lambda b.a)=(\lambda a.\lambda b.a)(\lambda a.\lambda b.b)(\lambda a.\lambda b.a)=(\lambda b.(\lambda a.\lambda b.b))(\lambda a.\lambda b.a)=\lambda a.\lambda b.b=\mathrm{false}\end{array}$

Predicates

A predicate is a function that returns a Boolean value. The most fundamental predicate is $\mathrm{IsZero}$, which returns $\mathrm{true}$ if its argument is the Church numeral $0$, and $\mathrm{false}$ if its argument is any other Church numeral:

$\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:

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

Because of the identity,

$x=y\equiv (x\le y\wedge y\le x)$

The test for equality may be implemented as,

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

Church pairs

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,

$\begin{array}{cc}\mathrm{pair}& \equiv \lambda x.\lambda y.\lambda z.zxy\\ \mathrm{first}& \equiv \lambda p.p(\lambda x.\lambda y.x)\\ \mathrm{second}& \equiv \lambda p.p(\lambda x.\lambda y.y)\end{array}$

For example,

$\begin{array}{cc}& \mathrm{first}(\mathrm{pair}ab)\\ =& (\lambda p.p(\lambda x.\lambda y.x))((\lambda x.\lambda y.\lambda z.zxy)ab)\\ =& (\lambda p.p(\lambda x.\lambda y.x))(\lambda z.zab)\\ =& (\lambda z.zab)(\lambda x.\lambda y.x)\\ =& (\lambda x.\lambda y.x)ab=a\end{array}$

List encodings

An (immutable) list is constructed from list nodes. The basic operations on the list are;

Function	Description
nil	Construct an empty list.
isnil	Test if list is empty.
cons	Prepend a given value to a (possibly empty) list.
head	Get the first element of the list.
tail	Get the rest of the list.

We give four different representations of lists below:

• Build each list node from two pairs (to allow for empty lists).
• Build each list node from one pair.
• Represent the list using the right fold function.
• Represent the list using Scott's encoding that takes cases of match expression as arguments

Two pairs as a list node

A nonempty list can be implemented by a Church pair;

• First contains the head.
• Second contains the tail.

However this does not give a representation of the empty list, because there is no "null" pointer. To represent null, the pair may be wrapped in another pair, giving three values:

• First - the null pointer (empty list).
• Second.First contains the head.
• Second.Second contains the tail.

Using this idea the basic list operations can be defined like this:

Expression	Description
$\mathrm{nil}\equiv \mathrm{pair}\mathrm{true}\mathrm{true}$	The first element of the pair is true meaning the list is null.
$\mathrm{isnil}\equiv \mathrm{first}$	Retrieve the null (or empty list) indicator.
$\mathrm{cons}\equiv \lambda h.\lambda t.\mathrm{pair}\mathrm{false}(\mathrm{pair}ht)$	Create a list node, which is not null, and give it a head h and a tail t.
$\mathrm{head}\equiv \lambda z.\mathrm{first}(\mathrm{second}z)$	second.first is the head.
$\mathrm{tail}\equiv \lambda z.\mathrm{second}(\mathrm{second}z)$	second.second is the tail.

In a nil node second is never accessed, provided that head and tail are only applied to nonempty lists.

One pair as a list node

Alternatively, define

$\begin{array}{cc}\mathrm{cons}& \equiv \mathrm{pair}\\ \mathrm{head}& \equiv \mathrm{first}\\ \mathrm{tail}& \equiv \mathrm{second}\\ \mathrm{nil}& \equiv \mathrm{false}\\ \mathrm{isnil}& \equiv \lambda l.l(\lambda h.\lambda t.\lambda d.\mathrm{false})\mathrm{true}\\ \end{array}$

where the last definition is a special case of the general

$\begin{array}{cc}\mathrm{process-list}& \equiv \lambda l.l(\lambda h.\lambda t.\lambda d.\mathrm{head-and-tail-clause})\mathrm{nil-clause}\\ \end{array}$

Other operations for one pair as a list node

$\begin{array}{cc}\mathrm{tail-or-nil}& \equiv \lambda l.l(\lambda h.\lambda t.\lambda d.t)\mathrm{nil}\\ \mathrm{fold}& \equiv \lambda f.\mathrm{Y}(\lambda r.\lambda a.\lambda l.l(\lambda h.\lambda t.\lambda d.r(fah)t)a)\\ \mathrm{rfold}& \equiv \lambda f.\lambda a.\mathrm{Y}(\lambda r.\lambda l.l(\lambda h.\lambda t.\lambda d.f(rt)h)a)\\ \mathrm{length}& \equiv \mathrm{fold}(\lambda a.\lambda h.\mathrm{succ}a)\mathrm{zero}\end{array}$

---

$\begin{array}{cc}\mathrm{map}& \equiv \lambda f.\lambda l.\mathrm{rfold}(\lambda a.\lambda h.\mathrm{cons}(fh)a)\mathrm{nil}l\\ & \equiv \lambda f.\mathrm{rfold}(\lambda a.\lambda h.\mathrm{cons}(fh)a)\mathrm{nil}\\ \mathrm{filter}& \equiv \lambda f.\lambda l.\mathrm{rfold}(\lambda a.\lambda h.fh(\mathrm{cons}ha)a)\mathrm{nil}l\\ & \equiv \lambda f.\mathrm{rfold}(\lambda a.\lambda h.fh(\mathrm{cons}ha)a)\mathrm{nil}\\ \mathrm{reverse}& \equiv \lambda l.\mathrm{fold}(\lambda a.\lambda h.\mathrm{cons}ha)\mathrm{nil}l\\ & \equiv \mathrm{fold}(\lambda a.\lambda h.\mathrm{cons}ha)\mathrm{nil}\\ \mathrm{concat}& \equiv \lambda l.\lambda g.\mathrm{rfold}(\lambda a.\lambda h.\mathrm{cons}ha)gl\\ \mathrm{append}& \equiv \lambda l.\lambda v.\mathrm{concat}l(\mathrm{cons}v\mathrm{nil})\end{array}$

---

$\begin{array}{cc}\mathrm{skip}& \equiv \lambda n.\lambda l.n\mathrm{tail-or-nil}l\\ & \equiv \lambda n.n\mathrm{tail-or-nil}\\ & \equiv \mathrm{Y}(\lambda r.\lambda n.\lambda l.l(\lambda h.\lambda t.\lambda d.\mathrm{IsZero}nl(r(\mathrm{pred}n)t))\mathrm{nil})\\ \mathrm{skip-last}& \equiv \lambda n.\lambda l.\mathrm{IsZero}nl\mathrm{second}(\\ & \mathrm{Y}(\lambda r.\lambda lr.lr(\lambda h.\lambda t.\lambda d.\\ & rt(\lambda na.\lambda la.\mathrm{IsZero}na\\ & (\mathrm{pair}\mathrm{zero}(\mathrm{cons}hla))\\ & (\mathrm{pair}(\mathrm{pred}na)\mathrm{nil})\\ & ))\\ & (\mathrm{pair}n\mathrm{nil})\\ & )l)\\ \mathrm{skip-while}& \equiv \lambda f.\mathrm{Y}(\lambda r.\lambda l.l(\lambda h.\lambda t.\lambda d.fh(rt)l)\mathrm{nil})\\ \mathrm{take}& \equiv \mathrm{Y}(\lambda r.\lambda n.\lambda l.l(\lambda h.\lambda t.\lambda d.\mathrm{IsZero}n\mathrm{nil}(\mathrm{cons}h(r(\mathrm{pred}n)t)))\mathrm{nil})\\ \mathrm{take-last}& \equiv \lambda n.\lambda l.\mathrm{IsZero}nl\mathrm{second}(\\ & \mathrm{Y}(\lambda r.\lambda lr.lr(\lambda h.\lambda t.\lambda d.\\ & rt(\lambda na.\lambda la.\mathrm{IsZero}na\\ & (\mathrm{pair}\mathrm{zero}la)\\ & (\mathrm{pair}(\mathrm{pred}na)lr)\\ & ))\\ & (\mathrm{pair}n\mathrm{nil})\\ & )l)\\ \mathrm{take-while}& \equiv \lambda f.\mathrm{Y}(\lambda r.\lambda l.l(\lambda h.\lambda t.\lambda d.fd(\mathrm{cons}h(rt))\mathrm{nil})\mathrm{nil})\end{array}$

---

$\begin{array}{cc}\mathrm{all}& \equiv \mathrm{Y}(\lambda r.\lambda f.\lambda l.l(\lambda h.\lambda t.\lambda d.fh(rft)\mathrm{false})\mathrm{true})\\ \mathrm{any}& \equiv \mathrm{Y}(\lambda r.\lambda f.\lambda l.l(\lambda h.\lambda t.\lambda d.fh\mathrm{true}(rft))\mathrm{false})\\ \mathrm{element-at}& \equiv \lambda n.\lambda l.\mathrm{head}(\mathrm{skip}nl)\\ \mathrm{insert-at}& \equiv \lambda n.\lambda v.\lambda l.\mathrm{concat}(\mathrm{take}nl)(\mathrm{cons}v(\mathrm{skip}nl))\\ \mathrm{remove-at}& \equiv \lambda n.\lambda l.\mathrm{concat}(\mathrm{take}nl)(\mathrm{skip}(\mathrm{succ}n)l)\\ \mathrm{replace-at}& \equiv \lambda n.\lambda v.\lambda l.\mathrm{concat}(\mathrm{take}nl)(\mathrm{cons}v(\mathrm{skip}(\mathrm{succ}n)l))\\ \mathrm{index-of}& \equiv \lambda f.\mathrm{Y}(\lambda r.\lambda n.\lambda l.l(\lambda h.\lambda t.\lambda d.fhn(r(\mathrm{succ}n)t))\mathrm{zero})\mathrm{one}\\ \mathrm{last-index-of}& \equiv \lambda f.\mathrm{Y}(\lambda r.\lambda n.\lambda l.l(\lambda h.\lambda t.\lambda d.(\lambda i.\mathrm{IsZero}i(fhn\mathrm{zero})i)(r(\mathrm{succ}n)t))\mathrm{zero})\mathrm{one}\\ \mathrm{range}& \equiv \lambda f.\lambda z.\mathrm{Y}(\lambda r.\lambda s.\lambda n.\mathrm{IsZero}n\mathrm{nil}(\mathrm{cons}(sfz)(r(\mathrm{succ}s)(\mathrm{pred}n))))\mathrm{zero}\\ \mathrm{repeat}& \equiv \lambda v.\mathrm{Y}(\lambda r.\lambda n.\mathrm{IsZero}n\mathrm{nil}(\mathrm{cons}v(r(\mathrm{pred}n))))\\ \mathrm{zip}& \equiv Y(\lambda r.\lambda l1.\lambda l2.l1(\lambda h1.\lambda t1.\lambda d1.l2(\lambda h2.\lambda t2.\lambda d2.\mathrm{cons}(\mathrm{pair}h1h2)(rt1t2))\mathrm{nil})\mathrm{nil})\\ \end{array}$

Represent the list using right fold

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)). Equivalently, it is an application of the chain of functional compositions of partial applications, (c x ∘ c y ∘ c z) n.

$\begin{array}{cc}\mathrm{nil}& \equiv \lambda c.\lambda n.n\\ \mathrm{singleton}& \equiv \lambda h.\lambda c.\lambda n.chn\\ \mathrm{cons}& \equiv \lambda h.\lambda t.\lambda c.\lambda n.ch(tcn)\\ \mathrm{append}& \equiv \lambda l.\lambda t.\lambda c.\lambda n.lc(tcn)\\ \mathrm{isnil}& \equiv \lambda l.l(\lambda h.\lambda r.\mathrm{false})\mathrm{true}\\ \mathrm{nonempty}& \equiv \lambda l.l(\lambda h.\lambda r.true)\mathrm{false}\\ \mathrm{head}& \equiv \lambda l.l(\lambda h.\lambda r.h)\mathrm{false}\\ \mathrm{map}& \equiv \lambda f.\lambda l.\lambda c.\lambda n.l(\lambda h.\lambda r.c(fh)r)n\\ \mathrm{tail}& \equiv \lambda l.\lambda c.\lambda n.l(\lambda h.\lambda r.\lambda g.gh(rc))(\lambda c.n)(\lambda h.\lambda t.t)\end{array}$

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. Right folding over such lists uses functions which necessarily ignore the element's value, and is equivalent to the chained functional composition, i.e. (c () ∘ c () ∘ c ()) n = (f ∘ f ∘ f) n, as is used in Church numerals.

Represent the list using Scott encoding

An alternative representation is Scott encoding, which uses the idea of continuations and can lead to simpler code. (see also Mogensen–Scott encoding).

In this approach, we use the fact that lists can be observed using pattern matching expression. For example, using Scala notation, if list denotes a value of type List with empty list Nil and constructor Cons(h, t) we can inspect the list and compute nilCode in case the list is empty and Template:Code when the list is not empty:

list match {
  case Nil        => nilCode
  case Cons(h, t) => consCode(h,t)
}

The Template:Code is given by how it acts upon Template:Code and Template:Code. We therefore define a list as a function that accepts such Template:Code and Template:Code as arguments, so that instead of the above pattern match we may simply write:

$\mathrm{list}\mathrm{nilCode}\mathrm{consCode}$

Let us denote by Template:Code the parameter corresponding to Template:Code and by Template:Code the parameter corresponding to Template:Code. The empty list is the one that returns the nil argument:

$\mathrm{nil}\equiv \lambda n.\lambda c.n$

The non-empty list with head Template:Code and tail Template:Code is given by

$\mathrm{cons}ht\equiv \lambda n.\lambda c.cht$

More generally, an algebraic data type with $m$ alternatives becomes a function with $m$ parameters. When the $i$th constructor has $n_i$ arguments, the corresponding parameter of the encoding takes $n_i$ arguments as well.

Scott encoding can be done in untyped lambda calculus, whereas its use with types requires a type system with recursion and type polymorphism. A list 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:

type List = 
  C =>                    // nil argument
  (E => List => C) =>     // cons argument
  C                       // result of pattern matching

A list that can be used to compute arbitrary types would have a type that quantifies over C. A list generic Template:Clarification needed in E would also take E as the type argument.

See also

• Lambda calculus
• System F for Church numerals in a typed calculus
• Mogensen–Scott encoding
• Von Neumann definition of ordinals — another way to encode natural numbers: as sets

References

• Template:Cite journal
• Template:Cite web
• Template:Cite thesis All about Church and other similar encodings, including how to derive them and operations on them, from first principles
• Some interactive examples of Church numerals
• Lambda Calculus Live Tutorial: Boolean Algebra