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
  • (B1 • B2) ∈ 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. •
  3. ((f • t) • (f • f))
  4. ((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
  • B1 ≍r B1
  • (f • B1) ≈r B1
  • (t • B1) ≈r t
  • B1 ≈r B1
  • B1 ≈r B2 ⇒ B2 ≈r B1
  • B1 ≈r B2 and B2 ≈r B3 ⇒ B1 ≈r B3

1.4 Directed Evaluation

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

  • B1 ↝↝r B1
  • B1 r B2 ⇒ B1 ↝↝r B2
  • B1 ↝↝r B2 and B2 ↝↝r B3 ⇒ B1 ↝↝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 B2 ⇒ B1 →r B2
  • B1 →r B1′ ⇒ (B1 • B2) →r (B1′ • B2)
  • B2 →r B2′ ⇒ (B1 • B2) →r (B1 • B2′)

↠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) | (P ⊙ P)

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

Exercise 2.1. Prove Theorem 2.2.

2.2 Definitions with Ellipses

  • W = α | (βWW…W)

… 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.

2.3 Induction on Proof Trees

  • △α [always]
  • △(P1 ⊙ P2) 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:

2.5 More Definitions and More Proofs

  • ((β ⊗ α) ⊙ α) ⋄ (β ⊗ α)
  • (α ⊙ (β ⊗ α)) ⋄ α
  • (α ⊙ α) ⋄ α
  • (P1 ⊙ P2) ⋄ (P1′ ⊙ P2) if P1 ⋄ P1′
  • (P1 ⊙ P2) ⋄ (P1 ⊙ P2′) if P2 ⋄ P2′
  • V = α | (β ⊗ V)

Theorem 2.9: Every V is in P.

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

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

Exercise 2.4. Prove Theorem 2.9.

Exercise 2.5. Prove Theorem 2.10.

First, we prove the following theorem:

Theorem: If △(P1 ⊙ P2), then (P1 ⊙ P2) ⋄ P′ for some P′.

Proof: By induction over the structure of (P1 ⊙ P2).

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

Now we prove theorem 2.10.

Induction over the structure of P:

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 P ⋄ P′.

Induction over the structure of P ⋄ P′:

Chapter 3: Consistency of Evaluation

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

Theorem 3.3 [Diamond Property for ↠r]: If L ↠r M and L ↠r N, then there exists an expression L′ such that M ↠r L′ and N ↠r 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).

L ↠r M ⇒ L =r M ⇒ M =r L.

L ↠r N ⇒ L =r N.

M =r L and L =r N ⇒ M =r N.

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

Exercise 3.2. Prove Theorem 3.5.

First, we prove this theorem:

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

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[X1 ← M] = M
  • X2[X1 ← M] = X2 where X1 ≠ X2
  • (λX1.M1)[X1 ← M2] = (λX1.M1)
  • (λX1.M1)[X2 ← M2] = (λX3.M1[X1 ← X3][X2 ← M2]) where X1 ≠ X2, X3 ∉ ℱ𝒱(M2) and X3 ∉ ℱ𝒱(M1) \ {X1}
  • (M1 M2)[X ← M3] = (M1[X ← M3] M2[X ← M3])
  • (λX1.M) α (λX2.M[X1 ← X2]) where X2 ∉ ℱ𝒱(M)
  • ((λX.M1) M2) β M1[X ← M2]
  • (λ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))

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

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.).

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).

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 M … M)
  • 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:

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 for ↠v ]: If L ↠v M and L ↠v N, then there exists an expression K such that M ↠v K and N ↠v K.

Theorem 5.6 [Diamond Property for ↪v]: If L ↪v M and L ↪v N, then there exists an expression K such that M ↪v K and N ↪v K.

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

Exercise 5.3. Prove that if N ↪v N′, then M[X ← N] ↪v M[X ← N′].

Induction over the structure of M:

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

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
  • M ≃0 N if eval0(C[M]) = eval0(C[N]) for all C

Does M ≃0 N imply anything about M ≃v N? Sketch an argument for your answer.

TODO.