Church encoding

Church Booleans

Church Booleans encode 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 embodies a choice between two alternatives. Thus the Church encodings of true and false are functions of two parameters:

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

The two definitions in lambda calculus are:

${\displaystyle \begin{array}{cc}\mathrm{true}& \equiv \lambda a.\lambda b.a=\lambda a.\lambda b.\mathrm{first}(\mathrm{pair}ab)\\ \mathrm{false}& \equiv \lambda a.\lambda b.b=\lambda a.\lambda b.\mathrm{second}(\mathrm{pair}ab)\end{array}}$

These definitions allow predicates (i.e. functions returning logical values) to directly act as if-test clauses, so that if operator is just an identity function, and thus can be omitted. Each logical value already acts as an if, 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}}$

returns then-clause if test-clause is true, and else-clause if test-clause is false.

Because logical values like true and false 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):

${\displaystyle \begin{array}{cccc}\mathrm{if}& =\lambda pab.pab& & \\ \mathrm{and}& =\lambda pq.pqp& & =\lambda pqab.p(qab)b\\ \mathrm{or}& =\lambda pq.ppq& & =\lambda pqab.pa(qab)\\ \mathrm{not}& =\lambda p.p\mathrm{false}\mathrm{true}& & =\lambda pab.pba\\ \mathrm{xor}& =\lambda pq.p(\mathrm{not}q)q& & =\lambda pqab.p(qba)(qab)\\ \mathrm{nand}& =\lambda pq.\mathrm{not}(\mathrm{and}pq)& & =\lambda pqab.p(qba)a\\ \mathrm{implies}& =\lambda pq.\mathrm{or}(\mathrm{not}p)q& & =\lambda pqab.p(qab)a\end{array}}$

Some examples:

${\displaystyle \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}\end{array}}$

${\displaystyle \begin{array}{cc}\mathrm{not}& \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}\end{array}}$

Optional values

An Optional value is represented as

${\displaystyle \begin{array}{cc}\mathrm{none}\equiv & \lambda f.\lambda s.f\\ \mathrm{val}\equiv \lambda v.& \lambda f.\lambda s.sv\end{array}}$

Using such a value means supplying it with two arguments – one, ${\displaystyle f}$, for the "failure" case, i.e. lack of a value, and the other, ${\displaystyle s}$, in case of "success," is a handler function which is presented with that value.

The optional value itself "knows" which case it is, and selects which argument to use, accordingly. It "knows" this by virtue of being created that way – either it was created as ${\displaystyle \mathrm{none}}$, or as ${\displaystyle \mathrm{val}v}$.

The user of an optional value has no way of knowing which case it is except by supplying it with the two arguments, one for each of the two possible cases.

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 ${\displaystyle f}$ to its n-fold composition. 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 a unary encoding of natural numbers, corresponding to simple counting. Each Church numeral achieves this by construction.

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 in a row, 3 applying the function three times in a row, etc.:

${\displaystyle \begin{array}{rll}\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^{\circ n}x& n=\lambda f.\lambda x.f^{\circ n}x\end{array}}$

The Church numeral 3 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 a successor function). The function itself, and not its end result, is the Church numeral 3. The Church numeral 3 means simply to do something three times. It is an ostensive demonstration of what is meant by "three times".

Calculation with Church numerals

Arithmetic operations on numbers produce numbers as their results. In Church encoding, these operations are represented by lambda 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 the n-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}$. The variable name ${\displaystyle r}$ is chosen as a mnemonic for "recursive result." This definition employs an additional argument to use the state-passing paradigm, since lambda calculus lacks mutation (so nothing can be changed, only replaced). See below for the detailed explanation.

This suggests implementing e.g. halving and factorial functions in the similar state-passing fashion,

${\displaystyle \begin{array}{cc}\mathrm{half}& \equiv \lambda nfx.n(\lambda rab.a(rba))(\lambda ab.x)If\\ \mathrm{fact}& \equiv \lambda nf.n(\lambda ra.a(r(\mathrm{succ}a)))(\lambda a.f)1\end{array}}$

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 \begin{array}{cc}(-)& \equiv \lambda mn.n\mathrm{pred}m\\ (+)& \equiv \lambda mn.n\mathrm{succ}m\\ (\times )& \equiv \lambda mn.n((+)m)0\\ \exp & \equiv \lambda mn.n((\times )m)1\{-m^n-\}\\ (\uparrow <!--\; -->\uparrow )& \equiv \lambda mn.n(\exp m)1\{-m\uparrow <!--\; -->\uparrow n-\}\\ {\uparrow }^k& \equiv k(\lambda fmn.n(fm)1)(\times )\\ & \equiv \lambda m.k(\lambda fn.nf1)(\times m)\end{array}}$

