2.  [3 points] A closed term (expression) is a term that has no free variables.  Evaluation of MinML preserves the closure property on terms.  In other words, if you start with a closed term and evaluate for any number of steps, the result will also be a closed term.   Define a judgement (and collection of interference rules for it) that determines when a term is closed.

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

4.  [3 points] 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.  [3 points] The Curry-Howard Isomorphism suggests that the typed lambda calculus (with functions and pairs, for instance) can be thought of as a logic instead of a programming language (intuitionistic propositional logic to be precise).  Suppose you add recursive functions, like those found in MinML, to the typed lambda calculus.  Will the result still serve as a useful logic?  Explain your answer.  Hint: think about the various components of the isomorphism (programs = proofs, types = theorems, inhabited types = true theorems, ...).  Which one is useful answering this question? 

6. [3 points] 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

7.  [10 points] 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:

Compiler.Control.Print.printDepth := 100;
Compiler.Control.Print.printLength := 100;