Not every problem set will be graded. Problem sets that are graded
should be submitted electronically --
using
gsubmit
.
- Problem Set 01: Posted Sept 8. Not graded, not submitted.
- Problem Set 02: Posted Sept 15. Graded, due Sept 22, no later than 11:59 pm.
- Problem Set 03: Posted Sept 22. Not graded, not submitted.
- Problem Set 04: Posted Sept 29. Graded, due Oct 6, no later than 11:59 pm.
- Problem Set 05: Posted Oct 6. Not graded, not submitted.
- Problem Set 06: Posted Oct 13. Graded, due Oct 20, no later than 11:59 pm.
- Problem Set 07: Posted Nov 3. Graded, due Nov 10, no later than 11:59 pm.
- Problem Set 08: Posted Nov 14. Not graded, not submitted.
- Problem Set 09: Posted Nov 21. Graded, due Dec 5, no later than 11:59 pm.
- Problem Set 10: Posted Dec 6. Not graded, not submitted.
Every implementation assignment will be graded, and
should be submitted electronically --
using
gsubmit
.
- Implementation 1: Assignment (pdf file), Implementation notes (tar.gz file),
Posted Sept 12, due Sept 26.
- Implementation 2: Assignment (pdf file), Implementation notes (tar.gz file),
Posted Sept 26, due Oct 17.
- Implementation 3: Assignment (pdf file), Implementation notes (tar.gz file),
Posted Oct 17, due Nov 9.
- Implementation 4: Assignment (pdf file), Implementation notes (tar.gz file),
Posted Nov 10, due Dec 1.
Problem 1. Exercise 3.5.10, page 39, in [Pierce].
Problem 2. Exercise 3.5.13, page
40, in [Pierce]. Give a counter-example for each theorem that fails
because
of the added rule.
Problem 3. Exercise 3.5.17, page
42, in [Pierce].
Problem 4. Exercise 3.5.18, page 43, in [Pierce]. Do this for the small-step semantics given in Figure 3-2, page 41.
Problem 1. Exercise 5.2.5, page 62, in [Pierce]. Check the definition, by carrying out the evaluation of subtracting one Church numeral from another Church numeral.
Problem 2. Exercise 5.3.6, page
72, in [Pierce].
Problem 3. Exercise 5.3.8, page
73, in [Pierce].
Problem 4. Consider the normal-order evaluation strategy, as in Exercise 5.3.6 and earlier in Chapter 5. Show how to formulate the normal-order evaluation rules for lambda-terms in the big-step style.
Problem 1. Exercise 8.3.5, page 98, in [Pierce].
Problem 2. Exercise 8.3.6, page
98, in [Pierce].
Problem 3. Exercise 8.3.8, page
98, in [Pierce].
Problem 4. Exercise 9.2.2, page
103 in [Pierce].
Problem 5. Exercise 9.2.3, page
103 in [Pierce].
Problem 1. Exercise 11.3.2, page 121, in [Pierce]. Warning: In some editions of [Pierce], there is an error in the solution given at the end of the book.
Problem 2. Exercise 11.5.2, page
125, in [Pierce].
Problem 3. Exercise 11.9.1, page
134, in [Pierce].
Problem 4. Exercise 11.11.1, page
144, in [Pierce].
Problem 5. Consider Figure 11-13
on page 147 in [Pierce]. In the evaluation rules (E-IsNilNil), (IsNilCons)
(E-HeadCons), and (E-TailCons), the types S and T do not have to be the
same. (1) Explain clearly why this does not break the soundness of the type
system. (2) Suppose we change "S" to "T" in the same evaluation rules.
Does anything go wrong now? If yes, give a little example. If no, justify
clearly.
Problem 1. Exercise 12.1.1, page 150, in [Pierce].
Problem 2. Consider the terms of the pure lambda-calculus, i.e. this is the lambda-calculus consisting of variables, abstractions, and applications only. Show that if a term t of the pure lambda-calculus is such that every binding occurrence of a variable x binds at most one bound occurrence of x, then t is normalizable -- regardless of the evaluation strategy.
Problem 3. Exercise on page 23 of Handout 09, "Extensions of the Simply-Typed Lambda-Calculus (Continued)".
Problem 4. Exercise 13.1.2, page 158, in [Pierce].
Problem 5. Exercise 13.1.3, page 158, in [Pierce].
Problem 1. Exercise 13.4.1, page 164, in [Pierce].
Problem 2. Exercise 13.5.2, page 167, in [Pierce].
Problem 3. Exercise 14.1.1, page 173, in [Pierce].
Problem 4. Exercise on page 23 of Handout 09, "Extensions of the Simply-Typed Lambda-Calculus (Continued)". (This exercise is assigned for a second time, it was already given as Problem 3 in the preceding problem set.)
Proposed solution for Problem 4 in Problem Set 06.Problem 1. Prove Lemma 0.2 in Handout 14. Caution: Make sure you have the most recent version of Handout 14. Hint: As stated, the lemma is restricted to closed terms. If you want to carry out the proof by induction on the structure of terms, you cannot restrict the induction to closed terms. Instead, generalize the statement of Lemma 0.2 so that it also applies to open terms -- in the style of Lemma 0.1 in Handout 16 -- and then prove this more general statement by induction on the structure of terms.
Problem 2. Do Exercise 0.3 in Handout 15. Caution: Make sure you have the most recent version of Handout 15.
Problem 3. Consider the treatment of exceptions in Handout 16. (Ignore references and side-effects in Handout 16.) These are exceptions that carry values, like the exceptions considered in [Pierce, Section 14.3]. But the syntax and semantics of exceptions in Handout 16 and in [Pierce, Section 14.3] are different. Compare both approaches of exceptions. Specifically, is one more general than the other, i.e., can an exception according to one approach be modelled (or simulated) by an exception according to the other? Justify your answer carefully.
If you cannot solve this problem in full generality, at least provide 2 or 3 small excerpts of codes using exceptions in the language of one approach, and show how these excerpts can be translated into equivalent codes in the language of the other approach.
Proposed solutions for Problem Set 07.Problem 1. Exercise 1 in Handout 21, page 6.
Problem 2. Exercise 2 in Handout 21, page 6.
Problem 3. Exercise 3 in Handout 21, page 6.
Problem 4. Exercise 4 in Handout 21, page 6.
Problem 1. Exercise 23.4.3, page 346 in [Pierce].
Problem 2. Exercise 23.4.8, page 349 in [Pierce].
Problem 3. Exercise 15.2.3, page 186 in [Pierce].
Problem 4. Last exercise in Handout 22, at the bottom of page 5.
Proposed solutions for Problem Set 09 by Michel Machado.
Problem 1. Exercise 20.1.2, page 271 in [Pierce].
Problem 2. Part 1: Answer the 3 questions on the last page (page 4) of Handout 27. Part 2: Give two recursive types, call them T1 and T2, which are not congruent according to the congruence relation defined in Part 1 but whose "infinite unwindings" produce the same infinite type.
Problem 3. Prove the first FACT in the last page (page 3) of Handout 28.
Problem 4. Show that not every term of the pure lambda-calculus is typable in the system of positive recursive types. (If this were not the case, the second FACT in the last page (page 3) of Handout 28 would be false -- why?) Hint: Consider the term x x, i.e., the self application of x.