# Programming Languages and Lambda Calculi exercises

The manuscript can be found here.

## Part I: Models of Languages

### Chapter 1: Computing with Text

#### 1.1 Defining Sets

• `t`B
• `f`B
• (B1B2) ∈ B

Exercise 1.1. Which of the following are in B? For each member of B, provide a proof tree showing that it must be in B.

1. `t`
2. ((`f``t`) • (`f``f`))
3. ((`f`) • (`t`))

`t` is in B:

``````t ∈ B
``````

((`f``t`) • (`f``f`)) is in B:

``````  f ∈ B  t ∈ B      f ∈ B  f ∈ B
----------------  ----------------
(f • t) ∈ B       (f • f) ∈ B
---------------------------------
((f • t) • (f • f)) ∈ B
``````

#### 1.2 Relations

• (`f`B1) r B1
• (`t`B1) r `t`
• (`f`B1) ≍r B1
• (`t`B1) ≍r `t`
• B1r B1
• (`f`B1) ≈r B1
• (`t`B1) ≈r `t`
• B1r B1
• B1r B2B2r B1
• B1r B2 and B2r B3B1r B3

#### 1.4 Directed Evaluation

↝↝r is the reflexive–transitive closure of r:

• B1 ↝↝r B1
• B1 r B2B1 ↝↝r B2
• B1 ↝↝r B2 and B2 ↝↝r B3B1 ↝↝r B3

Exercise 1.2. Show that (`f` • (`f` • (`f``f`))) ↝↝r `f` by showing its reduction with the `r` one-step relation.

``````(f • (f • (f • f))) r (f • (f • f))
r (f • f)
r f
``````

#### 1.5 Evaluation in Context

• B1 r B2B1r B2
• B1r B1′ ⇒ (B1B2) →r (B1′ • B2)
• B2r B2′ ⇒ (B1B2) →r (B1B2′)

r is the reflexive–transitive closure of →r.

=r is the equivalence closure of →r.

Exercise 1.3. Explain why (`f` • ((`t``f`) • `f`)) !↝↝r `t`.

``````(f • ((t • f) • f)) r ((t • f) • f)
``````

That’s all, we can’t reduce it any more because we can not apply either rule to ((`t``f`) • `f`).

Exercise 1.4. Show that (`f` • ((`t``f`) • `f`)) ↠r `t` by demonstrating a reduction with →r.

``````                                                  (t • f) r t
----------------
(f • ((t • f) • f)) r ((t • f) • f)             (t • f) →r t            (t • f) r t
----------------------------------------  ----------------------------  ----------------
(f • ((t • f) • f)) →r ((t • f) • f)      ((t • f) • f) →r (t • f)      (t • f) →r t
----------------------------------------------------------------------------------------
(f • ((t • f) • f)) ↠r t
``````

#### 1.6 Evaluation Function

• evalr(B) = `f` if B =r `f`
• evalr(B) = `t` if B =r `t`

Exercise 1.5. Among the relations r, ≍r, ≈r, ↝↝r, →r, ↠r, =r, and evalr, which are functions? For each non-function relation, find an expression and two expressions that it relates to.

Relation r and evalr are functions.

r is not function:

``````(t • B1) ≍r B1
(t • B1) ≍r (t • B1)
``````

r is not function:

``````(t • B1) ≈r B1
(t • B1) ≈r (t • B1)
``````

↝↝r is not function:

``````(t • B1) ↝↝r (t • B1)
(t • B1) ↝↝r t
``````

r is not function:

``````((t • B1) • (t • B1)) →r (t • (t • B1))
((t • B1) • (t • B1)) →r ((t • B1) • t)
``````

r is not function:

``````(t • B1) ↠r (t • B1)
(t • B1) ↠r t
``````

=r is not function:

``````(t • B1) =r (t • B1)
(t • B1) =r t
``````

### Chapter 2: Structural Induction

#### 2.1 Detecting the Need for Structural Induction

• P = α | (βP) | (PP)

