# カリー＝ハワード同型対応 [カリー＝ハワード同型対応 - Wikipedia](https://ja.wikipedia.org/wiki/%E3%82%AB%E3%83%AA%E3%83%BC%EF%BC%9D%E3%83%8F%E3%83%AF%E3%83%BC%E3%83%89%E5%90%8C%E5%9E%8B%E5%AF%BE%E5%BF%9C) **カリー＝ハワード同型対応**（カリー＝ハワードどうけいたいおう、[英語](https://ja.wikipedia.org/wiki/%E8%8B%B1%E8%AA%9E "英語"): Curry–Howard correspondence）とは、[プログラミング言語理論](https://ja.wikipedia.org/w/index.php?title=%E3%83%97%E3%83%AD%E3%82%B0%E3%83%A9%E3%83%9F%E3%83%B3%E3%82%B0%E8%A8%80%E8%AA%9E%E7%90%86%E8%AB%96&action=edit&redlink=1 "プログラミング言語理論 (存在しないページ)")と[証明論](https://ja.wikipedia.org/wiki/%E8%A8%BC%E6%98%8E%E8%AB%96 "証明論")において、計算機プログラムと証明との間の直接的な対応関係のことである。「プログラム＝証明」(proofs-as-programs)・「型＝命題」(formulae-as-types)などとしても知られる。これはアメリカの[数学者](https://ja.wikipedia.org/wiki/%E6%95%B0%E5%AD%A6%E8%80%85 "数学者")[ハスケル・カリー](https://ja.wikipedia.org/wiki/%E3%83%8F%E3%82%B9%E3%82%B1%E3%83%AB%E3%83%BB%E3%82%AB%E3%83%AA%E3%83%BC "ハスケル・カリー")と[論理学者](https://ja.wikipedia.org/wiki/%E8%AB%96%E7%90%86%E5%AD%A6%E8%80%85 "論理学者")[ウィリアム・アルヴィン・ハワード](https://ja.wikipedia.org/w/index.php?title=%E3%82%A6%E3%82%A3%E3%83%AA%E3%82%A2%E3%83%A0%E3%83%BB%E3%82%A2%E3%83%AB%E3%83%B4%E3%82%A3%E3%83%B3%E3%83%BB%E3%83%8F%E3%83%AF%E3%83%BC%E3%83%89&action=edit&redlink=1 "ウィリアム・アルヴィン・ハワード (存在しないページ)")（[英語版](https://en.wikipedia.org/wiki/William_Alvin_Howard "en:William Alvin Howard")）により最初に発見された形式論理の体系とある種の計算の体系との構文論的なアナロジーを一般化した概念である。通常はこの論理と計算の関連性はカリーとハワードに帰属される。しかしながら、このアイデアは[ブラウワー](https://ja.wikipedia.org/wiki/%E3%83%A9%E3%82%A4%E3%83%84%E3%82%A7%E3%83%B3%E3%83%BB%E3%82%A8%E3%83%92%E3%83%99%E3%83%AB%E3%83%88%E3%82%A5%E3%82%B9%E3%83%BB%E3%83%A4%E3%83%B3%E3%83%BB%E3%83%96%E3%83%A9%E3%82%A6%E3%83%AF%E3%83%BC "ライツェン・エヒベルトゥス・ヤン・ブラウワー")、[ハイティング](https://ja.wikipedia.org/wiki/%E3%82%A2%E3%83%AC%E3%83%B3%E3%83%BB%E3%83%8F%E3%82%A4%E3%83%86%E3%82%A3%E3%83%B3%E3%82%B0 "アレン・ハイティング")、[コルモゴロフ](https://ja.wikipedia.org/wiki/%E3%82%A2%E3%83%B3%E3%83%89%E3%83%AC%E3%82%A4%E3%83%BB%E3%82%B3%E3%83%AB%E3%83%A2%E3%82%B4%E3%83%AD%E3%83%95 "アンドレイ・コルモゴロフ")らが定式化した直観主義論理の操作的解釈の一種（[ブラウワー＝ハイティング＝ コルモゴロフ解釈（BHK 解釈）](https://ja.wikipedia.org/w/index.php?title=%E3%83%96%E3%83%A9%E3%82%A6%E3%83%AF%E3%83%BC%EF%BC%9D%E3%83%8F%E3%82%A4%E3%83%86%E3%82%A3%E3%83%B3%E3%82%B0%EF%BC%9D_%E3%82%B3%E3%83%AB%E3%83%A2%E3%82%B4%E3%83%AD%E3%83%95%E8%A7%A3%E9%87%88%EF%BC%88BHK_%E8%A7%A3%E9%87%88%EF%BC%89&action=edit&redlink=1 "ブラウワー＝ハイティング＝ コルモゴロフ解釈（BHK 解釈） (存在しないページ)")（[英語版](https://en.wikipedia.org/wiki/Brouwer%E2%80%93Heyting%E2%80%93Kolmogorov_interpretation "en:Brouwer–Heyting–Kolmogorov interpretation")））と関係している。[_要出典_](https://ja.wikipedia.org/wiki/Wikipedia:%E3%80%8C%E8%A6%81%E5%87%BA%E5%85%B8%E3%80%8D%E3%82%92%E3%82%AF%E3%83%AA%E3%83%83%E3%82%AF%E3%81%95%E3%82%8C%E3%81%9F%E6%96%B9%E3%81%B8 "Wikipedia:「要出典」をクリックされた方へ") ## 参考 - [関数を扱えることはどのようにプログラミング言語の能力をあげるか - きしだのHatena](https://nowokay.hatenablog.com/entry/20130807/1375879662) - [カリーハワード同型対応についてのまとめ - きしだのHatena](https://nowokay.hatenablog.com/entry/20130808/1375946759) - [Haskell/カリー=ハワード同型 - Wikibooks](https://ja.wikibooks.org/wiki/Haskell/%E3%82%AB%E3%83%AA%E3%83%BC%3D%E3%83%8F%E3%83%AF%E3%83%BC%E3%83%89%E5%90%8C%E5%9E%8B) - [TypeScriptでカリー＝ハワード同型対応（？）](https://gist.github.com/kom-bu/2d43bf1f0b940deccfdddb28557ea75c) ## まとめ 基本的な対応 | **論理（証明）** | **プログラミング（型付きラムダ計算）** | | ---------------- | -------------------------------------- | | 命題 | 型（Type） | | 証明 | プログラム（項、関数） | | 証明の構成 | プログラムの構築（型の付いた関数） | | 証明の簡約 | プログラムの評価（実行） | カリー＝ハワード同型対応を意識してプログラミングする ↓ 論理として「意味のある」型を定義し、その型を満たす関数を書く＝証明を書くことを意識する