π計算を復習
昨日のゼミで紹介してもらったけど、bisimulationで逆にわからなくなってしまったので自習。
まず、構文
- 小文字: チャネル、変数(プロセスもあり)
- 大文字: メタ変数(プロセス式だが、実際の式表現中には出ない)
- 0: nilプロセス(以降、何も影響しない)
- P | Q: プロセスを並行動作させるプロセス
- c(x).P: チャネルcに受信待ち、メッセージはxとしてbind、その後P実行するプロセス
- c
.P: チャネルcにxを送信、その後Pを実行するプロセス - (new x)P: チャネルxを作成し、bindしたプロセス
- !P: Pを無限に複製し並行実行させるプロセス
- たとえば、キューに、無限にイベントを発行したり、受け付けたりとか
例題:
- (new x)(x
.0 | x(y).y .x(y).0) | z(v).v .0 - 2つめのzは自由変数なチャネル
- 左はxにzを送り、停止
- 真ん中は、左からzを受け取り、そのzに xを送り、まつ
- 右は、真ん中からxを受け取り、xにxを送り、停止
- 真ん中でxを受け取り、停止
構造一致
- α: 束縛変数のリネーム
- P | Q ≡ Q | P
- (P | Q) | R ≡ P | (Q | R)
- P | 0 ≡ P
- (new x)(new y)P ≡ (new y)(new x)P
- (new x)0 ≡ 0
- Qにxがないとき、(new x)(P | Q) ≡ (new x)P | Q
簡約
- x
.P | x(y).Q → P | Q[z/y] (Q中のyを全部zに書き換える) - P → Qなら、P | R → Q | R
- P → Qなら、(new x)P → (new x) Q
- P ≡ P' かつ Q ≡ Q'のときP' → Q'なら、P → Q
ラベルつきの簡約
- P →a P': a
が実行されて、a(y)で受け取り、yをすべてxに置き換える
-
- 先の例では: P →x P' →z P'' →x P'''
- P': (new x)(0 | z
.x(y).0) | z(v).v(v).0 ≡ (new x)(z .x(y).0) | z(v).v .0 - P'': (new x)(x(y).0) | x
.0 - P''': (new x)(0) | 0 ≡ 0 | 0 ≡ 0
- P': (new x)(0 | z
- 先の例では: P →x P' →z P'' →x P'''
pi calculus自体は、ラムダ計算と同じような考え方でできるので、理解に問題はあまりない。
bisimulation関係
- ラベルつき状態遷移(状態S, イベントA, →)
- simulation関係R: (p,q) ⊆ R
- ∀a∀p'∃q'(p →a p' -> q →a q'): 状態pで起きる遷移すべてに対応した遷移がqになくてはいけない
- かつ (p',q') ⊆ R: つまり、関係Rの状態遷移はループする必要がある
- pRq: qはpをシミュレートする
- p ≦ q: 前順序関係として
- ∀a∀p'∃q'(p →a p' -> q →a q'): 状態pで起きる遷移すべてに対応した遷移がqになくてはいけない
- bisimulation関係: RかつR^-1
- p ≦ q かつ q ≦ p
- p 〜 q: 同値関係として
bisimulation性がpi calculusに3種類ある
- early
- late
- open
- 〜o ⊆ 〜l ⊆ 〜e
Milnerの論文: The Polyadic π-Calculus: a Tutorial
50ページあるけど、かなり読みやすい論文だと思う。これ読んだほうがはやいと思った。
オリジナル: A Calculus of Mobile Processes