Lambda算子6b: SKI组合子(下)

扫一扫
分享文章到微信
扫一扫
关注官方公众号
至顶头条

我们学习逻辑的时候，要仔细定义什么叫做等价。其实，我们可以把任何lambda表达式转换为等价的组合子项。

作者：g9 来源：CSDN 2008年2月6日

继续谈论SKI前，得澄清一件重要的事。我说用S K K可以创建等价于lambda x . x的东西，并不等于我们可以把S K K归约到lambda x. x。在我们讨论的lambda算子里，我们说”x = y”当且仅当x和y要么完全一样，要么可以通过alpha变换变得一样（所以lambda x y . x + y 等于 lambda a b . a + b, 但却不等于lambda x y . y + x）。这叫做intentional equivalence（内涵等价？）。不过另外一种等价关系极其有用。我们称之为extensional equivalence(外延等价？)或extentional equality。在extensional equality里，表达式X和表达式Y相等当且仅当X和Y如前所述等价，或者对任意值a, X a ＝ Y a。从现在开始，我们用“＝”或等价指代extensional equality。呵呵，其实编程的时候，equals()也是一个很难实现正确的函数。不然C＋＋不会在STL里加入等价的概念；Java里 ((Long)0L).equals(0) 居然返回false；Ruby里有equal?, eql?，和==；Common Lisp里有eq， eql， equal，和equalp；而Joshua Bloch在Effective Java里用了整整一节讨论equal。更不用说我们学习逻辑的时候，要仔细定义什么叫做等价。

其实，我们可以把任何lambda表达式转换为等价的组合子项。我们可以如下定义转换方程C，把lambda表达式转换为SKI组合子表达式：

(1) C{x} = x

(2) C{E1 E2} = C{E1} C{E2}

(3) C{lambda x . E} = K C{E} 如果x不是E的自由变量

(4) C{lambda x . x} = I

(5) C{lambda x. E1 E2} = (S C{lambda x.E1} C{lambda x.E2})

(6) C{lambda x.(lambda y. E)} = C{lambda x. C{lambda y . E}}, 如果x是E的自由变量

我们来一步一步推导一个例子：

C{lambda x y . y x}
=> Curry

一把

: C{lambda x . (lambda y . y x)}
=> By rule 6: C{lambda x .

C{lambda y . y x}} 
=> By rule 5: C{lambda x . S C{lambda y. y} C{lambda y . x}} 
=> By rule 4: C{lambda x . S I C{lambda y . x}} 
=> By rule 3: C{lambda x . S I (K C{x})} 
=> By rule 1: C{lambda x . S I (K x)} 
=>

By rule 5: S C{lambda x . S I} C{lambda x .

(K x)} 
=> By rule 3: S (K (S I)) C{lambda x . K x}
=> By rule 5: S (K (S I)) (S C{lambda x . K} C{lambda x . x})
=> By rule 1: S (K (S I)) (S C{lambda x . K} I)
=> By rule 3: S (K (S I)) (S (K K) I)

现在的问题是，我们怎么知道最后的结果S (K (S I)) (S (K K) I) 和给出的公式lambda x y . y x 等价？简单，我们传给这个SKI表达式两个参数，x和y，然后规约，看看结果是不是等于y x:

S (K (S I)) (S (K K) I) x y
我们先引进一些变量，让式子好读一些。A=(K (S I)), B = (S (K K) I), 于是原公式变为 S A B x y
展开 S: (A x (B x)) y
替换 B: (A x ((S (K K) I) x)) y
规约掉S: (A x ((K K) x (I x))) y
规约掉 I: (A x ((K K) x x)) y
规约(K K) x: (A x (K x)) y
替换A: ((K (S I)) x (K x)) y
规约 (K (S I)) x, giving: ((S I) (K x)) y
规约 S: I y (K x) y
规约 I: y (K x) y
最后规约(K x) y 得到: y x

因为C的存在，每一个lambda公式都能被转换为SKI组合子表达式。这是何等漂亮的结果！Lambda算子作为计算系统已经够简单了。可没有Curry等数学家的天才，我们很难想象，其貌不扬的组合子S和K，竟然也能构成同样图灵完备的计算系统。事实上，法国闲人David Madore就搞出了一门变态语言，unlambda。在unlambda里，所有东西都是函数。基本操作就是S， K，和I三个组合子。当然，unlambda也加入一些扩展，让程序稍微好些一点。但这些扩展只是句法糖而已。Good Math Bad Math有篇颇为详尽的文章介绍unlambda。 Unlambda的Hello World:

