カリー・ハワード書簡

プログラミング言語理論と証明理論において、カリー・ハワード対応とは、コンピュータプログラムと数学的証明との間の直接的な関係である。これは、カリー・ハワード同型性または同値性、あるいは証明をプログラムとして、命題または式を型として解釈する解釈としても知られている。

これは、アメリカの数学者ハスケル・カリーと論理学者ウィリアム・アルヴィン・ハワードによって初めて発見された、形式論理と計算のシステム間の統語 的類似性の一般化である。^[1]これは通常、カリーとハワードに帰せられる論理と計算のつながりであるが、そのアイデアは、LEJブラウワー、アーレント・ヘイティング、アンドレイ・コルモゴロフ（ブラウワー・ヘイティング・コルモゴロフ解釈を参照）^[2]およびスティーブン・クリーネ（実現可能性を参照）によって様々な定式化で与えられた直観論理の操作的解釈に関連している。この関係は、3方向のカリー・ハワード・ランベック対応として圏論を含むように拡張されている。^{[3] [4] [5]}

カリーとハワードの書簡の始まりは、いくつかの観察にあります。

1. 1934年にカリーは、コンビネータの型は直観主義的含意論理の公理体系として見ることができると指摘した。^[6]
2. 1958年に彼は、ヒルベルト型演繹システムと呼ばれるある種の証明システムが、組み合わせ論理として知られる計算の標準モデルの型付き断片とある部分で一致することを観察した。^[7]
3. 1969年にハワードは、自然演繹と呼ばれる別のより「高レベル」な証明システムが、その直観主義バージョンでは、ラムダ計算として知られる計算モデルの型付き変種として直接解釈できることを観察しました。^[8]

カリー・ハワード対応とは、証明システムと計算モデルの間に同型性があるという観察です。これは、これら 2 つの形式主義ファミリーは同一であるとみなせるという主張です。

いずれかの形式主義の特殊性を抽象化すると、次のような一般化が起こります。証明とはプログラムであり、証明する式はプログラムの型です。より非公式には、これは、関数の戻り値の型（つまり、関数によって返される値の型）が、関数に渡される引数値の型に対応する仮定に従う論理定理に類似していること、およびその関数を計算するプログラムは、その定理の証明に類似していることを述べた類推として見ることができます。これにより、論理プログラミングの形式が厳密な基礎の上に設定されます。証明はプログラムとして、特にラムダ項として表現することができ、証明は実行することができます。

この対応関係は、その発見以来、広範囲にわたる新たな研究の出発点となっており、特に、証明システムとしても型付き関数型プログラミング言語としても動作するように設計された新しい種類の形式体系につながっています。これには、Martin-Löfの直観主義型理論とCoquandの構成計算が含まれます。これら 2 つの計算では、証明が通常の議論の対象であり、証明の特性を任意のプログラムと同様に述べることができます。この研究分野は通常、現代型理論と呼ばれています。

カリー・ハワードパラダイムから派生したこのような型付きラムダ計算により、プログラムとして見られる証明を形式化し、チェックし、実行できる Coqのようなソフトウェアが生まれました。

逆の方向としては、証明の正しさを前提として、プログラムを使用して証明を抽出するというものがあります。これは、証明付きコードと密接に関連する研究分野です。これは、プログラムが記述されているプログラミング言語が非常に豊富な型付けを備えている場合にのみ実行可能です。このような型システムの開発は、カリー・ハワード対応を実際に関連性のあるものにしたいという願いによって部分的に動機付けられてきました。

カリー・ハワード対応は、カリーとハワードの元の研究で扱われていなかった証明概念の計算内容に関する新たな疑問も提起しました。特に、古典論理は、プログラムの継続を操作する能力と、名前による呼び出しと値による呼び出しとして知られる2 つの評価戦略間の二重性を表現するシーケント計算の対称性に対応することが示されました。

終了しないプログラムを書く可能性があるため、チューリング完全な計算モデル（任意の再帰関数を持つ言語など）は、対応関係を単純に適用すると矛盾したロジックにつながるため、慎重に解釈する必要があります。論理的な観点から任意の計算を処理する最善の方法は、現在も活発に議論されている研究課題ですが、人気のあるアプローチの 1 つは、モナドを使用して、終了する可能性の低いコードから終了することが証明できるコードを分離するというものです（このアプローチは、はるかに豊富な計算モデルにも一般化され、^[9]カリー–ハワード同型性^{[ext 1]の自然な拡張によって様相論理に関連付けられています）。}完全関数型プログラミングによって提唱されているより急進的なアプローチは、無制限の再帰を排除し（チューリング完全性を放棄しますが、依然として高い計算複雑性を保持します）、終了しない動作が実際に必要な場合は常に、より制御されたコアカージョンを使用することです。

