デカルト閉復圏とラムダ計算 - (新) 檜山正幸のキマイラ飼育記 メモ編、ラムダ図 - (新) 檜山正幸のキマイラ飼育記 メモ編 の続き。とても良い描画法を思いついた。
青で書いているのは黒がなかったせい。
ラムダハウスは関手ボックス／関手ストライプ／オペレータボックスなどと同じ描画法。復圏のなかに別な描画法の領域を埋め込んで描く。領域の形がお家の形なのでラムダハウス〈lambda house〉と呼ぶ。
ラムダハウスの外の世界はデカルト閉復圏＝閉クローン。復射のプロファイルは直観主義シーケント〈LJシーケント〉として書ける。
外の世界では：
| 図 | テキスト |
|---|---|
| ワイヤー | 論理式、型 |
| ケーブル | 論理式リスト、型コンテキスト |
| ノード、ツリー | 証明・推論ルール、関数 |
| ヘッジ | 証明リスト、関数リスト |
| ダイヤグラム書き換え | リーズニング、タクティク、スクリプト |
ラムダハウスは上部の屋根と下部の部屋からなる。屋根をラムダノード〈lambda node〉、部屋を指数ボックス〈exponential box〉と呼ぶ。
ラムダノード内はベンディングされたワイヤーを配置して、指数ボックス内には右指数配置されたワイヤー達と反変にされた復射（逆行する）と共変の射を配置する。共変の射はラムダハウスの外で結合しても同じ効果が得られる。反変の逆行射は、ラムダ抽象される前に結合しても同じ効果が得られる。
必要がなければ、指数ボックスを省略してもよい。そのときは、ラムダハウスは台形になる。ラムダハウスへの入力がないときは、屋根＝ラムダノードは三角で描く。いずれにしても、ラムダハウスは外から見ると一個の復射ノードに見える。
ラムダハウスに対する操作は、ラムダ抽象と左評価と右評価。
| 図 | テキスト式 | 論理 |
|---|---|---|
| ワイヤーベンディング | ラムダ抽象 | 含意導入、演繹定理 |
| 右評価、右リンク積 | 関数適用 | 含意消去、モーダスポネンス |
| 左評価、左リンク積 | 関数逆適用 | 含意消去、モーダスポネンス |
慣れれば、ラムダハウスの境界を描かなくてもよいが、ラムダハウスを意識しないのが混乱の原因。
ついでに書いておくが、関数型プログラミング言語は関数を扱えない。唯一扱える関数が評価で、それは処理系が実装している。プログラマは関数を定義できない。定義できるのは関数データ。関数データ〈関数オブジェクト〉を圏論で言えば、ポインティング射。つまり、一般の射を定義できるのではなくて、ポインティング射だけを定義できる。2つのポインティング射（のデカルトペア）に対して評価射を後結合する行為が関数適用。
関数データaを関数にしたいなら a∪ と腰にカップ（フル反カリー化演算子）を付ける必要がある。
