柯里-霍華德同構

柯里-霍華德對應（英語：Curry-Howard correspondence）是在電腦程式和數學證明之間的緊密聯繫；這種對應也叫做柯里-霍華德同構、公式為類型對應或命題為類型對應。這是對形式邏輯系統和公式計算（computational calculus）之間符號的相似性的推廣。它被認為是由美國數學家哈斯凱爾·柯里和邏輯學家威廉·阿爾文·霍瓦德（William Alvin Howard）獨立發現的。

對應的起源、範圍和結論[編輯]

對應可以在兩個層面上看到，首先是類比層次，它聲稱對一個函數計算出的值的類型的斷言可類比於一個邏輯定理，計算這個值的程序可類比於這個定理的證明。在理論計算機科學中，這是連接λ演算和類型論的毗鄰領域的一個重要的底層原理。它被經常以下列形式陳述為「證明是程序」。一個可選擇的形式化為「命題為類型」。其次，更加正式的，它指定了在兩個數學領域之間的同構，就是以一種特定方式形式化的自然演繹和簡單類型λ演算之間是雙射，首先是證明和項，其次是證明歸約步驟和beta歸約。

有多種方式考慮柯里-霍華德對應。在一個方向上，它工作於「把證明編譯為程序」級別上。這裏的「證明」最初被限定為在構造性邏輯中—典型的是直覺邏輯系統中的證明。而「程序」是在常規的函數式編程的意義上的；從語法的觀點上看，這種程序是用某種λ演算表達的。所以柯里-霍華德同構的具體實現是詳細研究如何把來自直覺邏輯的證明寫成λ項。（這是霍華德的貢獻；柯里貢獻了組合子，它是相對於是高級語言的λ演算是能寫所有東西的機器語言）。最近，同樣處理經典邏輯的柯里-霍華德對應的擴展可被公式化了，通過對經典有效規則比如雙重否定除去和皮爾士定律關聯上明確的用續體比如call/cc處理的一類項。

還有一個相反的方向，對一個程序的正確性關聯上「證明提取」的可能性。這在非常豐富的類型論環境中是可行的。實際上理論家對推進非常豐富類型的函數式程式語言的開發的動機，已經部分地混合了希望帶給柯里-霍華德對應更加顯著的地位的因素。

類型[編輯]

依據λ演算，我們將使用λx.E來指示帶有形式參數x和函數體E的函數。在應用於參數比如a的時候，這個函數生成E，並帶有x的所有自由出現都被替換為a。有效的λ演算表達式有如下形式之一：

v（這裏的v是個變量）
λv.E（這裏的v是個變量，而E是個λ演算表達式）
(E F)（這裏的E和F是λ演算表達式）

通常我們將縮寫(（A B）C)為(A B C)，縮寫λa.λb.E為λab.E。一個表達式被稱為是「閉合的」，如果它不包含自由變量。

類型確定規則[編輯]

類型可以依賴於類型變量，它被指示為小寫的希臘字母α, β等等。在我們概念中類型變量是被隱含的全稱量化的，就是說，如果一個值有包括類型變量的一個類型，則它必須由這個類型變量的所有可能實例組成。我們可以定義任意表達式的類型為如下：

一個變量比如x可以有任意類型。
如果變量x有類型α，而表達式E有類型β，則λx.E有指示為α→β的類型；就是說，它是取類型α的值，並映射到類型β的值。
在表達式(E F)中，如果F有類型α，則E必須有類型α→β（就是說它必須是期望類型α的參數的函數）並且這個表達式有類型β。

例如，考慮函數K = λa.λb.a。假定a有類型α而b有類型β。則λb.a有類型 β→α，而λa.λb.a有類型α→(β→α)。我們接受→是右結合的約定，所以這個類型也可以寫為α→β→α。這意味着K函數接受類型α的參數並返回一個函數，它接受類型β的參數並返回類型α的值。

類似的，考慮函數B = λa.λb.λc.(a (b c))。假定c有類型γ，則b必須有形如γ→β的某種類型，表達式(b c)有類型β。a必須有形如β→α的某種類型，表達式(a (b c))有類型α。那麼λc.(a (b c))有類型γ→α；λb.λc.(a (b c))有類型(γ→β)→γ→α，而λa.λb.λc.(a (b c))有類型(β→α)→(γ→β)→γ→α。你可以把這解釋為意味着B函數接受類型(β→α)的參數和類型(γ→β)的參數並返回一個函數，它接受類型γ的參數並返回類型α的結果。

類型居留問題[編輯]