${\displaystyle (\uparrow <!--\; -->\uparrow )}$ is the tetration operation, ${\displaystyle m\uparrow <!--\; -->\uparrow 3=m^{(m^{(m^1)})}}$, and ${\displaystyle {\uparrow }^k}$ is Knuth's ${\displaystyle k}$ th arrow in general.

Similarly to the factorial definition above, tetration 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:

${\displaystyle \begin{array}{cc}\mathrm{tet}& \equiv \lambda mn.n(\lambda r.rm)1\end{array}}$

Here, again, ${\displaystyle \mathrm{tet}m3=1mmm=m^{(m^{(m^1)})}}$.

Direct subtraction and division

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

${\displaystyle \begin{array}{cc}\mathrm{minus}\equiv \lambda & mnfx.\\ & m(\lambda rq.qr)(\lambda q.x)\\ & (n(\lambda qr.rq)(\mathrm{Y}(\lambda qr.f(rq))))\end{array}}$

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

${\displaystyle \begin{array}{cc}\mathrm{p}\mathrm{r}\mathrm{e}{\mathrm{d}}^{\prime }\equiv \lambda mfx.m& (\lambda rq.qr)(\lambda q.x)\\ & (\lambda r.r(\mathrm{Y}(\lambda qr.f(rq))))\end{array}}$

Direct definition of division is given quite similarly as

${\displaystyle \begin{array}{cc}\mathrm{div}\equiv \lambda & mnfx.\\ & m(\lambda rq.qr)(\lambda q.x)\\ & (\mathrm{Y}(\lambda q.n(\lambda qr.rq)(\lambda r.f(rq))(\lambda x.x)))\end{array}}$

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.

Table of functions on Church numerals

Notes:

Predecessor function

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

