プロセス計算のソースを表示

'''プロセス計算'''（プロセスけいさん、{{lang-en-short|Process calculus}}）または'''プロセス代数'''（プロセスだいすう、{{lang-en-short|Process algebras}}）は、[[計算機科学]]において[[並行性|並行システム]]を形式的にモデリングする各種手法の総称。プロセス計算は、独立エージェントやプロセスの集まりにおける相互作用/通信/同期を抽象的に記述するツールである。また、プロセス記述を操作・分析可能にする[[代数学]]的規則も提供し、プロセス間の等価性について（[[双模倣性]]を使った）形式的推論を可能とする。主な具体例としては、[[Communicating Sequential Processes|CSP]]、[[Calculus of Communicating Systems|CCS]]、[[Algebra of Communicating Processes|ACP]] がある<ref name="baeten2004">J.C.M. Baeten: [http://www.win.tue.nl/fm/0402history.pdf ''A brief history of process algebra''], Rapport CSR 04-02, Vakgroep Informatica, Technische Universiteit Eindhoven, [[2004年]]</ref>。近年ではこれら以外に [[π計算]]([[:en:π-calculus|英語]])、[[アンビエント計算]]、[[PEPA]] などもある。

== 基本機能 ==
プロセス計算には非常に様々な手法が存在するが（分子の相互作用の研究に特化し、[[確率論的]]振る舞いやタイミング情報を扱うものもある）、全てのプロセス計算に共通する機能もいくつか存在する<ref>Benjamin Pierce: “Foundational Calculi for Programming Languages”, The Computer Science and Engineering Handbook, pp. 2190-2207, CRC Press, ISBN 0-8493-2909-4.</ref>。

* 独立したプロセス間の相互作用を、共有変数の更新ではなく通信（メッセージパッシング）として表現する。
* プロセスやシステムの記述に少数のプリミティブとそれらプリミティブを組み合わせた演算子を使う。
* プロセス演算子の代数学的規則を定義し、プロセスの表現を方程式を解くように操作可能とする。

== プロセスの数学 ==
プロセス計算を定義するには、通信手段を提供することを目的とした「名前（name）」または「通信路（channel）」を始点とする。多くの実装で、通信路内には効率向上のための複雑な構造があるが、理論モデルではそれらは抽象化によって消え去る。名前に加えて、古いプロセスから新たなプロセスを形成する手段が必要である。そして、以下のような演算子が一般に存在する<ref>{{cite conference|last=Baeten |first=J.C.M. |first2=M. |last2=Bravetti |title=A Generic Process Algebra | book-title = Algebraic Process Calculi: The First Twenty Five Years and Beyond (BRICS Notes Series NS-05-3) | publisher=BRICS, Department of Computer Science, University of Aarhus |date=2005年8月 | location = Bertinoro, Forl`ı, Italy }}</ref>。

* プロセス群の並列合成（parallel composition）
* データの送受信にどの通信路を使うかの指定
* 相互作用の逐次化
* 相互作用点の隠蔽
* 再帰またはプロセス複製

=== 並列合成 ===
2つのプロセス <math>\mathit{P}</math> と <math>\mathit{Q}</math> の並列合成は <math>P \vert Q</math> のように記述され、逐次型計算モデルとプロセス計算の重要な違いとなっている。並列合成は <math>\mathit{P}</math> と <math>\mathit{Q}</math> における計算を同時並行的かつ独立に進めることを可能にする。しかし同時に相互作用も可能で、同期や <math>\mathit{P}</math> から <math>\mathit{Q}</math>（あるいは逆）への通信路による情報の受け渡しが可能である。エージェントやプロセスは1度に複数の通信路と接続可能である。

通信路は同期型と非同期型がある。同期通信路の場合、メッセージを送ったエージェントは相手がそのメッセージを受け取るのを待つ。非同期通信路ではそのような同期は不要である。一部のプロセス計算（特に[[π計算]]）では、通信路そのものをメッセージとして（他の）通信路経由で送信することができ、プロセス間の連結トポロジーを変更できる。また一部のプロセス計算では、計算途中に通信路を生成することができる。

=== 通信 ===
相互作用は情報の流れる方向が決まっている場合が多い。すなわち、入力と出力は双対的相互作用プリミティブとして区別される。プロセス計算では一般に入力演算子（例えば <math>x(v)</math>）と出力演算子（例えば <math>x\langle y\rangle</math>）を定義して、それらを区別する。これらには相互作用点として名前がつけられ（ここでは <math>\mathit{x}</math>）、双対的相互作用プリミティブとして同期に使われる。

情報を交換するには、出力プロセスから入力プロセスに情報が流れるということになる。出力プリミティブには送信すべきデータを指定する。<math>x\langle y\rangle</math> の場合、<math>\mathit{y}</math> がそのデータである。同様に入力はデータを受信することを期待し、1つ以上の[[束縛変数]]を受信データと置換するためのプレースホルダーとして用いる。<math>x(v)</math> の場合、<math>\mathit{v}</math> がそれである。一回の相互作用で交換できるデータの種類の選択は、個々のプロセス計算の大きな特徴の1つである。

=== 逐次合成 ===
場合によっては、相互作用を時間的に順番に行いたいことがある。例えば、「まず <math>\mathit{x}</math> でデータを受信し、そのデータを <math>\mathit{y}</math> に送信する」というようなアルゴリズム記述はよくある。逐次合成（Sequential composition）はそのようなプロセスで使われる。これは他の計算モデルでもよく使われる。プロセス計算では逐次化演算子は一般に入力や出力と結びついていることが多い。例えば、プロセス <math>x(v)\cdot P</math> は、入力を <math>\mathit{x}</math> で待ち受ける。そして入力があったときだけプロセス <math>\mathit{P}</math> を起動し、その際に受信データは <math>\mathit{x}</math> によって識別子 <math>\mathit{v}</math> と置換されている。

=== リダクション意味論 ===
プロセス計算の計算の本質を含む操作的リダクション規則は、並列合成、逐次化、入力、出力のみで与えられる。リダクションの詳細は個々のプロセス計算で異なるが、本質はほぼ同じである。リダクション規則は次の通りである。

:<math>
x\langle y\rangle \cdot P \; \vert \; x(v)\cdot Q  \longrightarrow P \; \vert \; Q[^y\!/\!_v]
</math>

このリダクション規則は次のように解釈される。
# プロセス <math>x\langle y\rangle \cdot P</math> はメッセージ <math>\mathit{y}</math> を通信路 <math>\mathit{x}</math> に送出する。双対的に、プロセス <math>x(v)\cdot Q</math> は通信路 <math>\mathit{x}</math> でメッセージを受信する。
# メッセージが送信されると <math>x\langle y\rangle \cdot P</math> はプロセス <math>\mathit{P}</math> となり、<math>x(v)\cdot Q</math> はプロセス <math>Q[^y\!/\!_v]</math> となる。すなわち <math>\mathit{Q}</math> におけるプレースホルダー <math>\mathit{v}</math> は <math>\mathit{x}</math> における受信データ <math>\mathit{y}</math> で置換される。
出力操作の継続として<math>\mathit{P}</math> ができる範囲は、プロセス計算の特徴に大きく影響する。

=== 隠蔽 ===
プロセスが、ある相互作用点との間に形成できるコネクションの数は制限されない。しかし、相互作用点における干渉は発生しうる。コンパクトで最小なシステムを合成する際、干渉を抑えることは重要である。隠蔽（Hiding）操作はエージェントの合成と並行して、相互作用点間のコネクションの制御を可能にする。隠蔽の表し方は様々である。例えば[[π計算]]では、<math>\mathit{P}</math> における名前 <math>\mathit{x}</math> の隠蔽は <math>(\nu\; x)P</math> と表され、[[Communicating Sequential Processes|CSP]] では <math>P \setminus \{x\}</math> のように表される。

=== 再帰と複製 ===
ここまで説明した操作は有限の相互作用だけであり、停止しない場合も含む完全な計算を表すには不十分である。再帰（Recursion）操作と複製（Replication）操作は、有限の記述で無限の振る舞いを表せる。再帰は逐次モデルでもよく使われる。複製 <math>!P</math> は、可算無限個のプロセス <math>\mathit{P}</math> の並列合成を表すと理解できる。

:<math>
!P = P \vert !P
</math> 

=== Nullプロセス === 
プロセス計算には一般に相互作用点を持たない Null プロセスも含まれる（<math>\mathit{nil}</math>、<math>0</math>、<math>\mathit{STOP}</math>、<math>\delta</math> など様々な表記法がある）。Null プロセスは何もせず、再帰的なプロセス生成の始点（または終点）として使われる。

== 歴史 ==
[[20世紀]]前半、非形式的な概念だった「計算可能関数」を表現する形式手法として、[[μ再帰関数]]、[[チューリングマシン]]、[[ラムダ計算]]などが提案された。これらは相互に変換可能であり、等価であることから、[[チャーチ＝チューリングのテーゼ]]が提唱された。もう1つの特徴はあまり言及されない。これらはいずれも「逐次的」計算のモデルだったのである。計算機科学の次の段階の発展において、並行性と通信を明確に表現できる計算の記法の確立が必要とされた。そのような状況で生まれたのが、プロセス計算、[[ペトリネット]]、[[アクターモデル]]などの並行性モデルである。

プロセス計算の研究は、[[ロビン・ミルナー]]が[[1973年]]から[[1980年]]にかけて行った Calculus of Communicating Systems (CCS) の研究が最初であった。[[アントニー・ホーア]]の [[Communicating Sequential Processes]] (CSP) は[[1978年]]に発表され、そこから[[1980年代]]初めにかけて完全なプロセス計算の研究が行われた。CCS と CSP をさらに発展させようという研究も行われた。1982年、Jan Bergstra と Jan Willem Klop は後に Algebra of Communicating Processes (ACP) と呼ばれるものの研究を開始し、「プロセス代数（Process algebra）」という用語を生み出した<ref name="baeten2004"/>。CCS と CSP と ACP がプロセス計算のファミリーを形成し、その後の様々なプロセス計算の源流となっている。

== 最近の研究 ==
プロセス計算は非常に様々なものがあり、ここで解説したパラダイムに適合しないものもある。特筆すべき例として[[アンビエント計算]]がある。現在、プロセス計算の研究では以下の問題が中心課題となっている。

* 計算現象のよりよいモデルとなる新たなプロセス計算の開発
* 既存のプロセス計算の行儀の良い（well-behaved）な部分を求める。多くのプロセス計算は汎用性が高いが故に「行儀が悪い（wild）」傾向がある。また、普通の計算はプロセス計算の全体を使い果たすことは滅多になく、非常に制限された形のプロセスしか使わない。プロセスの制限形態は[[型システム]]とも関連する。
* [[ホーア論理]]のような考え方で、プロセスの任意の特性を理解可能なプロセス論理。
* 行動理論（Behavioural theory）: 2つのプロセスが同じとはどういう意味だろうか? 2つのプロセスが違うかどうかをどうやって判断できるのか? プロセスの同値クラスの代表を見つけ出すことは可能か? 一般に、コンテキスト（並列に動作する他のプロセス群）が違いを発見できない場合、プロセスは同じと見なされる。しかし、この直観を明確化するのは難しく、同一性の明確な定義が必要となる（[[停止性問題]]の結論のように決定不能と考えられている）。プロセスの同一性を判断する技術的ツールとしては[[双模倣性]]がある。
* プロセス計算の表現能力。プログラミングをしてみると、ある問題は特定の言語で解き易く、別の問題は別の言語で解き易いということがわかる。この現象は、[[チャーチ＝チューリングのテーゼ]]が同じとした計算モデルの表現能力の特徴を、より明確に示す必要があることを意味している。1つの方法として、同じアルゴリズムを2つの計算モデルで表現し、それらの間でどのような属性が保持されるかを調べるという方法がある。属性をより多く保持する方が表現能力が高いと言える。プロセス計算では、同期型π計算は非同期型よりも表現能力が高く、高階π計算と同程度であり、アンビエント計算よりは低い、という結果が知られている。
* 生物系をプロセス計算を使ってモデル化する。

== 他の並行性モデルとの関係 ==
[[:en:history monoid|history monoid]] は、相互に通信するプロセスの履歴を表現できる汎用的な [[:en:free object|free object]] である。その場合、プロセス計算は一定の方式で history monoid 上に課された[[形式言語]]である{{要出典|date=2008年3月}}。すなわち、history monoid は同期を含めたイベントの並びだけを記録するが、その際の状態遷移は記録しない。従って、history monoid にとってのプロセス計算は、[[:en:free monoid|free monoid]] にとっての形式言語と同じである（形式言語は、[[クリーネ閉包]]で生成可能な[[アルファベット (計算機科学)|アルファベット]]の有限長文字列の集合の部分集合である）。

[[ペトリネット]]や[[アクターモデル]]といった他の[[並行計算]]モデルとの違いは、通信路を使った通信を行う点である。通信路を含めたのは、それによってある種の代数学的手法が可能になるためであり、それによってプロセスを代数学的に理解しやすくなっている。

== 脚注 ==
{{reflist}}

== 参考文献 ==

* Matthew Hennessy: ''Algebraic Theory of Processes'', The MIT Press, ISBN 0-262-08171-7.
* [[アントニー・ホーア|C. A. R. Hoare]]: ''Communicating Sequential Processes'', Prentice Hall, ISBN 0-13-153289-8. 
** 同書は Jim Davis（Oxford University Computing Laboratory）が改訂しており、''[http://www.usingcsp.com/ Using CSP]'' というサイトから[[Portable Document Format|PDF]]ファイルをダウンロード可能。
* [[ロビン・ミルナー|Robin Milner]]: ''A Calculus of Communicating Systems'', Springer Verlag, ISBN 0-387-10235-3.
* [[ロビン・ミルナー|Robin Milner]]: ''Communicating and Mobile Systems: the Pi-Calculus'', Springer Verlag, ISBN 0-521-65869-1.

{{DEFAULTSORT:ふろせすけいさん}}

[[Category:並行性]]
[[Category:形式手法]]
[[Category:計算モデル]]
[[Category:並行計算]]
[[Category:形式仕様記述言語]]
[[Category:数学に関する記事]]