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 的 $\iota$ 组合子，定义如下：

ιx = xSK

形式定义 [编辑]

在系统中的项和推导可以被形式定义：

项: 项的集合 T 用如下规则递归的定义。

S、K 和 I 是项。
如果 τ₁ 和 τ₂ 是项，则 (τ₁τ₂) 是项。
不是由前两个规则得到的东西都不是项。

推导: 推导是用下列规则递归定义的项的有限序列（这里的所有希腊字母表示有效的项或带有完全平衡的圆括号的表达式）:

如果 Δ 是结束于形如 α(Iβ)ι 的表达式的一个推导，则 Δ 尾随着项 αβι 是一个推导。
如果 Δ 是结束于形如 α((Kβ)γ)ι 的表达式的一个推导，则 Δ 尾随着项 αβι 是一个推导。
如果 Δ 是结束于形如 α(((Sβ)γ)δ)ι 的表达式的一个推导，则 Δ 尾随着项 α((βδ)(γδ))ι 是一个推导。

假定一个序列本来是一个有效的推导，则可以使用这些规则来扩展它。[1]

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（假）的一个布尔表达式和两个参数组成，使得：

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 對于直覺邏輯的蘊含片段是完備的。

参见 [编辑]

外部链接 [编辑]