昨日(9月9日)の圏論勉強会で、デカルト閉圏(CCC)の等式計算(equational calculation)が出てきました。
僕は等式計算できないし、できても納得感がないから、絵算(pictorial calculation)をしようと思いました。equational→pictorialの翻訳に手こずりましたが、絵算に持ち込んでしまえば、あとはなんとかなりました。
コンパクト閉圏では、絵を使ったラムダ計算が非常にうまくいくのですが、デカルト閉圏ではそれほどきれいな絵が描けません。それで、少しコジツケぎみの絵なんですが、これでも僕には等式計算より楽です。
とりあえず、equational→pictorial翻訳規則を書いた手書きノートのスキャン画像(デカイ、適当にサイジングしてね)。
この絵の根拠(合理化)とか、絵を使った計算例とかは、たぶんそのうち。