■

Robin Milner, "The Polyadic pi-Calculus: A Tutorial"
を引き続き読む。

3.1 Some derived forms

パイ計算で、ラムダ計算のカリー化のようなことをどうするか、という話。
これで便宜的に複数の引数をやりとりするチャンネルが導入される。
あと、パラメータと名前を使って、再帰的な定義を行う方法の話。
プロセスのレプリケーションを使ってほぼ同等のことを実現する、ということがかかれているようだが、
まだ理解できず。Ｙコンビネータの話を連想させる。

"Turing, Computing and Communication" Robin Milner, King's College, October 1997 http://www.fairdene.com/picalculus/

を流し読み。
HTMLのフォームやリンクをチャンネルとして考えるのは実用的かも。
フォームだったら、そのチャンネルに対して、どのような情報を送りつければよいのかというインターフェース的な仕様と、
その操作がどんな結果を引き起こすのかということに関するモデル的な仕様も必要。そこらへんをどうするか。
たとえばアマゾンのウィッシュリストを例にすると、同じ本を何度もウィッシュリストに入れるような操作を行うと、
初めの一回の操作以外は、ウィッシュリストの状態になんら変更を加えることなく、メッセージの表示のみで終わる。
あと、買い物かごに商品を入れるだけでは、商品の確保というか、リソースのロックは行われない。
こういうことは、ユーザーのメンタルモデルには漠然と存在するし、その旨がわかるような説明やＵＩの設計がなされているわけだけど、こういう外から見たときの抽象的なモデルの定義の形式的な仕方はないのか。
モデル検査、がしたいわけではなくて、クライアントとなるユーザーが、もつべきメンタルモデル（クライアントは人である必要はないんだけど）を直接記述できれば、それをもとにビュー・コントロール部分を生成したりできないかと妄想。