より一般的な定式化では、カリー・ハワード対応は、形式的な証明計算と計算モデルの型システムとの間の対応です。特に、この対応は 2 つの対応に分かれます。1 つは、特定の証明システムまたは計算モデルが考慮されているかどうかに依存しない式と型のレベルの対応であり、もう 1 つは、今回は、考慮されている証明システムと計算モデルの特定の選択に固有の 証明とプログラムのレベルの対応です。

式と型のレベルでは、対応関係は、含意は関数型、論理積は「積」型 (言語によってはタプル、構造体、リスト、またはその他の用語と呼ばれる)、論理和は和型 (この型はユニオンと呼ばれる)、偽の式は空の型、真の式は単位型 (その唯一のメンバーはヌル オブジェクト) と同じように動作することを示しています。量指定子は、従属関数空間または積 (適切な場合) に対応します。これは次の表にまとめられています。

証明システムと計算モデルのレベルでは、対応は主に、第一にヒルベルトスタイルの演繹システムと組合せ論理として知られるシステムの特定の定式化の間、そして第二に自然演繹とラムダ計算として知られるシステムの特定の定式化の間における構造の同一性を示します。

自然演繹システムとラムダ計算の間には、次のような対応関係があります。

1958 年に Curry と Feys が組み合わせ論理について書いた本には、当初は単純な記述がありました。組み合わせ論理の基本コンビネータ K と S の最も単純な型は、驚くべきことに、ヒルベルト スタイルの演繹システムで使用されるそれぞれの公理スキーム α → ( β → α ) と ( α → ( β → γ )) → (( α → β ) → ( α → γ )) に対応していました。このため、これらのスキームは現在では公理 K と S と呼ばれることがよくあります。ヒルベルト スタイルの論理で証明として見られるプログラムの例を以下に示します。

含意的直観主義的断片に限定すると、ヒルベルトのスタイルで論理を形式化する簡単な方法は次のようになります。Γ を仮説として考えられる式の有限集合とします。すると、δ はΓ から導出可能であり、Γ ⊢ δ と表記され、次のケースで表されます。

• δは仮説であり、Γの式である。
• δ は公理スキームのインスタンスです。つまり、最も一般的な公理システムでは次のようになります。
  • δ の形式はα → ( β → α )、または
  • δ の形式は ( α → ( β → γ )) → (( α → β ) → ( α → γ ))、
• δ は演繹によって導かれる。つまり、あるαに対して、α → δとαは両方とも Γ からすでに導出可能である（これはmodus ponensの規則である）。

これは、次の表の左の列のように、 推論規則を使用して形式化できます。

型付き組み合わせ論理は、同様の構文を使用して定式化できます。Γ を、型が注釈された変数の有限集合とします。項 T (これも型が注釈されています) は、次の場合にこれらの変数に依存します [Γ ⊢ T: δ ]:

• TはΓの変数の1つであり、
• T は基本的なコンビネータです。つまり、最も一般的なコンビネータの基底の下では、
  • TはK: α → ( β → α ) [ここでαとβは引数の型を表す]、または
  • T は S:( α → ( β → γ )) → (( α → β ) → ( α → γ ))、
• T は、Γ 内の変数に依存する 2 つの部分項の合成です。

ここで定義される生成規則は、以下の右の列に示されています。Curry のコメントは、両方の列が 1 対 1 に対応していることを単に述べています。直観主義論理への対応の制限は、パースの法則(( α → β ) → α ) → αなどのいくつかの古典的な トートロジーが対応から除外されること を意味します。

より抽象的なレベルで見ると、この対応は次の表のように言い換えることができます。特に、ヒルベルト型論理に特有の演繹定理は、組み合わせ論理の抽象除去のプロセスと一致しています。

対応のおかげで、組み合わせ論理の結果をヒルベルト スタイルの論理に転送することができ、その逆も可能です。たとえば、組み合わせ論理の項の簡約の概念はヒルベルト スタイルの論理に転送することができ、証明を同じステートメントの他の証明に標準的に変換する方法を提供します。通常の項の概念を通常の証明の概念に転送して、公理の仮説をすべて切り離す必要がないことを表現することもできます (そうしないと、単純化が発生する可能性があるため)。

逆に、直観主義論理におけるパースの法則の非証明可能性は、組み合わせ論理に転用することができる。組み合わせ論理には、型で型付け可能な型付き項は存在しない。

(( α → β ) → α ) → α。

いくつかのコンビネータや公理の集合の完全性に関する結果も転送できる。例えば、コンビネータXが（外延的）コンビネーション論理の1点基底​​を構成するという事実は、単一の公理スキームが

((( α → ( β → γ )) → (( α → β ) → ( α → γ ))) → (( δ → ( ε → δ )) → ξ )) → ξ、

これはXの主たる型であり、公理スキームの組み合わせの適切な代替である。

α → ( β → α ) および

( α → ( β → γ )) → (( α → β ) → ( α → γ ))。

