Programming Languages, Fall 2014 HW3 - Induction and Operational Semantics Due electronically on Blackboard on Tuesday Sep 30, 2pm. Expected Amount of Work for an average student: 8 hours. Textbooks for References: [1] TAPL, Chaps. 1 and 3 0. What's wrong with this proof? Theorem(?!): All horses are the same color. Proof: Let P(n) be the predicate "in all non-empty collections of n horses, all the horses are the same color." We show that P (n) holds for all n by induction on n (using 1 as the base case). Base case: Clearly, P(1) holds. Induction case: Given P (n), we must show P (n + 1). Consider an arbitrary collection of n + 1 horses. Remove one horse temporarily. Now we have n horses and hence, by the induction hypothesis, these n horses are all the same color. Now call the exiled horse back and send a different horse away. Again, we have a collection of n horses, which, by the induction hypothesis, are all the same color. Moreover, these n horses are the same color as the first collection. Thus, the horse we brought back was the same color as the second horse we sent away, and all the n + 1 horses are the same color. 1. How about this one? Theorem(?!): n^2 + n is odd for every n >= 1. Proof: By induction on n (again starting from 1). For the base case, observe that 1 is odd by definition. For the induction step, assume that n^2 + n is odd; we then show that (n + 1)^2 + (n + 1) is odd as follows. (n+1)^2 +(n+1) = n^2 +2n+1+n+1 = (n^2 +n)+(2n+2). But n^2 +n is odd by the induction hypothesis, and 2n + 2 is clearly even. Thus, (n^2 + n) + (2n + 2) is the sum of an odd number and an even number, hence odd. 2. Make up your own "false proof" in which an incorrect use of the induction hypothesis leads to a surprising conclusion. 3. What does "if iszero (succ 0) then pred (succ 0) else succ (pred 0)" evaluate to (in one step)? Draw the derivation tree for that one-step evaluation. 4. Exercise 3.5.13 in TAPL. 5. Exercise 3.5.17 in TAPL. 6. (from slides) We want to change the evaluation strategy so that the then and else branches of an if get evaluated (in that order) before the guard. Furthermore, if the evaluation of the then and else branches leads to the same value, we want to immediately produce that value and short-circuit the evaluation of the guard. Produce a new (complete) set of semantic rules for the above. Now redo this question using big-step semantics. 7. In Arithmetic Expressions (NB, Fig 3-2), show me a "stuck term" without using "if". How to modify the syntax to disallow such bad terms? 8. Implement in Haskell the "if then else" language (i.e., only booleans, no numbers), its one-step, multi-step, and big-step evalution. data Ast = TRUE | FALSE | IFTHENELSE Ast Ast Ast deriving (Show, Eq) For example, calling the one-step eval function eval (IFTHENELSE TRUE FALSE TRUE) will return FALSE Make sure your multi-step and big-step return the same results. 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.