Rules for collaboration: You may discuss the problem sets with other students to increase your understanding of the material. However, what you write down and turn in should be your own work.

All problem sets are due at 11:00 a.m. in class on the due date.

Print out your programs (and, where specified, transcripts of their execution) onto paper, and turn in the paper.

1.  Read Pierce, chapter 1, 8.

2.  NOT REQUIRED.  YOU DO NOT HAVE TO HAND IN ANSWERS TO THIS QUESTION.  (But it is still recommended as a good exercise.)  A closed term is a term that has no free variables.  Does the evaluation of the lambda calculus preserves the closure property on terms?  In other words, if you start with a closed term and evaluate for any number of steps, will the result be another closed term?   State this question more formally as a mathematical conjecture.  Then either prove it correct or disprove it by giving a counterexample.

3.  Conjecture:  In MinML, if G |- e : t and e' --> e then G |- e' : t.  Prove it or give a counterexample.

4.  Conjecture:  For any MinML expression e and any type t1 there is at most one type t2  such that (fun f(x:t1):t2 = e) is well typed.  Prove it or give a counter example.

5. Express the abstract syntax of MinML using a first-order representation strategy (as opposed to a higher-order representation strategy, like you did last week).  Variables should be implemented using ML strings. Numbers can be implemented as ML integers.

Relevant MinML Syntax:

t ::= int | bool | t1 --> t2

op ::= + | - | * | < | = | /\ | \/

n ::= ... | -2 | -1 | 0 | 1 | 2 | ...

b ::= true | false

e ::= x | n | b | if e then e else e | fix f(x : t) : t = e | e e | e op e

6.  Implement capture-avoiding substitution for this representation.  As well as handing in the code for your implementation, hand in a number of tests to demonstrate that (a) you understand where the "corner cases" in the implementation arise and (b) that you have implemented these corner cases correctly.  Efficiency should not be a concern in your implementation.  Clarity and elegance of your code are important.

SML/NJ note: To have the interactive-system pretty-printer show expressions to greater depth (and lists to greater length) than is the default, you can execute these commands: