カリー・ハワード同型対応

ウィキペディア

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

出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2023/09/01 16:04 UTC 版)

関数型プログラムとして書かれた証明：自然数の加法に関する交換律のCoqによる証明。

カリー＝ハワード同型対応（カリー＝ハワードどうけいたいおう、英語: Curry–Howard correspondence）とは、プログラミング言語理論と証明論において、計算機プログラムと証明との間の直接的な対応関係のことである。「プログラム＝証明」(proofs-as-programs)・「型＝命題」(formulae-as-types)などとしても知られる。これはアメリカの数学者ハスケル・カリーと論理学者ウィリアム・アルヴィン・ハワードにより最初に発見された形式論理の体系とある種の計算の体系との構文論的なアナロジーを一般化した概念である。通常はこの論理と計算の関連性はカリーとハワードに帰属される。しかしながら、このアイデアはブラウワー、ハイティング、コルモゴロフらが定式化した直観主義論理の操作的解釈の一種（ブラウワー＝ハイティング＝ コルモゴロフ解釈（BHK 解釈））と関係している。

一般的な定式化

もっと一般的な観点からいえば、カリー＝ハワード対応は証明計算と計算模型の型システムとの間の対応である。これは2つの対応に分けられる。ひとつは、論理式と型のレベルであり、これは特定の証明体系や計算模型の選択に依存しない。いまひとつは、形式的証明とプログラムのレベルであり、これは証明体系や計算模型の選択に依存する。

論理式と型のレベルにおいて、この対応によれば、含意は関数型、論理積は直積型（タプル、構造体、リストなど、言語によって様々に呼ばれる）、論理和は直和型（バリアント、共用体、Eitherなど）、偽は空な型、真はシングルトン型のように振る舞うという。量化子は依存直積または直和にそれぞれ対応する。

まとめると、次のような表になる：

論理	プログラミング
全称量化 $\forall x\in A.B(x)$	この記事には参考文献や外部リンクの一覧が含まれていますが、脚注による参照が不十分であるため、情報源が依然不明確です。適切な位置に脚注を追加して、記事の信頼性向上にご協力ください。（2010年4月）

歴史的な文献

• Curry, Haskell (1934), “Functionality in Combinatory Logic”, Proceedings of the National Academy of Sciences, 20, pp. 584–590 .
• Curry, Haskell B.; Feys, Robert (1958), Craig, William, ed., Combinatory Logic Vol. I, Amsterdam: North-Holland , with 2 sections by William Craig, see paragraph 9E.
• De Bruijn, Nicolaas (1968), Automath, a language for mathematics, Department of Mathematics, Eindhoven University of Technology, TH-report 68-WSK-05. Reprinted in revised form, with two pages commentary, in: Automation and Reasoning, vol 2, Classical papers on computational logic 1967–1970, Springer Verlag, 1983, pp. 159–200.
• Howard, William A. (September 1980) [original paper manuscript from 1969], “The formulae-as-types notion of construction”, in Seldin, Jonathan P.; Hindley, J. Roger, To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, Boston, MA: Academic Press, pp. 479–490, ISBN 978-0-12-349050-6 .

対応の拡張

• Griffin, Timothy G. (1990), “The Formulae-as-Types Notion of Control”, Conf. Record 17th Annual ACM Symp. on Principles of Programming Languages, POPL '90, San Francisco, CA, USA, 17–19 Jan 1990, pp. 47–57 .
• Parigot, Michel (1992), “Lambda-mu-calculus: An algorithmic interpretation of classical natural deduction”, Logic Programming and Automated Reasoning: International Conference LPAR '92 Proceedings, St. Petersburg, Russia, Lecture Notes in Computer Science, 624, Berlin; New York: Springer-Verlag, pp. 190–201, ISBN 978-3-540-55727-2 .
• Herbelin, Hugo (1995), “A Lambda-Calculus Structure Isomorphic to Gentzen-Style Sequent Calculus Structure”, in Pacholski, Leszek; Tiuryn, Jerzy, Computer Science Logic, 8th International Workshop, CSL '94, Kazimierz, Poland, September 25–30, 1994, Selected Papers, Lecture Notes in Computer Science, 933, Berlin; New York: Springer-Verlag, pp. 61–75, ISBN 978-3-540-60017-6 .
• Gabbay, Dov; de Queiroz, Ruy (1992), “Extending the Curry–Howard interpretation to linear, relevant and other resource logics”, Journal of Symbolic Logic, 57, pp. 1319–1365 . (Full version of the paper presented at Logic Colloquium '90, Helsinki. Abstract in JSL 56(3):1139–1140, 1991.)
• de Queiroz, Ruy; Gabbay, Dov (1994), “Equality in Labelled Deductive Systems and the Functional Interpretation of Propositional Equality”, in Dekker, Paul; Stokhof, Martin, Proceedings of the Ninth Amsterdam Colloquium, ILLC/Department of Philosophy, University of Amsterdam, pp. 547–565, ISBN 90-74795-07-2 .
• de Queiroz, Ruy; Gabbay, Dov (1995), “The Functional Interpretation of the Existential Quantifier”, Bulletin of the Interest Group in Pure and Applied Logics, 3(2–3), pp. 243–290 . (Full version of a paper presented at Logic Colloquium '91, Uppsala. Abstract in JSL 58(2):753–754, 1993.)
• de Queiroz, Ruy; Gabbay, Dov (1997), “The Functional Interpretation of Modal Necessity”, in de Rijke, Maarten, Advances in Intensional Logic, Applied Logic Series, 7, Springer-Verlag, pp. 61–91, ISBN 978-0-7923-4711-8 .
• de Queiroz, Ruy; Gabbay, Dov (1999), “Labelled Natural Deduction”, in Ohlbach, Hans-Juergen; Reyle, Uwe, Logic, Language and Reasoning. Essays in Honor of Dov Gabbay, Trends in Logic, 7, Kluwer Acad. Pub., pp. 173–250, ISBN 978-0-7923-5687-5, http://www.springer.com/philosophy/logic/book/978-0-7923-5687-5 .
• de Oliveira, Anjolina; de Queiroz, Ruy (1999), “A Normalization Procedure for the Equational Fragment of Labelled Natural Deduction”, Logic Journal of the Interest Group in Pure and Applied Logics, 7, Oxford Univ Press, pp. 173–215 . (Full version of a paper presented at 2nd WoLLIC'95, Recife. Abstract in Journal of the Interest Group in Pure and Applied Logics 4(2):330–332, 1996.)
• Poernomo, Iman; Crossley, John; Wirsing; Martin (2005) [2005], Adapting Proofs-as-Programs: The Curry–Howard Protocol, Monographs in Computer Science, Springer, ISBN 978-0-387-23759-6 , concerns the adaptation of proofs-as-programs program synthesis to coarse-grain and imperative program development problems, via a method the authors call the Curry–Howard protocol. Includes a discussion of the Curry–Howard correspondence from a Computer Science perspective.
• de Queiroz, Ruy J.G.B.; de Oliveira, Anjolina (2011), “The Functional Interpretation of Direct Computations”, Electronic Notes in Theoretical Computer Science, 269, Elsevier, pp. 19–40, doi:10.1016/j.entcs.2011.03.003 . (Full version of a paper presented at LSFA 2010, Natal, Brazil.)

哲学的解釈

• de Queiroz, Ruy J.G.B. (1994), “Normalisation and language-games”, Dialectica, 48, pp. 83–123, http://www3.interscience.wiley.com/journal/119262585/abstract?CRETRY=1&SRETRY=0 . (Early version presented at Logic Colloquium '88, Padova. Abstract in JSL 55:425, 1990.)
• de Queiroz, Ruy J.G.B. (2001), “Meaning, function, purpose, usefulness, consequences – interconnected concepts”, Logic Journal of the Interest Group in Pure and Applied Logics, 9, pp. 693–734, http://jigpal.oxfordjournals.org/cgi/content/abstract/9/5/693 . (Early version presented at Fourteenth International Wittgenstein Symposium (Centenary Celebration) held in Kirchberg/Wechsel, August 13–20, 1989.)
• de Queiroz, Ruy J.G.B. (2008), “On reduction rules, meaning-as-use and proof-theoretic semantics”, Studia Logica, 90, pp. 211–247, http://www.springerlink.com/content/27nk266126k817gq/ .

総合的な論文

• De Bruijn, Nicolaas Govert (1995), “On the roles of types in mathematics”, in Groote, Philippe de, The Curry–Howard isomorphism, Cahiers du Centre de logique (Université catholique de Louvain), 8, Academia-Bruyland, pp. 27–54, ISBN 978-2-87209-363-2, http://alexandria.tue.nl/repository/freearticles/597627.pdf , the contribution of de Bruijn by himself.
• Geuvers, Herman (1995), “The Calculus of Constructions and Higher Order Logic”, in Groote, Philippe de, The Curry–Howard isomorphism, Cahiers du Centre de logique (Université catholique de Louvain), 8, Academia-Bruyland, pp. 139–191, ISBN 978-2-87209-363-2 , contains a synthetic introduction to the Curry–Howard correspondence.
• Gallier, Jean H. (1995), “On the Correspondence between Proofs and Lambda-Terms”, in Groote, Philippe de, The Curry–Howard isomorphism, Cahiers du Centre de logique (Université catholique de Louvain), 8, Academia-Bruyland, pp. 55–138, ISBN 978-2-87209-363-2, ftp://ftp.cis.upenn.edu/pub/papers/gallier/cahiers.pdf , contains a synthetic introduction to the Curry–Howard correspondence.

書籍

• edited by Ph. de Groote. (1995), De Groote, Philippe, ed., The Curry–Howard Isomorphism, Cahiers du Centre de Logique (Université catholique de Louvain), 8, Academia-Bruylant, ISBN 978-2-87209-363-2 , reproduces the seminal papers of Curry-Feys and Howard, a paper by de Bruijn and a few other papers.
• Sørensen, Morten Heine; Urzyczyn, Paweł (2006) [1998], Lectures on the Curry–Howard isomorphism, Studies in Logic and the Foundations of Mathematics, 149, Elsevier Science, ISBN 978-0-444-52077-7, http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.17.7385 , notes on proof theory and type theory, that includes a presentation of the Curry–Howard correspondence, with a focus on the formulae-as-types correspondence
• Girard, Jean-Yves (1987–90). Proof and Types. Translated by and with appendices by Lafont, Yves and Taylor, Paul. Cambridge University Press (Cambridge Tracts in Theoretical Computer Science, 7), ISBN 0-521-37181-3, notes on proof theory with a presentation of the Curry–Howard correspondence.
• Thompson, Simon (1991). Type Theory and Functional Programming Addison–Wesley. ISBN 0-201-41667-0.
• Poernomo, Iman; Crossley, John; Wirsing; Martin (2005) [2005], Adapting Proofs-as-Programs: The Curry–Howard Protocol, Monographs in Computer Science, Springer, ISBN 978-0-387-23759-6 , concerns the adaptation of proofs-as-programs program synthesis to coarse-grain and imperative program development problems, via a method the authors call the Curry–Howard protocol. Includes a discussion of the Curry–Howard correspondence from a Computer Science perspective.
• 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.[2]
• de Queiroz, Ruy J.G.B.; de Oliveira, Anjolina G.; Gabbay, Dov M. (2011) [2011], The Functional Interpretation of Logical Deduction, Advances in Logic, 5, Imperial College Press / World Scientific, ISBN 978-981-4360-95-1 .

参考文献

• P.T. Johnstone, 2002, Sketches of an Elephant, section D4.2 (vol 2) gives a categorical view of "what happens" in the Curry–Howard correspondence.

関連項目

• 型理論
• 形式手法
• 証明論
• 数理論理学
• プログラム意味論
• Agda（マルティン＝レーフの直観主義型理論（ITT）に基づく定理証明器）
• Coq（コカンのCalculus of Construction（CoC）に基づく定理証明器）

外部リンク

• The Curry–Howard Correspondence in Haskell
• The Monad Reader 6: Adventures in Classical-Land: Curry–Howard in Haskell, Pierce's law.