Content deleted Content added
David Wahler (talk | contribs) →Church booleans: changed to {{sect-stub}} |
→Defining pred through pairs: c/e examples |
||
| (548 intermediate revisions by more than 100 users not shown) | |||
Line 1:
{{short description|Representation of natural numbers and other data types in lambda calculus}}
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 [[higher-order function|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 [[Lambda calculus#Notation|alternative syntax]] for lambda abstraction terms, where λ''x''.λ''y''.λ''z''.''N'' is abbreviated as λ''xyz''.''N'', as well as the two standard combinators, <math>I \equiv \lambda x. x</math> and <math>K \equiv \lambda x y. x</math>, as needed.
== Use ==
A straightforward implementation of Church encoding slows some access operations from <math>O(1)</math> to <math>O(n)</math>, where <math>n</math> is the size of the [[data structure]], making Church encoding impractical.<ref name=Widemann>{{cite conference <!-- Citation bot no --> |last1=Trancón y Widemann |first1=Baltasar |last2=Parnas |first2=David Lorge |chapter=Tabular Expressions and Total Functional Programming |title=Implementation and Application of Functional Languages |series=Lecture Notes in Computer Science |date=2008 |volume=5083 |pages=228–229 |doi=10.1007/978-3-540-85373-2_13|isbn=978-3-540-85372-5 |url=https://books.google.com/books?id=E1zuY1Q6sOsC&pg=PA228| conference=19th International Workshop, IFL 2007, Freiburg, Germany, September 27–29, 2007 Revised Selected Papers|editor1= Olaf Chitil|editor2= Zoltán Horváth|editor3= Viktória Zsók }}</ref> 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 type]]s.<ref>{{cite book |last1=Jansen |first1=Jan Martin |last2=Koopman |first2=Pieter W. M. |last3=Plasmeijer |first3=Marinus J. |editor1-last=Nilsson |editor1-first=Henrik |title=Trends in functional programming. Volume 7 |date=2006 |publisher=Intellect |___location=Bristol |isbn=978-1-84150-188-8 |chapter=Efficient interpretation by transforming data types and patterns to functions|pages=73–90|citeseerx=10.1.1.73.9841}}</ref> Nonetheless Church encoding is often used in theoretical arguments, as it is a natural representation for partial evaluation and theorem proving.<ref name=Widemann/> Operations can be typed using [[higher-ranked type]]s,<ref>{{cite web |work=Lambda Calculus and Lambda Calculators |url=https://okmij.org/ftp/Computation/lambda-calc.html#predecessor |publisher=okmij.org|title=Predecessor and lists are not representable in simply typed lambda calculus}}</ref> and primitive recursion is easily accessible.<ref name=Widemann/> 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 [[Extensionality|extensionally]] equal due to the [[Lambda calculus#Undecidability of equivalence|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 [[Deductive lambda calculus#Intensional versus extensional equality|intensional equality]]. There are [[Deductive lambda calculus#Intensional versus extensional equality|potential problems]] with the interpretation of results because of the difference between the intensional and extensional definition of equality.
==Church numerals==
:<math>n : f \mapsto f^{\circ n}</math>
: <math>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 ))</math>
Church encoding is thus a [[Unary numeral system|''unary'']] encoding of natural numbers,<ref>{{citation
| last = Jansen | first = Jan Martin
| title = The Beauty of Functional Code
| contribution = Programming in the λ-calculus: from Church to Scott and back
| doi = 10.1007/978-3-642-40355-2_12
| pages = 168–180
| publisher = Springer-Verlag
| series = Lecture Notes in Computer Science
| volume = 8106
| year = 2013| isbn = 978-3-642-40354-5
}}.</ref> 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.'':
:<math>
\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}
</math>
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 definition|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 calculus#lambdaAbstr|lambda abstractions]] which, when applied to Church numerals representing the operands, beta-reduce to the Church numerals representing the results. <!-- note: lambda calculus is not part of any programming language, it is a mathematical formalism in itself
These functions may be defined in [[lambda calculus]], or implemented in most functional programming languages (see [[Lambda lifting#Conversion without lifting|converting lambda expressions to functions]]). -->
Church representation of addition, <math>\operatorname{plus}(m, n)= m+n</math>, uses the identity <math>f^{\circ (m+n)}(x)=(f^{\circ m}\circ f^{\circ n})(x) =f^{\circ m}(f^{\circ n}(x))</math>:
: <math>\operatorname{plus} \equiv \lambda m n.\lambda f x. m\ f\ (n\ f\ x)</math>
The successor operation, <math>\operatorname{succ}(n)=n+1</math>, is obtained by [[Beta reduction#.CE.B2-reduction|β-reducing]] the expression "<math>\operatorname{plus}\ 1</math>":
: <math>\operatorname{succ} \equiv \lambda n.\lambda f x. f\ (n\ f\ x)</math>
Multiplication, <math>\operatorname{mult}(m, n) = m*n</math>, uses the identity <math>f^{\circ (m*n)}(x) = (f^{\circ n})^{\circ m}(x)</math>:
: <math>\operatorname{mult} \equiv \lambda m n.\lambda f x. m\ (n\ f)\ x</math>
Thus <math>b\ (b\ f) \equiv (\operatorname{mult} b\ b)\ f</math> and <math>b\ (b\ (b\ f)) \equiv (\operatorname{mult} b\ (\operatorname{mult} b\ b))\ f</math>, and so by the virtue of Church encoding expressing the ''n''-fold composition, the exponentiation operation <math>\operatorname{exp}(b, n) = b^n</math> is given by
: <math>\operatorname{exp} \equiv \lambda b n. n\ b \equiv \lambda b n f x. n\ b\ f\ x</math>
The predecessor operation <math>\operatorname{pred}(n)</math> is a little bit more involved. We need to devise an operation that when repeated <math>n+1</math> times will result in <math>n</math> applications of the given function <math>f</math>. This is achieved by using the identity function instead, one time only, and then switching back to <math>f</math>:
: <math>\operatorname{pred} \equiv \lambda n f x. n\ (\lambda r i. i\ (r\ f))\ (\lambda f. x)\ I</math>
As previously mentioned, <math>I</math> is the identity function, <math>\lambda x. x</math>. See [[#Predecessor function| below]] for a detailed explanation. This suggests implementing e.g. halving and factorial in the similar fashion,
: <math> \begin{align}
\operatorname{half} &\equiv \lambda n f x. n\ (\lambda r a b. a\ (r\ b\ a))\ (\lambda a b. x)\ I\ f \\
\operatorname{fact} &\equiv \lambda n f. n\ (\lambda r a. a\ (r\ (\operatorname{succ} a)))\ (\lambda a. f)\ 1
\end{align}</math>
For example, <math>\operatorname{pred} 4\ f\ x\,</math> beta-reduces to <math>I (f\ (f\ (f\ x)))</math>, <math>\operatorname{half}\ 5\ f\ x\,</math> beta-reduces to <math>I\ (f\ (I\ (f\ (I\ x))))</math>, and <math>\operatorname{fact} 4\,f\,</math> beta-reduces to <math>1\ (2\ (3\ (4\ f)))</math>.
Subtraction, <math>minus(m,n) = m-n</math>, 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.:
: <math>\begin{align}
\operatorname{minus} & \equiv \lambda m n. n \operatorname{pred}\ m \\
\operatorname{plus} & \equiv \lambda m n. n \operatorname{succ}\ m \\
\operatorname{mult} & \equiv \lambda m n. n\ (m \operatorname{plus})\ 0 \\
\operatorname{exp} & \equiv \lambda m n. n\ (m \operatorname{mult})\ 1 \\
\operatorname{tet} & \equiv \lambda n. n\ (\lambda r a. r\ a\ a)\ 0
\end{align}
</math>
<math>\operatorname{tet} n</math> is the ''n''th [[tetration]] operation, <math>\operatorname{tet}\ 3\ a = 0\ a\ a\ a\ a = a\ a\ a</math>, expressing <math>a^{(a^a)}</math>. <!-- 3W0a=W(W(W0))a=W(W0)aa=W0aaa=0aaaa 0W0a=0a=1 -->
==== Subtraction, directly ====
Just as addition as repeated successor has its counterpart in the direct style, so can subtraction be expressed directly and more efficiently as well:
: <math> \begin{align}
\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{align} </math>
For example, <math>\operatorname{minus}\ 6\ 3\ f\ x</math> reduces to the equivalent of <math>f\ (2\ f\ x)</math>.
=== Table of functions on Church numerals ===
{| class="wikitable"
|-
! Function !! Algebra !! Identity !! Function definition
! colspan="2" | Lambda expressions
|-
| [[Successor function|Successor]] || <math>n + 1</math> || <math>f^{\circ (n+1)} = f \circ f^{\circ n} </math> || <math>\operatorname{succ}\ n\ f\ x = f\ (n\ f\ x) </math> || <math>\lambda n f x.f\ (n\ f\ x) </math> || ...
|-
| [[Addition]] || <math>m + n</math> || <math>f^{\circ (m+n)} = f^{\circ m} \circ f^{\circ n} </math> || <math>\operatorname{plus}\ m\ n\ f\ x = m\ f\ (n\ f\ x) </math> || <math> \lambda m n f x.m\ f\ (n\ f\ x) </math> || <math>\lambda m n.n \operatorname{succ} m</math>
|-
| [[Multiplication]] || <math>m * n </math> || <math> f^{\circ (m*n)} = (f^{\circ m})^{\circ n} </math> ||<math>\operatorname{multiply}\ m\ n\ f\ x = m\ (n\ f) \ x </math> || <math>\lambda m n f x.m\ (n\ f) \ x </math> || <math>\lambda m n f.m\ (n\ f) </math>
|-
| [[Exponentiation]] || <math>b^n </math> || <math>b^{\circ n} = (\operatorname{mult} b)^{\circ n} </math> ||<math>\operatorname{exp} \ b\ n\ f\ x = n\ b\ f\ x </math> || <math> \lambda b n f x.n\ b\ f\ x </math> || <math> \lambda b n.n\ b </math>
|-
| [[Successor function|Predecessor]]{{efn|name=ce}} || <math>n - 1</math> || <math>first((\langle i,j\rangle \mapsto \langle j,f \circ j\rangle)^{\circ n}\langle I,I\rangle) = f^{\circ (n-1)} </math> || <math>\operatorname{pred} (n+1)\ f\ x = I\ (n\ f\ x)</math>
| colspan="2" |
<math>\lambda n f x.n\ (\lambda r i.i\ (r\ f))\ (\lambda f.x)\ (\lambda u.u) </math>
|-
| [[Subtraction]]{{efn|name=ce}} ([[Monus]]) || <math> m - n </math> || <math>m-n = pred^{\circ n}(m)</math> || <math>\operatorname{minus}\ m\ n = n \operatorname{pred} m</math> || ... || <math>\lambda m n.n \operatorname{pred} m</math>
|}
'''Notes''': {{notelist|refs={{efn|name=ce|In the Church encoding,
* <math> \operatorname{pred}(0) = 0 </math>
* <math> m \le n \to m - n = 0 </math>
}}}}
=== Predecessor function ===
The predecessor function is given as
: <math>\operatorname{pred} \equiv \lambda n f x. n\ (\lambda r i. i\ (r\ f))\ (\lambda f. x)\ (\lambda u. u)</math>
This encoding essentially uses the identity
:<math>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}</math>
or
:<math>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}</math>
==== An explanation of pred ====
The idea here is as follows. The only thing known to the Church numeral <math>\operatorname{pred} n</math> is the numeral <math>n</math> itself. Given two arguments <math>f</math> and <math>x</math>, 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) <math>f</math> in the chain replaced by the identity function:
:<math> \begin{align}
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{X f\ (X f\ ( \ldots (X f}_{{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{align}</math>
Here <math>X f</math> is the modified <math>f</math>, and <math>Z\,x</math> is the modified <math>x</math>. Since <math>Xf</math> itself can not be changed, its behavior can only be modified through an additional argument, <math>A</math>.
The goal is achieved, then, by passing that additional argument <math>A</math> along ''from the outside in'', while modifying it as necessary, with the definitions
:<math> \begin{align}
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{align}</math>
Which is exactly what we have in the <math>\operatorname{pred}</math> definition's lambda expression.
Now it is easy enough to see that
: <math>\begin{align}
\operatorname{pred}\ (\operatorname{succ}\ n)\ f\ x &= \operatorname{succ}\ n\ (X f)\ (K\ x)\ I \\
&= X\ f\ (n\ (X\ f)\ (K\ x))\ I \\
&= I\ (n\ (X f)\ (K\ x)\ \,\, f\,\,\, ) \\
&=\ \ldots \\
&= I\ (f\ (f\ \ldots (f\ (K\ x \,\, f\,\, )) \ldots)) \\
&= I\ (n\ f\ x) \\
&= n\ f\ x\ \end{align}</math>
: <math>\begin{align}
\operatorname{pred}\ 0\ f\ x &=\ 0\ (X f)\ (K\ x)\ I \\
&=\ K\ x\ I \\
&=\ x \\
&=\ 0\ f\ x
\end{align}</math>
i.e. by eta-contraction and then by induction, it holds that
: <math>\begin{align}
&\operatorname{pred}\ (\operatorname{succ}\ n) &&=\ n \\
&\operatorname{pred}\ 0 &&=\ 0 \\
&\operatorname{pred}\ (\operatorname{pred}\ 0) &&=\ \operatorname{pred}\ 0\ =\ 0 \\
& \ldots
\end{align}</math>
and so on.
==== Defining pred through pairs ====
The identity [[#Predecessor function|above]] may be coded with the explicit use of pairs. It can be done in several ways, for instance,
:<math>\begin{align}
\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{align}</math>
The expansion for <math>\operatorname{pred}_2 3</math> is:
:<math>\begin{align}
\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{align}</math>
This is a simpler definition to devise but leads to a more complex lambda expression,
:<math> \begin{align}
\operatorname{pred}_2 \equiv \lambda n.
n\ &(\lambda p. p\ (\lambda a b h. h\ b\ (\operatorname{succ}\ b)) ) \,\,
(\lambda h. h\ 0\ 0) \,\,
(\lambda a b. a)
\end{align}</math>
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 <math>\operatorname{pred}</math> definition. Another encoding follows the second variant of the predecessor identity directly,
:<math> \begin{align}
\operatorname{pred}_3 \equiv \lambda n f x.
n\ &(\lambda p. p\ (\lambda a b h. h\ b\ (f\ b)) ) \,\,
(\lambda h. h\ x\ x) \,\,
(\lambda a b. a)
\end{align}</math>
This way it is already quite close to the original, "outside-in" <math>\operatorname{pred}</math> definition, also creating the chain of <math>f</math>s like it does, only in a bit more wasteful way still. But it is very much less wasteful than the previous, <math>\operatorname{pred}_2</math> definition here. Indeed if we trace its execution we arrive at the new, even more streamlined, yet fully equivalent, definition
<!--
PRED n f x = n (^p. p (^abh. h b (f b))) (^h. h x x) (^ab. a)
PRED n f x = n (G f) (P x x) K
P a b h = h a b
G f p = p (^abh. h b (f b))
G f (P a b) = P a b (^abh. h b (f b))
= (^abh. h b (f b)) a b
= (^h. h b (f b))
= P b (f b) ==== G f: a, b ―――→ b, (f b) !!
PRED 3 f x = G f (G f (G f (P x x ))) K
= G f (G f (P x (f x) )) K
= G f (P (f x) (f (f x)) ) K
= P (f (f x)) (f (f (f x))) K
PRED 3 f x = H f (H f (H f K)) x x
= H f (H f K) x (f x)
= H f K (f x) (f (f x))
= K (f (f x)) (f (f (f x)))
= (f (f x))
-->
:<math> \begin{align}
\operatorname{pred}_4 \equiv \lambda n f x.
n\ &(\lambda r a b. r\ b\ (f\ b)) \,
K\ x\ x
\end{align}</math>
which makes it fully clear and apparent that this is all about just argument modification and passing. Its reduction proceeds as
:<math>\begin{align}
\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{align} </math>
clearly showing what is going on. Still, the original <math>\operatorname{pred}</math> 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 <math>f</math> is short-circuiting. The top-down approach is also used with other definitions like
:<math> \begin{align}
\operatorname{pred}_5 \equiv \lambda n f x.
n\ &(\lambda r a b. a\ (r\ b\ b)) \,
(\lambda a b. x)\ I\ f \\
\operatorname{third} \equiv \lambda n f x.
n\ &(\lambda r a b c. a\ (r\ b\ c\ a)) \,
(\lambda a b c. x)\ I\ I\ f \\
\operatorname{thirdRounded} \equiv \lambda n f x.
n\ &(\lambda r a b c. a\ (r\ b\ c\ a)) \,
(\lambda a b c. x)\ I\ f\ I \\
\operatorname{twoThirds} \equiv \lambda n f x.
n\ &(\lambda r a b c. a\ (r\ b\ c\ a)) \,
(\lambda a b c. x)\ I\ f\ f \\
\operatorname{factorial} \equiv \lambda n f x.
n\ &(\lambda r a. a\ (r\ (\operatorname{succ} a))) \,
(\lambda a. f)\ 1\ x \\
\end{align}</math>
=== Division ===
[[Division (mathematics)|Division]] of natural numbers may be implemented by,<ref>
{{cite web
|last=Allison
|first=Lloyd
|title=Lambda Calculus Integers
|url=http://www.csse.monash.edu.au/~lloyd/tildeFP/Lambda/Examples/const-int/}}
</ref>
: <math> n/m = \operatorname{if}\ n \ge m\ \operatorname{then}\ 1 + (n-m)/m\ \operatorname{else}\ 0 </math>
Calculating <math>n-m</math> takes many beta reductions. Unless doing the reduction by hand, this doesn't matter that much, but it is preferable to not have to do this calculation twice. The simplest predicate for testing numbers is ''IsZero'' so consider the condition.
: <math> \operatorname{IsZero}\ (\operatorname{minus}\ n\ m) </math>
But this condition is equivalent to <math> n \le m </math>, not <math> n<m </math>. If this expression is used then the mathematical definition of division given above is translated into function on Church numerals as,
: <math> \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) </math>
As desired, this definition has a single call to <math> \operatorname{minus}\ n\ m </math>. However the result is that this formula gives the value of <math>(n-1)/ m</math>.
This problem may be corrected by adding 1 to ''n'' before calling ''divide''. The definition of ''divide'' is then,
: <math> \operatorname{divide}\ n = \operatorname{divide1}\ (\operatorname{succ}\ n) </math>
''divide1'' is a recursive definition. The [[Fixed-point combinator|Y combinator]] may be used to implement the recursion. Create a new function called ''div'' by;
* In the left hand side <math> \operatorname{divide1} \rightarrow \operatorname{div} \ c</math>
* In the right hand side <math> \operatorname{divide1} \rightarrow c </math>
to get,
: <math> \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) </math>
Then,
:<math> \operatorname{divide} = \lambda n.\operatorname{divide1}\ (\operatorname{succ}\ n) </math>
where,
: <math>\begin{align}
\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{align}</math>
:: <math>\begin{align}
\operatorname{true} &\equiv \lambda a.\lambda b.a\\
\operatorname{false} &\equiv \lambda a.\lambda b.b
\end{align}</math>
: <math>\begin{align}
\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{align}</math>
Gives,
: <math>\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) </math>
Or as text, using \ for {{mvar|λ}},
divide = (\n.((\f.(\x.x x) (\x.f (x x))) (\c.\n.\m.\f.\x.(\d.(\n.n (\x.(\a.\b.b)) (\a.\b.a)) d ((\f.\x.x) f x) (f (c d m f x))) ((\m.\n.n (\n.\f.\x.n (\g.\h.h (g f)) (\u.x) (\u.u)) m) n m))) ((\n.\f.\x. f (n f x)) n))
For example, 9/3 is represented by
divide (\f.\x.f (f (f (f (f (f (f (f (f x))))))))) (\f.\x.f (f (f x)))
Using a lambda calculus calculator, the above expression reduces to 3, using normal order.
\f.\x.f (f (f (x)))
=== Signed numbers ===
One simple approach for extending Church Numerals to [[Integer|signed numbers]] is to use a Church pair, containing Church numerals representing a positive and a negative value.<ref>
{{cite web
|last=Bauer
|first=Andrej
|title=Andrej's answer to a question; "Representing negative and complex numbers using lambda calculus"
|url=https://cs.stackexchange.com/q/2272
}}</ref> The integer value is the difference between the two Church numerals.
A natural number is converted to a signed number by,
:<math>\operatorname{convert}_s = \lambda x.\operatorname{pair}\ x\ 0 </math>
Negation is performed by swapping the values.
:<math>\operatorname{neg}_s = \lambda x.\operatorname{pair}\ (\operatorname{second}\ x)\ (\operatorname{first}\ x) </math>
The integer value is more naturally represented if one of the pair is zero. The ''OneZero'' function achieves this condition,
:<math>\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)))))</math>
The recursion may be implemented using the Y combinator,
:<math>\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)))))</math>
:<math>\operatorname{OneZero} = Y \operatorname{OneZ}</math>
=== Plus and minus ===
Addition is defined mathematically on the pair by,
:<math>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] </math>
The last expression is translated into lambda calculus as,
:<math>\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))) </math>
Similarly subtraction is defined,
:<math>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] </math>
giving,
:<math>\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))) </math>
=== Multiply and divide ===
Multiplication may be defined by,
:<math>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]</math>
The last expression is translated into lambda calculus as,
:<math>\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))) </math>
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.
:<math>\operatorname{divZ} = \lambda x.\lambda y.\operatorname{IsZero}\ y\ 0 \ (\operatorname{divide}\ x\ y) </math>
''divZ'' is then used in the following formula, which is the same as for multiplication, but with ''mult'' replaced by ''divZ''.
:<math>\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))) </math>
=== Rational and real numbers ===
Rational and [[computable number|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.<ref>
{{cite web|url=https://wiki.haskell.org/Exact_real_arithmetic|title=Exact real arithmetic|last=|first=|date=|website=Haskell|url-status=live|archive-url=https://web.archive.org/web/20150326164041/https://wiki.haskell.org/Exact_real_arithmetic |archive-date=2015-03-26 |access-date=}}
</ref>
<ref>
{{cite web
|last=Bauer
|first=Andrej
|title=Real number computational software|website=[[GitHub]]
|date=26 September 2022
|url=https://github.com/andrejbauer/marshall}}
</ref> The references given describe software that could, in theory, be translated into lambda calculus. Once real numbers are defined, complex numbers are naturally encoded as a pair of real numbers.
The data types and functions described above demonstrate that any data type or calculation may be encoded in lambda calculus. This is the [[Church–Turing thesis]].
===Translation with other representations===
Most real-world languages have support for machine-native integers; the ''church'' and ''unchurch'' functions convert between nonnegative integers and their corresponding Church numerals. The functions are given here in [[Haskell (programming language)|Haskell]], where the <code>\</code> corresponds to the λ of Lambda calculus. Implementations in other languages are similar.
<syntaxhighlight lang="haskell">
type Church a = (a -> a) -> a -> a
church :: Integer -> Church Integer
church 0 = \f -> \x -> x
church n = \f -> \x -> f (church (n-1) f x)
unchurch :: Church Integer -> Integer
unchurch cn = cn (+ 1) 0
</syntaxhighlight>
==Church Booleans==
''Church Booleans'' are the Church encoding of the Boolean values ''true'' and ''false.'' Some programming languages use these as an implementation model for Boolean arithmetic; examples are [[Smalltalk]] and [[Pico (programming language)|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:
: <math>\begin{align}
\operatorname{true} &\equiv \lambda a.\lambda b.a\\
\operatorname{false} &\equiv \lambda a.\lambda b.b
\end{align}</math>
This definition allows predicates (i.e. functions returning [[Truth value|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:
: <math>\operatorname{predicate-}x\ \operatorname{then-clause}\ \operatorname{else-clause} </math>
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''.
: <math>\begin{align}
\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{align}</math>
Some examples:
: <math>\begin{align}
\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{align}</math>
== Predicates ==
A ''predicate'' is a function that returns a Boolean value. The most fundamental predicate is <math>\operatorname{IsZero}</math>, which returns <math>\operatorname{true}</math> if its argument is the Church numeral <math>0</math>, and <math>\operatorname{false}</math> if its argument is any other Church numeral:
: <math>\operatorname{IsZero} = \lambda n.n\ (\lambda x.\operatorname{false})\ \operatorname{true}</math>
The following predicate tests whether the first argument is less-than-or-equal-to the second:
: <math>\operatorname{LEQ} = \lambda m.\lambda n.\operatorname{IsZero}\ (\operatorname{minus}\ m\ n)</math>,
Because of the identity,
: <math> x = y \equiv (x \le y \land y \le x) </math>
The test for equality may be implemented as,
: <math>\operatorname{EQ} = \lambda m.\lambda n.\operatorname{and}\ (\operatorname{LEQ}\ m\ n)\ (\operatorname{LEQ}\ n\ m) </math>
==Church pairs==
{{See also|Cons}}
Church pairs are the Church encoding of the [[cons|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,
: <math>\begin{align}
\operatorname{pair} &\equiv \lambda x y.\lambda z.z\ x\ y \\
\operatorname{first} &\equiv \lambda p.p\ (\lambda x y.x) \\
\operatorname{second} &\equiv \lambda p.p\ (\lambda x y.y)
\end{align}
</math>
For example,
: <math>\begin{align}
& \operatorname{first}\ (\operatorname{pair}\ a\ b) \\
=& \ (\lambda p.p\ (\lambda x y.x))\ ((\lambda x y z.z\ x\ y)\ a\ b) \\
=& \ (\lambda p.p\ (\lambda x y.x))\ (\lambda z.z\ a\ b) \\
=& \ (\lambda z.z\ a\ b)\ (\lambda x y.x) \\
=& \ (\lambda x y.x)\ a\ b \\
=& \ a
\end{align}
</math>
==List encodings==
An ([[Immutable object|immutable]]) [[list (computing)|list]] is constructed from list nodes. The basic operations on the list are;
{| class="wikitable"
|-
! Function !! Description
|-
| ''nil'' || Construct an empty list.
|-
| ''isnil'' || Test if list is empty.
|-
| ''cons'' || Prepend a given value to a (possibly empty) list.
|-
| ''head'' || Get the first element of the list.
|-
| ''tail'' || Get the rest of the list.
|}
We give four different representations of lists below:
* Build each list node from two pairs (to allow for empty lists).
* Build each list node from one pair.
* Represent the list using the [[Fold (higher-order function)|right fold function]].
* Represent the list using Scott's encoding that takes cases of match expression as arguments
=== Two pairs as a list node ===
A nonempty list can be implemented by a Church pair;
* ''First'' contains the head.
* ''Second'' contains the tail.
However this does not give a representation of the empty list, because there is no "null" pointer. To represent null, the pair may be wrapped in another pair, giving three values:
* ''First'' - the null pointer (empty list).
* ''Second.First'' contains the head.
* ''Second.Second'' contains the tail.
Using this idea the basic list operations can be defined like this:<ref>{{cite book
| last = Pierce
| first = Benjamin C.
| authorlink = Benjamin C. Pierce
| title = [[Types and Programming Languages]]
| publisher = [[MIT Press]]
| year = 2002
| pages = 500
| isbn = 978-0-262-16209-8}}</ref>
{| class="wikitable"
|-
! Expression !! Description
|-
| <math> \operatorname{nil} \equiv \operatorname{pair}\ \operatorname{true}\ \operatorname{true} </math>
| The first element of the pair is ''true'' meaning the list is null.
|-
| <math> \operatorname{isnil} \equiv \operatorname{first} </math>
| Retrieve the null (or empty list) indicator.
|-
| <math> \operatorname{cons} \equiv \lambda h.\lambda t.\operatorname{pair} \operatorname{false}\ (\operatorname{pair} h\ t) </math>
| Create a list node, which is not null, and give it a head ''h'' and a tail ''t''.
|-
|<math> \operatorname{head} \equiv \lambda z.\operatorname{first}\ (\operatorname{second} z) </math>
| ''second.first'' is the head.
|-
| <math> \operatorname{tail} \equiv \lambda z.\operatorname{second}\ (\operatorname{second} z) </math>
| ''second.second'' is the tail.
|}
In a ''nil'' node ''second'' is never accessed, provided that '''head''' and '''tail''' are only applied to nonempty lists.
=== One pair as a list node ===
Alternatively, define<ref>{{cite book |first=John |last=Tromp |chapter=14. Binary Lambda Calculus and Combinatory Logic |editor-last=Calude |editor-first=Cristian S |title=Randomness And Complexity, From Leibniz To Chaitin |chapter-url=https://books.google.com/books?id=flPICgAAQBAJ&pg=PP1 |date=2007 |publisher=World Scientific |isbn=978-981-4474-39-9 |pages=237–262}}<br/>As PDF: {{cite web |first=John |last=Tromp |title=Binary Lambda Calculus and Combinatory Logic |date=14 May 2014 |publisher= |url=https://tromp.github.io/cl/LC.pdf |access-date=2017-11-24}}</ref>
: <math>\begin{align}
\operatorname{cons} &\equiv \operatorname{pair} \\
\operatorname{head} &\equiv \operatorname{ \{- first -\}} \equiv \lambda l.\ l\ (\lambda h t d.\ h)\ \operatorname{nil} \\
\operatorname{tail} &\equiv \operatorname{ \{- second -\}} \equiv \lambda l.\ l\ (\lambda h t d.\ t)\ \operatorname{nil} \\
\operatorname{nil} &\equiv \operatorname{false} \\
\operatorname{isnil} &\equiv \lambda l.l\ (\lambda h t d. \operatorname{false}) \operatorname{true} \\
\end{align}</math>
where the definitions like the last one follow the general pattern of the safe use of a list, where <math>h</math> and <math>t</math> refer to the list's head and tail:
: <math>\begin{align}
\operatorname{process-list} &\equiv \lambda l.l\ (\lambda h t d. \langle \operatorname{head-and-tail-clause}\rangle )\ \langle \operatorname{nil-clause}\rangle \\
\end{align}</math>
Other operations for one pair as a list node
: <math>\begin{align}
\operatorname{fold} &\equiv \lambda f.\ \operatorname{Y}\ (\lambda r.\lambda a l.\ l\ (\lambda h t d.\ r\ (f\ a\ h)\ t)\ a) \\
\operatorname{rfold} &\equiv \lambda f a.\ \operatorname{Y}\ (\lambda r.\lambda l.\ l\ (\lambda h t d.\ f\ (r\ t)\ h)\ a) \\
\operatorname{length} &\equiv \operatorname{fold}\ (\lambda a h.\ \operatorname{succ}\ a)\ \operatorname{zero}
\end{align}</math>
----
: <math>\begin{align}
\operatorname{map} &\equiv \lambda f.\ \operatorname{rfold}\ (\lambda a h.\ \operatorname{cons}\ (f\ h)\ a)\ \operatorname{nil} \\
\operatorname{filter} &\equiv \lambda p.\ \operatorname{rfold}\ (\lambda a h.\ p\ h\ (\operatorname{cons}\ h\ a)\ a)\ \operatorname{nil} \\
\operatorname{reverse} &\equiv \operatorname{fold}\ (\lambda a h.\ \operatorname{cons}\ h\ a)\ \operatorname{nil} \\
\operatorname{concat} &\equiv \lambda l g.\ \operatorname{rfold}\ (\lambda a h.\ \operatorname{cons}\ h\ a)\ g\ l \\
\operatorname{conj} &\equiv \lambda l v.\ \operatorname{concat}\ l\ (\operatorname{cons}\ v\ \operatorname{nil})
\end{align}</math>
----
: <math>\begin{align}
\operatorname{drop} &\equiv \lambda n.\ n\ \operatorname{tail} \\
& \equiv \operatorname{Y}\ (\lambda r.\lambda n l.\ l\ (\lambda h t d.\ \operatorname{IsZero}\ n\ l\ (r\ (\operatorname{pred}\ n)\ t))\ \operatorname{nil}) \\
\operatorname{drop-last} &\equiv \lambda n l.\ \operatorname{IsZero}\ n\ l\ \operatorname{second} ( \\
& \ \ \ \ \ \ \ \ \operatorname{Y}\ (\lambda r l_r.\ l_r\ (\lambda h t d. \\
& \ \ \ \ \ \ \ \ \ \ \ \ 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 r l.\ l\ (\lambda h t d.\ p\ h\ (r\ t)\ l)\ \operatorname{nil}) \\
\operatorname{take} &\equiv \operatorname{Y}\ (\lambda r n l.\ l\ (\lambda h t d.\ \operatorname{IsZero}\ n\ \operatorname{nil}\ (\operatorname{cons}\ h\ (r\ (\operatorname{pred}\ n)\ t)))\ \operatorname{nil}) \\
\operatorname{take-last} &\equiv \lambda n l.\ \operatorname{IsZero}\ n\ l\ \operatorname{second} ( \\
& \ \ \ \ \ \ \ \ \operatorname{Y}\ (\lambda r l_r.\ l_r\ (\lambda h t d. \\
& \ \ \ \ \ \ \ \ \ \ \ \ 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 r l.\ l\ (\lambda h t d.\ p\ h\ (\operatorname{cons}\ h\ (r\ t))\ \operatorname{nil})\ \operatorname{nil})
\end{align}</math>
----
: <math>\begin{align}
\operatorname{all} &\equiv \operatorname{Y}\ (\lambda r p l.\ l\ (\lambda h t d.\ p\ h\ (r\ p\ t)\ \operatorname{false})\ \operatorname{true}) \\
\operatorname{any} &\equiv \operatorname{Y}\ (\lambda r p l.\ l\ (\lambda h t d.\ p\ h\ \operatorname{true}\ (r\ p\ t))\ \operatorname{false}) \\
\operatorname{element-at} &\equiv \lambda n l.\ \operatorname{head}\ (\operatorname{drop}\ n\ l) \\
\operatorname{insert-at} &\equiv \lambda n v l.\ \operatorname{concat}\ (\operatorname{take}\ n\ l)\ (\operatorname{cons}\ v\ (\operatorname{drop}\ n\ l)) \\
\operatorname{remove-at} &\equiv \lambda n l.\ \operatorname{concat}\ (\operatorname{take}\ n\ l)\ (\operatorname{drop}\ (\operatorname{succ}\ n)\ l) \\
\operatorname{replace-at} &\equiv \lambda n v l.\ \operatorname{concat}\ (\operatorname{take}\ n\ l)\ (\operatorname{cons}\ v\ (\operatorname{drop}\ (\operatorname{succ}\ n)\ l)) \\
\operatorname{index-of} &\equiv \lambda p.\ \operatorname{Y}\ (\lambda r n l.\ l\ (\lambda h t d.\ p\ h\ n\ (r\ (\operatorname{succ}\ n)\ t))\ \operatorname{zero})\ \operatorname{one} \\
\operatorname{last-index-of} &\equiv \lambda p.\ \operatorname{Y}\ (\lambda r n l.\ l\ (\lambda h t d.\ (\lambda i.\ \operatorname{IsZero}\ i\ (p\ h\ n\ \operatorname{zero})\ i)\ (r\ (\operatorname{succ}\ n)\ t))\ \operatorname{zero})\ \operatorname{one} \\
\operatorname{range} &\equiv \lambda f z.\ \operatorname{Y}\ (\lambda r s n.\ \operatorname{IsZero}\ n\ \operatorname{nil}\ (\operatorname{cons}\ (s\ f\ z)\ (r\ (\operatorname{succ}\ s)\ (\operatorname{pred}\ n))))\ \operatorname{zero} \\
\operatorname{repeat} &\equiv \lambda v.\ \operatorname{Y}\ (\lambda r n.\ \operatorname{IsZero}\ n\ \operatorname{nil}\ (\operatorname{cons}\ v\ (r\ (\operatorname{pred}\ n)))) \\
\operatorname{zip} &\equiv Y\ (\lambda r l_1 l_2.\ l_1\ (\lambda h_1 t_1 d_1.\ l_2\ (\lambda h_2 t_2 d_2.\ \operatorname{cons}\ (\operatorname{pair}\ h_1\ h_2)\ (r\ t_1\ t_2))\ \operatorname{nil})\ \operatorname{nil}) \\
\end{align}</math>
=== Represent the list using ''right fold'' ===
As an alternative to the encoding using Church pairs, a list can be encoded by identifying it with its [[Fold (higher-order function)|right fold function]]. For example, a list of three elements x, y and z can be encoded by a higher-order function that when applied to a combinator c and a value n returns c x (c y (c z n)). Equivalently, it is an application of the chain of functional compositions of partial applications, (c x <math>\circ</math> c y <math>\circ</math> c z) n.
: <math>
\begin{align}
\operatorname{nil} &\equiv \lambda c.\lambda n.n\\
\operatorname{singleton} &\equiv \lambda h.\lambda c.\lambda n.c\ h\ n\\
\operatorname{cons} &\equiv \lambda h.\lambda t.\lambda c.\lambda n.c\ h\ (t\ c\ n)\\
\operatorname{append} &\equiv \lambda l.\lambda t.\lambda c.\lambda n.l\ c\ (t\ c\ n)\\
\operatorname{isnil} &\equiv \lambda l.l\ (\lambda h.\lambda r.\operatorname{false})\ \operatorname{true}\\
\operatorname{nonempty} &\equiv \lambda l.l\ (\lambda h.\lambda r.true)\ \operatorname{false}\\
\operatorname{head} &\equiv \lambda l.l\ (\lambda h.\lambda r.h)\ \operatorname{false}\\
\operatorname{map} &\equiv \lambda f.\lambda l.\lambda c.\lambda n.l\ (\lambda h.\lambda r.c\ (f\ h)\ r)\ n\\
\operatorname{tail} &\equiv \lambda l.\lambda c.\lambda n.l\ (\lambda h.\lambda r.\lambda g.g\ h\ (r\ c))\ (\lambda c.n)\ (\lambda h.\lambda t.t)
\end{align}</math>
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 () <math>\circ</math> c () <math>\circ</math> c ()) n = (f <math>\circ</math> f <math>\circ</math> f) n, as is used in Church numerals.
=== Represent the list using Scott encoding ===
An alternative representation is Scott encoding, which uses the idea of [[continuation]]s and can lead to simpler code.<ref>{{cite book
| last = Jansen | first = Jan Martin
| editor1-last = Achten | editor1-first = Peter
| editor2-last = Koopman | editor2-first = Pieter W. M.
| contribution = Programming in the λ-Calculus: From Church to Scott and Back
| doi = 10.1007/978-3-642-40355-2_12
| pages = 168–180
| publisher = Springer
| series = Lecture Notes in Computer Science
| title = The Beauty of Functional Code - Essays Dedicated to Rinus Plasmeijer on the Occasion of His 61st Birthday
| volume = 8106
| year = 2013| isbn = 978-3-642-40354-5
}}</ref> (see also [[Mogensen–Scott encoding]]).
In this approach, we use the fact that lists can be observed using [[pattern matching]] expression. For example, using [[Scala (programming language)|Scala]] notation, if <code>list</code> denotes a value of type <code>List</code> with empty list <code>Nil</code> and constructor <code>Cons(h, t)</code> we can inspect the list and compute <code>nilCode</code> in case the list is empty and {{code|consCode(h, t)}} when the list is not empty:
<syntaxhighlight lang="scala">
list match {
case Nil => nilCode
case Cons(h, t) => consCode(h,t)
}
</syntaxhighlight>
The {{code|list}} is given by how it acts upon {{code|nilCode}} and {{code|consCode}}. We therefore define a list as a function that accepts such {{code|nilCode}} and {{code|consCode}} as arguments, so that instead of the above pattern match we may simply write:
: <math>
\operatorname{list}\ \operatorname{nilCode}\ \operatorname{consCode}
</math>
Let us denote by {{code|n}} the parameter corresponding to {{code|nilCode}} and by {{code|c}} the parameter corresponding to {{code|consCode}}.
The empty list is the one that returns the nil argument:
: <math>
\operatorname{nil} \equiv \lambda n. \lambda c.\ n
</math>
The non-empty list with head {{code|h}} and tail {{code|t}} is given by
: <math>
\operatorname{cons}\ h\ t\ \ \equiv\ \ \lambda n.\lambda c.\ c\ h\ t
</math>
More generally, an [[algebraic data type]] with <math>m</math> alternatives becomes a function with <math>m</math> parameters. When the <math>i</math>th constructor has <math>n_i</math> arguments, the corresponding parameter of the encoding takes <math>n_i</math> arguments as well.
Scott encoding can be done in untyped lambda calculus, whereas its use with types requires a type system with recursion and type polymorphism. A list with element type E in this representation that is used to compute values of type C would have the following recursive type definition, where '=>' denotes [[function type]]:
<syntaxhighlight lang="scala">
type List =
C => // nil argument
(E => List => C) => // cons argument
C // result of pattern matching
</syntaxhighlight>
A list that can be used to compute arbitrary types would have a type that quantifies over <code>C</code>. A list generic {{Clarification needed|reason=|date=December 2019}} in <code>E</code> would also take <code>E</code> as the type argument.
==See also==
*[[Lambda calculus]]
*[[System F]] for Church numerals in a typed calculus
*[[Mogensen–Scott encoding]]
*[[Ordinal number#Von Neumann definition of ordinals|Von Neumann definition of ordinals]] — another way to encode natural numbers: as sets
== References ==
<references/>
*{{cite journal |first=A. |last=Stump |title=Directly reflective meta-programming |journal=High-Order Symb Comput |volume=22 |issue= 2|pages=115–144 |date=2009 |doi=10.1007/s10990-007-9022-0 |url=http://www.cs.uiowa.edu/~astump/papers/archon.pdf |citeseerx=10.1.1.489.5018|s2cid=16124152 }}
*{{cite web |url=http://www.cs.rice.edu/~javaplt/311/Readings/supplemental.pdf |title=Church numerals and booleans explained |first=Robert |last=Cartwright |work=Comp 311 — Review 2 |publisher=[[Rice University]]}}
*{{cite thesis |first=Colin |last=Kemp |title=Theoretical Foundations for Practical 'Totally Functional Programming' |date=2007 |type=PhD |publisher=School of Information Technology and Electrical Engineering, The University of Queensland |chapter-url=https://espace.library.uq.edu.au/view/UQ:171001 |citeseerx=10.1.1.149.3505 |chapter=§2.4.1 Church Naturals, §2.4.2 Church Booleans, Ch. 5 Derivation techniques for TFP |pages=14–17, 93–145}} All about Church and other similar encodings, including how to derive them and operations on them, from first principles
*[http://www.csse.monash.edu.au/~lloyd/tildeFP/Lambda/Examples/const-int/ Some interactive examples of Church numerals]
*[http://blog.klipse.tech/lambda/2016/07/24/lambda-calculus-2.html Lambda Calculus Live Tutorial: Boolean Algebra]
{{Mathematical logic}}
{{Alonzo Church}}
[[Category:Lambda calculus]]
| |||