`r```````````.H.e.l.l.o. .w.o.r.l.di

“`”是函数应用操作符。比如说`AB表示把函数A应用到参数B上。“.”是一个元操作符号。.X返回X并打印出X。“r”表示回车。最后的”i”是I组合子。而下面的程序打印出非波拉契数列，并在数列的每一项，F(n),旁边打印出n个星号，”*”：

```s``s``sii`ki

`k.*``s``s`ks

``s`k`s`ks``s``s`ks``s`k`s`kr``s`k`sikk

`k``s`ksk

如果还有老大不满足，还可以去学习另一门基于SKI组合子的语言，Lazy K。下面的程序打印出所有的质数：

 (SII(S(K(S(S(K(SII(S(S(KS)(S(K(S(KS)))(S(K(S(S(KS)(SS(S(S(KS)K))(KK)))))

 (S(S(KS)(S(KK)(S(KS)(S(S(KS)(S(KK)(S(KS)(S(S(KS)(S(KK)(SII)))

 (K(SI(KK)))))))(K(S(K(S(S(KS)(S(K(SI))(S(KK)(S(K(S(S(KS)K)(S(S(KS)K)I)

 (S(SII)I(S(S(KS)K)I)(S(S(KS)K)))))(SI(K(KI)))))))))(S(KK)K)))))))(K(S(KK)

 (S(SI(K(S(S(S(S(SSK(SI(K(KI))))(K(S(S(KS)K)I(S(S(KS)K)(S(S(KS)K)I))

 (S(K(S(SI(K(KI)))))K)(KK))))(KK))(S(S(KS)(S(K(SI))(S(KK)(S(K(S(S(KS)K)))

 (SI(KK))))))(K(K(KI)))))(S(S(KS)(S(K(SI))(SS(SI)(KK))))(S(KK)

 (S(K(S(S(KS)K)))(SI(K(KI)))))))))(K(K(KI))))))))))(K(KI)))))(SI(KK)))))

 (S(K(S(K(S(K(S(SI(K(S(K(S(S(KS)K)I))(S(SII)I(S(S(KS)K)I)))))))K))))

 (S(S(KS)(S(KK)(SII)))(K(SI(K(KI)))))))(SII(S(K(S(S(KS)(S(K(S(S(SI(KK))

 (KI))))(SS(S(S(KS)(S(KK)(S(KS)(S(K(SI))K)))))(KK))))))(S(S(KS)

 (S(K(S(KS)))(S(K(S(KK)))(S(S(KS)(S(KK)(SII)))(K(S(S(KS)K)))))))(K(S(S(KS)

 (S(K(S(S(SI(KK))(KI))))(S(KK)(S(K(SII(S(K(S(S(KS)(S(K(S(K(S(S(KS)(S(KK)

 (S(KS)(S(K(SI))K))))(KK)))))(S(S(KS)(S(KK)(S(K(SI(KK)))(SI(KK)))))

 (K(SI(KK))))))))(S(S(KS)(S(K(S(KS)))(S(K(S(KK)))(S(S(KS)(S(KK)(SII)))

 (K(SI(K(KI))))))))(K(K(SI(K(KI)))))))))(S(K(SII))(S(K(S(K(SI(K(KI))))))

 (S(S(KS)(S(KK)(SI(K(S(K(S(SI(K(KI)))))K)))))(K(S(K(S(SI(KK))))

 (S(KK)(SII)))))))))))(K(SI(K(KI))))))))(S(S(KS)K)I)

 (SII(S(K(S(K(S(SI(K(KI)))))K))(SII)))))

查看本文来源

Lambda算子6a: SKI组合子(上)

Lambda算子6a: SKI组合子(上)

VIP专区

VIP用户

普通用户

邮件订阅

如果您非常迫切的想了解IT领域最新产品与技术信息，那么订阅至顶网技术邮件将是您的最佳途径之一。

重磅专题

往期文章

Lambda算子6b: SKI组合子(下)

业界热点: