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

  • tB
  • fB
  • (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. ((ft) • (ff))
  3. ((f) • (t))

t is in B:

t ∈ B

((ft) • (ff)) 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

  • (fB1) r B1
  • (tB1) r t
  • (fB1) ≍r B1
  • (tB1) ≍r t
  • B1r B1
  • (fB1) ≈r B1
  • (tB1) ≈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 • (ff))) ↝↝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 • ((tf) • 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 ((tf) • f).

Exercise 1.4. Show that (f • ((tf) • 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.

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.

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:

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.

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.

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 PP′.

Induction over the structure of PP′:

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.

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

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 (fsttrue, x⟩) (sndtrue, x⟩) (f (sndtrue, x⟩))⟩)
n λf.λx.sndfalse, if true (sndtrue, x⟩) (f (sndtrue, x⟩))⟩
n λf.λx.sndfalse, (sndtrue, x⟩)⟩
n λf.λx.sndfalse, 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.sndtrue, 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.

lengthY (λ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:

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:

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


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.


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

Does M0 N imply anything about Mv N? Sketch an argument for your answer.