Lambda calculus

Lambda Definability

Equation form expr-0215b1ee4c46326d

(YSearch)Fn1¯…nk¯m¯↠m¯if f(n1,…,nk,m)=0, or↠(YSearch)Fn1¯…nk¯m+1¯otherwise. Since f is regular, f(n1,…,nk,y)=0 for some y, and so(YSearch)Fn1¯…nk¯0¯↠h(n1,…,nk)¯.(Y \, \fn{Search}) F \num{n_1} \dots\num{n_k}\, \num{m} & \red \num{m} \intertext{if $f(n_1, \dots, n_k, m) = 0$, or} & \red (Y \, \fn{Search}) F\, \num{n_1} \dots\num{n_k}\, \num{m+1} \intertext{otherwise. Since $f$ is regular, $f(n_1, \dots, n_k, y) = 0$ for some $y$, and so} (Y \, \fn{Search}) F \num{n_1} \dots\num{n_k}\,\num{0} & \red \num{h(n_1, \dots, n_k)}.

Read as: the application of capital Y applied to Search, then successively to capital F and the Church numerals for n subscript one through n subscript k, in that order to the Church numeral for m, end application reduces to the Church numeral for m if f of n subscript one through n subscript k, followed by m, equals zero. Or the same starting expression reduces to the application of capital Y applied to Search, then successively to capital F and the Church numerals for n subscript one through n subscript k, in that order to the Church numeral for m plus one, end application otherwise. Since f is regular, f of n subscript one through n subscript k, followed by y, equals zero for some y, and so the application of capital Y applied to Search, then successively to capital F and the Church numerals for n subscript one through n subscript k, in that order to the Church numeral for zero, end application reduces to the Church numeral for h of n subscript one through n subscript k.

Means: the application of capital Y applied to Search, then successively to capital F and the Church numerals for n subscript one through n subscript k, in that order to the Church numeral for m, end application reduces to the Church numeral for m if f of n subscript one through n subscript k, followed by m, equals zero. Or the same starting expression reduces to the application of capital Y applied to Search, then successively to capital F and the Church numerals for n subscript one through n subscript k, in that order to the Church numeral for m plus one, end application otherwise. Since f is regular, f of n subscript one through n subscript k, followed by y, equals zero for some y, and so the application of capital Y applied to Search, then successively to capital F and the Church numerals for n subscript one through n subscript k, in that order to the Church numeral for zero, end application reduces to the Church numeral for h of n subscript one through n subscript k.

1 occurrence in this chapter

Equation form expr-026426f5b7589465

λfx.n¯(m¯f)x\lambd[fx][\num{n}(\num{m}\, f)x]

Read as: lambda f then x, with body the application of the application of the Church numeral for n to the application of the Church numeral for m to f, end application, end application to x, end application, end abstraction

Means: lambda f then x, with body the application of the application of the Church numeral for n to the application of the Church numeral for m to f, end application, end application to x, end application, end abstraction

1 occurrence in this chapter

Equation form expr-03709ab133617afc

