カリー＝ハワード対応

カリー＝ハワード対応(カリー＝ハワードたいおう、Curry–Howard correspondence)

カリー＝ハワード同型対応（カリー＝ハワードどうけいたいおう、英語: Curry–Howard correspondence）とは、プログラミング言語理論と証明論において、計算機プログラムと証明との間の直接的な対応関係のことである。「プログラム＝証明」(proofs-as-programs)・「型＝命題」(formulae-as-types)などとしても知られる。

型理論と論理の対応関係

型＝命題(formulae-as-types、Propositions as Types)

プログラム＝証明(proofs-as-programs)

BHK解釈と関連しているらしい

単純型付きラムダ計算=直観主義命題論理

1934年，1958年に，カリーが今とは少し違う形で言及

1968年，ハワードが現在の形で定式化

$ \begin{array}{c|c} 論理 & 型 \\\hline 直観主義論理 & 型理論 \\ \text{命題}A & \text{型}A \\ \text{命題}A\text{の証明}a & \text{項}a:A \\ \bot & 0 \\ \top & 1 \\ A \lor B & A + B \\ A \land B & A \times B \\ A \implies B & A → B \\ \forall x \in A.B(x) & \prod_{x:A}B(x) \\ \exist x \in A.B(x) & \sum_{x:A} B(x) \\ \end{array}

命題$ A ⇔ 型$ A

命題$ A の証明$ a ⇔ 型$ A の項$ a

選言$ A \lor B ⇔ $ A + B : 直和型

連言$ A \land B ⇔ $ A \times B : 直積型

含意$ A \implies B $ A \to B : 関数型

$ \bot ⇔ $ 0

$ \bot : 偽とする命題定数、bottom

0: 空型

$ \top ⇔ $ 1

$ \top : 真とする命題定数、top

1: unit type

$ \forall x \in A.B(x) ⇔ $ \textstyle{\prod_{X:A}B(x)}

$ \textstyle{\prod_{X:A}B(x)} : 依存関数型

$ \exist x \in A.B(x) ⇔ $ \textstyle{\sum_{x:A}}B(x)

$ \textstyle{\sum_{x:A}}B(x) : 依存対型

元論文？

William A Howard. The formulae-as-types notion of construction. To HB Curry: essays on combinatory logic, lambda calculus and formalism, 44:479–490, 1980. (pdf, pdf2(LaTeX整形バージョン))

きちんと内容を把握する場合、下記を見るのが良さそう

Lectures on the Curry-Howard Isomorphism

さらに対応関係を圏論まで広げるとカリー／ハワード／ランベック対応というものがある

ホモトピー論でさらに対応関係がつくられた(？)ものはカリー=ハワード=ヴォエヴォドツキー対応

確認用

Q. カリー＝ハワード同型対応

Q. 対応していると何が良さがあるか