リダクション意味論
出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2018/10/03 08:13 UTC 版)
プロセス計算の計算の本質を含む操作的リダクション規則は、並列合成、逐次化、入力、出力のみで与えられる。リダクションの詳細は個々のプロセス計算で異なるが、本質はほぼ同じである。リダクション規則は次の通りである。 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}}} でメッセージを受信する。 メッセージが送信されると x ⟨ y ⟩ ⋅ P {\displaystyle x\langle y\rangle \cdot P} はプロセス P {\displaystyle {\mathit {P}}} となり、 x ( v ) ⋅ Q {\displaystyle x(v)\cdot Q} はプロセス Q [ y / v ] {\displaystyle Q[^{y}\!/\!_{v}]} となる。すなわち Q {\displaystyle {\mathit {Q}}} におけるプレースホルダー v {\displaystyle {\mathit {v}}} は x {\displaystyle {\mathit {x}}} における受信データ y {\displaystyle {\mathit {y}}} で置換される。 出力操作の継続として P {\displaystyle {\mathit {P}}} ができる範囲は、プロセス計算の特徴に大きく影響する。
※この「リダクション意味論」の解説は、「プロセス計算」の解説の一部です。
「リダクション意味論」を含む「プロセス計算」の記事については、「プロセス計算」の概要を参照ください。
- リダクション意味論のページへのリンク
