Lambda calculus

Lambda Calculus Syntax

Equation form expr-02c0bbc9f17e17b0

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

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

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

4 occurrences in this chapter

Equation form expr-03b168278337bc4d

FV(M¯0)=FV(M¯1)FV(\rep{M}[0]) = FV(\rep{M}[1])

Read as: the free variables of representative zero of class capital M, end free variable set equals the free variables of representative one of class capital M, end free variable set

Means: the free variables of representative zero of class capital M, end free variable set equals the free variables of representative one of class capital M, end free variable set

1 occurrence in this chapter

Equation form expr-050a47f60e228baf

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

Read as: Lambda x, whose body applies the abstraction lambda y with body y applied to x, to z, is applied to v. Contracting the outermost application in one beta step gives lambda y with body y applied to v, applied to z

Means: Lambda x, whose body applies the abstraction lambda y with body y applied to x, to z, is applied to v. Contracting the outermost application in one beta step gives lambda y with body y applied to v, applied to z

1 occurrence in this chapter

Equation form expr-054d5cacb7ab0427

λx.N′=αλz.N′[z/x]\lambd[x][N'] \aeq \lambd[z][\Subst{N'}{z}{x}]

Read as: lambda x, with body capital N prime, end abstraction is alpha equivalent to lambda z, with body the substitution of z for free x in capital N prime, end substitution, end abstraction

Means: lambda x, with body capital N prime, end abstraction is alpha equivalent to lambda z, with body the substitution of z for free x in capital N prime, end substitution, end abstraction

1 occurrence in this chapter

Equation form expr-063e16ef53b0df02

λm.m\lambd[m][m]

Read as: lambda lowercase m, with body lowercase m, end abstraction

Means: lambda lowercase m, with body lowercase m, end abstraction

1 occurrence in this chapter

Equation form expr-06cbb32c58964272

(λx.N)Q→βN[Q/x](\lambd[x][N])Q \bredone \Subst{N}{Q}{x}

Read as: the application of the class denoted by lambda x with body capital N to class capital Q beta contracts in one step to substitution of class capital Q for free x in class capital N

Means: the application of the class denoted by lambda x with body capital N to class capital Q beta contracts in one step to substitution of class capital Q for free x in class capital N

1 occurrence in this chapter

Equation form expr-081205724d9cfbf2

M′[R′/y]=αM′′[R′′/y]\Subst{M'}{R'}{y} \aeq \Subst{M''}{R''}{y}

Read as: the substitution of capital R prime for free y in capital M prime, end substitution is alpha equivalent to the substitution of capital R double prime for free y in capital M double prime, end substitution

Means: the substitution of capital R prime for free y in capital M prime, end substitution is alpha equivalent to the substitution of capital R double prime for free y in capital M double prime, end substitution

1 occurrence in this chapter

Equation form expr-08c74b35f31a26da

λx.Mx→ηM provided x∉FV(M)\lambd[x][M x] \eredone M \text{ provided } x \notin FV(M)

Read as: lambda x, with body the application of capital M to x, end application, end abstraction eta contracts in one step to capital M, provided x is not free in capital M

Means: lambda x, with body the application of capital M to x, end application, end abstraction eta contracts in one step to capital M, provided x is not free in capital M

1 occurrence in this chapter

Equation form expr-08dacf0f9d78188a

λ\lambd

Read as: lambda

Means: lambda

2 occurrences in this chapter

Equation form expr-08f271887ce94707

MM

Read as: capital M

Means: capital M

60 occurrences in this chapter

Equation form expr-08fb5113e396983b

λx.gx\lambd[x][g x]

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

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

1 occurrence in this chapter

Equation form expr-0a207ebf1d6710d1

M=NM \equal N

Read as: capital M is beta equivalent to capital N

Means: capital M is beta equivalent to capital N

7 occurrences in this chapter

Equation form expr-0aa53d46354bee12

λx.N¯\lambd[x][\rep{N}]

Read as: lambda x, with body a representative of class capital N, end abstraction

Means: lambda x, with body a representative of class capital N, end abstraction

1 occurrence in this chapter

Equation form expr-0b57522174f85b4d

RQQ′R Q Q'

Read as: relation capital R holds from capital Q to capital Q prime

Means: relation capital R holds from capital Q to capital Q prime

1 occurrence in this chapter

Equation form expr-0bd0f0335baa0da8

v0\Obj{v_0}

Read as: v subscript zero

Means: v subscript zero

1 occurrence in this chapter

Equation form expr-0c8820d81c53436b

R′′R''

Read as: capital R double prime

Means: capital R double prime

3 occurrences in this chapter

Equation form expr-0cf1d4508cdd0d98

y∈FV(Q)y \in \FV{Q}

Read as: y is free in capital Q

Means: y is free in capital Q

1 occurrence in this chapter

Equation form expr-0e11d71666303b87

y≠xy \neq x

Read as: y is not equal to x

Means: y is not equal to x

1 occurrence in this chapter

Equation form expr-0f0cb949c588797f

