組合子邏輯

組合子邏輯是Moses Schönfinkel和哈斯凱爾·加里介入的一種符號系統，用來消除數理邏輯中對變量的需要。它最近在計算機科學中被用做計算的理論模型和設計函數式程式語言的基礎。它所基於的組合子是只使用函數應用或早先定義的組合子來定義從它們的參數得出的結果的高階函數。

數學中的組合子邏輯

組合子邏輯意圖作為簡單的元邏輯，它能澄清在邏輯符號中的量化變量的意義，並真正的消除對它們的需要。消除量化變量的另一種方式是蒯因的謂詞函子。儘管多數組合子邏輯系統超出了一階邏輯的表達能力，蒯因的謂詞函子的表達能力等價於一階邏輯（Quine [1960] 1966）。

組合子邏輯的最初發明者Schönfinkel，在1929年之後基本停止了發表著作。Curry在1927年^[1]晚期於哥廷根大學讀博士的時候重新發現了組合子。在1930年代後期，邱奇和他的學生在普林斯頓發明了一個競爭的函數抽象的形式化，就是lambda演算，它比組合子邏輯更加流行。這些歷史上的意外事件的結果是直到在1960年代和1970年代理論計算機科學開始感興趣於組合子邏輯，關於這個主題的幾乎所有工作都是哈斯凱爾·柯里和他的學生們，或比利時的Robert Feys做的。Curry和Feys (1958)和Curry等人（1972） 縱覽了組合子邏輯的早期歷史。組合子邏輯和lambda演算的更現代的平行處置參見Barendregt（1984），他還評論了達納·斯科特在1960年代和1970年代為組合子邏輯設計的模型。

計算中的組合子邏輯

在計算機科學中，組合子邏輯被用做可計算性理論中計算和證明論的簡化模型。這個理論儘管簡單，但捕獲了計算本質的很多根本特徵。

組合子邏輯可以被看作是lambda演算的變體，它把lambda表達式（用來允許函數抽象）替代為組合子的有限集合，它們是不包含自由變量的原始函數。很容易把lambda表達式變換成組合子表達式，並且因為組合子歸約比lambda歸約要簡單，它已經被用做用軟體中的某些非嚴格的函數式編程語言和硬體的圖歸約機的實現基礎。

還可以用很多其他方式來看待它，很多早年的論文證明了各種組合子到各種邏輯公理的等價性[Hindley and Meredith, 1990]。

lambda演算概要

主條目：lambda演算

lambda演算關注的是叫做lambda-項的對象，它們是下列形式之一的符號串：

• v
• λv.E1
• (E1 E2)

這裡的v是變量名字，它取自預定義變量名字的無限集合，而E1和E2是lambda-項。形如λv.E1的項叫做抽象。變量v叫做抽象的形式參數，而E1是抽象的「主體」。

項λv.E1表示一個函數，它應用於一個參數，綁定形式參數v到這個參數，接著計算E1的結果值---就是說，它返回E1，帶有v的所有出現被參數所替代。

形如 (E1 E2)的項叫做應用。應用建模函數調用或執行：調用E1所代表的函數，帶有E2作為它的參數，並計算結果。如果E1（有時叫做applicand）是一個抽象，則這個項可以被歸約：參數E2可以被代換如E1的主體中E1的形式參數的位置上，而結果是一個新的lambda項，它等價於舊的。如果一個lambda項不包含形如 (λv.E1 E2)的子項，則它不能被歸約，而被稱為是範式。

表達式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演算中抽象是製造函數的唯一方式，在組合子演算中必須有某種東西替代它。不再使用抽象，組合子演算提供了有限的基本函數的集合，其他函數可以用它們來構建。

組合子項

組合子項是下列形式之一：

• v
• P
• (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首先將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[ ]可定義如下：

1. T[V] = > V
2. T[(E1 E2)] = >(T[E1] T[E2])
3. T[λx.E] = > (K T[E])（如果x在E中沒有自由出現）
4. T[λx.x] = > I
5. T[λx.λy.E] = > T[λx.T[λy.E]]（如果x在E中自由出現）
6. 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.(S I T[λy.x])]（通過4）

