CIS 500 — Software FoundationsHomework Assignment 3Induction and Operational SemanticsDue: Monday, September 25, 2006, by noonInstructions: Use the same submission procedure as last time, paying attention to the followingpoints:• Submit this file as hw3, for example, using the command:~cis500/bin/cis500submit hw3 hw3.pdf• For this assignment, please write out proofs in detail, even though the arguments we aredealing with are pretty simple (i.e., in a journal paper, the whole proof would probably be“By straightforward induction”!). The proof of T heorem 3.5.4 is a good model.1 Exercise Suppose we add a new term flip to the grammar in Figure 3-2 of TAPL, along withtwo evaluation rules:flip −→ true(E-Flip1)flip −→ false(E-Flip2)Obviously, these additions break the property of determinacy of evaluation: given a term t, theremay in general be more than one term t’ such that t −→ t’. Similarly, the uniqueness of normalforms is lost.Suppose we write R(t) for the set of values {v | t −→∗v}.a. Prove that R(t) is finite for every t.b. Can we do better than just “finite”? I.e., is there a simple way of calculating, from t, anupper bound on the size of R(t)?2 Exercise [Required for all groups containing at least one PhD student; optional oth-erwise] Suppose, instead, that we add a new term choose to the grammar in Figure 3-2 of TAPL,along with this evaluation rule:choose −→ nv(E-Choose)That is, choose reduces in one step to an arbitrary numeric value.Again, this addition breaks the properties of determinacy of evaluation and uniqueness of normalforms. Indeed, it even introduces infinite nondeterminism: it is easy to write down terms t forwhich R(t) is infinite.a. For which natural numbers n is it the case that there is some term t with |R(t)| = n. Definea function that, for each n, yields such a term.b. Prove that evaluation always terminates in the extended system.3 Exercise TAPL exercise 3.5.16.Note: Solutions to this exercise and the next one can be found in the back of TAPL. Feel free tocompare your solutions with these. However, to get the benefit of the exercise, it is important thatyou write out your own solutions in full before looking at ours.4 Exercise TAPL exercise 3.5.17.5 Debriefing1. Approximately how many hours per 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
View Full Document
Unlocking...