I. Relations (Chapter 9) A. motivation B. relation spaces (9.1) ------------------------------------------ RELATION SPACES (9.1) Def: the *relation space from S to G* is ^ S <-> G = S -> P(G) i.e., S <-> G = S -> (G -> Bool) Predicate/Set isomorphism for Relations: Relation r \subseteq S x G determines P_r where P_r.a.b == (a,b) \in r Predicate P: S -> P(G) determines r_P where (a,b) \in r_P == P.a.b i.e., r_P = {(a,b) | P.a.b} r_P can be thought of a as a: - set of pairs - set-valued function - a predicate-valued function - curried, Boolean-valued function ------------------------------------------ 1. lattice of relations ------------------------------------------ ORDERING PROPERTIES OF RELATIONS Def: if P, Q \in S <-> G, then ^ P \subseteq Q = (\forall s \in S :: P.s \subseteq Q.s) ------------------------------------------ how would you express the ordering using implications? is the relation space ordered by this ordering a lattice? is it complete? Boolean? bounded? What's the top element of this lattice? The bottom element? What are these in terms of the sets? Why does this make sense by the pointwise extension theorem? What are the meet can join in this lattice? What is the complement in this lattice? What are the indexed meet and joins in this lattice? Why can't we use universal and existential quantifier notation? 2. other operations on relations ------------------------------------------ OTHER OPERATIONS ON RELATIONS Def: The identity relation, Id, is ^ Id.s.g = s == g Def: Composition of relations, P and Q is ^ (P@Q).s.d = (\exists g :: P.s.g /\ Q.g.d) Def: Inverse of relation, R^{-1} is ^ R^{-1}.s.g = R.g.s ------------------------------------------ Suppose P,Q : S <-> S. Does P;Q == Q;P ? C. State relation category (9.2) ------------------------------------------ STATE RELATION CATEGORY (9.2) Def: A *state relation category*, Rel, has - state spaces as objects, - relations as morphisms. ^ 1 = Id ^ P;Q = P@Q ------------------------------------------ Can you prove that composition is associative? Has Id as its unit? is composition monotoic in the relation ordering? Can you prove that ; distributes over \union and vice versa? Why doesn't composition distributed over meets? We have P ; False == False False ; P == False does anything similar hold for the composition over relation and True? II. Coercion Operators (9.3) Does coercion from relations to predicates and functions work? So which is the supertype of the other? A. definition How could we regard a function of type S -> G as a relation in S <-> G? ------------------------------------------ COERCION OPERATORS (9.3) Mapping |.| : (S -> G) -> (S <-> G) ^ |f|.s.g = f.s == g Test |.| : (S -> Bool) -> (S <-> S) ^ |p|.s.g = s == g /\ p.s ------------------------------------------ What do these mean? For example, what is |(x := 1)|.s, where s maps x to 0? What is |x >= 3|.s.g ? Is |x >= 3| like "assert x >= 3" or "assume x >= 3"? B. utility What's |true|? |false|? How would you express conjunction of predicates using test? So can one express Q.s.g /\ p.s without using /\ ? C. properties Is test, |.|: (S -> Bool) -> (S <-> S) monotonic? Does test, |.|: (S -> Bool) -> (S <-> S) preserve top? why? Does test, |.|: (S -> Bool) -> (S <-> S) preserve negation? why? ------------------------------------------ DOMAIN AND RANGE dom.R.s = (\exists g :: R.s.g) ran.R.g = (\exists s :: R.s.g) What are the types of these? ------------------------------------------ D. partial functions ------------------------------------------ PARTIAL FUNCTIONS Modeled as deterministic relations. Def: R: S <-> G is deterministic iff (\forall s g g' : R.s.g /\ R.s.g' : g' == g) ------------------------------------------ Is False deterministic? Is True deterministic? Are these partial? When is |p| partial? III. Relational Assignment (9.4) ------------------------------------------ RELATIONAL ASSIGNMENT (9.4) Definition: let x: S -> G be an attribute, let x':G be a fresh variable, and let b.x': S -> Bool be a Boolean expression. Then the relational assignment, (x := x' | b.x'), is defined as ^ (x := x' | b.x').s = {s' | (\exists x' :: s' == set.x.x'.s /\ b.x'.s)} Lemma. (alpha conversion) Suppose x' and z do not occur free in Phi and z is free for x' in b.x'. Then Phi |- (x := x' | b.x') == (x := z | (b.x')[x' := z]) ------------------------------------------ ------------------------------------------ Lemma 9.3: (x := x' | b.x').s.s' <==> (\exists x' :: s' == set.x'.x'.s /\ b.x'.s) ------------------------------------------ How would you prove this lemma? how should a multiple relational assignment be defined? how would you extend lemma 9.3 for multiple relational assignments? A. Basic Properties ------------------------------------------ Theorem 9.4: assume that x is a list of program variables, and that b and c are Boolean expressions. Then (a) var x |- (x := x' | F) == False (b) var x |- (x := x' | b.x' /\ c.x') == (x := x' | b.x') \intersect (x := x' | c.x') (c) var x |- (x := x' | b.x' \/ c.x') == (x := x' | b.x') \union (x := x' | c.x') (d) var x |- (x := x' | b.x') \subseteq (x := x' | c.x') <==> (\forall x' :: b.x' \subseteq c.x') ------------------------------------------ ------------------------------------------ ARBITRARY MEETS AND JOINS Lemma var x |- (x := x' | (\forall i \in I :: b.i.x')) == (\intersect i \in I :: (x := x' | b.i.x')) Lemma var x |- (x := x' | (\exists i \in I :: b.i.x')) == (\union i \in I :: (x := x' | b.i.x')) ------------------------------------------ ------------------------------------------ Lemma 9.5: assume that x and y are lists of program variables, and that b.x' is a Boolean expression in which y' does not occur free. Then var x, y |- (x := x' | b.x') == (x,y := x',y' | b.x' /\ y' == y) ------------------------------------------ how would you prove this? ------------------------------------------ Theorem 9.6: assume that x is a list of attributes. Then (a) var x |- (x := x' | x' == x) == Id (b) var x |- (x := x'' | b.x''); (x:= x' | c.x') == (x := x' | (\exists x'' :: b.x'' /\ (c.x')[x := x''])) ------------------------------------------ why is the "Id" capitalized in part (a)? What is (c,d := c',d' | d' > 7); (c,d := c',d' | d' == d /\ c' > 0)? ------------------------------------------ Theorem 9.7: Assume x is a list of program variables, e is an expression, and b and c.x' are Boolean expressions. Furthermore, assume that x' does not occur free in b or e. Then (a) var x |- |b| == (x := x' | b /\ x == x') (b) var x |- |x := e| == (x := x' | x' == e) (c) var x |- dom.(x := x' | c.x') == (\exists x' :: c.x') ------------------------------------------ B. Derived Properties of Relational Assignments ------------------------------------------ INDEPENDENT RELATIONAL ASSIGNMENT Corollary 9.8: assume that x and y are disjoint lists of attributes. (a) If y' does not occur free in b.x', and x' does not occur free in c.y', then var x, y |- (x := x' | b.x'); (y := y' | c.y') == (x,y := x',y' | b.x' /\ c.y'[x := x']) (b) If x and x' do not occur free in c.y', and if y and y' do not occur free in b.x', then var x, y |- (x := x' | b.x'); (y := y' | c.y') == (y := y' | c.y'); (x := x' | b.x') ------------------------------------------ how do these follow from Theorem 9.6? ------------------------------------------ ADDING LEADING AND TRAIL AND ASSIGNMENTS Corollary 9.9: (a) If x' and y' are not free in e, then var x, y |- (x, y := x', y' | b.x'.y'[x := e]) == |x := e|; (x, y := x', y' | b.x'.y') (b) If x' is not free in b.y', and if y is not free in e, then var x, y |- (x, y := x', y' | b.y' /\ x' == e) == (y := y' | b.y'); |x := e[y' := y]| ------------------------------------------ What do these mean? 1. dividing a problem into subproblems IV. Using Relations To Reason About Programs A. Relations As Programs (9.5) ------------------------------------------ RELATIONS AS PROGRAMS (9.5) Relations can model - partiality, for R: S <-> G, when dom.R != S - nontermination - nondeterminism when R.s has more than one element Conditional state relation: ^ if p then Q else R = |p|;Q \union |!p|;R Guarded relations: |p1|;R1 \union ... \union |p2|;R2 Reflexive transitive closure: ^ R* = (\union i : i >= 0 : R^{i}), where R^{0} == Id, R^{i+1} == R;R^{i}, for i >= 0 Iterated relation: ^ while p do R od = (|p|;R)*; |!p| ------------------------------------------ Do conditional state relations preserve determinism? What happens if the guards in a guarded relation are not mutually exclusive? When does (while p do R od).s.s' hold? What is (while true do |x := x+1| od).s ? ------------------------------------------ LANGUAGE OF STATE RELATIONS Nondeterministic language (specifications) S ::= Id | |b| | (x := x' | b) | S1 ; S2 | S1 \union S2 | S* where b is an expression, x is a list of state attributes Deterministic language (programs) P ::= Id | |b| | |x := e| | P1 ; P2 | if b then P1 else P2 fi | while b do P od where b is an expression, x is a list of state attributes ------------------------------------------ Is the specification language deterministic? Is the programming language deterministic? Total? How would you define blocks for relations? B. Correctness and Refinement (9.6) 1. angelic choices ------------------------------------------ CORRECTNESS AND REFINEMENT (9.6) ANGELIC CHOICES Suppose only our agent can make choices: R1 \union R2 means s {| R |} q iff p {| R |} q iff Def: R is angelically correct wrt p and q iff ------------------------------------------ When does our agent have to breach the contract? ------------------------------------------ TOTAL CORRECTNESS Suppose R is deterministic. What does p {| R |} q mean then? ------------------------------------------ In what sense is this angelic? ------------------------------------------ ANGELIC REFINEMENT If our agent is making choices, when is R \refinedby_A R'? ------------------------------------------ If R \refinedby_A R', does s {| R |} q ==> s {| R' |} q ? If R \refinedby_A R', is R' at least as defined as R? If R \refinedby_A R', is R' at least as deterministic as R? Is this the right notion of refinement of a specification? 2. demonic choices ------------------------------------------ DEMONIC CHOICES Suppose only the other agent can make choices: R1 \union R2 means s {| R |} q iff p {| R |} q iff Def: R is demonically correct wrt p and q iff ------------------------------------------ What happens if there's no final state that satisfies q? ------------------------------------------ PARTIAL CORRECTNESS Suppose R is deterministic. What does p {| R |} q mean then? ------------------------------------------ In what sense is this demonic? ------------------------------------------ DEMONIC REFINEMENT If our agent is making choices, when is R \refinedby_D R'? ------------------------------------------ If R \refinedby_D R', does s {| R |} q ==> s {| R' |} q ? If R \refinedby_D R', is R' at least as defined as R? If R \refinedby_D R', is R' at least as deterministic as R? 3. Relations As Specifications Which is the right notion of refinement of a specification? ------------------------------------------ REFINEMENT OF SPECIFICATIONS (x := y | -e < x - y*y < e) \refinedby_D if x >= 0 and e > 0 then (x := y | -e < x - y*y < e) else True fi \refinedby_D if x >= 0 and e > 0 then (x := y | -e < x - y*y < e) else Id fi ------------------------------------------