= T[λx.(S I (K x))]（通過3）

= (S T[λx.(S I)] T[λx.(K x)])（通過6）

= (S (K (S I)) T[λx.(K x)])（通過3）

= (S (K (S I)) (S T[λx.K] T[λx.x]))（通過6）

= (S (K (S I)) (S (K K) T[λx.x]))（通過3）

= (S (K (S I)) (S (K K) I))（通過4）

如果我們應用這個組合子於任何兩個項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項展開為長度為Θ（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 (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。

一點基

有一點基（one point basis），所有組合子都可從它複合而外延等於任何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所使用，他們的名字已經關聯到了它們的應用上了。使用這些組合子，我們可以擴展變換規則為如下：

1. T[V] = > V
2. T[(E1 E2)] = >(T[E1] T[E2])
3. T[λx.E] = > (K T[E]) （如果x在E中不是自由的）
4. T[λx.x] = > I
5. T[λx.λy.E] = > T[λx.T[λy.E]]（如果x在E中是自由的）
6. T[λx.(E1 E2)] => (S T[λx.E1] T[λx.E2])（如果x在E1和E2二者中是自由的）
7. T[λx.(E1 E2)] => (C T[λx.E1] E2)（如果x在E1中是自由的，但在E2中不是自由的）
8. 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.(C I x)]

= (C I) （η-歸約）

= C_*（傳統規範記號：X_* = X I）

= I'（傳統規範記號：X' = C X）

(C I x y)的確歸約到 (y x):

(C I 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演算

在本文描述的CL_K和CL_I演算必須做出區分。這種區別對應於在λ_K和λ_I演算之間的區別。不同於λ_K演算，λ_I演算限制抽象為：

λv.E1這裡的v在E1中有至少一次自由出現。

作為結論，組合子K不出現在λ_I演算和CL_I演算中。CL_I的常量有：I, B, C和S，這形成了所有CL_I項可以從它複合出來的基，B和C模擬K。所有λ_I項可以轉換成等價的CL_I組合子，依據類似於前面提供的把λ_K項轉換成CL_K組合子的規則。參見Barendregt (1984)第9章。

逆轉換

從組合子項到lambda項的轉換L[ ]是平凡的：

L[I] = λx.x

L[K] = λx.λy.x

L[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項相應問題的不可判定性。但是，有一個直接證明如下：

首先，觀察到項

Ω = (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) => 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)有規範形式嗎?它有規範形式，若且唯若下列也有：

(S I I Z)

= (I Z (I Z))

= (Z (I Z))

=(Z Z)

= (C (C (B N (S I I)) Ω) I Z) （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) （N的定義）

= Ω

但是Ω沒有規範形式，所以我們得到矛盾。但是如果 (S I I Z)沒有規範形式，則前述歸約為如下：

(N (S I I Z) Ω I)

= (K I Ω I) （N的定義）

=(I I)

= I

這意味著 (S I I Z)的範式簡單的是I，這是另一個矛盾。所以，假設的範式組合子N不存在。

應用

函數式語言的編譯

函數式程式語言經常基於lambda演算的簡單而普遍的語義。

David Turner使用它的組合子實現了SASL程式語言。

Kenneth E. Iverson在他的J程式語言中使用了基於Curry的組合子的原語（primitive），J語言是APL語言的後繼者。這使得Iverson達成了隱式編程，就是說，編程採用不包含變量的函數表達式，並一起使用與這種程序共同工作的強力工具。結果是在任何帶有用戶定義算子的類APL語言中隱式編程都是可能的^[2]。

邏輯

Curry-Howard同構蘊涵了在邏輯和編程之間的聯繫：每個直覺邏輯的有效的定理證明都直接對應於一個有類型的lambda項的歸約，反之亦然。定理自身也通過函數類型標誌（signature）來識別。特別是，有類型的組合子邏輯對應於證明論中的希爾伯特系統。