カリーが直観主義ヒルベルトスタイルの演繹と型付き組合せ論理との構文上の対応を強調した後、ハワードは1969 年に単純型付きラムダ計算のプログラムと自然演繹の証明との構文上の類似性を明確にした。以下では、左辺は直観主義含意自然演繹を暗黙の弱化を伴うシークエント計算として形式化し(シークエントの使用は、演繹規則をより明確に述べることができるため、カリー - ハワード同型性の議論では標準的である)、右辺はラムダ計算の型付け規則を示す。左辺の Γ、Γ ₁ 、および Γ _{2 は}式の順序付きシーケンスを表し、右辺の Γ 1、および Γ 2 は、名前がすべて異なる名前付き (つまり、型付き) 式のシーケンスを表す。

対応を言い換えると、 Γ ⊢ α を証明することは、 Γ にリストされている型の値が与えられたときに、型αのオブジェクトを作成するプログラムを持つことを意味します。公理/仮説は、新しい制約のない型の新しい変数の導入に対応し、→  I規則は関数の抽象化に対応し、→  E規則は関数の適用に対応します。コンテキスト Γ が式の集合であると見なされる場合、対応は正確ではないことに注意してください。たとえば、型α → α → αの λ 項 λ x .λ y . xと λ x .λ y . y は、対応では区別されません。以下に例を示します。

ハワードは、この対応が論理の他の接続子や単純型付きラムダ計算の他の構成にも拡張されることを示した。抽象レベルで見ると、この対応は次の表のようにまとめられる。特に、ラムダ計算の正規形の概念が自然演繹におけるプラウィッツの正規演繹の概念と一致することも示しており、そこから、型居住問題のアルゴリズムは直観的証明可能性を決定するアルゴリズムに変換できることがわかる。

ハワードの対応は、自然演繹と単純型付きラムダ計算の他の拡張に自然に拡張されます。以下は網羅的ではないリストです。

• ジラール・レイノルズシステムFは、二階命題論理と多態的ラムダ計算の共通言語として、
• 高階論理とジラールのシステム_Fω
• 代数的データ型としての帰納的型
• 様相論理と段階的計算における必要性^{[ext 2]}${\displaystyle \Box }$
• 様相論理とモナド型における効果の可能性^{[ext 1]}${\displaystyle \Diamond }$
• λI計算（抽象化はλx.Eに制限され、xはE内で少なくとも1つの自由出現を持つ）_とCLI計算は_関連論理に対応する。^[10]
• グロタンディーク位相幾何学における局所真理（∇）様相、またはそれと同等のベントン、ビアマン、デ・パイヴァ（1998）の「緩い」様相（◯）は、「計算型」を記述するCL論理に対応する。^[11]

カリーの時代、そしてハワードの時代にも、証明をプログラムとして対応付けるのは直観主義論理、すなわち特にパースの法則が演繹できない論理のみでした。パースの法則への対応、ひいては古典論理への対応の拡張は、与えられたプログラム実行の評価コンテキストを捕捉し、この評価コンテキストを後で再インストールできるようにする型付け演算子に関するグリフィンの研究から明らかになりました。古典論理に対する基本的なカリー–ハワードスタイルの対応を以下に示します。古典的証明を直観主義論理にマッピングするために使用される二重否定変換と、制御を含むラムダ項を純粋なラムダ項にマッピングするために使用される継続渡しスタイルの変換との対応に注意してください。より具体的には、名前呼び出し継続渡しスタイルの翻訳はKolmogorovの二重否定翻訳に関連し、値呼び出し継続渡しスタイルの翻訳は Kuroda による一種の二重否定翻訳に関連します。

古典論理をパースの法則のような公理を追加するのではなく、シークエントで複数の結論を許容することによって定義すると、より細かいカリー・ハワード対応が古典論理に対して存在する。古典的な自然演繹の場合には、パリゴのλμ計算の型付きプログラムとの証明としてのプログラム対応が存在する。

証明とプログラムとの対応は、ゲンツェンのシーケント計算として知られる形式論では解決できるが、ヒルベルト式や自然演繹の場合のように、明確に定義された既存の計算モデルとは対応していない。

シークエント計算は、左導入規則、右導入規則、および削除可能なカット規則の存在によって特徴付けられます。シークエント計算の構造は、いくつかの抽象マシンの構造に近い計算に関連しています。非公式な対応は次のとおりです。

NG de Bruijn は定理チェッカーAutomathの証明を表現するためにラムダ記法を使用し、命題をその証明の「カテゴリ」として表現しました。これは 1960 年代後半、Howard が原稿を書いた時期と同時期のことでした。de Bruijn はおそらく Howard の研究を知らず、独自に対応を述べました (Sørensen & Urzyczyn [1998] 2006、pp 98–99)。一部の研究者は Curry–Howard 対応の代わりに Curry–Howard–de Bruijn 対応という用語を使用する傾向があります。

