Can you summarize the following document?
        
  對應可以在兩個層面上看到,首先是類比層次,它聲稱對一個函式計算出的值的型別的斷言可類比於一個邏輯定理,計算這個值的程式可類比於這個定理的證明。在理論電腦科學中,這是連線λ演算和型別論的毗鄰領域的一個重要的底層原理。它被經常以下列形式陳述為“證明是程式”。一個可選擇的形式化為“命題為型別”。其次,更加正式的,它指定了在兩個數學領域之間的同構,就是以一種特定方式形式化的自然演繹和簡單型別λ演算之間是雙射,首先是證明和項,其次是證明歸約步驟和beta歸約。  有多種方式考慮柯里-霍華德對應。在一個方向上,它工作於“把證明編譯為程式”級別上。這裡的“證明”最初被限定為在構造性邏輯中—典型的是直覺邏輯系統中的證明。而“程式”是在常規的函數語言程式設計的意義上的;從語法的觀點上看,這種程式是用某種λ演算表達的。所以柯里-霍華德同構的具體實現是詳細研究如何把來自直覺邏輯的證明寫成λ項。(這是霍華德的貢獻;柯里貢獻了組合子,它是相對於是高階語言的λ演算是能寫所有東西的機器語言)。最近,同樣處理經典邏輯的柯里-霍華德對應的擴充套件可被公式化了,通過對經典有效規則比如雙重否定除去和皮爾士定律關聯上明確的用續體比如call/cc處理的一類項。  還有一個相反的方向,對一個程式的正確性關聯上“證明提取”的可能性。這在非常豐富的型別論環境中是可行的。實際上理論家對推進非常豐富型別的函數語言程式設計語言的開發的動機,已經部分地混合了希望帶給柯里-霍華德對應更加顯著的地位的因素。

  依據λ演算,我們將使用λx.E來指示帶有形式引數x和函式體E的函式。在應用於引數比如a的時候,這個函式生成E,並帶有x的所有自由出現都被替換為a。有效的λ演算表示式有如下形式之一:  通常我們將縮寫((A B)C)為(A B C),縮寫λa.λb.E為λab.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和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,這次是替代α為(β→γ),替代β為α:  這同於前者公式的前件,所以我們推出後件:  交換變數α和γ的名字得到  這就是我們要證明的。

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

  希爾伯特式證明是很難構造的。證明邏輯定理的更加直覺的方式是根岑的相繼式演算。相繼式演算以同希爾伯特式證明對應於組合子表示式一樣的方式對應於λ-表示式程式。  直覺邏輯的蘊涵片段的相繼式演算規則是:
柯里-霍華德對應(英語:Curry-Howard correspondence)是在計算機程式和數學證明之間的緊密聯絡;這種對應也叫做柯里-霍華德同構、公式為型別對應或命題為型別對應。這是對形式邏輯系統和公式計算(computational calculus)之間符號的相似性的推廣。它被認為是由美國數學家哈斯凱爾·柯里和邏輯學家威廉·阿爾文·霍瓦德(William Alvin Howard)獨立發現的。