Lambda calculus

The Church–Rosser Property

Equation form expr-0080085f4d896d4c

↠X⊆↠β\xred \subseteq \bred

Read as: the transitive X reduction relation is contained in the beta reduction relation

Means: the transitive X reduction relation is contained in the beta reduction relation

1 occurrence in this chapter

Equation form expr-0082654bf022cfd3

(λx.N)[R/y]⇒β(λx.N′)[R′/y]\Subst{(\lambd[x][N])}{R}{y} \bredpar \Subst{(\lambd[x][N'])}{R'}{y}

Read as: the result of substituting R for free y in the lambda abstraction binding x with body N parallel beta reduces to the result of substituting R prime for free y in the lambda abstraction binding x with body N prime

Means: the result of substituting R for free y in the lambda abstraction binding x with body N parallel beta reduces to the result of substituting R prime for free y in the lambda abstraction binding x with body N prime

1 occurrence in this chapter

Equation form expr-01a40a7768819a04

Q⇒βQ′Q \bredpar Q'

Read as: Q parallel beta reduces to Q prime

Means: Q parallel beta reduces to Q prime

6 occurrences in this chapter

Equation form expr-03fc8fd080d487a4

Ni,j→XNi,j+1N_{i,j} \xredone N_{i,j+1}

Read as: N at row i and column j is X related to N at row i and column j plus one

Means: N at row i and column j is X related to N at row i and column j plus one

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: M

Means: M

16 occurrences in this chapter

Equation form expr-0a944e1bad2bc954

PQ*β\bcd{PQ}

Read as: the beta complete development of the application of P to Q

Means: the beta complete development of the application of P to Q

1 occurrence in this chapter

Equation form expr-0ba99a976544ca69

PQ⇒βηP′Q′PQ \beredpar P'Q'

Read as: the application of P to Q parallel beta eta reduces to the application of P prime to Q prime

Means: the application of P to Q parallel beta eta reduces to the application of P prime to Q prime

1 occurrence in this chapter

Equation form expr-0c370aa793b02aac

Q′Q'

Read as: Q prime

Means: Q prime

4 occurrences in this chapter

Equation form expr-0c8e83226a0de392

P′Q′P'Q'

Read as: the application of P prime to Q prime

Means: the application of P prime to Q prime

2 occurrences in this chapter

Equation form expr-0ee8d8eddfc77d4e

Ni−1,j→XRN_{i-1,j} \xredone R

Read as: N at row i minus one and column j is X related to R

Means: N at row i minus one and column j is X related to R

1 occurrence in this chapter

Equation form expr-10155e91b2b87c65

x↠βxx \bred x

Read as: x beta reduces in zero or more steps to x

Means: x beta reduces in zero or more steps to x

1 occurrence in this chapter

Equation form expr-1149b846319f9cbe

N⇒βNN \bredpar N

Read as: N parallel beta reduces to N

Means: N parallel beta reduces to N

1 occurrence in this chapter

Equation form expr-1476d23f5d31bc31

λx.N⇒βηλx.N′\lambd[x][N] \beredpar \lambd[x][N']

Read as: the lambda abstraction binding x with body N parallel beta eta reduces to the lambda abstraction binding x with body N prime

Means: the lambda abstraction binding x with body N parallel beta eta reduces to the lambda abstraction binding x with body N prime

1 occurrence in this chapter

Equation form expr-156d370aff5639ac

λx.N⇒βλx.N′\lambd[x][N] \bredpar \lambd[x][N']

Read as: the lambda abstraction binding x with body N parallel beta reduces to the lambda abstraction binding x with body N prime

Means: the lambda abstraction binding x with body N parallel beta reduces to the lambda abstraction binding x with body N prime

1 occurrence in this chapter

Equation form expr-163059d8693f055f

(λx.N)Q⇒βηN′[Q′/x](\lambd[x][N])Q \beredpar \Subst{N'}{Q'}{x}

Read as: the application to Q of the lambda abstraction binding x with body N parallel beta eta reduces to the result of substituting Q prime for free x in N prime

Means: the application to Q of the lambda abstraction binding x with body N parallel beta eta reduces to the result of substituting Q prime for free x in N prime

1 occurrence in this chapter

Equation form expr-16fc2aa09c7cb8f1

P⇒βP′P \bredpar P'

Read as: P parallel beta reduces to P prime

Means: P parallel beta reduces to P prime

3 occurrences in this chapter

Equation form expr-17174f2b720673c7

P′Q′⇒βP*βQ*βP'Q' \bredpar \bcd{P}\bcd{Q}

Read as: the application of P prime to Q prime parallel beta reduces to the application of the beta complete development of P to the beta complete development of Q

Means: the application of P prime to Q prime parallel beta reduces to the application of the beta complete development of P to the beta complete development of Q

1 occurrence in this chapter

Equation form expr-189f40034be7a199

jj

Read as: j

Means: j

1 occurrence in this chapter

Equation form expr-1a8777dab730b37b

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

Read as: the lambda abstraction binding x with body the application of N to x

Means: the lambda abstraction binding x with body the application of N to x

4 occurrences in this chapter

Equation form expr-1d7c3d142cc64b63

λx.Nx⇒βηN′\lambd[x][Nx] \beredpar N'

Read as: the lambda abstraction binding x with body the application of N to x parallel beta eta reduces to N prime

Means: the lambda abstraction binding x with body the application of N to x parallel beta eta reduces to N prime

1 occurrence in this chapter

Equation form expr-1f115f25daa03d95

PQ↠βP′Q′PQ \bred P'Q'

Read as: the application of P to Q beta reduces in zero or more steps to the application of P prime to Q prime

Means: the application of P to Q beta reduces in zero or more steps to the application of P prime to Q prime

1 occurrence in this chapter

Equation form expr-203e3e8dfef015fb

x*β=x(λx.N)*β=λx.N*β(PQ)*β=P*βQ*βif P is not a λ-abstract((λx.N)Q)*β=N*β[Q*β/x]\bcd{x} &= x \ollabel{defn:bcd1} \\ \bcd{(\lambd[x][N])} &= \lambd[x][\bcd{N}] \ollabel{defn:bcd2}\\ \bcd{(PQ)} &= \bcd{P}\bcd{Q} && \text{if $P$ is not a $\lambd$-abstract} \ollabel{defn:bcd3} \\ \bcd{((\lambd[x][N])Q)} &= \Subst{\bcd{N}}{\bcd{Q}}{x} \ollabel{defn:bcd4}

Read as: Beta complete development, four defining equations. One: the beta complete development of x equals x. Two: the beta complete development of the lambda abstraction binding x with body N equals the lambda abstraction binding x with body the beta complete development of N. Three: the beta complete development of the application of P to Q equals the application of the beta complete development of P to the beta complete development of Q, if P is not a lambda abstraction. Four: the beta complete development of the application to Q of the lambda abstraction binding x with body N equals the result of substituting the beta complete development of Q for free x in the beta complete development of N. End of the four equations.

Means: Beta complete development, four defining equations. One: the beta complete development of x equals x. Two: the beta complete development of the lambda abstraction binding x with body N equals the lambda abstraction binding x with body the beta complete development of N. Three: the beta complete development of the application of P to Q equals the application of the beta complete development of P to the beta complete development of Q, if P is not a lambda abstraction. Four: the beta complete development of the application to Q of the lambda abstraction binding x with body N equals the result of substituting the beta complete development of Q for free x in the beta complete development of N. End of the four equations.

1 occurrence in this chapter

Equation form expr-2244bb53830676ef

N′⇒βη(λx.Nx)*βηN' \beredpar \becd{(\lambd[x][Nx])}

Read as: N prime parallel beta eta reduces to the beta eta complete development of the lambda abstraction binding x with body the application of N to x

Means: N prime parallel beta eta reduces to the beta eta complete development of the lambda abstraction binding x with body the application of N to x

1 occurrence in this chapter

Equation form expr-2661676702e9860a

Nm,0→X…→XNm,nN_{m,0} \xredone \dots \xredone N_{m,n}

Read as: a forward chain in the X arrow relation along row m, from N at row m and column zero through successive columns to N at row m and column n

Means: a forward chain in the X arrow relation along row m, from N at row m and column zero through successive columns to N at row m and column n

1 occurrence in this chapter

Equation form expr-26a8beba51f82d98

(λf.fx)(λy.y)(\lambd[f][fx])(\lambd[y][y])

Read as: the application of the lambda abstraction binding f with body f applied to x, to the lambda abstraction binding y with body y

Means: the application of the lambda abstraction binding f with body f applied to x, to the lambda abstraction binding y with body y

2 occurrences in this chapter

Equation form expr-28280bcf72ec2165

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

Read as: the lambda abstraction binding x with body N

Means: the lambda abstraction binding x with body N

4 occurrences in this chapter

Equation form expr-2cff90fadfdbf700

→X\xredone

Read as: the X arrow relation

Means: the X arrow relation

5 occurrences in this chapter

Equation form expr-2d711642b726b044

xx

Read as: x

Means: x

12 occurrences in this chapter

Equation form expr-2e80839badcead2f

→β\bredone

Read as: one step beta reduction

Means: one step beta reduction

1 occurrence in this chapter

Equation form expr-34f2797ad4ac12c6

Ni,j−1→XRN_{i,j-1} \xredone R

Read as: N at row i and column j minus one is X related to R

Means: N at row i and column j minus one is X related to R

1 occurrence in this chapter

Equation form expr-3e0534ff9dda7eeb

N′N'

Read as: N prime

Means: N prime

9 occurrences in this chapter

Equation form expr-450538d272a06a68

Nm,0N_{m,0}

Read as: N at row m and column zero

Means: N at row m and column zero

1 occurrence in this chapter

Equation form expr-45a0d814064bfc3f

((λx.N)Q)[R/y]⇒βN′[Q′/x][R′/y]\Subst{((\lambd[x][N])Q)}{R}{y} \bredpar \Subst{\Subst{N'}{Q'}{x}}{R'}{y}

Read as: the result of substituting R for free y in the application to Q of the lambda abstraction binding x with body N parallel beta reduces to the result of first substituting Q prime for free x in N prime, then substituting R prime for free y in that result

Means: the result of substituting R for free y in the application to Q of the lambda abstraction binding x with body N parallel beta reduces to the result of first substituting Q prime for free x in N prime, then substituting R prime for free y in that result

1 occurrence in this chapter

Equation form expr-47606cb1683e2eb7

Q⇒βQQ \bredpar Q

Read as: Q parallel beta reduces to Q

Means: Q parallel beta reduces to Q

1 occurrence in this chapter

Equation form expr-48565644f8db0b56

M′⇒βM*βM' \bredpar \bcd{M}

Read as: M prime parallel beta reduces to the beta complete development of M

Means: M prime parallel beta reduces to the beta complete development of M

1 occurrence in this chapter

Equation form expr-4a9f87d26e3ad495

Ni,j→XNi+1,jN_{i,j} \xredone N_{i+1,j}

Read as: N at row i and column j is X related to N at row i plus one and column j

Means: N at row i and column j is X related to N at row i plus one and column j

1 occurrence in this chapter

Equation form expr-4aba7322bb56bb57

N↠βN′N \bred N'

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

Means: N beta reduces in zero or more steps to N prime

4 occurrences in this chapter

Equation form expr-4ae81572f06e1b88

QQ

Read as: Q

Means: Q

11 occurrences in this chapter

Equation form expr-4de2a723ebf08c0f

m+1m + 1

Read as: m plus one

Means: m plus one

1 occurrence in this chapter

Equation form expr-4e07408562bedb8b

33

Read as: three

Means: three

1 occurrence in this chapter

Equation form expr-4e4a38abdd3ec9fc

→βη\beredone

Read as: one step beta eta reduction

Means: one step beta eta reduction

1 occurrence in this chapter

Equation form expr-506bf63d9af5e7b1

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

Read as: the application to Q of the lambda abstraction binding x with body N parallel beta reduces to the result of substituting Q for free x in N

Means: the application to Q of the lambda abstraction binding x with body N parallel beta reduces to the result of substituting Q for free x in N

1 occurrence in this chapter

Equation form expr-53d3365efbcac8f9

M⇒βηMM \beredpar M

Read as: M parallel beta eta reduces to M

Means: M parallel beta eta reduces to M

1 occurrence in this chapter

Equation form expr-53d4deec55439449

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

Read as: x is not a free variable of N

Means: x is not a free variable of N

4 occurrences in this chapter

Equation form expr-585d86d076ac5357

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

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

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

2 occurrences in this chapter

Equation form expr-58f354292e087ef2

M→XP1→X…→XPm andM→XQ1→X…→XQn.M & \xredone P_1 \xredone \dots \xredone P_m \text{ and}\\ M & \xredone Q_1 \xredone \dots \xredone Q_n.

Read as: Two chains in the X arrow relation start at M. The first passes through P subscript one and successive P terms through P subscript m. The second passes through Q subscript one and successive Q terms through Q subscript n. Every displayed arrow points forward along its chain.

Means: Two chains in the X arrow relation start at M. The first passes through P subscript one and successive P terms through P subscript m. The second passes through Q subscript one and successive Q terms through Q subscript n. Every displayed arrow points forward along its chain.

1 occurrence in this chapter

Equation form expr-59a94416a2a319ca

η\eta

Read as: eta

Means: eta

2 occurrences in this chapter

Equation form expr-5c62e091b8c0565f

PP

Read as: P

Means: P

10 occurrences in this chapter

Equation form expr-5e796122348ad180

(λx.N[R/y])Q[R/y]⇒βN′[R′/y][Q′[R′/y]/x](\lambd[x][\Subst{N}{R}{y}])\Subst{Q}{R}{y} \bredpar \Subst{\Subst{N'}{R'}{y}}{\Subst{Q'}{R'}{y}}{x}

Read as: the application of the lambda abstraction binding x with body the result of substituting R for free y in N, to the result of substituting R for free y in Q parallel beta reduces to the result of the following nested substitution: into N prime with R prime substituted for free y, substitute for free x the term Q prime with R prime substituted for free y

Means: the application of the lambda abstraction binding x with body the result of substituting R for free y in N, to the result of substituting R for free y in Q parallel beta reduces to the result of the following nested substitution: into N prime with R prime substituted for free y, substitute for free x the term Q prime with R prime substituted for free y

1 occurrence in this chapter

Equation form expr-60910b501a5110f6

n+1n + 1

Read as: n plus one

Means: n plus one

1 occurrence in this chapter

Equation form expr-609c913086baab36

M*βη\becd{M}

Read as: the beta eta complete development of M

Means: the beta eta complete development of M

1 occurrence in this chapter

Equation form expr-60fefe498d83cd06

↠β⊆↠X\bred \subseteq \xred

Read as: the beta reduction relation is contained in the transitive X reduction relation

Means: the beta reduction relation is contained in the transitive X reduction relation

1 occurrence in this chapter

Equation form expr-6566b2e368ba3595

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

Read as: the lambda abstraction binding x with body the result of substituting R for free y in N parallel beta reduces to the lambda abstraction binding x with body the result of substituting R for free y in N prime

Means: the lambda abstraction binding x with body the result of substituting R for free y in N parallel beta reduces to the lambda abstraction binding x with body the result of substituting R for free y in N prime

1 occurrence in this chapter

Equation form expr-66173b0ee70961e0

M≡M1⇒β…⇒βMk≡M′M \ident M_1 \bredpar \dots \bredpar M_k \ident M'

Read as: M is syntactically identical to M subscript one, followed by a chain of parallel beta reductions through successive terms to M subscript k, which is syntactically identical to M prime

Means: M is syntactically identical to M subscript one, followed by a chain of parallel beta reductions through successive terms to M subscript k, which is syntactically identical to M prime

2 occurrences in this chapter

Equation form expr-669c3a487d3981a5

N0,nN_{0,n}

Read as: N at row zero and column n

Means: N at row zero and column n

1 occurrence in this chapter

Equation form expr-671dbb1e1842000c

⇒βη\beredpar

Read as: parallel beta eta reduction

Means: parallel beta eta reduction

4 occurrences in this chapter

Equation form expr-6e57516f07f09c46

M⇒βMM \bredpar M

Read as: M parallel beta reduces to M

Means: M parallel beta reduces to M

1 occurrence in this chapter

Equation form expr-704880f17512002d

N0,n→X…→XNm,nN_{0,n} \xredone \dots \xredone N_{m,n}

Read as: a forward chain in the X arrow relation along column n, from N at row zero and column n through successive rows to N at row m and column n

Means: a forward chain in the X arrow relation along column n, from N at row zero and column n through successive rows to N at row m and column n

1 occurrence in this chapter

Equation form expr-716341c96ea168ef

Q′⇒βQ*βQ' \bredpar \bcd{Q}

Read as: Q prime parallel beta reduces to the beta complete development of Q

Means: Q prime parallel beta reduces to the beta complete development of Q

3 occurrences in this chapter

Equation form expr-723eb973b2aee866

P′⇒βP*βP' \bredpar \bcd{P}

Read as: P prime parallel beta reduces to the beta complete development of P

Means: P prime parallel beta reduces to the beta complete development of P

1 occurrence in this chapter

Equation form expr-72ce3728e83db0c6

N′⇒βN*βN' \bredpar \bcd{N}

Read as: N prime parallel beta reduces to the beta complete development of N

Means: N prime parallel beta reduces to the beta complete development of N

2 occurrences in this chapter

Equation form expr-76a8c8c02bf83b7a

M′M'

Read as: M prime

Means: M prime

14 occurrences in this chapter

Equation form expr-7854781e585c9b59

↠βη\bered

Read as: beta eta reduction

Means: beta eta reduction

3 occurrences in this chapter

Equation form expr-785c47196d5c6c47

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

Read as: the result of substituting Q for free x in N

Means: the result of substituting Q for free x in N

1 occurrence in this chapter

Equation form expr-7b5ee2f9a2747c45

M↠βηM′M \bered M'

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

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

1 occurrence in this chapter

Equation form expr-7bad2c37ad32ba0a

Q→XNQ \xredone N

Read as: Q is X related to N

Means: Q is X related to N

1 occurrence in this chapter

Equation form expr-7d0168599b9a9839

N′⇒βηN*βηN' \beredpar \becd{N}

Read as: N prime parallel beta eta reduces to the beta eta complete development of N

Means: N prime parallel beta eta reduces to the beta eta complete development of N

1 occurrence in this chapter

Equation form expr-805405b159da980e

M⇒βηM′M \beredpar M'

Read as: M parallel beta eta reduces to M prime

Means: M parallel beta eta reduces to M prime

7 occurrences in this chapter

Equation form expr-829e4d66733e1268

1+21+2

Read as: one plus two

Means: one plus two

1 occurrence in this chapter

Equation form expr-8493e54c76609cf2

N→βN′N \xrightarrow{\beta} N'

Read as: N beta reduces in one step to N prime

Means: N beta reduces in one step to N prime

2 occurrences in this chapter

Equation form expr-8523e0f7b38caf5a

N↠βηN′N \bered N'

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

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

1 occurrence in this chapter

Equation form expr-86fa5a5b7a833ae8

PQPQ

Read as: the application of P to Q

Means: the application of P to Q

2 occurrences in this chapter

Equation form expr-8c2574892063f995

RR

Read as: R

Means: R

1 occurrence in this chapter

Equation form expr-8ce86a6ae65d3692

NN

Read as: N

Means: N

14 occurrences in this chapter

Equation form expr-8ceba25ef8b30d9e

((λx.N)Q)*β\bcd{((\lambd[x][N])Q)}

Read as: the beta complete development of the application to Q of the lambda abstraction binding x with body N

Means: the beta complete development of the application to Q of the lambda abstraction binding x with body N

1 occurrence in this chapter

Equation form expr-8d6ce9fe6deb3086

x*βη=x(λx.N)*βη=λx.N*βη(PQ)*βη=P*βηQ*βηif P is not a λ-abstract((λx.N)Q)*βη=N*βη[Q*βη/x](λx.Nx)*βη=N*βηif x∉FV(N)\becd{x} &= x \ollabel{defn:becd1} \\ \becd{(\lambd[x][N])} &= \lambd[x][\becd{N}] \ollabel{defn:becd2}\\ \becd{(PQ)} &= \becd{P}\becd{Q} && \text{if $P$ is not a $\lambd$-abstract} \ollabel{defn:becd3} \\ \becd{((\lambd[x][N])Q)} &= \Subst{\becd{N}}{\becd{Q}}{x} \ollabel{defn:becd4} \\ \becd{(\lambd[x][Nx])} &= \becd{N} \ollabel{defn:becd5} & \text{if $x \notin FV(N)$}

Read as: Beta eta complete development, five source equations. One: the beta eta complete development of x equals x. Two: the beta eta complete development of the lambda abstraction binding x with body N equals the lambda abstraction binding x with body the beta eta complete development of N. Three: the beta eta complete development of the application of P to Q equals the application of the beta eta complete development of P to the beta eta complete development of Q, if P is not a lambda abstraction. Four: the beta eta complete development of the application to Q of the lambda abstraction binding x with body N equals the result of substituting the beta eta complete development of Q for free x in the beta eta complete development of N. Five: the beta eta complete development of the lambda abstraction binding x with body the application of N to x equals the beta eta complete development of N, if x is not a free variable of N. End of the five source equations.

Means: Beta eta complete development, five source equations. One: the beta eta complete development of x equals x. Two: the beta eta complete development of the lambda abstraction binding x with body N equals the lambda abstraction binding x with body the beta eta complete development of N. Three: the beta eta complete development of the application of P to Q equals the application of the beta eta complete development of P to the beta eta complete development of Q, if P is not a lambda abstraction. Four: the beta eta complete development of the application to Q of the lambda abstraction binding x with body N equals the result of substituting the beta eta complete development of Q for free x in the beta eta complete development of N. Five: the beta eta complete development of the lambda abstraction binding x with body the application of N to x equals the beta eta complete development of N, if x is not a free variable of N. End of the five source equations.

1 occurrence in this chapter

Equation form expr-942b93933c5272db

λx.N′⇒β(λx.N)*β\lambd[x][N'] \bredpar \bcd{(\lambd[x][N])}

Read as: the lambda abstraction binding x with body N prime parallel beta reduces to the beta complete development of the lambda abstraction binding x with body N

Means: the lambda abstraction binding x with body N prime parallel beta reduces to the beta complete development of the lambda abstraction binding x with body N

1 occurrence in this chapter

Equation form expr-94a93d6a97d68ca6

λx.N′⇒βλx.N*β\lambd[x][N'] \bredpar \lambd[x][\bcd{N}]

Read as: the lambda abstraction binding x with body N prime parallel beta reduces to the lambda abstraction binding x with body the beta complete development of N

Means: the lambda abstraction binding x with body N prime parallel beta reduces to the lambda abstraction binding x with body the beta complete development of N

1 occurrence in this chapter

Equation form expr-978668c22e0a2d30

M→XQM \xredone Q

Read as: M is X related to Q

Means: M is X related to Q

1 occurrence in this chapter

Equation form expr-9929954f54fa92a7

↠X\xred

Read as: the transitive X reduction relation

Means: the transitive X reduction relation

5 occurrences in this chapter

Equation form expr-99e63d419521c210

(λx.N′)Q′⇒βN*β[Q*β/x](\lambd[x][N'])Q' \bredpar \Subst{\bcd{N}}{\bcd{Q}}{x}

Read as: the application to Q prime of the lambda abstraction binding x with body N prime parallel beta reduces to the result of substituting the beta complete development of Q for free x in the beta complete development of N

Means: the application to Q prime of the lambda abstraction binding x with body N prime parallel beta reduces to the result of substituting the beta complete development of Q for free x in the beta complete development of N

1 occurrence in this chapter

Equation form expr-9a3c4175e76ff6ef

Ni,jN_{i,j}

Read as: N at row i and column j

Means: N at row i and column j

1 occurrence in this chapter

Equation form expr-9b132b3fe4db985c

⇒β\bredpar

Read as: parallel beta reduction

Means: parallel beta reduction

6 occurrences in this chapter

Equation form expr-9d2c8d54c906576f

Q⇒βηQ′Q \beredpar Q'

Read as: Q parallel beta eta reduces to Q prime

Means: Q parallel beta eta reduces to Q prime

2 occurrences in this chapter

Equation form expr-9e06c570e1a4a009

↠β\bred

Read as: beta reduction

Means: beta reduction

3 occurrences in this chapter

Equation form expr-9e93b70549062c65

(λx.Nx)[R/y]⇒βηN′[R′/y]\Subst{(\lambd[x][Nx])}{R}{y} \beredpar \Subst{N'}{R'}{y}

Read as: the result of substituting R for free y in the lambda abstraction binding x with body the application of N to x parallel beta eta reduces to the result of substituting R prime for free y in N prime

Means: the result of substituting R for free y in the lambda abstraction binding x with body the application of N to x parallel beta eta reduces to the result of substituting R prime for free y in N prime

1 occurrence in this chapter

Equation form expr-9f87e1cb54ce84fa

4×1+4×2+34 \times 1+4 \times 2+3

Read as: four times one, plus four times two, plus three

Means: four times one, plus four times two, plus three

1 occurrence in this chapter

Equation form expr-a234136d6d3f072c

N⇒βηN′N \beredpar N'

Read as: N parallel beta eta reduces to N prime

Means: N parallel beta eta reduces to N prime

5 occurrences in this chapter

Equation form expr-a3cb0fc97868cb0a

(λx.N)Q⇒βN′[Q′/x](\lambd[x][N])Q \bredpar \Subst{N'}{Q'}{x}

Read as: the application to Q of the lambda abstraction binding x with body N parallel beta reduces to the result of substituting Q prime for free x in N prime

Means: the application to Q of the lambda abstraction binding x with body N parallel beta reduces to the result of substituting Q prime for free x in N prime

1 occurrence in this chapter

Equation form expr-a8102cc3b7e5e215

M→XPM \xredone P

Read as: M is X related to P

Means: M is X related to P

1 occurrence in this chapter

Equation form expr-a956d7cbce60c1f7

x⇒βxx \bredpar x

Read as: x parallel beta reduces to x

Means: x parallel beta reduces to x

1 occurrence in this chapter

Equation form expr-aad03dc357494737

M→βηM′M \beredone M'

Read as: M beta eta reduces in one step to M prime

Means: M beta eta reduces in one step to M prime

2 occurrences in this chapter

Equation form expr-abe0d4a99d82f0c7

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

Read as: the result of substituting Q prime for free x in N prime

Means: the result of substituting Q prime for free x in N prime

4 occurrences in this chapter

Equation form expr-ae11c5d4d5bcb948

4×(1+2)4 \times (1+2)

Read as: four times the quantity one plus two

Means: four times the quantity one plus two

1 occurrence in this chapter

Equation form expr-afaf141a2b1c3c3d

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

Read as: the application to Q prime of the lambda abstraction binding x with body N prime

Means: the application to Q prime of the lambda abstraction binding x with body N prime

1 occurrence in this chapter

Equation form expr-b25b33fbd94e5ff3

R⇒βR′R \bredpar R'

Read as: R parallel beta reduces to R prime

Means: R parallel beta reduces to R prime

1 occurrence in this chapter

Equation form expr-b38d9d5a2b9e2cfb

4×3+34 \times 3+3

Read as: four times three, then plus three

Means: four times three, then plus three

1 occurrence in this chapter

Equation form expr-b3f57f50afefd8b6

M′⇒βηM*βηM' \beredpar \becd{M}

Read as: M prime parallel beta eta reduces to the beta eta complete development of M

Means: M prime parallel beta eta reduces to the beta eta complete development of M

1 occurrence in this chapter

Equation form expr-b729d802fb24959b

12+312+3

Read as: twelve plus three

Means: twelve plus three

1 occurrence in this chapter

Equation form expr-b7811d7730dbff84

λx.N↠βλx.N′\lambd[x][N] \bred \lambd[x][N']

Read as: the lambda abstraction binding x with body N beta reduces in zero or more steps to the lambda abstraction binding x with body N prime

Means: the lambda abstraction binding x with body N beta reduces in zero or more steps to the lambda abstraction binding x with body N prime

1 occurrence in this chapter

Equation form expr-b78eaa654b95e6a3

M≡M1→β…→βMk≡M′M \ident M_1 \bredone \dots \bredone M_k \ident M'

Read as: M is syntactically identical to M subscript one, followed by a chain of one step beta reductions through successive terms to M subscript k, which is syntactically identical to M prime

Means: M is syntactically identical to M subscript one, followed by a chain of one step beta reductions through successive terms to M subscript k, which is syntactically identical to M prime

1 occurrence in this chapter

Equation form expr-b973f82585d6dbcc

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

Read as: the result of substituting R for free y in M parallel beta reduces to the result of substituting R prime for free y in M prime

Means: the result of substituting R for free y in M parallel beta reduces to the result of substituting R prime for free y in M prime

1 occurrence in this chapter

Equation form expr-bb3dbc389b0c7c6d

M↠βM′M \bred M'

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

Means: M beta reduces in zero or more steps to M prime

3 occurrences in this chapter

Equation form expr-bcf3b6fbaa82fba7

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

Read as: the lambda abstraction binding x with body N prime

Means: the lambda abstraction binding x with body N prime

4 occurrences in this chapter

Equation form expr-bf2170b7b5dbcc4e

(λx.N)Q↠βN′[Q′/x](\lambd[x][N])Q \bred \Subst{N'}{Q'}{x}

Read as: the application to Q of the lambda abstraction binding x with body N beta reduces in zero or more steps to the result of substituting Q prime for free x in N prime

Means: the application to Q of the lambda abstraction binding x with body N beta reduces in zero or more steps to the result of substituting Q prime for free x in N prime

1 occurrence in this chapter

Equation form expr-c3cbdf57d608506a

M≡M1↠β…↠βMk≡M′M \ident M_1 \bred \dots \bred M_k \ident M'

Read as: M is syntactically identical to M subscript one, followed by beta reductions through successive terms to M subscript k, which is syntactically identical to M prime

Means: M is syntactically identical to M subscript one, followed by beta reductions through successive terms to M subscript k, which is syntactically identical to M prime

1 occurrence in this chapter

Equation form expr-c54d611ef9ccb254

Q↠βQ′Q \bred Q'

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

Means: Q beta reduces in zero or more steps to Q prime

4 occurrences in this chapter

Equation form expr-c5f14bbd3d6a8d38

P↠βP′P \bred P'

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

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

2 occurrences in this chapter

Equation form expr-c6bfadccca263ff7

βη\beta\eta

Read as: beta eta

Means: beta eta

9 occurrences in this chapter

Equation form expr-c9b06458c7742d9e

M⇒βM′M \bredpar M'

Read as: M parallel beta reduces to M prime

Means: M parallel beta reduces to M prime

7 occurrences in this chapter

Equation form expr-ce1a564629c6f7ea

M[R/y]⇒βηM′[R′/y]\Subst{M}{R}{y} \beredpar \Subst{M'}{R'}{y}

Read as: the result of substituting R for free y in M parallel beta eta reduces to the result of substituting R prime for free y in M prime

Means: the result of substituting R for free y in M parallel beta eta reduces to the result of substituting R prime for free y in M prime

1 occurrence in this chapter

Equation form expr-cec4b8919e5f12a5

P′P'

Read as: P prime

Means: P prime

3 occurrences in this chapter

Equation form expr-cf453e913ed5c59b

P⇒βηP′P \beredpar P'

Read as: P parallel beta eta reduces to P prime

Means: P parallel beta eta reduces to P prime

1 occurrence in this chapter

Equation form expr-cff7f90a5f2bed6c

P→XNP \xredone N

Read as: P is X related to N

Means: P is X related to N

1 occurrence in this chapter

Equation form expr-d0b7bf19cd9ab9de

N′[Q′/x]⇒βN*β[Q*β/x]\Subst{N'}{Q'}{x} \bredpar \Subst{\bcd{N}}{\bcd{Q}}{x}

Read as: the result of substituting Q prime for free x in N prime parallel beta reduces to the result of substituting the beta complete development of Q for free x in the beta complete development of N

Means: the result of substituting Q prime for free x in N prime parallel beta reduces to the result of substituting the beta complete development of Q for free x in the beta complete development of N

1 occurrence in this chapter

Equation form expr-d9862f98f5d17e28

λx.N[R/y]x⇒βηN′[R′/y]\lambd[x][\Subst{N}{R}{y} x] \beredpar \Subst{N'}{R'}{y}

Read as: the lambda abstraction binding x with body the application to x of the result of substituting R for free y in N parallel beta eta reduces to the result of substituting R prime for free y in N prime

Means: the lambda abstraction binding x with body the application to x of the result of substituting R for free y in N parallel beta eta reduces to the result of substituting R prime for free y in N prime

1 occurrence in this chapter

Equation form expr-de4f41de921e5608

PQ⇒βP′Q′PQ \bredpar P'Q'

Read as: the application of P to Q parallel beta reduces to the application of P prime to Q prime

Means: the application of P to Q parallel beta reduces to the application of P prime to Q prime

1 occurrence in this chapter

Equation form expr-de7d1b721a1e0632

ii

Read as: i

Means: i

1 occurrence in this chapter

Equation form expr-df2d89f6494f5b81

N⇒βN′N \bredpar N'

Read as: N parallel beta reduces to N prime

Means: N parallel beta reduces to N prime

7 occurrences in this chapter

Equation form expr-e29db7a8e2984d37

4×(1+2)+34 \times (1+2) + 3

Read as: four times the quantity one plus two, then plus three

Means: four times the quantity one plus two, then plus three

1 occurrence in this chapter

Equation form expr-e629fa6598d73276

1515

Read as: fifteen

Means: fifteen

1 occurrence in this chapter

Equation form expr-ea07b065e84f2363

M*β\bcd{M}

Read as: the beta complete development of M

Means: the beta complete development of M

1 occurrence in this chapter

Equation form expr-ee983ce9ba2c4f07

M↠XM′M \xred M'

Read as: M X reduces to M prime

Means: M X reduces to M prime

2 occurrences in this chapter

Equation form expr-f2a6f79ba5441848

x⇒βηxx \beredpar x

Read as: x parallel beta eta reduces to x

Means: x parallel beta eta reduces to x

1 occurrence in this chapter

Equation form expr-f3f3804480e8551a

β\beta

Read as: beta

Means: beta

16 occurrences in this chapter

Equation form expr-f44e26ed80d67418

M→βM′M \bredone M'

Read as: M beta reduces in one step to M prime

Means: M beta reduces in one step to M prime

3 occurrences in this chapter

Equation form expr-f6eb08b5772c020d

4×(1+2)+34 \times (1+2)+3

Read as: four times the quantity one plus two, then plus three

Means: four times the quantity one plus two, then plus three

1 occurrence in this chapter

Equation form expr-f7bcd13e533602a5

N0,0=MNi,0=Piif 1≤i≤mN0,j=Qjif 1≤j≤nand otherwise:Ni,j=RN_{0,0} &= M \\ N_{i,0} &= P_i && \text{if } 1 \le i \le m \\ N_{0,j} &= Q_j && \text{if } 1 \le j \le n \\ \intertext{and otherwise:} N_{i,j} &= R

Read as: Grid definition. N at row zero and column zero equals M. N at row i and column zero equals P subscript i, for one less than or equal to i less than or equal to m. N at row zero and column j equals Q subscript j, for one less than or equal to j less than or equal to n. Otherwise, N at row i and column j equals R, the common successor specified immediately after this display. End of grid definition.

Means: Grid definition. N at row zero and column zero equals M. N at row i and column zero equals P subscript i, for one less than or equal to i less than or equal to m. N at row zero and column j equals Q subscript j, for one less than or equal to j less than or equal to n. Otherwise, N at row i and column j equals R, the common successor specified immediately after this display. End of grid definition.

1 occurrence in this chapter

Equation form expr-f8f2b718f8df5074

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

Read as: the application to Q of the lambda abstraction binding x with body N

Means: the application to Q of the lambda abstraction binding x with body N

4 occurrences in this chapter

Equation form expr-fbaec1115f44c33a

R⇒βηR′R \beredpar R'

Read as: R parallel beta eta reduces to R prime

Means: R parallel beta eta reduces to R prime

1 occurrence in this chapter

Definition of the Church Rosser property

For the relation denoted by an X labelled arrow, whenever M is related to P and M is related to Q, there is a term N to which both P and Q are related. The common successor is existentially quantified after the two branches; the arrow direction is not reversed.

Source

Church Rosser property passes to transitive closure

If the source relation has the Church Rosser property, its smallest transitive extension also has it. The source proof constructs a rectangular grid whose left and upper edges are the two given chains, and whose lower right corner is their common descendant.

Source

Two forward reduction chains from M

The first row is the X arrow chain from M through the P terms to P subscript m. The second row is the X arrow chain from M through the Q terms to Q subscript n. These rows are two hypotheses, not equalities or alternative conclusions.

Source

Recursive construction of the joining grid

The upper left entry is M, the left edge contains the P chain, and the upper edge contains the Q chain. Each remaining entry is a common X arrow successor of the entry above and the entry to its left. The two resulting boundary chains meet at row m, column n.

Source

Four source rules for parallel beta reduction

The source lists the variable, abstraction, application, and beta contraction rules. Application reduces its function and argument in parallel; contraction substitutes the reduced argument into the reduced body. The abstraction premise is printed as ordinary one step beta reduction, a separately disclosed source inconsistency. It is not silently read as parallel reduction.

Source

Reflexivity of parallel beta reduction

The source asserts that every term M parallel beta reduces to itself. Its proof is marked Exercise and is not supplied in this edition. The preceding definition's abstraction-premise issue remains disclosed.

Source

Exercise proving parallel beta reflexivity

Prove the preceding reflexivity theorem for parallel beta reduction. The exercise remains unsolved; the edition does not add an induction proof.

Source

Definition of beta complete development

Four equations recursively specify the development of a variable, abstraction, application whose function is not an abstraction, and beta redex. The redex equation develops body and argument before substituting. Only redexes of the original term are contracted; newly created redexes are not automatically contracted again.

Source

Four beta complete development equations

Read the four labelled equations in source order: variable, abstraction, non-redex application, then redex application. The non-abstraction condition belongs only to the third equation. The fourth equation substitutes the complete development of Q for free x in the complete development of N.

Source

Parallel beta reduction and substitution

If M parallel beta reduces to M prime and R parallel beta reduces to R prime, the source claims the corresponding substitutions for y are related. The proof uses induction on the first reduction, leaving the variable and ordinary application cases as exercises. Its dropped prime and unstated substitution-definedness conditions are disclosed separately, not repaired by adding a new proof.

Source

Exercise completing the parallel beta substitution proof

Complete the preceding substitution compatibility proof. The cases labelled Exercise remain open. No missing cases or additional assumptions are supplied as an exercise solution.

Source

Every parallel beta reduct reaches the complete development

If M parallel beta reduces to M prime, then M prime parallel beta reduces to the beta complete development of M. The proof splits by the final rule and, in the application case, whether the original function is a lambda abstraction. The variable case remains Exercise.

Source

Exercise completing the beta complete development lemma

Complete the proof that every parallel beta reduct reaches the original term's beta complete development in a parallel step. The omitted source case is not filled in.

Source

Church Rosser property for parallel beta reduction

The source concludes the Church Rosser property from the complete-development lemma: any two parallel reducts are asserted to have that development as a common parallel successor. This is the source's argument, with its earlier definition caveat retained.

Source

One beta contraction is a parallel beta reduction

The source claims inclusion of one step beta reduction in parallel beta reduction. Its written proof demonstrates the outermost beta redex using parallel reflexivity of body and argument; the missing compatible-context cases are disclosed separately, not silently supplied.

Source

A parallel beta step can be serialized

Parallel beta reduction is contained in ordinary beta reduction. The proof follows the four parallel rules. In the contraction case it reduces the body, reduces the argument, and then contracts the resulting outer redex. Zero ordinary steps cover the reflexive variable case.

Source

Beta reduction is the transitive closure of parallel beta reduction

The source proves both relation inclusions. A chain of ordinary beta contractions becomes a chain of parallel reductions; conversely, a chain of parallel reductions can be serialized into ordinary beta reductions. Syntactic identity marks the chain endpoints, and is distinct from a reduction arrow.

Source

Church Rosser property for beta reduction

The source combines the transitive-closure theorem, the parallel beta Church Rosser theorem, and the equality of ordinary beta reduction with the transitive closure of parallel beta reduction.

Source

Five source rules for parallel beta eta reduction

The source gives variable, abstraction, application, beta contraction, and eta contraction rules. The eta rule reduces the abstraction binding x with body N applied to x to N prime when N parallel beta eta reduces to N prime and x is not free in N. The abstraction premise is printed as ordinary one step beta, with a separate source caveat.

Source

Reflexivity of parallel beta eta reduction

The source asserts that M parallel beta eta reduces to itself. The proof is marked Exercise and remains unsolved, with the definition caveat disclosed.

Source

Exercise proving parallel beta eta reflexivity

Prove the preceding reflexivity theorem for parallel beta eta reduction. The source exercise is not solved in this edition.

Source

Source definition of beta eta complete development

Five equations describe variables, abstractions, non-redex applications, beta redexes, and eta redexes. The second and fifth equations overlap on eta redexes without a stated precedence rule. Both equations remain intact with a source caveat; the edition does not choose a replacement algorithm.

Source

Five beta eta complete development equations

The equations are read in source order without imposing priority. Equation three requires that P not be a lambda abstraction. Equation five requires that x not occur free in N. These side conditions are attached to their own equations, and the overlap of equations two and five is explicitly disclosed.

Source

Parallel beta eta reduction and substitution

The source extends the parallel beta substitution compatibility claim with an eta case. It substitutes R for y under an abstraction binding x and then appeals to the eta rule and induction. Definedness and fresh-variable assumptions for these steps are not stated and are disclosed rather than silently added.

Source

Source beta eta complete development lemma

The source claims every parallel beta eta reduct reaches the original term's beta eta complete development. It refers the first four proof cases to the beta proof, then treats the eta case. The overlap in the definition and the extra interaction of eta contraction with abstraction shape remain source caveats.

Source

Source Church Rosser theorem for parallel beta eta reduction

The source derives the Church Rosser property from its preceding complete-development lemma. The theorem and its dependency links are preserved; the edition does not claim to have repaired the source's definition or proof gaps.

Source

One beta eta contraction is a parallel beta eta reduction

The source proof adds an eta case to the beta argument and refers to the earlier eta-contraction definition. Its eta case incorrectly prints a beta-only arrow; the original arrow remains spoken with a separate source caveat.

Source

A parallel beta eta step can be serialized

In the additional eta case, first contract the abstraction binding x with body N applied to x to N, using the condition that x is not free in N. Then follow the ordinary beta eta sequence from N to N prime supplied by the induction hypothesis. The source supplies only this additional case here.

Source

Beta eta reduction is the transitive closure of parallel beta eta reduction

The source asserts this equality of relations and refers back to the analogous beta proof. That reference is retained rather than replaced with a newly authored proof.

Source

Church Rosser property for beta eta reduction

The source combines the general transitive-closure theorem, its parallel beta eta Church Rosser theorem, and the beta eta closure lemma. All three dependency references are retained, with the earlier source caveats still available.

Source

Cross-reference reference-000852

the theorem on reflexivity of parallel beta reduction

Source occurrence

Cross-reference reference-000853

the variable rule for parallel beta reduction

Source occurrence

Cross-reference reference-000854

the abstraction rule for parallel beta reduction

Source occurrence

Cross-reference reference-000855

the abstraction rule for parallel beta reduction

Source occurrence

Cross-reference reference-000856

the application rule for parallel beta reduction

Source occurrence

Cross-reference reference-000857

the contraction rule for parallel beta reduction

Source occurrence

Cross-reference reference-000858

the contraction rule for parallel beta reduction

Source occurrence

Cross-reference reference-000859

the substitution compatibility lemma for parallel beta reduction

Source occurrence

Cross-reference reference-000860

the variable rule for parallel beta reduction

Source occurrence

Cross-reference reference-000861

the abstraction rule for parallel beta reduction

Source occurrence

Cross-reference reference-000862

the abstraction equation for beta complete development

Source occurrence

Cross-reference reference-000863

the abstraction rule for parallel beta reduction

Source occurrence

Cross-reference reference-000864

the application rule for parallel beta reduction

Source occurrence

Cross-reference reference-000865

the contraction rule for parallel beta reduction

Source occurrence

Cross-reference reference-000866

the application rule for parallel beta reduction

Source occurrence

Cross-reference reference-000867

the non-redex application equation for beta complete development

Source occurrence

Cross-reference reference-000868

the contraction rule for parallel beta reduction

Source occurrence

Cross-reference reference-000869

the substitution compatibility lemma for parallel beta reduction

Source occurrence

Cross-reference reference-000870

the lemma that every parallel beta reduct reaches the complete development

Source occurrence

Cross-reference reference-000871

the lemma that every parallel beta reduct reaches the complete development

Source occurrence

Cross-reference reference-000872

the theorem on reflexivity of parallel beta reduction

Source occurrence

Cross-reference reference-000873

the definition of parallel beta reduction

Source occurrence

Cross-reference reference-000874

the contraction rule for parallel beta reduction

Source occurrence

Cross-reference reference-000875

the variable rule for parallel beta reduction

Source occurrence

Cross-reference reference-000876

the abstraction rule for parallel beta reduction

Source occurrence

Cross-reference reference-000877

the application rule for parallel beta reduction

Source occurrence

Cross-reference reference-000878

the contraction rule for parallel beta reduction

Source occurrence

Cross-reference reference-000879

the lemma that one beta contraction is a parallel beta reduction

Source occurrence

Cross-reference reference-000880

the lemma serializing parallel beta reduction

Source occurrence

Cross-reference reference-000881

the theorem that transitive closure preserves the Church Rosser property

Source occurrence

Cross-reference reference-000882

the Church Rosser theorem for parallel beta reduction

Source occurrence

Cross-reference reference-000883

the lemma identifying beta reduction as the transitive closure of parallel beta reduction

Source occurrence

Cross-reference reference-000884

the theorem on reflexivity of parallel beta eta reduction

Source occurrence

Cross-reference reference-000885

the substitution compatibility lemma for parallel beta reduction

Source occurrence

Cross-reference reference-000886

the eta rule for parallel beta eta reduction

Source occurrence

Cross-reference reference-000887

the definition of parallel beta eta reduction

Source occurrence

Cross-reference reference-000888

the eta rule for parallel beta eta reduction

Source occurrence

Cross-reference reference-000889

the lemma that every parallel beta reduct reaches the complete development

Source occurrence

Cross-reference reference-000890

the eta rule for parallel beta eta reduction

Source occurrence

Cross-reference reference-000891

the source lemma that every parallel beta eta reduct reaches the complete development

Source occurrence

Cross-reference reference-000892

the earlier definition of eta contraction

Source occurrence

Cross-reference reference-000893

the theorem on reflexivity of parallel beta eta reduction

Source occurrence

Cross-reference reference-000894

the lemma that one beta contraction is a parallel beta reduction

Source occurrence

Cross-reference reference-000895

the eta rule for parallel beta eta reduction

Source occurrence

Cross-reference reference-000896

the lemma identifying beta reduction as the transitive closure of parallel beta reduction

Source occurrence

Cross-reference reference-000897

the theorem that transitive closure preserves the Church Rosser property

Source occurrence

Cross-reference reference-000898

the Church Rosser theorem for parallel beta eta reduction

Source occurrence

Cross-reference reference-000899

the lemma identifying beta eta reduction as the transitive closure of parallel beta eta reduction

Source occurrence

Source disclosures