K和S組合子對應於公理

AK: A → (B → A),

AS: (A → (B → C)) → ((A → B) → (A → C)),

而函數應用對應於肯定前件規則

MP:從A且A → B推出B。

由AK, AS和MP組成的演算對於直覺邏輯的蘊涵片段是完備的。考慮所有演繹閉合的公式的集合W，按包含排序。則${\displaystyle \langle W,\subseteq \rangle }$是直覺Kripke框架，我們定義在這個框架內的模型${\displaystyle \langle W,\subseteq ,\Vdash \rangle }$為

${\displaystyle X\Vdash A\iff A\in X.}$

這個定義服從對→的滿足的條件：在一方面，如果${\displaystyle X\Vdash A\to B}$，並且${\displaystyle Y\in W}$使得${\displaystyle Y\supseteq X}$且${\displaystyle Y\Vdash A}$，則通過肯定前件而${\displaystyle Y\Vdash B}$。在另一方面，如${\displaystyle X\not \Vdash A\to B}$，則通過演繹定理而${\displaystyle X,A\not \vdash B}$，因此${\displaystyle X\cup \{A\}}$的演繹閉包是${\displaystyle Y\in W}$的一個元素使得${\displaystyle Y\supseteq X}$, ${\displaystyle Y\Vdash A}$和${\displaystyle Y\not \Vdash B}$。

設A是在演算中不能證明的任何公式。則A不屬於非空集合的演繹閉包X，所以${\displaystyle X\not \Vdash A}$，而A不是直覺有效的。

參見

• SKI組合子演算
• B,C,K,W系統
• 不動點組合子
• 圖歸約機
• 超組合子
• 柯里化
• λ演算
• 極小化求值
• 求值策略

注釋

1. Seldin, Jonathan. The Logic of Curry and Church.
2. Cherlin, Edward. Pure Functions in APL and J. Proceedings of the International Conference on APL '91. 1991: 88–93. ISBN 0897914414. doi:10.1145/114054.114065.

引用

• Moses Schönfinkel, 1924, "Über die Bausteine der mathematischen Logik," translated as "On the Building Blocks of Mathematical Logic" in From Frege to Gödel: a source book in mathematical logic, 1879-1931, Jean van Heijenoort, ed. Harvard University Press, 1967. ISBN 978-0-674-32449-7 The article that founded combinatory logic.
• Curry, Haskell B.; Robert Feys. Combinatory Logic Vol. I 1. Amsterdam: North Holland. 1958. 引文使用過時參數coauthors (幫助)
• Curry, Haskell B.; J. Roger Hindley and Jonathan P. Seldin. Combinatory Logic Vol. II 2. Amsterdam: North Holland. 1972. ISBN 978-0-7204-2208-5. 引文使用過時參數coauthors (幫助)
• Field, Anthony J. and Peter G. Harrison, 1998. Functional Programming. . Addison-Wesley. ISBN 978-0-201-19249-0
• Paulson, Lawrence C., 1995. Foundations of Functional Programming. （頁面存檔備份，存於網際網路檔案館） University of Cambridge.
• Sørensen, Morten Heine B. and Paweł Urzyczyn, 1999. Lectures on the Curry-Howard Isomorphism. University of Copenhagen and University of Warsaw, 1999.
• 1920-1931 Currys block notes
• Hindley, Roger, and Meredith, 1990, "Principal Type-Schemes and Condensed Detachment," Journal of Symbolic Logic 55: 90-105
• Hendrik Pieter Barendregt, 1984. The Lambda Calculus, Its Syntax and Semantics. Studies in Logic and the Foundations of Mathematics, Volume 103, North-Holland. ISBN 978-0-444-87508-2
• Quine, W. V., [1960] 1966. "Variables explained away." Chapter 23 in W. V. Quine, Selected Logic Papers, 227–235. New York: Random House. Originally read by invitation to the American Philosophical Association in April 1960 and published in their Proceedings.