Com S 641 --- Semantic Models of Programming Languages

	   HOMEWORK 6: Reasoning about Boolean Expressions
		 (File $Date: 2002/04/03 07:39:06 $)

Due: April 3, 2002.

The following are exercises based on Chapter 8 of Back and von Wright's book.

From now on, you may abbreviate proofs as is done in the book.  In
particular it's fine to apply focusing rules, and to compress steps
involving predicate calculus.  But check each step carefully, and be
sure that it's valid, and that it is obvious how to fill in the
missing subproofs or how to expand the step into several steps.
Remember that a proof is supposed to be convincing to a skeptical
reader.  In particular, include enough detail so that you don't fool
yourself.

Please also do your proofs on the computer with an editor.  If you use
ASCII, please write write ``=='' for equality (=), ``==>'' for
implication, ``<=='' for consequence, ``<==>'' for equivalence, ``!''
for negation, and != for inequality; also write the quantifiers as
``(\forall v :: t)'' and ``(\exists v :: t)'' and bounded
quantification as ``(\forall v : b : t)'' and ``(\exists v : b : t)''
``(\glb i \in I :: t)'' for greatest lower bound, \subseteq for
subset, etc.  (Of course, you can use a text editor that has a symbol
font with the proper symbols if you want; but I find this takes extra
time.)

1. (10 points) [8.1]
   Show that if t1 and t2 are Boolean terms, then
        if t then t1 else t2 fi <==> (t /\ t1) \/ (!t /\ t2) .

2. (15 points) [8.4]
   Prove the rules for conditional state transformers given in Theorem 8.5.

3. (15 points) [8.5]
   Show that if b is a Boolean expression,
   then (x := e); b == b[x := e]. 

4. (15 points) [8.6]
   Show that conditionals for statements and expressions are related
   as follows:
        if b then x := e1 else x := e2 fi  ==  (x := if b then e1 else e2 fi)

5. (20 points extra credit) [8.7]
   Generalize Theorem 8.4 to permit the conditions in the two
   conditional state transformers, (if b then f else g fi) and
   (if b then f' else g' fi) to be different (instead of both being b).