很明顯λ-表達式可以有非常複雜的類型。你可能要問是否有帶有給定類型的λ-表達式。找到帶有特定類型的λ-表達式的問題叫做類型居留問題。

答案是非常引人注目的：有帶有特定類型的閉合λ-表達式，若且唯若這個類型對應於一個邏輯定理，在這裏的→符號再次解釋為意味着邏輯蘊涵的時候。

例如，考慮恆等函數λx.x，它接受類型ξ的參數並返回類型ξ的結果，所以有類型ξ→ξ。ξ→ξ當然是邏輯定理：給定一個公式ξ，你可以結論出ξ。

K函數的類型α→β→α也是一個定理。如果已知α為真，則你可以結論出如果β為真就能推出α。這有時也叫做重複規則。B的類型是 (β→α)→(γ→β)→γ→α。你可類似的把它解釋為邏輯重言式；如果已知(β→α)為真，則如果已知(γ→β)為真，你就能推出γ蘊涵α。

在另一方面，考慮α→β，它不是定理。明顯的沒有這種類型的λ-項；它必定是接受類型α的參數並返回某個完全無關的和未約束類型的結果的函數。這是不可能的，因為你不能從這種函數裏得到什麼東西，除非把它放到其他什麼地方之中。

儘管有類型β→(α→α)的函數（比如，λb.λa.a，它接受一個參數b，忽略參數，並返回恆等函數），卻沒有類型(α→α)→β的函數，如果存在的話，它會是轉換恆等函數到任意值的函數。

直覺邏輯[編輯]

儘管所有居留類型對應於邏輯定理為真，逆命題卻不為真。即使我們限制我們的嘗試到只包含→運算的邏輯公式，所謂的邏輯的蘊涵片段，不是所有經典有效的邏輯公式是居留類型。例如，類型((α→β)→α)→α是非居留的，儘管叫做皮爾士定律的對應邏輯公式是重言式。

直覺邏輯是比經典邏輯弱的系統。經典邏輯把自身關注於在抽象的、柏拉圖主義意義上為真的公式，而直覺邏輯只在可以為它構造一個證明的時候認為公式為真。公式α ∨ ¬α示例了這種區別；它是經典邏輯的一個定理而不是直覺邏輯的定理。儘管它是經典的真的，在直覺邏輯中這個公式斷言了我們要麼證明α要麼證明¬α。因為我們不是總能做到這些事情之一，它不是直覺邏輯的一個定理。

在居留類型和有效邏輯公式之間的對應完全是雙向的，如果我們限制我們的注意力到直覺邏輯的蘊涵片段（這也叫做希爾伯特代數）。

希爾伯特演繹系統和組合子邏輯的對應[編輯]

形式上刻畫直覺邏輯的一個簡單方式是希爾伯特演繹系統。它有兩個公理模式。所有形式為

α→β→α

的公式都是公理，所有形式為

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

的公式都是公理。

唯一的演繹規則是肯定前件，它聲稱如果我們已經證明了兩個定理，一個有形式α→β而另一個有形式α，我們可以結論出β也是定理。以這種方式推導出來的公式的集合正好是直覺邏輯的集合。特別的是，皮爾士定律不能以這種方式演繹。（對皮爾士定律不能以這種方式演繹的證明請參見海廷代數條目）。

如果我們增加皮爾士定律為第三個公理模式，這個系統就有能力證明在經典邏輯的蘊涵片段中的所有定理。

考慮λ-表達式的下列兩個函數：

K: λxy.x

S: λxyz.(x z (y z))

可以證明任何函數都可以通過適當的K和S相互應用來建立。（有關證明請參見組合子邏輯）。例如，上面定義的函數B等價於(S(K S)K)。如果一個函數比如B，可以表達為S和K的複合，則這個表達式可以直接轉換成類型B的一個證明，它被解釋為邏輯公式，是直覺邏輯的一個定理。本質上，K的外觀對應於第一個公理模式的使用，S的外觀對應於第二個公理模式的使用，而函數應用對應於肯定前件演繹規則的使用。

第一個公理模式是α→β→α，並且它精確的是K函數的類型；類似的第二個公理模式(α→β→γ)→(α→β)→α→γ，是S函數的類型。肯定前件聲稱如果我們有兩個表達式，一個類型是α→β（就是說，接受類型α的值並返回類型β的值）而另一個類型是α（就是說，類型α的值），則我們應當能夠找到類型β的值；明顯的，我們可以通過應用這個函數到這個值之上來得到；結果會有類型β。