Theorem 2.2: For any P, P contains at least one α.

Exercise 2.1. Prove Theorem 2.2.

• Base case:

• Case α

α contains one α, the claim holds.

• Inductive cases:

• Case (βP)

By induction, P contains at least one α, therefore (βP) contains at least one α, the claim holds.

• Case (P1P2)

By induction, P contains at least one α, therefore (P1P2) contains at least two αs, the claim holds.

#### 2.2 Definitions with Ellipses

• W = α | (βWWW)

… Or more precisely:

• W = α | (βY)
• Y = W | YW

Theorem 2.4: For any W, each β in W is preceded by an open parenthesis.

Exercise 2.2. Prove Theorem 2.4.

• Base case:

• Case α

α contains no β, the claim holds.

• Inductive case:

• Case (βW0W1Wn)

By induction, each β in W is preceded by an open parenthesis, therefore each β in the sequence of W is preceded by an open parenthesis. Also, the other β outside of the sequence of W is preceded by an open parenthesis, so that all the βs in this case is preceded by open parenthesises, the claim holds.

#### 2.3 Induction on Proof Trees

• α [always]
• △(P1P2) if △P1 and △P2

#### 2.4 Multiple Structures

Theorem 2.6: For all △P, P contains no βs.

Theorem 2.7: For all P, either 1) P contains a β, or 2) △P.

Exercise 2.3. Prove Theorem 2.7. The theorem must be proved over a different structure than Theorem 2.6.

Induction over the structure of P:

• Base case:

• Case α

α does not contain a β, and △α, the claim holds.

• Inductive cases:

• Case (βP)

There’s a β in this case, according to Theorem 2.6, △P does not hold, so the claim holds.

• Case (P1P2)

If at least one of P1 and P2 contains a β, at least one of △P1 and △P2 does not hold, so △P does not hold. Also, in this case, P contains at least one β. The claim holds.

If none of P1 and P2 contains a β, by induction, △P1 and △P1, so △P. Also, in this case, P does not contain a β, so the claim holds.

#### 2.5 More Definitions and More Proofs

• ((βα) ⊙ α) ⋄ (βα)
• (α ⊙ (βα)) ⋄ α
• (αα) ⋄ α
• (P1P2) ⋄ (P1′ ⊙ P2) if P1P1
• (P1P2) ⋄ (P1P2′) if P2P2
• V = α | (βV)

Theorem 2.9: Every V is in P.

Theorem 2.10: If △P and P is not a V , then PP′ for some P′.

Theorem 2.11: If △P and PP′, then △P′.

Exercise 2.4. Prove Theorem 2.9.

• Base case:

• Case α

a is in P, the claim holds.

• Inductive cases:

• Case (βV)

By induction, V is in P, so (βV) is in P, the claim holds.

Exercise 2.5. Prove Theorem 2.10.

First, we prove the following theorem:

Theorem: If △(P1P2), then (P1P2) ⋄ P′ for some P′.

Proof: By induction over the structure of (P1P2).

Since △(P1P2), △P1 and △P2.

• Base case:

• Case (αα)

(αα) ⋄ α, the claim holds.

• Inductive cases:

• Case ((P1P2) ⊙ P3)

By induction, (P1P2) ⋄ P′ for some P′, therefore ((P1P2) ⊙ P3) ⋄ (P′ ⊙ P3), the claim holds.

• Case (P3 ⊙ (P1P2))

Analogous to the previous case.

Now we prove theorem 2.10.

Induction over the structure of P:

• Base case:

• Case α

Since α is a V, the claim holds.

• Inductive cases:

• Case (βP)

Since △(βP) does not hold, the claim holds.

• Case (P1P2)

(P1P2) is not a V. If △(P1P2), by the theorem we just proved, △(P1P2) ⋄ P′ for some P′, the claim holds.

Exercise 2.6. Prove Theorem 2.11. The proof can proceed in two different ways, since the implicit “for all” applies to both △P and PP′.

Induction over the structure of PP′:

• Base cases:

• Case ((βα) ⊙ α) ⋄ (βα)

△((βα) ⊙ α) does not hold, the claim holds.

• Case (α ⊙ (βα)) ⋄ α

△(α ⊙ (βα)) does not hold, the claim holds.

• Case (αα) ⋄ α

△(αα), and △α, the claim holds.

• Inductive cases:

• Case (P1P2) ⋄ (P1′ ⊙ P2)

△(P1P2), therefore △P1 and △P2. Since P1P1′, by induction, △P1′, therefore △(P1′ ⊙ P2), the claim holds.

• Case (P1P2) ⋄ (P1P2′)

Analogous to the previous case.

### Chapter 3: Consistency of Evaluation

Theorem 3.2 [Church-Rosser for =r]: If M =r N, then there exists an expression L such that Mr L and Nr L.

Theorem 3.3 [Diamond Property forr]: If Lr M and Lr N, then there exists an expression L′ such that Mr L′ and Nr L′.

Theorem 3.5: For any B0, evalr(B0) = R0 for some R0.

Exercise 3.1. Prove Theorem 3.3 (formally, instead of using a diagram).

Lr ML =r MM =r L.

Lr NL =r N.

M =r L and L =r NM =r N.

Because M =r N, by theorem 3.2, there exists an expression L′ such that Mr L′ and Nr L′.

Exercise 3.2. Prove Theorem 3.5.

First, we prove this theorem:

Theorem: For any B0, B0 =r R0 for some R0.

• Base cases:

• Case `t`

`t` =r `t`, the claim holds.

• Case `f`

`f` =r `f`, the claim holds.

• Inductive case:

• Case (B1B2)

By induction, B1 =r R1 for some R1, and B2 =r R2 for some R2. So that (B1B2) =r (R1B2) =r (R1R2) for some R1 and R2.

If R1 = `t`, (B1B2) =r (`t`R2) =r `t`, the claim holds.

Otherwise, R1 = `f`, (B1B2) =r (`f`R2) =R2, the claim holds.

Now we prove Theorem 3.5:

Since B0 =r R0 for some R0, if R0 = `t`, evalr(B0) = `t`, the claim holds; otherwise R0 = `f`, evalr(B0) = `f`, the claim holds. So this theorem is proved.

### Chapter 4: The λ-Calculus

#### 4.2 λ-Calculus Grammar and Reductions

• M, N, L = X | (λX.M) | (M M)
• X = a variable: x, y, …
• ℱ𝒱(X) = {X}
• ℱ𝒱((λX.M)) = ℱ𝒱(M) \ {X}
• ℱ𝒱((M1 M2)) = ℱ𝒱(M1) ∪ ℱ𝒱(M2)
• X1[X1M] = M
• X2[X1M] = X2 where X1X2
• (λX1.M1)[X1M2] = (λX1.M1)
• (λX1.M1)[X2M2] = (λX3.M1[X1X3][X2M2]) where X1X2, X3 ∉ ℱ𝒱(M2) and X3 ∉ ℱ𝒱(M1) \ {X1}
• (M1 M2)[XM3] = (M1[XM3] M2[XM3])
• (λX1.M) α (λX2.M[X1X2]) where X2 ∉ ℱ𝒱(M)
• ((λX.M1) M2) β M1[XM2]
• (λX.(M X)) η M where X ∉ ℱ𝒱(M)
• n = αβη

Exercise 4.1. Reduce the following expressions with →n until no more →nβ reductions are possible. Show all steps.

• (λx.x)
• (λx.(λy.y x)) (λy.y) (λx.x x)
• (λx.(λy.y x)) ((λx.x x) (λx.x x))
• (λx.x)
• (λx.(λy.y x)) (λy.y) (λx.x x)
nβ (λy.y (λy.y)) (λx.x x)
nβ (λx.x x) (λy.y)
nβ (λy.y) (λy.y)
nβ (λy.y)
• (λx.(λy.y x)) ((λx.x x) (λx.x x))
nβ (λy.y ((λx.x x) (λx.x x)))
nβ (λy.y ((λx.x x) (λx.x x)))
nβ