BHK解釈は直観主義的証明を関数として解釈しますが、解釈に関連する関数のクラスを指定しません。この関数のクラスにラムダ計算を採用すると、BHK 解釈はハワードの自然演繹とラムダ計算の対応と同じことを示します。

クリーネの再帰的実現可能性は、直観主義的算術の証明を再帰関数のペアと、再帰関数が「実現する」、つまり、式が真になるように初期式の選言と存在量指定子を正しくインスタンス化することを表現する式の証明に分割します。

クライゼルの修正実現可能性は、直観主義の高階述語論理に適用され、証明から帰納的に抽出された単純に型付けされたラムダ項が最初の式を実現することを示しています。命題論理の場合、これはハワードの声明と一致します。抽出されたラムダ項は証明そのものであり (型付けされていないラムダ項として見られる)、実現可能性声明は、抽出されたラムダ項が式が意味する型を持つという事実 (型として見られる) の言い換えです。

ゲーデルの弁証法解釈は、計算可能な関数による直観主義的算術（の拡張）を実現します。自然演繹の場合でも、ラムダ計算との関連は不明です。

ヨアヒム・ランベックは1970 年代初頭に、直観主義命題論理の証明と型付き組合せ論理のコンビネータが共通の等式理論、すなわちデカルト閉圏理論を共有していることを示した。カリー・ハワード・ランベック対応という表現は、現在では一部の人々^{[誰によって? ]}によって、直観主義論理、型付きラムダ計算、デカルト閉圏の関係を示すために使用されている。この対応では、デカルト閉圏の対象は命題 (型) として解釈でき、射は一連の仮定 (型付けコンテキスト) を有効な帰結 (適切に型付けされた項) にマッピングする演繹として解釈できる。^[12]

ランベックの対応は、ベータ削減や項正規化などの計算のダイナミクスを抽象化した等式理論の対応であり、カリーの対応やハワードの対応の場合のように構造の統語的同一性の表現ではありません。つまり、カルティシアン閉圏における明確に定義された射の構造は、ヒルベルトスタイルの論理や自然演繹における対応する判断の証明の構造と比較できません。たとえば、射が正規化されていることを述べたり証明したり、チャーチ・ロッサー型の定理を確立したり、「強く正規化」するカルティシアン閉圏について語ったりすることはできません。この区別を明確にするために、カルティシアン閉圏の基礎となる統語的構造を以下で言い換えます。

オブジェクト（命題/型）には以下が含まれます

• ${\displaystyle \top }$オブジェクトとして
• および がオブジェクトとして与えられた場合、および がオブジェクトとして与えられます。${\displaystyle \alpha }$${\displaystyle \beta }$${\displaystyle \alpha \times \beta }$${\displaystyle \alpha \rightarrow \beta }$

モルフィズム（演繹/用語）には以下が含まれる

• アイデンティティ:${\displaystyle {\text{id}}_{\alpha }:\alpha \to \alpha }$
• 合成:とが射であれば、は射である${\displaystyle t:\alpha \to \beta }$${\displaystyle u:\beta \to \gamma }$${\displaystyle u\circ t:\alpha \to \gamma }$
• 終端射:${\displaystyle \star _{\alpha }:\alpha \to \top }$
• 積:と が射ならば、は射である${\displaystyle t:\alpha \to \beta }$${\displaystyle u:\alpha \to \gamma }$${\displaystyle (t,u):\alpha \to \beta \times \gamma }$
• 予測：そして${\displaystyle \pi _{\alpha ,\beta ,1}:\alpha \times \beta \to \alpha }$${\displaystyle \pi _{\alpha ,\beta ,2}:\alpha \times \beta \to \beta }$
• 評価：${\displaystyle {\text{eval}}_{\alpha ,\beta }:(\alpha \to \beta )\times \alpha \to \beta }$
• カリー化: が射であれば、 は射です。${\displaystyle t:\alpha \times \beta \to \gamma }$${\displaystyle \lambda t:\alpha \to \beta \to \gamma }$

上記の注釈と同様に、任意のカルティシアン閉カテゴリ内の明確に定義された射（型付けされた項）は、次の型付け規則に従って構築できます。通常のカテゴリカル射記法は、型付けコンテキスト記法に置き換えられます。 ${\displaystyle f:\alpha \to \beta }$${\displaystyle \alpha \vdash f:\beta }$

身元：

${\displaystyle {\frac {}{\alpha \vdash {\text{id}}:\alpha }}}$

構成：

${\displaystyle {\frac {\alpha \vdash t:\beta \qquad \beta \vdash u:\gamma }{\alpha \vdash u\circ t:\gamma }}}$

ユニットタイプ（端末オブジェクト）:

${\displaystyle {\frac {}{\alpha \vdash \star :\top }}}$

デカルト積:

${\displaystyle {\frac {\alpha \vdash t:\beta \qquad \alpha \vdash u:\gamma }{\alpha \vdash (t,u):\beta \times \gamma }}}$

