並行プログラミング concurrent programming
分散,並列,並行 いずれも複数の処理を行う。おおよその違いは 分散(distributed): 複数の処理主体が空間的に分散している。厳密には同時性とは別。 並列(parallel): （物理的に）複数の処理主体が同時に処理を行う。 並行(concurrent): 処理主体の数は問わない。純粋に論理的。
並行プログラミングの要素 プロセス： 処理主体 通信と計算 オブジェクト指向との類似性に注意 プロセスは停まるとは限らない。 プロセス： 処理主体 プロセスは停まるとは限らない。 通信と計算 各プロセスが受け持つ処理の粒度によって通信と計算の比重が変わる。 オブジェクト指向との類似性に注意
並行プログラミングの例 Communicating Sequential Process(CSP) (Hoare, 1978) Concurrent Prolog (Shapiro, 1986) Guarded Horn Clauses(GHC) (Ueda, 1988) p-calculus (Milner, 1989) 近年はセキュリティ関連で。
GHC
GHCの構文 factorial(X,Y) :- X>0 | X1:=X1, factorial(X1,Y1),Y:=X＊Y1. factorial(0,Y) :- true | Y=1. 構文 各行はガード付ホーン節(guarded Horn clause) factorial(X,Y) ゴール（プロセスを表す） 節の左辺はヘッド 右辺の縦棒|（コミット演算子）の左をガード、右をボディ
GHCの動作 ゴールの変数に節のヘッドとのパタンマッチが成功するような結合（binding）が生じ、ガードの条件を満たせば、（非同期、並行して）そのゴールを具体化された節のボディに書き換える（ゴール書き換え規則） :=は右辺を評価して代入。=は評価せず項として代入 後戻り（バックトラック）はしない！
GHCにおけるストリーム factorials([X|Xs1],Ys1) :- true | factorial(X,Y),Ys=[Y|Ys1],factorials(Xs1,Ys2). factorials([],Ys) :- true | Ys=[]. factorial(Xs,Ys) Xs←[5|Xs1] とすると Ys←[120|Ys1]となる。 Xs1←[7|Xs2] とすると Ys1←[5040|Ys2]となる。
並行計算 Xs←[150, 3 | Xs2]とすると、 Y1←150! より Y2←3!のほうが早く得られる可能性がある。
GHCの特徴 通信は（節で共有する）変数を通じて行う。 I/Oもプロセス 通信は非同期 結合(binding)の生成と観測 outstream([write(‘hello’),nl|X1]) 通信は非同期 p(X,Y) :- true | X=5,q(Y). q(Y) :- true | Y=6. プロセスX=5とY=6の実行順序は不定
GHCによる記述例1 双方向通信 ストリームXを未完成メッセージ [write(‘more?’), nl, read(T) | X1] 観測可能。 cf. Cにおけるポインタ渡し（代入通知なし）
記述例２ 履歴のあるオブジェクト stack(Xs) :- true | stk(Xs, []). stk([push(T) | Xs1], Ls) :- true | stk(Xs1,[T|Ls]). stk([pop(T) |Xs1],[L|Ls1]) :- T=L, stk(Xs1,Ls1). stk([pop(T) |Xs1],[]) :- true | T=error, stk(Xs1,[]). stk([], Ls) :- true | ture.
πcalculus
π計算の要素 x,y,z, ‥‥ （チャネルの）名前 P,Q,R ‥‥ プロセス
π計算の構文と意味 （停止したプロセス） （出力ポートｘから引数ｙを送信） （入力ポートｘから値または通信ポート名をｙで受信） （PまたはQとして振る舞う） （PとQが並行に動作できる） （通信ポートｘをPのスコープ内に制限する） （ｘとｙが一致したときのみPとして振る舞う） （A=Pとなるとき、AをPで置換）
動作 xˉy.0 | x(u).uˉv.0 | xˉz.0 略記： xˉy | x(u).uˉv | xˉz は次のようにリダクションされる 0 | yˉv | xˉz または xˉy | zˉv | 0
π計算の性質 λ計算を模倣できる 計算＝通信 チャネルが動的に生成消滅
文献 The Polyadic -Calculus: A Tutorial, (by Robin Milner). http://lampwww.epfl.ch/mobility/papers/ECS-LFCS-91-180.ps.gz リンク http://move.to/mobility