Outline for January 21, 1999

1. Greetings and felicitations!
   1. Please get your project proposals in as soon as possible, so you can get started
   2. Hand out new homework; point out #6 and review rules of attacking lassen over the network
2. Take-Grant
   1. Show bridges (as a combination of terminal and initial spans)
   2. Show islands (maximal subject-only tg-connected subgraphs)
   3. can*share(r, x, y, G₀) iff there is an edge from x to y labelled r in G₀, or all of the following hold: (1) there is a vertex y'' with an edge from y' to y labelled r; (2) there is a subject y' which terminally spans to y'', or y' = y''; (3) there is a subject x' which initially spans to x, or x' = x; and (4) there is a sequence of islands I₁, ..., I_n connected by bridges for which x' is in I₁ and y' is in I_n .
   4. Describe can*steal; don't state theorem
3. Decidability vs. Undecidability
   1. Notion of type; subject, object types
   2. SPM: types fixed at creation
   3. tickets: X/r (apply right r to entity X), X/r:c (c copy flag, so can give right away)
   4. link predicate: X possesses tickets in set dom(X). Then link(X, Y) = rights over X and Y dom(X) and dom(Y), and true; basically, everything connecting X and Y
   5. copying X/r:c from dom(X) to dom(Z): needs X/rc dom(X), link(X, Z), and [[tau]](X)/r:c f([[tau]](X), [[tau]](Z)), f filter function
   6. Do TG example pp. 82-83
   7. create: can-create (cc) relation says that subject of type a can create entities of type b iff cc(a, b) holds
   8. create rule: cr_p(a, b) = set of tickets added to dom(A), cr_c(a, b) = set of tickets added to dom(B)
   9. attenuation: cr(a, b) = cr_pp(a,b)|cr_c(a, b) is attenuating if: (1) cr_c(a, b) SUBSETEQ cr_p(a, b) and (2) a/r:c SUBSETEQ cr_p(a, b) self/r:c cr_p(a, b)
   10. cyclic: cc(a, b) cc(b, a)
   11. if attenuating acyclic, it's decidable; so that is sufficient. Open question: is it necessary?