CSCI B522 Exercise A (Fall 2009)

Due in class Thursday, October 8, 2009

You can turn in handwritten solutions to this exercise.

Exercise

The purpose of this exercise is to give you some practice (and feedback) on how to properly write up proofs.

First, read these notes on How to Structure Proofs. When writing up the proofs below, try to follow the guidance in these notes as closely as possible.

Next, review the notes for lecture 7. In particular, review Section 6. (I have recently fixed some errors in these notes, so make sure that you look at the latest version.)

Prove the following lemmas for the IMP language:

Lemma A &lang a,&sigma &rang &dArr_a n implies &lang a,&sigma &rang &rarr_a* n

Lemma C &lang c,&sigma &rang &dArr &sigma' implies &lang c,&sigma &rang &rarr* &lang skip, &sigma' &rang

When proving Lemma C, you can assume that you already have a proof of Lemma B:

Lemma B &lang b,&sigma &rang &dArr_b t implies &lang b,&sigma &rang &rarr_b* t

Note that for Lemma C, a proof sketch is already given in Section 6.2 of the notes for lecture 7. Your job is to write out the proof (of both Lemmas A and C) rigorously. By that I do not mean that you need to spell out every boring detail. However, you should not skip non-obvious steps; always clearly state how one step follows from another (e.g., by definition of X, or by induction hypothesis, or by lemma X together with fact Y); and any lemmas that you need, should clearly be stated and proved earlier. (In the case of such helper lemmas that happen to be obvious, you don't have to give a detailed proof, but you do have to say how each one can be proved---e.g., by on induction on ...).

Finally, don't be verbose; succintness and clarity is key. In particular, I'll repeat one piece of advice from the notes on How to Structure Proofs: "In general, do not attempt to write your proof in English sentences. While some written explanations can be useful, normally they (attempt to) hide the fact that the proof is imprecise and has holes in it."