Lambda calculus

Introduction to Lambda Calculus

Equation form expr-02698ee916e95e18

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

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

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

1 occurrence in this chapter

Equation form expr-057527be7b514060

⟨n+1¯,H(n¯,F(n¯))⟩\tuple{\num{n+1}, H(\num{n}, F(\num{n}))}

Read as: the ordered pair whose first component is the Church numeral for n plus one, and whose second component is capital H applied to the Church numeral for n and then capital F applied to that numeral

Means: the ordered pair whose first component is the Church numeral for n plus one, and whose second component is capital H applied to the Church numeral for n and then capital F applied to that numeral

1 occurrence in this chapter

Equation form expr-06d646c0dbd15efb

⟨n+1¯,F(n+1¯)⟩\tuple{\num{n+1}, F(\num{n+1})}

Read as: the ordered pair of the Church numeral for n plus one and capital F applied to that numeral

Means: the ordered pair of the Church numeral for n plus one and capital F applied to that numeral

1 occurrence in this chapter

Equation form expr-08a31aaffef905c3

xnx_n

Read as: x subscript n

Means: x subscript n

1 occurrence in this chapter

Equation form expr-08c6aa8d5824f2de

succ\Succ

Read as: Successor

Means: Successor

2 occurrences in this chapter

Equation form expr-08dacf0f9d78188a

λ\lambd

Read as: lambda

Means: lambda

9 occurrences in this chapter

Equation form expr-08f271887ce94707

MM

Read as: capital M

Means: capital M

19 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-0abda97defb2f090

K(y)=λx.y.K(y) = \lambd[x][y].

Read as: capital K applied to y equals lambda x, with body y

Means: capital K applied to y equals lambda x, with body y

1 occurrence in this chapter

Equation form expr-0b33598471fdb4d5

F(u)=(u(T,⟨0¯,G⟩))1.F(u) = (u(T,\tuple{\num 0, G}))_1.

Read as: capital F applied to u equals the second component of the result of applying u first to capital T and then to the ordered pair of the Church numeral zero and capital G

Means: capital F applied to u equals the second component of the result of applying u first to capital T and then to the ordered pair of the Church numeral zero and capital G

1 occurrence in this chapter

Equation form expr-0efa22ea8f7ba6a7

F(0¯)≡GF(n+1¯)≡H(n¯,F(n¯))F(\num{0}) & \equiv G \\ F(\num{n+1}) & \equiv H(\num{n}, F(\num{n}))

Read as: capital F applied to the Church numeral zero is beta equivalent to capital G. Capital F applied to the Church numeral for n plus one is beta equivalent to capital H applied to the Church numeral for n and then capital F applied to that numeral

Means: capital F applied to the Church numeral zero is beta equivalent to capital G. Capital F applied to the Church numeral for n plus one is beta equivalent to capital H applied to the Church numeral for n and then capital F applied to that numeral

1 occurrence in this chapter

Equation form expr-10457071a295e5df

P(1¯)P(\num 1)

Read as: capital P applied to the Church numeral one

Means: capital P applied to the Church numeral one

1 occurrence in this chapter

Equation form expr-14fcb4e1ccaa4f01

M(x,y,z,w)M(x,y,z,w)

Read as: capital M, open parenthesis, x comma y comma z comma w, close parenthesis

Means: capital M, open parenthesis, x comma y comma z comma w, close parenthesis

1 occurrence in this chapter

Equation form expr-15a5f20420b60622

f(x)=x+3f(x) = x + 3

Read as: f of x equals x plus three

Means: f of x equals x plus three

1 occurrence in this chapter

Equation form expr-17353f1e3ded0f24

fx(y)f_x(y)

Read as: f subscript x applied to y

Means: f subscript x applied to y

1 occurrence in this chapter

Equation form expr-187ed3e0ef02ce2f

F(m¯,n¯)F(\num{m}, \num{n})

Read as: capital F applied first to the Church numeral for m, then to the Church numeral for n

Means: capital F applied first to the Church numeral for m, then to the Church numeral for n

2 occurrences in this chapter

Equation form expr-18f5384d58bcb1bb

YY

Read as: capital Y

Means: capital Y

4 occurrences in this chapter

Equation form expr-1b16b1df538ba12d

nn

Read as: n

Means: n

13 occurrences in this chapter

Equation form expr-1cb0dd24eeda5f8a

(P)1(P)_1

Read as: the second component of the pair represented by capital P

Means: the second component of the pair represented by capital P

1 occurrence in this chapter

Equation form expr-1f689e1f18761928

λx1.λx2.…λxn.N\lambd[x_1][\lambd[x_2][\ldots\lambd[x_n][N]]]

Read as: successive lambda abstractions binding x subscript one, x subscript two, through x subscript n, with innermost body capital N

Means: successive lambda abstractions binding x subscript one, x subscript two, through x subscript n, with innermost body capital N

1 occurrence in this chapter

Equation form expr-20834c302cbbb686

H(n¯)≡D(n¯,H(S(n¯)),F(x,n¯)).H(\num{n}) \equiv D(\num{n}, H(S(\num{n})), F(x, \num{n})).

Read as: capital H applied to the Church numeral for n is beta equivalent to capital D applied to that numeral, capital H applied to the result of applying capital S to that numeral, and capital F applied to x and that numeral, in that order

Means: capital H applied to the Church numeral for n is beta equivalent to capital D applied to that numeral, capital H applied to the result of applying capital S to that numeral, and capital F applied to x and that numeral, in that order

1 occurrence in this chapter

Equation form expr-20ae96ce3f15aa1e

P(0¯)P(\num 0)

Read as: capital P applied to the Church numeral zero

Means: capital P applied to the Church numeral zero

1 occurrence in this chapter

Equation form expr-20fa5e2300aaaa73

K(M)K(M)

Read as: capital K applied to capital M

Means: capital K applied to capital M

1 occurrence in this chapter

Equation form expr-21ff5c658a6fff1a

λx.(x+3)\lambd[x][(x + 3)]

Read as: lambda x, with body x plus three

Means: lambda x, with body x plus three

1 occurrence in this chapter

Equation form expr-22d49beaad9e2623

ReducesToInOneStep\fn{ReducesToInOneStep}

Read as: Reduces To In One Step

Means: Reduces To In One Step

1 occurrence in this chapter

Equation form expr-232ee327014602c6

F(n+1¯)≡H(n¯,F(n¯))F(\num {n+1}) \equiv H(\num n, F(\num{n}))

Read as: capital F applied to the Church numeral for n plus one is beta equivalent to capital H applied to the Church numeral for n and then capital F applied to that numeral

Means: capital F applied to the Church numeral for n plus one is beta equivalent to capital H applied to the Church numeral for n and then capital F applied to that numeral

1 occurrence in this chapter

Equation form expr-24ff3f7fddede28f

T(⟨n¯,M⟩)↠⟨n+1¯,H(n¯,M)⟩.T(\tuple{\num{n}, M}) \red \tuple{\num{n+1}, H(\num{n}, M)}.

Read as: capital T applied to the ordered pair of the Church numeral for n and capital M beta reduces to the ordered pair of the Church numeral for n plus one and capital H applied to the Church numeral for n and then capital M

Means: capital T applied to the ordered pair of the Church numeral for n and capital M beta reduces to the ordered pair of the Church numeral for n plus one and capital H applied to the Church numeral for n and then capital M

1 occurrence in this chapter

Equation form expr-252f10c83610ebca

ff

Read as: f

Means: f

16 occurrences in this chapter

Equation form expr-27271d42717f2051

(P)0(P)_0

Read as: the first component of the pair represented by capital P

Means: the first component of the pair represented by capital P

1 occurrence in this chapter

Equation form expr-28c24d498d4f4597

l(x)=g(diag(x))l(x) = g(\fn{diag}(x))

Read as: l applied to x equals g applied to diagonal of x

Means: l applied to x equals g applied to diagonal of x

1 occurrence in this chapter

Equation form expr-29e8525545d84c9c

hx(n)h_x(n)

Read as: h subscript x of n

Means: h subscript x of n

1 occurrence in this chapter

Equation form expr-2d711642b726b044

xx

Read as: x

Means: x

20 occurrences in this chapter

Equation form expr-2e7d2c03a9507ae2

cc

Read as: c

Means: c

1 occurrence in this chapter

Equation form expr-308fda5bda779517

fxf_x

Read as: f subscript x

