π算法とIO
ここでは次の記法を使います。
- 並行: P Q
- 入力: channel>(arg) P
- 出力: channel<(arg) P
- 複製: replicate P
- 制約: new(arg) P
- 空のプロセス: 何も書かない
同じインデントで並んでるのがconcurrencyで、インデントを下げた部分は時間経過+新しいスコープを表しているというPython風表記です。
この記法を使うと(νy'(x(z).y
new(y') x>(z) y<(z) x<(y') replicate P
となります。
紹介
この記法の上で、π算法の簡約規則は次のように描けます。
◀が実行中のプロセスで、通信が起きると参照が張られるイメージです。これが本当にもとの公理を表しているのか調べていませんが、たぶんあっている気がします。
網羅的な説明・・・なんですかそれ(
種類
π算法は同期・非同期、単項・複項で四種類考えることができます。非同期というのは出力ch<(arg):PでPが0以外取れないつまり送りっぱなしのもので、複項というのはch<(arg0,arg1,...)という風に任意の個数の引数をとれるものです。オリジナルのπ計算は同期・単項にあたります。
さて、これらの間の相互変換を考えてみます。
単項→複項・非同期→同期
自明
複項同期→単項同期
FIFOみたいなチャネルを立ててやることで複数の値を渡せます。
# output(polyadic) c<(y1,...,yn) P # output(monadic) new(t) c<(t) t<(y1) ... t<(yn) P # input(polyadic) c>(y1,...,yn) P # input(monadic) c>(t) t>(y1) ... t>(yn) P
他は再帰的に書き換えるだけで問題ありません。
単項同期→単項非同期
送信先に自分の場所sを渡して新しいコネクションtを張ってもらい、それに送る感じでいけます。3-way handshakeに似てます。
# output(sync) c<(x) P # output(async) new(s) c<(s) s>(t) t<(x) P # input(sync) c>(x) P # input(async) c>(s) s<(t) t>(x) P
相互変換
さて、以上でこれら四種類のπ算法はどれも同じぐらい強力であることが分かります。以下では複項同期のものを使うことにします。
データとIOの導入
さて、Churchエンコーディングのようなものはπ算法でもできるのですが、どうせ実装では特別な最適化を施すので内部表現がどうなっているか考えずにリテラルやプリミティブを追加したい、ということがあります。かといって、チャネル以外も送れるようにするというのは美しくない。となると、チャネルで何でも表すしか無い、ということになります。
ここでは古典的なstdioと文字列がどう表現され得るか考えてみます。とりあえず、print,readline,str[A],...,str[AA],...みたいなチャネルがいま考えてる名前空間に存在するとして、それぞれのチャネルがどう振る舞えばよいか考えてみます。
もっともナイーブにprintはstr[なんとか]を受け取ると"なんとか"とどこかに印字する、としてみると、次のようになります。
print<(str[Hello world!])
さて、一見問題ないように見えますがそうでもありません。
print<(str[Hello]) print<(str[ world!])
は期待通りには動きません。(というより動くべきではない)
というのもprintがstr[Hello]を受け取るのと印字を終えるタイミングは当然異なり、もしprintが印字が終わるまで「受け取っていないかのようにふるまう」という仕様ならば、printを例えばprintCharのようなものでπ算法の枠組みで表すことは不可能になり、いきなり実装が露出してしまうからです。
printを非同期とするのは本質的な解決にはなりません。というのも入力に応じて違う振る舞いをするというのは本質的に重要なことで、いずれ同期が必要になるのです。
そこで、継続渡し風に書いてみましょう。例えば
new(s) print<(str[Hello],s) s>() print<(str[ world!],s)
printは印字が終わったらs<()することで、元のプロセスの実行フローが再開されます。継続渡しだとそのままプロセスを渡すのですが、簡単に並行実行ができると新しいプロセスを作って、前のコマンド終了のシグナルを待つだけでよいのです。
さて、この調子でありがちな例(名前を聞く)を書いてみます。
new(s) print<(str[name?],s) s>() readline<(s) s>(name) print<(str[hello, ],s) s>() print<(name,_)
わりとよさげに見えませんか。