組合子邏輯

組合子邏輯是Moses Schönfinkel和哈斯凱爾·加里介入的一種符號系統，用來消除數理邏輯中對變數的需要。它最近在計算機科學中被用做計算的理論模型和設計函數語言程式設計語言的基礎。它所基於的組合子是隻使用函式應用或早先定義的組合子來定義從它們的引數得出的結果的高階函式。數學中的組合子邏輯.組合子邏輯意圖作為簡單的元邏輯，它能澄清在邏輯符號中的量化變數的意義，並真正的消除對它們的需要。消除量化變數的另一種方式是蒯因的謂詞函子。儘管多數組合子邏輯系統超出了一階邏輯的表達能力，蒯因的謂詞函子的表達能力等價於一階邏輯。組合子邏輯的最初發明者Schönfinkel，在1929年之後基本停止了發表著作。Curry在1927年晚期於哥廷根大學讀博士的時候重新發現了組合子。在1930年代後期，邱奇和他的學生在普林斯頓發明了一個競爭的函式抽象的形式化，就是lambda演算，它比組合子邏輯更加流行。這些歷史上的意外事件的結果是直到在1960年代和1970年代理論計算機科學開始感興趣於組合子邏輯，關於這個主題的幾乎所有工作都是哈斯凱爾·柯里和他的學生們，或比利時的Robert Feys做的。Curry和Feys (1958)和Curry等人，他還評論了達納·斯科特在1960年代和1970年代為組合子邏輯設計的模型。計算中的組合子邏輯.在計算機科學中，組合子邏輯被用做可計算性理論中計算和證明論的簡化模型。這個理論儘管簡單，但捕獲了計算本質的很多根本特徵。組合子邏輯可以被看作是lambda演算的變體，它把lambda表示式替代為組合子的有限集合，它們是不包含自由變數的原始函式。很容易把lambda表示式變換成組合子表示式，並且因為組合子歸約比lambda歸約要簡單，它已經被用做用軟體中的某些非嚴格的函數語言程式設計語言和硬體的圖歸約機的實現基礎。還可以用很多其他方式來看待它，很多早年的論文證明了各種組合子到各種邏輯公理的等價性[Hindley and Meredith, 1990]。lambda演算概要.lambda演算關注的是叫做lambda-項的物件，它們是下列形式之一的符號串：這裡的v是變數名字，它取自預定義變數名字的無限集合，而E1和E2是lambda-項。形如λv.E1的項叫做抽象。變數v叫做抽象的形式引數，而E1是抽象的“主體”。項λv.E1表示一個函式，它應用於一個引數，繫結形式引數v到這個引數，接著計算E1的結果值---就是說，它返回E1，帶有v的所有出現被引數所替代。形如 (E1 E2)的項叫做應用。應用建模函式呼叫或執行：呼叫E1所代表的函式，帶有E2作為它的引數，並計算結果。如果E1是一個抽象，則這個項可以被歸約：引數E2可以被代換如E1的主體中E1的形式引數的位置上，而結果是一個新的lambda項，它等價於舊的。如果一個lambda項不包含形如 (λv.E1 E2)的子項，則它不能被歸約，而被稱為是正規化。表示式E[v := a]表示接受項E並把v的所有自由出現替代為a的結果。所以我們寫(λv.E a) =&gt; E[v := a]出於方便，我們用 (a b c d ... z)來簡寫 (...(((a b) c) d) ... z)。。歸約的這個定義的動機是捕獲所有數學函式的本質行為。例如，考慮計算數的平方的函式。我們寫x的平方是x*x。這裡的x是這個函式的形式引數。要計算一個特定引數的平方，比如3，我們把它插入到這個定義中形式引數的位置上：3的平方是3*3要求值表示式3*3的結果，我們必須訴諸我們關於乘法和數3的知識。因為任何計算都簡單的就是在適當基本引數上的適當函式的計算的複合，這個簡單代換原理足夠捕獲計算的本質機制。此外，在lambda演算中，概念比如3和*，不需要任何額外定義基本運算子或常量就可以表示出來。有可能在lambda表示式中確定一些項，在做適合的解釋的時候，它們的表現得如同數3和乘法運算子。已知lambda演算在計算性上等價於關於計算的任何其他似乎為真的模型的能力；就是說，可以在任何這些模型中完成的計算都可以用lambda演算表達，反之亦然。根據邱奇-圖靈論題，這些模型都可以表達任何可能的計算。可能令人驚奇，只使用基於對項中變數的簡單文字代換的函式抽象和應用的簡單概念，lambda演算可以表達任何可想象出來的計算。但是更加不尋常的是甚至抽象都是不需要的。組合子邏輯就是等價於lambda演算的計算模型，它不需要抽象。組合子演算.因為在lambda演算中抽象是製造函式的唯一方式，在組合子演算中必須有某種東西替代它。不再使用抽象，組合子演算提供了有限的基本函式的集合，其他函式可以用它們來構建。組合子項.組合子項是下列形式之一：這裡的v是一個變數，P是基本函式之一，而E1和E2是組合子項。基本函式自身是組合子，或不包含自由變數的函式。組合子的例子.組合子的最簡單的例子是I，恆等組合子，定義為(I x) = x對於所有的項x。另一個簡單的組合子是K，製造常量函式：(K x)是對於任何引數都返回x的函式，所以我們定義((K x) y) = x對於所有的項x和y。或者，服從同lambda演算中多重應用同樣的約定，(K x y) = x第三個組合子是S，它是應用的一般化版本：(S x y z) = (x z (y z))S首先將z分別代換到x和y，然後再將兩個結果進行應用操作。給出S和K，I自身就不是必須的了，因為可以建造自其他兩個：((S K K) x)=(S K K x)= (K x (K x))= x對於任何的項x。注意儘管((S K K)x) = (I x)對於任何x，(S K K)自身不等於I。我們稱這種項是外延相等的。外延相等捕獲了函式的等式的數學概念：兩個函式是相等的，如果它們對於相同的引數總是生成相同的結果。相反的，項自身捕獲了函式的內涵相等的概念：兩個函式是相等的，當且僅當它們有相同的實現。有很多實現恆等函式的方式；(S K K)和I是其中的方式，(S K S)也是。我們將使用詞等價來指示外延相等，保留等於給同一的組合子項。更有趣的組合子是不動點組合子或Y組合子，它可以用來實現遞迴。S-K基的完備性.可能會令人驚奇，事實上S和K可以組合起來生成外延相等於任何lambda項的組合子，所以依據邱奇-圖靈論題，等價於任何可計算的函式。證明是提出一個變換T[ ]，它轉換一個任意的lambda項到等價的組合子。T[ ]可定義如下：把lambda項轉換成組合子項.例如，我們可以轉換λx.λy.(y x)為組合子：T[λx.λy.(y x)]= T[λx.T[λy.(y x)]]= T[λx.(S T[λy.y] T[λy.x])]= T[λx.(S I T[λy.x])]= T[λx.(S I (K x))]= (S T[λx.(S I)] T[λx.(K x)])= (S (K (S I)) T[λx.(K x)])= (S (K (S I)) (S T[λx.K] T[λx.x]))= (S (K (S I)) (S (K K) T[λx.x]))= (S (K (S I)) (S (K K) I))如果我們應用這個組合子於任何兩個項x和y，它可以歸約到如下：(S (K (S I)) (S (K K) I) x y)= (K (S I) x (S (K K) I x) y)= (S I (S (K K) I x) y)= (I y (S (K K) I x y))= (y (S (K K) I x y))= (y (K K x (I x) y))= (y (K (I x) y))= (y (I x))=(y x)組合子表示 (S (K (S I)) (S (K K) I))比相應的lambda項λx.λy.(y x)要長很多，這是典型的。一般的，T[ ]構造可以把長度為n的lambda項展開為長度為Θ的組合子項。T[ ]變換的解釋.T[ ]變換的目的是要消除抽象。兩個特殊情況，規則3和4是平凡的：λx.x明顯等價於I，而λx.E明顯等價於，如果x在E中不是自由出現的。前兩個規則也是簡單的：變數轉換為自身；透過簡單的轉換applicand和引數到組合子，把在組合子項中允許的應用轉換為組合子。有趣的是規則5和6。規則5簡單的聲稱要轉換一個複雜的抽象為組合子，我們必須首先把它的主體轉換成組合子，接著消除這個抽象。規則6實際上消除這個抽象。λx.(E1 E2)是一個函式，它接受一個引數比如a，並把它代換到lambda項 (E1 E2)中x的位置上，生成 (E1 E2)[x : = a]。但是代換a到 (E1 E2)中x的位置上同於代換它到E1和E2二者中，所以(E1 E2)[x := a] =(E1[x := a] E2[x := a])(λx.(E1 E2) a) = ((λx.E1 a) (λx.E2 a))=(S λx.E1 λx.E2 a)= ((S λx.E1 λx.E2) a)透過外延相等，λx.(E1 E2) =(S λx.E1 λx.E2)所以，要找到等價λx.(E1 E2)的組合子，找到等價於 (S λx.E1 λx.E2)的組合子就足夠了，而(S T[λx.E1] T[λx.E2])顯然合適。E1和E2每個都包含嚴格的比 (E1 E2)更少的應用，所以遞迴必定終止於根本沒有應用的lambda項之上---要麼是一個變數，要麼是形如λx.E的項。變換的簡化.η-歸約.透過T[ ]變換生成的組合子可以做的更小，如果我們採用η-歸約規則：T[λx.(E x)] = T[E]λx.(E x)是一個函式，它接受一個引數x並應用函式E於它之上；這外延相等於函式E自身。因此足夠轉換E到組合子形式。採用這種簡化，上面的例子變成：T[λx.λy.(y x)]= (S (K (S I)) T[λx.(K x)])= (S (K (S I)) K) 這個組合子等價於早先的更長的那個：(S (K (S I)) K x y)= (K (S I) x (K x) y)= (S I (K x) y)= (I y (K x y))= (y (K x y))=(y x)類似的，T[ ]變換的最初版本把恆等函式λf.λx.(f x)變換成 (S (S (K S) (S (K K) I)) (K I))。透過η-歸約規則，λf.λx.(f x)被變換成I。一點基.有一點基，所有組合子都可從它複合而外延等於任何lambda項。這種基的最簡單的例子是{X}:X ≡ λx.((xS)K)不難驗證：X (X (X X)) =ηβ K而X (X (X (X X)))) =ηβ S.因為{K, S}是基，得出{X}也是基。B和C組合子.除了組合子S和K之外，Schönfinkel的著作中包含了現在叫做B和C的兩個組合子，帶有如下歸約：(C a b c) =(a c b)(B a b c) = (a (b c))他還解釋瞭如何只使用S和K來表達它們。這些表示式在把謂詞邏輯或lambda演算轉換成組合子表示式的時候非常有用。它們也被Curry和更後來的David Turner所使用，他們的名字已經關聯到了它們的應用上了。使用這些組合子，我們可以擴充套件變換規則為如下：使用B和C組合子，λx.λy.(y x)的變換如下：T[λx.λy.(y x)]= T[λx.T[λy.(y x)]]= T[λx.(C T[λy.y] x)] = T[λx.(C I x)]= (C I) = C*= I'(C I x y)的確歸約到 (y x):(C I x y)=(I y x)=(y x)B和C的目的是S的有限版本。S接受一個值，並把在應用之前，把它代換入applicand和它的引數內，C只在applicand內進行代換，而B只在引數內進行代換。這些組合子的現代名字源於哈斯凱爾·加里在1930年的博士論文。在Schönfinkel的最初著作中，把現在的S, K, I, B和C分別叫做S, C, I, Z和T。CLK與CLI演算.在本文描述的CLK和CLI演算必須做出區分。這種區別對應於在λK和λI演算之間的區別。不同於λK演算，λI演算限制抽象為：λv.E1這裡的v在E1中有至少一次自由出現。作為結論，組合子K不出現在λI演算和CLI演算中。CLI的常量有：I, B, C和S，這形成了所有CLI項可以從它複合出來的基，B和C模擬K。所有λI項可以轉換成等價的CLI組合子，依據類似於前面提供的把λK項轉換成CLK組合子的規則。arendregt (1984)第9章。逆轉換.從組合子項到lambda項的轉換L[ ]是平凡的：L[I] = λx.xL[K] = λx.λy.xL[C] = λx.λy.λz.(x z y)L[B] = λx.λy.λz.(x (y z))L[S] = λx.λy.λz.(x z (y z))L[(E1 E2)] =但是，要注意這個變換不是我們見到的任何版本的T[ ]的逆變換。組合子演算的不可判定性.一個組合子項是否有規範形式，兩個組合子項是否是等價的等等都是不可判定的。者等價於lambda項相應問題的不可判定性。但是，有一個直接證明如下：首先，觀察到項Ω = (S I I (S I I))沒有規範形式，因為它在三個步驟之後歸約到自身，如下：(S I I (S I I))= (I (S I I) (I (S I I)))= (S I I (I (S I I)))= (S I I (S I I))而且沒有其他歸約次序可以使表示式更短些。現在，假設N是檢測正規化的組合子，使得(N x) =&gt; T,如果x有規範形式F,沒有規範形式。(這裡的T和F是常規的lambda演算的真假定義λx.λy.x和λx.λy.y的變換。組合子版本是T = K和F = (K I))。現在設Z = (C (C (B N (S I I)) Ω) I)現在考慮項。(S I I Z)有規範形式嗎?它有規範形式，當且僅當下列也有：(S I I Z)= (I Z (I Z))= (Z (I Z))=(Z Z)= (C (C (B N (S I I)) Ω) I Z) = (C (B N (S I I)) Ω Z I)= (B N (S I I) Z Ω I)= (N (S I I Z) Ω I)現在我們需要應用N於(S I I Z)。(S I I Z)要麼有規範形式，要麼沒有。如果它確實有規範形式，則前述歸約為如下：(N (S I I Z) Ω I)= (K Ω I) = Ω但是Ω沒有規範形式，所以我們得到矛盾。但是如果 (S I I Z)沒有規範形式，則前述歸約為如下：(N (S I I Z) Ω I)= (K I Ω I) =(I I)= I這意味著 (S I I Z)的正規化簡單的是I，這是另一個矛盾。所以，假設的正規化組合子N不存在。應用.函式式語言的編譯.函數語言程式設計語言經常基於lambda演算的簡單而普遍的語義。David Turner使用它的組合子實現了SASL程式語言。Kenneth E. Iverson在他的J程式語言中使用了基於Curry的組合子的原語，J語言是APL語言的後繼者。這使得Iverson達成了隱式程式設計，就是說，程式設計採用不包含變數的函式表示式，並一起使用與這種程式共同工作的強力工具。結果是在任何帶有使用者定義運算元的類APL語言中隱式程式設計都是可能的。邏輯.Curry-Howard同構蘊涵了在邏輯和程式設計之間的聯絡：每個直覺邏輯的有效的定理證明都直接對應於一個有型別的lambda項的歸約，反之亦然。定理自身也透過函式型別標誌來識別。特別是，有型別的組合子邏輯對應於證明論中的希爾伯特系統。K和S組合子對應於公理AK: A → (B → A),AS: (A → (B → C)) → ((A → B) → (A → C)),而函式應用對應於肯定前件規則MP:從A且A → B推出B。由AK, AS和MP組成的演算對於直覺邏輯的蘊涵片段是完備的。考慮所有演繹閉合的公式的集合W，按包含排序。則formula_1是直覺Kripke框架，我們定義在這個框架內的模型formula_2為formula_3這個定義服從對→的滿足的條件：在一方面，如果formula_4，並且formula_5使得formula_6且formula_7，則透過肯定前件而formula_8。在另一方面，如formula_9，則透過演繹定理而formula_10，因此formula_11的演繹閉包是formula_5的一個元素使得formula_6, formula_7和formula_15。設A是在演算中不能證明的任何公式。則A不屬於非空集合的演繹閉包X，所以formula_16，而A不是直覺有效的。