Means: f subscript x

1 occurrence in this chapter

Equation form expr-3269d94607e3df86

H=YU≡U(YU)=U(H).H = YU \equiv U(YU) = U(H).

Read as: capital H equals capital Y applied to capital U, which is beta equivalent to capital U applied to the result of applying capital Y to capital U, which equals capital U applied to capital H

Means: capital H equals capital Y applied to capital U, which is beta equivalent to capital U applied to the result of applying capital Y to capital U, which equals capital U applied to capital H

1 occurrence in this chapter

Equation form expr-333e0a1e27815d0c

GG

Read as: capital G

Means: capital G

5 occurrences in this chapter

Equation form expr-335b5e6f91a8441f

m0m_0

Read as: m subscript zero

Means: m subscript zero

1 occurrence in this chapter

Equation form expr-34953485bf2616fb

λx0.…λxn−1.xi\lambd[x_0][\dots \lambd[x_{n-1}][x_i]]

Read as: successive lambda abstractions binding x subscript zero through x subscript n minus one, with innermost body x subscript i

Means: successive lambda abstractions binding x subscript zero through x subscript n minus one, with innermost body x subscript i

1 occurrence in this chapter

Equation form expr-35b907cb05c2dfeb

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

Read as: lambda x, with body capital M applied first to capital N and then to capital P

Means: lambda x, with body capital M applied first to capital N and then to capital P

1 occurrence in this chapter

Equation form expr-36fe203bbfba2f8a

D(M,N,1¯)↠ND(M, N, \bar{1}) \red N

Read as: capital D applied to capital M, capital N, and the Church numeral one beta reduces to capital N

Means: capital D applied to capital M, capital N, and the Church numeral one beta reduces to capital N

1 occurrence in this chapter

Equation form expr-385262088dac5789

Y=(λxg.g(xxg))(λxg.g(xxg))Y = (\lambd[xg][g(xxg)])(\lambd[xg][g(xxg)])

Read as: capital Y equals the abstraction lambda x, then lambda g, with body g applied to the result of applying x to x and then g, applied to another copy of that same abstraction

Means: capital Y equals the abstraction lambda x, then lambda g, with body g applied to the result of applying x to x and then g, applied to another copy of that same abstraction

1 occurrence in this chapter

Equation form expr-38ac21ef682959c7

F(0¯)≡GF(n+1¯)≡H(n¯,F(n¯))for every natural number n, whereG=λz→.G′(z→) andH(u,v)=λz→.H′(u,v(u,z→),z→).F(\num 0) & \equiv G \\ F(\overline {n+1}) & \equiv H(\num{n},F(\num{n})) \intertext{for every natural number $n$, where} G & = \lambd[\vec z][G'(\vec z)] \text{ and}\\ H(u,v) & = \lambd[\vec z][H'(u,v(u,\vec z),\vec z)].

Read as: capital F applied to the Church numeral zero is beta equivalent to capital G. Capital F applied to the Church numeral for n plus one is beta equivalent to capital H applied to the Church numeral for n and capital F applied to that numeral. These hold for every natural number n, where capital G equals the successive lambda abstractions binding the parameter list z, with body capital G prime applied to that list; and capital H applied to u and v equals the abstractions binding the parameter list z, with body capital H prime applied to u, v applied to u and the parameter list z, and the parameter list z

Means: capital F applied to the Church numeral zero is beta equivalent to capital G. Capital F applied to the Church numeral for n plus one is beta equivalent to capital H applied to the Church numeral for n and capital F applied to that numeral. These hold for every natural number n, where capital G equals the successive lambda abstractions binding the parameter list z, with body capital G prime applied to that list; and capital H applied to u and v equals the abstractions binding the parameter list z, with body capital H prime applied to u, v applied to u and the parameter list z, and the parameter list z

1 occurrence in this chapter

Equation form expr-38bcd8e10f54eff9

F(u)F(u)

Read as: capital F applied to u

Means: capital F applied to u

1 occurrence in this chapter

Equation form expr-38de222787f08c1c

F(0¯)≡GF(\num 0) \equiv G

Read as: capital F applied to the Church numeral zero is beta equivalent to capital G

Means: capital F applied to the Church numeral zero is beta equivalent to capital G

1 occurrence in this chapter

Equation form expr-390de550262a3bc4

D(x,y,z)D(x,y,z)

Read as: capital D applied successively to x, y, and z

Means: capital D applied successively to x, y, and z

1 occurrence in this chapter

Equation form expr-3970c616f467980e

hxh_x

Read as: h subscript x

Means: h subscript x

2 occurrences in this chapter

Equation form expr-3bf8869004d647ba

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

Read as: lambda x, with body f subscript x

Means: lambda x, with body f subscript x

1 occurrence in this chapter

Equation form expr-3d0651532b8c262e

f(0,z→)=g(z→)f(x+1,z→)=h(z,f(x,z→),z→).f(0, \vec z) & = g(\vec z) \\ f(x+1, \vec z) & = h(z, f(x,\vec z), \vec z).

Read as: Base clause: f of zero and the parameter list z equals g of the parameter list z. Successor clause as written: f of x plus one and the parameter list z equals h of z, f of x and the parameter list z, and the parameter list z

Means: Base clause: f of zero and the parameter list z equals g of the parameter list z. Successor clause as written: f of x plus one and the parameter list z equals h of z, f of x and the parameter list z, and the parameter list z

1 occurrence in this chapter

Equation form expr-3e1c8f0184701034

F(0¯)≡GF(\num{0}) \equiv G

Read as: capital F applied to the Church numeral zero is beta equivalent to capital G

Means: capital F applied to the Church numeral zero is beta equivalent to capital G

1 occurrence in this chapter

Equation form expr-3e23e8160039594a

bb

Read as: b

Means: b

1 occurrence in this chapter

Equation form expr-3ed5109efad3bece

g(m)g(m)

Read as: g of m

Means: g of m

1 occurrence in this chapter

Equation form expr-3f39d5c348e5b79d

DD

Read as: capital D

Means: capital D

2 occurrences in this chapter

Equation form expr-3f543de4a017b06d

Projin\fn{Proj}^n_i

Read as: the n argument projection with index i

Means: the n argument projection with index i

1 occurrence in this chapter

Equation form expr-3ffb8d0c0c048885

λx.(x+3)\lambd[x][(x+3)]

Read as: lambda x, with body x plus three

Means: lambda x, with body x plus three

1 occurrence in this chapter

Equation form expr-40f87716a93e8e9e

D(M,N,0¯)↠MD(M, N, \bar{0}) \red M

Read as: capital D applied to capital M, capital N, and the Church numeral zero beta reduces to capital M

Means: capital D applied to capital M, capital N, and the Church numeral zero beta reduces to capital M

1 occurrence in this chapter

Equation form expr-42dfca9530b6e6b5

0¯(T,⟨0¯,G⟩)≡⟨0¯,G⟩\num{0} (T, \tuple{\num 0, G}) \equiv \tuple{\num{0}, G}

Read as: the Church numeral zero applied to capital T and the ordered pair of the Church numeral zero and capital G is beta equivalent to that initial ordered pair

Means: the Church numeral zero applied to capital T and the ordered pair of the Church numeral zero and capital G is beta equivalent to that initial ordered pair

1 occurrence in this chapter

Equation form expr-43797314848d20f1

g(x)≃μyf(x,y).g(x) \simeq \umin{y}{f(x,y)}.

Read as: g of x is partially equal to the least y for which f of x and y is zero, with every preceding tested value defined

Means: g of x is partially equal to the least y for which f of x and y is zero, with every preceding tested value defined

1 occurrence in this chapter

Equation form expr-43a86cd1a65542e0

M[x/N]M[x/N]

Read as: capital M followed by open square bracket, x slash capital N, close square bracket

Means: capital M followed by open square bracket, x slash capital N, close square bracket

1 occurrence in this chapter

Equation form expr-44bd7ae60f478fae

HH

Read as: capital H

Means: capital H

9 occurrences in this chapter

Equation form expr-44c584412319b4d8

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

Read as: the ordered pair of the Church numeral for n and capital F applied to that numeral

Means: the ordered pair of the Church numeral for n and capital F applied to that numeral

1 occurrence in this chapter

Equation form expr-45a7ad2dd6915d22

N1≡P≡N2N_1 \ident P \ident N_2