左と右の投影:

${\displaystyle {\frac {}{\alpha \times \beta ~\vdash ~\pi _{1}:\alpha }}\qquad {\frac {}{\alpha \times \beta ~\vdash ~\pi _{2}:\beta }}}$

カレー作り：

${\displaystyle {\frac {\alpha \times \beta ~\vdash ~t:\gamma }{\alpha \vdash \lambda t:\beta \to \gamma }}}$

応用：

${\displaystyle {\frac {}{(\alpha \rightarrow \beta )\times \alpha \vdash {\text{eval}}:\beta }}}$

最後に、このカテゴリーの方程式は

• ${\displaystyle {\text{id}}\circ t=t}$
• ${\displaystyle t\circ {\text{id}}=t}$
• ${\displaystyle (v\circ u)\circ t=v\circ (u\circ t)}$
• ${\displaystyle \star ={\text{id}}}$ （正しく入力されている場合）
• ${\displaystyle \star \circ u=\star }$
• ${\displaystyle \pi _{1}\circ (t,u)=t}$
• ${\displaystyle \pi _{2}\circ (t,u)=u}$
• ${\displaystyle (\pi _{1},\pi _{2})=id}$
• ${\displaystyle (t_{1},t_{2})\circ u=(t_{1}\circ u,t_{2}\circ u)}$
• ${\displaystyle {\text{eval}}\circ (\lambda t\circ \pi _{1},\pi _{2})=t}$
• ${\displaystyle \lambda {\text{eval}}={\text{id}}}$
• ${\displaystyle \lambda t\circ u=\lambda (t\circ (u\circ \pi _{1},\pi _{2}))}$

これらの方程式は次の法則を意味します。 ${\displaystyle \eta }$

• ${\displaystyle (\pi _{1}\circ t,\pi _{2}\circ t)=t}$
• ${\displaystyle \lambda ({\text{eval}}\circ (t\circ \pi _{1},\pi _{2}))=t}$

ここで、 t が存在し、iff は含意直観論理で証明可能です。 ${\displaystyle \alpha _{1}\times \ldots \times \alpha _{n}\vdash t:\beta }$${\displaystyle \alpha _{1},\ldots ,\alpha _{n}\vdash \beta }$

カリー・ハワード対応のおかげで、型が論理式に対応する型付き式は、その式の証明に類似しています。次に例を示します。

例として、定理α → αの証明を考えてみましょう。ラムダ計算では、これは恒等関数I = λ x . xのタイプであり、組み合わせ論理では、恒等関数はS = λ fgx . fx ( gx ) をK = λ xy . xに 2 回適用することで得られます。つまり、I = (( S K ) K )です。証明の説明として、これは、次の手順を使用してα → αを証明できることを示しています。

• 式α、β → αおよびαを使用して 2 番目の公理スキームをインスタンス化し、( α → (( β → α ) → α )) → (( α → ( β → α )) → ( α → α ) の証明を取得します。 ）、
• 最初の公理スキームをαとβ → αで一度インスタンス化して、 α → (( β → α ) → α )の証明を得る。
• 最初の公理スキームをαとβでもう一度インスタンス化して、α → ( β → α )の証明を得る。
• α → αの証明を得るためにモーダスポネンスを2回適用する

一般に、プログラムに形式 ( P Q ) のアプリケーションが含まれている場合は、次の手順に従う必要があります。

1. まず、 PとQの型に対応する定理を証明します。
2. P はQに適用されているので、 Pの型はα → β の形式を持ち、 Qの型は何らかのαとβに対してα の形式を持つ必要があります。したがって、モーダスポネンス規則を介して結論β を切り離すことが可能です。

より複雑な例として、 B関数に対応する定理を見てみましょう。B の型は( β → α ) → ( γ → β ) → γ → αです。Bは( S ( K S ) K )と同等です。これが、定理( β → α ) → ( γ → β ) → γ → αの証明のロードマップです。

最初のステップは、( K S ) を構築することです。K 公理の前提を S 公理のようにするには、αを( α → β → γ ) → ( α → β ) → α → γに等しく設定し、βをδに等しくします(変数の衝突を避けるため)。

K  : α → β → α

K [ α = ( α → β → γ ) → ( α → β ) → α → γ , β = δ] : (( α → β → γ ) → ( α → β ) → α → γ ) → δ → ( α → β → γ ) → ( α → β ) → α → γ

ここでの前件はSだけなので、後件は Modus Ponens を使用して切り離すことができます。

KS  : δ → ( α → β → γ ) → ( α → β ) → α → γ

これは ( K S )の型に対応する定理です。この式にSを適用します。S を次のように とります。

S  : ( α → β → γ ) → ( α → β ) → α → γ、

α = δ、β = α → β → γ、およびγ = ( α → β ) → α → γとすると、次のようになります。

S [ α = δ , β = α → β → γ , γ = ( α → β ) → α → γ ] : ( δ → ( α → β → γ ) → ( α → β ) → α → γ ) → ( δ → ( α → β → γ )) → δ → ( α → β ) → α → γ

そして結論を​​切り離します:

S (KS)  : ( δ → α → β → γ ) → δ → ( α → β ) → α → γ

これは ( S ( K S ) )の型の式です。この定理の特別なケースはδ = ( β → γ )です。

S (KS) [ δ = β → γ ] : (( β → γ ) → α → β → γ ) → ( β → γ ) → ( α → β ) → α → γ

この最後の式はKに適用する必要があります。K を再度特殊化しますが、今回はα を( β → γ )に、β をαに置き換えます。

K  : α → β → α

K [ α = β → γ , β = α ] : ( β → γ ) → α → ( β → γ )

これは前の式の前提と同じなので、結論を切り離すと次のようになります。

S (KS) K  : ( β → γ ) → ( α → β ) → α → γ

変数αとγの名前を入れ替えると、

( β → α ) → ( γ → β ) → γ → α

それが証明すべき残りの部分でした。

以下の図は、自然演繹における( β → α ) → ( γ → β ) → γ → αの証明と、それが λ 式λ a .λ b .λ g .( a ( b g )としてどのように解釈できるかを示しています。 ))タイプ( β → α ) → ( γ → β ) → γ → α。

                                     a:β → α、b:γ → β、g:γ ⊢ b : γ → β a:β → α、b:γ → β、g:γ ⊢ g : γ
