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