π計算

π計算の中心となるのは「名前」という概念である。この計算の単純さは、名前がコミュニケーションチャネルと変数という二重の役割を果たすことにある。

微積分で使用可能なプロセス構成要素は以下のとおりです^{[ 3 ]}（正確な定義は次のセクションで説明します）。

• 並行性、記述${\displaystyle P\mid Q}$、 どこ${\displaystyle P}$そして${\displaystyle Q}$2つのプロセスまたはスレッドが同時に実行される。
• コミュニケーション、
  • 入力プレフィックス${\displaystyle c\left(x\right).P}$は、通信チャネルで送信されたメッセージを待機するプロセスです。${\displaystyle c}$先に進む前に${\displaystyle P}$受信した名前を名前xにバインドします。通常、これはネットワークからの通信を期待するプロセス、または操作cによって一度だけ使用できるラベルをモデル化しますgoto c。
  • 出力プレフィックス${\displaystyle {\overline {c}}\langle y\rangle .P}$その名前は${\displaystyle y}$チャネルで発信されます${\displaystyle c}$先に進む前に${\displaystyle P}$通常、これはネットワーク上でメッセージを送信するか、goto c操作を実行することをモデル化します。
• 複製、書面${\displaystyle$ !\,P} は 、常に新しいコピーを作成できるプロセスと見なされるかもしれません。${\displaystyle P}$通常、これはネットワークサービスまたはラベルをモデル化しc、任意の数のgoto c操作を待機している状態を表します。
• 新しい名前の作成、書かれた${\displaystyle \left(\nu x\right)P}$これは、新しい定数x を内部に割り当てるプロセスと見なすことができる。${\displaystyle P}$π計算の定数は名前だけで定義され、常に通信チャネルです。プロセス内で新しい名前を作成することは、制限とも呼ばれます。
• nilプロセス、記述${\displaystyle 0}$は、実行が完了し停止したプロセスです。

π計算のミニマリズムゆえに通常の意味でのプログラムを書くことはできませんが、計算体系を拡張することは容易です。特に、再帰、ループ、逐次合成などの制御構造や、一階関数、真理値、リスト、整数などのデータ型を容易に定義できます。さらに、分散暗号や公開鍵暗号を考慮したπ計算の拡張も提案されています。アバディとフルネによる応用π計算もその一つです。これらの様々な拡張機能を、 π計算を任意のデータ型で拡張することによって、正式な基盤の上に置いた。

以下は、3つの並列コンポーネントで構成されるプロセスのごく簡単な例です。チャネル名xは、最初の2つのコンポーネントのみが認識しています。

${\displaystyle {\begin{aligned}(\nu x)&\;(\;{\overline {x}}\langle z\rangle .\;0\\&\;|\;x(y).\;{\overline {y}}\langle x\rangle .\;x(y).\;0\;)\\&\;|\;z(v).\;{\overline {v}}\langle v\rangle .0\end{aligned}}}$

最初の2つのコンポーネントはチャネルxで通信でき、名前yはzにバインドされます。したがって、プロセスの次のステップは

${\displaystyle {\begin{aligned}(\nu x)&\;(\;0\\&\;|\;{\overline {z}}\langle x\rangle .\;x(y).\;0\;)\\&\;|\;z(v).\;{\overline {v}}\langle v\rangle .\;0\end{aligned}}}$

残りのy は内部スコープで定義されているため影響を受けないことに注意してください。2 番目と 3 番目の並列コンポーネントはチャネル名zで通信できるようになり、名前vはxにバインドされます。プロセスの次のステップは次のとおりです。

${\displaystyle {\begin{aligned}(\nu x)&\;(\;0\\&\;|\;x(y).\;0\\&\;|\;{\overline {x}}\langle x\rangle .\;0\;)\end{aligned}}}$

ローカル名xが出力されたため、 xのスコープは第 3 コンポーネントもカバーするように拡張されることに注意してください。最後に、チャネルx は名前xを送信するために使用できます。その後、同時実行中のすべてのプロセスが停止します。

${\displaystyle {\begin{aligned}(\nu x)&\;(\;0\\&\;|\;0\\&\;|\;0\;)\end{aligned}}}$

Χ を名前と呼ばれるオブジェクトの集合とする。π計算の抽象構文は、次のBNF 文法から構築される(ここでxとyは Χ の任意の名前である)。^{[ 4 ]}

