CSCI B522 Exercise A (Fall 2009)
Due in class Thursday, October 8, 2009
You can turn in handwritten solutions to this 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:
When proving Lemma C, you can assume that you already have a proof of
&lang a,&sigma &rang &dArra n implies
&lang a,&sigma &rang &rarra* n
&lang c,&sigma &rang &dArr &sigma' implies
&lang c,&sigma &rang &rarr* &lang skip, &sigma' &rang
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 ...).
&lang b,&sigma &rang &dArrb t implies
&lang b,&sigma &rang &rarrb* t
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."