Read as: capital N subscript one, capital P, and capital N subscript two are the same term, under the chapter's bound variable renaming convention

Means: capital N subscript one, capital P, and capital N subscript two are the same term, under the chapter's bound variable renaming convention

1 occurrence in this chapter

Equation form expr-4675b4292c1aff69

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

Read as: lambda x, then lambda y, then lambda z, with innermost body capital M

Means: lambda x, then lambda y, then lambda z, with innermost body capital M

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-47bc44b8c80f1f24

(λx.λy.x)MN→β(λy.M)N→βM(\lambd[x][\lambd[y][x]])MN \bredone & (\lambd[y][M])N \\ \bredone & M

Read as: lambda x, then lambda y, with body x, applied first to capital M and then capital N, beta reduces in one step to lambda y with body capital M, applied to capital N. One further beta step gives capital M

Means: lambda x, then lambda y, with body x, applied first to capital M and then capital N, beta reduces in one step to lambda y with body capital M, applied to capital N. One further beta step gives capital M

1 occurrence in this chapter

Equation form expr-4893e9df8b5496eb

α\alpha

Read as: alpha

Means: alpha

1 occurrence in this chapter

Equation form expr-49045266e40616d4

λx.H(0¯)\lambd[x][H(\num 0)]

Read as: lambda x, with body capital H applied to the Church numeral zero

Means: lambda x, with body capital H applied to the Church numeral zero

1 occurrence in this chapter

Equation form expr-4ae81572f06e1b88

QQ

Read as: capital Q

Means: capital Q

1 occurrence in this chapter

Equation form expr-4b017fd4a0410046

YUYU

Read as: capital Y applied to capital U

Means: capital Y applied to capital U

1 occurrence in this chapter

Equation form expr-4b68ab3847feda7d

XX

Read as: capital X

Means: capital X

1 occurrence in this chapter

Equation form expr-4bc460034617c2e5

(λx.(x+3))(2)(\lambd[x][(x + 3)])(2)

Read as: the abstraction lambda x, with body x plus three, applied to two

Means: the abstraction lambda x, with body x plus three, applied to two

1 occurrence in this chapter

Equation form expr-4dc4e01def696af8

Pin\Proj{n}{i}

Read as: the n argument projection with index i

Means: the n argument projection with index i

1 occurrence in this chapter

Equation form expr-4f0f1e4a3167d257

xix_i

Read as: x subscript i

Means: x subscript i

1 occurrence in this chapter

Equation form expr-5081cbc657fe24bd

m¯\num{m}

Read as: m with an overbar

Means: m with an overbar

1 occurrence in this chapter

Equation form expr-5083e5d206a852bb

G(m¯)G(\num m)

Read as: capital G applied to the Church numeral for m

Means: capital G applied to the Church numeral for m

1 occurrence in this chapter

Equation form expr-52a6f36ab44880c7

λy.(y+3)\lambd[y][(y + 3)]

Read as: lambda y, with body y plus three

Means: lambda y, with body y plus three

1 occurrence in this chapter

Equation form expr-53aebbe1a4de6741

(MN)(MN)

Read as: capital M applied to capital N

Means: capital M applied to capital N

2 occurrences in this chapter

Equation form expr-54c66fee3cb6e550

(λx1.λx2.…λxn.N)M1…Mn→β→β((λx2.…λxn.N)[M1/x1])M2…Mn≡(λx2.…λxn.N[M1/x1])M2…Mn⋮→βP[M1/x1]…[Mn/xn](\lambd[x_1][\lambd[x_2][\ldots\lambd[x_n][N]]]) M_1 \dots M_n \bredone\\ \begin{aligned} \bredone {} & (\Subst{(\lambd[x_2][\ldots\lambd[x_n][N]])}{M_1}{x_1}) M_2 \dots M_n\\ \eqs {} & (\lambd[x_2][\ldots\lambd[x_n][\Subst{N}{M_1}{x_1}]]) M_2 \dots M_n \\ \vdots & \\ \bredone {} &\Subst{\Subst{P}{M_1}{x_1}\ldots}{M_n}{x_n} \end{aligned}

Read as: Take the nested abstractions binding x subscript one through x subscript n, with body capital N, and apply successively to capital M subscript one through capital M subscript n. The one step beta reduction sign is repeated across the source line break. The first result substitutes capital M subscript one for free x subscript one in the remaining abstractions, then applies the result to capital M subscript two through capital M subscript n. This equals the abstractions binding x subscript two through x subscript n, with body capital N after that first substitution, applied to the remaining arguments. Intermediate steps are omitted. The final displayed beta step gives capital P with successive substitutions of capital M subscript one for x subscript one, through capital M subscript n for x subscript n. The source's change from capital N to capital P is preserved

Means: Take the nested abstractions binding x subscript one through x subscript n, with body capital N, and apply successively to capital M subscript one through capital M subscript n. The one step beta reduction sign is repeated across the source line break. The first result substitutes capital M subscript one for free x subscript one in the remaining abstractions, then applies the result to capital M subscript two through capital M subscript n. This equals the abstractions binding x subscript two through x subscript n, with body capital N after that first substitution, applied to the remaining arguments. Intermediate steps are omitted. The final displayed beta step gives capital P with successive substitutions of capital M subscript one for x subscript one, through capital M subscript n for x subscript n. The source's change from capital N to capital P is preserved

1 occurrence in this chapter

Equation form expr-553780ea8a2cf901

M=λx.λy.λz.…M = \lambd[x][\lambd[y][\lambd[z][\dots]]]

Read as: capital M equals lambda x, then lambda y, then lambda z, with an unspecified innermost body

Means: capital M equals lambda x, then lambda y, then lambda z, with an unspecified innermost body

1 occurrence in this chapter

Equation form expr-556dc1570530269c

N2↠PN_2 \red P

Read as: capital N subscript two beta reduces to capital P

Means: capital N subscript two beta reduces to capital P

1 occurrence 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-588e9bc6c2f81c26

λx.λy.((((xx)y)x)(λz.(xz))).\lambd[x][\lambd[y][((((xx)y)x)(\lambd[z][(xz)]))]].

Read as: lambda x, then lambda y, with body the left associated application of x to x, then y, then x, then the abstraction lambda z with body x applied to z

Means: lambda x, then lambda y, with body the left associated application of x to x, then y, then x, then the abstraction lambda z with body x applied to z

1 occurrence in this chapter

Equation form expr-594e519ae499312b

zz

Read as: z

Means: z

2 occurrences in this chapter

Equation form expr-5a4395962f1774ea

f(x0,…,xk−1)f(x_0, \dots, x_{k-1})

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

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

1 occurrence in this chapter

Equation form expr-5ae19a29dd56473a

P↠P′P \red P'

Read as: capital P beta reduces in zero or more steps to capital P prime

Means: capital P beta reduces in zero or more steps to capital P prime

1 occurrence in this chapter

Equation form expr-5b93a9b0461acefd

YgYg

Read as: capital Y applied to g

Means: capital Y applied to g

2 occurrences in this chapter

Equation form expr-5c62e091b8c0565f

PP

Read as: capital P

Means: capital P

10 occurrences in this chapter

Equation form expr-5d57610ff217ffc8

D(M,N,0¯)↠0¯(K(N))M↠M andD(M,N,1¯)↠1¯(K(N))M↠K(N)M↠N,D(M,N,\num 0) & \red \num 0 (K(N)) M \red M \text{ and}\\ D(M,N,\num 1) & \red \num 1 (K(N)) M \red K(N) M \red N,

Read as: capital D applied to capital M, capital N, and the Church numeral zero beta reduces to the Church numeral zero applied to capital K of capital N and then capital M, and then reduces to capital M. Also, capital D applied to capital M, capital N, and the Church numeral one beta reduces to the Church numeral one applied to capital K of capital N and then capital M; this reduces to capital K of capital N applied to capital M; and this reduces to capital N

Means: capital D applied to capital M, capital N, and the Church numeral zero beta reduces to the Church numeral zero applied to capital K of capital N and then capital M, and then reduces to capital M. Also, capital D applied to capital M, capital N, and the Church numeral one beta reduces to the Church numeral one applied to capital K of capital N and then capital M; this reduces to capital K of capital N applied to capital M; and this reduces to capital N

1 occurrence in this chapter

Equation form expr-5e1a1a36d46632a4

G′G'

Read as: capital G prime

Means: capital G prime

2 occurrences in this chapter

