ラムダ・ミュー計算

パリゴ（Parigot）のラムダ・ミュー計算は、なんだか分からなかったが、純関数の計算であるラムダ計算に、コマンドの計算を足したものだと思えばいいかもしれない。

コマンドは値を持たず副作用を持つかもしれない。関数の値を捨てればコマンドとなる。コマンドの副作用はストレージに保存されていて、それを回復できるなら、関数とコマンドは相互変換できる。

コマンドの戻り値はvoidだが、voidを表す意味論的対象をレスポンス対象と呼んだりする。スター自律圏の立場なら、双対化対象（dualizing object, dualizer）のような気がする。

ラムダ・ミューでIOを表現できたりするらしいから、モナドと関連するかもしれない。ラムダ・ミューの標準的な意味論が継続だとすると、継続もモナドだから当然か？

一番興味深いのは、古典論理や否定との関係だ。古典論理のシーケントは右辺に選言を持つが、選言に近いナニカを継続変数とか制御変数とか呼ばれる変数のコンテキストで表現するらしい。

僕の山勘だと、結局は指数計算なのではないかと思うが。