————————————————————————————————————————————————— ————————————————————————————————————————————————— ———
a:β → α、b:γ → β、g:γ ⊢ a : β → α a:β → α、b:γ → β、g:γ ⊢ bg : β
————————————————————————————————————————————————— —————————————————————
               a:β → α、b:γ → β、g:γ ⊢ a (bg) : α
               ———————————————————————————————————
               a:β → α、b:γ → β ⊢ λ g. a (bg) : γ → α
               ———————————————————————————————————————
                        a:β → α ⊢ λ b. λ g. a (bg) : (γ → β) → γ → α
                        ———————————————————————————————————
                                ⊢ λ a. λ ｂ． λ g. a (bg) : (β → α) → (γ → β) → γ → α

最近、同型性は遺伝的プログラミングにおける探索空間の分割を定義する方法として提案されました。^[13]この方法は、遺伝子型（GPシステムによって進化したプログラムツリー）のセットを、そのカリー・ハワード同型証明（種と呼ばれる）によってインデックス付けします。

INRIAの研究ディレクターであるバーナード・ラングが指摘したように、 ^[14]カリー・ハワード対応はソフトウェアの特許性に反する議論を構成します。アルゴリズムは数学的な証明であるため、前者の特許性は後者の特許性を意味します。定理は私有財産である可能性があり、数学者はそれを使用するのに料金を支払い、それを販売するが証明を秘密にし、誤りに対する責任を拒否する会社を信頼する必要があります。

ここで挙げた対応関係は、さらに遠く深いものとなる。例えば、デカルト閉圏は、閉モノイド圏によって一般化される。これらの圏の内部言語は、線型論理に対応する線型システムであり、これは、単純に型付けされたラムダ計算をデカルト閉圏の内部言語として一般化する。さらに、これらは、弦理論で重要な役割を果たすコボルディズム^[15]に対応することが示される。

同値の拡張セットはホモトピー型理論でも探求されている。ここでは、型理論はユニバレンシー公理（「同値は等値と同値である」）によって拡張され、これによりホモトピー型理論はすべての数学（集合論や古典論理を含む、選択公理やその他の多くのことを議論する新しい方法を提供する）の基礎として使用できる。つまり、証明は居住型の要素であるというカリー・ハワード対応は、証明のホモトピック同値の概念に一般化される（空間内のパスとして、型理論の恒等型または等値型はパスとして解釈される）。^[16]

• カリー、 HB (1934-09-20)。「組み合わせ論理における機能性」。米国科学アカデミー紀要。20 (11  ) : 584–90。Bibcode : 1934PNAS ... 20..584C。doi : 10.1073 / pnas.20.11.584。ISSN 0027-8424。PMC 1076489。PMID 16577644  。 
• カリー、ハスケル B; フェイズ、ロバート (1958)。クレイグ、ウィリアム (編)。組み合わせ論理。論理と数学の基礎の研究。第 1 巻。ノースホランド出版会社。LCCN a59001593  。クレイグ、ウィリアムによる 2 つのセクションを含む。パラグラフ 9E を参照。{{cite book}}: CS1 maint: postscript (link)
• De Bruijn, Nicolaas (1968)、「Automath、数学のための言語」、アイントホーフェン工科大学数学部、TH レポート 68-WSK-05。2 ページの解説付きで改訂され、Automation and Reasoning、第 2 巻、Classical papers on computeal logic 1967–1970、Springer Verlag、1983 年、159 ～ 200 頁に再録。
• Howard, William A. (1980 年 9 月) [1969 年の原稿]、「構築の型としての式の概念」(PDF)、Seldin, Jonathan P.、Hindley, J. Roger (編)、『To HB Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism』、Academic Press、pp. 479–490、ISBN 978-0-12-349050-6。

