Lambda演算的類型

我們已經掌握了直覺邏輯（Intuitionistic Logic，IL），

------------------------------------------------------------------------------------
PS：這一小段是筆者擴充說明下：直覺邏輯。總所周知，最為著名的“經典邏輯（classical logic）/一階邏輯”是學習邏輯的一個起點，以及其他邏輯作為參照的標桿。經典邏輯側重“真值”，陳述的“真值”是其“絕對”特征。一個無歧義的合式陳述（well-formed statement）或真或假。假即非真，真即非假，是為“排中律”。它強調排中律。例如：基于經典邏輯，我們可以“非構造地”證明一個命題。如下圖：

? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ?
上面的證明雖然在經典邏輯里沒有問題，但我們仍無法確定究竟哪一種情況是正確的。除此之外，我們還可以做出一個構造性證明（constructive proof）：對于??我們有?。這種“構造式”的推理方式對應著“直覺主義邏輯”（intuitionistic logic）。直覺主義邏輯的哲學基礎是，不存在絕對真理，只存在理想化數學家（創造主體）的知識和直覺主義構建。邏輯判斷為真當且僅當創造主題可以核實它。所以，直覺主義邏輯不接受排中律。

直覺主義命題邏輯，或稱直覺主義命題演算（Intuitionistic propositional calculus, IPC），的語言和經典命題邏輯的語言是一樣的。直覺主義邏輯里的語義不是通過真值表來判斷的，而是通過構建模式來解釋的。這就是著名的BHK釋義（Brouwer-Heyting-Kolmogorov interpretation）。Heyting 是 Brouwer的學生。Kolmogorov有個著名的學生叫Martin-L?f。如下：? ?

? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ??
有很多邏輯式在經典邏輯里是重言式（tautology），但在直覺主義邏輯里卻沒有構造。如常見的排中律、雙重否定消除、De Morgan定律、反證法等等。直覺主義邏輯的一個證明系統是自然演繹系統??，其中J代表直覺主義邏輯。NK是經典邏輯的自然演繹系統。

布爾代數是經典邏輯的一種語義詮釋，而海廷代數則是直覺主義邏輯的代數語義學。在直覺主義邏輯里，我們關注的首要問題是“可證明性”（provability），而非“真值”。 詳情除了上述的鏈接外，還可以參考：直覺主義邏輯

------------------------------------------------------------------------------------

我們再回到lambda演算：我們已經得到了我們需要定義模型的邏輯工具。 當然，在沒有更簡單的事情了，對吧？

到目前為止我們討論的都是簡單的無類型lambda演算。一如丘奇首次提出LC的第一個版本。但它存在一些問題，為了解決這些問題，人們引入了「類型」（type）的概念，于是出現了簡單類型lambda演算，之后出現了各種變種 —— SystemT，SystemF，Lambda立方（和時間立方沒啥關系:-)）等等。最終，人們意識到無類型lambda演算實際上是類型化lambda演算的一個簡單到病態的特例 —— 只有一個類型的LC。

lambda演算的語義在類型化演算中最容易理解。現在，我們來看看最簡單的類型化LC，叫做「簡單類型化lambda演算」（simply typed lambda calculus）；以及它如何在語義上等同于直覺邏輯。（其實上，每個種類型化LC都對應于一種IL，而且每個LC中的beta規約都對應于IL中的一步推理，這就是為什么我們需要先跑去介紹直覺邏輯，然后再回到這里。）

類型化lambda演算的主要變化是增加了一個叫做「基類型」（base types）的概念。在類型化lambda演算中，你可以使用一些由原子值構成的論域（universe）， 這些值分為不同的簡單類型。基類型通常由單個的小寫希臘字母命名，然而這正好是Blogger的痛處（普通html文本打不出希臘字母），我只好用大寫英文字母來代替類型名稱。因此，例如，我們可以有一個類型「N」，它由包含了自然數集合，也可以有一個類型「B」，對應布爾值true / false，以及一個對應于字符串類型的類「S」。