${\displaystyle {\begin{aligned}P,Q::=&\;x(y).P\,\,\,\,\,&{\text{Receive on channel }}x{\text{, bind the result to }}y{\text{, then run }}P\\&\;|\;{\overline {x}}\langle y\rangle .P\,\,\,\,\,&{\text{Send the value }}y{\text{ over channel }}x{\text{, then run }}P\\&\;|\;P|Q\,\,\,\,\,\,\,\,\,&{\text{Run }}P{\text{ and }}Q{\text{ simultaneously}}\\&\;|\;(\nu x)P\,\,\,&{\text{Create a new channel }}x{\text{ and run }}P\\&\;|\;!P\,\,\,&{\text{Repeatedly spawn copies of }}P\\&\;|\;0&{\text{Terminate the process}}\end{aligned}}}$

以下の具体的な構文では、接頭辞は並列合成（|）よりも強く結び付けられ、括弧は曖昧さを解消するために使用されます。

名前は、制約と入力接頭辞構造によって制限されます。形式的には、 π計算におけるプロセスの自由名前の集合は、以下の表によって帰納的に定義されます。プロセスの制約名前の集合は、自由名前の集合に含まれないプロセスの名前として定義されます。

還元意味論とラベル付き遷移意味論の両方において中心となるのは、構造的一致の概念である。2つのプロセスは、構造を除いて同一である場合、構造的に一致する。特に、並列合成は可換かつ結合的である。

より正確には、構造的一致は、プロセス構成要素によって保持され、以下の条件を満たす最小の等価関係として定義される。

アルファ変換：

• ${\displaystyle P\equiv Q}$もし${\displaystyle Q}$入手先は${\displaystyle P}$バインドされた名前を 1 つ以上変更することにより${\displaystyle P}$。

並列合成の公理：

• ${\displaystyle P|Q\equiv Q|P}$
• ${\displaystyle (P|Q)|R\equiv P|(Q|R)}$
• ${\displaystyle P|0\equiv P}$

制限に関する公理：

• ${\displaystyle (\nu x)(\nu y)P\equiv (\nu y)(\nu x)P}$
• ${\displaystyle (\nu x)0\equiv 0}$

複製に関する公理：

• ${\displaystyle !P\equiv P|!P}$

制限と並列に関する公理：

• ${\displaystyle (\nu x)(P|Q)\equiv (\nu x)P|Q}$xがフリーネームでない場合${\displaystyle Q}$。

この最後の公理は「スコープ拡張」公理として知られています。この公理は、出力アクションによって束縛名x がどのように押し出され、 xのスコープが拡張されるかを記述するため、中心的なものです。xが自由名である場合、${\displaystyle Q}$アルファ変換を用いることで、拡張処理を進めることができる。

私たちは書く${\displaystyle P\rightarrow P'}$もし${\displaystyle P}$計算ステップを実行できます。その後、${\displaystyle P'}$この還元関係${\displaystyle \rightarrow }$は、一連の還元規則の下で閉じられる最小の関係として定義される。

プロセスがチャネルを介して通信する能力を捉える主な削減ルールは次のとおりです。

• ${\displaystyle {\overline {x}}\langle z\rangle .P|x(y).Q\rightarrow P|Q[z/y]}$

どこ${\displaystyle Q[z/y]}$プロセスを表す${\displaystyle Q}$自由名${\displaystyle z}$は、​${\displaystyle y}$. 自由発生の場合${\displaystyle y}$次のような場所で発生します${\displaystyle z}$無料ではなく、アルファ変換が必要になる場合があります。

さらに3つのルールがあります。

• もし${\displaystyle P\rightarrow Q}$そしてまた${\displaystyle P|R\rightarrow Q|R}$。

この規則は、並列合成が計算を阻害しないことを示している。

• もし${\displaystyle P\rightarrow Q}$そしてまた${\displaystyle (\nu x)P\rightarrow (\nu x)Q}$。

この規則により、制約の下でも計算が進められることが保証される。

• もし${\displaystyle P\equiv P'}$そして${\displaystyle P'\rightarrow Q'}$そして${\displaystyle Q'\equiv Q}$そしてまた${\displaystyle P\rightarrow Q}$。

後者の規則は、構造的に一致するプロセスは同じ還元を持つと述べている。

プロセスをもう一度検討してみましょう

${\displaystyle (\nu x)({\overline {x}}\langle z\rangle .0|x(y).{\overline {y}}\langle x\rangle .x(y).0)|z(v).{\overline {v}}\langle v\rangle .0}$

