Please read Chapter 8, and the first two sections of Chapter 9 in your textbook.
The rule E-PREDSUCC has a condition above the line. What happens if we remove this condition? Can we still prove progress and preservation? Explain!
The rule T-PRED has a condition above the line. What happens if we remove this condition? Can we still prove progress and preservation? Explain!
(You might find it helpful to try out what happens using the SASyLF proofs of program and preservation.)
Please do the following problems from the book:
8.3.5, 8.3.6 (p98), 9.2.2 (p103)Only turn in your answer to 9.2.2. For the others, check your answers against the back of the book.
Do the following exercises in SASyLF: 8.2.3 (you will need to define what it means to be a subterm) and 8.3.4.