${\displaystyle first((⟨i,j⟩\mapsto ⟨j,f\circ j⟩{)}^{\circ n}⟨I,I⟩)=\{\begin{array}{ll}I& \text{if }n=0,\\ f^{\circ (n-1)}& \text{otherwise}\end{array}}$

or

${\displaystyle first((⟨x,y⟩\mapsto ⟨y,f(y)⟩{)}^{\circ n}⟨x,x⟩)=\{\begin{array}{ll}x& \text{if }n=0,\\ f^{\circ (n-1)}(x)& \text{otherwise}\end{array}}$

An explanation of pred

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 the n-long chain of applications thus created will have one (specifically, leftmost) ${\displaystyle f}$ in the chain replaced by the identity function:

${\displaystyle \begin{array}{cc}{f}^{\circ (n-1)}(x)& =\underset{n\text{ times}}{\underbrace{I(\underset{n-1\text{ times}}{\underbrace{f(f(\dots (f}}}}(x))\dots )))=(Xf{)}^{\circ n}(Zx)A\\ & =\underset{n\text{ times}}{\underbrace{Xf(Xf(\dots (Xf}}(Zx))\dots ))A\\ & =Xf{r}_1{A}_1\{-anditmustbeequalto:-\}\\ & =I(Xf{r}_2{A}_2)\\ & =I(f(Xf{r}_3{A}_3))\\ & =I(f(f(Xf{r}_4{A}_4)))\\ & \dots \\ & =I(f(f\dots (Xf{r}_n{A}_n)\dots ))\\ & =\underset{n\text{ times}}{\underbrace{I(f(f\dots (f}}(Zx{A}_{n+1}))\dots ))\end{array}}$

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}$ along from the outside in, while modifying it as necessary, with the definitions

${\displaystyle \begin{array}{cc}{A}_1& =I\\ A_{i>1}& =f\\ Zxf& =x=Kxf\\ Xfr{A}_i& =A_i(r{A}_{i+1})\{-i.e.,-\}\\ Xfri& =i(rf)\end{array}}$

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

Now it is easy enough to see that

${\displaystyle \begin{array}{cc}\mathrm{pred}(\mathrm{succ}n)fx& =\mathrm{succ}n(Xf)(Kx)I\\ & =Xf(n(Xf)(Kx))I\\ & =I(n(Xf)(Kx)f)\\ & =\dots \\ & =I(f(f\dots (f(Kxf))\dots ))\\ & =I(nfx)\\ & =nfx\end{array}}$

${\displaystyle \begin{array}{cc}\mathrm{pred}0fx& =0(Xf)(Kx)I\\ & =KxI\\ & =x\\ & =0fx\end{array}}$

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

${\displaystyle \begin{array}{cccc}& \mathrm{pred}(\mathrm{succ}n)& & =n\\ & \mathrm{pred}0& & =0\\ & \mathrm{pred}(\mathrm{pred}0)& & =\mathrm{pred}0=0\\ & \dots \end{array}}$

and so on.

Defining pred through pairs

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

${\displaystyle \begin{array}{cc}\mathrm{f}=& \lambda p.\mathrm{pair}(\mathrm{second}p)(\mathrm{succ}(\mathrm{second}p))\\ {\mathrm{pred}}_2=& \lambda n.\mathrm{first}(n\mathrm{f}(\mathrm{pair}00))\end{array}}$

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

${\displaystyle \begin{array}{cc}{\mathrm{pred}}_{2}3=& \mathrm{first}(\mathrm{f}(\mathrm{f}(\mathrm{f}(\mathrm{pair}00))))\\ =& \mathrm{first}(\mathrm{f}(\mathrm{f}(\mathrm{pair}01)))\\ =& \mathrm{first}(\mathrm{f}(\mathrm{pair}12))\\ =& \mathrm{first}(\mathrm{pair}23)\\ =& 2\end{array}}$

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

${\displaystyle \begin{array}{cc}{\mathrm{pred}}_2\equiv \lambda n.n& (\lambda p.p(\lambda abh.hb(\mathrm{succ}b)))(\lambda h.h00)(\lambda ab.a)\end{array}}$

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,

${\displaystyle \begin{array}{cc}{\mathrm{pred}}_3\equiv \lambda nfx.n& (\lambda p.p(\lambda abh.hb(fb)))(\lambda h.hxx)(\lambda ab.a)\end{array}}$

This way, it is already close to the original, "outside-in" ${\displaystyle \mathrm{pred}}$ definition, also creating the chain of ${\displaystyle f}$s like it does, in a more wasteful way. But it is 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

${\displaystyle \begin{array}{cc}{\mathrm{pred}}_4\equiv \lambda nfx.n& (\lambda rab.rb(fb))Kxx\end{array}}$

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

${\displaystyle \begin{array}{cc}{\mathrm{pred}}_{4}3fx& =(..(..(..K)))xx\\ & =(..(..K))x(fx)\\ & =(..K)(fx)(f(fx))\\ & =K(f(fx))(f(f(fx)))\\ & =f(fx)\end{array}}$

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

${\displaystyle \begin{array}{cc}{\mathrm{pred}}_5\equiv \lambda nfx.n& (\lambda rab.a(rbb))(\lambda ab.x)If\\ \mathrm{third}\equiv \lambda nfx.n& (\lambda rabc.a(rbca))(\lambda abc.x)IIf\\ \mathrm{thirdRounded}\equiv \lambda nfx.n& (\lambda rabc.a(rbca))(\lambda abc.x)IfI\\ \mathrm{twoThirds}\equiv \lambda nfx.n& (\lambda rabc.a(rbca))(\lambda abc.x)Iff\\ \mathrm{factorial}\equiv \lambda nfx.n& (\lambda ra.a(r(\mathrm{succ}a)))(\lambda a.f)1x\end{array}}$

Division via general recursion

Division of natural numbers may be implemented by,

${\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 is IsZero so consider the condition.

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

But this condition is equivalent to ${\displaystyle n\le m}$, not ${\displaystyle n<m}$. 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 to n before calling divide. The definition of divide is then,

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

${\displaystyle \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}}$

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

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

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

Predicates

A predicate 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)}$

In programming languages

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.

