Thu Nov 4 09:34:55 UTC 2004 it would be nice to make some decent choices at the beginning that we can use over and over again... seems there are so many possibilities, though. we could have simple sums, or complex sums. P ::= pi.P new x.P Sum_k pi_k.P P | P strictly speaking we need complex sums if we want to write pi1.P1 + pi2.P2 + pi3.P3 with a straight face. but, likewise we can't assume associativity of | either. yuck. perhaps we can just have binary sums and parallel and say that in examples we'll rely on associativity since it can be proven ok? all: par, new Parrow: unguarded binary sum, match, mismatch, definitions Sewell: nil, async output, input Milner polyadic pi: guarded indexed sum, bang Milner grey book: guarded indexed sum, bang what are the advantages of an indexed sum: no need to worry about structural congruence. disadvantages: messy to the write the reduction rule, unless one assumes commutativity. with a binary sum, we can't be guarded, or it would be impossible to write: pi1.P1 + (pi2.P2 + pi3.P3) do we really care about forcing guarded sums? =============================== test video turn off screen blanking borrow video projector take power brick! be prepared for chalk =============================== explain motivation: new names (globally unique identifiers, keys, etc.) and communication of names definition reduction emphasise alpha conversion show how scope extrusion works for reduction polyadic to monadic synchronous to asynchronous prove formally, but first, let's define labelled transitions. x-y.P -{x-y}-> P x(y).P -{xz}-> {z/y}P really need a substitution? P -{x-y}-> P' --------------------- if x /= y new y.P -{x-(y)}-> P' P -{l}-> P' --------------- if bn(l) cap fn(Q) = empty P|Q -{l}-> P'|Q and symmetrically matching? early vs late? write exercises show the reductions of something barbs, coupled, diminishing diagrams, expansion? values? ========================== Tue Nov 9 11:16:11 UTC 2004 so let's take a simple pi calculus P ::= x-y.P output xy.P input (y binds in P) new y.P restriction ("new") P|P parallel ("par") 0 nil !P replication ("bang") (i.e. monadic, no choice). ========================= examples x-y.0 | binding! be careful! look informally and then be more precise define free names: fn(P) fn(x-y.P) = {x,y} U fn(P) fn(xy.P) = {x} U (fn(P) - {y}) fn(new y.P) = fn(P) - {y} fn(P|P') = fn(P) U fn(P') fn(0) = {} fn(!P) = fn(P) quotient by alpha-conversion: xy.P = xz.{y:=z}P, z notin fn(P) new y.P = new z.{y:=z}P z notin fn(P) labels x-y xy new y.xy ============================================= Wed Nov 17 00:28:44 UTC 2004 fix parens for async encodings should ask them for next week to: * derive bounded output transitions * show why the side condition on bisim is required * ask them to prove P ~ Q implies P|S ~ Q|S. * ask them to fix the encoding of async into sync the next time, what would i do: * label every exercise and comment and make a separate sheet of all the answers * include sums from the beginning (and maybe omit bang?) * do sync in terms of async the right way (see sangiorgi's book) Tue Nov 23 16:37:22 UTC 2004 where are we now? what should i talk about in my lectures? well to start with, we need to warm up again, get every ====================== Wed Dec 1 16:37:26 UTC 2004 what's the progression here...? strong bisim is not a congruence it can be fixed in two possible ways: substitution at every step or substitution at the beginning weak bisimulation: definition weak bisimulation: examples what is a good equivalence? * barbed observation * could say two processes are equivalent if they have the same barbs. this s not very useful though: x-.y equiv x- * could say two processes are equivalent if they have the same barbs in any context. C = x.y-.k-|- distinguishes the two above. but this is not enough: x-.(y- + z-) x-.y- + x-.z- * different direction. history ... automata, ccs, labelled transitions came from CCS, and automata... as the calculi became more complex, the problems of philosophical principle: an equivalence should distinguish between two processes if and only if a context of the language can distinguish between them what does sangiorgi call it? "ground bisimulation" "strong bisimilarity": ~ "strong full bisimularity": ~c P ~c Q iff for all sigma. sigma P ~ sigma Q "strong barbed bisimilarity": ~. "strong barbed congruence": -~c: P -~c Q iff for all C. C[P] ~. C[Q] "strong barbed equivalence" -~: "barbed bisimilarity": ~~. strong barb implies weak barb "barbed congruence": =~c P =~c Q iff for all C. C[P] ~~. C[Q] "barbed equivalence": =~ P =~ Q iff for all S. P|S ~~. Q|S "bisimilarity": ~~ weak bisimulation "full bisimilarity": ~~c P ~~ Q iff for all sigma. sigma P ~~ sigma Q CHECK * all exercises from last week * show the encoding of claim: P ~- Q implies P ~ Q ============================================ NOTES FOR NEXT TIME: * think about the alphabet ahead of time!