プロセス計算
プロセス計算には一般に相互作用点を持たない Null プロセスも含まれる( n i l {\displaystyle {\mathit {nil}}} 、 0 {\displaystyle 0} 、 S T O P {\displaystyle {\mathit {STOP}}} 、 δ {\displaystyle \delta } など様々な表記法がある)。Null プロセスは何もせず、再帰的なプロセス生成の始点(または終点)として使われる。
プロセス計算の計算の本質を含む操作的リダクション規則は、並列合成、逐次化、入力、出力のみで与えられる。リダクションの詳細は個々のプロセス計算で異なるが、本質はほぼ同じである。リダクション規則は次の通りである。
x ⟨ y ⟩ ⋅ P | x ( v ) ⋅ Q ⟶ P | Q [ y / v ] {\displaystyle x\langle y\rangle \cdot P\;\vert \;x(v)\cdot Q\longrightarrow P\;\vert \;Q[^{y}\!/\!_{v}]}
このリダクション規則は次のように解釈される。
プロセス x ⟨ y ⟩ ⋅ P {\displaystyle x\langle y\rangle \cdot P} はメッセージ y {\displaystyle {\mathit {y}}} を通信路 x {\displaystyle {\mathit {x}}} に送出する。双対的に、プロセス x ( v ) ⋅ Q {\displaystyle x(v)\cdot Q} は通信路 x {\displaystyle {\mathit {x}}} でメッセージを受信する。