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