Each problem set consists of hand-exercises and/or an implementation in SML. The two parts should be submitted separately, and each submitted electronically as an attachment, to an e-mail address (to be supplied each time) -- do not use gsubmit. In the e-mail message with your SML implementation, indicate how to load and run it.
- Problem Set 01, Posted Sept 10, hand exercises due Sept 17, implementation due Sept 24.
- Problem Set 02, Posted Sept 17, due Sept 24.
- Problem Set 03, Posted Sept 24, hand exercises due Oct 1, implementation due Oct 8.
- Problem Set 04, Posted Oct 1, due Oct 8.
- Problem Set 05, Posted Oct 9, hand exercises due Oct 15, implementation due Nov 1.
- Problem Set 06, Posted Oct 15, due Oct 22.
- Problem Set 07, Posted Oct 22, due Nov 1.
- Problem Set 08, Posted Nov 5, due Nov 15.
- Problem Set 09, Posted Nov 12, due Nov 22.
- Problem Set 10, Posted Nov 19, due Dec 1.
- Problem Set 11, Posted Dec 3, due Dec 13.
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.18, page 43, in [Pierce]. Do this for the small-step semantics given in Figure 3-2, page 41.
SML implementation
(due September 24, submitted
electronically
to Assaf Kfoury kfoury@cs.bu.edu):
An implementation for the language of arithmetical expressions (as defined in Chapter 3) is presented in Chapter 4. The implementation consists of several parts that carry out a syntactic analysis of an arithmetical expression, given as input, and then evaluates it (according to the small-operational semantics of Section 3.5). The code of this implementation can be downloaded from here, and it is written in OCaml, a variant of SML. You need to download the gzipped tarred file "arith.tar.gz", then gunzip it to obtain "arith.tar", and then extract the contents of the latter. We want you to re-write part of this implementation into SML, according to the following:
Solutions for Problem Set 01: tex file, ps file.
Problem 1. In Figure 5-3 in [Pierce], variables are not values. This means that the term t = ((lambda x.x) y) is in normal form according to call-by-value evaluation. For brevity, we say t is in cbv-normal form. Suppose we adjust the call-by-value semantics of Figure 5-3 to now include variables among values, so that t can be further reduced to y. We refer to this adjusted call-by-value by call-by-value'. Accordingly, we can say t is not in cbv'-normal form. Note that a term in cbv'-normal form is also in cbv-normal form, but not the other way around. Consider arbitrary terms u, u1 and u2 such that:
(This means that, as far as closed terms are concerned, cbv and cbv' produce exactly the same results.)
Problem 2. Exercise 5.2.8, page 63, in [Pierce].
Problem 3. Exercise 5.2.10, page 66, in [Pierce].
Problem 4. Exercise 5.3.6, page 72, in [Pierce]. Do it for full beta-reduction and normal-order only, omit lazy evaluation.
Problem 5. Exercise 5.3.7, page 73, in [Pierce].
Solutions for Problem Set 02: tex file, ps file.
Problem 1. Download ps file.
Problem 2. Download ps file.
Click here to download the LaTeX source file, if you want to see how Problems 1 and 2 are typeset, although you will not be able to compile the file (because of many missing customized LaTeX commands).
Problem 3. Exercise 8.3.6, page 98, in [Pierce].
Problem 4. Exercise 9.2.3, page 103, in [Pierce].
Problem 5. Exercise 9.3.2, page 104, in [Pierce].
Implementation (in any language of your choice)
(due October 8, submitted
electronically
to Assaf Kfoury kfoury@cs.bu.edu):
Implement the (untyped) pure lambda-calculus. Your implementation should consist of both a syntactic analysis and a semantic evaluation based on Figure 5-3 in [Pierce, page 72]. You may wish to consult Pierce's implementation, which is available from here, but be advised that Pierce uses de Bruijn indices as presented in [Pierce, Chapter 6]. If you decide to consult Pierce's implementation, you need to download the gzipped tarred file "untyped.tar.gz".
We want your implementation to avoid the use of de Bruijn indices completely.
You should submit a gzipped tarred file of a directory containing your implementation. Include a README file that explains how to run and test your code, and also describes the design of your implementation:
Solutions for Problem Set 03: tex file, ps file.
Problem 1. Download ps file.
Problem 2. Download ps file.
Problem 3. Part (1): Exercise 11.3.2, page 121, in [Pierce]. Part (2): Exercise 11.5.2, page 125, in [Pierce].
Problem 4. Exercise 11.9.1, page 134, in [Pierce].
Problem 5. Exercise 11.12.1, page 146, in [Pierce].
Solutions for Problem Set 04: tex file, ps file.
Problem 1. Exercise 13.1.3, page 158, in [Pierce].
Problem 2. Exercise 13.5.2, page 167, in [Pierce].
Problem 3. Part (1): Exercise 13.5.8, page 169, in [Pierce]. Part (2): Consider how the function fact is defined in [Pierce, page 516]. Carry out the evaluation of (fact 3) carefully, step by step.
Problem 4. For this exercise you have to use the SML-like programming language in [Pierce]. Suppose the language includes references (as presented in [Pierce, Chapter 13]), recursive definitions (as presented in [Pierce, Section 11.11]), and booleans and natural numbers with their respective primops. Write a short program with two reference variables x and y of type Ref Nat that halts iffx andy are aliases of each other. It is not necessary to preserve the initial contents of the locations referenced by xand y.
Implementation (in any language of your choice)
(due Monday, November 1, submitted
electronically to Assaf Kfoury kfoury@cs.bu.edu):
Implement the simply-typed lambda-calculus, as presented in [Pierce, Chapter 9], augmented with booleans and natural numbers with their primops [Pierce, Chapter 8]. Your implementation should consist of both a syntactic analysis and a semantic evaluation. Note that the syntactic analysis should now type-check terms given as input expressions.
Once more, we want your implementation to avoid the use of de Bruijn indices completely.
You should submit a gzipped tarred file of a directory containing
your
implementation. Include a README file that explains how to run and test
your code, and also describes the design of your implementation. An
explanation
in the e-mail message of your message is not
a substitute for the README file.
You should run and test your code on the provided input file (click
here
to download).
Solutions for Problem Set 05: tex file, ps file.
Problem 1. Exercise 15.2.3 in [Pierce, page 186].
Problem 2. Exercise 15.2.5 in [Pierce, page 187].
Problem 3. Exercise 15.3.2 in [Pierce, page 188]. Do part (1) only.
Problem 4. Exercise 15.5.2 in [Pierce, page 198].
Problem 5. Consider the term t = (lambda x. x x). Is t typable in the simply-typed lambda-calculus with subtyping [Pierce, Figure 15-1, page 186]? I.e., are there types T1 and T2 such that we can construct a typing derivation for the judgement (lambda x:T1 . x x) : T2 ? If yes, provide instances of T1 and T2 that will justify your answer. If no, explain your answer carefully.
Solutions for Problem Set 06: tex file, ps file.
Problem 1. Prove carefully and in detail part (1) of Lemma 16.1.2 in [Pierce, page 211]. (The solution in the back of the book says only that the proof is "a straightforward induction on the structure of S". This is not enough.)
Problem 2. Exercise 16.1.3 in [Pierce, page 211]. Consider also the case when we add the base types Nat and Char, in addition to Bool, which satisfy the following relations: Bool <: Nat and Char <: Nat.
Problem 3. Exercise 16.2.3 in [Pierce, page 217].
Problem 4. Download ps file.
Hand exercises -- optional (if you choose not to complete implementation #3):
Problem 5. Complete the pseudo-implementation on page 8 of Handout 15, to include the cases for records (corresponding to the last two rules on page 6 of Handout 15).
Problem 6. Consider the solution of Exercise 16.3.2 in [Pierce, page 219]. The solution is on page 522. Suppose we add the base types Bool, Char and Nat, such that: Bool <: Nat and Char <: Nat. Part 1: Adjust accordingly the definitions of the "join" and "meet" operations, as given on page 522. Part 2: List the changes that have to be made, if any, in the proofs of A.10 (page 523) A.11 (page 523) and A.12 (page 524) after the addition of Bool, Char and Nat.
Solutions for Problem Set 07: tex file, ps file.
Problem 1. Exercise 18.3.1 in [Pierce, page 245]. We will give you full credit if you produce a (correct!) solution different from Pierce's.
Problem 2. Part (1): Exercise in [Handout 18, page 4]. Part (2): Exercise in [Handout 18, page 5]. Part (3): Exercise in [Handout 18, page 6].
Problem 3. Part (1): Exercise in [Handout 19, page 7]. Part (2): Extend the pseudo-implementation in [Handout 19, page 8] to include the rules missing in [Handout 19, page 7].
Problem 4. Exercise 22.3.11 in [Pierce, page 326]. We want you to do this exercise in details and in conformity with the notation and approach of Handout 19, which are somewhat different from those of [Pierce, Chapter 22]. The solution proposed by Pierce in [Pierce, page 543] is sketchy and contains a typographical error; although it formulates the rule (CT-Fix), but not in the style of Handout 19, it does not say how to extend the algorithm to generate constraints in [Handout 19, page 8].
Problem 5. Use the algorithm in [Handout 19, page 8], properly extended according to Problem 3 above, to generate the constraint set C for the expression:
(lambda f:A. lambda x:B. f (f x)) (lambda y:C. succ y)
Use the algorithm in [Handout 19, page 12] to determine whether constraint set C has a solution. And if it has a solution, give the resulting principal type for the expression.
Problem 6. Use the algorithm in [Handout 19, page 8] to generate the constraint set C for the expression:
(lambda f:A. lambda x:B. f (f x)) (lambda y:C. lambda z:D. y)
Use the algorithm in [Handout 19, page 12] to determine whether constraint set C has a solution. And if it has a solution, give the resulting principal type for the expression.
Solutions for Problem Set 08: tex file, ps file.
Problem 1. First exercise in [Handout 20, page 7].
Problem 2. Second exercise in [Handout 20, page 7].
Problem 3. First exercise in [Handout 21, page 5]. Assume there are rules, without premises, which derive succ : Nat -> Nat and 3 : Nat.
Problem 4. Second exercise in [Handout 21, page 5]. Use the same assumption as in Problem 3.
Problem 5. Third exercise in [Handout 21, page 5]. Use the same assumption as in Problem 3.
Problem 6. Fourth exercise in [Handout 21, page 5].
Problem 7. Based on the constraint typing rules in [Handout 21, page 7], implement an algorithm (i.e., write its pseudo-code) that computes the function constraints as defined in [Handout 21, page 9]. State carefully how you specify the initial context (i.e., the first argument of the function constraints). Consider carefully how you handle a lambda-binding for a variable named x whose scope contains another lambda-binding for a variable also named x. Hint: Consider the implementation in [Handout 19, page 8].
Solutions for Problem Set 09: tex file, ps file.
Problem 1. First exercise in [Handout 22, page 6].
Problem 2. Second exercise in [Handout 22, page 6].
Problem 3. Third exercise in [Handout 22, page 6].
Problem 4. Fourth exercise in [Handout 22, page 6].
Problem 5. First exercise in [Handout 23, page 5].
Problem 6. Second exercise in [Handout 23, page 5].
Solutions for Problem Set 10: tex file, ps file.
This problem set will be in two parts, the first posted on December 3 and the second posted on December 6. Both parts are due on December 13.
The first part has 4 problems. Download the files here (tex, ps).
The second part has 2 problems. Download the files here (tex, ps).
Solutions for Problem Set 11: tex file, ps file.