Com S 641 --- Semantic Models of Programming Languages

			HOMEWORK 7: Relations
		 (File $Date: 2002/04/11 21:39:15 $)

Due: problems 1 and 4, April 8, 2002; the rest on April 15, 2002.

The following are exercises based on Chapter 9 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) [9.2]
   Show that the identity relation is deterministic, and that
   composition of two deterministic relations is deterministic.

2. (15 points) [9.3]
   Prove Theorem 9.4(a).  Then explain why there is no rule of the
   form (x := x' | T) == True.

3. (10 points) [9.4]
   Show that the conditional relation preserves determinism; i.e., if
   relations Q and R are deterministic, then any relation of the form
    if p then Q else R fi
   is deterministic.

4. (20 points) [9.6]
   Show that in the category of state relations, composition
   distributes over bottom and join from both the left and from the
   right.  Give a counterexample showing that composition does not
   distribute over meet or over top.

5. (20 points) [9.7]
   Show that if R is a state relation, then the following properties hold:
     |dom.R| \subseteq R; R^{-1} ,
     |ran.R| \subseteq R^{-1}; R .

6. (15 points) [9.8]
   Prove Corollary 9.9.

7. (40 points) [9.9]
    Prove the following:
       R*; R* == R* ,
       (R*)* == R* .

8. (15 points) [9.10]
   Show that, for all relations R and R',
      (\forall q s :: {R}.q.s ==> {R'}.q.s) <==> R \subseteq R'.
   Here the notation {Q} is as defined in chapter 1.  That is
                ^
        {Q}.q.s = (\exists s' :: s' \in q /\ Q.s.s')

9. (20 points) [9.12]
   Define a relational block with local variable y as follows:
                              ^
      begin var y | b; R end  =  |begin|; (y := y' | b[y := y']); R; |end| ,

   (note the correction from the textbook), where the initialization
   predicate, b, is a predicate over the global variables and y.

   What property of the predicate b makes the following equation valid?
       begin var y | b; Id end == Id