柯里-霍華德同構

Curry-Howard 同構顯示了推理系統和程序語言之間的相似性 ^[1]  ，類型即命題，程序即證明。或表示了計算機程序與數理邏輯之間的直接聯繫(邏輯上的等價關係)，即我們可以利用數理邏輯中的某些東西來去表示程序中的特定邏輯。

在此框架下：程序語言的語言構造同構為推理系統的推理規則、程序的類型同構為邏輯命題、閉合程序（不依賴環境的程序）可以同構為一條定理的證明過程，其類型就是一條定理以及邏輯上下文同構為自由變量類型指派。例如Lambda 演算同構為 Gentzen 的自然演繹：

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

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

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

程序語言是用來定義計算機指令執行流程的形式化語言。每種程序語言都包含一整套詞彙和語法規範。這些規範通常包括數據類型和數據結構、指令類型和指令控制、調用機制和庫函數以及不成文的規定(如遞進書寫、變量命名等) ^[2]  。每一種程序設計語言可以被看作是一套包含語法、詞彙和含義的正式規範。這些規範通常包括：數據和數據結構、指令及流程控制、引用機制和重用以及設計哲學。語法是説明編程語言中，哪些符號或文字的組合方式是正確的，語義則是對於編程的解釋。

數學上的證明包括兩個不同的概念。首先是非形式化的證明：一種以自然語言寫成的嚴密論證，用來説服聽眾或讀者去接受某個定理或論斷的真確性。由於這種證明使用了自然語言，因此對於非形式化證明在嚴謹性上的標準，將取決於聽眾或讀者對課題的理解程度。非形式化證明在大多數的應用場合中出現，例如科普講座、口頭辯論、初等教育或高等教育的某些部分。有時候非形式化的證明被稱作“正式的”，但這只是強調其中論證的嚴謹性。而當邏輯學家使用“正式證明”一詞時，指的是另一種完全不同的證明——形式化證明。

在數理邏輯中，形式化證明並不是以自然語言書寫，而是以形式化的語言書寫：這種語言包含了由一個給定的字母表中的字符所構成的字符串。而證明則是一種由該些字符串組成的有限長度的序列。這種定義使得人們可以談論嚴格意義上的“證明”，而不涉及任何邏輯上的模糊之處。研究證明的形式化和公理化的理論稱為證明論。儘管理論上來説，每個非形式化的證明都可以轉化為形式化證明，但實際中很少會這樣做。對形式化證明的研究主要應用在探討關於可證明性的一般性質，或説明某些命題的不可證明性等等。

依據

演算，我們將使用

來指示帶有形式參數x和函數體

的函數。在應用於參數比如

的時候，這個函數生成E，並帶有x的所有自由出現都被替換為

。有效的

演算表達式有如下形式之一：

1、

（這裏的

是個變量）

2、

（這裏的是

個變量，而E是個演算表達式）

3、(

)（這裏的

和F是

演算表達式）

通常我們將縮寫(

)為(

)，縮寫

為

。一個表達式被稱為是“閉合的”，如果它不包含自由變量。

類型可以依賴於類型變量，它被指示為小寫的希臘字母

,

等等。在我們概念中類型變量是被隱含的全稱量化的，就是説，如果一個值有包括類型變量的一個類型，則它必須由這個類型變量的所有可能實例組成。我們可以定義任意表達式的類型為如下：

1、一個變量比如

可以有任意類型。

2、如果變量有類型

，而表達式

有類型

，則

有指示為的類型；就是説，它是取類型

的值，並映射到類型

的值。

3、在表達式(

)中，如果F有類型

，則E必須有類型

（就是説它必須是期望類型的參數的函數）並且這個表達式有類型

。

例如，考慮函數

。假定

有類型

而b有類型

。則

有類型

，而

有類型

(

)。我們接受→是右結合的約定，所以這個類型也可以寫為

。這意味着K函數接受類型α的參數並返回一個函數，它接受類型β的參數並返回類型

的值。

很明顯

-表達式可以有非常複雜的類型。你可能要問是否有帶有給定類型的

-表達式。找到帶有特定類型的

-表達式的問題叫做類型居留問題。

答案是非常引人注目的：有帶有特定類型的閉合

-表達式，當且僅當這個類型對應於一個邏輯定理，在這裏的→符號再次解釋為意味着邏輯藴涵的時候。

例如，考慮恆等函數

，它接受類型ξ的參數並返回類型ξ的結果，所以有類型

。

當然是邏輯定理：給定一個公式

，你可以結論出

。

K函數的類型

也是一個定理。如果已知

為真，則你可以結論出如果

為真就能推出

。這有時也叫做重複規則。B的類型是 (

)→(

)

。你可類似的把它解釋為邏輯重言式；如果已知(

)為真，則如果已知(

)為真，你就能推出

藴涵

。

在證明論和數理邏輯中，相繼式演算（又譯矢列演算、矢列式演算）是眾所周知的一階邏輯（和作為它的特殊情況的命題邏輯）的演繹系統。這個系統也叫做

系統，用以區別於後來建立的有時也叫做相繼式演算的類似風格的各種其他系統。另一個給這種系統的術語是Gentzen系統。相繼式演算

由Gerhard Gentzen介入為研究自然演繹的工具。它已經變成構造邏輯推導的非常有用的演算。它的名字得來自德語的Logischer Kalkül，意思是"邏輯演算"。相繼式演算是關於這個主題的很多研究所選擇的方法。

證明邏輯定理的更加直覺的方式是根岑的相繼式演算。相繼式演算以同希爾伯特式證明對應於組合子表達式一樣的方式對應於λ-表達式程序。直覺邏輯的藴涵片段的相繼式演算規則是：

Γ表示上下文，它是假設的集合。

指示假定上下文Γ我們可以證明

。邏輯定理完全由其證明不需要假設的那些公式t組成的；就是説，t是一個定理，當且僅當我們可以證明

。

在相繼式演算中的證明是樹，它的根是我們要證明的定理，而它的葉子是公理模式實例；每個內部節點必須標記為要麼

要麼

，並且必須包含依據指定規則從子節點推出的一個公式。

相繼式演算證明緊密的對應於λ-演算表達式。斷言

可以被解釋為意味着，給定帶有在Γ中列出類型的值，我們可以製造帶有類型

的一個值。公理對應於帶有新的無約束的類型的新變量介入。

規則對應於函數抽象：

什麼時候我們能結論出某個程序Γ包含類型

的函數?在Γ加上類型

的一個值的時候，包含了足夠的機械來允許我們製造類型

的一個值。

規則對應於函數應用：

如果我們可以製造類型α的一個值，並且如果給出類型β的一個值，我們還可以製造

類型的一個值，則類型

的一個函數將允許我們製造類型

的一個值：首先我們可以製造

，接着應用

函數於它，並接着使用結果的β值來製造類型

的一個值。