π计算
- 2. 並?計算モデル ? （λ計算：並?計算じゃないけど、基礎的なモデル） ? π计算：プロセス代数ベースの、?常にシンプルな並?計算モデル ? アクターモデル：チャネルの無い並?計算モデル ? Join計算：化学反応プロセスのように並?計算を記述 ? Ambient計算：階層的な構造を持つ計算モデル。モビリティを記述可能 2
- 3. シンタックス 3 ::= ?cx x c c(x) c x P, Q ::= 0 .P P|Q P Q P + Q P Q ( c)P P c if x = y then P if x = y then P A(y1, . . . , yn) ::= A(xi, . . . , xn) P
- 4. 束縛変数と?由変数 ? 束縛変数 ? ??プレフィックスa(x).Pは、P中のxを束縛（P中のxは束縛変数） ? 新規チャネル(νx)Pは、P中のxを束縛する（P中のxは束縛変数） ? ?由変数 ? 送信プレフィックスax.Pは、P中のxを束縛しない（P中のxは?由変数） 4
- 5. 束縛変数と?由変数の集合 ? P中にある束縛変数の集合を、bn(P)と表記（bnはbounded nameの略） ? 例：bn(a(x).0)={x}、bn(ax)=? ? P中にある?由変数の集合を、fn(P)と表記（fnはfree nameの略） ? 例：fn(a(x).0)={a}、fn(ax)={a, x} 5
- 6. α変換 ? 束縛変数の名前を変換しても等価となる ? ただし、名前変換後の束縛変数は、既存の?由変数を新たに束縛しないと きに変換可能 ? 例 6 xをyに変換しても意味は同じ xをbに変換すると、既存の自由変数bを新たに 束縛してしまい、意味が変わってくる！ 誤例 a(x).?bx.0 a(y).?by.0 a(x).?bx.0 a(b).?bb.0
- 7. 簡約 ? チャネルの送受信で簡約していく ? （表記としてP{x0/y0, …, xn/yn}と?う表記を?いる。? これは、P中の?由変数xiをyi (0 ≦ i ≦ n)で置換するという意味） ? 例 7 （何も入力無しで簡約されるため、矢印の上にτと表記）a(x).P|?ab.Q P{x/b}|Q
- 8. ?項演算をもつ代数の性質 ? 演算?について ? 亜群：?は?項演算 ? 半群：?は、結合則を満たす?項演算 ? モノイド：?は、単位元をもち結合則を満たす?項演算? さらに、演算が可換であるときは可換モノイドという ? 群：?は、単位元をもち結合則を満たす?項演算で、各要素が逆元を持つ 8
- 9. |と+の可換モノイド的性質 9 P|Q Q|P P + Q Q + P (P|Q) P|(Q|P) (P + Q) + R P + (Q + R) P|0 P P + P P
- 10. スコープ拡張規則 10 ( x)0 0 ( x)(P|Q) P|( x)Q if x / fn(P) ( x)(P + Q) P + ( x)Q if x / fn(P) ( x)if u = v then P if u = v then ( x)P if x / {u, v} ( x)if u = v then P if u = v then ( x)P if x / {u, v} ( x)( y)P ( y)( x)P
- 11. スコープ拡張規則を?いた簡約の例（1/2） ? a(x).P|(νb)ab.Q という式を考える ? b ? fn(a(x).P) であるため(b ? fn(P)と仮定)、(νb)(a(x).P|ab.Q)と変換可能 ? よって、(νb)(P{x/b}|Q) と簡約される 11
- 12. スコープ拡張規則を?いた簡約の例（2/2） ? a(x).P|(νb)ab.Q かつb ∈ fn(P)、という式を考える ? そのままではスコープ拡張規則を適?できないため、(νb)ab.Qをα変換し、 (νb?)ab?.Qを得る。ただし、b? ? fn(P)とする。 ? あとは同様に、(νb?)(a(x).P|ab?.Q)を得て、(νb?)(P{x/b?}|Q) と簡約される 12
- 13. 同?チャネルでの複数受信 ? 同じチャネルで複数受信している場合は、?つだけ実?される 13 P =!a(x), Q = ?ay P|Q P|Q =!a(x)|?ay (a(x)|!a(x))|?ay (a(x)|?ay)!a(x) 0|!a(x) !a(x) = P !P P|!P
- 14. 多引数π计算 （Polyadic π-calculus） ? 単引数π计算（monadic π-calculus） ? これまで説明したπ计算 ? チャネルへ同時に1つの値しか送信できない ? 多引数π计算 ? チャネルへ同時に複数の値を送信可能 ? 以下の定義を、単引数π计算の定義へ追加 14 ::= ?c x0, . . . , xn x0, . . . , xn c c(x0, . . . , xn) c x0, . . . , xn
- 15. 多引数π计算から単引数π计算への変換 ? 多引数の送信と受信は、プライベートチャネルを?いた単引数π计算へ変 換可能 ? 送信 ? 受信 15 ?c x0, . . . , xn ( d)?cd. ?dx0. · · · . ?dxn c(x0, . . . , xn) c(d).d(x0). · · · .d(xn)
- 16. 多引数から単引数π计算への変換の補? 単純な変換ができない理由 16 ?c x0, . . . , xn ?cx0.?cx1. · · · .?c.xn ?c x, y |c(z, w)|c(z, w) c(x, y) ?cx.?cy|c(z).c(w)|c(z).c(w) ?cy|c(w)|c(z).c(w) c(w)|c(w)
- 17. プロセスの遷移 ? π计算のプロセスの遷移はラベル付き状態遷移系で表現される ? 例 17 P Q ?ax.P ?ax P .P P a(b).?bc.0 ?au ?uc.0 ?uc 0
- 18. π计算の操作的意味論 18 PREFIX .P P MATCH P P P + Q P STRUCT P P P Q Q Q P Q MISMATCH P P x = y if x = y then P P SUM P P P + Q P PAR P P bn( ) fn(Q) = P|Q P |Q COM P a(x) P Q ?au Q P|Q P {x/u}|Q RES P P x / ( x)P ( x)P
- 19. 推論規則を?いた、簡約の証明例（1/3） 19 a(b).?bc.0 a(u).?uc.0 a(u).?uc.0 a(u) ?uc.0 PREFIX ?uc.0 ?uc.0 a(b).?bc.0 a(u) ?uc.0 STRUCT a(b).?bc.0 a(u) ?uc.0
- 21. 推論規則を?いた、簡約の証明例（3/3） 21 ( x)(a(b).P|?ac.Q) ( x)(P{b/c}|Q) a(b).P a(b) P PREFIX ?ac.Q ?ac Q PREFIX a(b).P|?ac.Q P{b/c}|Q COM ( x)(a(b).P|?ac.Q) ( x)(P{b/c}|Q) RES ( 1)
- 22. RES規則の考察 ? αがa(b)かabで、(νx)a(b).Pと(νx)ab.Pはどう簡約されるか？ ? a≠x、b≠xのときのみRES規則が適?可能 ? a=xのとき ? (νx)a(b).P = (νx)x(b).P ≡ 0?（新規チャネルxへ送信してくる?はいない） ? (νx)ab.P = (νx)xb.P ≡ 0?（新規チャネルxを待ち受けている?はいない） ? b=xのとき（ただし、a≠x） ? (νx)a(b).P = (νx)a(x).Pのとき、(νx)のxは使われない。つまり ? (νx)ab = (νx)ax.Pは、そのままの意味。新規チャネルxを作成し、チャネルaへ送信。 22 ( x)P x / fn(P) P
- 23. 新規チャネルxを既存チャネルaに送信する場合 ? (νx)ax.Qは、a(b).P|(νx)ax.Qとなるとき、(νx)(P{b/x}|Q)と簡約される ? すなわち、 23 ( 2) ( 1) ( x)(a(b).P|?ax.Q) ( x)(P{b/x}|Q) a(b).P|( x)?ax.Q ( x)(P{b/x}|Q) STRUCT x / fn(P) {a} a(b).P|( x)?ax.Q ( x)(a(b).P|?ax.Q) ( 2)
- 24. a(b).P|(νx)ax.Qから(νx)(P{b/x}|Q)への簡約の 完全な証明図（前ページの完全版） 24 x / fn(P) {a} a(b).P|( x)?ax.Q ( x)(a(b).P|?ax.Q) a(b).P a(b) P PREFIX ?ax.Q ?ax Q PREFIX a(b).P|?ax.Q P{b/x}|Q COM ( x)(a(b).P|?ax.Q) ( x)(P{b/x}|Q) RES a(b).P|( x)?ax.Q ( x)(P{b/x}|Q) STRUCT
- 25. 新規チャネル送信のための追加規則 25 （ただし、これらは必須な規則ではなく、あくまでもオプショナル） ?a x a x fn(?a x) = {a}, bn(?a x) = {x} OPEN P ?ax P a = x ( x)P ?a x P RCOM P a(x) P Q ?a u Q u / fn(P) P|Q ( u)(P {x/u}|Q )
- 26. OPENとRCOM規則を?いた a(b).P|(νx)ax.Qの証明 26 a(b).P a(b) P PREFIX ?ax.Q ?ax Q PREFIX, a = x ( x)?ax.Q ?a x Q OPEN a(b).P|( x)?ax.Q ( x)(P{b/x}|Q) RCOM
- 27. 意味的に同じとは ? ある?つのプロセスが、意味的に同じとは厳密に表すとどう定義するか ? ?つのプロセスが、相互に動作をシミュレートできるときに、双模倣性を もつと定義（意味的に同じ） 27
- 28. 双模倣（Bisimulation） ? 同じ遷移をたどることの出来るプロセス同?は双模倣であるという ? すなわち、あるプロセスPとQが双模倣であるとは、ある対称な?項関係Rに おいて、以下が成り?つことをいう? 28 P R Q P P Q : Q Q P R Q
- 30. 強双模倣性 （Strong Bisimilarity） ? π计算では、以下の強模倣性の定義により、プロセスの同値性を定義する 30 R P Q P R Q P P bn( ) bn( ) (fn(P) fn(Q) = ) 1. = a(x) Q : Q a(x) Q u : P {x/u} R Q {x/u} 2. Q : Q Q P R Q
- 32. 表記 32 PとQが双模倣性である PとQが双模倣性でない PとQが強双模倣性である PとQが強双模倣性でない チャネルaから受信してPを実行 (aで受信したデータは利用しない） チャネルbに送信してPを実行 （bに送信するデータは何でも良い） P Q P Q P ˙ Q P ˙ Q a.P ?b.P
- 33. 双模倣性：例1 33 P P a ?b ?b 0 P ?b a a 0 Q Q a ?b ?b 0 P Q P ˙ Q P = a|?b Q = a.?b
- 34. 双模倣性：例2 34 P = a|?b Q = a.?b + ?b.a P P a ?b ?b 0 P ?b a a 0 Q Q a ?b ?b 0 Q ?b a a 0 P Q P ˙ Q
- 35. 双模倣性：例3 35 P = a(u) Q = a(x).( v)?vu P a(u) 0 Q u x u P Q P ˙ Q bn(a(u)) (fn(P) fn(Q)) = {u} = a(u)
- 36. 双模倣性：例4 36 P1 = a(x).P + a(x).0 P2 = a(x).P + a(x).0 + a(x).if x = u then P P1 x P1 a(x) P P1 a(x) 0 P2 P2 a(x) P P2 a(x) 0 P2 a(x) if x = u then P 3 x P2 a(y=u) 0 (if y = u then P ) P2 a(x=u) P (if u = u then P ) P1 P1 P2
- 37. 双模倣性：例4の続き 37 P1 = a(x).P + a(x).0 P2 = a(x).P + a(x).0 + a(x).if x = u then P P ˙ 0 P1 ˙ P2 P2 a(x) if x = u then P P1 {x/u} P1 P2 P1 ˙ P2
- 38. 強双模倣性から得られる等価式 38 STR If P Q then P = Q CG1 If P = Q then ?au.P = ?au.Q .P = .Q P + R = Q + R P|R = Q|R ( x)P = ( x)Q CG2 If P{x/y} = Q{x/y} for all y fn(P, Q, x) then a(x).P = a(x).Q S P + P = P M1 (if x = x then P) = P M2 (if x = y then P) = 0 if x = y MM1 (if x = x then P) = 0 MM2 (if x = y then P) = P if x = y R1 ( x) .P = .( x)P if x / R2 ( x) .P = 0 if = ?xy or = x(y) R3 ( x)(P + Q) = ( x)P + ( x)Q Parrow, J. (2001). An Introduction of the π calculus. In Bergs, Poise, Smolka (Eds.), Handbook of Process Algebra. Elsevier.
- 39. 強合同性 （strongly congruent） 39 P ˙ Q P Q
- 40. 強合同性の例 40 P = a|?b Q = a.?b + ?b.a + if a = b then P Q {a/b} {b/a} P ˙ Q
- 41. 強合同性から得られる等価式 41 STR If P Q then P = Q CG “=” is preserved by all operators S P + P = P MM1 (if x = x then P) = 0 GM1 (if M then P) = (if N then P) if M N GM2 (if x = y then P + if x = y then P) = P GM3 (if M then (P + Q)) = (if M then P + if M then Q) GM4 (if M then .P) = (if M then ( .if M then P)) if bn( ) / M GM5 (if x = y then .P) = (if x = y then ( {y/x}).P) GM6 (( x)if x = y then P) = 0 if x = y R1 ( x) .P = .( x)P if x / R2 ( x) .P = 0 if = ?xy or = x(y) R3 ( x)(P + Q) = ( x)P + ( x)Q Parrow, J. (2001). An Introduction of the π calculus. In Bergs, Poise, Smolka (Eds.), Handbook of Process Algebra. Elsevier.
- 42. π计算の例：セマフォ 42 Sem(r) ?r Get(r) r Rel(r) ?r P Q ( r)(Sem(r)|!Get(r).P.Rel(r)|!Get(r).Q.Rel(r)) r (r / fn(P) fn(Q))
- 43. π计算の例：?事する哲学者問題 43 Phil(l, r) !l.r.(?l|?r) Chopstick(c) ?c Phil(c0, c1)|Phil(c1, c0)|Chopstick(c0)|Chopstick(c1)
- 44. まとめ ? π计算について説明 ? 変数について（束縛変数、?由変数、α変換） ? 簡約について ? 操作的意味論 ? プロセスの等価性（双模倣性、強双模倣性、強合同性） 44
- 45. EOF 45