現在我們有了基本類型，接下來我們討論函數的類型。函數將一種類型（參數的類型）的值映射到的第二種類型（返回值的類型）的值。對于一個接受類型A的輸入參數，并且返回類型B的值的函數，我們將它的類型寫為A -> B 。「 ->」叫做函數類型構造器（function type constructor），它是右關聯的，所以 A -> B -> C 表示 A -> (B -> C)。

為了將類型應用于lambda演算，我們還要做幾件事情。首先，我們需要更新語法，使我們可以包含類型信息。第二，我們需要添加一套規則，以表示哪些類型化程序是合法的。

語法部分很簡單。我們添加了一個「:」符號； 冒號左側是表達式或變量的綁定，其右側是類型規范。 它表明，其左側擁有其右側指定的類型。舉幾個例子：

• lambda x : N . x + 3。表示參數x?類型為N?，即自然數。這里沒有指明函數的結果的類型；但我們知道，函數「+」的類型是?N -> N?，于是可以推斷，函數結果的類型是N。
• (lambda x . x + 3) : N -> N，這和上面一樣，但類型聲明被提了出來，所以它給出了lambda表達式作為一個整體的類型。這一次我們可以推出?x : N?，因為該函數的類型為?N -> N，這意味著該函數參數的類型為 N 。
• lambda x : N, y : B . if y then x * x else x。這是個兩個參數的函數，第一個參數類型是 N ，第二個的類型是 B 。我們可以推斷返回類型為 N 。于是整個函數的類型是?N -> B -> N?。乍看之下有點奇怪；但請記住，lambda演算實際上只有單個參數；多參數函數的寫法只是柯里化的簡寫。所以實際上這個函數是：lambda x : N . (lambda y : B . if y then x * x else x)；內層lambda的類型是?B -> N?; 外層類型是?N -> (B -> N)。

為了討論程序是否關于類型合法（即「良類型的」(well-typed) ），我們需要引入一套類型推理規則。當使用這些規則推理一個表達式的類型時，我們稱之為類型判斷（type judgement）。類型推理和判斷使我們能推斷lambda表達式的類型；如果表達式的任一部分和類型判斷結果不一致，則表達式非法。（丘奇開始研究類型化LC的動機之一是區分「原子」值和「謂詞」值，他通過使用類型以確保謂詞不能操作謂詞，以試圖避免的哥德爾式的悖論。）

我將采用一套不太正規的符號表示類型判斷；標準符號太難用我目前使用的軟件渲染了。常用的符號跟分數有點像；分子由我們已知為真的語句組成；分母則是我們可以從分子中推斷出來的東西。 我們經常在分子中使用一個叫「上下文」（context）的概念，它包含了一組我們已知為真的語句，通常表示為一個大寫的希臘字母。這里我用大寫的希臘字母的名稱表示。如果一個類型上下文包含聲明”x : A，我會寫成?CONTEXT |- x : A。對于分數形式的推理符號，我用兩行表示，分子一行標有「Given: 」，分母一行標有「Infer: 」。 （正常符號用法可以訪問維基百科的STLC頁 。）

**規則1：（類型標識） **

Given: nothing Infer: x : A |- x : A

最簡單的規則：如果我們只知道變量的類型聲明，那么我們知道這個變量是它所聲明的類型。

**規則2：（類型不變式） **

Given: GAMMA |- x : A, x != y Infer: (GAMMA + y : B) |- x : A

這是不干涉語句。 如果我們知道?x : A，那么我們可以推斷出其他任何類型判斷都不能改變我們對x的類型推斷。

規則3：（參數到函數的推理）

Given: (GAMMA + x : A) |- y : B Infer: GAMMA |- (lambda x : A . y) : A -> B

這個語句使我們能夠推斷函數的類型：如果我們知道函數參數的類型是?A，而且該函數返回值的類型是?B?，那么我們可以推出函數的類型為?A -> B?。

