カリー＝ハワード同型対応
出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2023/09/01 16:04 UTC 版)
カリー＝ハワード同型対応（カリー＝ハワードどうけいたいおう、英語: Curry–Howard correspondence）とは、プログラミング言語理論と証明論において、計算機プログラムと証明との間の直接的な対応関係のことである。「プログラム＝証明」(proofs-as-programs)・「型＝命題」(formulae-as-types)などとしても知られる。これはアメリカの数学者ハスケル・カリーと論理学者ウィリアム・アルヴィン・ハワードにより最初に発見された形式論理の体系とある種の計算の体系との構文論的なアナロジーを一般化した概念である。通常はこの論理と計算の関連性はカリーとハワードに帰属される。しかしながら、このアイデアはブラウワー、ハイティング、コルモゴロフらが定式化した直観主義論理の操作的解釈の一種（ブラウワー＝ハイティング＝ コルモゴロフ解釈（BHK 解釈））と関係している。[要出典]
歴史的な文献
- ^ Sørenson, Morten; Urzyczyn, Paweł, Lectures on the Curry-Howard Isomorphism
- ^ Goldblatt, “7.6 Grothendieck Topology as Intuitionistic Modality”, Mathematical Modal Logic: A Model of its Evolution, pp. 76–81
- ^ Benton; Bierman; de Paiva (1998), “Computational types from a logical perspective”, Journal of Functional Programming 8: 177–193
- ^ F. Binard and A. Felty, "Genetic programming with polymorphic types and higher-order functions." In Proceedings of the 10th annual conference on Genetic and evolutionary computation, pages 1187 1194, 2008.[1]
対応の拡張
- ^ Davies, Rowan; Pfenning, Frank (2001), “A Modal Analysis of Staged Computation”, Journal of the ACM 48 (3): 555–604, doi:10.1145/382780.382785
- ^ Pfenning, Frank; Davies, Rowan (2001), “A Judgmental Reconstruction of Modal Logic”, Mathematical Structures in Computer Science 11: 511–540, doi:10.1017/S0960129501003322
- ^ Komori, Yuichi; Cho, Arato (2010), λρ-calculus, p. 11
[続きの解説]
「カリー＝ハワード同型対応」の続きの解説一覧
- カリー＝ハワード同型対応のページへのリンク
