プログラムとして書かれた証明:自然数の加法に関する交換律のCoqによる証明。correspondence)とは、プログラミング言語理論と証明論において、計算機プログラムと証明との間の直接的な対応関係のことである。「プログラム=証明」(proofs-as-programs)・「型=命題」(formulae-as-types)などとしても知られる。これはアメリカの数学者ハスケル・カリーと論理学者ウィリアム・アルヴィン・ハワードにより最初に発見された形式論理の体系とある種の計算の体系との構文論的なアナロジーを一般化した概念である。通常はこの論理と計算の関連性はカリーとハワードに帰属される。このアイデアはブラウワー、ハイティング、コルモゴロフらが定式化した直観主義論理の操作的解釈の一種と関係している。外部リンク一般的な定式化[編集]もっと一般的な観点からいえば、カリー=ハワード対応は証明計算と計算模型の型システムとの間の対応である。これは2つの対応に分けられる。ひとつは、論理式と型のレベルであり、これは特定の証明体系や計算模型の選択に依存しない。いまひとつは、形式的証明とプログラムのレベルであり、これは証明体系や計算模型の選択に依存する。論理式と型のレベルにおいて、この対応によれば、含意は関数型、論理積は直積型(タプル、構造体、リストなど、言語によって様々に呼ばれる)、論理和は直和型(バリアント、共用体、Eitherなど)、偽は空な型、真はシングルトン型のように振る舞うという。量化子は依存直積または直和にそれぞれ対応する。0}証明体系と計算模型のレベルにおいて、この対応は主に構造的な同一性を示す。ひとつはヒルベルト流の推論体系とコンビネータ論理、いまひとつはゲンツェンの自然演繹とラムダ計算との間の同一性である。))}とにそれぞれ対応するのである。ヒルベルト流の証明と見做せるプログラムの例が与えられる(後述)。直観主義論理の含意断片に制限するならば、次のようにヒルベルト流の極めて簡明な形式化が存在する。}を論理式の有限集合として、これを仮定と見做す。}から導出可能である。これは推論規則を用いて形式化できる。以下に示す表の左の列を参照されたい。我々は同様の構文により型付きコンビネータ論理を形式化することができる。}を次の形式の有限集合(ただし同じ変数に異なる型が紐付けられてはならない)として、これを変数の型宣言と見做す。型付きCL項の構成規則は以下に示す表の右の列を参照されたい。カリーは各々の行が同型に対応していることを指摘した。}などがこの対応から締め出されていることを意味する。}}{\text{Application}}}もっと抽象的なレベルから見ると、この対応は以下の表のようにして述べ直すことができる。ヒルベルト流の推論体系における演繹定理(のメタ証明)は、コンビネータ論理における抽象の除去手続きと対応している。除去この対応によって、コンビネータ論理の結果をヒルベルト流の推論体系の結果に翻訳できる。その逆もまた同様である。CL項の簡約はヒルベルト流の証明図の簡約手続きと見ることができる。正規なCL項は正規な証明図へと翻訳される。ここで正規とは、これ以上簡約できないことを意味する。正規化定理は型付け可能なCL項は必ず正規形を持つという定理であるが、これはヒルベルト流の証明図は必ず正規形を持つという結果に翻訳できる。}を持つCL項は存在しない。コンビネータからなる集合の完全性の結果もまた翻訳できる。X}は任意のCL項を表現できることが知られている。X}の可能な型で代入に関して極小なもの)である。))}自然演繹とラムダ計算との間の対応[編集]ハスケル・カリーがヒルベルト流の体系とコンビネータ論理の構文的対応を強調した後、ウィリアム・アルヴィン・ハワードは1969年に単純型付きラムダ計算と自然演繹との構文的な同型性を明確にした。含意断片を形式化し、右辺でラムダ計算の型付け規則を示す。_{2}}で順序付けられた論理式の列を表す。右辺ではラムダ項で名前付けられた論理式の列を表す。}を持つオブジェクトを構成することに対応する。規則は関数適用に対応する。}を単なる論理式の集合と見做す(暗黙の縮約と弱化を認める)ならば、この対応は正確ではないことが分かる。}が属していたならば、右辺ではこれらを区別するが、左辺ではこれを同じものと見做す。ハワードは他の論理の結合子と単純型付きラムダ項の他の構成との間に対応を拡張できることを示した。_{i}}}}もっと抽象的に見ればこの対応は次の表として纏められる。ラムダ計算における正規形の概念は自然演繹におけるプラヴィッツの正規な証明に対応する。型付けられたラムダ項は正規形を持つという結果(正規化定理)は、自然演繹の無矛盾性や論理和分離特性の証明に利用できる。型の具体性の問題の決定手続きを直観主義的な証明可能性の決定手続きに変換できる。type)ハワードの対応は自然演繹およびラムダ計算の拡張に対しても自然に延長できる。lax様相(○)は計算型を記述するCL論理と対応する。[2][3]ハワードの対応はまた自然演繹およびラムダ計算の制限に対しても成り立つ。BCKλ計算とBCK論理の対応が挙げられる。ラムダ項であると制限することにより得られる項書換え系である。これにより自由変数の複数回の使用が禁止される。したがってこの体系は1つの仮定を複数回使用する(縮約規則)ことを禁止するBCK論理と対応する。ラムダ項であると制限することにより得られる体系はBCI論理と対応する。これにより未使用の変数の束縛が禁止される。したがってこの体系は縮約規則に加えて未使用の仮定を解消する(弱化規則)ことを禁止するBCI論理と対応する。古典論理と制御演算子との間の対応[編集]カリーおよびハワードの時代では、「証明=プログラム」対応は専ら直観主義論理においてのみ考察されていた。ここでの論理では、とくにパースの法則は導出不能であった。パースの法則すなわち古典論理を含む明確な対応の拡張はグリフィンの仕事による。グリフィンはプログラムの実行における評価文脈(継続)をキャプチャしそれを再度使用するような制御演算子を持つラムダ計算が古典論理と対応することを指摘した。基本的な古典論理のカリー=ハワード対応は以下で与えられる。古典論理の証明から直観論理の証明への変換(グリベンコの定理)に用いられる二重否定変換は、制御演算子を持つラムダ項から純粋なラムダ項へのCPS変換に対応する。具体的にいえば、名前呼びCPS変換はコルモゴロフの二重否定変換に、値呼びCPS変換は黒田の二重否定変換に関係する。}継続呼び出し二重否定変換CPS変換パースの法則の代りにシークエントの結論に複数の論理式を許容することのよっても古典論理の自然演繹を定義できる。この場合もやはり対応が成立する。Parigotのλμ計算の間に「証明=プログラム」の対応が存在する。シークエント計算[編集]「証明=プログラム」対応はゲンツェンのシークエント計算においても確立されるが、ヒルベルト流の体系や自然演繹のように、既に知られていたような計算模型との対応関係は存在しない。ならびに除去可能なカット規則により特徴づけられる。シークエント計算の構造はある種の抽象機械の構造に似ている。