Exercise 4.2. Prove the following equivalences by showing reductions.

• (λx.x) =n (λy.y)
• (λx.(λy.(λz.z z) y) x) (λx.x x) =n (λa.a ((λg.g) a)) (λb.b b)
• λy.(λx.λy.x) (y y) =n λa.λb.(a a)
• (λf.λg.λx.f x (g x)) (λx.λy.x) (λx.λy.x) =n λx.x
• Case (λx.x) =n (λy.y):
• (λx.x) →nα (λy.y)
• Case (λx.(λy.(λz.z z) y) x) (λx.x x) =n (λa.a ((λg.g) a)) (λb.b b):
• (λx.(λy.(λz.z z) y) x) (λx.x x)
nη (λy.(λz.z z) y) (λx.x x)
nβ (λy.y y) (λx.x x)
• (λa.a ((λg.g) a)) (λb.b b)
nβ (λa.a a) (λb.b b)
nα (λy.y y) (λb.b b)
nα (λy.y y) (λx.x x)
• So that (λx.(λy.(λz.z z) y) x) (λx.x x) =n (λa.a ((λg.g) a)) (λb.b b)
• Case λy.(λx.λy.x) (y y) =n λa.λb.(a a):
• λy.(λx.λy.x) (y y)
nα λa.(λx.λy.x) (a a)
nβ λa.λy.(a a)
nα λa.λb.(a a)
• Case (λf.λg.λx.f x (g x)) (λx.λy.x) (λx.λy.x) =n λx.x:
• (λf.λg.λx.f x (g x)) (λx.λy.x) (λx.λy.x)
nβ (λg.λx.(λx.λy.x) x (g x)) (λx.λy.x)
nβ (λg.λx.(λy.x) (g x)) (λx.λy.x)
nβ (λg.λx.x) (λx.λy.x)
nβ λx.x

#### 4.3 Encoding Booleans

• `true`λx.λy.x
• `false`λx.λy.y
• `if`λv.λt.λf.v t f

Exercise 4.3. Show that (`if` `true`) =n `true` and (`if` `false`) =n `false`.

(`if` `true`)
= ((λv.λt.λf.v t f) (λx.λy.x))
nβ (λt.λf.(λx.λy.x) t f)
nβ (λt.λf.(λy.t) f)
nβ (λt.λf.t)
nα (λx.λy.x)
= `true`

(`if` `false`)
= ((λv.λt.λf.v t f) (λx.λy.y))
nβ (λt.λf.(λx.λy.y) t f)
nβ (λt.λf.(λy.y) f)
nβ (λt.λf.f)
nα (λx.λf.f)
nα (λx.λy.y)
= `false`

#### 4.4 Encoding Pairs

… In other words, we need functions `mkpair`, `fst`, and `snd` that obey the following equations:

• `fst` (`mkpair` M N) =n M
• `snd` (`mkpair` M N) =n N
• M, N⟩ ≐ `λs`.`s` M N
• `mkpair`λx.λy.λs.s x y
• `fst`λp.p `true`
• `snd`λp.p `false`

Exercise 4.4. Define macros for binary `and` and `or` prefix operators that evaluate in the natural way with `true` and `false` (so that `and` `true` `false` =n `false`, etc.).

• `and`λx.λy `if` x y `false`
• `or`λx.λy `if` x `true` y

#### 4.4 Encoding Pairs

Exercise 4.5. Show that `mkpair`, `fst`, and `snd` obey the equations at the beginning of this section.

`fst` (`mkpair` M N)
= (λp.p `true`) ((λx.λy.λs.s x y) M N)
nβ ((λx.λy.λs.s x y) M N) `true`
nβ ((λy.λs.s M y) N) `true`
nβ (λs.s M N) `true`
nβ `true` M N
= (λx.λy.x) M N
nβ (λy.M) N
nβ M

