This assignment has 25 points.

1. Read Pierce, chapter 1,
8. 2. [3 points] A 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 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.
Compiler.Control.Print.printDepth := 100; Compiler.Control.Print.printLength := 100; |