カリー・ハワード対応

(コンピュータ)

【かりーはわーどたいおう】

カリー・ハワード対応(Curry-Howard correspondence)とは、論理と計算の間に存在する対応関係のこと。特に命題⇔型、証明⇔プログラムの対応関係がある。カリー・ハワード同型対応(Curry-Howard isomorphism)とも呼ばれる。

起源

ヒルベルトスタイルの直観主義論理演繹系とコンビネータに型を与えた体系の対応関係をH.カリー(Haskell B. Curry)が指摘し(1934年、1958年)、後にW.ハワード(William A. Howard)が直観主義論理の自然演繹と型付きラムダ計算の対応関係を与えた(1969年)。

対応関係の例

命題と型の間には、例えば次のような対応関係がある。

命題	型
論理積(∧)	直積型
論理和(∨)	直和型
含意(→)	関数型
量化(∀、∃)	依存型
二階論理	多相型

証明の変形(正規化)と計算の実行(簡約)の間にも対応関係があり、これは証明⇔プログラムの対応と考えることができる。

古典論理への拡張

当初は演繹体系と計算体系との対応付けは直観主義論理の範囲でなされていたが、call/ccとパースの式(Peirce's law)との対応がグリフィン(Timothy G. Griffin)によって指摘された(1990年)。
その後、パリゴ(Michel Parigot)のλμ計算(lambda-mu calculus)やワドラー(Philip Wadler)の双対計算(dual calculus)のように、古典論理に対応する計算体系も作られている。

なぜ型ファーストで考えるのか

How do you imagine a building? You consciously create each aspect, puzzling over it in stages. Inception 型なし言語に馴染みはあるものの型付言語をいざ使ってみたらどういう気持ちで書いたらいいのかわからなかったと同僚から相談があり, それをきっかけにして社内の勉強会で以下の話をしました. よく型なし vs. 型付の文脈では「型を書くのは面倒だ」「安全の方が大事だ」「でも面倒だ」「それは型推論を前提にしていないからだ」などの議論になりがちな気がしますが、これはあくまで「計算ありきの型」を考えてい…

#カリー・ハワード対応#型理論#ラムダ計算#TypeScript