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

カリー／ハワード／ランベック対応〈Curry-Howard-Lambek correspondence〉は、「型理論（ラムダ計算を含む）」「論理」「圏論」の三分野の概念のあいだの精密・詳細な対応を与えてくれます。しかし、言葉はうまく対応してくれません。異なる分野の言語・文化・習慣にはギャップがあるからです。

言葉の対応表（つまり翻訳の辞書）が作れないのは僕の長年の悩みです。ことあるごとに辞書を試作してはうまくいかずヘコんでいます。

以下は、現時点でのだいたいの辞書〈対応表〉です。ハイフンの欄は適切な言葉が見つからなかった場所です。単語末尾の疑問符 '?' は、その言葉をその意味で使うことがポピュラーではないことを示します。単語末尾のアスタリスク '*' は、その言葉の意味を拡張・制限して使う必要があることを示します。

型理論	論理	圏論
型	命題	対象
計算	証明	射
ペア型	連言命題	直積対象
タグ付きユニオン型	選言命題	直和対象
ユニット型	真命題	終対象
ネバー型?	偽命題	始対象
アロー型	含意命題	指数対象〈内部ホム対象〉
-	-	図式
-	-	スパン図式
-	-	コスパン図式
パイ型	全称命題	スパン図式の極限対象
シグマ型	存在命題	コスパン図式の余極限対象
-	-	射達のデカルト・タプル
-	-	射達の余デカルト・コタプル
-	-	関手
型演算?	結合子〈コネクティブ〉	圏論的コンストラクタ?
コンビネータ?	シーケントの推論規則	圏論的オペレーター?
型項?	論理式	-
計算項?	証明項〈証明オブジェクト〉	-
-	証明可能	-
型付けコンテキスト*	前提*	-
ターゲット型	結論命題	余域対象
型付け判断*	シーケント*	プロファイル?*
関数定義	定理記述	-
-	ゴール〈証明要求?〉	-

ハイフンの部分を無理やりに埋めてみます。当然に、見慣れない言葉が登場してしまいます。また、上の表にはない幾つかの言葉を追加します。すべてポピュラーではない言葉なので、いちいち疑問符は付けません。

型理論	論理	圏論
型宇宙	命題宇宙	圏の対象類
（型の）要ç´	（命題の）証æ‹	ポインティグ射
基本型〈組み込み型〉	基本命題〈アトム命題〉	基本単純対象
基本関数〈組み込み関数〉	公理（命題と証拠）	基本射
型・計算の図式	命題・証明の図式	対象・射の図式
同一コンテキストの計算族	同一前提の証明族	スパン図式
同一ターゲットの計算族	同一結論の証明族	コスパン図式
計算族のインデックス	パラメータ変数	図式のインデックス〈ラベル〉
計算達のデカルト・タプル	証明達のデカルト・タプル	射達のデカルト・タプル
計算達の余デカルト・コタプル	証明達の余デカルト・コタプル	射達の余デカルト・コタプル
型理論的関手	論理的関手	関手
型項	論理式	対象項
計算項	証明項	射項
可達	証明可能	可達
型付けコンテキスト	前提	圏論的コンテキスト〈複域／多域〉
型のバンチ	命題のバンチ	対象のバンチ
関数定義	定理記述	射定義
関数宣言	事実（の宣言）	射のプロファイル（の宣言）
生成された計算系	セオリー	生成された圏
計算構成要求	証明構成要求〈ゴール〉	射構成要求

---

関連記事：

1. カリー／ハワード／ランベック対応の辞書（この記事）
2. 続・カリー／ハワード／ランベック対応の辞書
3. 論理と圏論： 導入規則と除去規則のあいだの等式的法則
4. まだある、カリー／ハワード／ランベック対応の辞書
5. タプル・コタプルとVΣ計算
6. 矢印の混乱に対処する： デカルト閉圏のための記法
7. 矢印のオーバーロードがひどい件： 所感
8. カリー／ハワード／ランベック対応の辞書： 推論規則再論
9. カリー／ハワード／ランベック対応： チートシート
10. 外部バージョンの依存カリー同型
11. 依存カリー同型に向けて
12. 集合圏における依存カリー同型
13. デカルト閉・型システム
14. 「プログラミング ＝ 証明」のはずだが