最后，Rule4：（函數應用推理）

Given: GAMMA |- x : A -> B, GAMMA |- y : A Infer: GAMMA |- (x y) : B

如果我們知道一個函數的類型為?A -> B?，且把它應用到類型為A的值上，那么結果是類型為?B?的表達式。

規則就是這四個。如果我們有一個lambda表達式，且表達式中每一項的類型判斷都保持一致，那么表達式就是良類型化的（well-typed）。如果不是，則表達式非法。

下面我們找點刺激，描述下SKI組合子的類型。這些都是不完整的類型——我用的是類型變量，而不是具體的類型。 在真正使用組合子的程序中，你可以找到實際類型來替換類型變量。 別擔心，我會用一個例??子來闡明這一點。

• I組合子：?(lambda x . x) : A -> A
• K組合子：?(lambda x : A . ((lambda y : B . x) : B -> A)): A -> B -> A
• S組合子：?(lambda x : A -> B-> C . (lambda y : A -> B . (lambda z : A . (x z : B -> C) (y z : B)))) : (A -> B -> C) -> (A -> B) -> C

現在，讓我們來看一個簡單的lambda演算表達式：lambda x y . y x。由于沒有任何關于類型的聲明或參數，我們無法知道確切的類型。但是，我們知道，x一定具有某種類型，我們稱之為A；而且我們知道，y是一個函數，它以x作為應用的參數，所以它的參數類型為A，但它的結果類型是未知的。因此，利用類型變量，我們有?x : A, y : A -> B。我們可以通過看分析完整的具體表達式來確定A?和?B?。所以，讓我們用x = 3，和y = lambda a : N. a * a?來計算類型。假設我們的類型上下文已經包含了?*?的類型為 “N -> N -> N“。

• (lambda x y . y x) 3 (lambda a : N . a * a)
• 3是整數，所以它的類型是：?3 : N?。
• 根據規則4，我們可以推出出表達式?a * a?的類型是?N，其中?a : N?（*的類型：N -> N -> N），因此，由規則3，lambda表達式的類型是?N - > N?。 于是，我們的表達式現在變成了：(lambda x y . y x) (3 : N) (lambda a : N . (a * a) : N) : N -> N
• 所以 —— 現在我們知道，第一個lambda的參數?x?須是?N?類型，以及?y是?N -> N?類型 。根據規則4我們知道，應用表達式的類型?y x?一定是?N?，然后根據規則3，表達式的類型為：?N -> (N -> N) -> N?。
• 所以此處的類型 A 和 B 最后都是N。

所以，現在我們得到了一個簡單的類型化lambda演算。說它是簡單的類型化，是因為這里對類型的處理方式很少：建立新類型的唯一途徑就是通過「?->」 構造器。其他的類型化lambda演算包括了定義「參數化類型」（parametric types）的能力，它將類型表示為不同類型的函數。

?

終章，Lambda演算建模——程序即證明！

我們已經講過直覺邏輯（intuitionistic logic）和它的模型；從無類型的Lambda演算講到了簡單類型化Lambda演算；終于，我們可以看看Lambda演算模型了。而這正是真正有趣的地方。

先來考慮簡單類型化Lambda演算中的類型。任何可以從下面語法生成的形式都是Lambda演算類型：

type ::= primitive | function | ( type ) primitive ::= A | B | C | D | ... function ::= type -> type

這個語法中的一個陷阱是，你可以創建一個類型的表達式，而且它們是合法的類型定義，但是你無法你寫出一個擁有該類型的單獨的，完整的，封閉表達式。（封閉表達式是指沒有自由變量的表達式。）如果一個表達式類型有類型，我們說表達式「居留」（inhabit）該類型，而該類型是一個居留類型。如果沒有表達式可以居留類型，我們說這是「不可居留的」（uninhabitable） 。

那么什么是居留類型和不可居留類型之間的區別？