normalize(#Fn1¯…nk¯#)\fn{normalize}(\Gn{F\num{n_1}\dots\num{n_k}})

Read as: Normalize of the Gödel number of capital F successively applied to the Church numerals for n subscript one through n subscript k, in that order

Means: Normalize of the Gödel number of capital F successively applied to the Church numerals for n subscript one through n subscript k, in that order

1 occurrence in this chapter

Equation form expr-03a9b09b35d993ff

n=0n=0

Read as: n equals zero

Means: n equals zero

1 occurrence in this chapter

Equation form expr-059b2d69503206fd

nm¯\num{nm}

Read as: the Church numeral for n times m

Means: the Church numeral for n times m

1 occurrence in this chapter

Equation form expr-07abbb6e48508206

Mult≡λab.λfx.a(bf)x\fn{Mult} \ident \lambd[ab][\lambd[fx][a (b f) x]]

Read as: Multiply is syntactically identical to lambda a then b, with body lambda f then x, with body the application of the application of a to the application of b to f, end application, end application to x, end application, end abstraction, end abstraction

Means: Multiply is syntactically identical to lambda a then b, with body lambda f then x, with body the application of the application of a to the application of b to f, end application, end application to x, end application, end abstraction, end abstraction

1 occurrence in this chapter

Equation form expr-08c6aa8d5824f2de

succ\Succ

Read as: the successor function

Means: the successor function

4 occurrences in this chapter

Equation form expr-08dacf0f9d78188a

λ\lambd

Read as: lambda

Means: lambda

7 occurrences in this chapter

Equation form expr-08f271887ce94707

MM

Read as: capital M

Means: capital M

2 occurrences in this chapter

Equation form expr-0a566b1db5acde7f

g0g_0

Read as: g subscript zero

Means: g subscript zero

1 occurrence in this chapter

Equation form expr-0bfdd7135668149c

Fn¯↠m¯F\, \num n \red \num m

Read as: the application of capital F to the Church numeral for n, end application reduces to the Church numeral for m

Means: the application of capital F to the Church numeral for n, end application reduces to the Church numeral for m

2 occurrences in this chapter

Equation form expr-0db78f5df32e0b90

g(YCg)g(Y_Cg)

Read as: the application of g to the application of capital Y subscript capital C to g, end application, end application

Means: the application of g to the application of capital Y subscript capital C to g, end application, end application

1 occurrence in this chapter

Equation form expr-0e66d86741d7890d

Fac3¯↠YFac′3¯↠Fac′(YFac′)3¯≡(λx.λn.IsZeron1¯(Multn(x(Predn))))Fac3¯↠IsZero3¯1¯(Mult3¯(Fac(Pred3¯)))↠Mult3¯(Fac2¯).Similarly,Fac2¯↠Mult2¯(Fac1¯)Fac1¯↠Mult1¯(Fac0¯)butFac0¯↠Fac′(YFac′)0¯≡(λx.λn.IsZeron1¯(Multn(x(Predn))))Fac0¯↠IsZero0¯1¯(Mult0¯(Fac(Pred0¯))).↠1¯.So togetherFac3¯↠Mult3¯(Mult2¯(Mult1¯1¯)).\fn{Fac}\,\num 3 &\red Y\, \fn{Fac}' \, \num 3 \\ &\red \fn{Fac}' (Y \,\fn{Fac}') \, \num 3 \\ &\ident (\lambd[x][\lambd[n][\fn{IsZero} \, n\, \num 1\, (\fn{Mult}\, n\, (x (\fn{Pred}\, n)))]]) \, \fn{Fac} \, \num 3\\ & \red \fn{IsZero} \, \num 3\, \num 1\, (\fn{Mult}\, \num 3\, (\fn{Fac} (\fn{Pred}\, \num 3))) \\ &\red \fn{Mult}\, \num 3 \, (\fn{Fac} \, \num 2). \intertext{Similarly,} \fn{Fac}\,\num 2 &\red \fn{Mult}\, \num 2 \, (\fn{Fac} \, \num 1) \\ \fn{Fac}\,\num 1 &\red \fn{Mult}\, \num 1 \, (\fn{Fac} \, \num 0) \intertext{but} \fn{Fac}\,\num 0 &\red \fn{Fac}' (Y \,\fn{Fac}') \, \num 0 \\ &\ident (\lambd[x][\lambd[n][\fn{IsZero} \, n\, \num 1\, (\fn{Mult}\, n\, (x (\fn{Pred}\, n)))]]) \, \fn{Fac} \, \num 0\\ & \red \fn{IsZero} \, \num 0\, \num 1\, (\fn{Mult}\, \num 0\, (\fn{Fac} (\fn{Pred}\, \num 0))).\\ &\red \num 1. \intertext{So together} \fn{Fac}\,\num 3 &\red \fn{Mult}\, \num 3 \, (\fn{Mult} \, \num 2\, (\fn{Mult} \, \num 1\, \num 1)).

Read as: the application of Factorial to the Church numeral for three, end application reduces to the application of the application of capital Y to Factorial prime, end application to the Church numeral for three, end application, which reduces to the application of the application of Factorial prime to the application of capital Y to Factorial prime, end application, end application to the Church numeral for three, end application, syntactically identical to the application of the application of lambda x, with body lambda n, with body the application of the application of the application of Is Zero to n, end application to the Church numeral for one, end application to the application of the application of Multiply to n, end application to the application of x to the application of Predecessor to n, end application, end application, end application, end application, end abstraction, end abstraction to Factorial, end application to the Church numeral for three, end application. This reduces to the application of the application of the application of Is Zero to the Church numeral for three, end application to the Church numeral for one, end application to the application of the application of Multiply to the Church numeral for three, end application to the application of Factorial to the application of Predecessor to the Church numeral for three, end application, end application, end application, end application, which reduces to the application of the application of Multiply to the Church numeral for three, end application to the application of Factorial to the Church numeral for two, end application, end application. Similarly, the application of Factorial to the Church numeral for two, end application reduces to the application of the application of Multiply to the Church numeral for two, end application to the application of Factorial to the Church numeral for one, end application, end application. the application of Factorial to the Church numeral for one, end application reduces to the application of the application of Multiply to the Church numeral for one, end application to the application of Factorial to the Church numeral for zero, end application, end application. But the application of Factorial to the Church numeral for zero, end application reduces to the application of the application of Factorial prime to the application of capital Y to Factorial prime, end application, end application to the Church numeral for zero, end application, syntactically identical to the application of the application of lambda x, with body lambda n, with body the application of the application of the application of Is Zero to n, end application to the Church numeral for one, end application to the application of the application of Multiply to n, end application to the application of x to the application of Predecessor to n, end application, end application, end application, end application, end abstraction, end abstraction to Factorial, end application to the Church numeral for zero, end application. This reduces to the application of the application of the application of Is Zero to the Church numeral for zero, end application to the Church numeral for one, end application to the application of the application of Multiply to the Church numeral for zero, end application to the application of Factorial to the application of Predecessor to the Church numeral for zero, end application, end application, end application, end application, which reduces to the Church numeral for one. So together, the application of Factorial to the Church numeral for three, end application reduces to the application of the application of Multiply to the Church numeral for three, end application to the application of the application of Multiply to the Church numeral for two, end application to the application of the application of Multiply to the Church numeral for one, end application to the Church numeral for one, end application, end application, end application.

Means: the application of Factorial to the Church numeral for three, end application reduces to the application of the application of capital Y to Factorial prime, end application to the Church numeral for three, end application, which reduces to the application of the application of Factorial prime to the application of capital Y to Factorial prime, end application, end application to the Church numeral for three, end application, syntactically identical to the application of the application of lambda x, with body lambda n, with body the application of the application of the application of Is Zero to n, end application to the Church numeral for one, end application to the application of the application of Multiply to n, end application to the application of x to the application of Predecessor to n, end application, end application, end application, end application, end abstraction, end abstraction to Factorial, end application to the Church numeral for three, end application. This reduces to the application of the application of the application of Is Zero to the Church numeral for three, end application to the Church numeral for one, end application to the application of the application of Multiply to the Church numeral for three, end application to the application of Factorial to the application of Predecessor to the Church numeral for three, end application, end application, end application, end application, which reduces to the application of the application of Multiply to the Church numeral for three, end application to the application of Factorial to the Church numeral for two, end application, end application. Similarly, the application of Factorial to the Church numeral for two, end application reduces to the application of the application of Multiply to the Church numeral for two, end application to the application of Factorial to the Church numeral for one, end application, end application. the application of Factorial to the Church numeral for one, end application reduces to the application of the application of Multiply to the Church numeral for one, end application to the application of Factorial to the Church numeral for zero, end application, end application. But the application of Factorial to the Church numeral for zero, end application reduces to the application of the application of Factorial prime to the application of capital Y to Factorial prime, end application, end application to the Church numeral for zero, end application, syntactically identical to the application of the application of lambda x, with body lambda n, with body the application of the application of the application of Is Zero to n, end application to the Church numeral for one, end application to the application of the application of Multiply to n, end application to the application of x to the application of Predecessor to n, end application, end application, end application, end application, end abstraction, end abstraction to Factorial, end application to the Church numeral for zero, end application. This reduces to the application of the application of the application of Is Zero to the Church numeral for zero, end application to the Church numeral for one, end application to the application of the application of Multiply to the Church numeral for zero, end application to the application of Factorial to the application of Predecessor to the Church numeral for zero, end application, end application, end application, end application, which reduces to the Church numeral for one. So together, the application of Factorial to the Church numeral for three, end application reduces to the application of the application of Multiply to the Church numeral for three, end application to the application of the application of Multiply to the Church numeral for two, end application to the application of the application of Multiply to the Church numeral for one, end application to the Church numeral for one, end application, end application, end application.

1 occurrence in this chapter

Equation form expr-0f05083b80c3d7e0

n¯(m¯f)x\num{n} (\num{m} f) x

Read as: the application of the application of the Church numeral for n to the application of the Church numeral for m to f, end application, end application to x, end application

Means: the application of the application of the Church numeral for n to the application of the Church numeral for m to f, end application, end application to x, end application

1 occurrence in this chapter

Equation form expr-0f1e7ab45dedbe30

fn(x)f^{n}(x)

Read as: the result of iterating f n times on x, end iteration

Means: the result of iterating f n times on x, end iteration

1 occurrence in this chapter

Equation form expr-0fa108e5fbe8f278

⟨n−1¯,n¯⟩\tuple{\num{n-1}, \num n}

Read as: the ordered pair with first component the Church numeral for n minus one, and second component the Church numeral for n, end pair

Means: the ordered pair with first component the Church numeral for n minus one, and second component the Church numeral for n, end pair

1 occurrence in this chapter

Equation form expr-103f7de3482048f3

GkG_k

Read as: capital G subscript k

Means: capital G subscript k

1 occurrence in this chapter

Equation form expr-12afc54f79271fad

Fac′f\fn{Fac}'\,f

Read as: the application of Factorial prime to f, end application

Means: the application of Factorial prime to f, end application

1 occurrence in this chapter

Equation form expr-139c7c04318de35e

n=0n = 0

Read as: n equals zero

Means: n equals zero

2 occurrences in this chapter

Equation form expr-13e197624394a30a

Mult\fn{Mult}

Read as: Multiply

Means: Multiply

2 occurrences in this chapter

Equation form expr-148de9c5a7a44d19

pp

Read as: p

Means: p

2 occurrences in this chapter

Equation form expr-155536ea6d332f78

Hn0¯…nn−1¯↠h(n0,…,nn−1)¯H\num{n_0}\dots\num{n_{n-1}} \red \num{h(n_0, \dots, n_{n-1})}

Read as: capital H successively applied to the Church numerals for n subscript zero through n subscript n minus one reduces to the Church numeral for h of n subscript zero through n subscript n minus one

Means: capital H successively applied to the Church numerals for n subscript zero through n subscript n minus one reduces to the Church numeral for h of n subscript zero through n subscript n minus one

1 occurrence in this chapter

Equation form expr-15a9b40b9daf2ace

Search≡λg.λfx→y.IsZero(fx→y)y(gx→(Succy)H≡λx→.(YSearch)Fx→0¯,\fn{Search} & \ident \lambd[g][\lambd[f\,\vec{x}\,y][ \fn{IsZero} (f\, \vec{x}\, y)\, y\, (g\, \vec{x} (\fn{Succ}\, y)]]\\ H & \ident \lambd[\vec x][(Y \, \fn{Search}) F\, \vec{x}\, \num{0}],

Read as: Search is syntactically identical to lambda g, with body lambda f, then the entries of vector x, then y, with body the application of the application of the application of Is Zero to f successively applied to the entries of vector x and then y, end application to y, end application to g successively applied to the entries of vector x and then to the application of Successor to y, end successive application, end application, end abstraction, end abstraction. capital H is syntactically identical to lambda the entries of vector x, with body capital Y applied to Search, then to capital F, then successively to the entries of vector x, and finally to the Church numeral for zero, end successive application, end abstraction.

Means: Search is syntactically identical to lambda g, with body lambda f, then the entries of vector x, then y, with body the application of the application of the application of Is Zero to f successively applied to the entries of vector x and then y, end application to y, end application to g successively applied to the entries of vector x and then to the application of Successor to y, end successive application, end application, end abstraction, end abstraction. capital H is syntactically identical to lambda the entries of vector x, with body capital Y applied to Search, then to capital F, then successively to the entries of vector x, and finally to the Church numeral for zero, end successive application, end abstraction.

1 occurrence in this chapter

Equation form expr-162c50fcdef2d170

Dnm+1⟨0¯,Fn¯⟩↠⟨m+1¯,h(n,m+1)¯⟩D_n^{m+1} \tuple{\num{0}, F\, \num{n}} \red \tuple{\num{m+1}, \num{h(n, m+1)}}

Read as: the result of iterating capital D subscript n m plus one times on the ordered pair with first component the Church numeral for zero, and second component the application of capital F to the Church numeral for n, end application, end pair, end iteration reduces to the ordered pair with first component the Church numeral for m plus one, and second component the Church numeral for h of n and m plus one, end pair

Means: the result of iterating capital D subscript n m plus one times on the ordered pair with first component the Church numeral for zero, and second component the application of capital F to the Church numeral for n, end application, end pair, end iteration reduces to the ordered pair with first component the Church numeral for m plus one, and second component the Church numeral for h of n and m plus one, end pair

1 occurrence in this chapter

Equation form expr-164a18c4e98fdae5

Dnm+1⟨0¯,Fn¯⟩≡Dn(Dnm⟨0¯,Fn¯⟩)↠Dn⟨m¯,h(n,m)¯⟩ (by IH)≡(λp.⟨Succ(Fstp),(Gn¯(Fstp)(Sndp))⟩)⟨m¯,h(n,m)¯⟩→⟨Succ(Fst⟨m¯,h(n,m)¯⟩),(Gn¯(Fst⟨m¯,h(n,m)¯⟩)(Snd⟨m¯,h(n,m)¯⟩))⟩↠⟨Succm¯,(Gn¯m¯h(n,m)¯)⟩↠⟨m+1¯,g(n,m,h(n,m))¯⟩D_n^{m+1} \tuple{\num{0}, F\, \num{n}} & \ident D_n(D_n^{m} \tuple{\num{0}, F\, \num{n}})\\ & \red D_n\,\tuple{\num{m}, \num{h(n, m)}} \text{\qquad (by IH)}\\ & \ident (\lambd[p][ \tuple{ \fn{Succ} (\fn{Fst}\, p), (G \, \num{n} (\fn{Fst}\, p) (\fn{Snd}\, p)) }]) \tuple{\num{m}, \num{h(n,m)}}\\ & \redone \tuple{\fn{Succ} (\fn{Fst}\, \tuple{\num{m}, \num{h(n,m)}}),\\ & \qquad (G \, \num{n} (\fn{Fst}\, \tuple{\num{m}, \num{h(n,m)}}) (\fn{Snd}\, \tuple{\num{m}, \num{h(n,m)}}))}\\ & \red \tuple{\fn{Succ}\, \num{m}, (G \, \num{n} \,\num{m} \, \num{h(n,m)})}\\ & \red \tuple{\num{m+1}, \num{g(n, m, h(n, m))}}

Read as: the result of iterating capital D subscript n m plus one times on the ordered pair with first component the Church numeral for zero, and second component the application of capital F to the Church numeral for n, end application, end pair, end iteration is syntactically identical to the application of capital D subscript n to the result of iterating capital D subscript n m times on the ordered pair with first component the Church numeral for zero, and second component the application of capital F to the Church numeral for n, end application, end pair, end iteration, end application. By the induction hypothesis, this reduces to the application of capital D subscript n to the ordered pair with first component the Church numeral for m, and second component the Church numeral for h of n and m, end pair, end application, syntactically identical to the application of lambda p, with body the ordered pair with first component the application of Successor to the application of First to p, end application, end application, and second component the application of the application of the application of capital G to the Church numeral for n, end application to the application of First to p, end application, end application to the application of Second to p, end application, end application, end pair, end abstraction to the ordered pair with first component the Church numeral for m, and second component the Church numeral for h of n and m, end pair, end application. This reduces in one step to the ordered pair with first component the application of Successor to the application of First to the ordered pair with first component the Church numeral for m, and second component the Church numeral for h of n and m, end pair, end application, end application, and second component the application of the application of the application of capital G to the Church numeral for n, end application to the application of First to the ordered pair with first component the Church numeral for m, and second component the Church numeral for h of n and m, end pair, end application, end application to the application of Second to the ordered pair with first component the Church numeral for m, and second component the Church numeral for h of n and m, end pair, end application, end application, end pair. This reduces to the ordered pair with first component the application of Successor to the Church numeral for m, end application, and second component the application of the application of the application of capital G to the Church numeral for n, end application to the Church numeral for m, end application to the Church numeral for h of n and m, end application, end pair. This reduces to the ordered pair with first component the Church numeral for m plus one, and second component the Church numeral for g of n, m, and h of n and m, end pair.

Means: the result of iterating capital D subscript n m plus one times on the ordered pair with first component the Church numeral for zero, and second component the application of capital F to the Church numeral for n, end application, end pair, end iteration is syntactically identical to the application of capital D subscript n to the result of iterating capital D subscript n m times on the ordered pair with first component the Church numeral for zero, and second component the application of capital F to the Church numeral for n, end application, end pair, end iteration, end application. By the induction hypothesis, this reduces to the application of capital D subscript n to the ordered pair with first component the Church numeral for m, and second component the Church numeral for h of n and m, end pair, end application, syntactically identical to the application of lambda p, with body the ordered pair with first component the application of Successor to the application of First to p, end application, end application, and second component the application of the application of the application of capital G to the Church numeral for n, end application to the application of First to p, end application, end application to the application of Second to p, end application, end application, end pair, end abstraction to the ordered pair with first component the Church numeral for m, and second component the Church numeral for h of n and m, end pair, end application. This reduces in one step to the ordered pair with first component the application of Successor to the application of First to the ordered pair with first component the Church numeral for m, and second component the Church numeral for h of n and m, end pair, end application, end application, and second component the application of the application of the application of capital G to the Church numeral for n, end application to the application of First to the ordered pair with first component the Church numeral for m, and second component the Church numeral for h of n and m, end pair, end application, end application to the application of Second to the ordered pair with first component the Church numeral for m, and second component the Church numeral for h of n and m, end pair, end application, end application, end pair. This reduces to the ordered pair with first component the application of Successor to the Church numeral for m, end application, and second component the application of the application of the application of capital G to the Church numeral for n, end application to the Church numeral for m, end application to the Church numeral for h of n and m, end application, end pair. This reduces to the ordered pair with first component the Church numeral for m plus one, and second component the Church numeral for g of n, m, and h of n and m, end pair.

1 occurrence in this chapter

Equation form expr-181eb8788541fd73

Yg↠g(Yg)↠g(g(Yg))↠g(g(g(Yg)))…Y g &\red g (Y g) \\ &\red g (g (Y g)) \\ &\red g(g (g (Y g)))\\ &\ldots

Read as: the application of capital Y to g, end application reduces to the application of g to the application of capital Y to g, end application, end application, which reduces to the application of g to the application of g to the application of capital Y to g, end application, end application, end application, which reduces to the application of g to the application of g to the application of g to the application of capital Y to g, end application, end application, end application, end application, and so on.

Means: the application of capital Y to g, end application reduces to the application of g to the application of capital Y to g, end application, end application, which reduces to the application of g to the application of g to the application of capital Y to g, end application, end application, end application, which reduces to the application of g to the application of g to the application of g to the application of capital Y to g, end application, end application, end application, end application, and so on.

1 occurrence in this chapter

Equation form expr-18f5384d58bcb1bb

YY

Read as: capital Y

Means: capital Y

3 occurrences in this chapter

Equation form expr-19d058036fc48554

toChurch\fn{toChurch}

Read as: To Church

Means: To Church

1 occurrence in this chapter

Equation form expr-1b16b1df538ba12d

nn

Read as: n

Means: n

13 occurrences in this chapter

Equation form expr-1b8340cbc4763167

f:ℕk→ℕf\colon \Nat^k \to \Nat

Read as: f from k tuples of natural numbers to the natural numbers

Means: f from k tuples of natural numbers to the natural numbers

1 occurrence in this chapter

Equation form expr-1be95b047631a3d6

And\fn{And}

Read as: And

Means: And

3 occurrences in this chapter

Equation form expr-1cda3dcefc1d3319

Fn0¯n1¯…nk−1¯↠f(n0,n1,…,nk−1)¯F \, \num{n_0} \, \num{n_1} \dots \num{n_{k-1}} \red \num{f(n_0, n_1, \dots, n_{k-1})}

Read as: capital F successively applied to the Church numerals for n subscript zero through n subscript k minus one, in that order reduces to the Church numeral for f of n subscript zero through n subscript k minus one

Means: capital F successively applied to the Church numerals for n subscript zero through n subscript k minus one, in that order reduces to the Church numeral for f of n subscript zero through n subscript k minus one

1 occurrence in this chapter

Equation form expr-1fe9736f2c37f7c1

⟨0¯,f(n)¯⟩\tuple{\num{0}, \num{f(n)}}

Read as: the ordered pair with first component the Church numeral for zero, and second component the Church numeral for f of n, end pair

Means: the ordered pair with first component the Church numeral for zero, and second component the Church numeral for f of n, end pair

1 occurrence in this chapter

Equation form expr-20c23d922e552a64

g(x1,…,xk)=μyf(x1,…,xk,y)=0g(x_1, \dots, x_k) = \umin{y}{f(x_1,\dots,x_k, y) = 0}

Read as: g of x subscript one through x subscript k equals the least y such that f of x subscript one through x subscript k, followed by y, equals zero

Means: g of x subscript one through x subscript k equals the least y such that f of x subscript one through x subscript k, followed by y, equals zero

1 occurrence in this chapter

Equation form expr-23146883045d970e

m¯\num m

Read as: the Church numeral for m

Means: the Church numeral for m

1 occurrence in this chapter

Equation form expr-252f10c83610ebca

ff

Read as: f

Means: f

25 occurrences in this chapter

Equation form expr-26e91de6b43af143

normalize\fn{normalize}

Read as: Normalize

Means: Normalize

1 occurrence in this chapter

Equation form expr-27456b6742a25d6e

Mult′≡λab.a(Adda)0¯.\fn{Mult}' \ident \lambd[ab][a (\fn{Add}\, a) \num{0}].

Read as: Multiply prime is syntactically identical to lambda a then b, with body the application of the application of a to the application of Add to a, end application, end application to the Church numeral for zero, end application, end abstraction

Means: Multiply prime is syntactically identical to lambda a then b, with body the application of the application of a to the application of Add to a, end application, end application to the Church numeral for zero, end application, end abstraction

1 occurrence in this chapter

Equation form expr-286f997f317dc96d

Pred≡λn.Fst(n(λp.⟨Sndp,Succ(Sndp)⟩)⟨0¯,0¯⟩)\fn{Pred} \ident \lambd[n][\fn{Fst}(n (\lambd[p][\tuple{\fn{Snd}\, {p}, \fn{Succ}(\fn{Snd}\, {p})}]) \tuple{\num 0, \num 0})]

Read as: Predecessor is syntactically identical to lambda n, with body the application of First to the application of the application of n to lambda p, with body the ordered pair with first component the application of Second to p, end application, and second component the application of Successor to the application of Second to p, end application, end application, end pair, end abstraction, end application to the ordered pair with first component the Church numeral for zero, and second component the Church numeral for zero, end pair, end application, end application, end abstraction

Means: Predecessor is syntactically identical to lambda n, with body the application of First to the application of the application of n to lambda p, with body the ordered pair with first component the application of Second to p, end application, and second component the application of Successor to the application of Second to p, end application, end application, end pair, end abstraction, end application to the ordered pair with first component the Church numeral for zero, and second component the Church numeral for zero, end pair, end application, end application, end abstraction

1 occurrence in this chapter

Equation form expr-289244ef9e61a1d7

(Yg)N(Yg)N

Read as: the application of the application of capital Y to g, end application to capital N, end application

Means: the application of the application of capital Y to g, end application to capital N, end application

1 occurrence in this chapter

Equation form expr-2d291fa7d9d39b0e

Add\fn{Add}

Read as: Add

Means: Add

3 occurrences in this chapter

Equation form expr-2d711642b726b044

xx

Read as: x

Means: x

13 occurrences in this chapter

Equation form expr-32381516983cb54a

(YSearch)Fn1¯…nk¯0¯(Y \, \fn{Search}) F \num{n_1}\dots\num{n_k}\,\num{0}

Read as: the application of capital Y applied to Search, then successively to capital F and the Church numerals for n subscript one through n subscript k, in that order to the Church numeral for zero, end application

Means: the application of capital Y applied to Search, then successively to capital F and the Church numerals for n subscript one through n subscript k, in that order to the Church numeral for zero, end application

1 occurrence in this chapter

Equation form expr-33269765b8421f29

f(x1,…,xk,y)f(x_1, \dots, x_k, y)

Read as: f of x subscript one through x subscript k, followed by y

Means: f of x subscript one through x subscript k, followed by y

1 occurrence in this chapter

Equation form expr-333e0a1e27815d0c

GG

Read as: capital G

Means: capital G

2 occurrences in this chapter

Equation form expr-348c95b48a520fd5

YCgY_Cg

Read as: the application of capital Y subscript capital C to g, end application

Means: the application of capital Y subscript capital C to g, end application

1 occurrence in this chapter

Equation form expr-34f8e8c2065a124d

IsZero={0}\fn{IsZero} = \{0\}

Read as: Is Zero equals the set whose sole element is zero

Means: Is Zero equals the set whose sole element is zero

1 occurrence in this chapter

Equation form expr-36c47edad7da5b52

Yg=βg(Yg)Yg \equal[\beta] g(Yg)

Read as: the application of capital Y to g, end application is beta equivalent to the application of g to the application of capital Y to g, end application, end application

Means: the application of capital Y to g, end application is beta equivalent to the application of g to the application of capital Y to g, end application, end application

1 occurrence in this chapter

Equation form expr-37f059acdabdba58

Succ′≡λn.λfx.nf(fx)\fn{Succ}' & \ident \lambd[{n}][\lambd[fx][{n} f (f x)]]

Read as: Successor prime is syntactically identical to lambda n, with body lambda f then x, with body the application of the application of n to f, end application to the application of f to x, end application, end application, end abstraction, end abstraction

Means: Successor prime is syntactically identical to lambda n, with body lambda f then x, with body the application of the application of n to f, end application to the application of f to x, end application, end application, end abstraction, end abstraction

1 occurrence in this chapter

Equation form expr-387ecd4f9f07b479

Snd\fn{Snd}

Read as: Second

Means: Second

1 occurrence in this chapter

Equation form expr-3a92e2a77861c0ec

Fac≡λn.IsZeron1¯(Multn((λn.IsZeron1¯(Multn(Fac(Predn))))(Predn)))\fn{Fac} & \ident \lambd[n][\fn{IsZero}\, n\, \num{1}] \\ & \qquad (\fn{Mult}\, n ((\lambd[n][\fn{IsZero} \, n \, \num 1\, (\fn{Mult}\, n\, (\fn{Fac} (\fn{Pred}\, n)))]) (\fn{Pred}\, n)))

Read as: Factorial is syntactically identical to lambda n, with body the application of the application of the application of Is Zero to n, end application to the Church numeral for one, end application to the application of the application of Multiply to n, end application to the application of lambda n, with body the application of the application of the application of Is Zero to n, end application to the Church numeral for one, end application to the application of the application of Multiply to n, end application to the application of Factorial to the application of Predecessor to n, end application, end application, end application, end application, end abstraction to the application of Predecessor to n, end application, end application, end application, end application, end abstraction.

Means: Factorial is syntactically identical to lambda n, with body the application of the application of the application of Is Zero to n, end application to the Church numeral for one, end application to the application of the application of Multiply to n, end application to the application of lambda n, with body the application of the application of the application of Is Zero to n, end application to the Church numeral for one, end application to the application of the application of Multiply to n, end application to the application of Factorial to the application of Predecessor to n, end application, end application, end application, end application, end abstraction to the application of Predecessor to n, end application, end application, end application, end application, end abstraction.

1 occurrence in this chapter

Equation form expr-3cf13e5a10558a53

Not\fn{Not}

Read as: Not

Means: Not

1 occurrence in this chapter

Equation form expr-3e23e8160039594a

bb

Read as: b

Means: b

2 occurrences in this chapter

Equation form expr-3f79bb7b435b0532

ee

Read as: e

Means: e

1 occurrence in this chapter

Equation form expr-3fcca9f4a6175738

Rn1¯…nk¯↠βtruewhenever R(n1,…,nk) andRn1¯…nk¯↠βfalseR\, \num{n_1} \dots \num{n_k} & \bred \fn{true} \intertext{whenever $R(n_1, \dots, n_k)$ and} R\, \num{n_1} \dots \num{n_k} & \bred \fn{false}

Read as: Capital R successively applied to the Church numerals for n subscript one through n subscript k beta reduces to True whenever the relation capital R holds of n subscript one through n subscript k, and capital R successively applied to those same Church numerals beta reduces to False

Means: Capital R successively applied to the Church numerals for n subscript one through n subscript k beta reduces to True whenever the relation capital R holds of n subscript one through n subscript k, and capital R successively applied to those same Church numerals beta reduces to False

1 occurrence in this chapter

Equation form expr-420acba5c6453ea4

Fac′\fn{Fac}'

Read as: Factorial prime

Means: Factorial prime

4 occurrences in this chapter

Equation form expr-4219f3c92eb4e243

m=0m=0

Read as: m equals zero

Means: m equals zero

1 occurrence in this chapter

Equation form expr-42253cfb46807387

c(n)=kc(n) = k

Read as: c of n equals k

Means: c of n equals k

1 occurrence in this chapter

Equation form expr-42b6dd4c5bca1d62

m¯f\num{m} f

Read as: the application of the Church numeral for m to f, end application

Means: the application of the Church numeral for m to f, end application

1 occurrence in this chapter

Equation form expr-430c6a52fc3a4cf9

Fac′\fn{Fac'}

Read as: Factorial prime

Means: Factorial prime

2 occurrences in this chapter

Equation form expr-449dbada7186d092

H≡λx.λy.Snd(yD⟨0¯,Fx⟩)where D≡λp.⟨Succ(Fstp),(Gx(Fstp)(Sndp))⟩H \ident & \lambd[x][\lambd[y][\fn{Snd} (y D \tuple{\num{0}, F x})]] \intertext{where } D \ident & \lambd[p][\tuple{\fn{Succ} (\fn{Fst}\, p), (G x (\fn{Fst}\, p) (\fn{Snd}\, p))}]

Read as: capital H is syntactically identical to lambda x, with body lambda y, with body the application of Second to the application of the application of y to capital D, end application to the ordered pair with first component the Church numeral for zero, and second component the application of capital F to x, end application, end pair, end application, end application, end abstraction, end abstraction. Where capital D is syntactically identical to lambda p, with body the ordered pair with first component the application of Successor to the application of First to p, end application, end application, and second component the application of the application of the application of capital G to x, end application to the application of First to p, end application, end application to the application of Second to p, end application, end application, end pair, end abstraction.

Means: capital H is syntactically identical to lambda x, with body lambda y, with body the application of Second to the application of the application of y to capital D, end application to the ordered pair with first component the Church numeral for zero, and second component the application of capital F to x, end application, end pair, end application, end application, end abstraction, end abstraction. Where capital D is syntactically identical to lambda p, with body the ordered pair with first component the application of Successor to the application of First to p, end application, end application, and second component the application of the application of the application of capital G to x, end application to the application of First to p, end application, end application to the application of Second to p, end application, end application, end pair, end abstraction.

1 occurrence in this chapter

Equation form expr-44bd7ae60f478fae

HH

Read as: capital H

Means: capital H

1 occurrence in this chapter

Equation form expr-4533627b60db3935

Yg↠g(Yg)Yg \red g(Yg)

Read as: the application of capital Y to g, end application reduces to the application of g to the application of capital Y to g, end application, end application

Means: the application of capital Y to g, end application reduces to the application of g to the application of capital Y to g, end application, end application

1 occurrence in this chapter

Equation form expr-45db310895af4af0

g(n,m,h(n,m))=h(n,m+1)g(n, m, h(n, m)) = h(n, m+1)

Read as: g of n, m, and h of n and m, equals h of n and m plus one

Means: g of n, m, and h of n and m, equals h of n and m plus one

1 occurrence in this chapter

Equation form expr-47031b2080b536b6

f(n0,…,nk−1)f(n_0, \dots, n_{k-1})

Read as: f of n subscript zero through n subscript k minus one

Means: f of n subscript zero through n subscript k minus one

1 occurrence in this chapter

Equation form expr-489c746df378ca97

f(n)=h(n,0)f(n) = h(n, 0)

Read as: f of n equals h of n and zero

Means: f of n equals h of n and zero

1 occurrence in this chapter

Equation form expr-4940ad5fa499a571

fn(x)f^n(x)

Read as: the result of iterating f n times on x, end iteration

Means: the result of iterating f n times on x, end iteration

2 occurrences in this chapter

Equation form expr-4d8861c598775b72

Succ≡λa.λfx.f(afx).Given our conventions, this is short forSucc≡λa.λf.λx.(f((af)x)).Succ is a function that accepts as argument a number a, and evaluates to another function, λfx.f(afx). That function is not itself a Church numeral. However, if the argument a is a Church numeral, it reduces to one. Consider:(λa.λfx.f(afx))n¯→λfx.f(n¯fx).The embedded term n¯fx is a redex, since n¯ is λfx.fnx. So n¯fx→fnx and so, for the entire term we haveSuccn¯↠λfx.f(fn(x)),\fn{Succ} & \ident \lambd[a][\lambd[fx][f ({a} f x)]]. \intertext{Given our conventions, this is short for} \fn{Succ} & \ident \lambd[a][\lambd[f][\lambd[x][(f (({a} f) x))]]]. \intertext{$\fn{Succ}$ is a function that accepts as argument a number~$a$, and evaluates to another function, $\lambd[fx][f ({a} f x)]$. That function is not itself a Church numeral. However, if the argument $a$ is a Church numeral, it reduces to one. Consider:} (\lambd[a][\lambd[fx][f ({a} f x)]])\,\num{n} & \redone \lambd[fx][f ({\num{n}} f x)]. \intertext{The embedded term $\num{n}fx$ is a redex, since $\num{n}$ is $\lambd[fx][f^nx]$. So $\num{n}fx \redone f^nx$ and so, for the entire term we have} \fn{Succ}\, \num n & \red \lambd[fx][f(f^n(x))],

Read as: Successor is syntactically identical to lambda a, with body lambda f then x, with body the application of f to the application of the application of a to f, end application to x, end application, end application, end abstraction, end abstraction. Given our conventions, this is short for Successor is syntactically identical to lambda a, with body lambda f, with body lambda x, with body the application of f to the application of the application of a to f, end application to x, end application, end application, end abstraction, end abstraction, end abstraction. Successor is a function that accepts as argument a number a, and evaluates to another function, lambda f then x, with body the application of f to the application of the application of a to f, end application to x, end application, end application, end abstraction. That function is not itself a Church numeral. However, if the argument a is a Church numeral, it reduces to one. Consider: the application of lambda a, with body lambda f then x, with body the application of f to the application of the application of a to f, end application to x, end application, end application, end abstraction, end abstraction to the Church numeral for n, end application reduces in one step to lambda f then x, with body the application of f to the application of the application of the Church numeral for n to f, end application to x, end application, end application, end abstraction. The embedded term the application of the application of the Church numeral for n to f, end application to x, end application is a redex, since the Church numeral for n is lambda f then x, with body the result of iterating f n times on x, end iteration, end abstraction. So the application of the application of the Church numeral for n to f, end application to x, end application reduces in one step to the result of iterating f n times on x, end iteration, and so, for the entire term we have the application of Successor to the Church numeral for n, end application reduces to lambda f then x, with body the application of f to the result of iterating f n times on x, end iteration, end application, end abstraction

Means: Successor is syntactically identical to lambda a, with body lambda f then x, with body the application of f to the application of the application of a to f, end application to x, end application, end application, end abstraction, end abstraction. Given our conventions, this is short for Successor is syntactically identical to lambda a, with body lambda f, with body lambda x, with body the application of f to the application of the application of a to f, end application to x, end application, end application, end abstraction, end abstraction, end abstraction. Successor is a function that accepts as argument a number a, and evaluates to another function, lambda f then x, with body the application of f to the application of the application of a to f, end application to x, end application, end application, end abstraction. That function is not itself a Church numeral. However, if the argument a is a Church numeral, it reduces to one. Consider: the application of lambda a, with body lambda f then x, with body the application of f to the application of the application of a to f, end application to x, end application, end application, end abstraction, end abstraction to the Church numeral for n, end application reduces in one step to lambda f then x, with body the application of f to the application of the application of the Church numeral for n to f, end application to x, end application, end application, end abstraction. The embedded term the application of the application of the Church numeral for n to f, end application to x, end application is a redex, since the Church numeral for n is lambda f then x, with body the result of iterating f n times on x, end iteration, end abstraction. So the application of the application of the Church numeral for n to f, end application to x, end application reduces in one step to the result of iterating f n times on x, end iteration, and so, for the entire term we have the application of Successor to the Church numeral for n, end application reduces to lambda f then x, with body the application of f to the result of iterating f n times on x, end iteration, end application, end abstraction

1 occurrence in this chapter

Equation form expr-4dc4e01def696af8

Pin\Proj{n}{i}

Read as: the projection of arity n with index i

Means: the projection of arity n with index i

3 occurrences in this chapter

Equation form expr-5038d55159bf6364

Multn¯m¯\fn{Mult} \, \num{n} \, \num{m}

Read as: the application of the application of Multiply to the Church numeral for n, end application to the Church numeral for m, end application

Means: the application of the application of Multiply to the Church numeral for n, end application to the Church numeral for m, end application

1 occurrence in this chapter

Equation form expr-5081cbc657fe24bd

m¯\num{m}

Read as: the Church numeral for m

Means: the Church numeral for m

1 occurrence in this chapter

Equation form expr-50fe35055a91ceed

Succ\fn{Succ}

Read as: Successor

Means: Successor

2 occurrences in this chapter

Equation form expr-51aeea8ffa05d262

n−1n-1

Read as: n minus one

Means: n minus one

1 occurrence in this chapter

Equation form expr-526c8fec0deb09e9

efe f

Read as: the application of e to f, end application

Means: the application of e to f, end application

1 occurrence in this chapter

Equation form expr-53bef11c8a572fb4

Fac′≡λg.λn.IsZeron1¯(Multn(g(Predn)))\fn{Fac}' \ident \lambd[g][\lambd[n][\fn{IsZero} \, n \, \num 1\, (\fn{Mult} \, n\, (g (\fn{Pred} n)))]]

Read as: Factorial prime is syntactically identical to lambda g, with body lambda n, with body the application of the application of the application of Is Zero to n, end application to the Church numeral for one, end application to the application of the application of Multiply to n, end application to the application of g to the application of Predecessor to n, end application, end application, end application, end application, end abstraction, end abstraction

Means: Factorial prime is syntactically identical to lambda g, with body lambda n, with body the application of the application of the application of Is Zero to n, end application to the Church numeral for one, end application to the application of the application of Multiply to n, end application to the application of g to the application of Predecessor to n, end application, end application, end application, end application, end abstraction, end abstraction

1 occurrence in this chapter

Equation form expr-540280aaf3c57a0d

gx1…xn=βNwhere N may contain g and x1, …, xn. Then there is always a term G≡(Yλg.λx1…xn.N) such thatGx1…xn=βN[G/g].For by the fixpoint theorem,G≡(Yλg.λx1…xn.N)↠λg.λx1…xn.N(Yλg.λx1…xn.N)≡(λg.λx1…xn.N)Gand consequentlyGx1…xn↠(λg.λx1…xn.N)Gx1…xn↠(λx1…xn.N[G/g])x1…xn↠N[G/g].g\,x_1\dots x_n & \equal[\beta] N \intertext{where $N$ may contain~$g$ and $x_1$, \dots,~$x_n$. Then there is always a term~$G \ident (Y \lambd[g][\lambd[x_1\dots x_n][N]])$ such that} G\,x_1 \dots x_n & \equal[\beta] \Subst{N}{G}{g}. \intertext{For by the fixpoint theorem,} G \ident (Y \lambd[g][\lambd[x_1\dots x_n][N]]) & \red \lambd[g][\lambd[x_1\dots x_n][N]](Y \lambd[g][\lambd[x_1\dots x_n][N]])\\ & \ident (\lambd[g][\lambd[x_1\dots x_n][N]])\,G \intertext{and consequently} G\,x_1 \dots x_n & \red (\lambd[g][\lambd[x_1\dots x_n][N]])\,G\,x_1\dots x_n\\ & \red (\lambd[x_1\dots x_n][\Subst{N}{G}{g}])\,x_1\dots x_n\\ & \red \Subst{N}{G}{g}.

Read as: g successively applied to x subscript one through x subscript n is beta equivalent to capital N. Here capital N may contain g and x subscript one through x subscript n. Then there is always a term capital G is syntactically identical to the application of capital Y to lambda g, with body lambda x subscript one through x subscript n, with body capital N, end abstraction, end abstraction, end application, such that capital G successively applied to x subscript one through x subscript n is beta equivalent to the result of substituting capital G for free g in capital N, end substitution. For by the fixpoint theorem, capital G is syntactically identical to the application of capital Y to lambda g, with body lambda x subscript one through x subscript n, with body capital N, end abstraction, end abstraction, end application, which reduces to lambda g, with body lambda x subscript one through x subscript n, with body the application of capital N to the application of capital Y to lambda g, with body lambda x subscript one through x subscript n, with body capital N, end abstraction, end abstraction, end application, end application, end abstraction, end abstraction, syntactically identical to the application of lambda g, with body lambda x subscript one through x subscript n, with body capital N, end abstraction, end abstraction to capital G, end application. And consequently, capital G successively applied to x subscript one through x subscript n reduces to the application of lambda g, with body lambda x subscript one through x subscript n, with body capital N, end abstraction, end abstraction to capital G, end application successively applied to x subscript one through x subscript n. This reduces to lambda x subscript one through x subscript n, with body the result of substituting capital G for free g in capital N, end substitution, end abstraction successively applied to x subscript one through x subscript n, which reduces to the result of substituting capital G for free g in capital N, end substitution.

Means: g successively applied to x subscript one through x subscript n is beta equivalent to capital N. Here capital N may contain g and x subscript one through x subscript n. Then there is always a term capital G is syntactically identical to the application of capital Y to lambda g, with body lambda x subscript one through x subscript n, with body capital N, end abstraction, end abstraction, end application, such that capital G successively applied to x subscript one through x subscript n is beta equivalent to the result of substituting capital G for free g in capital N, end substitution. For by the fixpoint theorem, capital G is syntactically identical to the application of capital Y to lambda g, with body lambda x subscript one through x subscript n, with body capital N, end abstraction, end abstraction, end application, which reduces to lambda g, with body lambda x subscript one through x subscript n, with body the application of capital N to the application of capital Y to lambda g, with body lambda x subscript one through x subscript n, with body capital N, end abstraction, end abstraction, end application, end application, end abstraction, end abstraction, syntactically identical to the application of lambda g, with body lambda x subscript one through x subscript n, with body capital N, end abstraction, end abstraction to capital G, end application. And consequently, capital G successively applied to x subscript one through x subscript n reduces to the application of lambda g, with body lambda x subscript one through x subscript n, with body capital N, end abstraction, end abstraction to capital G, end application successively applied to x subscript one through x subscript n. This reduces to lambda x subscript one through x subscript n, with body the result of substituting capital G for free g in capital N, end substitution, end abstraction successively applied to x subscript one through x subscript n, which reduces to the result of substituting capital G for free g in capital N, end substitution.

1 occurrence in this chapter

Equation form expr-545988f122ef6e4d

Fac′f\fn{Fac'}\, f

Read as: the application of Factorial prime to f, end application

Means: the application of Factorial prime to f, end application

1 occurrence in this chapter

Equation form expr-5684a211c68076b6

Ck≡λx.k¯C_k \ident \lambd[x][\num{k}]

Read as: capital C subscript k is syntactically identical to lambda x, with body the Church numeral for k, end abstraction

Means: capital C subscript k is syntactically identical to lambda x, with body the Church numeral for k, end abstraction

1 occurrence in this chapter

Equation form expr-56cb2ce615a8eaca

F(Gx)F (G x)

Read as: the application of capital F to the application of capital G to x, end application, end application

Means: the application of capital F to the application of capital G to x, end application, end application

2 occurrences in this chapter

Equation form expr-575d86b85365c7b4

G0G_0

Read as: capital G subscript zero

Means: capital G subscript zero

1 occurrence in this chapter

Equation form expr-583cf6290785d72c

λ\lambda

Read as: lambda

Means: lambda

1 occurrence in this chapter

Equation form expr-59a94416a2a319ca

η\eta

Read as: eta

Means: eta

2 occurrences in this chapter

Equation form expr-5afa20230f875253

n∈ℕn \in \Nat

Read as: n is a natural number

Means: n is a natural number

2 occurrences in this chapter

Equation form expr-5b93a9b0461acefd

YgYg

Read as: the application of capital Y to g, end application

Means: the application of capital Y to g, end application

9 occurrences in this chapter

Equation form expr-5c51a8649f399bee

YCg=βg(YCg)Y_Cg \equal[\beta] g(Y_Cg)

Read as: the application of capital Y subscript capital C to g, end application is beta equivalent to the application of g to the application of capital Y subscript capital C to g, end application, end application

Means: the application of capital Y subscript capital C to g, end application is beta equivalent to the application of g to the application of capital Y subscript capital C to g, end application, end application

1 occurrence in this chapter

Equation form expr-5c5b8c4423165d39

H≡λx0…xn−1.F(G0x0…xn−1)…(Gk−1x0…xn−1)H \ident \lambd[x_0 \dots x_{n-1}][F\, (G_0 x_0 \dots x_{n-1}) \dots (G_{k-1} x_0 \dots x_{n-1})]

Read as: capital H is syntactically identical to lambda x subscript zero through x subscript n minus one, with body capital F successively applied to k arguments, from the result of applying capital G subscript zero to x subscript zero through x subscript n minus one, through the result of applying capital G subscript k minus one to those same x arguments, in that order, end successive application, end abstraction

Means: capital H is syntactically identical to lambda x subscript zero through x subscript n minus one, with body capital F successively applied to k arguments, from the result of applying capital G subscript zero to x subscript zero through x subscript n minus one, through the result of applying capital G subscript k minus one to those same x arguments, in that order, end successive application, end abstraction

1 occurrence in this chapter

Equation form expr-5e948d069c545f38

f(n1,…,nk,m)=0f(n_1, \dots, n_k, m) = 0

Read as: f of n subscript one through n subscript k, followed by m, equals zero

Means: f of n subscript one through n subscript k, followed by m, equals zero

1 occurrence in this chapter

Equation form expr-5fc0166478cd48dd

Fac\fn{Fac}

Read as: Factorial

Means: Factorial

8 occurrences in this chapter

Equation form expr-5fc0ad6ce11af400

Dnm⟨0¯,Fn¯⟩↠⟨m¯,h(n,m)¯⟩D_n^m \tuple{\num{0}, F\, \num{n}} \red \tuple{\num{m}, \num{h(n, m)}}

Read as: the result of iterating capital D subscript n m times on the ordered pair with first component the Church numeral for zero, and second component the application of capital F to the Church numeral for n, end application, end pair, end iteration reduces to the ordered pair with first component the Church numeral for m, and second component the Church numeral for h of n and m, end pair

Means: the result of iterating capital D subscript n m times on the ordered pair with first component the Church numeral for zero, and second component the application of capital F to the Church numeral for n, end application, end pair, end iteration reduces to the ordered pair with first component the Church numeral for m, and second component the Church numeral for h of n and m, end pair

2 occurrences in this chapter

Equation form expr-5fc9cece534f0f27

λy.y\lambd[y][y]

Read as: lambda y, with body y, end abstraction

Means: lambda y, with body y, end abstraction

1 occurrence in this chapter

Equation form expr-5fe6dc6b2281b3d2

zero\Zero

Read as: the zero function

Means: the zero function

3 occurrences in this chapter

Equation form expr-5feceb66ffc86f38

00

Read as: zero

Means: zero

2 occurrences in this chapter

Equation form expr-60a4c2f46b84de07

Add≡λab.λfx.af(bfx)or, alternatively,Add′≡λab.aSuccb.The first addition works as follows: Add first accept two numbers a and b. The result is a function that accepts f and x and returns af(bfx). If a and b are Church numerals n¯ and m¯, this reduces to fn+m(x), which is identical to fn(fm(x)). Or, slowly:(λab.λfx.af(bfx))n¯m¯→λfx.n¯f(m¯fx)→λfx.n¯f(fmx)→λfx.fn(fmx)≡n+m¯.The second representation of addition Add′ works differently: Applied to two Church numerals n¯ and m¯,Add′n¯m¯→n¯Succm¯.But n¯fx always reduces to fn(x). So,n¯Succm¯↠Succn(m¯).\fn{Add} & \ident \lambd[{a}{b}][\lambd[fx][{a} f ({b} f x)]] \intertext{or, alternatively,} \fn{Add}' & \ident \lambd[{a}{b}][{a}\, \fn{Succ} \, {b}]. \intertext{The first addition works as follows: $\fn{Add}$ first accept two numbers ${a}$ and ${b}$. The result is a function that accepts $f$ and $x$ and returns $af(bfx)$. If $a$ and $b$ are Church numerals $\num{n}$ and $\num{m}$, this reduces to $f^{n+m}(x)$, which is identical to $f^{n}(f^{m}(x))$. Or, slowly:} (\lambd[{a}{b}][\lambd[fx][{a} f ({b} f x)]])\num n\,\num m & \redone \lambd[fx][\num{n}\, f (\num {m}\, f x)] \\ & \redone \lambd[fx][\num{n}\, f (f^m x)] \\ & \redone \lambd[fx][f^n (f^m x)] \ident \num {n+m}. \intertext{The second representation of addition $\fn{Add'}$ works differently: Applied to two Church numerals $\num{n}$ and $\num{m}$,} \fn{Add}' \num n \,\num m & \redone \num{n}\, \fn{Succ}\, \num{m}. \intertext{But $\num{n} f x$ always reduces to $f^n(x)$. So,} \num{n}\, \fn{Succ}\, \num{m} & \red \fn{Succ}^n(\num{m}).

Read as: Add is syntactically identical to lambda a then b, with body lambda f then x, with body the application of the application of a to f, end application to the application of the application of b to f, end application to x, end application, end application, end abstraction, end abstraction. Or, alternatively, Add prime is syntactically identical to lambda a then b, with body the application of the application of a to Successor, end application to b, end application, end abstraction. The first addition works as follows. Add first accept two numbers a and b. The result is a function that accepts f and x and returns the application of the application of a to f, end application to the application of the application of b to f, end application to x, end application, end application. If a and b are the Church numerals for n and m, this reduces to the result of iterating f n plus m times on x, end iteration, which is identical to the result of iterating f n times on the result of iterating f m times on x, end iteration, end iteration. Or, slowly: the application of the application of lambda a then b, with body lambda f then x, with body the application of the application of a to f, end application to the application of the application of b to f, end application to x, end application, end application, end abstraction, end abstraction to the Church numeral for n, end application to the Church numeral for m, end application reduces in one step to lambda f then x, with body the application of the application of the Church numeral for n to f, end application to the application of the application of the Church numeral for m to f, end application to x, end application, end application, end abstraction. Then in one step to lambda f then x, with body the application of the application of the Church numeral for n to f, end application to the result of iterating f m times on x, end iteration, end application, end abstraction, then in one step to lambda f then x, with body the result of iterating f n times on the result of iterating f m times on x, end iteration, end iteration, end abstraction, syntactically identical to the Church numeral for n plus m. The second representation of addition, Add prime, works differently. Applied to the two Church numerals for n and m, the application of the application of Add prime to the Church numeral for n, end application to the Church numeral for m, end application reduces in one step to the application of the application of the Church numeral for n to Successor, end application to the Church numeral for m, end application. But the application of the application of the Church numeral for n to f, end application to x, end application reduces to the result of iterating f n times on x, end iteration always. So the application of the application of the Church numeral for n to Successor, end application to the Church numeral for m, end application reduces to the result of iterating Successor n times on the Church numeral for m, end iteration.

Means: Add is syntactically identical to lambda a then b, with body lambda f then x, with body the application of the application of a to f, end application to the application of the application of b to f, end application to x, end application, end application, end abstraction, end abstraction. Or, alternatively, Add prime is syntactically identical to lambda a then b, with body the application of the application of a to Successor, end application to b, end application, end abstraction. The first addition works as follows. Add first accept two numbers a and b. The result is a function that accepts f and x and returns the application of the application of a to f, end application to the application of the application of b to f, end application to x, end application, end application. If a and b are the Church numerals for n and m, this reduces to the result of iterating f n plus m times on x, end iteration, which is identical to the result of iterating f n times on the result of iterating f m times on x, end iteration, end iteration. Or, slowly: the application of the application of lambda a then b, with body lambda f then x, with body the application of the application of a to f, end application to the application of the application of b to f, end application to x, end application, end application, end abstraction, end abstraction to the Church numeral for n, end application to the Church numeral for m, end application reduces in one step to lambda f then x, with body the application of the application of the Church numeral for n to f, end application to the application of the application of the Church numeral for m to f, end application to x, end application, end application, end abstraction. Then in one step to lambda f then x, with body the application of the application of the Church numeral for n to f, end application to the result of iterating f m times on x, end iteration, end application, end abstraction, then in one step to lambda f then x, with body the result of iterating f n times on the result of iterating f m times on x, end iteration, end iteration, end abstraction, syntactically identical to the Church numeral for n plus m. The second representation of addition, Add prime, works differently. Applied to the two Church numerals for n and m, the application of the application of Add prime to the Church numeral for n, end application to the Church numeral for m, end application reduces in one step to the application of the application of the Church numeral for n to Successor, end application to the Church numeral for m, end application. But the application of the application of the Church numeral for n to f, end application to x, end application reduces to the result of iterating f n times on x, end iteration always. So the application of the application of the Church numeral for n to Successor, end application to the Church numeral for m, end application reduces to the result of iterating Successor n times on the Church numeral for m, end iteration.

1 occurrence in this chapter

Equation form expr-611c1d36da398626

n¯≡λfx.fn(x)\num{n} \ident \lambd[fx][f^n(x)]

Read as: the Church numeral for n is syntactically identical to lambda f then x, with body the result of iterating f n times on x, end iteration, end abstraction

Means: the Church numeral for n is syntactically identical to lambda f then x, with body the result of iterating f n times on x, end iteration, end abstraction

1 occurrence in this chapter

Equation form expr-62c66a7a5dd70c31

mm

Read as: m

Means: m

7 occurrences in this chapter

Equation form expr-62d0789e727d78d6

g(Yg)=βYgg(Yg) \equal[\beta] Yg

Read as: the application of g to the application of capital Y to g, end application, end application is beta equivalent to the application of capital Y to g, end application

Means: the application of g to the application of capital Y to g, end application, end application is beta equivalent to the application of capital Y to g, end application

1 occurrence in this chapter

Equation form expr-69b50c1b3bbe6f2b

Fac′f=βf\fn{Fac}' \, f \equal[\beta] f

Read as: the application of Factorial prime to f, end application is beta equivalent to f

Means: the application of Factorial prime to f, end application is beta equivalent to f

1 occurrence in this chapter

Equation form expr-6a766438d1de2cc9

n+mn+m

Read as: n plus m

Means: n plus m

1 occurrence in this chapter

Equation form expr-6b86b273ff34fce1

11

Read as: one

Means: one

1 occurrence in this chapter

Equation form expr-6dce451ebd9bcf6c

Y≡(λux.x(uux))(λux.x(uux)).Y \ident (\lambd[ux][x(uux)])(\lambd[ux][x(uux)]).

Read as: capital Y is syntactically identical to the application of lambda u then x, with body the application of x to the application of the application of u to u, end application to x, end application, end application, end abstraction to lambda u then x, with body the application of x to the application of the application of u to u, end application to x, end application, end application, end abstraction, end application

Means: capital Y is syntactically identical to the application of lambda u then x, with body the application of x to the application of the application of u to u, end application to x, end application, end application, end abstraction to lambda u then x, with body the application of x to the application of the application of u to u, end application to x, end application, end application, end abstraction, end application

1 occurrence in this chapter

Equation form expr-6e951179169137ff

false\fn{false}

Read as: False

Means: False

7 occurrences in this chapter

Equation form expr-7038021faba64787

ck:ℕ→ℕc_k\colon \Nat \to \Nat

Read as: c subscript k from the natural numbers to the natural numbers

Means: c subscript k from the natural numbers to the natural numbers

1 occurrence in this chapter

Equation form expr-70e2a490fe78b799

IsZero≡λn.n(λx.false)true.\fn{IsZero} \ident \lambd[n][n (\lambd[x][\fn{false}])\, \fn{true}].

Read as: Is Zero is syntactically identical to lambda n, with body the application of the application of n to lambda x, with body False, end abstraction, end application to True, end application, end abstraction

Means: Is Zero is syntactically identical to lambda n, with body the application of the application of n to lambda x, with body False, end abstraction, end application to True, end application, end abstraction

1 occurrence in this chapter

Equation form expr-71a0363bfb077add

#F#\Gn{F}

Read as: the Gödel number of capital F

Means: the Gödel number of capital F

1 occurrence in this chapter

Equation form expr-727971ccd449d21b

VV≡(λx.g(xx))V↠g(VV) and thusYCg≡(λg.VV)g↠VV↠g(VV), but alsog(YCg)≡g((λg.VV)g)↠g(VV).VV & \ident (\lambd[x][g(xx)])V \red g(VV) \text{ and thus}\\ Y_C g & \ident (\lambd[g][VV])g \red VV \red g(VV), \text{ but also}\\ g(Y_C g) & \ident g((\lambd[g][VV])g) \red g(VV).

Read as: the application of capital V to capital V, end application is syntactically identical to the application of lambda x, with body the application of g to the application of x to x, end application, end application, end abstraction to capital V, end application, which reduces to the application of g to the application of capital V to capital V, end application, end application. And thus the application of capital Y subscript capital C to g, end application is syntactically identical to the application of lambda g, with body the application of capital V to capital V, end application, end abstraction to g, end application, which reduces to the application of capital V to capital V, end application, which reduces to the application of g to the application of capital V to capital V, end application, end application. But also the application of g to the application of capital Y subscript capital C to g, end application, end application is syntactically identical to the application of g to the application of lambda g, with body the application of capital V to capital V, end application, end abstraction to g, end application, end application, which reduces to the application of g to the application of capital V to capital V, end application, end application.

Means: the application of capital V to capital V, end application is syntactically identical to the application of lambda x, with body the application of g to the application of x to x, end application, end application, end abstraction to capital V, end application, which reduces to the application of g to the application of capital V to capital V, end application, end application. And thus the application of capital Y subscript capital C to g, end application is syntactically identical to the application of lambda g, with body the application of capital V to capital V, end application, end abstraction to g, end application, which reduces to the application of capital V to capital V, end application, which reduces to the application of g to the application of capital V to capital V, end application, end application. But also the application of g to the application of capital Y subscript capital C to g, end application, end application is syntactically identical to the application of g to the application of lambda g, with body the application of capital V to capital V, end application, end abstraction to g, end application, end application, which reduces to the application of g to the application of capital V to capital V, end application, end application.

1 occurrence in this chapter

Equation form expr-72fcd7dafa1f7007

n+1¯\num{n+1}

Read as: the Church numeral for n plus one

Means: the Church numeral for n plus one

1 occurrence in this chapter

Equation form expr-76611dd34d50f93b

f(n)=mf(n) = m

Read as: f of n equals m

Means: f of n equals m

1 occurrence in this chapter

Equation form expr-77c1144d54fcb017

Succ0¯≡(λa.λf.λx.(f((af)x)))(λf.λx.x)→λf.λx.(f(((λf.λx.x)f)x))→λf.λx.(f((λx.x)x))→λf.λx.(fx)≡1¯\fn{Succ}\, \num{0} & \ident (\lambd[a][\lambd[f][\lambd[x][(f (({a} f) x))]]])(\lambd[f][\lambd[x][x]])\\ & \redone \lambd[f][\lambd[x][(f (({(\lambd[f][\lambd[x][x]])} f) x))]] \\ & \redone \lambd[f][\lambd[x][(f ({(\lambd[x][x])} x))]] \\ & \redone \lambd[f][\lambd[x][(f x)]] \ident \num{1}\\

Read as: the application of Successor to the Church numeral for zero, end application is syntactically identical to the application of lambda a, with body lambda f, with body lambda x, with body the application of f to the application of the application of a to f, end application to x, end application, end application, end abstraction, end abstraction, end abstraction to lambda f, with body lambda x, with body x, end abstraction, end abstraction, end application. This reduces in one step to lambda f, with body lambda x, with body the application of f to the application of the application of lambda f, with body lambda x, with body x, end abstraction, end abstraction to f, end application to x, end application, end application, end abstraction, end abstraction, then in one step to lambda f, with body lambda x, with body the application of f to the application of lambda x, with body x, end abstraction to x, end application, end application, end abstraction, end abstraction, then in one step to lambda f, with body lambda x, with body the application of f to x, end application, end abstraction, end abstraction, syntactically identical to the Church numeral for one.

Means: the application of Successor to the Church numeral for zero, end application is syntactically identical to the application of lambda a, with body lambda f, with body lambda x, with body the application of f to the application of the application of a to f, end application to x, end application, end application, end abstraction, end abstraction, end abstraction to lambda f, with body lambda x, with body x, end abstraction, end abstraction, end application. This reduces in one step to lambda f, with body lambda x, with body the application of f to the application of the application of lambda f, with body lambda x, with body x, end abstraction, end abstraction to f, end application to x, end application, end application, end abstraction, end abstraction, then in one step to lambda f, with body lambda x, with body the application of f to the application of lambda x, with body x, end abstraction to x, end application, end application, end abstraction, end abstraction, then in one step to lambda f, with body lambda x, with body the application of f to x, end application, end abstraction, end abstraction, syntactically identical to the Church numeral for one.

1 occurrence in this chapter

Equation form expr-7ed5ff618d7df81c

⟨M,N⟩≡λf.fMN.\tuple{M,N} \ident \lambd[f][fMN].

Read as: the ordered pair with first component capital M, and second component capital N, end pair is syntactically identical to lambda f, with body the application of the application of f to capital M, end application to capital N, end application, end abstraction

Means: the ordered pair with first component capital M, and second component capital N, end pair is syntactically identical to lambda f, with body the application of the application of f to capital M, end application to capital N, end application, end abstraction

1 occurrence in this chapter

Equation form expr-7f024b2d7f1db4d4

n¯\num{n}

Read as: the Church numeral for n

Means: the Church numeral for n

2 occurrences in this chapter

Equation form expr-81351b457e719b1d

Or\fn{Or}

Read as: Or

Means: Or

1 occurrence in this chapter

Equation form expr-8254c329a92850f6

kk

Read as: k

Means: k

1 occurrence in this chapter

Equation form expr-837e308e5130032f

3¯\num{3}

Read as: the Church numeral for three

Means: the Church numeral for three

1 occurrence in this chapter

Equation form expr-83f81a2d3a3b24e0

Fn¯F \, \num n

Read as: the application of capital F to the Church numeral for n, end application

Means: the application of capital F to the Church numeral for n, end application

1 occurrence in this chapter

Equation form expr-8441f669e31640d0

YC≡λg.(λx.g(xx))(λx.g(xx)).Y_C \ident \lambd[g][(\lambd[x][g(xx)])(\lambd[x][g(xx)])].

Read as: capital Y subscript capital C is syntactically identical to lambda g, with body the application of lambda x, with body the application of g to the application of x to x, end application, end application, end abstraction to lambda x, with body the application of g to the application of x to x, end application, end application, end abstraction, end application, end abstraction

Means: capital Y subscript capital C is syntactically identical to lambda g, with body the application of lambda x, with body the application of g to the application of x to x, end application, end application, end abstraction to lambda x, with body the application of g to the application of x to x, end application, end application, end abstraction, end application, end abstraction

1 occurrence in this chapter

Equation form expr-898913c4326a0b49

fromChurch\fn{fromChurch}

Read as: From Church

Means: From Church

2 occurrences in this chapter

Equation form expr-8ad397891c5ed5a1

n¯\num n

Read as: the Church numeral for n

Means: the Church numeral for n

2 occurrences in this chapter

Equation form expr-8c2574892063f995

RR

Read as: the representing lambda term capital R

Means: the representing lambda term capital R

1 occurrence in this chapter

Equation form expr-8ce86a6ae65d3692

NN

Read as: capital N

Means: capital N

2 occurrences in this chapter

Equation form expr-8d733118b0ae3ff8

Add′\fn{Add}'

Read as: Add prime

Means: Add prime

1 occurrence in this chapter

Equation form expr-8f6170b68c913e60

Dn0⟨0¯,Fn¯⟩↠⟨0¯,h(n,0)¯⟩D_n^0 \tuple{\num{0}, F\, \num{n}} \red \tuple{\num{0}, \num{h(n, 0)}}

Read as: the result of iterating capital D subscript n zero times on the ordered pair with first component the Church numeral for zero, and second component the application of capital F to the Church numeral for n, end application, end pair, end iteration reduces to the ordered pair with first component the Church numeral for zero, and second component the Church numeral for h of n and zero, end pair

Means: the result of iterating capital D subscript n zero times on the ordered pair with first component the Church numeral for zero, and second component the application of capital F to the Church numeral for n, end application, end pair, end iteration reduces to the ordered pair with first component the Church numeral for zero, and second component the Church numeral for h of n and zero, end pair

1 occurrence in this chapter

Equation form expr-9155d40a7b7a127a

Fn¯F\, \num n

Read as: the application of capital F to the Church numeral for n, end application

Means: the application of capital F to the Church numeral for n, end application

1 occurrence in this chapter

Equation form expr-919d287f88a6b2ff

R⊆ℕnR \subseteq \Nat^n

Read as: capital R is a subset of the n tuples of natural numbers

Means: capital R is a subset of the n tuples of natural numbers

1 occurrence in this chapter

Equation form expr-927d37f267dcac72

λfx.x\lambd[fx][x]

Read as: lambda f then x, with body x, end abstraction

Means: lambda f then x, with body x, end abstraction

2 occurrences in this chapter

Equation form expr-93f09ee73e9abe97

(g(g(Yg)))N(g(g(Yg)))N

Read as: the application of the application of g to the application of g to the application of capital Y to g, end application, end application, end application to capital N, end application

Means: the application of the application of g to the application of g to the application of capital Y to g, end application, end application, end application to capital N, end application

1 occurrence in this chapter

Equation form expr-9661bf75db6a2bcf

⟨0¯,h(n,0)¯⟩\tuple{\num{0}, \num{h(n,0)}}

Read as: the ordered pair with first component the Church numeral for zero, and second component the Church numeral for h of n and zero, end pair

Means: the ordered pair with first component the Church numeral for zero, and second component the Church numeral for h of n and zero, end pair

1 occurrence in this chapter

Equation form expr-973c8320b3dd6fc4

Ckn¯≡(λx.k¯)n¯→k¯C_k \, \num n \ident (\lambd[x][\num{k}])\num n \redone \num{k}

Read as: the application of capital C subscript k to the Church numeral for n, end application is syntactically identical to the application of lambda x, with body the Church numeral for k, end abstraction to the Church numeral for n, end application, which reduces in one step to the Church numeral for k

Means: the application of capital C subscript k to the Church numeral for n, end application is syntactically identical to the application of lambda x, with body the Church numeral for k, end abstraction to the Church numeral for n, end application, which reduces in one step to the Church numeral for k

1 occurrence in this chapter

Equation form expr-982d20d1e491c9e1

f:ℕ→ℕf\colon \Nat \to \Nat

Read as: f from the natural numbers to the natural numbers

Means: f from the natural numbers to the natural numbers

2 occurrences in this chapter

Equation form expr-98f0455530b5b3d8

gk−1g_{k-1}

Read as: g subscript k minus one

Means: g subscript k minus one

1 occurrence in this chapter

Equation form expr-99688af5fa62bf90

λx.λy.y\lambd[x][\lambd[y][y]]

Read as: lambda x, with body lambda y, with body y, end abstraction, end abstraction

Means: lambda x, with body lambda y, with body y, end abstraction, end abstraction

1 occurrence in this chapter

Equation form expr-9c8b4c6fe53274f4

normalize(t)\fn{normalize}(t)

Read as: Normalize of t

Means: Normalize of t

1 occurrence in this chapter

Equation form expr-9ddfa415125373dc

f(n1,…,nk)f(n_1, \dots, n_k)

Read as: f of n subscript one through n subscript k

Means: f of n subscript one through n subscript k

2 occurrences in this chapter

Equation form expr-9f27f22c5eb4b279

true≡λx.λy.xfalse≡λx.λy.y\fn{true} & \ident \lambd[x][\lambd[y][x]]\\ \fn{false} & \ident \lambd[x][\lambd[y][y]]

Read as: True is syntactically identical to lambda x, with body lambda y, with body x, end abstraction, end abstraction. False is syntactically identical to lambda x, with body lambda y, with body y, end abstraction, end abstraction.

Means: True is syntactically identical to lambda x, with body lambda y, with body x, end abstraction, end abstraction. False is syntactically identical to lambda x, with body lambda y, with body y, end abstraction, end abstraction.

1 occurrence in this chapter

Equation form expr-a0ce237c6e3eed67

YCY_C

Read as: capital Y subscript capital C

Means: capital Y subscript capital C

1 occurrence in this chapter

Equation form expr-a1fce4363854ff88

yy

Read as: y

Means: y

8 occurrences in this chapter

Equation form expr-a2277e0b98ac28a5

g(x)g(x)

Read as: g of x

Means: g of x

1 occurrence in this chapter

Equation form expr-a25513c7e0f6eaa8

UU

Read as: capital U

Means: capital U

1 occurrence in this chapter

Equation form expr-a2bf86292ef9d747

Yg↠βg(Yg)Yg \bred g(Yg)

Read as: the application of capital Y to g, end application beta reduces to the application of g to the application of capital Y to g, end application, end application

Means: the application of capital Y to g, end application beta reduces to the application of g to the application of capital Y to g, end application, end application

1 occurrence in this chapter

Equation form expr-a3790cd28ac3b155

f(x→,y)f(\vec x, y)

Read as: f of the entries of the vector x, followed by y

Means: f of the entries of the vector x, followed by y

1 occurrence in this chapter

Equation form expr-a53a3d7051fc3402

toChurch(ni)\fn{toChurch}(n_i)

Read as: To Church of n subscript i

Means: To Church of n subscript i

1 occurrence in this chapter

Equation form expr-a8a24ca5755eaa27

f(x1,…,xn)f(x_1, \dots, x_n)

Read as: f of x subscript one through x subscript n

Means: f of x subscript one through x subscript n

1 occurrence in this chapter

Equation form expr-aa0f669ef6e981d2

n¯fx\num n\, f x

Read as: the application of the application of the Church numeral for n to f, end application to x, end application

Means: the application of the application of the Church numeral for n to f, end application to x, end application

1 occurrence in this chapter

Equation form expr-aa956277254bce94

g0,…,gk−1g_0, \dots, g_{k-1}

Read as: g subscript zero through g subscript k minus one

Means: g subscript zero through g subscript k minus one

1 occurrence in this chapter

Equation form expr-aaa9402664f1a41f

hh

Read as: h

Means: h

11 occurrences in this chapter

Equation form expr-aac9cfa1e2337865

⟨M,N⟩\tuple{M,N}

Read as: the ordered pair with first component capital M, and second component capital N, end pair

Means: the ordered pair with first component capital M, and second component capital N, end pair

1 occurrence in this chapter

Equation form expr-af401dbee4afc95b

Dn0⟨0¯,Fn¯⟩D_n^0 \tuple{\num{0}, F\, \num{n}}

Read as: the result of iterating capital D subscript n zero times on the ordered pair with first component the Church numeral for zero, and second component the application of capital F to the Church numeral for n, end application, end pair, end iteration

Means: the result of iterating capital D subscript n zero times on the ordered pair with first component the Church numeral for zero, and second component the application of capital F to the Church numeral for n, end application, end pair, end iteration

1 occurrence in this chapter

Equation form expr-af5b5886d350bce5

λfx.f(f(fx))\lambd[fx][f(f(f\,x))]

Read as: lambda f then x, with body the application of f to the application of f to the application of f to x, end application, end application, end application, end abstraction

Means: lambda f then x, with body the application of f to the application of f to the application of f to x, end application, end application, end application, end abstraction

1 occurrence in this chapter

Equation form expr-b0d6e31a1159a2cb

g(VV)g(VV)

Read as: the application of g to the application of capital V to capital V, end application, end application

Means: the application of g to the application of capital V to capital V, end application, end application

1 occurrence in this chapter

Equation form expr-b0fd41899402dde6

h(x1,…,xn,0)=f(x1,…,xn)h(x1,…,xn,y+1)=h(x1,…,xn,y,h(x1,…,xn,y)).h(x_1, \dots, x_n, 0) &= f(x_1, \dots, x_n)\\ h(x_1, \dots, x_n, y+1) & = h(x_1, \dots, x_n, y, h(x_1, \dots, x_n, y)).

Read as: h of x subscript one through x subscript n, followed by zero, equals f of x subscript one through x subscript n. h of x subscript one through x subscript n, followed by y plus one, equals h of x subscript one through x subscript n, followed by y and then h of x subscript one through x subscript n followed by y. End equations.

Means: h of x subscript one through x subscript n, followed by zero, equals f of x subscript one through x subscript n. h of x subscript one through x subscript n, followed by y plus one, equals h of x subscript one through x subscript n, followed by y and then h of x subscript one through x subscript n followed by y. End equations.

1 occurrence in this chapter

Equation form expr-b3f6ba5bad3f6071

n0n_0

Read as: n subscript zero

Means: n subscript zero

1 occurrence in this chapter

Equation form expr-b48f66241d74a302

Succy\fn{Succ}\, y

Read as: the application of Successor to y, end application

Means: the application of Successor to y, end application

1 occurrence in this chapter

Equation form expr-b5fd30809feccf8e

Dn≡D[n¯/x]D_n \ident \Subst{D}{\num{n}}{x}

Read as: capital D subscript n is syntactically identical to the result of substituting the Church numeral for n for free x in capital D, end substitution

Means: capital D subscript n is syntactically identical to the result of substituting the Church numeral for n for free x in capital D, end substitution

1 occurrence in this chapter

Equation form expr-b620f7fd0a05aeb7

0¯\num{0}

Read as: the Church numeral for zero

Means: the Church numeral for zero

2 occurrences in this chapter

Equation form expr-b8e2b244c77b7c22

λx.g(xx)\lambd[x][g(xx)]

Read as: lambda x, with body the application of g to the application of x to x, end application, end application, end abstraction

Means: lambda x, with body the application of g to the application of x to x, end application, end application, end abstraction

1 occurrence in this chapter

Equation form expr-b9711ee2915de9c0

add\Add

Read as: the addition function

Means: the addition function

1 occurrence in this chapter

Equation form expr-bb547d3afeec7211

Sub≡λab.bPreda.\fn{Sub} \ident \lambd[ab][b \fn{Pred}\, a].

Read as: Subtract is syntactically identical to lambda a then b, with body the application of the application of b to Predecessor, end application to a, end application, end abstraction

Means: Subtract is syntactically identical to lambda a then b, with body the application of the application of b to Predecessor, end application to a, end application, end abstraction

1 occurrence in this chapter

Equation form expr-bb69021ab191ecba

Yg≡(λux.x(uux))Ug↠(λx.x(UUx))g↠g(UUg)≡g(Yg).Y g &\ident (\lambd[ux][x(uux)])U\,g \\ &\red (\lambd[x][x(UUx)])g\\ & \red g(UUg) \ident g(Yg).

Read as: the application of capital Y to g, end application is syntactically identical to the application of the application of lambda u then x, with body the application of x to the application of the application of u to u, end application to x, end application, end application, end abstraction to capital U, end application to g, end application. This reduces to the application of lambda x, with body the application of x to the application of the application of capital U to capital U, end application to x, end application, end application, end abstraction to g, end application, which reduces to the application of g to the application of the application of capital U to capital U, end application to g, end application, end application, syntactically identical to the application of g to the application of capital Y to g, end application, end application.

Means: the application of capital Y to g, end application is syntactically identical to the application of the application of lambda u then x, with body the application of x to the application of the application of u to u, end application to x, end application, end application, end abstraction to capital U, end application to g, end application. This reduces to the application of lambda x, with body the application of x to the application of the application of capital U to capital U, end application to x, end application, end application, end abstraction to g, end application, which reduces to the application of g to the application of the application of capital U to capital U, end application to g, end application, end application, syntactically identical to the application of g to the application of capital Y to g, end application, end application.

1 occurrence in this chapter

Equation form expr-be4beea42f462725

Pred\fn{Pred}

Read as: Predecessor

Means: Predecessor

2 occurrences in this chapter

Equation form expr-c2c5eeeab86b1b20

g(Yg)g(Yg)

Read as: the application of g to the application of capital Y to g, end application, end application

Means: the application of g to the application of capital Y to g, end application, end application

2 occurrences in this chapter

Equation form expr-c511a3b8638ce823

Fn0¯n1¯…nk−1¯F \, \num{n_0} \, \num{n_1} \dots \num{n_{k-1}}

Read as: capital F successively applied to the Church numerals for n subscript zero through n subscript k minus one, in that order

Means: capital F successively applied to the Church numerals for n subscript zero through n subscript k minus one, in that order

1 occurrence in this chapter

Equation form expr-c677c0cf951a25ee

trueMN\fn{true}\, M N

Read as: the application of the application of True to capital M, end application to capital N, end application

Means: the application of the application of True to capital M, end application to capital N, end application

1 occurrence in this chapter

Equation form expr-c67c51696170f090

Pair≡λmn.λf.fmn\fn{Pair} \ident \lambd[mn][\lambd[f][fmn]]

Read as: Pair is syntactically identical to lambda m then n, with body lambda f, with body the application of the application of f to m, end application to n, end application, end abstraction, end abstraction

Means: Pair is syntactically identical to lambda m then n, with body lambda f, with body the application of the application of f to m, end application to n, end application, end abstraction, end abstraction

1 occurrence in this chapter

Equation form expr-c802c05458a6a818

Exp′≡λbe.e(Multb)1¯.\fn{Exp}' \ident \lambd[be][e (\fn{Mult}\, b) \num{1}].

Read as: Exponentiate prime is syntactically identical to lambda b then e, with body the application of the application of e to the application of Multiply to b, end application, end application to the Church numeral for one, end application, end abstraction

Means: Exponentiate prime is syntactically identical to lambda b then e, with body the application of the application of e to the application of Multiply to b, end application, end application to the Church numeral for one, end application, end abstraction

1 occurrence in this chapter

Equation form expr-c972eac8cc96ee71

Fn1¯…nk¯F \num{n_1}\dots\num{n_k}

Read as: capital F successively applied to the Church numerals for n subscript one through n subscript k, in that order

Means: capital F successively applied to the Church numerals for n subscript one through n subscript k, in that order

2 occurrences in this chapter

Equation form expr-c99c9b4e359a1216

GxG x

Read as: the application of capital G to x, end application

Means: the application of capital G to x, end application

1 occurrence in this chapter

Equation form expr-c9ab1bcbdc746fc5

Mult≡λab.a(Adda)0\fn{Mult} \ident \lambd[ab][a (\fn{Add}\, a) 0]

Read as: Multiply is syntactically identical to lambda a then b, with body the application of the application of a to the application of Add to a, end application, end application to zero, end application, end abstraction

Means: Multiply is syntactically identical to lambda a then b, with body the application of the application of a to the application of Add to a, end application, end application to zero, end application, end abstraction

1 occurrence in this chapter

Equation form expr-c9d0558c7e3f86f4

Fst\fn{Fst}

Read as: First

Means: First

1 occurrence in this chapter

Equation form expr-ca978112ca1bbdca

aa

Read as: a

Means: a

1 occurrence in this chapter

Equation form expr-cd0aa9856147b6c5

gg

Read as: g

Means: g

13 occurrences in this chapter

Equation form expr-cd82e83b1115adc2

Y≡UUY \ident UU

Read as: capital Y is syntactically identical to the application of capital U to capital U, end application

Means: capital Y is syntactically identical to the application of capital U to capital U, end application

1 occurrence in this chapter

Equation form expr-cfa522140d47a072

(g(Yg))N(g(Yg))N

Read as: the application of the application of g to the application of capital Y to g, end application, end application to capital N, end application

Means: the application of the application of g to the application of capital Y to g, end application, end application to capital N, end application

1 occurrence in this chapter

Equation form expr-d09cf35692bbb2b4

Not≡λx.xfalsetrueAnd≡λx.λy.xyfalse\fn{Not} & \ident \lambd[x][x\, \fn{false}\, \fn{true}]\\ \fn{And} & \ident \lambd[x][\lambd[y][xy \,\fn{false}]]

Read as: Not is syntactically identical to lambda x, with body the application of the application of x to False, end application to True, end application, end abstraction. And is syntactically identical to lambda x, with body lambda y, with body the application of the application of x to y, end application to False, end application, end abstraction, end abstraction.

Means: Not is syntactically identical to lambda x, with body the application of the application of x to False, end application to True, end application, end abstraction. And is syntactically identical to lambda x, with body lambda y, with body the application of the application of x to y, end application to False, end application, end abstraction, end abstraction.

1 occurrence in this chapter

Equation form expr-d25d2f2c6168e7eb

Mult≡λab.λf.a(bf).\fn{Mult} \ident \lambd[ab][\lambd[f][a (b f)]].

Read as: Multiply is syntactically identical to lambda a then b, with body lambda f, with body the application of a to the application of b to f, end application, end application, end abstraction, end abstraction

Means: Multiply is syntactically identical to lambda a then b, with body lambda f, with body the application of a to the application of b to f, end application, end application, end abstraction, end abstraction

1 occurrence in this chapter

Equation form expr-d3482b3a268726b8

n+m¯\num{n+m}

Read as: the Church numeral for n plus m

Means: the Church numeral for n plus m

1 occurrence in this chapter

Equation form expr-d35f51c70f9cbfbe

Search\fn{Search}

Read as: Search

Means: Search

1 occurrence in this chapter

Equation form expr-d3a14e4b9aa5d562

Exp≡λbe.eb.\fn{Exp} \ident \lambd[be][e b].

Read as: Exponentiate is syntactically identical to lambda b then e, with body the application of e to b, end application, end abstraction

Means: Exponentiate is syntactically identical to lambda b then e, with body the application of e to b, end application, end abstraction

1 occurrence in this chapter

Equation form expr-d429d8bf14e16a51

YFac′Y\, \fn{Fac}'

Read as: the application of capital Y to Factorial prime, end application

Means: the application of capital Y to Factorial prime, end application

1 occurrence in this chapter

Equation form expr-dbbc007a11153411

⟨0¯,Fn¯⟩\tuple{\num{0}, F\, \num{n}}

Read as: the ordered pair with first component the Church numeral for zero, and second component the application of capital F to the Church numeral for n, end application, end pair

Means: the ordered pair with first component the Church numeral for zero, and second component the application of capital F to the Church numeral for n, end application, end pair

1 occurrence in this chapter

Equation form expr-dc9b0b3b2175345a

falseMN\fn{false}\, M N

Read as: the application of the application of False to capital M, end application to capital N, end application

Means: the application of the application of False to capital M, end application to capital N, end application

1 occurrence in this chapter

Equation form expr-de5a6f78116eca62

VV

Read as: capital V

Means: capital V

1 occurrence in this chapter

Equation form expr-dee4e23ed8ed88a4

Fst≡λp.p(λmn.m)Snd≡λp.p(λmn.n)\fn{Fst} & \ident \lambd[p][p(\lambd[mn][m])]\\ \fn{Snd} & \ident \lambd[p][p(\lambd[mn][n])]

Read as: First is syntactically identical to lambda p, with body the application of p to lambda m then n, with body m, end abstraction, end application, end abstraction. Second is syntactically identical to lambda p, with body the application of p to lambda m then n, with body n, end abstraction, end application, end abstraction.

Means: First is syntactically identical to lambda p, with body the application of p to lambda m then n, with body m, end abstraction, end application, end abstraction. Second is syntactically identical to lambda p, with body the application of p to lambda m then n, with body n, end abstraction, end application, end abstraction.

1 occurrence in this chapter

Equation form expr-df9e0b7f67e3f3ee

Zero≡λa.λfx.xSucc≡λa.λfx.f(afx)Projin≡λx0…xn−1.xi\fn{Zero} & \ident \lambd[a][\lambd[fx][x]]\\ \fn{Succ} & \ident \lambd[a][\lambd[fx][f (a f x)]] \\ \fn{Proj}^n_i & \ident \lambd[x_0\dots x_{n-1}][x_i]

Read as: Zero is syntactically identical to lambda a, with body lambda f then x, with body x, end abstraction, end abstraction. Successor is syntactically identical to lambda a, with body lambda f then x, with body the application of f to the application of the application of a to f, end application to x, end application, end application, end abstraction, end abstraction. Projection superscript n subscript i is syntactically identical to lambda x subscript zero through x subscript n minus one, with body x subscript i, end abstraction.

Means: Zero is syntactically identical to lambda a, with body lambda f then x, with body x, end abstraction, end abstraction. Successor is syntactically identical to lambda a, with body lambda f then x, with body the application of f to the application of the application of a to f, end application to x, end application, end application, end abstraction, end abstraction. Projection superscript n subscript i is syntactically identical to lambda x subscript zero through x subscript n minus one, with body x subscript i, end abstraction.

1 occurrence in this chapter

Equation form expr-e0d406650afce565

Fac≡λn.IsZeron1¯(Multn(Fac(Predn)))\fn{Fac} \ident \lambd[n][\fn{IsZero}\, n\, \num 1 (\fn{Mult}\, n (\fn{Fac}(\fn{Pred} \, n)))]

Read as: Factorial is syntactically identical to lambda n, with body the application of the application of the application of Is Zero to n, end application to the Church numeral for one, end application to the application of the application of Multiply to n, end application to the application of Factorial to the application of Predecessor to n, end application, end application, end application, end application, end abstraction

Means: Factorial is syntactically identical to lambda n, with body the application of the application of the application of Is Zero to n, end application to the Church numeral for one, end application to the application of the application of Multiply to n, end application to the application of Factorial to the application of Predecessor to n, end application, end application, end application, end application, end abstraction

1 occurrence in this chapter

Equation form expr-e3b98a4da31a127d

tt

Read as: t

Means: t

1 occurrence in this chapter

Equation form expr-e4639072bcb2aaeb

nk−1n_{k-1}

Read as: n subscript k minus one

Means: n subscript k minus one

1 occurrence in this chapter

Equation form expr-e51d5dc07716fb99

fx→yf\, \vec x\, y

Read as: f successively applied to the entries of vector x, followed by y

Means: f successively applied to the entries of vector x, followed by y

1 occurrence in this chapter

Equation form expr-e677449e14a68e98

Hn¯m¯↠h(n,m)¯H\,\num{n}\,\num{m} \red \num{h(n,m)}

Read as: the application of the application of capital H to the Church numeral for n, end application to the Church numeral for m, end application reduces to the Church numeral for h of n and m

Means: the application of the application of capital H to the Church numeral for n, end application to the Church numeral for m, end application reduces to the Church numeral for h of n and m

1 occurrence in this chapter

Equation form expr-e9cfd958aef9dcf9

λx.F(Gx)\lambd[x][F (G x)]

Read as: lambda x, with body the application of capital F to the application of capital G to x, end application, end application, end abstraction

Means: lambda x, with body the application of capital F to the application of capital G to x, end application, end application, end abstraction

1 occurrence in this chapter

Equation form expr-ea4e4dd4a814275c

Hn¯m¯≡λx.λy.Snd(y(λp.⟨Succ(Fstp),(Gx(Fstp)(Sndp))⟩)⟨0¯,Fx⟩)n¯m¯↠Snd(m¯(λp.⟨Succ(Fstp),(Gn¯(Fstp)(Sndp))⟩)⏟Dn⟨0¯,Fn¯⟩)≡Snd(m¯Dn⟨0¯,Fn¯⟩)↠Snd(Dnm⟨0¯,Fn¯⟩)↠Snd⟨m¯,h(n,m)¯⟩↠h(n,m)¯.H\,\num n\,\num m &\ident \lambd[x][\lambd[y][\fn{Snd} (y (\lambd[p].\tuple{\fn{Succ} (\fn{Fst}\, p), (G\, x\, (\fn{Fst}\, p)\, (\fn{Snd}\, p))}) \tuple{\num{0}, F x})]]\\ & \qquad\,\num n\, \num m\\ & \red \fn{Snd} (\num m \, \underbrace{(\lambd[p].\tuple{\fn{Succ} (\fn{Fst}\, p), (G \,\num n\, (\fn{Fst}\, p) (\fn{Snd}\, p))})}_{D_n} \tuple{\num{0}, F \num n})\\ & \ident \fn{Snd} (\num m \, D_n\, \tuple{\num{0}, F \num n})\\ & \red \fn{Snd} \,(D_n^m \tuple{\num{0}, F \num n})\\ & \red \fn{Snd} \,\tuple{\num{m}, \num{h(n, m)}} \\ & \red \num{h(n,m)}.

Read as: the application of the application of capital H to the Church numeral for n, end application to the Church numeral for m, end application is syntactically identical to lambda x, with body lambda y, with body the application of the application of the application of Second to the application of the application of y to lambda p, with body the ordered pair with first component the application of Successor to the application of First to p, end application, end application, and second component the application of the application of the application of capital G to x, end application to the application of First to p, end application, end application to the application of Second to p, end application, end application, end pair, end abstraction, end application to the ordered pair with first component the Church numeral for zero, and second component the application of capital F to x, end application, end pair, end application, end application to the Church numeral for n, end application to the Church numeral for m, end application, end abstraction, end abstraction. This reduces to the application of Second to the application of the application of the Church numeral for m to lambda p, with body the ordered pair with first component the application of Successor to the application of First to p, end application, end application, and second component the application of the application of the application of capital G to the Church numeral for n, end application to the application of First to p, end application, end application to the application of Second to p, end application, end application, end pair, end abstraction, end application to the ordered pair with first component the Church numeral for zero, and second component the application of capital F to the Church numeral for n, end application, end pair, end application, end application. The displayed underbrace names this step abstraction capital D subscript n. The preceding expression is syntactically identical to the application of Second to the application of the application of the Church numeral for m to capital D subscript n, end application to the ordered pair with first component the Church numeral for zero, and second component the application of capital F to the Church numeral for n, end application, end pair, end application, end application, which reduces to the application of Second to the result of iterating capital D subscript n m times on the ordered pair with first component the Church numeral for zero, and second component the application of capital F to the Church numeral for n, end application, end pair, end iteration, end application, which reduces to the application of Second to the ordered pair with first component the Church numeral for m, and second component the Church numeral for h of n and m, end pair, end application, which reduces to the Church numeral for h of n and m.

Means: the application of the application of capital H to the Church numeral for n, end application to the Church numeral for m, end application is syntactically identical to lambda x, with body lambda y, with body the application of the application of the application of Second to the application of the application of y to lambda p, with body the ordered pair with first component the application of Successor to the application of First to p, end application, end application, and second component the application of the application of the application of capital G to x, end application to the application of First to p, end application, end application to the application of Second to p, end application, end application, end pair, end abstraction, end application to the ordered pair with first component the Church numeral for zero, and second component the application of capital F to x, end application, end pair, end application, end application to the Church numeral for n, end application to the Church numeral for m, end application, end abstraction, end abstraction. This reduces to the application of Second to the application of the application of the Church numeral for m to lambda p, with body the ordered pair with first component the application of Successor to the application of First to p, end application, end application, and second component the application of the application of the application of capital G to the Church numeral for n, end application to the application of First to p, end application, end application to the application of Second to p, end application, end application, end pair, end abstraction, end application to the ordered pair with first component the Church numeral for zero, and second component the application of capital F to the Church numeral for n, end application, end pair, end application, end application. The displayed underbrace names this step abstraction capital D subscript n. The preceding expression is syntactically identical to the application of Second to the application of the application of the Church numeral for m to capital D subscript n, end application to the ordered pair with first component the Church numeral for zero, and second component the application of capital F to the Church numeral for n, end application, end pair, end application, end application, which reduces to the application of Second to the result of iterating capital D subscript n m times on the ordered pair with first component the Church numeral for zero, and second component the application of capital F to the Church numeral for n, end application, end pair, end iteration, end application, which reduces to the application of Second to the ordered pair with first component the Church numeral for m, and second component the Church numeral for h of n and m, end pair, end application, which reduces to the Church numeral for h of n and m.

1 occurrence in this chapter

Equation form expr-ebd225f165c0ba97

λx.x\lambd[x][x]

Read as: lambda x, with body x, end abstraction

Means: lambda x, with body x, end abstraction

1 occurrence in this chapter

Equation form expr-ecb6f9a9e83f3652

Xor\fn{Xor}

Read as: Exclusive Or

Means: Exclusive Or

1 occurrence in this chapter

Equation form expr-f23ca6dac7289a4f

true\fn{true}

Read as: True

Means: True

9 occurrences in this chapter

Equation form expr-f38618c24799a1c3

⟨0,0⟩\tuple{0,0}

Read as: the ordered pair with first component zero, and second component zero, end pair

Means: the ordered pair with first component zero, and second component zero, end pair

2 occurrences in this chapter

Equation form expr-f3f3804480e8551a

β\beta

Read as: beta

Means: beta

1 occurrence in this chapter

Equation form expr-f67ab10ad4e4c531

FF

Read as: capital F

Means: capital F

12 occurrences in this chapter

Equation form expr-f7a8152d221b3f10

YC≡λg.VVY_C \ident \lambd[g][VV]

Read as: capital Y subscript capital C is syntactically identical to lambda g, with body the application of capital V to capital V, end application, end abstraction

Means: capital Y subscript capital C is syntactically identical to lambda g, with body the application of capital V to capital V, end application, end abstraction

1 occurrence in this chapter

Equation form expr-f7f902bb1aa5eac7

(λux.x(uux))(\lambd[ux][x(uux)])

Read as: lambda u then x, with body the application of x to the application of the application of u to u, end application to x, end application, end application, end abstraction

Means: lambda u then x, with body the application of x to the application of the application of u to u, end application to x, end application, end application, end abstraction

1 occurrence in this chapter

Equation form expr-fc314b71d7a909f5

n+2n+2

Read as: n plus two

Means: n plus two

1 occurrence in this chapter

Equation form expr-fd5a7ff1d00de312

n·mn\cdot m

Read as: n times m

Means: n times m

1 occurrence in this chapter

Equation form expr-fe7ef25f6b14a2f9

fef^e

Read as: f iterated e times

Means: f iterated e times

1 occurrence in this chapter

Definition of Church numerals

The Church numeral for n is the abstraction binding f and then x whose body iterates f on x n times. The definition gives zero as the selector returning x and three as three nested applications of f. Numerals are lambda terms, distinct from the natural numbers they represent.

Source

Definition of lambda definability for a partial function

For every ordered list of k natural-number arguments, the representing term capital F applied to their Church numerals must reduce to the Church numeral for the function value when it is defined. When the value is undefined, that application must have no normal form. Both clauses and their argument order are part of the definition.

Source

Successor is lambda definable

The proposition states that the natural-number successor function is lambda definable. The following proof constructs a term and unfolds its application to a Church numeral.

Source

Successor construction and reduction

The display first gives the Successor abstraction in compressed and fully nested binder notation. It then applies that abstraction to the Church numeral for n and relates the resulting body to one more iteration of f. All intermediate terms and the source's one-step arrows are retained; a separate source note discloses that some printed one-step claims compress multiple beta contractions.

Source

Example computing the successor of zero

The example expands the complete Successor term and the complete Church-zero term, then follows three displayed single-step reductions to the Church-one term. Each inner abstraction retains its binder and body scope.

Source

Expanded successor-of-zero reduction chain

Start with Successor applied to Church zero. The first contraction substitutes the Church-zero abstraction for a; the next contracts its application to f; the final contraction yields the abstraction binding f then x with body f applied to x. The source identifies that endpoint with Church one.

Source

Exercise on an alternative successor term

Explain why Successor prime, which binds n then f then x and applies n first to f and then to f applied to x, lambda defines successor. The exercise remains unsolved.

Source

Alternative successor term in the exercise

Successor prime binds n outside the abstractions binding f and x. Its body applies n to f and then to the grouped argument f applied to x. This is the term to be examined, not a supplied solution.

Source

Addition is lambda definable

The proposition states that the natural-number addition function is lambda definable. Two representing terms and their source calculations follow.

Source

Two addition terms and their reductions

The first term combines the iteration represented by b with that represented by a. The alternative term applies a to Successor and b. The display follows both Church-numeral calculations, retaining each intermediate expression and each printed reduction arrow. Some printed one-step arrows compress multiple beta contractions; this source notation is separately disclosed, not silently replaced.

Source

Multiplication is lambda definable

The displayed term binds a, b, f, and x in that order and applies a to the grouped application of b to f, then to x. The proof interprets this as n iterations of an m-fold iterator, giving n times m applications of f.

Source

Exercise on an alternative multiplication term

Explain why the printed Multiply-prime term works. The source term binds a and b but uses a twice and never uses b. This discrepancy is disclosed separately. The exercise is preserved unsolved, without replacing it by a corrected term or a proof.

Source

Definition of an encoded pair

The ordered pair of capital M and capital N is the lambda abstraction binding f whose body applies f to capital M and then capital N. The first and second component positions are distinct and ordered.

Source

First and second component accessors

First binds p and applies p to the two-argument selector returning m. Second binds p and applies p to the two-argument selector returning n. The definitions precede an exercise asking why these access functions work.

Source

Exercise on pair access functions

Explain why the given First and Second access functions work. No verification or missing proof is supplied for the exercise.

Source

Encoded truth values

True is the abstraction binding x and then y whose body is x. False binds x and then y whose body is y. They are ordered selectors; they do not interchange the first and second arguments.

Source

Definition of a lambda-definable relation

A representing term must beta reduce to True when the relation holds and to False otherwise, on the corresponding Church-numeral inputs. The source calls the relation n-ary but indexes the displayed arguments through k; that mismatch remains disclosed and is not silently reconciled.

Source

Two cases for a relation's representing term

The first row gives reduction to True whenever the relation holds of the listed arguments. The second gives reduction to False otherwise. These are conditional alternatives with the same ordered input sequence, not successive stages of a single reduction.

Source

Definitions of encoded negation and conjunction

Not applies its argument x to False and then True. And binds x then y and applies x to y and then False. The accompanying explanation assumes that the arguments are encoded truth values; it makes no claim that arbitrary lambda terms behave as truth values.

Source

Exercise defining disjunction and exclusive disjunction

Define Or and Exclusive Or using the given lambda-term encoding of truth values. Both requested definitions remain unsupplied; the exercise is not solved.

Source

Basic primitive recursive functions are lambda definable

The lemma asserts lambda definability of the zero function, successor, and every projection of arity n with index i. The following display gives the representing terms.

Source

Terms for zero, successor, and projections

Zero ignores its argument a and returns the Church-zero abstraction. Successor adds one application of f. Projection binds x subscript zero through x subscript n minus one and returns x subscript i. Each name and binder range remains distinct.

Source

Closure of lambda-definable total functions under composition

The source assumes a k-ary function f and n-ary component functions, represented by capital F and the capital G terms, and asserts closure under composition. Its list ends with capital G subscript k and its conclusion names capital H rather than h. The following formula uses capital G through subscript k minus one. These source mismatches are disclosed without rewriting the lemma.

Source

Exercise verifying the composition term

Complete the proof of the composition lemma by showing that capital H applied to the input Church numerals reduces to the Church numeral for the value of h. The source leaves this verification as an exercise, and it remains unsolved.

Source

Closure under primitive recursion

If an n-ary f and an n plus two arity g are lambda definable, the source claims that the function h obtained by primitive recursion from them is lambda definable. The proof treats one additional argument using a pair containing the iteration counter and the current value. Printed h versus g inconsistencies remain separately disclosed.

Source

Source primitive-recursion equations

The first equation sets h at final argument zero equal to f of the preceding arguments. The next equation prints h, not g, as the outer function on its right side, with one extra argument. The exact equation is retained; a source note relates this discrepancy to the surrounding lemma and later calculation without supplying a replacement proof.

Source

Pair-iteration term for primitive recursion

Capital H binds x then y, iterates capital D from the pair consisting of Church zero and capital F applied to x, and returns the second component. Capital D maps p to the pair of the successor of its first component and capital G applied to x and both components of p. The free x in the displayed abbreviation for capital D is retained.

Source

Induction step for the iteration-state pair

The chain expands m plus one iterations into one application of capital D subscript n after m iterations. The induction hypothesis gives the pair for m. Expanding the step abstraction and applying the accessors yields the pair of Church m plus one and the Church numeral for g of n, m, and h of n and m. The surrounding source then uses the primitive-recursion equation for the endpoint.

Source

Final primitive-recursion reduction

The calculation expands capital H on Church n and Church m, identifies the step abstraction by the underbrace capital D subscript n, converts the Church-m iteration to m repeated steps, applies the established pair invariant, and returns its second component. The first right-hand side lacks enclosing parentheses around the abstraction; its printed scope and the resulting mismatch with the next row are preserved with a source note. The final source term is the Church numeral for h of n and m.

Source

Every primitive recursive function is lambda definable

The source combines the basic-function lemma with the composition and primitive-recursion closure lemmas. All three dependency references are retained. Earlier source caveats remain available rather than being hidden by this conclusion.

Source

Unfolding the attempted recursive factorial definition

The display replaces a recursive occurrence of Factorial by another copy of its proposed defining expression, leaving Factorial in the result. Under the source's widest-scope convention, the outer lambda n binds the entire continued expression, including the multiplication factor on the following display row. Closing a TeX macro argument does not introduce a mathematical parenthesis.

Source

Definition of Turing's fixpoint combinator

Capital Y is the application of the abstraction binding u then x with body x applied to u applied to u then x, to a second copy of the same abstraction. The term is due to Alan Turing, as the later source attribution states.

Source

Turing combinator produces a fixpoint

For any term g, capital Y applied to g reduces to g applied to capital Y applied to g. The source concludes that capital Y applied to g is a fixpoint of g, using beta equivalence.

Source

Reduction proving the Turing fixpoint property

Capital U abbreviates the repeated abstraction. The calculation contracts the applications in capital Y applied to g until it reaches g applied to capital U applied to capital U then g, which is syntactically identical to g applied to capital Y applied to g.

Source

Continuing a fixpoint reduction indefinitely

Each displayed row adds one outer application of g around capital Y applied to g. The ellipsis indicates that this expansion continues. The following prose explicitly permits a different reduction sequence to terminate in a normal form.

Source

Factorial example using a fixpoint

The source defines Factorial using capital Y and Factorial prime, unfolds the applications on Church three, two, and one, and handles Church zero using Is Zero. The chain ends with nested multiplication of Church three, two, one, and one. No further arithmetic result is added beyond the source display.

Source

Turning a recursive equation into a fixpoint term

The display starts from the recursive beta equation for g on x subscript one through x subscript n. It defines capital G using capital Y and abstractions binding g and the x arguments, then unfolds that term and substitutes capital G for free g in capital N. One unparenthesized right-hand abstraction extends over the following factor under the source's widest-scope convention; that source mismatch is preserved and disclosed. All subsequent parenthesized applications, beta-equivalence signs, reduction directions, and substitution binders are retained.

Source

Common reduct for Church's fixpoint combinator

Capital V abbreviates lambda x with body g applied to x applied to x. Capital Y subscript capital C applied to g and g applied to that term both reduce to g applied to capital V applied to itself. The common reduct supports beta equivalence, not a claimed forward reduction from one of those endpoints to the other.

Source

Closure under regular minimization

For a regular lambda-definable f, the lemma asserts lambda definability of the function giving the least y at which f on the fixed preceding arguments equals zero. The source names that function g in the statement and h in the proof; this difference is disclosed.

Source

Source search term for minimization

Search binds g, then f, the vector x arguments, and y. Its body tests f on those arguments with Is Zero, returning y in one branch and applying g to the vector x arguments and Successor of y in the other. The recursive branch as printed omits f and has an unmatched opening parenthesis. These source defects are preserved and disclosed, not silently repaired.

Source

Claimed search reductions and termination

The source claims that the fixed-point search on m returns Church m if the tested value is zero, or otherwise repeats the search at Church m plus one. Regularity is then invoked to obtain a final zero and the Church numeral for h. The two branches are alternatives, not consecutive reduction steps. The preceding source search-definition caveat remains in effect.

Source

Every general recursive function is lambda definable

The proof cites lambda definability of basic functions and closure under composition, primitive recursion, and regular minimization. Each of the four source references is retained.

Source

Partial recursive functions are lambda definable

The theorem is recorded without proof. The preceding text explains why naive composition may discard a non-normalizing argument and therefore does not automatically represent undefinedness correctly. This edition does not supply the more complicated construction omitted by the source.

Source

Lambda-definable partial functions are partial recursive

The source sketches a computation using Gödel numbers of lambda terms: encode the input Church numerals, form the code of their application to capital F, partially normalize that code, then decode the resulting Church numeral. Undefined values correspond to applications having no normal form. The source supplies a proof sketch, not complete definitions of the coding and normalization functions.

Source

Cross-reference reference-000900

the lemma on closure under composition

Source occurrence

Cross-reference reference-000901

the lemma on closure under composition

Source occurrence

Cross-reference reference-000902

the lemma on lambda definability of the basic functions

Source occurrence

Cross-reference reference-000903

the lemma on closure under composition

Source occurrence

Cross-reference reference-000904

the lemma on closure under primitive recursion

Source occurrence

Cross-reference reference-000905

the definition of Turing's fixpoint combinator

Source occurrence

Cross-reference reference-000906

the lemma on lambda definability of the basic functions

Source occurrence

Cross-reference reference-000907

the lemma on closure under composition

Source occurrence

Cross-reference reference-000908

the lemma on closure under primitive recursion

Source occurrence

Cross-reference reference-000909

the lemma on closure under regular minimization

Source occurrence

Source disclosures