Equation form expr-5e99ae39a3dcfd6c

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

Read as: lambda x, then lambda y, with innermost body x

Means: lambda x, then lambda y, with innermost body x

2 occurrences in this chapter

Equation form expr-5fc9cece534f0f27

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

Read as: lambda y, with body y

Means: lambda y, with body y

1 occurrence in this chapter

Equation form expr-5fe6dc6b2281b3d2

zero\Zero

Read as: Zero

Means: Zero

2 occurrences in this chapter

Equation form expr-5fea10b1c5e67a23

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

Read as: lambda y, with body x

Means: lambda y, with body x

2 occurrences in this chapter

Equation form expr-611fd5e7e553a5ef

f(x,y)f(x,y)

Read as: f of x and y

Means: f of x and y

1 occurrence in this chapter

Equation form expr-62484e37ccfd112e

M(x,y)M(x,y)

Read as: capital M, open parenthesis, x comma y, close parenthesis

Means: capital M, open parenthesis, x comma y, close parenthesis

1 occurrence in this chapter

Equation form expr-628a80a5ab89758a

f(x,y)=xf(x,y) = x

Read as: f of x and y equals x

Means: f of x and y equals x

1 occurrence in this chapter

Equation form expr-62c66a7a5dd70c31

mm

Read as: m

Means: m

1 occurrence in this chapter

Equation form expr-638d6219cf79de01

M(x,y,z)=…M(x,y,z) = \dots

Read as: capital M, open parenthesis, x comma y comma z, close parenthesis, equals an ellipsis standing for the unspecified body

Means: capital M, open parenthesis, x comma y comma z, close parenthesis, equals an ellipsis standing for the unspecified body

1 occurrence in this chapter

Equation form expr-65b364bb82ea19d5

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

Read as: lambda y, then lambda x, with innermost body y

Means: lambda y, then lambda x, with innermost body y

1 occurrence in this chapter

Equation form expr-68df1dc4dce4ac05

F(n+1¯)↠(n+1¯(T,⟨0¯,G⟩))1≡(T(n¯(T,⟨0¯,G⟩)))1≡(T(⟨n¯,F(n¯)⟩))1≡(⟨n+1¯,H(n¯,F(n¯))⟩)1≡H(n¯,F(n¯)).F(\num{n+1}) & \red (\num{n+1}(T, \tuple{\num 0, G}))_1 \\ & \equiv (T(\num{n} (T, \tuple{\num 0, G})))_1 \\ & \equiv (T(\tuple{\num{n}, F(\num{n})}))_1 \\ & \equiv (\tuple{\num{n+1}, H(\num{n}, F(\num{n}))})_1 \\ & \equiv H(\num{n}, F(\num{n})).

Read as: capital F applied to the Church numeral for n plus one beta reduces to the second component obtained by iterating capital T n plus one times on the initial pair of the Church numeral zero and capital G. This is beta equivalent to the second component of capital T applied after n iterations on the initial pair. This is beta equivalent to the second component of capital T applied to the pair of the Church numeral for n and capital F applied to that numeral. This is beta equivalent to the second component of the pair of the Church numeral for n plus one and capital H applied to the Church numeral for n and capital F applied to that numeral. Finally, this is beta equivalent to that second component, capital H applied to the Church numeral for n and then capital F applied to that numeral

Means: capital F applied to the Church numeral for n plus one beta reduces to the second component obtained by iterating capital T n plus one times on the initial pair of the Church numeral zero and capital G. This is beta equivalent to the second component of capital T applied after n iterations on the initial pair. This is beta equivalent to the second component of capital T applied to the pair of the Church numeral for n and capital F applied to that numeral. This is beta equivalent to the second component of the pair of the Church numeral for n plus one and capital H applied to the Church numeral for n and capital F applied to that numeral. Finally, this is beta equivalent to that second component, capital H applied to the Church numeral for n and then capital F applied to that numeral

1 occurrence in this chapter

Equation form expr-6d70a9984848e206

M↠PM \red P

Read as: capital M beta reduces to capital P

Means: capital M beta reduces to capital P

1 occurrence in this chapter

Equation form expr-6de290a1107c89bb

M↠N1M \red N_1

Read as: capital M beta reduces to capital N subscript one

Means: capital M beta reduces to capital N subscript one

2 occurrences in this chapter

Equation form expr-6e686b1f43cff88f

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 applied successively to the Church numerals for n subscript zero, n subscript one, through n subscript k minus one, beta reduces to the Church numeral for f of that same argument list

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

1 occurrence in this chapter

Equation form expr-7022f5cc704457a8

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

Read as: capital F, followed in the source by a comma, then the Church numerals for n subscript zero through n subscript k minus one

Means: capital F, followed in the source by a comma, then the Church numerals for n subscript zero through n subscript k minus one

1 occurrence in this chapter

Equation form expr-7082050d06a3d44b

(λx.M)(\lambd[x][M])

Read as: the abstraction lambda x, with body capital M

Means: the abstraction lambda x, with body capital M

2 occurrences in this chapter

Equation form expr-70c41d2f523a43cf

(λx.(λy.yx)z)v→(λy.yv)z(\lambd[x][(\lambd[y][yx]) z]) v \redone (\lambd[y][yv]) z

Read as: the abstraction lambda x, whose body is the abstraction lambda y with body y applied to x, applied to z, is applied to v. One outermost beta step gives the abstraction lambda y with body y applied to v, applied to z

Means: the abstraction lambda x, whose body is the abstraction lambda y with body y applied to x, applied to z, is applied to v. One outermost beta step gives the abstraction lambda y with body y applied to v, applied to z

1 occurrence in this chapter

Equation form expr-721575d946b455ec

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

Read as: lambda x, with body capital M

Means: lambda x, with body capital M

2 occurrences in this chapter

Equation form expr-72ec741403c87a9e

N2N_2

Read as: capital N subscript two

Means: capital N subscript two

3 occurrences in this chapter

Equation form expr-752a4517b8b53d0a

MNPQMNPQ

Read as: capital M applied successively to capital N, capital P, and capital Q

Means: capital M applied successively to capital N, capital P, and capital Q

1 occurrence in this chapter

Equation form expr-76da57b1a01eccae

N1↠PN_1 \red P

Read as: capital N subscript one beta reduces to capital P

Means: capital N subscript one beta reduces to capital P

1 occurrence in this chapter

Equation form expr-777e6971be9f36a9

2+32 + 3

Read as: two plus three

Means: two plus three

1 occurrence in this chapter

Equation form expr-77c413b453e89606

Yg≡βg(Yg)Yg \equiv_\beta g(Yg)

Read as: capital Y applied to g is beta equivalent to g applied to the term capital Y applied to g

Means: capital Y applied to g is beta equivalent to g applied to the term capital Y applied to g

1 occurrence in this chapter

Equation form expr-79c10412438be53b

Projin(x0,…,xn−1)=xi\fn{Proj}^n_i(x_0, \dots, x_{n-1}) = x_i

Read as: the n argument projection with index i, applied successively to x subscript zero through x subscript n minus one, equals x subscript i

Means: the n argument projection with index i, applied successively to x subscript zero through x subscript n minus one, equals x subscript i

1 occurrence in this chapter

Equation form expr-79d4c7f9c8579543

ℕ\Nat

Read as: the natural numbers

Means: the natural numbers

2 occurrences in this chapter

Equation form expr-7a8dd6984c28609c

H(n¯)≡U(H,n¯)↠D(n¯,H(S(n¯)),F(x,n¯)),H(\num{n}) & \equiv U(H, \num{n}) \\ & \red D(\num{n}, H(S(\num{n})), F(x, \num{n})),

Read as: capital H applied to the Church numeral for n is beta equivalent to capital U applied to capital H and that numeral. This beta reduces to capital D applied to that numeral, capital H applied to the result of applying capital S to that numeral, and capital F applied to x and that numeral, in that order

Means: capital H applied to the Church numeral for n is beta equivalent to capital U applied to capital H and that numeral. This beta reduces to capital D applied to that numeral, capital H applied to the result of applying capital S to that numeral, and capital F applied to x and that numeral, in that order

1 occurrence in this chapter

Equation form expr-7f024b2d7f1db4d4

n¯\num{n}

Read as: n with an overbar

Means: n with an overbar

6 occurrences in this chapter

Equation form expr-807308ed00edd33b

hx(0)h_x(0)