還元意味論の定義を適用すると、還元が得られます。

${\displaystyle (\nu x)({\overline {x}}\langle z\rangle .0|x(y).{\overline {y}}\langle x\rangle .x(y).0)|z(v).{\overline {v}}\langle v\rangle .0\rightarrow (\nu x)(0|{\overline {z}}\langle x\rangle .x(y).0)|z(v).{\overline {v}}\langle v\rangle .0}$

還元置換公理を適用すると、${\displaystyle y}$現在は次のようにラベル付けされています${\displaystyle z}$。

次に、削減率を取得します。

${\displaystyle (\nu x)(0|{\overline {z}}\langle x\rangle .x(y).0)|z(v).{\overline {v}}\langle v\rangle .0\rightarrow (\nu x)(0|x(y).0|{\overline {x}}\langle x\rangle .0)}$

ローカル名xが出力されたため、 xのスコープは第 3 番目のコンポーネントも含むように拡張されていることに注意してください。これは、スコープ拡張公理を使用して取得されました。

次に、簡約置換公理を用いると、

${\displaystyle (\nu x)(0|0|0)}$

最後に、並列合成と制限の公理を用いると、

${\displaystyle 0}$

あるいは、π計算にラベル付き遷移意味論を与えることもできる（通信システムの計算で行われたように）。 この意味論では、状態からの遷移は${\displaystyle P}$他の州へ${\displaystyle P'}$アクションの後${\displaystyle \alpha }$表記は次のように表されます。

• ${\displaystyle P\,{\xrightarrow {\overset {}{\alpha }}}P'}$

州${\displaystyle P}$そして${\displaystyle P'}$プロセスを表し、${\displaystyle \alpha }$入力アクション${\displaystyle a(x)}$出力アクション${\displaystyle {\overline {a}}\langle x\rangle }$、または無音の作用τ。^{[ 5 ]}

ラベル付き意味論に関する標準的な結果は、構造的一致の点で還元意味論と一致するということである。 ${\displaystyle P\rightarrow P'}$かつその場合に限り${\displaystyle P\,\xrightarrow {\overset {}{\tau }} \equiv P'}$^{[ 6 ]}

π計算は普遍的な計算モデルである。これはミルナーが論文「関数をプロセスとして捉える」[10]で初めて指摘したもので、彼^はπ計算におけるラムダ計算の2つのエンコーディングを提示している。1つは即時評価（値渡し）戦略をシミュレートし、もう1つは正規順序（名前渡し）戦略をシミュレートする。どちらの場合も、重要な洞察は環境バインディングのモデリングである。例えば、「xは項に束縛される」といった具合である。${\textstyle M}$「 – 用語への接続を返すことでバインディングの要求に応答する複製エージェントとして${\displaystyle M}$。

これらの符号化を可能にするπ計算の特徴は、名前渡しと複製（または同等に、再帰的に定義されたエージェント）です。複製/再帰がない場合、π計算はチューリング完全ではなくなります。これは、再帰のない計算、さらには任意のプロセスの並列コンポーネントの数が定数で制限される有限制御π計算でも双模倣等価性が決定可能になるという事実からわかります。 ^{[ 11 ]}

初期双相似性と後期双相似性は、いずれもミルナー、パロウ、ウォーカーがπ計算に関する彼らの最初の論文で定式化した。^{[ 12 ]}

二項関係${\displaystyle R}$プロセス間の早期双模倣とは、任意のプロセスペアに対して、${\displaystyle (p,q)\in R}$、

• いつでも${\displaystyle p\,{\xrightarrow {a(x)}}\,p'}$そして、それぞれの名前について${\displaystyle y}$いくつか存在する${\displaystyle q'}$そのため${\displaystyle q\,{\xrightarrow {a(x)}}\,q'}$そして${\displaystyle (p'[y/x],q'[y/x])\in R}$;
• 入力以外の操作の場合${\displaystyle \alpha }$、 もし${\displaystyle {p{\xrightarrow {\overset {}{\alpha }}}p'}}$すると、いくつかの${\displaystyle q'}$そのため${\displaystyle q{\xrightarrow {\overset {}{\alpha }}}q'}$そして${\displaystyle (p',q')\in R}$;
• 対称的な要件${\displaystyle p}$そして${\displaystyle q}$交換された。

プロセス${\displaystyle p}$そして${\displaystyle q}$初期の二相似文字と言われ、${\displaystyle p\sim _{e}q}$ペアが${\displaystyle (p,q)\in R}$初期の双模倣性について${\displaystyle R}$。

後期双類似性では、遷移一致は伝達される名前とは独立していなければならない。二項関係${\displaystyle R}$プロセス間の遅延双模倣とは、任意のプロセスペアに対して、${\displaystyle (p,q)\in R}$、

• いつでも${\displaystyle p{\xrightarrow {a(x)}}p'}$そして何人かのために${\displaystyle q'}$それは、${\displaystyle q{\xrightarrow {a(x)}}q'}$そして${\displaystyle (p'[y/x],q'[y/x])\in R}$すべての名前 y に対して;
• 入力以外の操作の場合${\displaystyle \alpha }$、 もし${\displaystyle p{\xrightarrow {\overset {}{\alpha }}}p'}$何らかの存在が存在することを示唆する${\displaystyle q'}$そのため${\displaystyle q{\xrightarrow {\overset {}{\alpha }}}q'}$そして${\displaystyle (p',q')\in R}$;
• 対称的な要件${\displaystyle p}$そして${\displaystyle q}$交換された。

プロセス${\displaystyle p}$そして${\displaystyle q}$後期の双相文字と言われ、${\displaystyle p\sim _{l}q}$ペアが${\displaystyle (p,q)\in R}$遅延双模倣性の場合${\displaystyle R}$。

両方${\displaystyle \sim _{e}}$そして${\displaystyle \sim _{l}}$それらは、すべてのプロセス構成要素によって保存されるわけではないという意味で、一致関係ではないという問題を抱えている。より正確には、プロセスが存在する。${\displaystyle p}$そして${\displaystyle q}$そのため${\displaystyle p\sim _{e}q}$しかし${\displaystyle a(x).p\not \sim _{e}a(x).q}$この問題は、最大合同関係を考慮することで解決できる。${\displaystyle \sim _{e}}$そして${\displaystyle \sim _{l}}$それぞれ、早期一致と後期一致として知られています。

幸いなことに、この問題を回避する第3の定義が可能であり、それはSangiorgiによるオープン双類似性の問題である。 ^{[ 13 ]}

二項関係${\displaystyle R}$プロセス上の任意の要素のペアに対して、プロセスがオープン双模倣である場合${\displaystyle (p,q)\in R}$名前の置換ごとに${\displaystyle \sigma }$そしてすべての行動${\displaystyle \alpha }$、 いつでも${\displaystyle p\sigma {\xrightarrow {\overset {}{\alpha }}}p'}$すると、いくつかの${\displaystyle q'}$そのため${\displaystyle q\sigma {\xrightarrow {\overset {}{\alpha }}}q'}$そして${\displaystyle (p',q')\in R}$。

プロセス${\displaystyle p}$そして${\displaystyle q}$オープンバイシミラーであると言われ、${\displaystyle p\sim _{o}q}$ペアが${\displaystyle (p,q)\in R}$ある開双模倣に対して${\displaystyle R}$。

あるいは、双模倣同値性を還元意味論から直接定義することもできる。我々は次のように書く。${\displaystyle p\Downarrow a}$プロセスの場合${\displaystyle p}$名前に対して即座に入力または出力を許可する${\displaystyle a}$。

二項関係${\displaystyle R}$プロセス間の関係が、すべての要素のペアに対して次の条件を満たす対称関係である場合、それは有刺双模倣である。${\displaystyle (p,q)\in R}$私たちはそれを持っています

（１）${\displaystyle p\Downarrow a}$かつその場合に限り${\displaystyle q\Downarrow a}$すべての名前に対して${\displaystyle a}$

そして

（２）減少ごとに${\displaystyle p\rightarrow p'}$減少が存在する${\displaystyle q\rightarrow q'}$

そのため${\displaystyle (p',q')\in R}$。

私たちはこう言います${\displaystyle p}$そして${\displaystyle q}$バーブ双模倣が存在する場合、バーブ双模倣である。${\displaystyle R}$どこ${\displaystyle (p,q)\in R}$。

文脈を穴[]を持つπ項として定義すると、2つのプロセスPとQはバーブ合同であると言い、${\displaystyle P\sim _{b}Q\,\!}$あらゆる状況において${\displaystyle C[]}$私たちはそれを持っています${\displaystyle C[P]}$そして${\displaystyle C[Q]}$それらは有刺双相似である。有刺合同は、初期双相似によって誘発される合同と一致することが判明した。