カリー＝ハワード対応

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

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

型理論と論理の対応関係

命題＝型

(formulae-as-types、Propositions as Types)

証明＝(プログラム/項)

proofs-as-programs

pは命題Pの証明である = pは型Pの項である

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

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 : 直和型

選言(OR)と直和型の対応

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

連言(AND)と直積型の対応

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

含意と関数型の対応

$ \bot ⇔ $ 0

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

0: 空型

偽(false)と空型の対応

$ \top ⇔ $ 1

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

1: unit type

真(true)とunit型の対応

$ \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』(pdf)

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

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

カリー＝ハワード対応をきちんと学ぶ

確認用

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

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

Q. それぞれどんな風に対応しているといえるか