SKI組合子演算

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

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

基本介紹

• 中文名：SKI組合子演算
• 外文名：SKI combinatorial calculus
• 類型：一個計算系統

非形式定義

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

I接受一個參數並返回：

• Ix → x
  

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

• Kxy → x
  

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

• Sxyz → xz(yz)
  

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

• SKKx →Kx(Kx) → x
  

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

• ιx = xSK
  

形式定義

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

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

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

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

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

假定一個序列本來是一個有效的推導，則可以使用這些規則來擴展它。

SKI表達式

自套用和遞歸

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

• SIIα →Iα(Iα) → αα
  

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

• SII(SII) →I(SII)(I(SII)) →SII(SII)
  

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

• (S(Kα)(SII))β →Kαβ(SIIβ) → α(SIIβ) → α(ββ)
  

這個函式可以用來完成遞歸。如果{\displaystyle \beta }是套用{\displaystyle \alpha }到其他某個東西的自套用的函式，則自套用{\displaystyle \beta }在{\displaystyle \beta \beta }上遞歸的進行{\displaystyle \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（假）的一個布爾表達式和兩個參數組成，使得：

• Txy → x
  

和

• Fxy → y
  

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

• T=K
  
• Kxy → x
  

第二個也非常簡單：

• F=KI
  
• KIxy →Iy → 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對於直覺邏輯的蘊含片段是完備的。