カリー=ハワード同型対応
カリー=ハワード同型対応(カリー=ハワードどうけいたいおう、Curry–Howard correspondence)
カリー=ハワード同型対応(カリー=ハワードどうけいたいおう、英語: Curry–Howard correspondence)とは、プログラミング言語理論と証明論において、計算機プログラムと証明との間の直接的な対応関係のことである。「プログラム=証明」(proofs-as-programs)・「型=命題」(formulae-as-types)などとしても知られる。
1934年,1958年に,カリーが今とは少し違う形で言及
1968年,ハワードが現在の形で定式化
プログラム=証明(proofs-as-programs) カリー化
複数の引数をとる関数を1変数関数に置き換えることをカリー化
$ \begin{array}{c|c} 論理 & プログラミング \\ \hline \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}
$ \bot : 偽とする命題定数、bottom
$ \top : 真とする命題定数、top
https://www.youtube.com/watch?v=q02uYIc0s6g
参考
関連