Read as: h subscript x of zero

Means: h subscript x of zero

1 occurrence in this chapter

Equation form expr-8098ac49d9f4170a

F(0¯,z→)≡G(z→)F(n+1¯,z→)≡H(n¯,F(n¯,z→),z→)F(\num{0}, \vec z) & \equiv G(\vec z) \\ F(\overline{n+1}, \vec z) & \equiv H(\num{n}, F(\num{n}, \vec z), \vec z)

Read as: capital F applied to the Church numeral zero and the parameter list z is beta equivalent to capital G applied to the parameter list z. Capital F applied to the Church numeral for n plus one and the parameter list z is beta equivalent to capital H applied to the Church numeral for n, capital F applied to that numeral and the parameter list z, and the parameter list z

Means: capital F applied to the Church numeral zero and the parameter list z is beta equivalent to capital G applied to the parameter list z. Capital F applied to the Church numeral for n plus one and the parameter list z is beta equivalent to capital H applied to the Church numeral for n, capital F applied to that numeral and the parameter list z, and the parameter list z

1 occurrence in this chapter

Equation form expr-8254c329a92850f6

kk

Read as: k

Means: k

4 occurrences in this chapter

Equation form expr-831b03e703e0af67

(λz.yz)x(\lambd[z][yz])x

Read as: the abstraction lambda z, with body y applied to z, applied to x

Means: the abstraction lambda z, with body y applied to z, applied to x

1 occurrence in this chapter

Equation form expr-83237ad595be847b

M=βNM \equal[\beta] N

Read as: capital M is beta equivalent to capital N

Means: capital M is beta equivalent to capital N

2 occurrences in this chapter

Equation form expr-86aad91554a7b587

Gk−1G_{k-1}

Read as: capital G subscript k minus one

Means: capital G subscript k minus one

1 occurrence in this chapter

Equation form expr-86be9a55762d316a

KK

Read as: capital K

Means: capital K

2 occurrences in this chapter

Equation form expr-8a83ec2d66cc5c25

g(x,k)g(x, k)

Read as: g of x and k

Means: g of x and k

1 occurrence in this chapter

Equation form expr-8ce86a6ae65d3692

NN

Read as: capital N

Means: capital N

11 occurrences in this chapter

Equation form expr-8e93fb0fe49526c0

f(m0,…,mn−1)f(m_0, \dots, m_{n-1})

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

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

1 occurrence in this chapter

Equation form expr-907ff5c260690bd0

(λw.xxw)[yyz/x]=λw.(yyz)(yyz)w.\Subst{(\lambd[w][xxw])}{yyz}{x} = \lambd[w][(yyz)(yyz)w].

Read as: substituting the term y applied to y and then z for free x in lambda w with body x applied to x and then w, gives lambda w with body the term y applied to y and then z, applied to a second copy of that same term, then applied to w

Means: substituting the term y applied to y and then z for free x in lambda w with body x applied to x and then w, gives lambda w with body the term y applied to y and then z, applied to a second copy of that same term, then applied to w

1 occurrence in this chapter

Equation form expr-90b5caa820bdc1a8

λx.λy.(x(x(x(…x(y)))))\lambd[x][\lambd[y][(x(x(x(\dots x(y)))))]]

Read as: lambda x, then lambda y, with body x applied repeatedly to y, nested to the right, with the number of applications specified as n

Means: lambda x, then lambda y, with body x applied repeatedly to y, nested to the right, with the number of applications specified as n

1 occurrence in this chapter

Equation form expr-9133bd98ed6c0a50

⟨0¯,G⟩\tuple{\num 0, G}

Read as: the ordered pair of the Church numeral zero and capital G

Means: the ordered pair of the Church numeral zero and capital G

2 occurrences in this chapter

Equation form expr-9190f4419c12dcc4

Succ(u)=λx.λy.x(uxy)\fn{Succ}(u) = \lambd[x][\lambd[y][x(uxy)]]

Read as: Successor of u equals lambda x, then lambda y, with body x applied to the result of applying u first to x and then to y

Means: Successor of u equals lambda x, then lambda y, with body x applied to the result of applying u first to x and then to y

1 occurrence in this chapter

Equation form expr-93d01507fa1b7448

(λx.(λy.yx)z)v→(λx.zx)v(\lambd[x][(\lambd[y][yx]) z]) v \redone (\lambd[x][zx]) v

Read as: the abstraction lambda x, whose body is the abstraction lambda y with body y applied to x, applied to z, is applied to v. One innermost beta step gives the abstraction lambda x with body z applied to x, applied to v

Means: the abstraction lambda x, whose body is the abstraction lambda y with body y applied to x, applied to z, is applied to v. One innermost beta step gives the abstraction lambda x with body z applied to x, applied to v

1 occurrence in this chapter

Equation form expr-94687039028990df

D(M,N)(1¯)↠ND(M,N)(\num{1}) \red N

Read as: capital D applied to capital M and capital N, then to the Church numeral one, beta reduces to capital N

Means: capital D applied to capital M and capital N, then to the Church numeral one, beta reduces to capital N

1 occurrence in this chapter

Equation form expr-98f0455530b5b3d8

gk−1g_{k-1}

Read as: g subscript k minus one

Means: g subscript k minus one

2 occurrences in this chapter

Equation form expr-99688af5fa62bf90

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

Read as: lambda x, then lambda y, with innermost body y

Means: lambda x, then lambda y, with innermost body y

1 occurrence in this chapter

Equation form expr-999cf9b6169c9aca

(λx.xxy)λz.z→(λz.z)(λz.z)y→(λz.z)y→y.(\lambd[x][xxy]) \lambd[z][z] & \redone (\lambd[z][z])(\lambd[z][z]) y \\ & \redone (\lambd[z][z]) y \\ & \redone y.

Read as: Start with lambda x, with body x applied to x and then y, applied to the identity abstraction lambda z with body z. One beta step gives the identity abstraction applied to itself and then y. One further beta step gives the identity abstraction applied to y. One final beta step gives y

Means: Start with lambda x, with body x applied to x and then y, applied to the identity abstraction lambda z with body z. One beta step gives the identity abstraction applied to itself and then y. One further beta step gives the identity abstraction applied to y. One final beta step gives y

1 occurrence in this chapter

Equation form expr-9caf7de2e5dca87b

=β\equal[\beta]

Read as: beta equivalence

Means: beta equivalence

2 occurrences in this chapter

Equation form expr-9df361b4e347d18b

k=(λx.g(xx))(λx.g(xx))↠g((λx.g(xx))(λx.g(xx)))=gk.k & = (\lambd[x][g(xx)])(\lambd[x][g(xx)]) \\ & \red g((\lambd[x][g(xx)])(\lambd[x][g(xx)])) \\ & = gk.

Read as: k equals the abstraction lambda x with body g applied to the self application of x, applied to another copy of that same abstraction. This beta reduces to g applied to the self application of that abstraction. This equals g applied to k

Means: k equals the abstraction lambda x with body g applied to the self application of x, applied to another copy of that same abstraction. This beta reduces to g applied to the self application of that abstraction. This equals g applied to k

1 occurrence in this chapter

Equation form expr-9f0772bab16d2fa7

F(x0,…,xl−1)=H(G0(x0,…,xl−1),…,Gk−1(x0,…,xl−1)).F(x_0, \dots, x_{l-1}) = H(G_0(x_0, \dots, x_{l-1}), \dots, G_{k-1}(x_0, \dots, x_{l-1})).

Read as: capital F applied to x subscript zero through x subscript l minus one equals capital H applied successively to the results of capital G subscript zero through capital G subscript k minus one, each applied to that same list of l arguments

Means: capital F applied to x subscript zero through x subscript l minus one equals capital H applied successively to the results of capital G subscript zero through capital G subscript k minus one, each applied to that same list of l arguments

1 occurrence in this chapter

Equation form expr-a1fce4363854ff88

yy

Read as: y

Means: y

9 occurrences in this chapter

Equation form expr-a2277e0b98ac28a5

g(x)g(x)

Read as: g of x

Means: g of x

2 occurrences in this chapter

Equation form expr-a25513c7e0f6eaa8

UU

Read as: capital U

Means: capital U

1 occurrence in this chapter

Equation form expr-a318c24216defe20

++

Read as: plus

Means: plus

1 occurrence in this chapter

Equation form expr-a39b32492df35396

gkgk

Read as: g applied to k