`snd` (`mkpair` M N)
= (λp.p `false`) ((λx.λy.λs.s x y) M N)
nβ ((λx.λy.λs.s x y) M N) `false`
nβ ((λy.λs.s M y) N) `false`
nβ (λs.s M N) `false`
nβ `false` M N
= (λx.λy.y) M N
nβ (λy.y) N
nβ N

#### 4.5 Encoding Numbers

• 0 ≐ λf.λx.x
• 1 ≐ λf.λx.f x
• 2 ≐ λf.λx.f (f x)
• 3 ≐ λf.λx.f (f (f x))
• `add1`λn.λf.λx.f (n f x)
• `add`λn.λm.m `add1` n
• `iszero`λn.n (λx.`false`) `true`
• `wrap`λf.λp.⟨`false`, `if` (`fst` p) (`snd` p) (f (`snd` p))⟩
• `sub1`λn.λf.λx.`snd` (n (`wrap` f) ⟨`true`, x⟩)

Exercise 4.6. Show that `add1` 1 =n 2.

`add1` 1
= (λn.λf.λx.f (n f x)) (λf.λx.f x)
nβ λf.λx.f ((λf.λx.f x) f x)
nβ λf.λx.f ((λx.f x) x)
nβ λf.λx.f ((λx.f x) x)
nβ λf.λx.f (f x)
= 2

Exercise 4.7. Show that `iszero` 1 =n `false`.

`iszero` 1
= (λn.n (λx.`false`) `true`) (λf.λx.f x)
nβ (λf.λx.f x) (λx.`false`) `true`
nβ (λx.(λx.`false`) x) `true`
nβ (λx.`false`) `true`
nβ `false`

Exercise 4.8. Show that `sub1` 1 =n 0.

`sub1` 1
= (λn.λf.λx.`snd` (n (`wrap` f) ⟨`true`, x⟩)) (λf.λx.f x)
nβ λf.λx.`snd` ((λf.λx.f x) (`wrap` f) ⟨`true`, x⟩)
nβ λf.λx.`snd` ((λx.(`wrap` f) x) ⟨`true`, x⟩)
nβ λf.λx.`snd` ((`wrap` f) ⟨`true`, x⟩)
= λf.λx.`snd` (((λf.λp.⟨`false`, `if` (`fst` p) (`snd` p) (f (`snd` p))⟩) f) ⟨`true`, x⟩)
nβ λf.λx.`snd` ((λp.⟨`false`, `if` (`fst` p) (`snd` p) (f (`snd` p))⟩) ⟨`true`, x⟩)
nβ λf.λx.`snd` (⟨`false`, `if` (`fst``true`, x⟩) (`snd``true`, x⟩) (f (`snd``true`, x⟩))⟩)
n λf.λx.`snd``false`, `if` `true` (`snd``true`, x⟩) (f (`snd``true`, x⟩))⟩
n λf.λx.`snd``false`, (`snd``true`, x⟩)⟩
n λf.λx.`snd``false`, x
n λf.λx.x
= 0

Exercise 4.9. Define `mult` using the technique that allowed us to define `add`. In other words, implement (`mult` n m) as n additions of m to 0 by exploiting the fact that n itself applies a function n times. Hint: what kind of value is (`add` m)?

`mult`λn.λm.λf.m (n f)

Exercise 4.10. The λ-calculus provides no mechanism for signalling an error. What happens when `sub1` is applied to 0? What happens when `iszero` is applied to `true`?

Let’s try:

`sub1` 0
= (λn.λf.λx.`snd` (n (`wrap` f) ⟨`true`, x⟩)) (λf.λx.x)
nβ λf.λx.`snd` ((λf.λx.x) (`wrap` f) ⟨`true`, x⟩)
nβ λf.λx.`snd` ((λx.x) ⟨`true`, x⟩)
nβ λf.λx.`snd``true`, x
n λf.λx.x
= 0

