カリー＝ハワード同型対応
カリー=ハワード同型対応(カリー=ハワードどうけいたいおう、英語: Curry–Howard correspondence)とは、プログラミング言語理論と証明論において、計算機プログラムと証明との間の直接的な対応関係のことである。「プログラム=証明」(proofs-as-programs)・「型=命題」(formulae-as-types)などとしても知られる。これはアメリカの数学者ハスケル・カリーと論理学者ウィリアム・アルヴィン・ハワード(英語版)により最初に発見された形式論理の体系とある種の計算の体系との構文論的なアナロジーを一般化した概念である。通常はこの論理と計算の関連性はカリーとハワードに帰属される。しかしながら、このアイデアはブラウワー、ハイティング、コルモゴロフらが定式化した直観主義論理の操作的解釈の一種(ブラウワー=ハイティング= コルモゴロフ解釈(BHK 解釈)(英語版))と関係している。
x {\displaystyle \lambda x.\lambda y.x} と λ x . λ y . y {\displaystyle \lambda x.\lambda y.y} で名前付けられた論理式 α → α → α {\displaystyle \alpha \to \alpha \to \alpha } が属していたならば、右辺ではこれらを区別するが、左辺ではこれを同じものと見做す。
ハワードは他の論理の結合子と単純型付きラムダ項の他の構成との間に対応を拡張できることを示した。例えば論理積との対応は次に示す表のようになる:
もっと抽象的に見ればこの対応は次の表として纏められる。とりわけ、ラムダ計算における正規形の概念は自然演繹におけるプラヴィッツの正規な証明に対応する。型付けられたラムダ項は正規形を持つという結果(正規化定理)は、自然演繹の無矛盾性や論理和分離特性の証明に利用できる。型の具体性の問題の決定手続きを直観主義的な証明可能性の決定手続きに変換できる。
ハワードの対応は自然演繹およびラムダ計算の拡張に対しても自然に延長できる。網羅的ではないがここに列挙しておく:
ジラールとレイノルズのSystem F:2階の命題論理と多相ラムダ計算
高階述語論理とジラールのSystem Fω
帰納型と代数的データ型
様相論理における必然性様相 ◻ {\displaystyle \Box } とstaged computation
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.
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 .
最近ではカリー=ハワード対応が遺伝的プログラミングにおける探索空間のパーティションを定義する方法として提案されている。この手法は遺伝子型(システムにより進化するプログラムの木)の集合に対して(種と呼ばれる)カリー=ハワード対応する証明を索引付ける。
↑ Davies, Rowan; Pfenning, Frank (2001), “A Modal Analysis of Staged Computation”, Journal of the ACM 48 (3): 555–604, doi:10.1145/382780.382785, http://www.cs.cmu.edu/~fp/papers/jacm00.pdf
↑ Pfenning, Frank; Davies, Rowan (2001), “A Judgmental Reconstruction of Modal Logic”, Mathematical Structures in Computer Science 11: 511–540, doi:10.1017/S0960129501003322, http://www.cs.cmu.edu/~fp/papers/mscs00.pdf
↑ Komori, Yuichi; Cho, Arato (2010), λρ-calculus, p. 11, http://komoriyuichi.web.fc2.com/symposium/lambda-rho5.pdf
Griffin, Timothy G. (1990), “The Formulae-as-Types Notion of Control”, Conf. Record 17th Annual ACM Symp.