このブログの更新は Twitterアカウント @m_hiyama で通知されます。
Follow @m_hiyama

メールでのご連絡は hiyama{at}chimaira{dot}org まで。

はじめてのメールはスパムと判定されることがあります。最初は、信頼されているドメインから差し障りのない文面を送っていただけると、スパムと判定されにくいと思います。

参照用 記事

続・カリー/ハワード/ランベック対応の辞書

カリー/ハワード/ランベック対応の辞書」の続きです。カリー/ハワード/ランベック対応〈Curry-Howard-Lambek correspondence〉は、細部まで対応が行き届いているので、論理の推論規則の対応物を見てみます。

論理では、「導入規則と除去規則が“きれいに”ペアになっている」と言ったりしますが、他分野に移って考えると、けっこうゴチャゴチャで、たいして“きれい”でもないことが分かります。導入と除去のペアは憶えやすいのがメリットですが、整合的対称性があるわけではないです。

型理論 論理 圏論
ペア型値関数の構成 連言導入規則 射のデカルト・ペアの構成
ペアの射影関数の後結合 連言除去規則 直積の射影の後結合
値コンストラクタの挿入・補完 選言導入規則 直和の入射の挿入・補完
パターンマッチ分岐による関数の構成と後結合 選言除去規則 射の余デカルト・コペアの構成と後結合
ユニット型値関数の後結合 真の導入規則 終対象への射(一意自明)の後結合
ユニット型からの関数の構成 真の除去規則(通常証明) 終対象からの射(要素)の構成
ネバー型値関数の構成 偽の導入規則(背理法) 始対象への射(余要素)の構成
ネバー型からの関数の後結合 偽の除去規則 始対象から射(一意自明)の後結合
ラムダ抽象 含意導入規則 カリー化
適用〈球値〉 含意除去規則 評価射の後結合
依存ラムダ抽象 全称導入規則 依存カリー化
依存関数の球値関数の後結合 全称除去規則 一般化射影の後結合
パラメータ付き値コンストラクタの挿入・補完 存在導入規則 一般化入射の挿入・補完
パラメータ付き関数の構成と後結合 存在除去規則 一般化コタプルの構成と後結合

圏論では、射のあいだの等式的関係、例えば $`\langle f , g \rangle; \pi_1 = f`$ などが重要ですが、論理ではあまり言及しません。分野ごとに、興味のあり方や価値観が違うからでしょう。圏論ベースで考えるなら、依存カリー化と(離散図式の)極限・余極限の議論に集約されます。