<span id="mwAkw"></span><span class="kr" id="mwAk0">type</span><span class="w" id="mwAk4"> </span><span class="kt" id="mwAk8">Church</span><span class="w" id="mwAlA"> </span><span class="n" id="mwAlE">a</span><span class="w" id="mwAlI"> </span><span class="ow" id="mwAlM">=</span><span class="w" id="mwAlQ"> </span><span class="p" id="mwAlU">(</span><span class="n" id="mwAlY">a</span><span class="w" id="mwAlc"> </span><span class="ow" id="mwAlg">-></span><span class="w" id="mwAlk"> </span><span class="n" id="mwAlo">a</span><span class="p" id="mwAls">)</span><span class="w" id="mwAlw"> </span><span class="ow" id="mwAl0">-></span><span class="w" id="mwAl4"> </span><span class="n" id="mwAl8">a</span><span class="w" id="mwAmA"> </span><span class="ow" id="mwAmE">-></span><span class="w" id="mwAmI"> </span><span class="n" id="mwAmM">a</span> <span class="nf" id="mwAmQ">church</span><span class="w" id="mwAmU"> </span><span class="ow" id="mwAmY">::</span><span class="w" id="mwAmc"> </span><span class="kt" id="mwAmg">Integer</span><span class="w" id="mwAmk"> </span><span class="ow" id="mwAmo">-></span><span class="w" id="mwAms"> </span><span class="kt" id="mwAmw">Church</span><span class="w" id="mwAm0"> </span><span class="kt" id="mwAm4">Integer</span> <span class="nf" id="mwAm8">church</span><span class="w" id="mwAnA"> </span><span class="mi" id="mwAnE">0</span><span class="w" id="mwAnI"> </span><span class="ow" id="mwAnM">=</span><span class="w" id="mwAnQ"> </span><span class="nf" id="mwAnU">\</span><span class="n" id="mwAnY">f</span><span class="w" id="mwAnc"> </span><span class="ow" id="mwAng">-></span><span class="w" id="mwAnk"> </span><span class="nf" id="mwAno">\</span><span class="n" id="mwAns">x</span><span class="w" id="mwAnw"> </span><span class="ow" id="mwAn0">-></span><span class="w" id="mwAn4"> </span><span class="n" id="mwAn8">x</span> <span class="nf" id="mwAoA">church</span><span class="w" id="mwAoE"> </span><span class="n" id="mwAoI">n</span><span class="w" id="mwAoM"> </span><span class="ow" id="mwAoQ">=</span><span class="w" id="mwAoU"> </span><span class="nf" id="mwAoY">\</span><span class="n" id="mwAoc">f</span><span class="w" id="mwAog"> </span><span class="ow" id="mwAok">-></span><span class="w" id="mwAoo"> </span><span class="nf" id="mwAos">\</span><span class="n" id="mwAow">x</span><span class="w" id="mwAo0"> </span><span class="ow" id="mwAo4">-></span><span class="w" id="mwAo8"> </span><span class="n" id="mwApA">f</span><span class="w" id="mwApE"> </span><span class="p" id="mwApI">(</span><span class="n" id="mwApM">church</span><span class="w" id="mwApQ"> </span><span class="p" id="mwApU">(</span><span class="n" id="mwApY">n</span><span class="o" id="mwApc">-</span><span class="mi" id="mwApg">1</span><span class="p" id="mwApk">)</span><span class="w" id="mwApo"> </span><span class="n" id="mwAps">f</span><span class="w" id="mwApw"> </span><span class="n" id="mwAp0">x</span><span class="p" id="mwAp4">)</span> <span class="nf" id="mwAp8">unchurch</span><span class="w" id="mwAqA"> </span><span class="ow" id="mwAqE">::</span><span class="w" id="mwAqI"> </span><span class="kt" id="mwAqM">Church</span><span class="w" id="mwAqQ"> </span><span class="kt" id="mwAqU">Integer</span><span class="w" id="mwAqY"> </span><span class="ow" id="mwAqc">-></span><span class="w" id="mwAqg"> </span><span class="kt" id="mwAqk">Integer</span> <span class="nf" id="mwAqo">unchurch</span><span class="w" id="mwAqs"> </span><span class="n" id="mwAqw">cn</span><span class="w" id="mwAq0"> </span><span class="ow" id="mwAq4">=</span><span class="w" id="mwAq8"> </span><span class="n" id="mwArA">cn</span><span class="w" id="mwArE"> </span><span class="p" id="mwArI">(</span><span class="o" id="mwArM">+</span><span class="w" id="mwArQ"> </span><span class="mi" id="mwArU">1</span><span class="p" id="mwArY">)</span><span class="w" id="mwArc"> </span><span class="mi" id="mwArg">0</span>

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,