• Griffin, Timothy G. (1990)、「制御の型としての式の概念」、Conf. Record 17th Annual ACM Symp. on Principles of Programming Languages、POPL '90、サンフランシスコ、カリフォルニア州、米国、1990 年 1 月 17 ～ 19 日、pp. 47 ～ 57、doi :10.1145/96709.96714、ISBN 978-0-89791-343-0、S2CID  3005134。
• パリゴ、ミシェル (1992)、「ラムダミュー計算: 古典的自然演繹のアルゴリズム的解釈」、国際論理プログラミングおよび自動推論会議: LPAR '92 議事録、ロシア、サンクトペテルブルク、コンピュータサイエンスの講義ノート、第 624 巻、Springer-Verlag、pp. 190–201、ISBN 978-3-540-55727-2。
• Herbelin, Hugo (1995)、「Gentzen スタイルのシークエント計算構造と同型のラムダ計算構造」、Pacholski, Leszek、Tiuryn, Jerzy (編)、Computer Science Logic、第 8 回国際ワークショップ、CSL '94、ポーランド、カジミエシュ、1994 年 9 月 25 ～ 30 日、Selected Papers、Lecture Notes in Computer Science、vol. 933、Springer-Verlag、pp. 61 ～ 75、ISBN 978-3-540-60017-6。
• Gabbay, Dov; de Queiroz, Ruy (1992)。 「 Curry-Howard 解釈の線形論理、関連論理、およびその他のリソース論理への拡張」。Journal of Symbolic Logic。Vol . 57。Association for Symbolic Logic。pp. 1319–1365。doi :10.2307/2275370。JSTOR  2275370。S2CID 7159005  。（ヘルシンキで開催されたLogic Colloquium '90で発表された論文の完全版。要約はJSL 56(3):1139–1140、1991に掲載。）
• de Queiroz, Ruy; Gabbay, Dov (1994)、「ラベル付き演繹システムにおける等式と命題等式の機能的解釈」、Dekker, Paul; Stokhof, Martin (編)、第 9 回アムステルダム コロキウム議事録、ILLC/アムステルダム大学哲学部、pp. 547–565、ISBN 978-90-74795-07-4。
• de Queiroz, Ruy; Gabbay, Dov (1995)、「存在量指定子の機能的解釈」、純粋および応用論理学の関心グループの紀要、第 3 巻、pp. 243–290（ウプサラのLogic Colloquium '91で発表された論文の完全版。要約はJSL 58(2):753–754、1993に掲載。）
• de Queiroz, Ruy; Gabbay, Dov (1997)、「様相必然性の機能的解釈」、de Rijke, Maarten (編)、Advances in Intensional Logic、Applied Logic Series、vol. 7、Springer-Verlag、pp. 61–91、ISBN 978-0-7923-4711-8。
• de Queiroz, Ruy; Gabbay, Dov (1999)、「ラベル付き自然演繹」、Ohlbach, Hans-Juergen、Reyle, Uwe (編)、『論理、言語、推論。Dov Gabbay を讃えて』、Trends in Logic、第 7 巻、Kluwer、pp. 173–250、ISBN 978-0-7923-5687-5。
• de Oliveira, Anjolina; de Queiroz, Ruy (1999)、「ラベル付き自然演繹の等式フラグメントの正規化手順」、純粋および応用論理の利益団体の論理ジャーナル、第 7 巻、オックスフォード大学出版局、pp. 173–215（第2回WoLLIC'95 、レシフェで発表された論文の完全版。Journal of the Interest Group in Pure and Applied Logics 4(2):330–332、1996年の抄録。）
• ポエルノモ、イマン、クロスリー、ジョン、ウィルシング、マーティン（2005）、プログラムとしての証明の適応：カリー・ハワード・プロトコル、コンピュータサイエンスのモノグラフ、シュプリンガー、ISBN 978-0-387-23759-6は、著者らが Curry-Howard プロトコルと呼ぶ方法を介して、プログラムとしての証明によるプログラム合成を粗粒度および命令型プログラム開発問題に適用することに関するものです。コンピュータ サイエンスの観点から見た Curry-Howard 対応についての議論も含まれています。
• de Queiroz, Ruy JGB; de Oliveira, Anjolina (2011)、「直接計算の機能的解釈」、Electronic Notes in Theoretical Computer Science、269、Elsevier : 19–40、doi : 10.1016/j.entcs.2011.03.003（ブラジルのナタールで開催されたLSFA 2010で発表された論文の完全版。 ）

