Pict: A Programming Language Based on the Pi-Calculus

ふとした縁で雑におべんきょうした。以下のはなしは不正確な恐れがいつもの 5割増し位で高いです。そして例のごとく時宜を見て頭を整理するために適当に並べただけのメモです。

Pi-Calculus というのは Lambda-Calculus に対応するような概念らしい。つまり、計算の仕方の定義というか。

Lambda-Calculus の嬉しいこととして、シンプルな単一な概念のみで構成されている言語というのは統一的な扱いができて良い、というようなことももちろんあるけど、計算の枠組みが数学の対象として扱えるため、数学的に何々ができるということを証明してしまえばその特徴は言語として実現可能である、ということもある、らしい。具体例としては OCaml は変数宣言に型名を省略できる(型推論してくれる) 言語なのですが、その型推論が可能であるということも数学的に証明されているそうな。

で、 Pi-Calculus は並列演算の計算モデルらしい。並列計算の重要性はしばらくは増えていくでしょうからちょっと勉強しておこうと思ったわけ。

具体的にどういう計算モデルか、ということに関しては A Very Brief Introduction to the Pi-Calculus (in Japanese) がわかりやすかった。 Lambda-Calculus よりいくらかややこしい。

で、なんか適当に実際の並列処理であるところの thread とか fiber を Pi-Calculus で考えて、数学的に「コンパイラはデッドロックが起き得るコードを検出してエラーを報告できる」なんていう事実を証明しておいてくれたりすると嬉しかろうなーと思って Pict を見てみたのですけど、どちらかというと、 Pi-Calculus Base で既存のパラダイムが表現できて、十分に効率良く実行できることを証明する、というようなことを目標にしているように見えた。つまり、 Pi-Calculus 使ってちょっと今までの言語にない機能ができたぜー、というような感じではなく、とりあえず現実的な言語を実装した reference implementation 的な意味合いが強い感じがした。

まあ私は死ぬまで数学に関しては client side の人間であろうし、まあいろいろ面白そうな言語機能が実際に実装されてから見れば良いかと思っておべんきょうをやめることにした。

ちなみに今のところこの言語に関しての日本語のリソースは ほとんど無いみたい。 Pict のパッケージに入っている PostScript ドキュメントは非常に詳細書かれているし、 X を使ったソフトなど、かなり実際的なサンプルも非常に豊富に入っているので、勉強はそれなりにできると思う。

というか、誰かわかりやすく説明して下さい。