命题为类型原理

**柯里 - 霍華德對應**（英語：**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** 函數的類型。肯定前件聲稱如果我們有兩個表達式，一個類型是 α→β（就是說，接受類型 α 的值並返回類型 β 的值）而另一個類型是 α（就是說，類型 α 的值），則我們應當能夠找到類型 β 的值；明顯的，我們可以通過應用這個函數到這個值之上來得到；結果會有類型 β。

### 證明 α→α

作為一個簡單的例子，我們將構造定理 α→α 的證明。這是恆等函數 **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 $ - 演算的標準類型指派（賦值）系統。

## 相繼式演算

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

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

　
: ${{} \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))，它仍有類型 α。

## 參見

* 直覺主義
* BHK 釋義
* 直覺類型論
* 經典邏輯
* 中間邏輯
* 線性邏輯
* 構造性證明
* Curry-Howard 對應
* 可計算性邏輯
* 博弈語義

## 引用

### 開創性引用

* 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  .
* 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], ISBN978-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.