答案來自一種叫做「柯里-霍華德同構」（Curry-Howard isomorphism）的理論。這種理論提出，每個類型化的lambda演算，都有相應的直覺邏輯；類型表達式是可居留的當且僅當該類型是在對應邏輯上的定理。

先看類型?A -> A。現在，我們不把?->?看作函數類型構造器，而把它視作邏輯蘊涵。A 蘊含 A?顯然是直覺主義邏輯的定理。因此，類型?A -> A?是可居留的。

再來看看?A -> B?。這不是一個定理，除非在某個上下文中能證明它。作為一個函數類型，這表示一類函數，在不包括任何上下文的情況下，以A類型作為參數，并返回一個不同類型B。你沒法做到這一點——必須有某個上下文提供B類型的值——為了訪問這個上下文，必須存在某種允許函數訪問它的上下文的方式：一個自由變量。這一點在邏輯上和lambda演算上是一樣的：你需要某種上下文建立?A->B?作為一個定理（在邏輯上）或可居留的類型（在lambda演算上）。

下面就容易理解些了。如果有一個封閉LC表達式，其類型是在相應的直覺邏輯中的定理，那么，該類型的表達式就是定理的一個證明。每個Beta規約則等同于邏輯中的一個推理步驟。對應于這個lambda演算的邏輯就是它的模型。從某種意義上說，lambda演算和直覺邏輯，只是同一件事的不同反映。

有兩種方式可以證明這個同構：一種是柯里當初采用的，組合子演算的方式；另一種則用到了所謂的「相繼式演算」（Sequent calculus）。我會組合子證明的版本，所以下面我會快速的過一遍。以后，很可能下個禮拜，我會講相繼式演算的版本。

讓我們回憶一下什么是模型。模型是一種表示演算中的每條聲明（statement）在某些具體值域上都合法的方式——所以存在具體實體和演算中的實體的對應關系，凡演算中的聲明都對應真正的實體的某些聲明。所以我們實際上并不需要做充分的同構；我們只需要一個從演算到邏輯的同態（homomorphism）。（同構是雙向的，從演算到邏輯和邏輯到演算；而同態只從演算到邏輯。）

所以我們需要做的是取任意完整的lambda演算表達式，然后將其轉化為一系列合法的的直覺邏輯語句。由于直覺邏輯本身已被證明是合法的，如果我們可以把lambda演算翻譯成IL，這樣我們就證明了lambda演算的合法性——這意味著我們將表明，在lambda演算中的計算是合法的計算，以及lambda演算是一個完全的，合法的，有效的計算系統。

我們如何從組合子（它們只是省去了變量的lambda演算的簡寫）得到直覺邏輯？它實際上簡單得令人難以相信。

直覺邏輯中的所有證明可以歸結為一系列的步驟，其中的每一步都是使用了以下兩個基本公理之一的推理：

• A implies B implies A
• (A implies B implies C) implies ((A implies B) implies (A implies C))

讓我們用箭頭重寫它們，讓它們看起來像一個類型：A -> B -> A?；及(A -> B -> C) -> ((A -> B) -> (A -> C))。

眼熟嗎？不熟的話再回頭看看簡單類型化lambda演算。這就是S和K組合子的類型。

接下來的建模步驟就很明顯了。lambda演算的類型對應于直覺邏輯的原子類型。函數是推理規則。每個函數可以規約為一個組合子表達式；每個組合子表達式是直覺邏輯的某個基本推理規則的實例。于是，函數就成了相應邏輯里的定理的一個構造性證明。

酷吧？

（任何正常人看完會說“什么？”，但，我顯然不是正常人，我是一個數學怪咖。）

總結

以上是生活随笔為你收集整理的【逻辑与计算理论】Lambda 演算的类型与其 Lambda 演算建模的全部內容，希望文章能夠幫你解決所遇到的問題。

如果覺得生活随笔網站內容還不錯，歡迎將生活随笔推薦給好友。