カリー＝ハワード同型対応
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.)
カリーおよびハワードの時代では、「証明=プログラム」対応は専ら直観主義論理においてのみ考察されていた。すなわち、ここでの論理では、とくにパースの法則は導出不能であった。パースの法則すなわち古典論理を含む明確な対応の拡張はグリフィンの仕事による。グリフィンはプログラムの実行における評価文脈(継続)をキャプチャしそれを再度使用するような制御演算子を持つラムダ計算が古典論理と対応することを指摘した。基本的な古典論理のカリー=ハワード対応は以下で与えられる。なお、古典論理の証明から直観論理の証明への変換(グリベンコの定理)に用いられる二重否定変換は、制御演算子を持つラムダ項から純粋なラムダ項へのCPS変換に対応する。もっと具体的にいえば、名前呼びCPS変換はコルモゴロフの二重否定変換に、値呼びCPS変換は黒田の二重否定変換に関係する。
パースの法則の代りにシークエントの結論に複数の論理式を許容することによっても古典論理の自然演繹を定義できる。この場合もやはり対応が成立する。例えばある種の古典論理の自然演繹とM. Parigotのλμ計算の間に「証明=プログラム」の対応が存在する。
簡単な例として α → α {\displaystyle \alpha \to \alpha } のヒルベルト流の証明を構成する。ラムダ計算では、これは恒等関数 I = λ x . x {\displaystyle I=\lambda x.x} の型であり、コンビネータ論理では恒等関数は S {\displaystyle S} と K {\displaystyle K} により I = S K K {\displaystyle I=SKK} (ただし慣例によって適用は左結合と見做す)と表現できる。以上の説明は α → α {\displaystyle \alpha \to \alpha } の証明の構成を与えている。実際、この論理式は次のようにしてヒルベルト流の証明体系にて証明可能である(慣例に従い含意記号は右結合と見做す):
この論理式の最初の部分 δ → α → β → γ {\displaystyle \delta \to \alpha \to \beta \to \gamma } と公理 K : α → β → α {\displaystyle K:\alpha \to \beta \to \alpha } とが同一になるような代入を求めれば、それは δ = β → γ {\displaystyle \delta =\beta \to \gamma } であるから、
K : ( β → γ ) → α → β → γ {\displaystyle K:(\beta \to \gamma )\to \alpha \to \beta \to \gamma }
S ( K S ) : ( ( β → γ ) → α → β → γ ) → ( β → γ ) → ( α → β ) → α → γ {\displaystyle S(KS):((\beta \to \gamma )\to \alpha \to \beta \to \gamma )\to (\beta \to \gamma )\to (\alpha \to \beta )\to \alpha \to \gamma }
最後にこれらにモーダス・ポネンスを適用すれば次を得る:
S ( K S ) K : ( β → γ ) → ( α → β ) → α → γ {\displaystyle S(KS)K:(\beta \to \gamma )\to (\alpha \to \beta )\to \alpha \to \gamma }
適当に命題変数の名前を付け替えれば所望の論理式の証明が得られる。
δ {\displaystyle \delta } は公理図式の代入例である、すなわち: δ {\displaystyle \delta } は α → ( β → α ) {\displaystyle \alpha \to (\beta \to \alpha )} の形をしているか、 δ {\displaystyle \delta } は ( α → ( β → γ ) ) → ( ( α → β ) → ( α → γ ) ) {\displaystyle (\alpha \to (\beta \to \gamma ))\to ((\alpha \to \beta )\to (\alpha \to \gamma ))} の形をしている、
δ {\displaystyle \delta } は推論により得られる、すなわち、ある α {\displaystyle \alpha } について α {\displaystyle \alpha } と α → δ {\displaystyle \alpha \to \delta } が Γ {\displaystyle \Gamma } から導出可能である。
これは推論規則を用いて形式化できる。以下に示す表の左の列を参照されたい。
我々は同様の構文により型付きコンビネータ論理を形式化することができる。いま Γ {\displaystyle \Gamma } を次の形式の有限集合(ただし同じ変数に異なる型が紐付けられてはならない)として、これを変数の型宣言と見做す。
x : α {\displaystyle x:\alpha } ここで x {\displaystyle x} は変数、 α {\displaystyle \alpha } は型
もっと一般的な観点からいえば、カリー=ハワード対応は証明計算と計算模型の型システムとの間の対応である。これは2つの対応に分けられる。ひとつは、論理式と型のレベルであり、これは特定の証明体系や計算模型の選択に依存しない。いまひとつは、形式的証明とプログラムのレベルであり、これは証明体系や計算模型の選択に依存する。
論理式と型のレベルにおいて、この対応によれば、含意は関数型、論理積は直積型(タプル、構造体、リストなど、言語によって様々に呼ばれる)、論理和は直和型(バリアント、共用体、Eitherなど)、偽は空な型、真はシングルトン型のように振る舞うという。量化子は依存直積または直和にそれぞれ対応する。
まとめると、次のような表になる:
証明体系と計算模型のレベルにおいて、この対応は主に構造的な同一性を示す。ひとつはヒルベルト流の推論体系とコンビネータ論理、いまひとつはゲンツェンの自然演繹とラムダ計算との間の同一性である。
自然演繹とラムダ計算との間には次のような対応関係が存在する:
x\,(yz):\gamma \rightarrow \alpha }}}{\dfrac {\lambda y.\lambda z.x\,(yz):(\gamma \rightarrow \beta )\rightarrow \gamma \rightarrow \alpha }{\lambda x.\lambda y.\lambda z.x\,(yz):(\beta \rightarrow \alpha )\rightarrow (\gamma \rightarrow \beta )\rightarrow \gamma \rightarrow \alpha }}}}
この証明が型付きラムダ項 λ x . λ y . λ z . x ( y z ) {\displaystyle \lambda x.\lambda y.\lambda z.x(yz)} と解釈できることは明らかである。なお、前述の ( β → α ) → ( γ → β ) → γ → α {\displaystyle (\beta \to \alpha )\to (\gamma \to \beta )\to \gamma \to \alpha } のヒルベルト流の証明は、自然演繹におけるこの証明に対して抽象の除去とη変換を何度か使用することで得られる。