N′[z/x]\Subst{N'}{z}{x}

Read as: the substitution of z for free x in capital N prime, end substitution

Means: the substitution of z for free x in capital N prime, end substitution

2 occurrences in this chapter

Equation form expr-0f47d125c8abb33b

P→αP′P \aconvone P'

Read as: capital P changes one bound variable to give capital P prime

Means: capital P changes one bound variable to give capital P prime

1 occurrence in this chapter

Equation form expr-136ab36db1dc0f91

N=ON \equal O

Read as: capital N is beta equivalent to capital O

Means: capital N is beta equivalent to capital O

1 occurrence in this chapter

Equation form expr-13a9c1634d12df54

FV(λx.(λy.(λz.xy)z)y)\FV{\lambd[x][(\lambd[y][(\lambd[z][x y]) z]) y]}

Read as: the free variables of lambda x, with body the application of lambda y, with body the application of lambda z, with body the application of x to y, end application, end abstraction to z, end application, end abstraction to y, end application, end abstraction, end free variable set

Means: the free variables of lambda x, with body the application of lambda y, with body the application of lambda z, with body the application of x to y, end application, end abstraction to z, end application, end abstraction to y, end application, end abstraction, end free variable set

1 occurrence in this chapter

Equation form expr-15beea0f82829592

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

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

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

2 occurrences in this chapter

Equation form expr-18a73cfddd6ad3fb

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

Read as: open parenthesis, lambda x, dot, open parenthesis, lambda y, dot, open parenthesis, open parenthesis, open parenthesis, open parenthesis, x x, close parenthesis, y, close parenthesis, x, close parenthesis, open parenthesis, lambda z, dot, open parenthesis, x z, close parenthesis, close parenthesis, close parenthesis, close parenthesis, close parenthesis, period

Means: open parenthesis, lambda x, dot, open parenthesis, lambda y, dot, open parenthesis, open parenthesis, open parenthesis, open parenthesis, x x, close parenthesis, y, close parenthesis, x, close parenthesis, open parenthesis, lambda z, dot, open parenthesis, x z, close parenthesis, close parenthesis, close parenthesis, close parenthesis, close parenthesis, period

1 occurrence in this chapter

Equation form expr-19c9de3506e870f4

M=ηNM \equal[\eta] N

Read as: capital M is equivalent, under beta equivalence extended by eta conversion, to capital N

Means: capital M is equivalent, under beta equivalence extended by eta conversion, to capital N

3 occurrences in this chapter

Equation form expr-1b16b1df538ba12d

nn

Read as: n

Means: n

3 occurrences in this chapter

Equation form expr-1b6218573a84d84e

λy.x(λx.x)[(λy.xy)/x]\Subst{\lambd[y][x(\lambd[x][x])]}{(\lambd[y][xy])}{x}

Read as: the substitution of lambda y, with body the application of x to y, end application, end abstraction for free x in lambda y, with body the application of x to lambda x, with body x, end abstraction, end application, end abstraction, end substitution

Means: the substitution of lambda y, with body the application of x to y, end application, end abstraction for free x in lambda y, with body the application of x to lambda x, with body x, end abstraction, end application, end abstraction, end substitution

1 occurrence in this chapter

Equation form expr-1bc9009ffb52af99

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

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

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

1 occurrence in this chapter

Equation form expr-1bee337b70fa3802

FV(M)\FV{M}

Read as: the free variables of capital M, end free variable set

Means: the free variables of capital M, end free variable set

1 occurrence in this chapter

Equation form expr-1ce2922c73b3ce7c

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

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

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

1 occurrence in this chapter

Equation form expr-1d8d6a792845c3ac

x∉FV(Q)x \notin \FV{Q}

Read as: x is not free in capital Q

Means: x is not free in capital Q

1 occurrence in this chapter

Equation form expr-1fb17be39daaa223

x,y,zx,y,z

Read as: x, y, z

Means: x, y, z

2 occurrences in this chapter

Equation form expr-207a2868af9988e2

x∈FV(P)x \in \FV{P}

Read as: x is free in capital P

Means: x is free in capital P

1 occurrence in this chapter

Equation form expr-234f1ed048cf69ae

y∈FV(N)y \in \FV{N}

Read as: y is free in capital N

Means: y is free in capital N

1 occurrence in this chapter

Equation form expr-23d89c48e90309ce

R′′=αRR'' \aeq R

Read as: capital R double prime is alpha equivalent to capital R

Means: capital R double prime is alpha equivalent to capital R

1 occurrence in this chapter

Equation form expr-2459e5bee10e7d13

P¯Q¯\rep{P}\rep{Q}

Read as: the application of a representative of class capital P to a representative of class capital Q, end application

Means: the application of a representative of class capital P to a representative of class capital Q, end application

1 occurrence in this chapter

Equation form expr-252f10c83610ebca

ff

Read as: f

Means: f

13 occurrences in this chapter

Equation form expr-2738d1657e6c9870

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

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

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

1 occurrence in this chapter

Equation form expr-277257c7047b40d0

FV(M[N/x])=FV(M)\FV{\Subst{M}{N}{x}} = \FV{M}

Read as: the free variables of the substitution of capital N for free x in capital M, end substitution, end free variable set equals the free variables of capital M, end free variable set

Means: the free variables of the substitution of capital N for free x in capital M, end substitution, end free variable set equals the free variables of capital M, end free variable set

1 occurrence in this chapter

Equation form expr-28280bcf72ec2165

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

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

Means: lambda x, with body capital N, end abstraction

8 occurrences in this chapter

Equation form expr-28489f4d36a4acda

FΓ(x)=Γ(x)FΓ(PQ)=FΓ(P)FΓ(Q)FΓ(λx.N)=λ.Fx,Γ(N)F_\Gamma(x) &= \Gamma(x) \\ F_\Gamma(PQ) &= F_\Gamma(P)F_\Gamma(Q) \\ F_\Gamma(\lambd[x][N]) &= \lambd[][F_{x,\Gamma}(N)]

Read as: Translation capital F, with environment Gamma, is defined by three equations. First, capital F subscript Gamma of x equals the position of x in Gamma. Second, capital F subscript Gamma of the application of capital P to capital Q equals the application of capital F subscript Gamma of capital P to capital F subscript Gamma of capital Q. Third, capital F subscript Gamma of lambda x with body capital N equals an unnamed abstraction whose body is capital F, with environment x prepended to Gamma, of capital N. End equations

Means: Translation capital F, with environment Gamma, is defined by three equations. First, capital F subscript Gamma of x equals the position of x in Gamma. Second, capital F subscript Gamma of the application of capital P to capital Q equals the application of capital F subscript Gamma of capital P to capital F subscript Gamma of capital Q. Third, capital F subscript Gamma of lambda x with body capital N equals an unnamed abstraction whose body is capital F, with environment x prepended to Gamma, of capital N. End equations

1 occurrence in this chapter

Equation form expr-2a068fe5130a6f11

M[R/y]\Subst{M}{R}{y}

Read as: the substitution of capital R for free y in capital M, end substitution

Means: the substitution of capital R for free y in capital M, end substitution

3 occurrences in this chapter

Equation form expr-2a83f670a3935ea4

M′=αMM' \aeq M

Read as: capital M prime is alpha equivalent to capital M

Means: capital M prime is alpha equivalent to capital M

1 occurrence in this chapter

Equation form expr-2b57a66d247e028d

M[R′/y]\Subst{M}{R'}{y}

Read as: the substitution of capital R prime for free y in capital M, end substitution

Means: the substitution of capital R prime for free y in capital M, end substitution

1 occurrence in this chapter

Equation form expr-2cb5560b48621a3c

=ext\equal[ext]

Read as: beta equivalence extended by extensionality

Means: beta equivalence extended by extensionality

1 occurrence in this chapter

Equation form expr-2d711642b726b044

xx

Read as: x

Means: x

42 occurrences in this chapter

Equation form expr-2e80839badcead2f

→β\bredone

Read as: one step beta contraction

Means: one step beta contraction

5 occurrences in this chapter

Equation form expr-2eb58d37261708a1

M↠βηNM \bered N

Read as: capital M beta eta reduces in zero or more steps to capital N

Means: capital M beta eta reduces in zero or more steps to capital N

2 occurrences in this chapter

Equation form expr-2fa5e30aeba480e7

x∈FV(N)x \in \FV{N}

Read as: x is free in capital N

Means: x is free in capital N

1 occurrence in this chapter

Equation form expr-32e73a075181d28a

λx.x[y/x]\Subst{\lambd[x][x]}{y}{x}

Read as: the substitution of y for free x in lambda x, with body x, end abstraction, end substitution

Means: the substitution of y for free x in lambda x, with body x, end abstraction, end substitution

1 occurrence in this chapter

Equation form expr-33546aeed2bed3fe

λb.λa.bc\lambd[b][\lambd[a][b c]]

Read as: lambda b, with body lambda a, with body the application of b to c, end application, end abstraction, end abstraction

Means: lambda b, with body lambda a, with body the application of b to c, end application, end abstraction, end abstraction

1 occurrence in this chapter

Equation form expr-3362fe6c239f4966

(λ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 the abstraction lambda x, whose body is x applied to x and then to y, applied to the identity abstraction lambda z with body z. One beta contraction gives that identity abstraction applied to itself, and then to y. One beta contraction gives the identity abstraction applied to y. One beta contraction gives y. End reduction chain

Means: Start with the abstraction lambda x, whose body is x applied to x and then to y, applied to the identity abstraction lambda z with body z. One beta contraction gives that identity abstraction applied to itself, and then to y. One beta contraction gives the identity abstraction applied to y. One beta contraction gives y. End reduction chain

1 occurrence in this chapter

Equation form expr-347c928784fb6ae3

(PQ)→α(P′Q)(PQ) \aconvone (P'Q)

Read as: the application of capital P to capital Q, end application changes one bound variable to give the application of capital P prime to capital Q, end application

Means: the application of capital P to capital Q, end application changes one bound variable to give the application of capital P prime to capital Q, end application

1 occurrence in this chapter

Equation form expr-348d9961c3ef935e

FV(M¯)FV(\rep{M})

Read as: the free variables of a representative of class capital M, end free variable set

Means: the free variables of a representative of class capital M, end free variable set

1 occurrence in this chapter

Equation form expr-35b907cb05c2dfeb

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

Read as: lambda x, dot, capital M, capital N, capital P, with no enclosing parentheses

Means: lambda x, dot, capital M, capital N, capital P, with no enclosing parentheses

1 occurrence in this chapter

Equation form expr-3794ce84ac332257

λz.N′[z/x][R/y]\Subst{\lambd[z][\Subst{N'}{z}{x}]}{R}{y}

Read as: the substitution of capital R for free y in lambda z, with body the substitution of z for free x in capital N prime, end substitution, end abstraction, end substitution

Means: the substitution of capital R for free y in lambda z, with body the substitution of z for free x in capital N prime, end substitution, end abstraction, end substitution

1 occurrence in this chapter

Equation form expr-385bc1d2ff3c62e4

M=αM′M \aeq M'

Read as: capital M is alpha equivalent to capital M prime

Means: capital M is alpha equivalent to capital M prime

1 occurrence in this chapter

Equation form expr-39573eff5ddfb0a9

y[N/x]=y\Subst{y}{N}{x} = y

Read as: the substitution of capital N for free x in y, end substitution equals y

Means: the substitution of capital N for free x in y, end substitution equals y

1 occurrence in this chapter

Equation form expr-39d2df82f526a166

RPP′R P P'

Read as: relation capital R holds from capital P to capital P prime

Means: relation capital R holds from capital P to capital P prime

1 occurrence in this chapter

Equation form expr-39f9dce10b8af464

M[y/x][x/y]=M\Subst{\Subst{M}{y}{x}}{x}{y} = M

Read as: the substitution of x for free y in the substitution of y for free x in capital M, end substitution, end substitution equals capital M

Means: the substitution of x for free y in the substitution of y for free x in capital M, end substitution, end substitution equals capital M

1 occurrence in this chapter

Equation form expr-3a06509c75170744

(λy.P)[N/x]=λy.P[N/x]\Subst{(\lambd[y][P])}{N}{x} = \lambd[y][\Subst{P}{N}{x}]

Read as: the substitution of capital N for free x in lambda y, with body capital P, end abstraction, end substitution equals lambda y, with body the substitution of capital N for free x in capital P, end substitution, end abstraction

Means: the substitution of capital N for free x in lambda y, with body capital P, end abstraction, end substitution equals lambda y, with body the substitution of capital N for free x in capital P, end substitution, end abstraction

1 occurrence in this chapter

Equation form expr-3adf93cb34ed49ca

λx.N[R/y]\Subst{\lambd[x][N]}{R}{y}

Read as: substitution of class capital R for free y in the class denoted by lambda x, with body capital N, end abstraction

Means: substitution of class capital R for free y in the class denoted by lambda x, with body capital N, end abstraction

1 occurrence in this chapter

Equation form expr-3b7fb64f2f6f0206

z∉FV(R)z \notin FV(R)

Read as: z is not free in capital R

Means: z is not free in capital R

1 occurrence in this chapter

Equation form expr-3bd40cb291628762

FV(λy.N[y/x])=FV(N[y/x])∖{y}=((FV(N)∖{x})∪{y})∖{y} by the substitution theorem for a variable free in the term=FV(N)∖{x}=FV(λx.N)\FV{\lambd[y][\Subst{N}{y}{x}]} &= \FV{\Subst{N}{y}{x}} \setminus \{y\} \\ & = ((\FV{N} \setminus \{x\}) \cup \{y\}) \setminus \{y\} && \text{ by \olref[sub]{thm:infv}} \\ & = \FV{N} \setminus \{x\} \\ & = \FV{\lambd[x][N]}

Read as: The free variables of lambda y with body capital N after substitution of y for free x equal the free variables of that substituted body with y removed. This equals the union of the free variables of capital N with x removed, and the singleton set containing y, with y then removed from the whole union, by the substitution theorem for a variable free in the term. This equals the free variables of capital N with x removed. This equals the free variables of lambda x with body capital N. End equation chain

Means: The free variables of lambda y with body capital N after substitution of y for free x equal the free variables of that substituted body with y removed. This equals the union of the free variables of capital N with x removed, and the singleton set containing y, with y then removed from the whole union, by the substitution theorem for a variable free in the term. This equals the free variables of capital N with x removed. This equals the free variables of lambda x with body capital N. End equation chain

1 occurrence in this chapter

Equation form expr-3c1f3438862ce45c

M¯\rep{M}

Read as: a representative of class capital M

Means: a representative of class capital M

2 occurrences in this chapter

Equation form expr-3de20430234ebb71

x∉FV(MN)x \notin FV(MN)

Read as: x is not free in the application of capital M to capital N, end application

Means: x is not free in the application of capital M to capital N, end application

1 occurrence in this chapter

Equation form expr-3e0534ff9dda7eeb

N′N'

Read as: capital N prime

Means: capital N prime

1 occurrence in this chapter

Equation form expr-3f4a61513c53648c

Q→αQ′Q \aconvone Q'

Read as: capital Q changes one bound variable to give capital Q prime

Means: capital Q changes one bound variable to give capital Q prime

1 occurrence in this chapter

Equation form expr-423c5e893aafcfd8

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

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

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

1 occurrence in this chapter

Equation form expr-4263dcca38a79bb1

R¯\rep{R}

Read as: a representative of class capital R

Means: a representative of class capital R

1 occurrence in this chapter

Equation form expr-4331381ecf41e713

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

Read as: the substitution of y for free x in capital M, end substitution

Means: the substitution of y for free x in capital M, end substitution

1 occurrence in this chapter

Equation form expr-45caa0f949630296

FV(PQ)=FV(P)∪FV(Q)\FV{PQ} = \FV{P} \cup \FV{Q}

Read as: the free variables of the application of capital P to capital Q, end application, end free variable set equals the union of the free variables of capital P, end free variable set and the free variables of capital Q, end free variable set

Means: the free variables of the application of capital P to capital Q, end application, end free variable set equals the union of the free variables of capital P, end free variable set and the free variables of capital Q, end free variable set

1 occurrence in this chapter

Equation form expr-4675b4292c1aff69

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

Read as: lambda x, dot, lambda y, dot, lambda z, dot, capital M

Means: lambda x, dot, lambda y, dot, lambda z, dot, capital M

1 occurrence in this chapter

Equation form expr-4893e9df8b5496eb

α\alpha

Read as: alpha

Means: alpha

27 occurrences in this chapter

Equation form expr-48ec837032cbb482

x∉FV(N)x \notin \FV{N}

Read as: x is not free in capital N

Means: x is not free in capital N

1 occurrence in this chapter

Equation form expr-4ae81572f06e1b88

QQ

Read as: capital Q

Means: capital Q

14 occurrences in this chapter

Equation form expr-4b5a67f2d028ca2b

Mx=NxMx \equal Nx

Read as: the application of capital M to x, end application is beta equivalent to the application of capital N to x, end application

Means: the application of capital M to x, end application is beta equivalent to the application of capital N to x, end application

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-4bf211aa1a4cc025

M=αNM \aeq N

Read as: capital M is alpha equivalent to capital N

Means: capital M is alpha equivalent to capital N

2 occurrences in this chapter

Equation form expr-4dbcfb1adc7a6192

z∉FV(N)z \notin \FV{N}

Read as: z is not free in capital N

Means: z is not free in capital N

1 occurrence in this chapter

Equation form expr-4e73a24d6dbb26ff

Λ\Lambda

Read as: capital lambda

Means: capital lambda

5 occurrences in this chapter

Equation form expr-4ea7275366105234

R=αR′R \aeq R'

Read as: capital R is alpha equivalent to capital R prime

Means: capital R is alpha equivalent to capital R prime

2 occurrences in this chapter

Equation form expr-505eb18fa728228d

=X\equal[X]

Read as: beta equivalence extended by rule capital X

Means: beta equivalence extended by rule capital X

1 occurrence in this chapter

Equation form expr-525ed932ff3a5484

y∉FV(N[y/x])y \notin \FV{\Subst{N}{y}{x}}

Read as: y is not free in the substitution of y for free x in capital N, end substitution

Means: y is not free in the substitution of y for free x in capital N, end substitution

1 occurrence in this chapter

Equation form expr-52d00aa042aca361

FΓ(M)≡FΓ(M′)F_\Gamma(M) \eqs F_\Gamma(M')

Read as: capital F subscript Gamma of capital M is syntactically identical to capital F subscript Gamma of capital M prime

Means: capital F subscript Gamma of capital M is syntactically identical to capital F subscript Gamma of capital M prime

1 occurrence in this chapter

Equation form expr-5364f82ab3240fba

Γ(x)\Gamma(x)

Read as: the position of x in Gamma

Means: the position of x in Gamma

2 occurrences in this chapter

Equation form expr-53aebbe1a4de6741

(MN)(MN)

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

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

2 occurrences in this chapter

Equation form expr-53d4deec55439449

x∉FV(N)x \notin FV(N)

Read as: x is not free in capital N

Means: x is not free in capital N

1 occurrence in this chapter

Equation form expr-566fc0a2da4d65f7

PQ[N/x]=(P[N/x])(Q[N/x])\Subst{PQ}{N}{x} = (\Subst{P}{N}{x}) (\Subst{Q}{N}{x})

Read as: the substitution of capital N for free x in the application of capital P to capital Q, end application, end substitution equals the application of the substitution of capital N for free x in capital P, end substitution to the substitution of capital N for free x in capital Q, end substitution, end application

Means: the substitution of capital N for free x in the application of capital P to capital Q, end application, end substitution equals the application of the substitution of capital N for free x in capital P, end substitution to the substitution of capital N for free x in capital Q, end substitution, end application

1 occurrence in this chapter

Equation form expr-57885e4c75965b23

Γ\Gamma

Read as: Gamma

Means: Gamma

9 occurrences in this chapter

Equation form expr-582fb3b50465a8e5

RNN′R N N'

Read as: relation capital R holds from capital N to capital N prime

Means: relation capital R holds from capital N to capital N prime

1 occurrence in this chapter

Equation form expr-583cf6290785d72c

λ\lambda

Read as: lowercase lambda

Means: lowercase lambda

4 occurrences in this chapter

Equation form expr-594e519ae499312b

zz

Read as: z

Means: z

4 occurrences in this chapter

Equation form expr-5960416eafca0295

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

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

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

2 occurrences in this chapter

Equation form expr-59a94416a2a319ca

η\eta

Read as: eta

Means: eta

10 occurrences in this chapter

Equation form expr-59ea38537bbaa083

Γ(z)\Gamma(z)

Read as: the position of z in Gamma

Means: the position of z in Gamma

1 occurrence in this chapter

Equation form expr-5a2b622063671c1b

Γ[1]\Gamma[1]

Read as: the variable at position one in Gamma

Means: the variable at position one in Gamma

1 occurrence in this chapter

Equation form expr-5c1cf7304072d4f8

FV(λx.N)=FV(N)∖{x}\FV{\lambd[x][N]} = \FV{N} \setminus \{x\}

Read as: the free variables of lambda x, with body capital N, end abstraction, end free variable set equals the free variables of capital N, end free variable set with x removed

Means: the free variables of lambda x, with body capital N, end abstraction, end free variable set equals the free variables of capital N, end free variable set with x removed

1 occurrence in this chapter

Equation form expr-5c62e091b8c0565f

PP

Read as: capital P

Means: capital P

19 occurrences in this chapter

Equation form expr-5dde896887f6754c

xxxx

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

Means: the application of x to x, end application

1 occurrence in this chapter

Equation form expr-5e99ae39a3dcfd6c

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

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

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

3 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

3 occurrences in this chapter

Equation form expr-5fea10b1c5e67a23

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

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

Means: lambda y, with body x, end abstraction

2 occurrences in this chapter

Equation form expr-5feceb66ffc86f38

00

Read as: zero

Means: zero

1 occurrence in this chapter

Equation form expr-6136a2b1bee16cb3

λx.fx=f\lambd[x][f x] \equal f

Read as: lambda x, with body the application of f to x, end application, end abstraction is declared equivalent by the added eta rule to f

Means: lambda x, with body the application of f to x, end application, end abstraction is declared equivalent by the added eta rule to f

1 occurrence in this chapter

Equation form expr-6221bd941a082f11

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

Read as: 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: 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-63fe3f3f6592ebc7

FV(λy.N[y/x])=FVN[y/x]∖{y}=FV(N)∖{x}by the substitution theorem for a variable not free in the term=FV(λx.N).\FV{\lambd[y][\Subst{N}{y}{x}]} & = FV{\Subst{N}{y}{x}} \setminus \{y\} \\ & = \FV{N} \setminus \{x\} && \text{by \olref[sub]{thm:notinfv}} \\ & = \FV{\lambd[x][N]}.

Read as: The free variables of lambda y with body capital N after substitution of y for free x equal the free variables of that substituted body with y removed. The source writes the letters F and V literally in this row. This equals the free variables of capital N with x removed, citing the substitution theorem for a variable not free in the term. This equals the free variables of lambda x with body capital N. End equation chain

Means: The free variables of lambda y with body capital N after substitution of y for free x equal the free variables of that substituted body with y removed. The source writes the letters F and V literally in this row. This equals the free variables of capital N with x removed, citing the substitution theorem for a variable not free in the term. This equals the free variables of lambda x with body capital N. End equation chain

1 occurrence in this chapter

Equation form expr-644013adb19040ad

λz.N\lambd[z][N]

Read as: lambda z, with body capital N, end abstraction

Means: lambda z, with body capital N, end abstraction

1 occurrence in this chapter

Equation form expr-64e1d6674ee83f37

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

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

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

2 occurrences in this chapter

Equation form expr-65b364bb82ea19d5

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

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

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

1 occurrence in this chapter

Equation form expr-69f4944311bc6a0d

→η\eredone

Read as: one step eta contraction

Means: one step eta contraction

3 occurrences in this chapter

Equation form expr-6bbccac981227e98

z∉FV(R)z \notin \FV{R}

Read as: z is not free in capital R

Means: z is not free in capital R

1 occurrence in this chapter

Equation form expr-6e331925df1c2302

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

Read as: the substitution of capital N for free x in x, end substitution equals capital N

Means: the substitution of capital N for free x in x, end substitution equals capital N

1 occurrence in this chapter

Equation form expr-7082050d06a3d44b

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

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

Means: lambda x, with body capital M, end abstraction

2 occurrences in this chapter

Equation form expr-70fd3696da78df35

(PQ)(PQ)

Read as: the application of capital P to capital Q, end application

Means: the application of capital P to capital Q, end application

7 occurrences in this chapter

Equation form expr-721575d946b455ec

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

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

Means: lambda x, with body capital M, end abstraction

6 occurrences in this chapter

Equation form expr-739539e1235aa458

y∈FV(P)y \in \FV{P}

Read as: y is free in capital P

Means: y is free in capital P

2 occurrences in this chapter

Equation form expr-752a4517b8b53d0a

MNPQMNPQ

Read as: the unparenthesized string capital M, capital N, capital P, capital Q

Means: the unparenthesized string capital M, capital N, capital P, capital Q

1 occurrence in this chapter

Equation form expr-760fab6bc12a96d3

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

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

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

1 occurrence in this chapter

Equation form expr-76a8c8c02bf83b7a

M′M'

Read as: capital M prime

Means: capital M prime

3 occurrences in this chapter

Equation form expr-77cc647105438652

λy.x(λw.vwx)[(uv)/x]\Subst{\lambd[y][x(\lambd[w][vwx])]}{(uv)}{x}

Read as: the substitution of the application of u to v, end application for free x in lambda y, with body the application of x to lambda w, with body the application of the application of v to w, end application to x, end application, end abstraction, end application, end abstraction, end substitution

Means: the substitution of the application of u to v, end application for free x in lambda y, with body the application of x to lambda w, with body the application of the application of v to w, end application to x, end application, end abstraction, end application, end abstraction, end substitution

1 occurrence in this chapter

Equation form expr-7854781e585c9b59

↠βη\bered

Read as: beta eta reduction in zero or more steps

Means: beta eta reduction in zero or more steps

2 occurrences in this chapter

Equation form expr-791f82d681fcae7a

fNfN

Read as: the application of f to capital N, end application

Means: the application of f to capital N, end application

2 occurrences in this chapter

Equation form expr-79d26653553df3e9

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

Read as: 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: 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

3 occurrences in this chapter

Equation form expr-7a8c7e35cb827563

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

Read as: the substitution of x for free y in the substitution of y for free x in capital N, end substitution, end substitution

Means: the substitution of x for free y in the substitution of y for free x in capital N, end substitution, end substitution

1 occurrence in this chapter

Equation form expr-7ab6979a96077910

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

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

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

1 occurrence in this chapter

Equation form expr-7c10234a5acf6817

λx.N→αλy.N[y/x]\lambd[x][N] \redone[\alpha] \lambd[y][\Subst{N}{y}{x}]

Read as: lambda x, with body capital N, end abstraction changes one bound variable to give lambda y, with body the substitution of y for free x in capital N, end substitution, end abstraction

Means: lambda x, with body capital N, end abstraction changes one bound variable to give lambda y, with body the substitution of y for free x in capital N, end substitution, end abstraction

1 occurrence in this chapter

Equation form expr-7d508f582fa45222

FV(M)=FV(N)\FV{M} = \FV{N}

Read as: the free variables of capital M, end free variable set equals the free variables of capital N, end free variable set

Means: the free variables of capital M, end free variable set equals the free variables of capital N, end free variable set

1 occurrence in this chapter

Equation form expr-7e6204dc5518dc5d

x∈FV(Q)x \in \FV{Q}

Read as: x is free in capital Q

Means: x is free in capital Q

1 occurrence in this chapter

Equation form expr-7f0e689dc723088e

λ.λ.01\lambd[][\lambd[][01]]

Read as: an unnamed lambda abstraction, whose body is an unnamed lambda abstraction, whose body applies de Bruijn index zero to de Bruijn index one; end inner abstraction; end outer abstraction

Means: an unnamed lambda abstraction, whose body is an unnamed lambda abstraction, whose body applies de Bruijn index zero to de Bruijn index one; end inner abstraction; end outer abstraction

1 occurrence in this chapter

Equation form expr-7f2679cd2c88e451

M→αM′M \aconvone M'

Read as: capital M changes one bound variable to give capital M prime

Means: capital M changes one bound variable to give capital M prime

1 occurrence in this chapter

Equation form expr-8021307faf3abead

λz.N[y/x]\Subst{\lambd[z][N]}{y}{x}

Read as: the substitution of y for free x in lambda z, with body capital N, end abstraction, end substitution

Means: the substitution of y for free x in lambda z, with body capital N, end abstraction, end substitution

1 occurrence in this chapter

Equation form expr-813fc2a50ed0558b

z∉FV(N′)z \notin FV(N')

Read as: z is not free in capital N prime

Means: z is not free in capital N prime

1 occurrence in this chapter

Equation form expr-858fa9055e3e3d8d

x∉FV(M)x \notin \FV{M}

Read as: x is not free in capital M

Means: x is not free in capital M

1 occurrence in this chapter

Equation form expr-8591914cae179a8e

w,Γw,\Gamma

Read as: the list with w prepended to Gamma

Means: the list with w prepended to Gamma

1 occurrence in this chapter

Equation form expr-86fa5a5b7a833ae8

PQPQ

Read as: the application of capital P to capital Q, end application

Means: the application of capital P to capital Q, end application

3 occurrences in this chapter

Equation form expr-8721b86268d9e793

x≠yx \neq y

Read as: x is not equal to y

Means: x is not equal to y

9 occurrences in this chapter

Equation form expr-899317a234d75815

PM=PNPM \equal PN

Read as: the application of capital P to capital M, end application is beta equivalent to the application of capital P to capital N, end application

Means: the application of capital P to capital M, end application is beta equivalent to the application of capital P to capital N, end application

1 occurrence in this chapter

Equation form expr-8a2ebe61053f024a

FV(x)={x}\FV{x} = \{x\}

Read as: the free variables of x form the singleton set containing x

Means: the free variables of x form the singleton set containing x

1 occurrence in this chapter

Equation form expr-8aa1b9aa30655097

P↠αPP \aconv P

Read as: capital P alpha converts to capital P

Means: capital P alpha converts to capital P

1 occurrence in this chapter

Equation form expr-8b0150d4ec261493

↠\red

Read as: the unlabelled zero or more step reduction arrow

Means: the unlabelled zero or more step reduction arrow

1 occurrence in this chapter

Equation form expr-8c15ecd9882309fc

P↠αQP \aconv Q

Read as: capital P alpha converts to capital Q

Means: capital P alpha converts to capital Q

2 occurrences in this chapter

Equation form expr-8c2574892063f995

RR

Read as: capital R

Means: capital R

6 occurrences in this chapter

Equation form expr-8ce86a6ae65d3692

NN

Read as: capital N

Means: capital N

23 occurrences in this chapter

Equation form expr-8e15ad994c118e86

FV(M)FV(M)

Read as: the free variables of capital M, end free variable set

Means: the free variables of capital M, end free variable set

1 occurrence in this chapter

Equation form expr-8e73391a5bed7e37

FV((λy.P)[N/x])==FV(λy.P[N/x])=FV(P[N/x])∖{y}=((FV(P)∖{y})∪(FV(N)∖{x})by inductive hypothesis=(FV(P)∖{x,y})∪FV(N)x∉FV(N)=(FV(λy.P)∖{x})∪FV(N)\FV{\Subst{(\lambd[y][P])}{N}{x}} = \\ \begin{aligned} & = \FV{\lambd[y][\Subst{P}{N}{x}]} \\ & = \FV{\Subst{P}{N}{x}} \setminus \{y\} \\ & = ((\FV{P} \setminus \{y\}) \cup (\FV{N} \setminus \{x\}) && \text{by inductive hypothesis} \\ & = (\FV{P} \setminus \{x, y\}) \cup \FV{N} && x \notin \FV{N} \\ & = (\FV{\lambd[y][P]} \setminus \{x\}) \cup \FV{N} \end{aligned}

Read as: The free variables of substituting capital N for free x in lambda y with body capital P. The source repeats the equality sign across the first line break. This equals the free variables of lambda y with body capital P after substitution of capital N for free x. This equals the free variables of capital P after substitution of capital N for free x, with y removed. The next printed row has an unmatched opening parenthesis, and claims this equals the union of the free variables of capital P with y removed, and the free variables of capital N with x removed, by the inductive hypothesis. The next row claims equality with the union of the free variables of capital P with both x and y removed, and the free variables of capital N, citing x not free in capital N. The final row gives the union of the free variables of lambda y with body capital P, with x removed, and the free variables of capital N. End source equation chain

Means: The free variables of substituting capital N for free x in lambda y with body capital P. The source repeats the equality sign across the first line break. This equals the free variables of lambda y with body capital P after substitution of capital N for free x. This equals the free variables of capital P after substitution of capital N for free x, with y removed. The next printed row has an unmatched opening parenthesis, and claims this equals the union of the free variables of capital P with y removed, and the free variables of capital N with x removed, by the inductive hypothesis. The next row claims equality with the union of the free variables of capital P with both x and y removed, and the free variables of capital N, citing x not free in capital N. The final row gives the union of the free variables of lambda y with body capital P, with x removed, and the free variables of capital N. End source equation chain

1 occurrence in this chapter

Equation form expr-8f68cff8d36406c5

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

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

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

1 occurrence in this chapter

Equation form expr-91d2631d16c96c97

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

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

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

1 occurrence in this chapter

Equation form expr-92ecc1b72c2f2134

(λz.N)[y/x][x/y]=(λz.N[y/x])[x/y]=λz.N[y/x][x/y]=λz.N by inductive hypothesis\Subst{\Subst{(\lambd[z][N])}{y}{x}}{x}{y}\\ & = \Subst{(\lambd[z][\Subst{N}{y}{x}])}{x}{y} \\ & = \lambd[z][\Subst{\Subst{N}{y}{x}}{x}{y}] \\ &= \lambd[z][N] \text{ by inductive hypothesis}

Read as: the substitution of x for free y in the substitution of y for free x in lambda z, with body capital N, end abstraction, end substitution, end substitution equals the substitution of x for free y in lambda z, with body the substitution of y for free x in capital N, end substitution, end abstraction, end substitution. This equals lambda z, with body the substitution of x for free y in the substitution of y for free x in capital N, end substitution, end substitution, end abstraction. This equals lambda z, with body capital N, end abstraction, by the inductive hypothesis. End equation chain

Means: the substitution of x for free y in the substitution of y for free x in lambda z, with body capital N, end abstraction, end substitution, end substitution equals the substitution of x for free y in lambda z, with body the substitution of y for free x in capital N, end substitution, end abstraction, end substitution. This equals lambda z, with body the substitution of x for free y in the substitution of y for free x in capital N, end substitution, end substitution, end abstraction. This equals lambda z, with body capital N, end abstraction, by the inductive hypothesis. End equation chain

1 occurrence in this chapter

Equation form expr-931dff339d332fc5

(P[N/x])(Q[N/x])(\Subst{P}{N}{x})(\Subst{Q}{N}{x})

Read as: the application of the substitution of capital N for free x in capital P, end substitution to the substitution of capital N for free x in capital Q, end substitution, end application

Means: the application of the substitution of capital N for free x in capital P, end substitution to the substitution of capital N for free x in capital Q, end substitution, end application

1 occurrence in this chapter

Equation form expr-9326d29e3d5eb3f0

M=OM \equal O

Read as: capital M is beta equivalent to capital O

Means: capital M is beta equivalent to capital O

1 occurrence in this chapter

Equation form expr-93861fafd96351e1

(P′Q′)(P'Q')

Read as: the application of capital P prime to capital Q prime, end application

Means: the application of capital P prime to capital Q prime, end application

1 occurrence in this chapter

Equation form expr-9555464a9cb5c291

w,x,y,zw,x,y,z

Read as: w, x, y, z

Means: w, x, y, z

1 occurrence in this chapter

Equation form expr-95c00def61e377ca

yxy x

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

Means: the application of y to x, end application

2 occurrences in this chapter

Equation form expr-968e35d94421eec4

λx.N→αλy.N[y/x]if x≠y, y∉FV(N)and N[y/x] is defined&\lambd[x][N] \redone[\alpha] \lambd[y][\Subst{N}{y}{x}] && \text{if $x \neq y$, $y \notin \FV{N}$} \\ & &&\text{and $\Subst{N}{y}{x}$ is defined}

Read as: lambda x, with body capital N, end abstraction changes one bound variable to give lambda y, with body the substitution of y for free x in capital N, end substitution, end abstraction, if x differs from y, y is not free in capital N, and the substitution of y for free x in capital N, end substitution is defined

Means: lambda x, with body capital N, end abstraction changes one bound variable to give lambda y, with body the substitution of y for free x in capital N, end substitution, end abstraction, if x differs from y, y is not free in capital N, and the substitution of y for free x in capital N, end substitution is defined

1 occurrence in this chapter

Equation form expr-9769e9a7d02e5968

λy.P[N/x]\Subst{\lambd[y][P]}{N}{x}

Read as: the substitution of capital N for free x in lambda y, with body capital P, end abstraction, end substitution

Means: the substitution of capital N for free x in lambda y, with body capital P, end abstraction, end substitution

2 occurrences in this chapter

Equation form expr-9845833f92063118

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

Read as: the substitution of y for free x in capital N, end substitution

Means: the substitution of y for free x in capital N, end substitution

4 occurrences in this chapter

Equation form expr-9b2e39cb9e377535

N=MN \equal M

Read as: capital N is beta equivalent to capital M

Means: capital N is beta equivalent to capital M

1 occurrence in this chapter

Equation form expr-9c45747bde2280c6

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

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

Means: lambda y, with body capital P, end abstraction

3 occurrences in this chapter

Equation form expr-9e06c570e1a4a009

↠β\bred

Read as: beta reduction in zero or more steps

Means: beta reduction in zero or more steps

3 occurrences in this chapter

Equation form expr-9e54c68e5e139945

z≠yz \neq y

Read as: z is not equal to y

Means: z is not equal to y

2 occurrences in this chapter

Equation form expr-9f7a6a25f90c1a32

M¯[R¯/y]\Subst{\rep{M}}{\rep{R}}{y}

Read as: the substitution of a representative of class capital R for free y in a representative of class capital M, end substitution

Means: the substitution of a representative of class capital R for free y in a representative of class capital M, end substitution

1 occurrence in this chapter

Equation form expr-9f96955b475f7670

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

Read as: open parenthesis, lambda x, dot, capital M, capital N, capital P, close parenthesis

Means: open parenthesis, lambda x, dot, capital M, capital N, capital P, close parenthesis

1 occurrence in this chapter

Equation form expr-a10967f9861dbeed

M′′=αMM'' \aeq M

Read as: capital M double prime is alpha equivalent to capital M

Means: capital M double prime is alpha equivalent to capital M

2 occurrences in this chapter

Equation form expr-a1188f68d024694f

N→αN′N \aconvone N'

Read as: capital N changes one bound variable to give capital N prime

Means: capital N changes one bound variable to give capital N prime

1 occurrence in this chapter

Equation form expr-a1fce4363854ff88

yy

Read as: y

Means: y

13 occurrences in this chapter

Equation form expr-a2f7be0b3d2558a0

λy.N[y/x]\lambd[y][\Subst{N}{y}{x}]

Read as: lambda y, with body the substitution of y for free x in capital N, end substitution, end abstraction

Means: lambda y, with body the substitution of y for free x in capital N, end substitution, end abstraction

3 occurrences in this chapter

Equation form expr-a3caa158f35b5ff8

λy\lambd[y]

Read as: the lambda binder on y

Means: the lambda binder on y

2 occurrences in this chapter

Equation form expr-a48e09ce041cfa6f

(PQ)→α(PQ′)(PQ) \aconvone (PQ')

Read as: the application of capital P to capital Q, end application changes one bound variable to give the application of capital P to capital Q prime, end application

Means: the application of capital P to capital Q, end application changes one bound variable to give the application of capital P to capital Q prime, end application

1 occurrence in this chapter

Equation form expr-a697fb0d0b17db1c

Rλx.Nλx.N′R \lambd[x][N] \lambd[x][N']

Read as: relation capital R holds from lambda x, with body capital N, end abstraction to lambda x, with body capital N prime, end abstraction

Means: relation capital R holds from lambda x, with body capital N, end abstraction to lambda x, with body capital N prime, end abstraction

1 occurrence in this chapter

Equation form expr-a6fdee2c7d448c1b

FV(P)\FV{P}

Read as: the free variables of capital P, end free variable set

Means: the free variables of capital P, end free variable set

1 occurrence in this chapter

Equation form expr-a75097b4aae27f72

x∈FV(M))x \in \FV{M})

Read as: x is free in capital M, followed by an unmatched closing parenthesis in the source

Means: x is free in capital M, followed by an unmatched closing parenthesis in the source

1 occurrence in this chapter

Equation form expr-a7e7e2f59b128bdb

extext

Read as: extensionality

Means: extensionality

1 occurrence in this chapter

Equation form expr-a805479a5a7f785f

P↠αRP \aconv R

Read as: capital P alpha converts to capital R

Means: capital P alpha converts to capital R

1 occurrence in this chapter

Equation form expr-a80e71fb95e7f946

x,Γx,\Gamma

Read as: the list with x prepended to Gamma

Means: the list with x prepended to Gamma

1 occurrence in this chapter

Equation form expr-a882526ce5eaec21

(λx.N)Q=N[Q/x](\lambd[x][N])Q \equal \Subst{N}{Q}{x}

Read as: the application of lambda x, with body capital N, end abstraction to capital Q, end application is beta equivalent to the substitution of capital Q for free x in capital N, end substitution

Means: the application of lambda x, with body capital N, end abstraction to capital Q, end application is beta equivalent to the substitution of capital Q for free x in capital N, end substitution

1 occurrence in this chapter

Equation form expr-a88509ac49ef6afb

λ.N\lambd[][N]

Read as: an unnamed lambda abstraction with body capital N, end abstraction

Means: an unnamed lambda abstraction with body capital N, end abstraction

1 occurrence in this chapter

Equation form expr-aabc6d88cbd006dc

R′R'

Read as: capital R prime

Means: capital R prime

1 occurrence in this chapter

Equation form expr-aafc99e4b1bb6db2

M′[R/y]\Subst{M'}{R}{y}

Read as: the substitution of capital R for free y in capital M prime, end substitution

Means: the substitution of capital R for free y in capital M prime, end substitution

1 occurrence in this chapter

Equation form expr-aca25da774229c87

(λz.N′′[z/x])[R′′/y]==λz.N′′[z/x][R′′/y]=λz.N′′[z/x][R/y]by the substitution lemma for alpha equivalent replacement terms=λz.N′[z/x][R/y]by inductive hypothesis=(λz.N′[z/x])[R/y]\Subst{(\lambd[z][\Subst{N''}{z}{x}])}{R''}{y} =\\ \begin{aligned} &= \lambd[z][\Subst{\Subst{N''}{z}{x}}{R''}{y}] \\ &= \lambd[z][\Subst{\Subst{N''}{z}{x}}{R}{y}] && \text{by \olref{lem:sub:R}}\\ &=\lambd[z][\Subst{\Subst{N'}{z}{x}}{R}{y}] && \text{by inductive hypothesis}\\ &=\Subst{(\lambd[z][\Subst{N'}{z}{x}])}{R}{y} \end{aligned}

Read as: Substitute capital R double prime for free y in lambda z with body capital N double prime after substitution of z for free x. The source repeats the equality sign across the first line break. This equals lambda z whose body is capital N double prime after substitution of z for free x, followed by substitution of capital R double prime for free y. The next equality replaces capital R double prime by capital R, citing the substitution lemma for alpha equivalent replacement terms. The next equality replaces capital N double prime by capital N prime, citing the inductive hypothesis. The final equality writes the result as substitution of capital R for free y in lambda z with body capital N prime after substitution of z for free x. All printed relations in this chain are equalities, not alpha equivalences. End source equation chain

Means: Substitute capital R double prime for free y in lambda z with body capital N double prime after substitution of z for free x. The source repeats the equality sign across the first line break. This equals lambda z whose body is capital N double prime after substitution of z for free x, followed by substitution of capital R double prime for free y. The next equality replaces capital R double prime by capital R, citing the substitution lemma for alpha equivalent replacement terms. The next equality replaces capital N double prime by capital N prime, citing the inductive hypothesis. The final equality writes the result as substitution of capital R for free y in lambda z with body capital N prime after substitution of z for free x. All printed relations in this chain are equalities, not alpha equivalences. End source equation chain

1 occurrence in this chapter

Equation form expr-afb3682cb47e637f

P→βQP \bredone Q

Read as: capital P beta contracts in one step to capital Q

Means: capital P beta contracts in one step to capital Q

1 occurrence in this chapter

Equation form expr-b1b4b2f6c4f93892

FV(λy.P[N/x])==FV(λy.P[N/x])by the substitution definition's abstraction clause=FV(P[N/x])∖{y}by the definition of free variablesthe free variable definition's abstraction clause=FV(P)∖{y}by inductive hypothesis=FV(λy.P)by the definition of free variablesthe free variable definition's abstraction clause\FV{\Subst{\lambd[y][P]}{N}{x}} = \\ \begin{aligned} & = \FV{\lambd[y][\Subst{P}{N}{x}]} && \text{by \olref{defn:substitution-4}}\\ & = \FV{\Subst{P}{N}{x}} \setminus \{y\} && \text{by \olref[fv]{def:fv}\olref[fv]{def:fv2}}\\ & = \FV{P} \setminus \{y\} && \text{by inductive hypothesis} \\ & = \FV{\lambd[y][P]} && \text{by \olref[fv]{def:fv}\olref[fv]{def:fv2}} \end{aligned}

Read as: The free variables of substituting capital N for free x in lambda y with body capital P. The source repeats the equality sign across the first line break. This equals the free variables of lambda y with body capital P after substitution of capital N for free x, by the substitution definition's abstraction clause. This equals the free variables of capital P after substitution of capital N for free x, with y removed, by the definition of free variables, the free variable definition's abstraction clause. This equals the free variables of capital P with y removed, by the inductive hypothesis. This equals the free variables of lambda y with body capital P, by the definition of free variables, the free variable definition's abstraction clause. End equation chain

Means: The free variables of substituting capital N for free x in lambda y with body capital P. The source repeats the equality sign across the first line break. This equals the free variables of lambda y with body capital P after substitution of capital N for free x, by the substitution definition's abstraction clause. This equals the free variables of capital P after substitution of capital N for free x, with y removed, by the definition of free variables, the free variable definition's abstraction clause. This equals the free variables of capital P with y removed, by the inductive hypothesis. This equals the free variables of lambda y with body capital P, by the definition of free variables, the free variable definition's abstraction clause. End equation chain

1 occurrence in this chapter

Equation form expr-b27a3505a45595b2

y∈FV(λx.N)y \in \FV{\lambd[x][N]}

Read as: y is free in lambda x, with body capital N, end abstraction

Means: y is free in lambda x, with body capital N, end abstraction

1 occurrence in this chapter

Equation form expr-b2e60b47d920383e

λy.P[N/x]\lambd[y][\Subst{P}{N}{x}]

Read as: lambda y, with body the substitution of capital N for free x in capital P, end substitution, end abstraction

Means: lambda y, with body the substitution of capital N for free x in capital P, end substitution, end abstraction

2 occurrences in this chapter

Equation form expr-b3460543c506b16b

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

Read as: open parenthesis, open parenthesis, open parenthesis, capital M, capital N, close parenthesis, capital P, close parenthesis, capital Q, close parenthesis

Means: open parenthesis, open parenthesis, open parenthesis, capital M, capital N, close parenthesis, capital P, close parenthesis, capital Q, close parenthesis

1 occurrence in this chapter

Equation form expr-b44c937bc57103cb

Mx=ηNxMx \equal[\eta] Nx

Read as: the application of capital M to x, end application is equivalent, under beta equivalence extended by eta conversion, to the application of capital N to x, end application

Means: the application of capital M to x, end application is equivalent, under beta equivalence extended by eta conversion, to the application of capital N to x, end application

1 occurrence in this chapter

Equation form expr-b4651d829ade5f5d

M→αM′M \redone[\alpha] M'

Read as: capital M changes one bound variable to give capital M prime

Means: capital M changes one bound variable to give capital M prime

1 occurrence in this chapter

Equation form expr-b4cecddd9ec1fd2c

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

Read as: the substitution of capital N for free x in capital M, end substitution

Means: the substitution of capital N for free x in capital M, end substitution

1 occurrence in this chapter

Equation form expr-b4db03dab703b98b

zvzv

Read as: the application of z to v, end application

Means: the application of z to v, end application

1 occurrence in this chapter

Equation form expr-b5f6733cef0e61ab

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

Read as: Lambda x, whose body applies the abstraction lambda y with body y applied to x, to z, is applied to v. Contracting the inner application in one beta step gives lambda x with body z applied to x, applied to v

Means: Lambda x, whose body applies the abstraction lambda y with body y applied to x, to z, is applied to v. Contracting the inner application in one beta step gives lambda x with body z applied to x, applied to v

1 occurrence in this chapter

Equation form expr-b679f4f8b9c95cc6

N′=αNN' \aeq N

Read as: capital N prime is alpha equivalent to capital N

Means: capital N prime is alpha equivalent to capital N

1 occurrence in this chapter

Equation form expr-b93a6310e53dd662

λx.M=λx.N\lambd[x][M] \equal \lambd[x][N]

Read as: lambda x, with body capital M, end abstraction is beta equivalent to lambda x, with body capital N, end abstraction

Means: lambda x, with body capital M, end abstraction is beta equivalent to lambda x, with body capital N, end abstraction

1 occurrence in this chapter

Equation form expr-b96f630b32f05b54

y∉FV(N)y \notin \FV{N}

Read as: y is not free in capital N

Means: y is not free in capital N

7 occurrences in this chapter

Equation form expr-b993eae99f643780

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

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

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

1 occurrence in this chapter

Equation form expr-b9bacb461b2d35cc

M=MM \equal M

Read as: capital M is beta equivalent to capital M

Means: capital M is beta equivalent to capital M

1 occurrence in this chapter

Equation form expr-b9cd46368aa50edd

y(λv.xv)[(λy.vy)/x]\Subst{y(\lambd[v][xv])}{(\lambd[y][vy])}{x}

Read as: the substitution of lambda y, with body the application of v to y, end application, end abstraction for free x in the application of y to lambda v, with body the application of x to v, end application, end abstraction, end application, end substitution

Means: the substitution of lambda y, with body the application of v to y, end application, end abstraction for free x in the application of y to lambda v, with body the application of x to v, end application, end abstraction, end application, end substitution

1 occurrence in this chapter

Equation form expr-bb13614dbfa85eef

P↠βQP \bred Q

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

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

1 occurrence in this chapter

Equation form expr-bba68044955ccf8c

(λm.(λy.y)m)(\lambd[m][(\lambd[y][y]) m])

Read as: lambda lowercase m, with body the application of lambda y, with body y, end abstraction to lowercase m, end application, end abstraction

Means: lambda lowercase m, with body the application of lambda y, with body y, end abstraction to lowercase m, end application, end abstraction

1 occurrence in this chapter

Equation form expr-bc4aedc0a4533f6a

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

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

Means: lambda x, with body y, end abstraction

1 occurrence in this chapter

Equation form expr-bc6344b9abf6f7c5

λx.x[y/x]==λz.z[y/x]=λz.z[y/x]=λz.z\Subst{\lambd[x][x]}{y}{x} & =\ollabel{eq:1}\\ &= \Subst{\lambd[z][z]}{y}{x} \ollabel{eq:2}\\ &= \lambd[z][\Subst{z}{y}{x}] \\ &= \lambd[z][z]

Read as: On alpha equivalence classes, substitute y for free x in lambda x with body x. This is the first labelled equation. The source repeats the equality sign at the next line. This equals substitution of y for free x in lambda z with body z, the second labelled equation. This equals lambda z with body z after substitution of y for free x. This equals lambda z with body z. End equation chain

Means: On alpha equivalence classes, substitute y for free x in lambda x with body x. This is the first labelled equation. The source repeats the equality sign at the next line. This equals substitution of y for free x in lambda z with body z, the second labelled equation. This equals lambda z with body z after substitution of y for free x. This equals lambda z with body z. End equation chain

1 occurrence in this chapter

Equation form expr-bcdf1c064c26f6e8

z≠xz \ne x

Read as: z is not equal to x

Means: z is not equal to x

1 occurrence in this chapter

Equation form expr-bd53a883bdd83021

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

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

Means: lambda x, with body capital N, end abstraction

2 occurrences in this chapter

Equation form expr-bda27c8005ffaf81

λx.Mx=extM\lambd[x][Mx] \equal[\ext] M

Read as: lambda x, with body the application of capital M to x, end application, end abstraction is equivalent, under beta equivalence extended by extensionality, to capital M

Means: lambda x, with body the application of capital M to x, end application, end abstraction is equivalent, under beta equivalence extended by extensionality, to capital M

1 occurrence in this chapter

Equation form expr-c3874a3943dc32d1

x∉FV(M[N/x])x \notin \FV{\Subst{M}{N}{x}}

Read as: x is not free in the substitution of capital N for free x in capital M, end substitution

Means: x is not free in the substitution of capital N for free x in capital M, end substitution

1 occurrence in this chapter

Equation form expr-c4658b9a314f5119

M=extNM \equal[\ext] N

Read as: capital M is equivalent, under beta equivalence extended by extensionality, to capital N

Means: capital M is equivalent, under beta equivalence extended by extensionality, to capital N

2 occurrences in this chapter

Equation form expr-c4f10a264b3814f4

λa.λb.ac\lambd[a][\lambd[b][a c]]

Read as: lambda a, with body lambda b, with body the application of a to c, end application, end abstraction, end abstraction

Means: lambda a, with body lambda b, with body the application of a to c, end application, end abstraction, end abstraction

2 occurrences in this chapter

Equation form expr-c54618f49ac331ce

λz.z\lambd[z][z]

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

Means: lambda z, with body z, end abstraction

1 occurrence in this chapter

Equation form expr-c5c5541538c3a4b0

λx\lambd[x]

Read as: the lambda binder on x

Means: the lambda binder on x

15 occurrences in this chapter

Equation form expr-c662fb992708cb56

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

Read as: lambda x y, dot, x x y x, lambda z, dot, x z; the abbreviated string has no parentheses

Means: lambda x y, dot, x x y x, lambda z, dot, x z; the abbreviated string has no parentheses

1 occurrence in this chapter

Equation form expr-c6bfadccca263ff7

βη\beta\eta

Read as: beta eta

Means: beta eta

2 occurrences in this chapter

Equation form expr-c9de49c1c772adfc

M→ηNM \eredone N

Read as: capital M eta contracts in one step to capital N

Means: capital M eta contracts in one step to capital N

1 occurrence in this chapter

Equation form expr-ca399e1bbf86e8db

=ext\equal[\ext]

Read as: beta equivalence extended by extensionality

Means: beta equivalence extended by extensionality

2 occurrences in this chapter

Equation form expr-cb8c633db2f749e1

λx.Mx=ηλx.Nx\lambd[x][Mx] \equal[\eta] \lambd[x][Nx]

Read as: lambda x, with body the application of capital M to x, end application, end abstraction is equivalent, under beta equivalence extended by eta conversion, to lambda x, with body the application of capital N to x, end application, end abstraction

Means: lambda x, with body the application of capital M to x, end application, end abstraction is equivalent, under beta equivalence extended by eta conversion, to lambda x, with body the application of capital N to x, end application, end abstraction

1 occurrence in this chapter

Equation form expr-cc057a45e04f5e2e

λy.fy\lambd[y][f y]

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

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

1 occurrence in this chapter

Equation form expr-cd0aa9856147b6c5

gg

Read as: g

Means: g

2 occurrences in this chapter

Equation form expr-cd7826d0b1f9587c

Γ[n]\Gamma[n]

Read as: the variable at position n in Gamma

Means: the variable at position n in Gamma

1 occurrence in this chapter

Equation form expr-cec4b8919e5f12a5

P′P'

Read as: capital P prime

Means: capital P prime

1 occurrence in this chapter

Equation form expr-cfd1fc5548b24eea

x∉FV(M)x \notin FV(M)

Read as: x is not free in capital M

Means: x is not free in capital M

1 occurrence in this chapter

Equation form expr-d03a1e90beae7e2c

010\, 1

Read as: the application of de Bruijn index zero to de Bruijn index one

Means: the application of de Bruijn index zero to de Bruijn index one

1 occurrence in this chapter

Equation form expr-d0514611d1833612

N′′N''

Read as: capital N double prime

Means: capital N double prime

1 occurrence in this chapter

Equation form expr-d09c0982c7627db9

x,yx, y

Read as: x and y

Means: 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 the abstraction lambda x, whose body is x applied to x and then to y, applied to a second copy of the same abstraction. One beta contraction gives that original self application, then applied to y. One beta contraction gives that original self application, then applied to y and then to y again. One step contractions continue. End displayed reduction chain

Means: Start with the abstraction lambda x, whose body is x applied to x and then to y, applied to a second copy of the same abstraction. One beta contraction gives that original self application, then applied to y. One beta contraction gives that original self application, then applied to y and then to y again. One step contractions continue. End displayed reduction chain

1 occurrence in this chapter

Equation form expr-d25bf1df1c1711b7

M¯0,M¯1,etc.\rep{M}[0], \rep{M}[1], etc.

Read as: representative zero of class capital M, representative one of class capital M, and so on

Means: representative zero of class capital M, representative one of class capital M, and so on

1 occurrence in this chapter

Equation form expr-d4735e3a265e16ee

22

Read as: two

Means: two

1 occurrence in this chapter

Equation form expr-d5b7043b071e96af

M→βNM \bredone N

Read as: capital M beta contracts in one step to capital N

Means: capital M beta contracts in one step to capital N

1 occurrence in this chapter

Equation form expr-d5e1e2d4b7ed89ef

↠α\aconv

Read as: alpha conversion

Means: alpha conversion

4 occurrences in this chapter

Equation form expr-d613a1caf1c7bc5b

(λ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 contracts in one step to that very same self application

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

1 occurrence in this chapter

Equation form expr-d6a337514e3fb9aa

λg\lambd[g]

Read as: the lambda binder on g

Means: the lambda binder on g

1 occurrence in this chapter

Equation form expr-d75af9381cb596da

GΓ(n)=Γ[n]GΓ(PQ)=GΓ(P)GΓ(Q)GΓ(λ.N)=λx.Gx,Γ(N)G_\Gamma(n) &= \Gamma[n] \\ G_\Gamma(PQ) &= G_\Gamma(P) G_\Gamma(Q) \\ G_\Gamma(\lambd[][N]) &= \lambd[x][G_{x,\Gamma}(N)]

Read as: Recovery capital G, with environment Gamma, is defined by three equations. First, capital G subscript Gamma of n equals the variable in position n of Gamma. Second, capital G subscript Gamma of the application of capital P to capital Q equals the application of capital G subscript Gamma of capital P to capital G subscript Gamma of capital Q. Third, capital G subscript Gamma of an unnamed abstraction with body capital N equals lambda x with body capital G, with environment x prepended to Gamma, of capital N. End equations

Means: Recovery capital G, with environment Gamma, is defined by three equations. First, capital G subscript Gamma of n equals the variable in position n of Gamma. Second, capital G subscript Gamma of the application of capital P to capital Q equals the application of capital G subscript Gamma of capital P to capital G subscript Gamma of capital Q. Third, capital G subscript Gamma of an unnamed abstraction with body capital N equals lambda x with body capital G, with environment x prepended to Gamma, of capital N. End equations

1 occurrence in this chapter

Equation form expr-d953b8f4ed216699

x∈FV(N)x \in FV(N)

Read as: x is free in capital N

Means: x is free in capital N

1 occurrence in this chapter

Equation form expr-d9fd866fe7568aed

=\equal

Read as: beta equivalence

Means: beta equivalence

5 occurrences in this chapter

Equation form expr-da760196c117ebed

(PQ)[N/y]\Subst{(PQ)}{N}{y}

Read as: the substitution of capital N for free y in the application of capital P to capital Q, end application, end substitution

Means: the substitution of capital N for free y in the application of capital P to capital Q, end application, end substitution

1 occurrence in this chapter

Equation form expr-dcd042f10a941457

N,QN, Q

Read as: capital N and capital Q

Means: capital N and capital Q

1 occurrence in this chapter

Equation form expr-dcf13ff1c9c49fad

Q↠αRQ \aconv R

Read as: capital Q alpha converts to capital R

Means: capital Q alpha converts to capital R

1 occurrence in this chapter

Equation form expr-dcf4658b4f10052f

=η\equal[\eta]

Read as: beta equivalence extended by eta conversion

Means: beta equivalence extended by eta conversion

5 occurrences in this chapter

Equation form expr-dd01549086a4e096

λx.N→αλx.N′\lambd[x][N] \aconvone \lambd[x][N']

Read as: lambda x, with body capital N, end abstraction changes one bound variable to give lambda x, with body capital N prime, end abstraction

Means: lambda x, with body capital N, end abstraction changes one bound variable to give lambda x, with body capital N prime, end abstraction

1 occurrence in this chapter

Equation form expr-dd0c88090a6969fd

FV(P)=FV(Q)\FV{P} = \FV{Q}

Read as: the free variables of capital P, end free variable set equals the free variables of capital Q, end free variable set

Means: the free variables of capital P, end free variable set equals the free variables of capital Q, end free variable set

1 occurrence in this chapter

Equation form expr-dd97864297a18a62

λc.λb.a\lambd[c][\lambd[b][a]]

Read as: lambda c, with body lambda b, with body a, end abstraction, end abstraction

Means: lambda c, with body lambda b, with body a, end abstraction, end abstraction

2 occurrences in this chapter

Equation form expr-de07a47862f699cf

→\redone

Read as: the unlabelled one step reduction arrow

Means: the unlabelled one step reduction arrow

1 occurrence in this chapter

Equation form expr-df5dd3f9dd78acfd

λy.N[y/x]→αλx.N[y/x][x/y]=λx.N\lambd[y][\Subst{N}{y}{x}] \aconvone \lambd[x][\Subst{\Subst{N}{y}{x}}{x}{y}] = \lambd[x][N]

Read as: lambda y, with body the substitution of y for free x in capital N, end substitution, end abstraction changes one bound variable to give lambda x, with body the substitution of x for free y in the substitution of y for free x in capital N, end substitution, end substitution, end abstraction, which equals lambda x, with body capital N, end abstraction

Means: lambda y, with body the substitution of y for free x in capital N, end substitution, end abstraction changes one bound variable to give lambda x, with body the substitution of x for free y in the substitution of y for free x in capital N, end substitution, end substitution, end abstraction, which equals lambda x, with body capital N, end abstraction

1 occurrence in this chapter

Equation form expr-dfb5cefbd56635f9

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

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

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

1 occurrence in this chapter

Equation form expr-e0a167ff84e99dd7

x∉FV(R)x \notin FV(R)

Read as: x is not free in capital R

Means: x is not free in capital R

1 occurrence in this chapter

Equation form expr-e1f690b803d4593d

y∉FV(M)y \notin \FV{M}

Read as: y is not free in capital M

Means: y is not free in capital M

1 occurrence in this chapter

Equation form expr-e47a89e2c6495350

M′[R′/y]\Subst{M'}{R'}{y}

Read as: the substitution of capital R prime for free y in capital M prime, end substitution

Means: the substitution of capital R prime for free y in capital M prime, end substitution

2 occurrences in this chapter

Equation form expr-e4fbf0696654e5e3

R(PQ)(PQ′)R (PQ) (PQ')

Read as: relation capital R holds from the application of capital P to capital Q, end application to the application of capital P to capital Q prime, end application

Means: relation capital R holds from the application of capital P to capital Q, end application to the application of capital P to capital Q prime, end application

1 occurrence in this chapter

Equation form expr-e51a791b7830372c

Q→αPQ \aconvone P

Read as: capital Q changes one bound variable to give capital P

Means: capital Q changes one bound variable to give capital P

1 occurrence in this chapter

Equation form expr-e551de20e786b708

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

Read as: lambda followed by x, y, z, then dot and capital M

Means: lambda followed by x, y, z, then dot and capital M

1 occurrence in this chapter

Equation form expr-e719436aaf3191c8

y∈FV(PQ)y \in \FV{PQ}

Read as: y is free in the application of capital P to capital Q, end application

Means: y is free in the application of capital P to capital Q, end application

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

4 occurrences in this chapter

Equation form expr-ec974ae2d0e631f6

(PQ)[y/x][x/y]=((P[y/x])(Q[y/x]))[x/y]=(P[y/x][x/y])(Q[y/x][x/y])=(PQ) by inductive hypothesis\Subst{\Subst{(PQ)}{y}{x}}{x}{y} &=\Subst{((\Subst{P}{y}{x})(\Subst{Q}{y}{x}))}{x}{y} \\ &= (\Subst{\Subst{P}{y}{x}}{x}{y})(\Subst{\Subst{Q}{y}{x}}{x}{y}) \\ &= (PQ) \text{ by inductive hypothesis}

Read as: the substitution of x for free y in the substitution of y for free x in the application of capital P to capital Q, end application, end substitution, end substitution equals the substitution of x for free y in the application of the substitution of y for free x in capital P, end substitution to the substitution of y for free x in capital Q, end substitution, end application, end substitution. This equals the application of the substitution of x for free y in the substitution of y for free x in capital P, end substitution, end substitution to the substitution of x for free y in the substitution of y for free x in capital Q, end substitution, end substitution, end application. This equals the application of capital P to capital Q, end application, by the inductive hypothesis. End equation chain

Means: the substitution of x for free y in the substitution of y for free x in the application of capital P to capital Q, end application, end substitution, end substitution equals the substitution of x for free y in the application of the substitution of y for free x in capital P, end substitution to the substitution of y for free x in capital Q, end substitution, end application, end substitution. This equals the application of the substitution of x for free y in the substitution of y for free x in capital P, end substitution, end substitution to the substitution of x for free y in the substitution of y for free x in capital Q, end substitution, end substitution, end application. This equals the application of capital P to capital Q, end application, by the inductive hypothesis. End equation chain

1 occurrence in this chapter

Equation form expr-ed78facde36e0d2c

FV(M[N/x])=(FV(M)∖{x})∪FV(N)\FV{\Subst{M}{N}{x}} = (\FV{M} \setminus \{x\}) \cup \FV{N}

Read as: the free variables of the substitution of capital N for free x in capital M, end substitution, end free variable set equals the union of the free variables of capital M with x removed, and the free variables of capital N

Means: the free variables of the substitution of capital N for free x in capital M, end substitution, end free variable set equals the union of the free variables of capital M with x removed, and the free variables of capital N

1 occurrence in this chapter

Equation form expr-ee738e92d7aa7652

R(PQ)(P′Q)R (PQ) (P'Q)

Read as: relation capital R holds from the application of capital P to capital Q, end application to the application of capital P prime to capital Q, end application

Means: relation capital R holds from the application of capital P to capital Q, end application to the application of capital P prime to capital Q, end application

1 occurrence in this chapter

Equation form expr-eea8c44bdd64f1ee

λy.x[y/x]\Subst{\lambd[y][x]}{y}{x}

Read as: the substitution of y for free x in lambda y, with body x, end abstraction, end substitution

Means: the substitution of y for free x in lambda y, with body x, end abstraction, end substitution

1 occurrence in this chapter

Equation form expr-f0b8efdd5dcab8c8

(λx.Mx)x=extMx(\lambd[x][Mx])x \equal[\ext] Mx

Read as: the application of lambda x, with body the application of capital M to x, end application, end abstraction to x, end application is equivalent, under beta equivalence extended by extensionality, to the application of capital M to x, end application

Means: the application of lambda x, with body the application of capital M to x, end application, end abstraction to x, end application is equivalent, under beta equivalence extended by extensionality, to the application of capital M to x, end application

1 occurrence in this chapter

Equation form expr-f13351f03cd35fef

y∈FV(λx.P)y \in \FV{\lambd[x][P]}

Read as: y is free in lambda x, with body capital P, end abstraction

Means: y is free in lambda x, with body capital P, end abstraction

1 occurrence in this chapter

Equation form expr-f1a1acd406486777

M′[R/y]=αM′′[R′′/y]\Subst{M'}{R}{y} \aeq \Subst{M''}{R''}{y}

Read as: the substitution of capital R for free y in capital M prime, end substitution is alpha equivalent to the substitution of capital R double prime for free y in capital M double prime, end substitution

Means: the substitution of capital R for free y in capital M prime, end substitution is alpha equivalent to the substitution of capital R double prime for free y in capital M double prime, end substitution

1 occurrence in this chapter

Equation form expr-f2d43dd64c57fccb

x∈FV(PQ)x \in \FV{PQ}

Read as: x is free in the application of capital P to capital Q, end application

Means: x is free in the application of capital P to capital Q, end application

1 occurrence in this chapter

Equation form expr-f367453e2c78c023

λx.N=αλx.N′\lambd[x][N] \aeq \lambd[x][N']

Read as: lambda x, with body capital N, end abstraction is alpha equivalent to lambda x, with body capital N prime, end abstraction

Means: lambda x, with body capital N, end abstraction is alpha equivalent to lambda x, with body capital N prime, end abstraction

1 occurrence in this chapter

Equation form expr-f3f3804480e8551a

β\beta

Read as: beta

Means: beta

24 occurrences in this chapter

Equation form expr-f54a6dabb61819ad

M↠βNM \bred N

Read as: capital M beta reduces in zero or more steps to capital N

Means: capital M beta reduces in zero or more steps to capital N

2 occurrences in this chapter

Equation form expr-f561216a2b855043

→α\redone[\alpha]

Read as: one change of bound variable

Means: one change of bound variable

1 occurrence in this chapter

Equation form expr-f8442ee54d86d209

P→αQP \aconvone Q

Read as: capital P changes one bound variable to give capital Q

Means: capital P changes one bound variable to give capital Q

5 occurrences in this chapter

Equation form expr-f8f2b718f8df5074

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

Read as: the application of lambda x, with body capital N, end abstraction to capital Q, end application

Means: the application of lambda x, with body capital N, end abstraction to capital Q, end application

1 occurrence in this chapter

Equation form expr-faaea1a9da397a05

MQ=NQMQ \equal NQ

Read as: the application of capital M to capital Q, end application is beta equivalent to the application of capital N to capital Q, end application

Means: the application of capital M to capital Q, end application is beta equivalent to the application of capital N to capital Q, end application

1 occurrence in this chapter

Equation form expr-fba9b1a1d75025f9

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

Read as: the substitution of capital N for free x in capital P, end substitution

Means: the substitution of capital N for free x in capital P, end substitution

2 occurrences in this chapter

Equation form expr-fc45a145264fffef

v1\Obj{v_1}

Read as: v subscript one

Means: v subscript one

1 occurrence in this chapter

Equation form expr-ff60f5a85358826a

→α\aconvone

Read as: one change of bound variable

Means: one change of bound variable

6 occurrences in this chapter

Equation form expr-fff4857a152b8200

M′′[R′′/y]\Subst{M''}{R''}{y}

Read as: the substitution of capital R double prime for free y in capital M double prime, end substitution

Means: the substitution of capital R double prime for free y in capital M double prime, end substitution

1 occurrence in this chapter

Definition of lambda terms

Inductive formation has three clauses: a variable is a term; an abstraction on a variable with a term as body is a term; and an application of one term to another is a term. Official syntax is fully parenthesized.

Source

Exercise on formation of a nested lambda term

Describe the formation of the displayed term with outer binder g and two inner abstractions binding x. No formation or solution is supplied.

Source

Lemma on the first symbol of a term

Every term starts with a variable or a parenthesis.

Source

Lemma on the first symbols of an application

An application starts with either two parentheses or a parenthesis followed by a variable.

Source

Lemma on proper initial parts

No proper initial part of a term is itself a term.

Source

Exercise proving the initial part lemma

Prove the initial part lemma by induction on the length of terms. The exercise remains unsolved.

Source

Unique readability proposition

Every term has exactly one formation using the inductive formation rules.

Source

Three uniquely determined forms of a term

A term has exactly one of three forms: a uniquely determined variable; an abstraction with uniquely determined parameter and body; or an application with uniquely determined left and right terms.

Source

Exercise expanding abbreviated syntax

Expand the given abbreviated term with binder g and two x abstractions into official syntax. The source supplies no solution.

Source

Definition of scope as printed

The printed definition calls the occurrence of capital N the scope of lambda x when lambda x with body capital M occurs inside capital N. This conflicts with the surrounding body examples and is preserved with a source note.

Source

Definition of free and bound occurrence

An occurrence of x is free when outside the scope of every binder on x, and bound otherwise. An occurrence inside lambda x with body capital M is bound by that initial binder exactly when its occurrence in capital M is free.

Source

Examples distinguishing nested binders

The examples distinguish a free final x outside an abstraction from occurrences inside it. In a nested abstraction that reuses x, the inner occurrence is bound by the inner binder and the final occurrence in the outer body is bound by the outer binder.

Source

Recursive definition of free variables

The free variables of a variable form its singleton set. Abstraction removes its parameter from the free variables of its body. Application takes the union of the free variable sets of the two component terms.

Source

Exercises identifying scopes and free variables

Identify the scopes of the binder g and both binders x in the specified term, decide which occurrences are bound and by which binders, and give the free variables of the final nested term. None of these exercises is solved here.

Source

Definition of closed term and combinator

A term with no free variables is called a closed term or a combinator.

Source

Free variable membership lemma

If y differs from x, y is free in lambda x with body capital N exactly when y is free in capital N. A variable is free in an application exactly when it is free in at least one component.

Source

Exercise proving free variable membership

Prove both clauses of the free variable lemma. The proof is left as an exercise.

Source

Definition of partial substitution on terms

Substitution replaces the matching variable, leaves a different variable unchanged, and distributes over application. Under lambda y it is defined by substitution into the body only when x differs from y and y is not free in the replacement. Otherwise the abstraction clause explicitly says undefined. It does not automatically rename bound variables.

Source

Exercises evaluating partial substitutions

Determine the results of three displayed substitutions using the given partial definition. Capture risks and undefined cases must not be silently resolved by changing the definition. No answers are supplied.

Source

Free variables after substitution for a variable not free

If x is not free in capital M, the free variables after substitution of capital N for x equal the free variables of capital M, provided the left hand side is defined.

Source

Abstraction case for a variable not free

The displayed chain computes the free variables of a substituted abstraction, removes y from the free variables of the substituted body, uses the inductive hypothesis, and restores the abstraction notation. The initial equality sign is repeated at the line break.

Source

Exercise completing the nonfree substitution proof

Complete the variable and application cases of the proof for substitution when x is not free in capital M. The source leaves them as exercises.

Source

Free variables after substitution for a free variable

The source states that if x is free in capital M, the resulting free variables are the union of the free variables of capital M with x removed and the free variables of capital N, provided substitution is defined. The antecedent has an unmatched closing parenthesis, preserved in source.

Source

Printed abstraction calculation for free substitution

The displayed calculation is reproduced row by row, including the differing removals of x and y and the printed condition x not free in capital N. Those steps have source anomalies disclosed separately; this description does not certify the proof.

Source

Exercise completing the free substitution proof

Complete the proof of the theorem for substitution when x is free. The omitted cases remain exercises, and defects in the printed supplied calculation are disclosed separately.

Source

Theorem on removal of a free variable

After defined substitution of capital N for free x in capital M, x is no longer free if x is not free in capital N.

Source

Exercise proving removal of a free variable

Prove the theorem that substitution removes x when x is absent from the replacement. The source proof is only the word Exercise.

Source

Theorem on inverse variable substitution

If substituting y for free x in capital M is defined and y is not free in capital M, substituting x for free y in that result returns capital M.

Source

Inverse substitution calculation for application

Both substitutions distribute over the application, and the inductive hypothesis returns each component to its original term. The final result is capital P applied to capital Q.

Source

Inverse substitution calculation for abstraction

The substitutions pass under the binder z, the inductive hypothesis restores body capital N, and the result is lambda z with body capital N.

Source

Exercise completing the inverse substitution proof

Complete the inverse substitution proof, including the variable case left as an exercise. No solution is added.

Source

Local definition of change of bound variable

Replace an occurrence of lambda x with body capital N by lambda y whose body is capital N after substitution of y for free x, when y is not free in capital N and that substitution is defined. This first version omits the explicit inequality required by the subsequent versions; the mismatch is disclosed.

Source

Replacement abstraction for alpha change

The replacement binds y and has capital N after substitution of y for free x as its body.

Source

Definition of compatible relation

A relation on terms is compatible when it is preserved under abstraction, under application to a fixed right term, and under application with a fixed left term.

Source

Compatible closure definition of bound variable change

One change of bound variable is the smallest compatible relation containing the displayed renaming step, with x distinct from y, y not free in the old body, and the substitution defined.

Source

Generating bound variable renaming rule

Lambda x with body capital N changes to lambda y with capital N after substitution of y for free x as body, if x differs from y, y is not free in capital N, and the substitution is defined.

Source

Inductive definition of one alpha change

The four clauses propagate a change through abstraction, through the left side of application, through the right side of application, and perform a fresh defined change of bound variable at the binder itself.

Source

Reflexive transitive closure definition of alpha conversion

Alpha conversion is the smallest reflexive and transitive relation containing one change of bound variable.

Source

Inductive definition of alpha conversion

Alpha conversion has a transitivity rule, includes each one step change of bound variable, and relates every term to itself.

Source

Examples of alpha conversion and free names

Changing the bound x to y in a term that applies free f to its argument is alpha conversion. Replacing the free name f by a different free name g is not alpha conversion.

Source

Exercise deciding alpha convertibility

Decide whether each of the three listed pairs is alpha convertible. The second and third pairs are identical in the frozen source; both are retained. No answers are supplied.

Source

Lemma that one alpha change preserves free variables

If capital P changes one bound variable to give capital Q, their free variable sets are equal.

Source

Free variable calculation when x occurs freely

Remove y after substituting y for x in the body. The substitution theorem gives the union of the old free variables with x removed and the singleton y; removing y leaves the old free variables with x removed, equal to the free variables of the original x abstraction.

Source

Free variable calculation when x is not free

The printed calculation goes from the substituted body with y removed to the old body with x removed and then the original abstraction. The letters F and V are literal text in one source row; the intended free variable role is explained without altering the native source formula.

Source

Exercise completing preservation of free variables

Complete the other three inductive cases in the proof that one alpha change preserves free variables. They remain unsolved.

Source

Lemma reversing one alpha change

If capital P changes one bound variable to give capital Q, then capital Q changes one bound variable to give capital P. A variable mismatch in the supplied proof is disclosed separately.

Source

Exercise completing reversibility of alpha change

Complete the proof that one change of bound variable can be reversed. The missing cases are not supplied.

Source

Theorem that alpha conversion is an equivalence relation

Alpha conversion is reflexive by a zero step sequence, symmetric by reversing individual changes in reverse order, and transitive by concatenating sequences.

Source

Alpha equivalence preserves free variables

Alpha equivalent terms have equal sets of free variables.

Source

Lemma on an alpha equivalent replacement term

If capital R and capital R prime are alpha equivalent and substitution of capital R for y in capital M is defined, substitution of capital R prime is also defined and alpha equivalent to the original result.

Source

Exercise on an alpha equivalent replacement term

Prove the lemma for substitution of alpha equivalent replacement terms. The source supplies no proof.

Source

Theorem making substitution defined by alpha conversion

For any capital M, capital R, and y, an alpha equivalent capital M prime can be chosen so substitution of capital R for y is defined. Results using any other suitably defined alpha equivalent term and replacement are alpha equivalent. The proof's stronger equalities and definedness gap are preserved with a note.

Source

Printed comparison of renamed substitutions

The displayed chain moves substitution under binder z, changes the double prime replacement to the original replacement, changes the double prime body to the prime body, and rewrites substitution outside the abstraction. The source uses equality signs even where its cited lemma only gives alpha equivalence; no stronger claim is silently substituted.

Source

Exercise completing alpha representative substitution

Complete the proof for choosing representatives that make substitution defined. The missing cases remain exercises.

Source

Printed corollary on pairs of representatives

The corollary asserts existence of alpha equivalent representatives admitting substitution and uniqueness up to alpha equivalence. Its moreover clause repeats the first pair in its definedness condition and omits a condition on the second replacement; these anomalies are preserved and disclosed.

Source

Definition of de Bruijn terms

De Bruijn terms are natural number indices, applications of two de Bruijn terms, and unnamed abstractions with a de Bruijn term as body.

Source

Translation from named terms to de Bruijn terms

Capital F maps a variable to its position in the zero indexed environment, preserves application, and converts an abstraction by prepending its variable to the environment. Index zero refers to the nearest binder and index one to the next outer binder in the example.

Source

Three equations for translation to de Bruijn indices

The equations give the variable, application, and abstraction cases of capital F. The abstraction case prepends the bound variable before recursively translating the body.

Source

Recovery of named terms from de Bruijn terms

Capital G maps an index to the variable at that environment position, preserves application, and replaces an unnamed abstraction by a fresh named abstraction, prepending the chosen variable to the environment for the body.

Source

Three equations for recovery from de Bruijn indices

The equations give the index, application, and abstraction cases of capital G, with the fresh name chosen outside Gamma as required by the surrounding definition.

Source

De Bruijn translation is unchanged by alpha change

If capital M changes one bound variable to give capital M prime, their translations in an environment containing the free variables are syntactically identical. The statement is given without proof.

Source

Abstraction and application on alpha equivalence classes

Abstraction of class capital N is the class containing an abstraction of any representative of capital N. Application of two classes is the class containing the application of representatives of those classes.

Source

Free variables of an alpha equivalence class

The free variable set of a class is the free variable set of any representative; alpha invariance makes this independent of the representative.

Source

Substitution on alpha equivalence classes

Choose representatives of the term class and replacement class for which the earlier partial substitution is defined, and use that result for substitution on classes. This is the point where representatives may be renamed to satisfy the conditions; it does not retroactively change the earlier partial definition.

Source

Substitution example after passage to classes

Substituting y for x in the class represented by lambda x with body x is evaluated using the alpha equivalent representative lambda z with body z. The result is that same identity class, although the first syntactic substitution would have been undefined.

Source

Definition of beta contraction

Beta contraction is the smallest compatible relation containing application of lambda x with body capital N to capital Q reducing to substitution of capital Q for free x in capital N. Terms here are alpha equivalence classes as established in the preceding section.

Source

Exercise giving inductive beta contraction rules

Spell out equivalent inductive rules for beta contraction, following the earlier inductive definition of bound variable change. The rules are not supplied as an exercise solution.

Source

Definition of beta reduction

Beta reduction is the smallest reflexive transitive relation containing beta contraction, allowing zero or more directed beta steps.

Source

Definition of beta normal term

A term is beta normal if no beta contraction can be performed in it.

Source

Three step beta reduction to y

Apply lambda x with body x applied to x and then y to the identity abstraction. Three directed beta contractions end at y.

Source

Beta reduction increasing a term

A self application of lambda x with body x applied to x and then y produces its original self application followed by one more application to y at each displayed step. Reduction need not make a term shorter.

Source

Inductive definition of beta equivalence

Beta equivalence is reflexive, symmetric, and transitive; is compatible with application in either component and with abstraction; and contains the beta contraction equation. Equivalence allows contractions and their inverses, unlike directed beta reduction.

Source

Definition of eta contraction

An abstraction lambda x with body capital M applied to x contracts to capital M only when x is not free in capital M. Eta contraction is the smallest compatible relation containing these steps.

Source

Definition of beta eta reduction

Beta eta reduction is the smallest reflexive transitive relation containing both beta contraction and eta contraction; its steps remain directed.

Source

Extending equivalence by eta conversion

The source adds the equation lambda x with body f applied to x equals f and names the extended equivalence eta. The freshness condition from eta contraction is not repeated at this displayed rule and is discussed in a source note.

Source

Extensionality rule

If capital M applied to x is equivalent to capital N applied to x, then capital M is equivalent to capital N, provided x is free in neither capital M nor capital N. The resulting extension is named extensionality equivalence.

Source

Equivalence of eta and extensionality extensions

Equivalence obtained by adding extensionality holds exactly when equivalence obtained by adding eta conversion holds. The proof argues containment in both directions, retaining the required freshness premise.

Source

Cross-reference reference-000794

the abstraction formation clause

Source occurrence

Cross-reference reference-000795

the application formation clause

Source occurrence

Cross-reference reference-000796

the definition of lambda terms

Source occurrence

Cross-reference reference-000797

the definition of lambda terms

Source occurrence

Cross-reference reference-000798

the definition of lambda terms

Source occurrence

Cross-reference reference-000799

the variable formation clause

Source occurrence

Cross-reference reference-000800

the abstraction formation clause

Source occurrence

Cross-reference reference-000801

the application formation clause

Source occurrence

Cross-reference reference-000802

the lemma on the first symbol of a term

Source occurrence

Cross-reference reference-000803

the lemma that no proper initial part is a term

Source occurrence

Cross-reference reference-000804

the definition of lambda terms

Source occurrence

Cross-reference reference-000805

the variable formation clause

Source occurrence

Cross-reference reference-000806

the definition of lambda terms

Source occurrence

Cross-reference reference-000807

the variable formation clause

Source occurrence

Cross-reference reference-000808

the lemma on the first symbols of an application

Source occurrence

Cross-reference reference-000809

the definition of lambda terms

Source occurrence

Cross-reference reference-000810

the variable formation clause

Source occurrence

Cross-reference reference-000811

the lemma on the first symbol of a term

Source occurrence

Cross-reference reference-000812

the lemma that no proper initial part is a term

Source occurrence

Cross-reference reference-000813

the definition of lambda terms

Source occurrence

Cross-reference reference-000814

the free variable membership lemma

Source occurrence

Cross-reference reference-000815

the definition of partial substitution

Source occurrence

Cross-reference reference-000816

the substitution definition's abstraction clause

Source occurrence

Cross-reference reference-000817

the substitution definition's abstraction clause

Source occurrence

Cross-reference reference-000818

the definition of free variables

Source occurrence

Cross-reference reference-000819

the free variable definition's abstraction clause

Source occurrence

Cross-reference reference-000820

the definition of free variables

Source occurrence

Cross-reference reference-000821

the free variable definition's abstraction clause

Source occurrence

Cross-reference reference-000822

the substitution theorem for a variable not free in the term

Source occurrence

Cross-reference reference-000823

the substitution theorem for a variable free in the term

Source occurrence

Cross-reference reference-000824

the theorem on removal of a free variable by substitution

Source occurrence

Cross-reference reference-000825

the inverse substitution theorem

Source occurrence

Cross-reference reference-000826

the bound variable renaming clause

Source occurrence

Cross-reference reference-000827

the substitution theorem for a variable free in the term

Source occurrence

Cross-reference reference-000828

the substitution theorem for a variable not free in the term

Source occurrence

Cross-reference reference-000829

the lemma that one alpha change preserves free variables

Source occurrence

Cross-reference reference-000830

the bound variable renaming clause

Source occurrence

Cross-reference reference-000831

the theorem on removal of a free variable by substitution

Source occurrence

Cross-reference reference-000832

the inverse substitution theorem

Source occurrence

Cross-reference reference-000833

the bound variable renaming clause

Source occurrence

Cross-reference reference-000834

the lemma reversing one change of bound variable

Source occurrence

Cross-reference reference-000835

the lemma reversing one change of bound variable

Source occurrence

Cross-reference reference-000836

the lemma that one alpha change preserves free variables

Source occurrence

Cross-reference reference-000837

the substitution lemma for alpha equivalent replacement terms

Source occurrence

Cross-reference reference-000838

the section Substitution

Source occurrence

Cross-reference reference-000839

the inductive definition of one change of bound variable

Source occurrence

Cross-reference reference-000840

its abstraction compatibility clause

Source occurrence

Cross-reference reference-000841

the inductive definition of one change of bound variable

Source occurrence

Cross-reference reference-000842

the bound variable renaming clause

Source occurrence

Cross-reference reference-000843

the substitution lemma for alpha equivalent replacement terms

Source occurrence

Cross-reference reference-000844

the theorem choosing alpha equivalent representatives for defined substitution

Source occurrence

Cross-reference reference-000845

the theorem choosing alpha equivalent representatives for defined substitution

Source occurrence

Cross-reference reference-000846

the theorem that alpha equivalence preserves free variables

Source occurrence

Cross-reference reference-000847

the corollary on substitution using pairs of representatives

Source occurrence

Cross-reference reference-000848

the first labelled equation, substitution into the identity abstraction on x

Source occurrence

Cross-reference reference-000849

the second labelled equation, substitution into the identity abstraction on z

Source occurrence

Cross-reference reference-000850

the inductive definition of one change of bound variable

Source occurrence

Cross-reference reference-000851

the section Free Variables

Source occurrence

Source disclosures