${\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. The OneZero 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}}$

Plus and minus

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

Multiply and divide

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 (see OneZero above). The divZ 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 with mult replaced by divZ.

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

List encodings

A list contains some items in order. The basic operations on lists are:

A representation of lists should provide ways to implement these operations. Some of these operations can be defined in terms of others, like

${\displaystyle \begin{array}{cc}\mathrm{singleton}& \equiv \lambda v.\mathrm{cons}v\mathrm{nil}\\ \mathrm{cons}& \equiv \lambda h.\mathrm{append}(\mathrm{singleton}h)\\ \mathrm{append}& \equiv \lambda lr.\mathrm{foldr}\mathrm{cons}rl\\ \mathrm{isnil}& \equiv \mathrm{foldr}(\lambda hr.\mathrm{false})\mathrm{true}\\ \mathrm{head}& \equiv \mathrm{foldr}(\lambda hr.h)\mathrm{nil}\\ \mathrm{map}& \equiv \lambda f.\mathrm{foldr}(\lambda h.\mathrm{cons}(fh))\mathrm{nil}\end{array}}$

Like this definition of ${\displaystyle \mathrm{map}}$, many more functions can be defined in terms of structural recursion (right fold, i.e. catamorphism, also paramorphism, etc.), or general recursion using fixpoint recursion.

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

It follows the paradigm of "a thing is something that can be observed". 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 of linked list nodes. Two possible encodings use either two Church pairs for each list node, or just one pair per each node.

Seen as an algebraic data type, lists are represented via Scott encoding.

Church lists – right fold representation

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 the right 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 with head h and tail t is the result of combining, by the supplied function, of the head h with the result of folding the tail t with the supplied two arguments. Thus the combining function's two arguments are, conceptually, the current element and the result of folding the rest 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 of functional compositions ( ${\displaystyle \circ }$ ) of partial applications, ((c x) ${\displaystyle \circ }$ (c y) ${\displaystyle \circ }$ (c z)) n.

${\displaystyle \begin{array}{cc}\mathrm{nil}& \equiv \lambda cn.n\\ \mathrm{cons}& \equiv \lambda ht.\lambda cn.ch(tcn)\\ \mathrm{singleton}& \equiv \lambda h.\lambda cn.chn\\ \mathrm{foldr}& \equiv \lambda cnl.lcn\\ \mathrm{isnil}& \equiv \lambda l.l(\lambda hr.\mathrm{false})\mathrm{true}\\ \mathrm{append}& \equiv \lambda lm.\lambda cn.lc(mcn)\\ & \equiv \lambda lm.\lambda cn.\mathrm{foldr}c(\mathrm{foldr}cnm)l\\ \mathrm{head}& \equiv \lambda l.l(\lambda hr.h)\mathrm{nil}\\ \mathrm{safehead}& \equiv \lambda les.l(\lambda hr.sh)e\\ \mathrm{map}& \equiv \lambda fl.\lambda cn.l(\lambda hr.c(fh)r)n\\ \mathrm{tail}& \equiv \lambda l.\lambda cn.l(\lambda hrg.gh(rc))(\lambda g.n)(\lambda ht.t)\end{array}}$

This encoding follows the following logic: the equations

foldr c n [ ] = n foldr c n [x ] = c x n foldr c n [x,y,z] = c x (foldr c n [y,z]) = c x (c y (c z n))

mean that

${\displaystyle \begin{array}{cccc}& \{[]\}& & \equiv \lambda cn.n\\ & \{[x]\}& & \equiv \lambda cn.cxn\\ & \{[x,y,z]\}& & \equiv \lambda cn.cx(cy(czn))\end{array}}$

where ${\displaystyle \{l\}=\lambda cn.\mathrm{foldr}cnl}$ denotes the Church List representation of the list ${\displaystyle l}$.

