SKI组合子演算

SKI组合子演算是一个计算系统，它是对无类型版本的Lambda演算的简约。这个系统声称在Lambda演算中所有运算都可以用三个组合子S、K和I来表达。

在这个系统中的所有函数可以只使用S、K、I的字母表和圆括号（分组符号）来表达。通常假定组合子是左结合的，从而在不影响执行次序的情况下精简表达式中的圆括号。

非形式定义

非正式的说，在这个系统中的组合子定义如下（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. 如果τ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β) → α(ββ)

这个函数可以用来完成递归。如果 是应用 到其他某个东西的自应用的函数，则自应用 在 上递归的进行 。更加明确的，如果：

β = 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对于直觉逻辑的蕴含片段是完备的。

参见

外部链接