「カリー／ハワード／ランベック対応の辞書」の続きです。カリー／ハワード／ランベック対応〈Curry-Howard-Lambek correspondence〉は、細部まで対応が行き届いているので、論理の推論規則の対応物を見てみます。
論理では、「導入規則と除去規則が“きれいに”ペアになっている」と言ったりしますが、他分野に移って考えると、けっこうゴチャゴチャで、たいして“きれい”でもないことが分かります。導入と除去のペアは憶えやすいのがメリットですが、整合的対称性があるわけではないです。
| 型理論 | 論理 | 圏論 |
|---|---|---|
| ペア型値関数の構成 | 連言導入規則 | 射のデカルト・ペアの構成 |
| ペアの射影関数の後結合 | 連言除去規則 | 直積の射影の後結合 |
| 値コンストラクタの挿入・補完 | 選言導入規則 | 直和の入射の挿入・補完 |
| パターンマッチ分岐による関数の構成と後結合 | 選言除去規則 | 射の余デカルト・コペアの構成と後結合 |
| ユニット型値関数の後結合 | 真の導入規則 | 終対象への射（一意自明）の後結合 |
| ユニット型からの関数の構成 | 真の除去規則（通常証明） | 終対象からの射（要素）の構成 |
| ネバー型値関数の構成 | 偽の導入規則（背理法） | 始対象への射（余要素）の構成 |
| ネバー型からの関数の後結合 | 偽の除去規則 | 始対象から射（一意自明）の後結合 |
| ラムダ抽象 | 含意導入規則 | カリー化 |
| 適用〈球値〉 | 含意除去規則 | 評価射の後結合 |
| 依存ラムダ抽象 | 全称導入規則 | 依存カリー化 |
| 依存関数の球値関数の後結合 | 全称除去規則 | 一般化射影の後結合 |
| パラメータ付き値コンストラクタの挿入・補完 | 存在導入規則 | 一般化入射の挿入・補完 |
| パラメータ付き関数の構成と後結合 | 存在除去規則 | 一般化コタプルの構成と後結合 |
圏論では、射のあいだの等式的関係、例えば $`\langle f , g \rangle; \pi_1 = f`$ などが重要ですが、論理ではあまり言及しません。分野ごとに、興味のあり方や価値観が違うからでしょう。圏論ベースで考えるなら、依存カリー化と（離散図式の）極限・余極限の議論に集約されます。