Means: g applied to k

1 occurrence in this chapter

Equation form expr-a46932c35387322e

F(F)F(F)

Read as: capital F applied to itself

Means: capital F applied to itself

1 occurrence in this chapter

Equation form expr-a99a2c4f0f78871b

D(x,y,z)=z(K(y))xD(x,y,z) = z (K(y))x

Read as: capital D applied successively to x, y, and z equals z applied first to capital K applied to y, then to x

Means: capital D applied successively to x, y, and z equals z applied first to capital K applied to y, then to x

1 occurrence in this chapter

Equation form expr-a9cb3b937e2cd2a7

F(n+1¯,m→¯)F(\num{n+1}, \num{\vec m})

Read as: capital F applied to the Church numeral for n plus one, followed by the list of Church numerals for m

Means: capital F applied to the Church numeral for n plus one, followed by the list of Church numerals for m

1 occurrence in this chapter

Equation form expr-aaa9402664f1a41f

hh

Read as: h

Means: h

4 occurrences in this chapter

Equation form expr-ac3032285419b06b

Succ(n¯,f)\fn{Succ}(\num{n},f)

Read as: Successor applied first to the Church numeral for n, and then to f

Means: Successor applied first to the Church numeral for n, and then to f

1 occurrence in this chapter

Equation form expr-acac86c0e609ca90

ll

Read as: l

Means: l

1 occurrence in this chapter

Equation form expr-aec6d6d44dae2bfb

Xm¯0…m¯n−1X \num m_0 \ldots \num m_{n-1}

Read as: capital X applied successively to the Church numerals for m subscript zero through m subscript n minus one

Means: capital X applied successively to the Church numerals for m subscript zero through m subscript n minus one

1 occurrence in this chapter

Equation form expr-b0d426d00081371f

z→\vec z

Read as: the parameter list z

Means: the parameter list z

2 occurrences in this chapter

Equation form expr-b1eb06f6029b52e0

λh.λz.D(z,(h(Sz)),F(x,z)),\lambd[h][\lambd[z][D(z,(h(Sz)),F(x,z))]],

Read as: lambda h, then lambda z, with body capital D applied to z, h applied to the result of applying capital S to z, and capital F applied to x and z, in that order

Means: lambda h, then lambda z, with body capital D applied to z, h applied to the result of applying capital S to z, and capital F applied to x and z, in that order

1 occurrence in this chapter

Equation form expr-b3460543c506b16b

(((MN)P)Q)(((MN)P)Q)

Read as: the result of applying capital M to capital N, then to capital P, then to capital Q

Means: the result of applying capital M to capital N, then to capital P, then to capital Q

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

(λx.xx)(λx.xx)→(λx.xx)(λx.xx).(\lambd[x][xx])(\lambd[x][xx]) \redone (\lambd[x][xx])(\lambd[x][xx]).

Read as: the abstraction lambda x with body x applied to x, applied to itself, beta reduces in one step to that very same self application

Means: the abstraction lambda x with body x applied to x, applied to itself, beta reduces in one step to that very same self application

1 occurrence in this chapter

Equation form expr-b4cecddd9ec1fd2c

M[N/x]\Subst{M}{N}{x}

Read as: capital M with capital N substituted for free x, avoiding variable capture

Means: capital M with capital N substituted for free x, avoiding variable capture

3 occurrences in this chapter

Equation form expr-b4db03dab703b98b

zvzv

Read as: z applied to v

Means: z applied to v

1 occurrence in this chapter

Equation form expr-b620f7fd0a05aeb7

0¯\num{0}

Read as: the Church numeral zero

Means: the Church numeral zero

1 occurrence in this chapter

Equation form expr-b721524250a31c52