`iszero` `true`
= (λn.n (λx.`false`)) (λx.λy.x)
nβ (λx.λy.x) (λx.`false`)
nβ λy.λx.`false`

I think that’s it.

#### 4.6 Recursion

##### 4.6.1 Recursion via Self-Application

Exercise 4.11. Define a macro `mksum` such that (`mksum` `mksum`) acts like a “sum” function by consuming a number n and adding all the numbers from 0 to n.

`mksum`λt.λn `if` (`iszero` n) 0 (`add` ((t t) (`sub1` n)) n)

##### 4.6.3 Fixed Points and the `Y` Combinator

`Y`λf.(λx.f (x x)) (λx.f (x x))

Exercise 4.12. Prove that M (`Y` M) =n (`Y` M) for any M.

(`Y` M)
= ((λf.(λx.f (x x)) (λx.f (x x))) M)
nβ (λx.M (x x)) (λx.M (x x))
nβ (M ((λx.M (x x)) (λx.M (x x))))

M (`Y` M)
= M ((λf.(λx.f (x x)) (λx.f (x x))) M)
nβ (M ((λx.M (x x)) (λx.M (x x))))

The claim holds.

Exercise 4.13. Define an encoding for Lisp cons cells, consisting of the following macros:

• `null`, a constant
• `cons`, a function that takes two arguments and returns a cons cell
• `isnull`, a function that returns `true` if its argument is `null`, `false` if it is a cons cell
• `car`, a function that takes a cons cell and returns its first element
• `cdr`, a function that takes a cons cell and returns its second element

In particular, your encoding must satisfy the following equations:

• (`isnull` `null`) =n `true`
• (`isnull` (`cons` M N)) =n `false`
• (`car` (`cons` M N)) =n M
• (`cdr` (`cons` M N)) =n N

Your encoding need not assign any particular meaning to expressions such as (`car` `null`) or (`car` `cons`).

• `null` ≐ ⟨`true`, `false`
• `cons`λM.λN`false`, ⟨M, N⟩⟩
• `isnull`λM.`fst` M
• `car`λM.`fst` (`snd` M)
• `cdr`λM.`snd` (`snd` M)

Exercise 4.14. Using your encoding from the previous exercise, define `length`, which takes a list of booleans and returns the number of cons cells in the list. A list of booleans is either `null`, or (`cons` b l) where b is `true` or `false` and l is a list of booleans.

`length``Y` (λf.λM.`if` (`isnull` M) 0 (`add1` (f (`cdr` M))))

Why does the question say “a list of booleans”? I think `length` can be applied to a list of anything.

#### 4.7 Facts About the λ-Calculus

Exercise 4.15. Prove that ((λx.x x) (λx.x x)) has no normal form.

We can only apply β reduction to ((λx.x x) (λx.x x)) using normal order reduction:

((λx.x x) (λx.x x)) β ((λx.x x) (λx.x x))

So, after the only reduction we can do, we get the original expression. This leads to a infinite loop, so we can’t reach a normal form expression, therefore ((λx.x x) (λx.x x)) has no normal form.

## Part II: Models of Realistic Languages

### Chapter 5: ISWIM

#### 5.1 ISWIM Expressions

• M, N, L, K = X | (λX.M) | (M M) | b | (on MM)
• X = a variable: x, y, …
• b = a basic constant
• on = an n-ary primitive operation
• b = {⌈n⌉ | n ∈ ℤ}
• o1 = {`add1`, `sub1`, `iszero`}
• o2 = {+, −, ∗, ↑}

#### 5.2 ISWIM Reductions

Exercise 5.1. Show a reduction of
(λw.(− (w ⌈1⌉) ⌈5⌉)) ((λx.x ⌈10⌉) λyz.(+ z y))
to a value with →v.

