Church encoding

In mathematics, Church encoding is a way of representing various data types in the lambda 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, by functions that are taking functions as their arguments and are returning functions as their results.

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. It can also be extended to represent other data types in the similar spirit.

This article makes occasional use of the alternative 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}${\displaystyle I\equiv \lambda x.x} and ${\displaystyle K\equiv \lambda xy.x}${\displaystyle K\equiv \lambda xy.x}, as needed.

A straightforward implementation of Church encoding slows some access operations from ${\displaystyle O(1)}${\displaystyle O(1)} to ${\displaystyle O(n)}${\displaystyle O(n)}, where ${\displaystyle n}${\displaystyle n} is the size of the data structure, making Church encoding impractical.^[1] Research has shown that this can be addressed by targeted optimizations, but most functional programming languages instead expand their intermediate representations to contain algebraic data types.^[2] Nonetheless Church encoding is often used in theoretical arguments, as it is a natural representation for partial evaluation and theorem proving.^[1] Operations can be typed using higher-ranked types,^[3] and primitive recursion is easily accessible.^[1] 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 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:

${\displaystyle {\begin{aligned}\operatorname {true} &\equiv \lambda a.\lambda b.a\\\operatorname {false} &\equiv \lambda a.\lambda b.b\end{aligned}}}${\displaystyle {\begin{aligned}\operatorname {true} &\equiv \lambda a.\lambda b.a\\\operatorname {false} &\equiv \lambda a.\lambda b.b\end{aligned}}}

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:

