CIS 500 — Software FoundationsHomework Assignment 5Simple typesDue: Monday, October 9, 2006, by noonSubmit your solutions as hw5, for example using the command:~cis500/bin/cis500submit hw5 hw5.pdf1 Exercise Give a typing derivation showing that:if true then 0 else succ (pred 0) : Nat2 Exercise Exercise 8.3.4 in TAPL.3 Exercise Exercise 8.3.6 in TAPL.4 Exercise Each part of this exercise suggests a different way of changing the language of typedarithmetic and boolean expressions from Chapter 8. (Note that these changes are not cumulative:each part starts from the ordinary language of Chapter 8) For each part, say w hich of the followingproperties are true in the enriched system.• Uniqueness of types• Preservation• ProgressFor each the properties that fail, give a counter-example. For those that hold, briefly explain why.(You don’t need to give a full proof — just an intuition.)1. Suppose we remove the typing rule E-PredZero.2. Suppose we add the following typing axiom:0 : Bool3. Suppose we add a new evaluation axiom:if t1then t2else t3−→ t24. Suppose we add the following typing rule:t1: Nat t2: T t3: Tif t1then t2else t3: T5. Suppose we add two new evaluation rulespred true −→ falsepred false −→ trueand the following typing rule:t1: Boolpred t1: Bool6. Suppose we add a new type Foo and two new typing rules:t1: Natpred t1: Foot1: Foosucc t1: Nat5 Exercise What rules could we add to the evaluation relation to recover the properties that failedin part 4 of exercise 4?6 Exercise State the inversion lemma (i.e., the appropriate analog of Lemma 8.2.2) for the enrichedtyping relation from part 6 of exercise 4.7 Exercise Read through the explanation and proof of the “Preservation of Types Under Substi-tution” Lemma (9.3.8). Then without looking at the book, write out the proof again in your ownwords.8 Exercise Exercise 9.3.9 in TAPL.9 Exercise Required for groups containing at least one PhD student . Optional for others.Exercise 9.3.10 in TAPL.10 Debriefing1. Approximately how many hours (p e r person, on average) did you spend on this assignment?2. Would you rate it as easy, moderate, or difficult?3. How deeply do you feel you understand the material it covers (0%–100%)?4. Any other comm
View Full Document
Unlocking...