π計算

π計算でキャンセルできるファイルコピーユーティリティを書く、というのをやっている。ちょっとした頭の体操。 Haskell を勉強し始めた頃と近いものを感じるかもしれない。
非同期π計算だと、送信をしたあとには何もできないという制約がつく。チャネル a で受けて、チャネル b に送信して再帰する(自分を呼ぶ)プロセス proc は、同期π計算だとこんな感じになるはず。

agent Proc (a,b) = a.'b.Proc(a,b)

非同期π計算だと、 'b のあとは 0 しか書けない。で、本とかで調べたわけではないからあんまり自信ないけど、たぶん proc は次のように書き換えることができる。

agent Proc2 (a,b) = a.'b.0 | a.'b.0 | ...

つまり

agent Proc2 (a,b) = !(a.'b.0)

となる、はず…。 ! はシグマ的なもののつもりだけどよくわかってない。というか Mobility Workbench において ! をどうしたらいいのかわからん。

• -

あ、これでいいのか。

agent Proc2(a,b) = a.'b.0 | Proc2(a,b)

ふーむ。