希爾伯特式直覺蘊含邏輯	簡單類型的組合子邏輯
${\frac {}{\Gamma _{1},\alpha ,\Gamma _{2}\vdash \alpha }}Assum$	${\frac {}{\Gamma _{1},x:\alpha ,\Gamma _{2}\vdash x:\alpha }}$
${\frac {}{\Gamma \vdash \alpha \rightarrow (\beta \rightarrow \alpha )}}Ax_{1}$	${\frac {}{\Gamma \vdash K:\alpha \rightarrow (\beta \rightarrow \alpha )}}$
${\frac {}{\Gamma \vdash (\alpha \!\rightarrow \!(\beta \!\rightarrow \!\gamma ))\!\rightarrow \!((\alpha \!\rightarrow \!\beta )\!\rightarrow \!(\alpha \!\rightarrow \!\gamma ))}}Ax_{2}$	${\frac {}{\Gamma \vdash S:(\alpha \!\rightarrow \!(\beta \!\rightarrow \!\gamma ))\!\rightarrow \!((\alpha \!\rightarrow \!\beta )\!\rightarrow \!(\alpha \!\rightarrow \!\gamma ))}}$
${\frac {\Gamma \vdash \alpha \rightarrow \beta \qquad \Gamma \vdash \alpha }{\Gamma \vdash \beta }}{\textit {Modus~Ponens}}$	${\frac {\Gamma \vdash E_{1}:\alpha \rightarrow \beta \qquad \Gamma \vdash E_{2}:\alpha }{\Gamma \vdash E_{1}\;E_{2}:\beta }}$

證明α→α[編輯]

作為一個簡單的例子，我們將構造定理α→α的證明。這是恆等函數I = λx.x的類型。函數((S K)K)等價於恆等函數。作為對證明的描述，它聲稱了我們需要首先應用S到K。我們做如下：

α→β→α

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

如果我們在S中設γ = α，我們得到：

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

因為這個公式的前件(α→β→α)是一個已知定理，並且實際上正好是K，我們可以應用肯定前件並推導出後件：

(α→β)→α→α

這是函數(S K)的類型。現在我們需要應用這個函數到K。我們再次操縱公式使得前件看起來像K，這次我們替代β為(β→α):

(α→β→α)→α→α

我們再次應用肯定前件來推出後件：

α→α

我們完成了。

一般的說，這個過程是只要程序包含形如(P Q)的應用，我們應當首先證明對應於P和Q的類型的定理。因為P要被應用於Q，對於某種α和β，P的類型必定有形式α→β而Q的類型必定有形式α。我們可以通過肯定前件規則推出β。

證明 (β→α)→(γ→β)→γ→α[編輯]

作為一個更加複雜的例子，我們看對應於函數B的定理的證明。B的類型是(β→α)→(γ→β)→γ→α。B等價於(S(K S)K)。這是對證明定理(β→α)→(γ→β)→γ→α的指引。

首先我們需要構造(K S)。我要使K公理的前件看起來像S公理，通過設置α等於(α→β→γ)→(α→β)→α→γ，和β等於δ:

α→β→α

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

因為前件正好是S，我們可以推出後件：

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

這是對應於(K S)的定理。現在我們要應用S到這個表達式。取得S

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

我們設置α = δ，β = (α→β→γ)和γ = ((α→β)→α→γ)，生成

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

我們可以接着推出後件：

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

這是類型(S(K S))的公式。這個定理的一個特殊情況有δ = (β→γ):

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

我們需要應用最後這個公式到K。我們再次特殊化K，這次是替代α為(β→γ)，替代β為α:

α→β→α

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

這同於前者公式的前件，所以我們推出後件：

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

交換變量α和γ的名字得到

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

這就是我們要證明的。

自然演繹和lambda演算的對應[編輯]

在下表第一列中的推導規則定義了直覺蘊涵自然演繹（為蘊涵連結詞準備一個介入和一個除去規則）的標準系統。在第二列中給出 $\lambda$ -演算的標準類型指派（賦值）系統。

直覺蘊涵自然演繹	lambda演算類型指派規則
${{} \over \Gamma ,\alpha \vdash \alpha }\quad {\rm {(Ax)}}$	${{} \over \Gamma ,x{:}\alpha \vdash x:\alpha }\quad {\rm {(Ax)}}$
${\Gamma ,\alpha \vdash \beta \over \Gamma \vdash \alpha \rightarrow \beta }\quad (\rightarrow {\rm {I}})$	${\Gamma ,x{:}\alpha \vdash E:\beta \over \Gamma \vdash \lambda x.E:\alpha \rightarrow \beta }\quad (\rightarrow {\rm {I}})$
${\Gamma \vdash \alpha \rightarrow \beta \qquad \Gamma \vdash \alpha \over \Gamma \vdash \beta }\quad (\rightarrow {\rm {E}})$	${\Gamma \vdash E:\alpha \rightarrow \beta \qquad \Gamma \vdash F:\alpha \over \Gamma \vdash (E\ F):\beta }\quad (\rightarrow {\rm {E}})$

相繼式演算[編輯]

希爾伯特式證明是很難構造的。證明邏輯定理的更加直覺的方式是根岑的相繼式演算。相繼式演算以同希爾伯特式證明對應於組合子表達式一樣的方式對應於λ-表達式程序。

直覺邏輯的蘊涵片段的相繼式演算規則是：

{{} \over \Gamma ,\alpha \vdash \alpha }

(公理)

{\Gamma ,\alpha \vdash \beta  \over \Gamma \vdash \alpha \rightarrow \beta }

(Right →)

{\Gamma \vdash \alpha \qquad \qquad \Sigma ,\beta \vdash \gamma  \over \Gamma ,\Sigma ,\alpha \rightarrow \beta \vdash \gamma }

(Left →)

Γ表示上下文，它是假設的集合。 $\Gamma \vdash a$ 指示假定上下文Γ我們可以證明a。邏輯定理完全由其證明不需要假設的那些公式t組成的；就是說，t是一個定理，若且唯若我們可以證明 $\vdash t$ 。詳情請參見相繼式演算。

在相繼式演算中的證明是樹，它的根是我們要證明的定理，而它的葉子是公理模式實例；每個內部節點必須標記為要麼Right →要麼Left →，並且必須包含依據指定規則從子節點推出的一個公式。

相繼式演算證明緊密的對應於λ-演算表達式。斷言 $\Gamma \vdash a$ 可以被解釋為意味着，給定帶有在Γ中列出類型的值，我們可以製造帶有類型a的一個值。公理對應於帶有新的無約束的類型的新變量介入。

Right →規則對應於函數抽象：

{\Gamma ,\alpha \vdash \beta  \over \Gamma \vdash \alpha \rightarrow \beta }

(Right →)

什麼時候我們能結論出某個程序Γ包含類型α→β的函數?在Γ加上類型α的一個值的時候，包含了足夠的機械來允許我們製造類型β的一個值。

Left →規則對應於函數應用：

{\Gamma \vdash \alpha \qquad \Sigma ,\beta \vdash \gamma  \over \Gamma ,\Sigma ,\alpha \rightarrow \beta \vdash \gamma }

(Left →)

如果我們可以製造類型α的一個值，並且如果給出類型β的一個值，我們還可以製造類型γ的一個值，則類型α→β的一個函數將允許我們製造類型γ的一個值：首先我們可以製造α，接着應用α→β函數於它，並接着使用結果的β值來製造類型γ的一個值。

例子[編輯]

例如，(β→α)→(γ→β)→γ→α的相繼式演算如下：

{\cfrac {\gamma \vdash \gamma \qquad {\cfrac {\beta \vdash \beta \qquad \alpha \vdash \alpha }{\beta ,\beta \rightarrow \alpha \vdash \alpha }}Left\rightarrow }{\qquad {\cfrac {\gamma ,\beta \rightarrow \alpha ,\gamma \rightarrow \beta \vdash \alpha }{\qquad {\cfrac {\beta \rightarrow \alpha ,\gamma \rightarrow \beta \vdash \gamma \rightarrow \alpha }{\qquad {\cfrac {\beta \rightarrow \alpha \vdash (\gamma \rightarrow \beta )\rightarrow \gamma \rightarrow \alpha }{\vdash (\beta \rightarrow \alpha )\rightarrow (\gamma \rightarrow \beta )\rightarrow \gamma \rightarrow \alpha }}Right\rightarrow }}Right\rightarrow }}Right\rightarrow }}Left\rightarrow

(β→α)→(γ→β)→γ→α的證明告訴我們如何製造帶有這個類型的一個λ-表達式。首先，介入分別帶有類型α和β的變量a和b。Left →規則聲稱製造程序 (λb.a b)，它構造類型α的一個值。我們再次使用Left →來構造(λb.a (λg.b g))，它仍有類型α。

參見[編輯]

引用[編輯]

開創性引用[編輯]