• de Queiroz, Ruy JGB (1994)、「正規化と言語ゲーム」、Dialectica、48 (2): 83–123、doi :10.1111/j.1746-8361.1994.tb00107.x、JSTOR  42968904(初期バージョンはLogic Colloquium '88、パドヴァで発表されました。要約はJSL 55:425、1990に掲載されています。)
• de Queiroz, Ruy JGB (2001)、「意味、機能、目的、有用性、結果 - 相互に関連する概念」、純粋および応用論理の興味グループの論理ジャーナル、第 9 巻、693 ～ 734 ページ（ 1989 年 8 月 13 日から 20 日までキルヒベルク/ヴェクセルで開催された第 14 回国際ウィトゲンシュタインシンポジウム（100 周年記念）で発表された初期バージョン。 ）
• de Queiroz, Ruy JGB (2008)、「還元規則、使用としての意味、証明理論的意味論について」、Studia Logica、90 (2): 211–247、doi :10.1007/s11225-008-9150-5、S2CID  11321602。

• De Bruijn、Nicolaas Govert (1995)、「数学における型の役割について」(PDF)、Groote、Philippe de (編)、De Groote 1995、pp. 27–54、de Bruijn 自身による寄稿。
• Geuvers, Herman (1995)、「構成と高階論理の計算」、De Groote 1995、pp. 139–191には、Curry-Howard 対応の総合的な紹介が含まれています。
• Gallier, Jean H. (1995)、「証明とラムダ項の対応について」(PDF)、De Groote 1995、pp. 55–138 、 2017年7月5日のオリジナル(PDF)からアーカイブには、Curry-Howard 対応の総合的な紹介が含まれています。
• Wadler, Philip (2014)、「命題としての型」(PDF)、Communications of the ACM、58 (12): 75–84、doi :10.1145/2699407、S2CID  11957500

• デ・グルーテ、フィリップ編（1995）、「The Curry–Howard Isomorphism」、Cahiers du Centre de Logique (Université catholique de Louvain)、vol. 8、アカデミア-ブリュイラン、ISBN 978-2-87209-363-2は、Curry-Feys と Howard の重要な論文、de Bruijn の論文、およびその他のいくつかの論文を再現します。
• Sørensen, Morten Heine; Urzyczyn, Paweł (2006) [1998], Lectures on the Curry–Howard isomorphism , Studies in Logic and the Foundations of Mathematics, vol. 149, Elsevier Science , CiteSeerX  10.1.1.17.7385 , ISBN 978-0-444-52077-7証明理論と型理論に関するノート。カリー・ハワード対応の提示を含み、特に式と型の対応に焦点を当てている。
• ジャン=イヴ・ジラール（1987-1990）「証明と型」、ケンブリッジ理論計算機科学論文集、第7巻、イヴ・ラフォンとポール・テイラーの翻訳と付録、ケンブリッジ大学出版局、ISBN 0-521-37181-3、2008-04-18にオリジナルからアーカイブ、カリー・ハワード対応の提示を伴う証明理論に関するノート。
• トンプソン、サイモン（1991）、型理論と関数型プログラミング、アディソン・ウェズレー、ISBN 0-201-41667-0。
• ポエルノモ、イマン、クロスリー、ジョン、ウィルシング、マーティン（2005）、プログラムとしての証明の適応：カリー・ハワード・プロトコル、コンピュータサイエンスのモノグラフ、シュプリンガー、ISBN 978-0-387-23759-6は、著者らが Curry-Howard プロトコルと呼ぶ方法を介して、プログラムとしての証明によるプログラム合成を粗粒度および命令型プログラム開発問題に適用することに関するものです。コンピュータ サイエンスの観点から見た Curry-Howard 対応についての議論も含まれています。
• Binard, F.; Felty, A. (2008)、「多態型と高階関数による遺伝的プログラミング」(PDF)、遺伝的および進化的計算に関する第 10 回年次会議の議事録、Association for Computing Machinery、pp. 1187–94、doi :10.1145/1389095.1389330、ISBN 9781605581309、S2CID  3669630
• de Queiroz, Ruy JGB; de Oliveira, Anjolina G.; Gabbay, Dov M. (2011)、論理的演繹の機能的解釈、Advances in Logic、第 5 巻、Imperial College Press/World Scientific、ISBN 978-981-4360-95-1。

• ジョンストン、PT (2002)、「D4.2 λ-計算とデカルトの閉カテゴリ」、スケッチの象、トポス理論概要、第 2 巻、クラレンドン プレス、pp. 951–962、ISBN 978-0-19-851598-2—カリー・ハワード対応において「何が起こるか」についてのカテゴリカルな見解を示します。

• ハワード・オン・カリー・ハワード
• ハスケルにおけるカリー・ハワード通信
• モナドリーダー 6: 古典の世界への冒険: ハスケルにおけるカリー・ハワード、ピアスの法則。