SKI组合子演算

**SKI 組合子演算**是一個計算系統，它是對無類型版本的 Lambda 演算的簡約。這個系統聲稱在 Lambda 演算中所有運算都可以用三個組合子 **S**、**K** 和 **I** 來表達。

在這個系統中的所有函數可以只使用 **S**、**K**、**I** 的字母表和圓括號（分組符號）來表達。通常假定組合子是左結合的，從而在不影響執行次序的情況下精簡表達式中的圓括號。

## 非形式定義

非正式的說，在這個系統中的組合子定義如下（x, y 和 z 表示從函數 **S**, **K**, **I** 與規定值製作的表達式）:

**I** 接受一個參數並返回：

　
: **I**x → x

**K** 接受兩個參數，丟棄第二個，返回第一個：

　
: **K**xy → x

**S** 是代換運算。它接受三個參數，把第一個參數應用於第三個，接著把它應用於把第二個應用於第三個的結果，返回最終的結果。更加清晰的：

　
: **S**xyz → xz(yz)

注意從這些定義可以證實 SKI 演算不是完全進行 Lambda 演算的計算的最小化系統，因為 **I** 可以用 **S** 和 **K** 來表達。這可以通過比較下列表達式和上面的 **I** 的定義來證明：

　
: **SKK**x → **K**x(**K**x) → x

事實上，只使用一個組合子定義一個完備的系統是可能的。一個例子是 Chris Barker 的 $\iota $ 組合子，定義如下：

　
: **ι**x = x**SK**

## 形式定義

在系統中的項和推導可以被形式定義：

**項**:
項的集合 T 用如下規則遞歸的定義。

1. **S**、**K** 和 **I** 是項。
2. 如果 τ1 和 τ2 是項，則 (τ1τ2) 是項。
3. 不是由前兩個規則得到的東西都不是項。

**推導**:
推導是用下列規則遞歸定義的項的有限序列（這裡的所有希臘字母表示有效的項或帶有完全平衡的圓括號的表達式）:

1. 如果 Δ 是結束於形如 α(**I**β)ι 的表達式的一個推導，則 Δ 尾隨著項 αβι 是一個推導。
2. 如果 Δ 是結束於形如 α((**K**β)γ)ι 的表達式的一個推導，則 Δ 尾隨著項 αβι 是一個推導。
3. 如果 Δ 是結束於形如 α(((**S**β)γ)δ)ι 的表達式的一個推導，則 Δ 尾隨著項 α((βδ)(γδ))ι 是一個推導。

假定一個序列本來是一個有效的推導，則可以使用這些規則來擴展它。[1] Archive.is 的存檔，存檔日期 2012-12-15

## SKI 表達式

### 自應用和遞歸

**SII** 是接受一個參數並應用這個參數於自身的表達式：

　
: **SII**α → **I**α(**I**α) → αα

這個表達式的一個有趣的性質是它使表達式 **SII**(**SII**) 不可歸約：

　
: **SII**(**SII**) → **I**(**SII**)(**I**(**SII**)) → **I**(**SII**)(**SII**) → **SII**(**SII**)

這個表達式的另一個結果是它允許你寫應用某個東西到其他某個東西的自應用的函數：

　
: (**S**(**K**α)(**SII**))β → **K**αβ(**SII**β) → α(**SII**β) → α(ββ)

這個函數可以用來完成遞歸。如果 $\beta $ 是應用 $\alpha $ 到其他某個東西的自應用的函數，則自應用 $\beta $ 在 $\beta \beta $ 上遞歸的進行 $\alpha $ 。更加明確的，如果：

　
: β = **S**(**K**α,**SII**) 則：

　
: **SII**β → ββ → α(ββ) → α(α(ββ))→…

### 反轉表達式

**S**(**K**(**SI**))**K** 反轉隨後的兩項：

　
: **S**(**K**(**SI**))**K**αβ →

　
: **K**(**SI**)α(**K**α)β →

　
: **SI**(**K**α)β →

　
: **I**β(**K**αβ) →

　
: **I**βα → βα

### 布爾邏輯

SKI 組合子演算還可以用 if-then-else 結構的形式實現布爾邏輯。if-then-else 結構由要麼為 **T**（真）要麼為 **F**（假）的一個布爾表達式和兩個參數組成，使得：

　
: **T**xy → x

和

　
: **F**xy → y

關鍵在這兩個布爾表達式的定義之中。第一個表現如同我們的基本組合子之一：

　
: **T** = **K**

　
: **K**xy → x

第二個也非常簡單：

　
: **F** = **KI**

　
: **KI**xy → **I**y → y

一旦定義了真和假，所有布爾邏輯都可以用 if-then-else 結構的形式來實現。

布爾運算 NOT（它返回給定布爾值的對立值）表現如同帶有假和真作為第二個和第三個值的 if-then-else 結構，所以可以實現為後綴運算：

　
: NOT = (**F**)(**T**) =(**KI**,**K**) 如果把它們放入 if-then-else 結構中，可以證實它有預期的結果：

　
: (**T**)NOT=**T**(**F**)(**T**)=**F**

　
: (**F**)NOT=**F**(**F**)(**T**)=**T**

布爾運算 OR（如果圍繞它的兩個布爾值任何一個為真則它返回真）表現如同帶有真作為第二個參數的 if-then-else 結構，所以可以實現為中綴運算：

　
: OR = **T** = **K**

如果把它放入 if-then-else 結構中，可以證實它有預期的結果：

　
: (**T**)OR(**T**)=**T**(**T**)(**T**)=**T**

　
: (**T**)OR(**F**)=**T**(**T**)(**F**)=**T**

　
: (**F**)OR(**T**)=**F**(**T**)(**T**)=**T**

　
: (**F**)OR(**F**)=**F**(**T**)(**F**)=**F**

布爾運算 AND（如果圍繞它的兩個布爾值兩個都為真則它返回真）表現如同帶有假作為第三個參數的 if-then-else 結構，所以它可以實現為後綴運算：

　
: AND = **F** = **KI**

如果把它放入 if-then-else 結構中，可以證實它有預期的結果：

　
: (**T**)(**T**)AND=**T**(**T**)(**F**)=**T**

　
: (**T**)(**F**)AND=**T**(**F**)(**F**)=**F**

　
: (**F**)(**T**)AND=**F**(**T**)(**F**)=**F**

　
: (**F**)(**F**)AND=**F**(**F**)(**F**)=**F**

因為如此以 SKI 符號的方式定義了真，假，NOT（作為後綴運算符），OR（作為中綴運算符），AND（作為後綴運算符），這證明了 SKI 系統可以完全的表達布爾邏輯。

### 直覺邏輯

組合子 **K** 和 **S** 對應於兩個周知的命題邏輯公理：

　
: **AK**: A →(B → A)

　
: **AS**:(A →(B → C))→((A → B) →(A → C)) 函數應用對應於肯定前件規則：

**MP**：從 A 和 A → B 推出 B。

公理 **AK** 和 **AS** 和規則 **MP** 對於直覺邏輯的蘊含片段是完備的。

## 參見

* 函數式編程
* 組合子邏輯
* B,C,K,W 系統
* 邱奇數

## 外部連結

* S and K Combinators（頁面存檔備份，存於網際網路檔案館）
* The SKI Combinator Calculus as a Universal SystemArchive.is 的存檔，存檔日期 2012-12-15
* Javascript SKI combinator interpreter（頁面存檔備份，存於網際網路檔案館）