Since Church encoded list is its own folding function, folding it just means applying that function to the supplied arguments.

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 ()) ${\displaystyle \circ }$ (c ()) ${\displaystyle \circ }$ (c ()) ) n = (f ${\displaystyle \circ }$ f ${\displaystyle \circ }$ f) n, as is used in Church numerals.

Two pairs as a list node

A nonempty list can be represented by a Church pair, where

• first contains the list's head
• second contains the list's tail

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

• first - the null list indicator (a Boolean).
• first of second contains the head (car).
• second of second contains the tail (cdr).

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

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

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

where the definitions like the last one all follow the same general pattern for the safe use of a list, with ${\displaystyle h}$ and ${\displaystyle t}$ referring to the list's head and tail, and ${\displaystyle d}$ being discarded, as an artificial device:

${\displaystyle \begin{array}{c}\lambda l.l(\lambda htd.⟨\mathrm{h}\mathrm{e}\mathrm{a}\mathrm{d}\text{-}\mathrm{a}\mathrm{n}\mathrm{d}\text{-}\mathrm{t}\mathrm{a}\mathrm{i}\mathrm{l}\text{-}\mathrm{c}\mathrm{l}\mathrm{a}\mathrm{u}\mathrm{s}\mathrm{e}⟩)⟨\mathrm{n}\mathrm{i}\mathrm{l}\text{-}\mathrm{c}\mathrm{l}\mathrm{a}\mathrm{u}\mathrm{s}\mathrm{e}⟩\end{array}}$

Other operations in this encoding are:

${\displaystyle \begin{array}{cc}\mathrm{lfold}& \equiv \lambda g.\mathrm{Y}(\lambda r.\lambda al.l(\lambda htd.r(gah)t)a)\\ \mathrm{foldr}& \equiv \lambda gz.\mathrm{Y}(\lambda r.\lambda l.l(\lambda htd.gh(rt))z)\\ \mathrm{zip}& \equiv Y(\lambda rlm.l(\lambda htd.m(\lambda esz.\\ & \mathrm{cons}(\mathrm{pair}he)(rts))\mathrm{nil})\mathrm{nil})\end{array}}$

${\displaystyle \begin{array}{cc}\mathrm{drop}\equiv & \lambda n.n(\lambda rl.l(\lambda htd.rt)\mathrm{nil})(\lambda l.l)\\ \mathrm{d}\mathrm{r}\mathrm{o}\mathrm{p}\text{-}\mathrm{w}\mathrm{h}\mathrm{i}\mathrm{l}\mathrm{e}\equiv & \lambda p.\mathrm{Y}(\lambda rl.l(\lambda htd.ph(rt)l)\mathrm{nil})\\ \mathrm{d}\mathrm{r}\mathrm{o}\mathrm{p}\text{-}\mathrm{u}\mathrm{n}\mathrm{t}\mathrm{i}\mathrm{l}\equiv & \lambda p.\mathrm{Y}(\lambda rl.l(\lambda htd.pht(rt))\mathrm{nil})\\ \mathrm{take}\equiv & \lambda n.n(\lambda rl.l(\lambda htd.\mathrm{cons}h(rt))\mathrm{nil})(\lambda l.\mathrm{nil})\\ \mathrm{t}\mathrm{a}\mathrm{k}\mathrm{e}\text{-}\mathrm{l}\mathrm{a}\mathrm{s}\mathrm{t}\equiv & \lambda nl.Y(\lambda rlm.l(\lambda htd.m(\lambda esz.rts)l)\mathrm{nil})l(\mathrm{drop}nl)\end{array}}$

