pi calclusを学ぶにあたって参照したドキュメントとその紹介その一
動機
ぼくはgopherなのでgorutine/channelを用いたプログラミングが好きだ。
ついでに非同期、並行プログラミングも好ましいもので、haskellやrustなんかの手法を知ってにやにやしている。
それらにともなって背景とされるhoareのCSPとその拡張のpi calclusについて調べて遊んでいる。
なんか寄り道をしてタネンバウムの分散システム本をなめたりTaPL再読なんかもしているが、
それはそれとして様々なドキュメントを参照した。
それぞれを紹介することで自分への理解度を試したいと思う。
言ってしまえば、ぼくの愚痴であり、自習ノートである。
ついては、ぼくの紹介が不十分であったり間違っていたりした場合には、
ブクマコメやツイッターなどでdisっていただけるとぼくの勉強の一助となってありがたい。
ついでに、間違った情報を界隈に広めずに済む利点がある。ご協力いただける方々には感謝を捧げたい。
以下紹介
初歩の理解のために
和訳版TaPL監修やmini-camlのsumii先生(たぶん)のところのWebにあるπ計算の紹介記事。
true/falseの定義や再帰的な処理に関しての記述を簡単に書いてある。
十全な学習にはならないが導入としてわかりやすい。
encoding: ISO-2022-JPじゃないと読めないため要注意
大学の諸先生方には口を酸っぱくして「wikipediaは参考にするな」と教えられたが
それはそれとして和訳本が見つからず、一単語しか知らない時にwikipediaのreferenceとlinkを参考にするのは大変手っ取り早い。
後に述べるMilnerの原論文のsummary的なものに仕上がっている。また、応用についてのrefをたやすく得ることができる。
spi calculus, ambient calclus, Calculi of Sequential Process, Algebra of Sequential System などだ。
pi calculusはCSPの拡張だからprocess algebraの歴史をさらっておくと理解が進むような気がする。
process algebraのサーベイ論文を読むことにした。
意味論の登場からbetri netにつながり、CCSやCSP、ASPへの経緯。またpi calclusへの拡張のモチベーションが分かるような気がする。
大本命、pi calculusの原論文。この後何回かの拡張(チャネルの可変引数とか)がされているため、後発の資料に書いてある定義と異なる部分が多々ある。
あと、記法に関しても多くの方言が存在するようだ。
part 1とpart 2で構成されていてpart 1は最小のにgrammer(と僅かなsyntax sugar)と等価性、双模倣性に関する簡単な記述と数多くの具体例(encoding to lambda calculus, tupple etcetc)、
part 2は等価性と双模倣性の関係や、強い双模倣性と弱い双模倣性に関する詳しい記述がある。
双模倣性は余再帰を用いてよしなにするらしいという点とTaPL21章に詳しいと聴くがちゃんと読んでいない。
大学の図書館にあったので借りて読んでみた。日本語で書いてあり、大変わかりやすく、前提なしでも程度理解できる。
食事する哲学者の例えを用いていたりJCSPを用いて実装からCSPを用いた並列と検証について記述している。
Javaが読めなかったので半分くらいしか読んでないが、実用における用途は大体書いてあってちょっと知りたいだけなら
これよんでおしまいで十分のようだ。
next step
可変長の引数を取るプロセスへの拡張。
Milnerの原論文でプロセスに多変数を束縛する構文が備えられていた。
複数の経路を受け取ることもできるわけだし、この構文がそのまま可変長引数に当たると思うので何故わざわざ拡張しなくてはいけないか。
自分の理解は
間違っている事に気がついたのであとで書き直す
単純な型付きpi calculusについてのスライド。形式的定義が書いてあるので、どのような定義が与えられるのか参考にした。 このあたりで一度TaPLを読み返し単純型付きラムダ計算との比較などをすると面白い。
conclusion
pi calculus、ひいてはCSPさらにはプロセス代数にまつわるドキュメントを参照として並べた。大変お粗末なものである。
形式的な定義を理解しその意味を知ることはより良い並行性、非同期性の手法を考えるのに意味があるんじゃないかなと思う。
pi calculus特有の型システムの存在しているのかだとかASPやspi calculusにanbient calculus
あまり関係ないがbetri netやactor modelなどの比較ドキュメントなども知りたいので探していきたいと思う。
プロセス間の通信経路を持つ（そのような抽象化がされている）言語でregion infferenceは使えるのかとかgorutineのGC実装にどれくらいCSPの影響あるのかなども気になるところだ。
multithread programmingにおけるGCが使えるような気がするからgorutineでのGCはそんなにプロセス代数を背景にしていないような気もする。
グリーンスレッドに関する研究開発はそれは昔からあったであろうし。
線形型をpi calculusに落としこんだらメモリ開放もよしなにできるとかないだろうか。
こんなアホなことやってないで、留年生らしく単位とって進級しろと怒る学友の姿が目に浮かびすぎてつらい。
だいがくおもんないなぁ
appendix
コレも読んどけ
* Type and Programming language
邦訳"型システム入門" 通称TaPL
ある程度の予備知識として単純型付きラムダ計算についての理解があるとpi calculusの動機についてインフォーマルな理解ができると思う。
5,6章辺りまで、深く追いかけたとしても10章まで読めばpi calculusへの導入としては十分に思える。
- Advanced Topic in Type and Programming language
上記"型システム入門"の発展版 多分通称はATTaPL
ただし僕の周りにこれを読んだことがある人がいないのでなんて呼ばれているかは分からない。
