π計算を復習

昨日のゼミで紹介してもらったけど、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

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: 前順序関係として
  • 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