Curry, Haskell, Functionality in Combinatory Logic, Proceedings of the National Academy of Sciences 20: 584–590, 1934 .

Curry, Haskell B.; Feys, Robert, Combinatory Logic Vol. I, William Craig, Amsterdam: North-Holland, 1958 , 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., The formulae-as-types notion of construction, Seldin, Jonathan P.; Hindley, J. Roger (編), to H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, Boston, MA: Academic Press: 479–490, 1980年9月 [1969], ISBN 978-0-12-349050-6 (original manuscript from 1969).

對應的擴展[編輯]

Griffin, Timothy G., 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: 47–57, 1990 .

Parigot, Michel, 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: 190–201, 1992, ISBN 978-3-540-55727-2 .

Herbelin, Hugo, A Lambda-Calculus Structure Isomorphic to Gentzen-Style Sequent Calculus Structure, Pacholski, Leszek (編), Computer Science Logic, 8th International Workshop, CSL '94, Kazimierz, Poland, September 25-30, 1994, Selected Papers, Lecture Notes in Computer Science 933, Springer-Verlag: 61–75, 1995, ISBN 978-3-540-60017-6 Editors list列表中的|first2=缺少|last2= (幫助).

Gabbay, Dov; de Queiroz, Ruy, Extending the Curry-Howard interpretation to linear, relevant and other resource logics, Journal of Symbolic Logic 57: 1319–1365, 1992 . (Full version of the paper presented at Logic Colloquium '90, Helsinki. Abstract in JSL 56(3):1139-1140, 1991.)

de Queiroz, Ruy; Gabbay, Dov, Equality in Labelled Deductive Systems and the Functional Interpretation of Propositional Equality, Dekker, Paul; Stokhof, Martin (編), Proceedings of the Ninth Amsterdam Colloquium, ILLC/Department of Philosophy, University of Amsterdam: 547–565, 1994, ISBN 9074795072 .

de Queiroz, Ruy; Gabbay, Dov, The Functional Interpretation of the Existential Quantifier, Bulletin of the Interest Group in Pure and Applied Logics 3(2–3): 243–290, 1995 . (Full version of a paper presented at Logic Colloquium '91, Uppsala. Abstract in JSL 58(2):753-754, 1993.)

de Queiroz, Ruy; Gabbay, Dov, The Functional Interpretation of Modal Necessity, de Rijke, Maarten (編), Advances in Intensional Logic, Applied Logic Series 7, Springer-Verlag: 61–91, 1997, ISBN 978-0-7923-4711-8 .

de Oliveira, Anjolina; de Queiroz, Ruy, A Normalization Procedure for the Equational Fragment of Labelled Natural Deduction, Logic Journal of the Interest Group in Pure and Applied Logics 7(2), Oxford Univ Press: 173–215, 1999 . (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.)

綜合性論文[編輯]

De Bruijn, Nicolaas Govert, On the roles of types in mathematics (PDF), Groote, Philippe de (編), The Curry-Howard isomorphism, Cahiers du Centre de logique (Université catholique de Louvain) 8, Academia-Bruyland: 27–54, [2008-08-28], ISBN 978-2-87209-363-2, （原始內容存檔 (PDF)於2021-03-06） , the contribution of de Bruijn by himself.

Geuvers, Herman, The Calculus of Constructions and Higher Order Logic, Groote, Philippe de (編), The Curry-Howard isomorphism, Cahiers du Centre de logique (Université catholique de Louvain) 8, Academia-Bruyland: 139–191, ISBN 978-2-87209-363-2 , contains a synthetic introduction to the Curry-Howard correspondence.

Gallier, Jean H., On the Correspondence between Proofs and Lambda-Terms (PDF), Groote, Philippe de (編), The Curry-Howard isomorphism, Cahiers du Centre de logique (Université catholique de Louvain) 8, Academia-Bruyland: 55–138, ISBN 978-2-87209-363-2 , contains a synthetic introduction to the Curry-Howard correspondence.

書籍[編輯]

De Groote, Philippe (編), The Curry-Howard Isomorphism, Cahiers du Centre de Logique (Université catholique de Louvain) 8, Academia-Bruylant, 1995, 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ł, Lectures on the Curry-Howard isomorphism, Studies in Logic and the Foundations of Mathematics 149, Elsevier Science, 2006 [1998], ISBN 978-0-44452-077-7 , 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.

外部連結[編輯]

Thompson, Simon (1991). Type Theory and Functional Programming （頁面存檔備份，存於互聯網檔案館） Addison-Wesley. ISBN 0-201-41667-0.