Programming Languages, Fall 2013 HW7 - Simple Types and Simply-Typed Lambda Calculus Due electronically on Blackboard on Monday November 4, 11:59pm. Problems 1--7 concern the arithmetic expressions language on slide 5. 1. Draw the derivation tree of the typing derivation: if true then 0 else succ (pred 0) : Nat 2. Complete the full proof of the progress theorem on slide 25. 3. Complete the full proof of the preservation theorem on slide 30. 4. Redo this preservation theorem proof using induction on t->t'. 5. Draw the derivation tree for the three typing derivations on slide 45. 6. (inverse of preservation theorem) Is it always the case that, if t->t' and t':T, then t:T? If so, prove it. If not, give a counterexample. 7. Reformulate type safety theorem(s) using big-step semantics. Problems 8--10 concern the "pair language" in the Midterm. 8. Formalize the typing rules. You may use P(T1, T2) for the type of pair. 9. Prove the progress and preservation theorems. 10. Implement (based on your work in HW6) in Haskell: a) a recursive type-checking function: given a term, returns a type, or raise "untypable". Note you have to define type first. b) show a few examples of type preservation Problems 11-12 concern the simply-typed lambda-calculus. 11. Complete the full proof of the progress theorem on slide 63. 12. Why in simply-typed lambda-calculus, the progress theorem has empty typing context, while the preservation theorem has a typing context? Many of these problems are from the textbook, and therefore many solutions can be found in it. Debriefing (required!): -------------------------- 1. Approximately how many hours did you spend on this assignment? 2. Would you rate it as easy, moderate, or difficult? 3. Did you work on it mostly alone, or mostly with other people? 4. How deeply do you feel you understand the material it covers (0%–100%)? 5. Any other comments? This section is intended to help us calibrate the homework assignments. Your answers to this section will *not* affect your grade; however, skipping it will certainly do.