カリー＝ハワード対応

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

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

型＝命題(formulae-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 + B : 直和型

$ A \times B : 直積型

$ A \to B : 関数型

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

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

$ \textstyle{\prod_{X:A}B(x)}

カリー化

Propositions as Types

確認用

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

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