${\displaystyle \operatorname {predicate-} x\ \operatorname {then-clause} \ \operatorname {else-clause} }${\displaystyle \operatorname {predicate-} x\ \operatorname {then-clause} \ \operatorname {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.

${\displaystyle {\begin{aligned}\operatorname {and} &=\lambda p.\lambda q.p\ q\ p\\\operatorname {or} &=\lambda p.\lambda q.p\ p\ q\\\operatorname {not} _{1}&=\lambda p.\lambda a.\lambda b.p\ b\ a\\\operatorname {not} _{2}&=\lambda p.p\ (\lambda a.\lambda b.b)\ (\lambda a.\lambda b.a)=\lambda p.p\operatorname {false} \operatorname {true} \\\operatorname {xor} &=\lambda a.\lambda b.a\ (\operatorname {not} \ b)\ b\\\operatorname {if} &=\lambda p.\lambda a.\lambda b.p\ a\ b\end{aligned}}}${\displaystyle {\begin{aligned}\operatorname {and} &=\lambda p.\lambda q.p\ q\ p\\\operatorname {or} &=\lambda p.\lambda q.p\ p\ q\\\operatorname {not} _{1}&=\lambda p.\lambda a.\lambda b.p\ b\ a\\\operatorname {not} _{2}&=\lambda p.p\ (\lambda a.\lambda b.b)\ (\lambda a.\lambda b.a)=\lambda p.p\operatorname {false} \operatorname {true} \\\operatorname {xor} &=\lambda a.\lambda b.a\ (\operatorname {not} \ b)\ b\\\operatorname {if} &=\lambda p.\lambda a.\lambda b.p\ a\ b\end{aligned}}}

Some examples:

${\displaystyle {\begin{aligned}\operatorname {and} \operatorname {true} \operatorname {false} &=(\lambda p.\lambda q.p\ q\ p)\ \operatorname {true} \ \operatorname {false} =\operatorname {true} \operatorname {false} \operatorname {true} =(\lambda a.\lambda b.a)\operatorname {false} \operatorname {true} =\operatorname {false} \\\operatorname {or} \operatorname {true} \operatorname {false} &=(\lambda p.\lambda q.p\ p\ q)\ (\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)=\operatorname {true} \\\operatorname {not} _{1}\ \operatorname {true} &=(\lambda p.\lambda a.\lambda b.p\ b\ a)(\lambda a.\lambda b.a)=\lambda a.\lambda b.(\lambda a.\lambda b.a)\ b\ a=\lambda a.\lambda b.(\lambda c.b)\ a=\lambda a.\lambda b.b=\operatorname {false} \\\operatorname {not} _{2}\ \operatorname {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=\operatorname {false} \end{aligned}}}${\displaystyle {\begin{aligned}\operatorname {and} \operatorname {true} \operatorname {false} &=(\lambda p.\lambda q.p\ q\ p)\ \operatorname {true} \ \operatorname {false} =\operatorname {true} \operatorname {false} \operatorname {true} =(\lambda a.\lambda b.a)\operatorname {false} \operatorname {true} =\operatorname {false} \\\operatorname {or} \operatorname {true} \operatorname {false} &=(\lambda p.\lambda q.p\ p\ q)\ (\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)=\operatorname {true} \\\operatorname {not} _{1}\ \operatorname {true} &=(\lambda p.\lambda a.\lambda b.p\ b\ a)(\lambda a.\lambda b.a)=\lambda a.\lambda b.(\lambda a.\lambda b.a)\ b\ a=\lambda a.\lambda b.(\lambda c.b)\ a=\lambda a.\lambda b.b=\operatorname {false} \\\operatorname {not} _{2}\ \operatorname {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=\operatorname {false} \end{aligned}}}

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,

${\displaystyle {\begin{aligned}\operatorname {pair} &\equiv \lambda xy.\lambda z.z\ x\ y\\\operatorname {first} &\equiv \lambda p.p\ (\lambda xy.x)\\\operatorname {second} &\equiv \lambda p.p\ (\lambda xy.y)\end{aligned}}}${\displaystyle {\begin{aligned}\operatorname {pair} &\equiv \lambda xy.\lambda z.z\ x\ y\\\operatorname {first} &\equiv \lambda p.p\ (\lambda xy.x)\\\operatorname {second} &\equiv \lambda p.p\ (\lambda xy.y)\end{aligned}}}

For example,

${\displaystyle {\begin{aligned}&\operatorname {first} \ (\operatorname {pair} \ a\ b)\\=&\ (\lambda p.p\ (\lambda xy.x))\ ((\lambda xyz.z\ x\ y)\ a\ b)\\=&\ (\lambda p.p\ (\lambda xy.x))\ (\lambda z.z\ a\ b)\\=&\ (\lambda z.z\ a\ b)\ (\lambda xy.x)\\=&\ (\lambda xy.x)\ a\ b\\=&\ a\end{aligned}}}${\displaystyle {\begin{aligned}&\operatorname {first} \ (\operatorname {pair} \ a\ b)\\=&\ (\lambda p.p\ (\lambda xy.x))\ ((\lambda xyz.z\ x\ y)\ a\ b)\\=&\ (\lambda p.p\ (\lambda xy.x))\ (\lambda z.z\ a\ b)\\=&\ (\lambda z.z\ a\ b)\ (\lambda xy.x)\\=&\ (\lambda xy.x)\ a\ b\\=&\ a\end{aligned}}}

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}${\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 n:f\mapsto f^{\circ n}}

${\displaystyle f^{\circ n}(x)=(\underbrace {f\circ f\circ \ldots \circ f} _{n{\text{ times}}}),円(x)=\underbrace {f(f(\ldots (f} _{n{\text{ times}}},円(x))\ldots ))}${\displaystyle f^{\circ n}(x)=(\underbrace {f\circ f\circ \ldots \circ f} _{n{\text{ times}}}),円(x)=\underbrace {f(f(\ldots (f} _{n{\text{ times}}},円(x))\ldots ))}

Church encoding is thus a unary encoding of natural numbers,^[4] 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}{r|l|l}{\text{Number}}&{\text{Function definition}}&{\text{Lambda expression}}\\\hline 0&0\ f\ x=x&0=\lambda f.\lambda x.x\1円&1\ f\ x=f\ x&1=\lambda f.\lambda x.f\ x\2円&2\ f\ x=f\ (f\ x)&2=\lambda f.\lambda x.f\ (f\ x)\3円&3\ f\ x=f\ (f\ (f\ x))&3=\lambda f.\lambda x.f\ (f\ (f\ x))\\\vdots &\vdots &\vdots \\n&n\ f\ x=f^{\circ n}\ x&n=\lambda f.\lambda x.f^{\circ n}\ x\end{array}}}${\displaystyle {\begin{array}{r|l|l}{\text{Number}}&{\text{Function definition}}&{\text{Lambda expression}}\\\hline 0&0\ f\ x=x&0=\lambda f.\lambda x.x\1円&1\ f\ x=f\ x&1=\lambda f.\lambda x.f\ x\2円&2\ f\ x=f\ (f\ x)&2=\lambda f.\lambda x.f\ (f\ x)\3円&3\ f\ x=f\ (f\ (f\ x))&3=\lambda f.\lambda x.f\ (f\ (f\ x))\\\vdots &\vdots &\vdots \\n&n\ f\ x=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".

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 \operatorname {plus} (m,n)=m+n}${\displaystyle \operatorname {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 f^{\circ (m+n)}(x)=(f^{\circ m}\circ f^{\circ n})(x)=f^{\circ m}(f^{\circ n}(x))}:

${\displaystyle \operatorname {plus} \equiv \lambda mn.\lambda fx.m\ f\ (n\ f\ x)}${\displaystyle \operatorname {plus} \equiv \lambda mn.\lambda fx.m\ f\ (n\ f\ x)}

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

${\displaystyle \operatorname {succ} \equiv \lambda n.\lambda fx.f\ (n\ f\ x)}${\displaystyle \operatorname {succ} \equiv \lambda n.\lambda fx.f\ (n\ f\ x)}

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

${\displaystyle \operatorname {mult} \equiv \lambda mn.\lambda fx.m\ (n\ f)\ x}${\displaystyle \operatorname {mult} \equiv \lambda mn.\lambda fx.m\ (n\ f)\ x}

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

${\displaystyle \operatorname {exp} \equiv \lambda bn.n\ b\equiv \lambda bnfx.n\ b\ f\ x}${\displaystyle \operatorname {exp} \equiv \lambda bn.n\ b\equiv \lambda bnfx.n\ b\ f\ x}

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

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

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

${\displaystyle {\begin{aligned}\operatorname {half} &\equiv \lambda nfx.n\ (\lambda rab.a\ (r\ b\ a))\ (\lambda ab.x)\ I\ f\\\operatorname {fact} &\equiv \lambda nf.n\ (\lambda ra.a\ (r\ (\operatorname {succ} a)))\ (\lambda a.f)\ 1\end{aligned}}}${\displaystyle {\begin{aligned}\operatorname {half} &\equiv \lambda nfx.n\ (\lambda rab.a\ (r\ b\ a))\ (\lambda ab.x)\ I\ f\\\operatorname {fact} &\equiv \lambda nf.n\ (\lambda ra.a\ (r\ (\operatorname {succ} a)))\ (\lambda a.f)\ 1\end{aligned}}}

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

Subtraction, ${\displaystyle minus(m,n)=m-n}${\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{aligned}\operatorname {minus} &\equiv \lambda mn.n\operatorname {pred} \ m\\\operatorname {plus} &\equiv \lambda mn.n\operatorname {succ} \ m\\\operatorname {mult} &\equiv \lambda mn.n\ (m\operatorname {plus} )\ 0\\\operatorname {exp} &\equiv \lambda mn.n\ (m\operatorname {mult} )\ 1\\\operatorname {tet} &\equiv \lambda n.n\ (\lambda ra.r\ a\ a)\ 0\end{aligned}}}${\displaystyle {\begin{aligned}\operatorname {minus} &\equiv \lambda mn.n\operatorname {pred} \ m\\\operatorname {plus} &\equiv \lambda mn.n\operatorname {succ} \ m\\\operatorname {mult} &\equiv \lambda mn.n\ (m\operatorname {plus} )\ 0\\\operatorname {exp} &\equiv \lambda mn.n\ (m\operatorname {mult} )\ 1\\\operatorname {tet} &\equiv \lambda n.n\ (\lambda ra.r\ a\ a)\ 0\end{aligned}}}

${\displaystyle \operatorname {tet} n}${\displaystyle \operatorname {tet} n} is the nth tetration operation, ${\displaystyle \operatorname {tet} \ 3\ a=0\ a\ a\ a\ a=a\ a\ a}${\displaystyle \operatorname {tet} \ 3\ a=0\ a\ a\ a\ a=a\ a\ a}, expressing ${\displaystyle a^{(a^{a})}}${\displaystyle 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:

${\displaystyle {\begin{aligned}\operatorname {minus} \equiv \lambda &mnfx.\\&m\ (\lambda rq.q\ r)\ (\lambda q.x)\\&(n\ (\lambda qr.r\ q)\ (\operatorname {Y} \ (\lambda qr.f\ (r\ q))))\end{aligned}}}${\displaystyle {\begin{aligned}\operatorname {minus} \equiv \lambda &mnfx.\\&m\ (\lambda rq.q\ r)\ (\lambda q.x)\\&(n\ (\lambda qr.r\ q)\ (\operatorname {Y} \ (\lambda qr.f\ (r\ q))))\end{aligned}}}

For example, ${\displaystyle \operatorname {minus} \ 6\ 3\ f\ x}${\displaystyle \operatorname {minus} \ 6\ 3\ f\ x} reduces to an equivalent of ${\displaystyle f\ (2\ f\ x)}${\displaystyle f\ (2\ f\ x)}.

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

${\displaystyle {\begin{aligned}\operatorname {pred'} \equiv \lambda mfx.m\ &(\lambda rq.q\ r)\ (\lambda q.x)\\&(\lambda r.r\ (\operatorname {Y} \ (\lambda qr.f\ (r\ q))))\end{aligned}}}${\displaystyle {\begin{aligned}\operatorname {pred'} \equiv \lambda mfx.m\ &(\lambda rq.q\ r)\ (\lambda q.x)\\&(\lambda r.r\ (\operatorname {Y} \ (\lambda qr.f\ (r\ q))))\end{aligned}}}

Direct definition of division is given quite similarly as

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

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

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

Notes:

The predecessor function is given as

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

This encoding essentially uses the identity

${\displaystyle first(\ (\langle i,j\rangle \mapsto \langle j,f\circ j\rangle )^{\circ n}\langle I,I\rangle \ )={\begin{cases}I&{\mbox{if }}n=0,\\f^{\circ (n-1)}&{\mbox{otherwise}}\end{cases}}}${\displaystyle first(\ (\langle i,j\rangle \mapsto \langle j,f\circ j\rangle )^{\circ n}\langle I,I\rangle \ )={\begin{cases}I&{\mbox{if }}n=0,\\f^{\circ (n-1)}&{\mbox{otherwise}}\end{cases}}}

or

${\displaystyle first(\ (\langle x,y\rangle \mapsto \langle y,f(y)\rangle )^{\circ n}\langle x,x\rangle \ )={\begin{cases}x&{\mbox{if }}n=0,\\f^{\circ (n-1)}(x)&{\mbox{otherwise}}\end{cases}}}${\displaystyle first(\ (\langle x,y\rangle \mapsto \langle y,f(y)\rangle )^{\circ n}\langle x,x\rangle \ )={\begin{cases}x&{\mbox{if }}n=0,\\f^{\circ (n-1)}(x)&{\mbox{otherwise}}\end{cases}}}

The idea here is as follows. The only thing known to the Church numeral ${\displaystyle \operatorname {pred} n}${\displaystyle \operatorname {pred} n} is the numeral ${\displaystyle n}${\displaystyle n} itself. Given two arguments ${\displaystyle f}${\displaystyle f} and ${\displaystyle x}${\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}${\displaystyle f} in the chain replaced by the identity function:

${\displaystyle {\begin{aligned}f^{\circ (n-1)}(x)&=\underbrace {I\ (\underbrace {f(f(\ldots (f} _{{n-1}{\text{ times}}}} _{n{\text{ times}}},円(x))\ldots )))=(Xf)^{\circ n}(Z,円x)\ A\\&=\underbrace {Xf\ (Xf\ (\ldots (Xf} _{{n}{\text{ times}}},円(Z,円x))\ldots ))\ A\\&=X\ f\ r_{1}\ A_{1},円,円,円\{-\ and\ it\ must\ be\ equal\ to:\ -\}\\&=I\ (X\ f\ r_{2}\ A_{2})\\&=I\ (f\ (X\ f\ r_{3}\ A_{3}))\\&=I\ (f\ (f\ (X\ f\ r_{4}\ A_{4})))\\&\ldots \\&=I\ (f\ (f\ \ldots (X\ f\ r_{n}\ A_{n})\ldots ))\\&=\underbrace {I\ (f\ (f\ \ldots (f} _{n{\text{ times}}}\ (Z\ x\ A_{n+1}))\ldots ))\\\end{aligned}}}${\displaystyle {\begin{aligned}f^{\circ (n-1)}(x)&=\underbrace {I\ (\underbrace {f(f(\ldots (f} _{{n-1}{\text{ times}}}} _{n{\text{ times}}},円(x))\ldots )))=(Xf)^{\circ n}(Z,円x)\ A\\&=\underbrace {Xf\ (Xf\ (\ldots (Xf} _{{n}{\text{ times}}},円(Z,円x))\ldots ))\ A\\&=X\ f\ r_{1}\ A_{1},円,円,円\{-\ and\ it\ must\ be\ equal\ to:\ -\}\\&=I\ (X\ f\ r_{2}\ A_{2})\\&=I\ (f\ (X\ f\ r_{3}\ A_{3}))\\&=I\ (f\ (f\ (X\ f\ r_{4}\ A_{4})))\\&\ldots \\&=I\ (f\ (f\ \ldots (X\ f\ r_{n}\ A_{n})\ldots ))\\&=\underbrace {I\ (f\ (f\ \ldots (f} _{n{\text{ times}}}\ (Z\ x\ A_{n+1}))\ldots ))\\\end{aligned}}}

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

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

${\displaystyle {\begin{aligned}A_{1},円,円,円,円,円,円,円,円,円,円&=,円I\\A_{,円i>1},円,円,円,円,円&=,円f\\Z\ x\ f,円,円,円,円&=x=K\ x\ f\\X\ f\ r\ A_{i}&=A_{i}\ (r\ A_{i+1}),円,円,円,円,円,円\{-\ i.e.,\ -\}\\X\ f\ r\ i,円,円,円,円,円&=i\ (r\ f)\end{aligned}}}${\displaystyle {\begin{aligned}A_{1},円,円,円,円,円,円,円,円,円,円&=,円I\\A_{,円i>1},円,円,円,円,円&=,円f\\Z\ x\ f,円,円,円,円&=x=K\ x\ f\\X\ f\ r\ A_{i}&=A_{i}\ (r\ A_{i+1}),円,円,円,円,円,円\{-\ i.e.,\ -\}\\X\ f\ r\ i,円,円,円,円,円&=i\ (r\ f)\end{aligned}}}

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

Now it is easy enough to see that

${\displaystyle {\begin{aligned}\operatorname {pred} \ (\operatorname {succ} \ n)\ f\ x&=\operatorname {succ} \ n\ (Xf)\ (K\ x)\ I\\&=X\ f\ (n\ (X\ f)\ (K\ x))\ I\\&=I\ (n\ (Xf)\ (K\ x)\ ,円,円f,円,円,円)\\&=\ \ldots \\&=I\ (f\ (f\ \ldots (f\ (K\ x,円,円f,円,円))\ldots ))\\&=I\ (n\ f\ x)\\&=n\ f\ x\ \end{aligned}}}${\displaystyle {\begin{aligned}\operatorname {pred} \ (\operatorname {succ} \ n)\ f\ x&=\operatorname {succ} \ n\ (Xf)\ (K\ x)\ I\\&=X\ f\ (n\ (X\ f)\ (K\ x))\ I\\&=I\ (n\ (Xf)\ (K\ x)\ ,円,円f,円,円,円)\\&=\ \ldots \\&=I\ (f\ (f\ \ldots (f\ (K\ x,円,円f,円,円))\ldots ))\\&=I\ (n\ f\ x)\\&=n\ f\ x\ \end{aligned}}}

${\displaystyle {\begin{aligned}\operatorname {pred} \ 0\ f\ x&=\ 0\ (Xf)\ (K\ x)\ I\\&=\ K\ x\ I\\&=\ x\\&=\ 0\ f\ x\end{aligned}}}${\displaystyle {\begin{aligned}\operatorname {pred} \ 0\ f\ x&=\ 0\ (Xf)\ (K\ x)\ I\\&=\ K\ x\ I\\&=\ x\\&=\ 0\ f\ x\end{aligned}}}

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

${\displaystyle {\begin{aligned}&\operatorname {pred} \ (\operatorname {succ} \ n)&&=\ n\\&\operatorname {pred} \ 0&&=\ 0\\&\operatorname {pred} \ (\operatorname {pred} \ 0)&&=\ \operatorname {pred} \ 0\ =\ 0\\&\ldots \end{aligned}}}${\displaystyle {\begin{aligned}&\operatorname {pred} \ (\operatorname {succ} \ n)&&=\ n\\&\operatorname {pred} \ 0&&=\ 0\\&\operatorname {pred} \ (\operatorname {pred} \ 0)&&=\ \operatorname {pred} \ 0\ =\ 0\\&\ldots \end{aligned}}}

and so on.

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

${\displaystyle {\begin{aligned}\operatorname {f} =&\ \lambda p.\ \operatorname {pair} \ (\operatorname {second} \ p)\ (\operatorname {succ} \ (\operatorname {second} \ p))\\\operatorname {pred} _{2}=&\ \lambda n.\ \operatorname {first} \ (n\ \operatorname {f} \ (\operatorname {pair} \ 0\ 0))\\\end{aligned}}}${\displaystyle {\begin{aligned}\operatorname {f} =&\ \lambda p.\ \operatorname {pair} \ (\operatorname {second} \ p)\ (\operatorname {succ} \ (\operatorname {second} \ p))\\\operatorname {pred} _{2}=&\ \lambda n.\ \operatorname {first} \ (n\ \operatorname {f} \ (\operatorname {pair} \ 0\ 0))\\\end{aligned}}}

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

${\displaystyle {\begin{aligned}\operatorname {pred} _{2}3=&\ \operatorname {first} \ (\operatorname {f} \ (\operatorname {f} \ (\operatorname {f} \ (\operatorname {pair} \ 0\ 0))))\\=&\ \operatorname {first} \ (\operatorname {f} \ (\operatorname {f} \ (\operatorname {pair} \ 0\ 1)))\\=&\ \operatorname {first} \ (\operatorname {f} \ (\operatorname {pair} \ 1\ 2))\\=&\ \operatorname {first} \ (\operatorname {pair} \ 2\ 3)\\=&\ 2\end{aligned}}}${\displaystyle {\begin{aligned}\operatorname {pred} _{2}3=&\ \operatorname {first} \ (\operatorname {f} \ (\operatorname {f} \ (\operatorname {f} \ (\operatorname {pair} \ 0\ 0))))\\=&\ \operatorname {first} \ (\operatorname {f} \ (\operatorname {f} \ (\operatorname {pair} \ 0\ 1)))\\=&\ \operatorname {first} \ (\operatorname {f} \ (\operatorname {pair} \ 1\ 2))\\=&\ \operatorname {first} \ (\operatorname {pair} \ 2\ 3)\\=&\ 2\end{aligned}}}

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

${\displaystyle {\begin{aligned}\operatorname {pred} _{2}\equiv \lambda n.n\ &(\lambda p.p\ (\lambda abh.h\ b\ (\operatorname {succ} \ b))),円,円(\lambda h.h\ 0\ 0),円,円(\lambda ab.a)\end{aligned}}}${\displaystyle {\begin{aligned}\operatorname {pred} _{2}\equiv \lambda n.n\ &(\lambda p.p\ (\lambda abh.h\ b\ (\operatorname {succ} \ b))),円,円(\lambda h.h\ 0\ 0),円,円(\lambda ab.a)\end{aligned}}}

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 \operatorname {pred} }${\displaystyle \operatorname {pred} } definition. Another encoding follows the second variant of the predecessor identity directly,

${\displaystyle {\begin{aligned}\operatorname {pred} _{3}\equiv \lambda nfx.n\ &(\lambda p.p\ (\lambda abh.h\ b\ (f\ b))),円,円(\lambda h.h\ x\ x),円,円(\lambda ab.a)\end{aligned}}}${\displaystyle {\begin{aligned}\operatorname {pred} _{3}\equiv \lambda nfx.n\ &(\lambda p.p\ (\lambda abh.h\ b\ (f\ b))),円,円(\lambda h.h\ x\ x),円,円(\lambda ab.a)\end{aligned}}}

This way it is already quite close to the original, "outside-in" ${\displaystyle \operatorname {pred} }${\displaystyle \operatorname {pred} } definition, also creating the chain of ${\displaystyle f}${\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 \operatorname {pred} _{2}}${\displaystyle \operatorname {pred} _{2}} definition here. Indeed if we trace its execution we arrive at the new, even more streamlined, yet fully equivalent, definition

${\displaystyle {\begin{aligned}\operatorname {pred} _{4}\equiv \lambda nfx.n\ &(\lambda rab.r\ b\ (f\ b)),円K\ x\ x\end{aligned}}}${\displaystyle {\begin{aligned}\operatorname {pred} _{4}\equiv \lambda nfx.n\ &(\lambda rab.r\ b\ (f\ b)),円K\ x\ x\end{aligned}}}

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

${\displaystyle {\begin{aligned}\operatorname {pred} _{4}3\ f\ x&=\ (..(..(..K)))\ x\ ,円x\\&=\ (..(..K)),円,円,円,円,円,円,円x\ ,円,円(f\ x)\\&=\ (..K),円,円,円,円,円,円(f\ x)\ ,円,円(f\ (f\ x))\\&=\ K,円,円,円,円(f\ (f\ x))\ ,円,円(f\ (f\ (f\ x)))\\&=\ f\ (f\ x)\\\end{aligned}}}${\displaystyle {\begin{aligned}\operatorname {pred} _{4}3\ f\ x&=\ (..(..(..K)))\ x\ ,円x\\&=\ (..(..K)),円,円,円,円,円,円,円x\ ,円,円(f\ x)\\&=\ (..K),円,円,円,円,円,円(f\ x)\ ,円,円(f\ (f\ x))\\&=\ K,円,円,円,円(f\ (f\ x))\ ,円,円(f\ (f\ (f\ x)))\\&=\ f\ (f\ x)\\\end{aligned}}}

clearly showing what is going on. Still, the original ${\displaystyle \operatorname {pred} }${\displaystyle \operatorname {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}${\displaystyle f} is short-circuiting. The top-down approach is also used with other definitions like

${\displaystyle {\begin{aligned}\operatorname {pred} _{5}\equiv \lambda nfx.n\ &(\lambda rab.a\ (r\ b\ b)),円(\lambda ab.x)\ I\ f\\\operatorname {third} \equiv \lambda nfx.n\ &(\lambda rabc.a\ (r\ b\ c\ a)),円(\lambda abc.x)\ I\ I\ f\\\operatorname {thirdRounded} \equiv \lambda nfx.n\ &(\lambda rabc.a\ (r\ b\ c\ a)),円(\lambda abc.x)\ I\ f\ I\\\operatorname {twoThirds} \equiv \lambda nfx.n\ &(\lambda rabc.a\ (r\ b\ c\ a)),円(\lambda abc.x)\ I\ f\ f\\\operatorname {factorial} \equiv \lambda nfx.n\ &(\lambda ra.a\ (r\ (\operatorname {succ} a))),円(\lambda a.f)\ 1\ x\\\end{aligned}}}${\displaystyle {\begin{aligned}\operatorname {pred} _{5}\equiv \lambda nfx.n\ &(\lambda rab.a\ (r\ b\ b)),円(\lambda ab.x)\ I\ f\\\operatorname {third} \equiv \lambda nfx.n\ &(\lambda rabc.a\ (r\ b\ c\ a)),円(\lambda abc.x)\ I\ I\ f\\\operatorname {thirdRounded} \equiv \lambda nfx.n\ &(\lambda rabc.a\ (r\ b\ c\ a)),円(\lambda abc.x)\ I\ f\ I\\\operatorname {twoThirds} \equiv \lambda nfx.n\ &(\lambda rabc.a\ (r\ b\ c\ a)),円(\lambda abc.x)\ I\ f\ f\\\operatorname {factorial} \equiv \lambda nfx.n\ &(\lambda ra.a\ (r\ (\operatorname {succ} a))),円(\lambda a.f)\ 1\ x\\\end{aligned}}}

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

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

Calculating ${\displaystyle n-m}${\displaystyle n-m} with ${\displaystyle \lambda nm.m,円\operatorname {pred} ,円n}${\displaystyle \lambda nm.m,円\operatorname {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 \operatorname {IsZero} \ (\operatorname {minus} \ n\ m)}${\displaystyle \operatorname {IsZero} \ (\operatorname {minus} \ n\ m)}

But this condition is equivalent to ${\displaystyle n\leq m}${\displaystyle n\leq m}, not ${\displaystyle n<m}${\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 \operatorname {divide1} \ n\ m\ f\ x=(\lambda d.\operatorname {IsZero} \ d\ (0\ f\ x)\ (f\ (\operatorname {divide1} \ d\ m\ f\ x)))\ (\operatorname {minus} \ n\ m)}${\displaystyle \operatorname {divide1} \ n\ m\ f\ x=(\lambda d.\operatorname {IsZero} \ d\ (0\ f\ x)\ (f\ (\operatorname {divide1} \ d\ m\ f\ x)))\ (\operatorname {minus} \ n\ m)}

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

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

${\displaystyle \operatorname {divide} \ n=\operatorname {divide1} \ (\operatorname {succ} \ n)}${\displaystyle \operatorname {divide} \ n=\operatorname {divide1} \ (\operatorname {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 \operatorname {divide1} \rightarrow \operatorname {div} \ c}${\displaystyle \operatorname {divide1} \rightarrow \operatorname {div} \ c}
• In the right hand side ${\displaystyle \operatorname {divide1} \rightarrow c}${\displaystyle \operatorname {divide1} \rightarrow c}

to get,

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

Then,

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

where,

${\displaystyle {\begin{aligned}\operatorname {divide1} &=Y\ \operatorname {div} \\\operatorname {succ} &=\lambda n.\lambda f.\lambda x.f\ (n\ f\ x)\\Y&=\lambda f.(\lambda x.f\ (x\ x))\ (\lambda x.f\ (x\ x))\0円&=\lambda f.\lambda x.x\\\operatorname {IsZero} &=\lambda n.n\ (\lambda x.\operatorname {false} )\ \operatorname {true} \end{aligned}}}${\displaystyle {\begin{aligned}\operatorname {divide1} &=Y\ \operatorname {div} \\\operatorname {succ} &=\lambda n.\lambda f.\lambda x.f\ (n\ f\ x)\\Y&=\lambda f.(\lambda x.f\ (x\ x))\ (\lambda x.f\ (x\ x))\0円&=\lambda f.\lambda x.x\\\operatorname {IsZero} &=\lambda n.n\ (\lambda x.\operatorname {false} )\ \operatorname {true} \end{aligned}}}

${\displaystyle {\begin{aligned}\operatorname {true} &\equiv \lambda a.\lambda b.a\\\operatorname {false} &\equiv \lambda a.\lambda b.b\end{aligned}}}${\displaystyle {\begin{aligned}\operatorname {true} &\equiv \lambda a.\lambda b.a\\\operatorname {false} &\equiv \lambda a.\lambda b.b\end{aligned}}}

${\displaystyle {\begin{aligned}\operatorname {minus} &=\lambda m.\lambda n.n\operatorname {pred} m\\\operatorname {pred} &=\lambda n.\lambda f.\lambda x.n\ (\lambda g.\lambda h.h\ (g\ f))\ (\lambda u.x)\ (\lambda u.u)\end{aligned}}}${\displaystyle {\begin{aligned}\operatorname {minus} &=\lambda m.\lambda n.n\operatorname {pred} m\\\operatorname {pred} &=\lambda n.\lambda f.\lambda x.n\ (\lambda g.\lambda h.h\ (g\ f))\ (\lambda u.x)\ (\lambda u.u)\end{aligned}}}

Gives,

${\displaystyle \scriptstyle \operatorname {divide} =\lambda n.((\lambda f.(\lambda x.x\ x)\ (\lambda x.f\ (x\ x)))\ (\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)\ f\ x)\ (f\ (c\ d\ m\ f\ x)))\ ((\lambda m.\lambda n.n(\lambda n.\lambda f.\lambda x.n\ (\lambda g.\lambda h.h\ (g\ f))\ (\lambda u.x)\ (\lambda u.u))m)\ n\ m)))\ ((\lambda n.\lambda f.\lambda x.f\ (n\ f\ x))\ n)}${\displaystyle \scriptstyle \operatorname {divide} =\lambda n.((\lambda f.(\lambda x.x\ x)\ (\lambda x.f\ (x\ x)))\ (\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)\ f\ x)\ (f\ (c\ d\ m\ f\ x)))\ ((\lambda m.\lambda n.n(\lambda n.\lambda f.\lambda x.n\ (\lambda g.\lambda h.h\ (g\ f))\ (\lambda u.x)\ (\lambda u.u))m)\ n\ m)))\ ((\lambda n.\lambda f.\lambda x.f\ (n\ f\ x))\ 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)))

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.^[6] The integer value is the difference between the two Church numerals.

