I. state transformers (5.1) ------------------------------------------ STATES AND STATE TRANSFORMERS (CH 5) Ideas: Def: a *state space*, S, over a set of types X is a type environment whose types are drawn from X; i.e., a finite map from names to X. Example: Def: a *state*, s, of type S, s:S is a collection of attributes, such for all x:U in S, s has an attribute x of type U Example: Def: a state transformer, f: S -> T, is such that for all states s:S, f.s : T Example: ------------------------------------------ ------------------------------------------ TRAN State transformer category Objects: state spaces over a given set of types Arrows: state transformers Notation: category Tran has morphisms over set of types X X Hom-set ^ Tran (S,T) = S -> T X ------------------------------------------ What's the unit (1) of this category? What's composition in this category? What's an example? II. variables (5.2) A. model ------------------------------------------ STATE ATTRIBUTES (5.2) Def: An attribute of type T over state space \Sigma is a pair (gt,st) of functions, where gt: \Sigma -> T (access) st: T -> \Sigma -> \Sigma (update). Define: val.(gt,st) == gt, set.(gt,st) == st Example: ------------------------------------------ How to describe a sequence of updates? B. axioms ------------------------------------------ AXIOMS FOR ATTRIBUTES (p. 87) Let x, y be attributes of type T over \Sigma, s be a state of type \Sigma, a, b be values of type T. Basics: val.x.(set.x.a.s) == a (a) Attributes are independent (no aliasing): val.y.(set.x.a.s) == val.y.s (b) * if x != y One value per attribute: set.x.a; set.x.b == set.x.b (c) Order doesn't matter if independent set.x.a;set.y.b == set.y.b;set.x.a (d) * if x != y Only the value matters set.x.(val.x.s).s == s (e) Def: distinct attributes are called program variables if they satisfy (a) - (e). ------------------------------------------ Can you give examples of these? Can we think of x and a as lists? What is val.x2.((set.x1.3; set.x2.5; set.x1.0).s)? Why do we need to show there's a model for these? C. expressions 1. pointwise extension ------------------------------------------ EXPRESSIONS Def: an *expression of type T* is a term of HOL of type \Sigma -> T built as follows. . . e ::= gt | y | f.e1. ... .en where gt: \Sigma -> T is an access function y is a name f is a function constant Semantics [[gt]].s == gt.s . [[y]].s == y . [[f.e1. ... .en]].s == f.([[e1]].s). ... .([[en]].s) ------------------------------------------ Can these expressions have side-effects? 2. overloaded notation ------------------------------------------ OVERLOADED NOTATION FOR EXPRESSIONS . Use the same notation for both f and f since these have different types. So we define: expression value applied in that to state state ================================= 0.s == 0 1.s == 1 plus.f1.f2.s == plus.(f1.s).(f2.s) ------------------------------------------ What are f1 and f2? What are the types of 0 and 1 here? ------------------------------------------ Assume access functions are the attributes x1,...,xn, so can write plus.(val.x1).(val.x2) Overload that attribute names for names of the corresponding access functions: name access function =========================== x = val.x (f) ------------------------------------------ What's the type of each x in this table? Can we now write expressions as we want to? 3. assignment how would you generalize the update operation (set) on states to take expressions (not just values)? can you prove that (x := a); (x := x) == (x := a) ? How would you generalize the meaning of assignment to multiple assignment, x1,...,xn := e1,...,en, where x1, ..., xn are distinct? Does the order matter in a multiple assignment? III. Reasoning with program variables (5.3) ------------------------------------------ REASONING WITH PROGRAM VARIABLES (5.3) Def P_a.x means assumption (a) holds for x P_b.x.y means assump (b) for x & y etc. Def: var x1: T1, ..., xn:Tn means the set of assumptions that contains, for all 1 <= i <= n, 1 <= j <= n, i != j: P_a.xi, P_c.xi, P_e.xi, xi == val.xi P_b.xi.xj, and P_d.xi.xj. Example: var x:Int, y: Bool means the set of assumptions: val.x.(set.x.a.s) == a set.x.a; set.x.b == set.x.b set.x.(val.x.s).s == s x == val.x val.y.(set.y.a.s) == a set.y.a; set.y.b == set.y.b set.y.(val.y.s).s == s y == val.y val.x.(set.y.a.s) == val.x.s set.x.a; set.y.b == set.y.b; set.x.a val.y.(set.x.a.s) == val.y.s set.y.a; set.x.b == set.x.b; set.y.a ------------------------------------------ ------------------------------------------ GROWING AND SHRINKING ENVIRONMENTS/ASSUMPTIONS Monotonicity: Phi |- t ___________ Phi,t' |- t So for variables: var x1, ..., xm |- t _________________________________ var x1, ..., xm, y1, ..., yn |- t Change of variables var x1, ..., xm |- t _________________________________ var y1, ..., ym |- t[x1,...,xm := y1,...,ym] IV. if y1,...,ym are distinct, and if y1,...,ym are free for x1,...,xm in t ------------------------------------------ A. substitution property ------------------------------------------ SUBSTITUTION PROPERTY Lemma 5.1 (substitution lemma). Suppose x:S and y:T are state attributes. Suppose that e and f are expressions such that {x:S,y:T} |- e:S and {x:S,y:T} |- f:S. Then for all states s, var x:S, y:T |- e.((x := f).s) == e[x := f].s ------------------------------------------ How to prove this? Does this generalize to multiple assignments? ------------------------------------------ Corollary 5.2. Let x:S and y:T be state attributes. Suppose {y:T} |- e:S and {x:S,y:T} |- f:S. Then for all states s, var x:T |- e.((x := f).s) == e.s ------------------------------------------ How does this follow from the substitution lemma? B. Assignments as state transformers ------------------------------------------ Composing Successive Assignments Theorem 5.3. Suppose x:T, {x:T} |- f:T, and {x:T} |- e:T. Then var x:T |- (x := e); (x := f) == (x := f[x := e]) Proof: Let s be a state. ((x := e); (x := f)).s ------------------------------------------ How can we use this theorem for assignments to different variables? What does this say about assignments to distinct variables? C. straight-line programs (5.4) ------------------------------------------ STRAIGHT-LINE PROGRAMS (5.4) Grammar: f ::= id | x := e | f1 ; f2 where e is an expression Example: x := x + y; y := x - y; x := x - y ------------------------------------------ 1. typing ------------------------------------------ TYPING What's the state space of x := x - y ? a. {x:Int, y: Int} b. {x:Int, y: Int, z: Int} c. {x:Int, y: Int, z: Bool, w: Bool} Def: TE1 and TE2 are similar for program P iff P is well-typed in both TE1 and TE2. Def: if P is well-typed in both TE1 and TE2, then P: TE1 is similar to P: TE2. Alternative: think of progam as polymorphic P : TE -> TE for all type environments TE ------------------------------------------ So what does similar really mean for state transformers? 2. example ------------------------------------------ var x: Nat, y:Nat |- (x := x+y); (y := x-y); (x := x-y) ------------------------------------------ D. Procedures (5.5) ------------------------------------------ PROCEDURES WITH CALL-BY-REFERENCE (5.5) ^ swap.x.y = (x := x+y); (y := x-y); (x := x-y) So var a, b |- swap.a.b == (a,b := b,a) ------------------------------------------ Why does this hold? ------------------------------------------ ALIASING What is swap.a.a? Violates indepence assumptions var a,a So var a, b |- swap.a.b == (a,b := b,a) does not mean that var a, a |- swap.a.a == (a,a := a,a) instead var a |- swap.a == (a := 0) But (a,a := a,a) == skip Nonaliasing requirement for call by reference: Procedures must be applied to distinct actuals. ------------------------------------------ E. blocks and value parameters (5.6) ------------------------------------------ BLOCKS (5.6) Def: Let TE1 and TE2 be such that for all x:S \in TE1, x:S \in TE2. Then state transformers begin: TE1 -> TE2 and end: TE2 -> TE1 are a state extension pair between TE1 and TE2 iff they satisfy begin; end == id (g) Idea: begin maps s to a copy of s inside the larger state space If f: TE2 -> TE2, then we call begin; f; end a *block*. ------------------------------------------ 1. local variables ------------------------------------------ PROPERTIES OF STATE EXTENSION PAIRS Let TE1 and TE2 be such that for all xi:Ti \in TE1, xi:Ti \in TE2. Let begin, end be a state extension pair between TE1 and TE2. Named independence assumptions for all xi:Ti \in TE1, yj:Sj \in TE2 s.t. yj:Sj \not\in TE1, TE1 |- ai: Ti, TE2 |- bj: Si (xi := ai); begin == begin; (xi := ai) (h) (xi := ai); end == end; (xi := ai) (j) val.xi == end; val.xi (k) (yj := bj); end == end (l) Shorthand: begin var y1,...,yn := e1, ..., en; f end =^= begin; (y1,...,yn := e1 o end,...,en o end); f; end where the ei do not use y1, ..., yn ------------------------------------------ What do conditions (h)-(k) mean? What does e1 o end mean? How could you implement begin and end to have these properties? Should we permit redeclaration and shadowing? Can we omit the initializers? 2. working with blocks ------------------------------------------ PROVING PROPERTIES OF BLOCKS Example: var x, y |- begin var z := x; x := y; y := z end ------------------------------------------ ------------------------------------------ BLOCK/LOCAL INTRODUCTION RULES ______________________(block introduction) Phi |- f == begin var y := e; f' end * if f and f' are similar, and if f is written using only assignments __________________(local var introduction) Phi |- begin var z := e'; f end == begin var y,z := e,e'; f' end * if f and f' are similar. ------------------------------------------ What does similar mean again? So why do we have both f and f' here? 3. value parameters ------------------------------------------ CALL BY VALUE PARAMETERS Mode notation (a la Pascal): var mode = by reference val mode = by value Notation: proc set_it(var x, val e) = (x := e) means ^ set_it.x.e = (x := e) Call by value handled at call site: ^ set_it(y,3) = begin var e' := 3; set_it.y.e' end ------------------------------------------ How does that model call by value? Can this handle recursion? 4. local procedure definitions ------------------------------------------ LOCAL PROCEDURE DEFINTIONS proc f(var x, val y) = s in ... f(u,e)... =^= let f = (\ x y . s) in ... begin var y' := e; f.u.y' end ... ------------------------------------------ Do we have to be careful choosing the name y' in general?