${\displaystyle \begin{array}{cc}\mathrm{e}\mathrm{l}\mathrm{e}\mathrm{m}\mathrm{e}\mathrm{n}\mathrm{t}\text{-}\mathrm{a}\mathrm{t}& \equiv \lambda nl.\mathrm{drop}nl(\lambda htd.\mathrm{val}h)\mathrm{none}\\ \mathrm{i}\mathrm{n}\mathrm{s}\mathrm{e}\mathrm{r}\mathrm{t}\text{-}\mathrm{a}\mathrm{t}& \equiv \lambda nv.n(\lambda rl.l(\lambda htd.\mathrm{cons}h(rt))(\mathrm{cons}v\mathrm{nil}))(\mathrm{cons}v)\\ \mathrm{r}\mathrm{e}\mathrm{m}\mathrm{o}\mathrm{v}\mathrm{e}\text{-}\mathrm{a}\mathrm{t}& \equiv \lambda n.n(\lambda rl.l(\lambda htd.\mathrm{cons}h(rt))\mathrm{nil})\mathrm{tail}\\ \mathrm{r}\mathrm{e}\mathrm{p}\mathrm{l}\mathrm{a}\mathrm{c}\mathrm{e}\text{-}\mathrm{a}\mathrm{t}& \equiv \lambda nv.n(\lambda rl.l(\lambda htd.\mathrm{cons}h(rt))\mathrm{nil})\\ & (\lambda l.l(\lambda htd.\mathrm{cons}vt)\mathrm{nil})\\ \mathrm{l}\mathrm{a}\mathrm{s}\mathrm{t}\text{-}\mathrm{i}\mathrm{n}\mathrm{d}\mathrm{e}\mathrm{x}\text{-}\mathrm{o}\mathrm{f}& \equiv \lambda p.\mathrm{Y}(\lambda rnl.l(\lambda htd.(\lambda i.i(ph(\mathrm{val}n)i)(\lambda n.i))\\ & (r(\mathrm{succ}n)t))\mathrm{none})\mathrm{zero}\end{array}}$

For some of the definitions the general fold-based ones (found below) are efficient enough.

It is important for the successor function on Church numerals to be defined in the lazy fashion, succ := λnfx.f(nfx), as opposed to succ := λnfx.nf(fx), so that the function length produces lazy numerals, for overall most lazy operation of reductions under the topmost leftmost reduction strategy. In other words, we don't need to know the final length value if all we need to know is whether it is non-zero or not.

Scott lists

Scott encoding for data types follows their surface syntax without regard to recursion in the data type. In the disjunction of conjunctions a.k.a. sum of products style of algebraic data type definitions, it represents a given datum as a function which expects as many arguments as there are alternatives in its data type definition, where each such argument is expected to be a "handler" function that must be able to handle the given number of data arguments that will correspond to the data fields for that alternative.

Given all the handlers as arguments, the datum representation function will then call the appropriate handler with the corresponding internal data. Scott encoded values can thus be said to embody the pattern matching case handling for their data type.

For lists, it means the data type definition of

${\displaystyle List:=\mathrm{NIL}|\mathrm{Cons}⟨val⟩List}$

and lists being represented as

${\displaystyle \begin{array}{cc}\mathrm{nil}=& \lambda nc.n\\ \mathrm{cons}=& \lambda ad.\lambda nc.cad\\ \mathrm{isnil}=& \lambda l.l\mathrm{true}(\lambda ad.\mathrm{false})\\ \mathrm{head}=& \lambda l.l\mathrm{nil}(\lambda ad.a)\\ \mathrm{tail}=& \lambda l.l\mathrm{nil}(\lambda ad.d)\\ \mathrm{foldr}=& \lambda gz.\mathrm{Y}\lambda rl.lz(\lambda ad.ga(rd))\\ =& \lambda gz.\mathrm{U}\lambda sl.lz(\lambda ad.ga(ssd))\\ =& \lambda gz.(\lambda h.\mathrm{U}\lambda s.h(ss))\lambda rl.lz(\lambda ad.ga(rd))\\ =& \lambda gz.\mathrm{U}(\lambda sh.h(ssh))\lambda rl.lz(\lambda ad.ga(rd))\\ =& \lambda gz.(\lambda sh.ssh)(\lambda sh.h(ssh))\lambda rl.lz(\lambda ad.ga(rd))\\ =& \lambda gz.(\lambda sh.shs)(\lambda hs.h(shs))\lambda rl.lz(\lambda ad.ga(rd))\\ \mathrm{foldr2}=& \lambda gz.\mathrm{Y}\lambda rpq.pz(\lambda ad.\\ & qz(\lambda be.gab(rde)))\\ \mathrm{map2}=& \lambda f.\mathrm{Y}\lambda rpq.p\mathrm{nil}(\lambda ad.\\ & q\mathrm{nil}(\lambda be.\mathrm{cons}(fab)(rde)))\end{array}}$