A natural number is converted to a signed number by,

${\displaystyle \operatorname {convert} _{s}=\lambda x.\operatorname {pair} \ x\ 0}${\displaystyle \operatorname {convert} _{s}=\lambda x.\operatorname {pair} \ x\ 0}

Negation is performed by swapping the values.

${\displaystyle \operatorname {neg} _{s}=\lambda x.\operatorname {pair} \ (\operatorname {second} \ x)\ (\operatorname {first} \ x)}${\displaystyle \operatorname {neg} _{s}=\lambda x.\operatorname {pair} \ (\operatorname {second} \ x)\ (\operatorname {first} \ x)}

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

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

The recursion may be implemented using the Y combinator,

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

${\displaystyle \operatorname {OneZero} =Y\operatorname {OneZ} }${\displaystyle \operatorname {OneZero} =Y\operatorname {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}]}${\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 \operatorname {plus} _{s}=\lambda x.\lambda y.\operatorname {OneZero} \ (\operatorname {pair} \ (\operatorname {plus} \ (\operatorname {first} \ x)\ (\operatorname {first} \ y))\ (\operatorname {plus} \ (\operatorname {second} \ x)\ (\operatorname {second} \ y)))}${\displaystyle \operatorname {plus} _{s}=\lambda x.\lambda y.\operatorname {OneZero} \ (\operatorname {pair} \ (\operatorname {plus} \ (\operatorname {first} \ x)\ (\operatorname {first} \ y))\ (\operatorname {plus} \ (\operatorname {second} \ x)\ (\operatorname {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}]}${\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 \operatorname {minus} _{s}=\lambda x.\lambda y.\operatorname {OneZero} \ (\operatorname {pair} \ (\operatorname {plus} \ (\operatorname {first} \ x)\ (\operatorname {second} \ y))\ (\operatorname {plus} \ (\operatorname {second} \ x)\ (\operatorname {first} \ y)))}${\displaystyle \operatorname {minus} _{s}=\lambda x.\lambda y.\operatorname {OneZero} \ (\operatorname {pair} \ (\operatorname {plus} \ (\operatorname {first} \ x)\ (\operatorname {second} \ y))\ (\operatorname {plus} \ (\operatorname {second} \ x)\ (\operatorname {first} \ y)))}

Multiplication may be defined 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_{n}+x_{n}*y_{p})=[x_{p}*y_{p}+x_{n}*y_{n},x_{p}*y_{n}+x_{n}*y_{p}]}${\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_{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,

${\displaystyle \operatorname {mult} _{s}=\lambda x.\lambda y.\operatorname {pair} \ (\operatorname {plus} \ (\operatorname {mult} \ (\operatorname {first} \ x)\ (\operatorname {first} \ y))\ (\operatorname {mult} \ (\operatorname {second} \ x)\ (\operatorname {second} \ y)))\ (\operatorname {plus} \ (\operatorname {mult} \ (\operatorname {first} \ x)\ (\operatorname {second} \ y))\ (\operatorname {mult} \ (\operatorname {second} \ x)\ (\operatorname {first} \ y)))}${\displaystyle \operatorname {mult} _{s}=\lambda x.\lambda y.\operatorname {pair} \ (\operatorname {plus} \ (\operatorname {mult} \ (\operatorname {first} \ x)\ (\operatorname {first} \ y))\ (\operatorname {mult} \ (\operatorname {second} \ x)\ (\operatorname {second} \ y)))\ (\operatorname {plus} \ (\operatorname {mult} \ (\operatorname {first} \ x)\ (\operatorname {second} \ y))\ (\operatorname {mult} \ (\operatorname {second} \ x)\ (\operatorname {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 \operatorname {divZ} =\lambda x.\lambda y.\operatorname {IsZero} \ y\ 0\ (\operatorname {divide} \ x\ y)}${\displaystyle \operatorname {divZ} =\lambda x.\lambda y.\operatorname {IsZero} \ y\ 0\ (\operatorname {divide} \ x\ y)}

divZ is then used in the following formula, which is the same as for multiplication, but with mult replaced by divZ.

${\displaystyle \operatorname {divide} _{s}=\lambda x.\lambda y.\operatorname {pair} \ (\operatorname {plus} \ (\operatorname {divZ} \ (\operatorname {first} \ x)\ (\operatorname {first} \ y))\ (\operatorname {divZ} \ (\operatorname {second} \ x)\ (\operatorname {second} \ y)))\ (\operatorname {plus} \ (\operatorname {divZ} \ (\operatorname {first} \ x)\ (\operatorname {second} \ y))\ (\operatorname {divZ} \ (\operatorname {second} \ x)\ (\operatorname {first} \ y)))}${\displaystyle \operatorname {divide} _{s}=\lambda x.\lambda y.\operatorname {pair} \ (\operatorname {plus} \ (\operatorname {divZ} \ (\operatorname {first} \ x)\ (\operatorname {first} \ y))\ (\operatorname {divZ} \ (\operatorname {second} \ x)\ (\operatorname {second} \ y)))\ (\operatorname {plus} \ (\operatorname {divZ} \ (\operatorname {first} \ x)\ (\operatorname {second} \ y))\ (\operatorname {divZ} \ (\operatorname {second} \ x)\ (\operatorname {first} \ y)))}

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.^{[7] [8]} 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.

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.

typeChurcha=(a->a)->a->a
church::Integer->ChurchInteger
church0=\f->\x->x
churchn=\f->\x->f(church(n-1)fx)
unchurch::ChurchInteger->Integer
unchurchcn=cn(+1)0

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

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

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

${\displaystyle \operatorname {LEQ} =\lambda m.\lambda n.\operatorname {IsZero} \ (\operatorname {minus} \ m\ n)}${\displaystyle \operatorname {LEQ} =\lambda m.\lambda n.\operatorname {IsZero} \ (\operatorname {minus} \ m\ n)},

Because of the identity,

${\displaystyle x=y\equiv (x\leq y\land y\leq x)}${\displaystyle x=y\equiv (x\leq y\land y\leq x)}

The test for equality may be implemented as,

${\displaystyle \operatorname {EQ} =\lambda m.\lambda n.\operatorname {and} \ (\operatorname {LEQ} \ m\ n)\ (\operatorname {LEQ} \ n\ m)}${\displaystyle \operatorname {EQ} =\lambda m.\lambda n.\operatorname {and} \ (\operatorname {LEQ} \ m\ n)\ (\operatorname {LEQ} \ n\ m)}

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

We give four different representations of lists below:

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

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:^[9]

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

Alternatively, define^[10]

${\displaystyle {\begin{aligned}\operatorname {cons} &\equiv \operatorname {pair} \\\operatorname {head} &\equiv \operatorname {\{-first-\}} \equiv \lambda l.\ l\ (\lambda htd.\ h)\ \operatorname {nil} \\\operatorname {tail} &\equiv \operatorname {\{-second-\}} \equiv \lambda l.\ l\ (\lambda htd.\ t)\ \operatorname {nil} \\\operatorname {nil} &\equiv \operatorname {false} \\\operatorname {isnil} &\equiv \lambda l.l\ (\lambda htd.\operatorname {false} )\operatorname {true} \\\end{aligned}}}${\displaystyle {\begin{aligned}\operatorname {cons} &\equiv \operatorname {pair} \\\operatorname {head} &\equiv \operatorname {\{-first-\}} \equiv \lambda l.\ l\ (\lambda htd.\ h)\ \operatorname {nil} \\\operatorname {tail} &\equiv \operatorname {\{-second-\}} \equiv \lambda l.\ l\ (\lambda htd.\ t)\ \operatorname {nil} \\\operatorname {nil} &\equiv \operatorname {false} \\\operatorname {isnil} &\equiv \lambda l.l\ (\lambda htd.\operatorname {false} )\operatorname {true} \\\end{aligned}}}

where the definitions like the last one follow the general pattern of the safe use of a list, where ${\displaystyle h}${\displaystyle h} and ${\displaystyle t}${\displaystyle t} refer to the list's head and tail:

${\displaystyle {\begin{aligned}\operatorname {process-list} &\equiv \lambda l.l\ (\lambda htd.\langle \operatorname {head-and-tail-clause} \rangle )\ \langle \operatorname {nil-clause} \rangle \\\end{aligned}}}${\displaystyle {\begin{aligned}\operatorname {process-list} &\equiv \lambda l.l\ (\lambda htd.\langle \operatorname {head-and-tail-clause} \rangle )\ \langle \operatorname {nil-clause} \rangle \\\end{aligned}}}

Other operations for one pair as a list node

${\displaystyle {\begin{aligned}\operatorname {fold} &\equiv \lambda f.\ \operatorname {Y} \ (\lambda r.\lambda al.\ l\ (\lambda htd.\ r\ (f\ a\ h)\ t)\ a)\\\operatorname {rfold} &\equiv \lambda fa.\ \operatorname {Y} \ (\lambda r.\lambda l.\ l\ (\lambda htd.\ f\ (r\ t)\ h)\ a)\\\operatorname {length} &\equiv \operatorname {fold} \ (\lambda ah.\ \operatorname {succ} \ a)\ \operatorname {zero} \end{aligned}}}${\displaystyle {\begin{aligned}\operatorname {fold} &\equiv \lambda f.\ \operatorname {Y} \ (\lambda r.\lambda al.\ l\ (\lambda htd.\ r\ (f\ a\ h)\ t)\ a)\\\operatorname {rfold} &\equiv \lambda fa.\ \operatorname {Y} \ (\lambda r.\lambda l.\ l\ (\lambda htd.\ f\ (r\ t)\ h)\ a)\\\operatorname {length} &\equiv \operatorname {fold} \ (\lambda ah.\ \operatorname {succ} \ a)\ \operatorname {zero} \end{aligned}}}

${\displaystyle {\begin{aligned}\operatorname {map} &\equiv \lambda f.\ \operatorname {rfold} \ (\lambda ah.\ \operatorname {cons} \ (f\ h)\ a)\ \operatorname {nil} \\\operatorname {filter} &\equiv \lambda p.\ \operatorname {rfold} \ (\lambda ah.\ p\ h\ (\operatorname {cons} \ h\ a)\ a)\ \operatorname {nil} \\\operatorname {reverse} &\equiv \operatorname {fold} \ (\lambda ah.\ \operatorname {cons} \ h\ a)\ \operatorname {nil} \\\operatorname {concat} &\equiv \lambda lg.\ \operatorname {rfold} \ (\lambda ah.\ \operatorname {cons} \ h\ a)\ g\ l\\\operatorname {conj} &\equiv \lambda lv.\ \operatorname {concat} \ l\ (\operatorname {cons} \ v\ \operatorname {nil} )\end{aligned}}}${\displaystyle {\begin{aligned}\operatorname {map} &\equiv \lambda f.\ \operatorname {rfold} \ (\lambda ah.\ \operatorname {cons} \ (f\ h)\ a)\ \operatorname {nil} \\\operatorname {filter} &\equiv \lambda p.\ \operatorname {rfold} \ (\lambda ah.\ p\ h\ (\operatorname {cons} \ h\ a)\ a)\ \operatorname {nil} \\\operatorname {reverse} &\equiv \operatorname {fold} \ (\lambda ah.\ \operatorname {cons} \ h\ a)\ \operatorname {nil} \\\operatorname {concat} &\equiv \lambda lg.\ \operatorname {rfold} \ (\lambda ah.\ \operatorname {cons} \ h\ a)\ g\ l\\\operatorname {conj} &\equiv \lambda lv.\ \operatorname {concat} \ l\ (\operatorname {cons} \ v\ \operatorname {nil} )\end{aligned}}}

${\displaystyle {\begin{aligned}\operatorname {drop} &\equiv \lambda n.\ n\ \operatorname {tail} \\&\equiv \operatorname {Y} \ (\lambda r.\lambda nl.\ l\ (\lambda htd.\ \operatorname {IsZero} \ n\ l\ (r\ (\operatorname {pred} \ n)\ t))\ \operatorname {nil} )\\\operatorname {drop-last} &\equiv \lambda nl.\ \operatorname {IsZero} \ n\ l\ \operatorname {second} (\\&\ \ \ \ \ \ \ \ \operatorname {Y} \ (\lambda rl_{r}.\ l_{r}\ (\lambda htd.\\&\ \ \ \ \ \ \ \ \ \ \ \ r\ t\ (\lambda n_{a}l_{a}.\ \operatorname {IsZero} \ n_{a}\\&\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ (\operatorname {pair} \ \operatorname {zero} \ (\operatorname {cons} \ h\ l_{a}))\\&\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ (\operatorname {pair} \ (\operatorname {pred} \ n_{a})\ \operatorname {nil} )\ ))\\&\ \ \ \ \ \ \ \ \ \ \ \ (\operatorname {pair} \ n\ \operatorname {nil} )\ )\\&\ \ \ \ \ \ \ \ \ l\ )\\\operatorname {drop-while} &\equiv \lambda p.\ \operatorname {Y} \ (\lambda rl.\ l\ (\lambda htd.\ p\ h\ (r\ t)\ l)\ \operatorname {nil} )\\\operatorname {take} &\equiv \operatorname {Y} \ (\lambda rnl.\ l\ (\lambda htd.\ \operatorname {IsZero} \ n\ \operatorname {nil} \ (\operatorname {cons} \ h\ (r\ (\operatorname {pred} \ n)\ t)))\ \operatorname {nil} )\\\operatorname {take-last} &\equiv \lambda nl.\ \operatorname {IsZero} \ n\ l\ \operatorname {second} (\\&\ \ \ \ \ \ \ \ \operatorname {Y} \ (\lambda rl_{r}.\ l_{r}\ (\lambda htd.\\&\ \ \ \ \ \ \ \ \ \ \ \ r\ t\ (\lambda n_{a}l_{a}.\ \operatorname {IsZero} \ n_{a}\\&\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ (\operatorname {pair} \ \operatorname {zero} \ l_{a})\\&\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ (\operatorname {pair} \ (\operatorname {pred} \ n_{a})\ l_{r})\ ))\\&\ \ \ \ \ \ \ \ \ \ \ \ (\operatorname {pair} \ n\ \operatorname {nil} )\ )\\&\ \ \ \ \ \ \ \ \ l)\\\operatorname {take-while} &\equiv \lambda p.\ \operatorname {Y} \ (\lambda rl.\ l\ (\lambda htd.\ p\ h\ (\operatorname {cons} \ h\ (r\ t))\ \operatorname {nil} )\ \operatorname {nil} )\end{aligned}}}${\displaystyle {\begin{aligned}\operatorname {drop} &\equiv \lambda n.\ n\ \operatorname {tail} \\&\equiv \operatorname {Y} \ (\lambda r.\lambda nl.\ l\ (\lambda htd.\ \operatorname {IsZero} \ n\ l\ (r\ (\operatorname {pred} \ n)\ t))\ \operatorname {nil} )\\\operatorname {drop-last} &\equiv \lambda nl.\ \operatorname {IsZero} \ n\ l\ \operatorname {second} (\\&\ \ \ \ \ \ \ \ \operatorname {Y} \ (\lambda rl_{r}.\ l_{r}\ (\lambda htd.\\&\ \ \ \ \ \ \ \ \ \ \ \ r\ t\ (\lambda n_{a}l_{a}.\ \operatorname {IsZero} \ n_{a}\\&\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ (\operatorname {pair} \ \operatorname {zero} \ (\operatorname {cons} \ h\ l_{a}))\\&\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ (\operatorname {pair} \ (\operatorname {pred} \ n_{a})\ \operatorname {nil} )\ ))\\&\ \ \ \ \ \ \ \ \ \ \ \ (\operatorname {pair} \ n\ \operatorname {nil} )\ )\\&\ \ \ \ \ \ \ \ \ l\ )\\\operatorname {drop-while} &\equiv \lambda p.\ \operatorname {Y} \ (\lambda rl.\ l\ (\lambda htd.\ p\ h\ (r\ t)\ l)\ \operatorname {nil} )\\\operatorname {take} &\equiv \operatorname {Y} \ (\lambda rnl.\ l\ (\lambda htd.\ \operatorname {IsZero} \ n\ \operatorname {nil} \ (\operatorname {cons} \ h\ (r\ (\operatorname {pred} \ n)\ t)))\ \operatorname {nil} )\\\operatorname {take-last} &\equiv \lambda nl.\ \operatorname {IsZero} \ n\ l\ \operatorname {second} (\\&\ \ \ \ \ \ \ \ \operatorname {Y} \ (\lambda rl_{r}.\ l_{r}\ (\lambda htd.\\&\ \ \ \ \ \ \ \ \ \ \ \ r\ t\ (\lambda n_{a}l_{a}.\ \operatorname {IsZero} \ n_{a}\\&\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ (\operatorname {pair} \ \operatorname {zero} \ l_{a})\\&\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ (\operatorname {pair} \ (\operatorname {pred} \ n_{a})\ l_{r})\ ))\\&\ \ \ \ \ \ \ \ \ \ \ \ (\operatorname {pair} \ n\ \operatorname {nil} )\ )\\&\ \ \ \ \ \ \ \ \ l)\\\operatorname {take-while} &\equiv \lambda p.\ \operatorname {Y} \ (\lambda rl.\ l\ (\lambda htd.\ p\ h\ (\operatorname {cons} \ h\ (r\ t))\ \operatorname {nil} )\ \operatorname {nil} )\end{aligned}}}