hx(n)≃{nif f(x,n)=0hx(n+1)otherwise.h_x(n) \simeq \begin{cases} n & \text{if $f(x,n) = 0$} \\ h_x(n+1) & \text{otherwise.} \end{cases}

Read as: h subscript x of n is partially equal to the following cases: n, if f of x and n equals zero; h subscript x of n plus one, otherwise

Means: h subscript x of n is partially equal to the following cases: n, if f of x and n equals zero; h subscript x of n plus one, otherwise

1 occurrence in this chapter

Equation form expr-b77bd89ddde577d6

Substitute\fn{Substitute}

Read as: Substitute

Means: Substitute

1 occurrence in this chapter

Equation form expr-b8bdb1c02444ca91

H′H'

Read as: capital H prime

Means: capital H prime

2 occurrences in this chapter

Equation form expr-b8e2b244c77b7c22

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

Read as: lambda x, with body g applied to the self application of x

Means: lambda x, with body g applied to the self application of x

1 occurrence in this chapter

Equation form expr-bb2f7432725587ea

T(u)T(u)

Read as: capital T applied to u

Means: capital T applied to u

1 occurrence in this chapter

Equation form expr-bdc8f4297f780b8d

MxyzMxyz

Read as: capital M followed by x, y, and z without parentheses

Means: capital M followed by x, y, and z without parentheses

1 occurrence in this chapter

Equation form expr-c2c5eeeab86b1b20

g(Yg)g(Yg)

Read as: g applied to the term capital Y applied to g

Means: g applied to the term capital Y applied to g

2 occurrences in this chapter

Equation form expr-c539f4c197e57dfb

n+1¯(T,⟨0¯,G⟩)≡⟨n+1¯,F(n+1¯)⟩\num{n+1}(T, \tuple{\num{0}, G}) \equiv \tuple{\num{n+1}, F(\num{n+1})}

Read as: the Church numeral for n plus one applied to capital T and the initial pair of the Church numeral zero and capital G is beta equivalent to the pair of the Church numeral for n plus one and capital F applied to that numeral

Means: the Church numeral for n plus one applied to capital T and the initial pair of the Church numeral zero and capital G is beta equivalent to the pair of the Church numeral for n plus one and capital F applied to that numeral

1 occurrence in this chapter

Equation form expr-c662fb992708cb56

λxy.xxyxλz.xz\lambd[xy][xxyx \lambd[z][xz]]

Read as: lambda x, then lambda y, with body x applied successively to x, y, x, and the abstraction lambda z with body x applied to z

Means: lambda x, then lambda y, with body x applied successively to x, y, x, and the abstraction lambda z with body x applied to z

1 occurrence in this chapter

Equation form expr-c8bbb88c1ea1e57a

IsASubterm\fn{IsASubterm}

Read as: Is A Subterm

Means: Is A Subterm

1 occurrence in this chapter

Equation form expr-c9961da8e760d85c

D(M,N)(0¯)↠MD(M,N)(\num{0}) \red M

Read as: capital D applied to capital M and capital N, then to the Church numeral zero, beta reduces to capital M

Means: capital D applied to capital M and capital N, then to the Church numeral zero, beta reduces to capital M

1 occurrence in this chapter

Equation form expr-ca978112ca1bbdca

aa

Read as: a

Means: a

1 occurrence in this chapter

Equation form expr-cb834f72b616517f

M↠NM \red N

Read as: capital M beta reduces to capital N

Means: capital M beta reduces to capital N

1 occurrence in this chapter

Equation form expr-cb839aa1a91f5c9e

λx.g(x,k)\lambd[x][g(x,k)]

Read as: lambda x, with body g of x and k

Means: lambda x, with body g of x and k

1 occurrence in this chapter

Equation form expr-cc927341266dfe87

[x/N]M[x/N]M

Read as: open square bracket, x slash capital N, close square bracket, followed by capital M

Means: open square bracket, x slash capital N, close square bracket, followed by capital M

1 occurrence in this chapter

Equation form expr-cd0aa9856147b6c5

gg

Read as: g

Means: g

9 occurrences in this chapter

Equation form expr-cd5f54466703d5af

fn(y)f^n(y)

Read as: the n fold iterate of f applied to y

Means: the n fold iterate of f applied to y

1 occurrence in this chapter

Equation form expr-cec4b8919e5f12a5

P′P'

Read as: capital P prime

Means: capital P prime

4 occurrences in this chapter

Equation form expr-d073f13bc0b87b1d

m→¯\num{\vec m}

Read as: the corresponding list of Church numerals for m

Means: the corresponding list of Church numerals for m

1 occurrence in this chapter

Equation form expr-d18b2e1f58b5b65d

g(x,y)g(x, y)

Read as: g of x and y

Means: g of x and y

1 occurrence in this chapter

Equation form expr-d24ec8bc305d8434

(λx.xxy)(λx.xxy)→(λx.xxy)(λx.xxy)y→(λx.xxy)(λx.xxy)yy→…(\lambd[x][xxy])(\lambd[x][xxy]) & \redone (\lambd[x][xxy])(\lambd[x][xxy])y \\ & \redone (\lambd[x][xxy])(\lambd[x][xxy])yy \\ & \redone \dots

Read as: Start with lambda x, with body x applied to x and then y, applied to another copy of the same abstraction. One beta step gives the original self application, applied to y. Another beta step gives the original self application, applied to y and then y again. One step reductions continue in this pattern

Means: Start with lambda x, with body x applied to x and then y, applied to another copy of the same abstraction. One beta step gives the original self application, applied to y. Another beta step gives the original self application, applied to y and then y again. One step reductions continue in this pattern

1 occurrence in this chapter

Equation form expr-d309f64e845d867f

M(x,y,z)M(x, y, z)

Read as: capital M, open parenthesis, x comma y comma z, close parenthesis

Means: capital M, open parenthesis, x comma y comma z, close parenthesis

1 occurrence in this chapter

Equation form expr-d3d4feb97d64ae95

(λx.((MN)P))(\lambd[x][((MN)P)])

Read as: lambda x, with body the result of applying capital M to capital N, applied to capital P

Means: lambda x, with body the result of applying capital M to capital N, applied to capital P

1 occurrence in this chapter

Equation form expr-d4735e3a265e16ee

22

Read as: two

Means: two

1 occurrence in this chapter

Equation form expr-d7fd0cf2d5e69efb

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

Read as: capital Y equals lambda g, whose body is the abstraction lambda x with body g applied to the self application of x, applied to a second copy of that same abstraction

Means: capital Y equals lambda g, whose body is the abstraction lambda x with body g applied to the self application of x, applied to a second copy of that same abstraction

1 occurrence in this chapter

Equation form expr-d9b1567a52bb6c42

x1x_1

Read as: x subscript one

Means: x subscript one

1 occurrence in this chapter

Equation form expr-df92634da3a3e068

MiM_i

Read as: capital M subscript i

Means: capital M subscript i

1 occurrence in this chapter

Equation form expr-e14947c63ab5c942

D(M,N)D(M,N)

Read as: capital D applied to capital M and then capital N

Means: capital D applied to capital M and then capital N

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

λy.(x+y)\lambd[y][(x+y)]

Read as: lambda y, with body x plus y

Means: lambda y, with body x plus y

1 occurrence in this chapter

Equation form expr-e4d3caf41b363b7e

Numeral\fn{Numeral}

Read as: Numeral

Means: Numeral

1 occurrence in this chapter

Equation form expr-e533b9707d2fc77c

N↠MN \red M

Read as: capital N beta reduces to capital M

Means: capital N beta reduces to capital M

1 occurrence in this chapter

Equation form expr-e551de20e786b708

λxyz.M\lambd[xyz][M]

Read as: lambda x, then lambda y, then lambda z, with innermost body capital M

Means: lambda x, then lambda y, then lambda z, with innermost body capital M

1 occurrence in this chapter

Equation form expr-e632b7095b0bf32c

TT

Read as: capital T

Means: capital T

2 occurrences in this chapter

Equation form expr-e63f0f6fdcd06cac

g(m)¯\overline {g(m)}

Read as: the Church numeral for g of m

Means: the Church numeral for g of m

1 occurrence in this chapter

Equation form expr-ea69086296a86e29

⟨0¯,F(0¯)⟩,⟨1¯,F(1¯)⟩,…,\tuple{\num 0, F(\num 0)}, \tuple{\num 1, F(\num 1)}, \dots,

Read as: the ordered pair of the Church numeral zero and capital F applied to that numeral; the ordered pair of the Church numeral one and capital F applied to that numeral; and so on

Means: the ordered pair of the Church numeral zero and capital F applied to that numeral; the ordered pair of the Church numeral one and capital F applied to that numeral; and so on

1 occurrence in this chapter

Equation form expr-eaecc8d701f26335

mn−1m_{n-1}

Read as: m subscript n minus one

Means: m subscript n minus one

1 occurrence in this chapter

Equation form expr-ebd225f165c0ba97

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

Read as: lambda x, with body x

Means: lambda x, with body x

1 occurrence in this chapter

Equation form expr-eee9da921ae691af

H(S(n¯))H(S(\num{n}))

Read as: capital H applied to the result of applying capital S to the Church numeral for n

Means: capital H applied to the result of applying capital S to the Church numeral for n

1 occurrence in this chapter

Equation form expr-ef0bd2cbdc2d86f5

λ(x,y).(x+y)\lambd[(x,y)][(x+y)]

Read as: the proposed abstraction lambda, binding the pair x comma y, with body x plus y

Means: the proposed abstraction lambda, binding the pair x comma y, with body x plus y

1 occurrence in this chapter

Equation form expr-ef3ebca2f4bdc229

P→P′P \redone P'

Read as: capital P beta reduces in one step to capital P prime

Means: capital P beta reduces in one step to capital P prime

1 occurrence in this chapter

Equation form expr-f3f3804480e8551a

β\beta

Read as: beta

Means: beta

10 occurrences in this chapter

Equation form expr-f67ab10ad4e4c531

FF

Read as: capital F

Means: capital F

11 occurrences in this chapter

Equation form expr-f717e078e4d12cb2

Xm0¯…mn−1¯X \num{m_0} \dots \num{m_{n-1}}

Read as: capital X applied successively to the Church numerals for m subscript zero through m subscript n minus one

Means: capital X applied successively to the Church numerals for m subscript zero through m subscript n minus one

1 occurrence in this chapter

Equation form expr-f7e71329e81956d2

N↠PN \red P

Read as: capital N beta reduces to capital P

Means: capital N beta reduces to capital P

1 occurrence in this chapter

Equation form expr-f8cba426b94bcfbf

T(u)=⟨S((u)0),H((u)0,(u)1)⟩.T(u) = \tuple{S((u)_0), H((u)_0,(u)_1)}.

Read as: capital T applied to u equals the ordered pair whose first component is capital S applied to the first component of u, and whose second component is capital H applied to the first and second components of u, in that order

Means: capital T applied to u equals the ordered pair whose first component is capital S applied to the first component of u, and whose second component is capital H applied to the first and second components of u, in that order

1 occurrence in this chapter

Equation form expr-f929041d6d33af68

n+1¯(T,⟨0¯,G⟩)≡T(n¯(T,⟨0¯,G⟩))≡T(⟨n¯,F(n¯)⟩)≡⟨n+1¯,H(n¯,F(n¯))⟩≡⟨n+1¯,F(n+1¯)⟩.\num{n+1} (T, \tuple{\num 0, G}) & \equiv T(\num{n} (T, \tuple{\num 0, G})) \\ & \equiv T( \tuple{\num{n}, F(\num{n})}) \\ & \equiv \tuple{\num{n+1}, H(\num{n}, F(\num{n}))} \\ & \equiv \tuple{\num{n+1}, F(\num{n+1})}.

Read as: the Church numeral for n plus one applied to capital T and the initial pair of the Church numeral zero and capital G is beta equivalent to capital T applied after n iterations on that initial pair. This is beta equivalent to capital T applied to the pair of the Church numeral for n and capital F applied to that numeral. This is beta equivalent to the pair of the Church numeral for n plus one and capital H applied to the Church numeral for n and capital F applied to that numeral. Finally, this is beta equivalent to the pair of the Church numeral for n plus one and capital F applied to that numeral

Means: the Church numeral for n plus one applied to capital T and the initial pair of the Church numeral zero and capital G is beta equivalent to capital T applied after n iterations on that initial pair. This is beta equivalent to capital T applied to the pair of the Church numeral for n and capital F applied to that numeral. This is beta equivalent to the pair of the Church numeral for n plus one and capital H applied to the Church numeral for n and capital F applied to that numeral. Finally, this is beta equivalent to the pair of the Church numeral for n plus one and capital F applied to that numeral

1 occurrence in this chapter

Equation form expr-f9383901eebb1eca

diag(x)=xx\fn{diag}(x) = xx

Read as: diagonal of x equals x applied to itself

Means: diagonal of x equals x applied to itself

1 occurrence in this chapter

Equation form expr-f99273cd05fa204e

g0,g_0,

Read as: g subscript zero,

Means: g subscript zero,

1 occurrence in this chapter

Equation form expr-f9e012396be65db0

llll

Read as: l applied to itself

Means: l applied to itself

1 occurrence in this chapter

Equation form expr-f9e8714de7a28837

(g(x))y=fx(y)=x+y(g(x))y = f_x(y) = x+y

Read as: g of x applied to y equals f subscript x of y, which equals x plus y

Means: g of x applied to y equals f subscript x of y, which equals x plus y

1 occurrence in this chapter

Equation form expr-fa7e89041b7dc09f

(λx.M)N(\lambd[x][M])N

Read as: the abstraction lambda x, with body capital M, applied to capital N

Means: the abstraction lambda x, with body capital M, applied to capital N

2 occurrences in this chapter

Equation form expr-fb4344dcbac88869

[N/x]M[N/x]M

Read as: open square bracket, capital N slash x, close square bracket, followed by capital M

Means: open square bracket, capital N slash x, close square bracket, followed by capital M

1 occurrence in this chapter

Equation form expr-fbeb608737cf8ff4

M↠N2M \red N_2

Read as: capital M beta reduces to capital N subscript two

Means: capital M beta reduces to capital N subscript two

2 occurrences in this chapter

Equation form expr-fd15e3089f2a7e5b

f(2)f(2)

Read as: f of two

Means: f of two

1 occurrence in this chapter

Equation form expr-fd5059e32d8d3b14

F(n+1¯)≡H(n¯,F(n¯))F(\num{n+1}) \equiv H(\num{n}, F(\num{n}))

Read as: capital F applied to the Church numeral for n plus one is beta equivalent to capital H applied to the Church numeral for n and then capital F applied to that numeral

Means: capital F applied to the Church numeral for n plus one is beta equivalent to capital H applied to the Church numeral for n and then capital F applied to that numeral

1 occurrence in this chapter

Equation form expr-fe6931045ae1d37a

ReductionSequence\fn{ReductionSequence}

Read as: Reduction Sequence

Means: Reduction Sequence

1 occurrence in this chapter

Equation form expr-ffaa0ad23479bca8

N1N_1

Read as: capital N subscript one

Means: capital N subscript one

3 occurrences in this chapter

A three step beta reduction to y

The first example substitutes the identity abstraction for both occurrences of x, then contracts the two resulting identity applications in order. The final term is y. Every intermediate term and one step arrow is spoken in the accompanying formula.

Source

A growing beta reduction sequence

A self application of lambda x with body x applied to x and then y reproduces itself with one extra final argument y at each step. Two steps are displayed, followed by an ellipsis. The sequence is not presented as terminating.

Source

The Church Rosser property

If one term beta reduces to two terms, there is a common term to which each of those two terms beta reduces. Both paths point from the original term to descendants, and then from those descendants to the common descendant.

Source

Uniqueness of normal form

If a term has a normal form, that form is unique under the chapter's convention of identifying terms that differ only by bound variable renaming. The source proof uses Church Rosser: two normal forms can share a reduct only by already being the same term.

Source

Curried first projection applied to two arguments

Apply lambda x, then lambda y, with body x, to capital M and then capital N. The first beta step returns lambda y with body capital M, applied to capital N. The second beta step returns capital M. Bound variables are understood to have been renamed to avoid capture, as specified earlier in the chapter.

Source

Successive applications of a curried abstraction

The displayed chain applies a nested abstraction to n arguments, eliminating one binder at a time by capture avoiding substitution. The first intermediate substitution and the final nested substitution are retained. The source repeats a reduction sign across a line break and changes the body name from capital N to capital P in the last line; those source issues are disclosed, not silently rewritten.

Source

Definition of Church numerals

The Church numeral for n binds a function variable x and an initial value variable y, then applies x to y n times. Numerals are lambda terms in normal form. The count n refers to the applications of x in the body, not to the binder itself.

Source

Lambda definability of a partial function

A term lambda defines a partial numerical function when applying it to Church numerals beta reduces to the numeral of the function value whenever defined, and has no normal form on undefined inputs. The source calls the function n ary but indexes k arguments, and includes a stray comma in the undefined-input term; these are preserved source caveats.

Source

Lambda definability characterizes partial computability

A numerical function is partial computable if and only if some lambda term lambda defines it. This theorem asserts both directions; the following two sections treat them separately.

Source

Lambda definable partial functions are computable

The proof searches a finitely branching tree of all one step beta reductions, increasing the path length. If it reaches a Church numeral, it returns the represented number. The source outlines primitive recursive coding relations but leaves their routine details unexpanded. An undefined input is not detected by a terminating test; the search may continue forever.

Source

Computable partial functions are lambda definable

The proof reduces the task to representing initial functions and closure under composition, primitive recursion, and unbounded search. It appeals to Kleene's normal form theorem. Subsequent sections provide the constructions; no additional proof is inserted here.

Source

Lambda definability of initial functions

The lemma states that zero, successor, and the projections are lambda definable. The successor construction adds one application to a Church iterator, and each projection returns its selected argument. The source identifies the zero function with the Church numeral zero itself, a distinction requiring the recorded source caveat.

Source

Closure under composition

Given terms representing h and the functions g with indices zero through k minus one, define capital F by applying capital H to the results of the corresponding capital G terms on the same argument list. Applications remain left associated; function composition is not multiplication.

Source

Primitive recursion equations with parameters

The first row supplies the base value at zero. The second supplies a successor equation. Its first argument to h is written z, although the recursion variable on the left is x. The exact source formula is preserved and the mismatch is disclosed.

Source

Lambda term equations with numerical first argument

The two rows replace numerical inputs by Church numerals and equality by beta equivalence. Extra parameters are passed unchanged. The surrounding prose names capital G prime and capital H prime, while these rows name unprimed capital G and capital H; the source notation inconsistency is recorded.

Source

Absorbing parameters into lambda abstractions

The display gives base and successor equations for capital F, then defines capital G and capital H by abstractions over the parameter list. Every application in the definition of capital H is retained, including the source's extra u argument to v. The edition does not silently replace that construction.

Source

Representing ordered pairs by a lambda term

There is a term capital D whose first two arguments select the components. Applying the resulting term to the Church numeral zero yields its first component; applying it to the Church numeral one yields its second. The proof defines the constant-function combinator capital K, then capital D.

Source

Two projection calculations for the pair representation

The first row evaluates capital D on numeral zero and returns capital M. The second evaluates it on numeral one and returns capital N after an intermediate capital K application. The two rows are separate directed reduction chains, not premises of an inference rule.

Source

Closure under primitive recursion

The construction iterates a pair-update term capital T using Church numerals. Each pair records the current numeral and current recursively computed term. Capital F retrieves the second component after the requested number of iterations. The source proves base and step equations by induction.

Source

Target base and successor equations

Capital F on the Church numeral zero is beta equivalent to capital G. Capital F on the Church numeral for n plus one is beta equivalent to capital H applied to the Church numeral for n and the preceding value capital F of that numeral. The equations are required for every natural number n.

Source

Inductive verification of the recursive output component

Five displayed stages unfold capital F, separate the final iteration of capital T, replace the preceding iterator value using induction, expand the pair update, and select the second component. The first connector is directed beta reduction; the remaining connectors are beta equivalence.

Source

Inductive verification of the entire updated pair

The four displayed stages separate the final update, substitute the induction hypothesis, expand capital T, and replace the second component using the recursion equation. Every connector in this chain is beta equivalence.

Source

The fixed point self application calculation

The term k is a self application of lambda x with body g applied to the self application of x. One directed reduction yields g applied to that same abstraction self application, which is g applied to k. This is the source calculation underlying the subsequent fixed point combinators.

Source

Closure under minimization

For a lambda definable two argument function f, the least-zero search defining g is asserted lambda definable. The proof uses a fixed point to repeat the search after a nonzero test result. Its unexpected primitive recursive assumption and its otherwise clause for possibly undefined tests are explicitly recorded source limitations, rather than silently strengthened hypotheses.

Source

The fixed point equation on a numeral

Capital H on the Church numeral for n is beta equivalent to capital U applied to capital H and that numeral, and then beta reduces to capital D applied to the current numeral, recursive successor search, and current test value. The test result determines which of the first two arguments is returned.

Source

Cross-reference reference-000793

the Church Rosser theorem

Source occurrence

Source disclosures