「並行プロセスの理論と設計検証入門」
１２月１日土曜日、晴れ
タイトルのセミナーに参加してきた。これ。
主催者はいろいろな意味で大きな人で、尊敬する憧れの大先輩、初谷さん。
並行プロセス CSP の理論からはじめて、プロセスをいくつか定義し、それらの合成（組み合わせ）によって定義できる並行プロセスが「同じ」かどうかを確かめられる（＝検証できる）ようになろう！
そんな盛りだくさんの内容を６時間に詰め込んだ野心的なセミナー。
（検証は、初谷さんが自作なさったツール SyncStitch 上で実施）
＊ ＊ ＊
ものすごい量の勉強を背景に、咀嚼して理解を深めた達人を貸切で、手取り足取り教えてもらえるという、めちゃくちゃ贅沢な時間……！
しかし、いかんせん時間が短すぎた。
午前中基礎編の並行合成あたりまでは、ついていけたんだけれど、午後のツールを使ったハンズオンが始まったあたりから僕の脳みそが失速気味に。悔しい。
＊ ＊ ＊
仕様に非決定性があるのは、仕様を実現する実装に選択の幅があるということ。これは実装者に工夫の余地を残していると捉えられる。
非決定性があるほど、ゆるい、懐の深い仕様だと言える。（つまり、実装に工夫のしがいがある）
ただし、この仕様を実現した実装（ライブラリーとか）の利用者は、その非決定性の幅を「すべて」受け止められるように自らの仕様（と実装）を定める必要が生まれる。これは非決定性の幅が大きいほど苦労する。
＊ ＊ ＊
質疑で参加者が「拒否」について聞いてくれたのはありがたかった。
拒否はデッドロックする「可能性がある」ことなので、この否定（補集合）はシステムが「かならず」受理しなければいけないことになる。
拒否という単語のニュアンスが強いから、そうと言われるまで僕も「必ず」デッドロックすることだとぼんやりおもいこんでいた。気がする。
そして補集合をとって考える意味が見えたのは楽しかった。
非決定性があるから、この境界面は捉えるのが難しい。
＊ ＊ ＊
先ほど初谷さんのページで、過去の CSP に関する発表資料を見たんだけれど、今日の説明は涙が出そうなほど簡単にしてくださっていたんだということがわかった。
さすが名にし負う「プロセス代数」。代数に恥じぬ数式ばかりで、これは辛い。（かっこいいんだけれど……）
表示的意味論と操作的意味論による違いをおもわずにいられない。
つまり、命令型のプログラミング言語で鳴らしている人が、どうにも関数型言語はダメだ、というのに通じる、といえばいいか。
たとえ話にたとえ話を重ねる愚を犯すけれど、数学的帰納法の話で、あれも具体的に１ステップ目、２ステップ目、３ステップ目と具体例を考えていき、どうやら確からしい、という「操作的」な確認を経てから基底ステップとＮおよびＮ＋１ステップ目を定義するようなものではなかったか。
あるいは帰納的定義を見て、よくわからないからＮに２や５といった具体的な数字を入れて操作的に理解する、みたいな。
for ループで１ステップごと逐次的に書くスタイルから、 map や filter、 reduce といった関数型に移行する、その捉え方の地殻大変動的な。
＊ ＊ ＊
数式でなく、状態遷移図とイベント同期というプリミティブで、オリジナルの CSP を十全に表現できているのかは、わからない。けれどそんなのはさておいて、具体例として視覚化されたものは、ほんとうに受け取りやすい。
＊ ＊ ＊
資料をいま、少し行きつ戻りつ流し読みしているんだけれど、午後のツールを使ったところで僕の頭がだんだん失速していったのは、午前の基礎理論編では出てこなかった「チャネル」という概念や状態変数あたりから、だ。
イベント同期という話で進んでいたのに、「チャネル」があってこの上に「送信」と「受信」という「向き」が生まれた。そして、状態遷移図上の状態の「上」に状態変数が定義された。
ここいらの雑音が、集中力を奪っていったように、いまにしてみれば思える。
資料を読み返していると、観測のためにイベントを「提示」する、ともあって、ここのあたりが「送信」、そして「受信」にも繋がるのかもしれない。
＊ ＊ ＊
並行合成での同期イベントは、合成するふたつのプロセスをそれぞれ関数と見立てたときに、それらの形式パラメーターの束縛をあらわしているようにもおもえた。
隠蔽まで考えると、ふつうに関数合成をしていることと同じなのかもしれない。
＊ ＊ ＊
なにを考えるための道具なのか、なにを理解するための道具なのか、まだピンときていないけれど、プログラムが「動く」とはどういうことなのか（という僕の興味のひとつに）新しい視点をもたらしてくれそうな予感はある。
小分けにして、うまく咀嚼していきたい。