基本介紹
數學中的組合子邏輯,計算中的組合子邏輯,lambda 演算概要,組合子演算,組合子項,組合子的例子,S-K 基的完備性,把 lambda 項轉換成組合子項,T[ ] 變換的解釋,變換的簡化,和 C 組合子,CLK 與 CLI 演算,逆轉換,組合子演算的不可判定性,套用,函式式語言的編譯,邏輯,
它最近在計算機科學中被用做計算的理論模型和設計函式式程式語言的基礎。它所基於的組合子是只使用函式套用或早先定義的組合子來定義從它們的參數得出的結果的高階函式。
數學中的組合子邏輯
組合子邏輯意圖作為簡單的元邏輯，它能澄清在邏輯符號中的量化變數的意義，並真正的消除對它們的需要。消除量化變數的另一種方式是蒯因的謂詞函子。儘管多數組合子邏輯系統超出了一階邏輯的表達能力，蒯因的謂詞函子的表達能力等價於一階邏輯（Quine [1960] 1966）。
組合子邏輯的最初發明者 Schönfinkel，在1929年之後基本停止了發表著作。Curry 在 1927 年晚期於哥廷根大學讀博士的時候重新發現了組合子。在 1930 年代後期，邱奇和他的學生在普林斯頓發明了一個競爭的函式抽象的形式化，就是 lambda 演算，它比組合子邏輯更加流行。這些歷史上的意外事件的結果是直到在 1960 年代和 1970 年代理論計算機科學開始感興趣於組合子邏輯，關於這個主題的幾乎所有工作都是 Haskell Curry 和他的學生們，或比利時的 Robert Feys 做的。Curry 和 Feys (1958) 和 Curry 等人(1972) 縱覽了組合子邏輯的早期歷史。組合子邏輯和 lambda 演算的更現代的平行處置參見 Barendregt (1984)，他還評論了 Dana Scott 在 1960 年代和 1970 年代為組合子邏輯設計的模型。
計算中的組合子邏輯
組合子邏輯可以被看作是 lambda 演算的變體，它把 lambda 表達式（用來允許函式抽象）替代為組合子的有限集合，它們是不包含自由變數的原始函式。很容易把 lambda 表達式變換成組合子表達式，並且因為組合子歸約比 lambda 歸約要簡單，它已經被用做用軟體中的某些非嚴格的函式式編程語言和硬體的圖歸約機的實現基礎。
還可以用很多其他方式來看待它，很多早年的論文證明了各種組合子到各種邏輯公理的等價性 [Hindley and Meredith, 1990]。
lambda 演算概要
lambda 演算關注的是叫做 lambda-項的對象，它們是下列形式之一的符號串:
vλv.E1(E1 E2)
這裡的 v 是變數名字，它取自預定義變數名字的無限集合，而 E1 和 E2 是 lambda-項。形如 λv.E1 的項叫做抽象。變數 v 叫做抽象的形式參數，而 E1 是抽象的“主體”。
項 λv.E1 表示一個函式，它套用於一個參數，綁定形式參數 v 到這個參數，接著計算 E1 的結果值---就是說，它返回 E1，帶有 v 的所有出現被參數所替代。
表達式 E[v := a] 表示接受項 E 並把 v 的所有自由出現替代為 a 的結果。所以我們寫
(λv.E a) => 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 演算中抽象是製造函式的唯一方式，在組合子演算中必須有某種東西替代它。不再使用抽象，組合子演算提供了有限的基本函式的集合，其他函式可以用它們來構建。
組合子項
組合子項是下列形式之一:
vP(E1 E2)
這裡的 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 套用 x 於 y，在首先代換 z 到它們中的每個之後。
給出 S 和 K，I 自身就不是必須的了，因為可以建造自其他兩個:
((SKK) x)= (SKK x)= (K x (K x))= x
對於任何的項 x。注意儘管 ((SKK) x) = (I x) 對於任何 x，(SKK) 自身不等於 I。我們稱這種項是外延相等的。外延相等捕獲了函式的等式的數學概念: 兩個函式是相等的，如果它們對於相同的參數總是生成相同的結果。相反的，項自身捕獲了函式的內涵相等的概念: 兩個函式是相等的，若且唯若它們有相同的實現。有很多實現恆等函式的方式；(SKK) 和 I 是其中的方式，(SKS) 也是。我們將使用詞等價來指示外延相等，保留等於給同一的組合子項。
S-K 基的完備性
可能會令人驚奇，事實上 S 和 K可以組合起來生成外延相等於任何 lambda 項的組合子，所以依據邱奇-圖靈論題，等價於任何可計算的函式。證明是提出一個變換 T[ ]，它轉換一個任意的 lambda 項到等價的組合子。
T[ ] 可定義如下:
T[V] => VT[(E1 E2)] => (T[E1] T[E2])T[λx.E] => (K T[E]) （如果 x 在 E 中不是自由的）T[λx.x] => IT[λx.λy.E] => T[λx.T[λy.E]] （如果 x 在 E 中是自由的）T[λx.(E1 E2)] => (S T[λx.E1] T[λx.E2])
把 lambda 項轉換成組合子項
例如，我們可以轉換 λx.λy.(y x) 為組合子:
T[λx.λy.(y x)]= T[λx.T[λy.(y x)]] （通過 5）= T[λx.(S T[λy.y] T[λy.x])] （通過 6）= T[λx.(SI T[λy.x])] （通過 4）= T[λx.(SI (K x))] （通過 3）= (S T[λx.(SI)] T[λx.(K x)]) （通過 6）= (S (K (SI)) T[λx.(K x)]) （通過 3）= (S (K (SI)) (S T[λx.K] T[λx.x])) （通過 6）= (S (K (SI)) (S (KK) T[λx.x])) （通過 3）= (S (K (SI)) (S (KK) I)) （通過 4）
如果我們套用這個組合子於任何兩個項 x 和 y，它可以歸約到如下:
(S (K (SI)) (S (KK) I) x y)= (K (SI) x (S (KK) I x) y)= (SI (S (KK) I x) y)= (I y (S (KK) I x y))= (y (S (KK) I x y))= (y (KK x (I x) y))= (y (K (I x) y))= (y (I x))= (y x)
組合子表示 (S (K (SI)) (S (KK) I)) 比相應的 lambda 項 λx.λy.(y x) 要長很多，這是典型的。一般的，T[ ] 構造可以把長度為 n 的 lambda 項展開為長度為 Θ(3) 的組合子項。
T[ ] 變換的解釋
T[ ] 變換的目的是要消除抽象。兩個特殊情況，規則 3 和 4 是平凡的: λx.x 明顯等價於 I，而 λx.E 明顯等價於 (K 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.(E x) 是一個函式，它接受一個參數 x 並套用函式 E 於它之上；這外延相等於函式 E 自身。因此足夠轉換 E 到組合子形式。
採用這種簡化，上面的例子變成:
T[λx.λy.(y x)]= ...= (S (K (SI)) T[λx.(K x)])= (S (K (SI)) K) （通過 η-歸約）
這個組合子等價於早先的更長的那個:
(S (K (SI)) K x y)= (K (SI) x (K x) y)= (SI (K x) y)= (I y (K x y))= (y (K x y))= (y x)
類似的，T[ ] 變換的最初版本把恆等函式 λf.λx.(f x) 變換成 (S (S (KS) (S (KK) I)) (KI))。通過 η-歸約規則，λf.λx.(f x) 被變換成 I。
一點基
有一點基(one point basis)，所有組合子都可從它複合而外延等於任何 lambda 項。這種基的最簡單的例子是 {X}:
X ≡ λx.((xS)K)
不難驗證:
X (X (XX)) =K 而X (X (X (XX)))) =S.
因為 {K, S} 是基，得出 {X} 也是基。
和 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 所使用，他們的名字已經關聯到了它們的套用上了。使用這些組合子，我們可以擴展變換規則為如下:
T[V] => VT[(E1 E2)] => (T[E1] T[E2])T[λx.E] => (K T[E]) （如果 x 在 E 中不是自由的）T[λx.x] => IT[λx.λy.E] => T[λx.T[λy.E]] （如果 x 在 E 中是自由的）T[λx.(E1 E2)] => (S T[λx.E1] T[λx.E2]) （如果 x 在 E1 和 E2 二者中是自由的）T[λx.(E1 E2)] => (C T[λx.E1] E2) （如果 x 在 E1 中是自由的，但在 E2 中不是自由的）T[λx.(E1 E2)] => (B E1 T[λx.E2]) （如果 x 在 E2 中是自由的，但在 E1 中不是自由的）
使用 B 和 C 組合子，λx.λy.(y x) 的變換如下:
T[λx.λy.(y x)]= T[λx.T[λy.(y x)]]= T[λx.(C T[λy.y] x)] （通過規則 7）= T[λx.(CI x)]= (CI) （η-歸約）= C*（傳統規範記號: X* = XI）= I'（傳統規範記號: X' = CX）
(CI x y) 的確歸約到 (y x):
(CI x y)= (I y x)= (y x)
B 和 C 的目的是 S 的有限版本。S 接受一個值，並把在套用之前，把它代換入 applicand 和它的參數內，C 只在 applicand 內進行代換，而 B 只在參數內進行代換。
這些組合子的現代名字源於 哈斯凱爾·加里 在 1930 年的博士論文（參見 B,C,K,W系統）。在 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 組合子的規則。參見 Barendregt (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)] = (L[E1] L[E2])
但是，要注意這個變換不是我們見到的任何版本的 T[ ] 的逆變換。
組合子演算的不可判定性
一個組合子項是否有規範形式，兩個組合子項是否是等價的等等都是不可判定的。者等價於 lambda 項相應問題的不可判定性。但是，有一個直接證明如下:
首先，觀察到項
Ω = (SII (SII))
沒有規範形式，因為它在三個步驟之後歸約到自身，如下:
(SII (SII))= (I (SII) (I (SII)))= (SII (I (SII)))= (SII (SII))
而且沒有其他歸約次序可以使表達式更短些。
現在，假設 N 是檢測範式的組合子，使得
(N x) => T, 如果 x 有規範形式F, 沒有規範形式。
(這裡的 T 和 F 是常規的 lambda 演算的真假定義 λx.λy.x 和 λx.λy.y 的變換。 組合子版本是 T = K 和 F = (KI))。
現在設
Z = (C (C (BN (SII)) Ω) I)
現在考慮項 (SII Z)。(SII Z) 有規範形式嗎? 它有規範形式，若且唯若下列也有:
(SII Z)= (I Z (I Z))= (Z (I Z))= (Z Z)= (C (C (BN (SII)) Ω) I Z) （Z 的定義）= (C (BN (SII)) Ω Z I)= (BN (SII) Z ΩI)= (N (SII Z) ΩI)
現在我們需要套用 N 於 (SII Z)。(SII Z) 要么有規範形式，要么沒有。如果它確實有規範形式，則前述歸約為如下:
(N (SII Z) ΩI)= (KΩI) （N 的定義）= Ω
但是 Ω 沒有規範形式，所以我們得到矛盾。但是如果 (SII Z) 沒有規範形式，則前述歸約為如下:
(N (SII Z) ΩI)= (KIΩI) （N 的定義）= (II)= I
這意味著 (SII Z) 的範式簡單的是 I，這是另一個矛盾。所以，假設的範式組合子 N 不存在。
套用
函式式語言的編譯
函式式程式語言經常基於 lambda 演算的簡單而普遍的語義。
David Turner 使用它的組合子實現了 SASL 程式語言。
邏輯
Curry-Howard同構蘊涵了在邏輯和編程之間的聯繫: 每個直覺邏輯的有效的定理證明都直接對應於一個有類型的 lambda 項的歸約，反之亦然。 定理自身也通過函式類型標誌(signature)來識別。特別是，有類型的組合子邏輯對應於證明論中的希爾伯特系統。
K 和 S 組合子對應於公理
AK: A → (B → A),AS: (A → (B → C)) → ((A → B) → (A → C)),
而函式套用對應於肯定前件規則
MP: 從 A 且 A → B 推出 B。