(λw.(− (w ⌈1⌉) ⌈5⌉)) ((λx.x ⌈10⌉) λyz.(+ z y))
v (λw.(− (w ⌈1⌉) ⌈5⌉)) (λyz.(+ z y) ⌈10⌉)
v (λw.(− (w ⌈1⌉) ⌈5⌉)) (λz.(+ z ⌈10⌉))
v (− ((λz.(+ z ⌈10⌉)) ⌈1⌉) ⌈5⌉)
v (− (+ ⌈1⌉ ⌈10⌉) ⌈5⌉)
v (− ⌈11⌉ ⌈5⌉)
v ⌈6⌉

#### 5.4 Evaluation

Exercise 5.2. Suppose that we try to strengthen the evaluation function as follows:

• eval1(M) = b if M =v b
• eval1(M) = `function1` if M =v λX.N and NλY.N′ for any Y, N
• eval1(M) = `function+` if M =v λX.λY.N

Is eval1 a function? If so, prove it. If not, provide a counter-example.

No, eval1 is not a function:

• λx.(λy.y) (λz.z) =v λx.(λy.y) (λz.z)
• λx.(λy.y) (λz.z) =v λx.λz.z

So eval1(λx.(λy.y) (λz.z)) = `function1`, and eval1(λx.(λy.y) (λz.z)) = `function+`. Therefore eval1 is not a function.

#### 5.5 Consistency

Theorem 5.5 [Diamond Property forv ]: If Lv M and Lv N, then there exists an expression K such that Mv K and Nv K.

Theorem 5.6 [Diamond Property forv]: If Lv M and Lv N, then there exists an expression K such that Mv K and Nv K.

• Mv N if M =α N
• (on b1bn) ↪v δ(on, b1, … bn) if δ(on, b1, … bn) is defined
• ((λX.M) N) ↪v M′[XV ] if Mv M′ and Nv V
• (M N) ↪v (MN′) if Mv M′ and Nv N
• (λX.M) ↪v (λX.M′) if Mv M′ (Different than the manuscript, I think the manuscript is wrong.)
• (on M1Mn) ↪v (on M1′ … Mn′) if Miv Mi′ , i ∈ [1, n]

Exercise 5.3. Prove that if Nv N′, then M[XN] ↪v M[XN′].

Induction over the structure of M:

• Base cases

• Case X:

If M = X, M[XN] = N, and M[XN′] = N′, therefore M[XN] ↪v M[XN′]. Otherwise M[XN] = M, and M[XN′] = M, therefore M[XN] ↪v M[XN′]. The claim holds.

• Case b:

b[XN] = b, b[XN′] = b, therefore b[XN] ↪v b[XN′], the claim holds.

• Inductive cases:

• Case (λX′.M):

If X′ = X, (λX′.M)[XN] = (λX′.M), (λX′.M)[XN′] = (λX′.M), the claim holds.

Otherwise, (λX′.M)[XN] = (λX′.M[XN]), (λX′.M)[XN′] = (λX′.M[XN′]). By induction, M[XN] ↪v M[XN′], therefore (λX′.M[XN]) ↪v (λX′.M[XN′]), the claim holds.

• Case (M1 M2):

(M1 M2)[XN] = (M1[XN] M2[XN]), (M1 M2)[XN′] = (M1[XN′] M2[XN′]). By induction, M1[XN] ↪v M1[XN′], M2[XN] ↪v M2[XN′], therefore (M1 M2)[XN] ↪v (M1 M2)[XN′], the claim holds.

• Case (on MM):

Analogous to the previous case.

Exercise 5.4. Prove that if X ∉ ℱ𝒱(L) then K[XL][X′ ← M[XL]] =α K[X′ ← M][XL]

TODO.

Exercise 5.5. Prove that the transitive–reflexive closure of the parallel reduction ↪v is the same as ↠v. This fact, along with Theorem 5.6, supports the proof of Theorem 5.5.

TODO.

#### 5.6 Observational Equivalence

Exercise 5.6. Consider the following evaluation function eval0, plus its associated observational equivalence relation ≃0:

• eval0(M) = `value` if M =v V for some V
• M0 N if eval0(C[M]) = eval0(C[N]) for all C