王垠的「40 行代码」真如他说的那么厉害吗?

"我有什么资格说话呢?如果你要了解我的本事,真的很简单:我最精要的代码都放在 GitHub 上了。但是除非接受过专门的训练,你绝对不会理解它们的价值。你会很难想象,这样一片普通人看起来像是玩具的 40 行 cps.ss 代码,融入了我一个星期的日日夜夜的心血,数以几十计的推翻重写。这段代码,曾经耗费了一些顶尖专家十多年的研究。一个教授告诉我,光是想看懂他们的论文就需要不止一个月。而它却被我在一个星期之内闷头写出来了…
关注者
3927
被浏览
1307128

33 个回答

王垠 cps.ss explained:


1. 背景知识

CPS: Continuation-Passing Style. 有一篇介绍 CPS 通俗易懂的文章中文翻译)。

简单来讲,CPS 是一种编程风格:

Javascript:

(原味)

function foo(x) {

return x ;

}



(CPS)

function cps_foo(x, return_point) {

return return_point (x) ;

}


CPS 多了一个参数 return_point,return_point 来自 caller ,是 caller 所在的“世界”,caller 将这个“世界” 传递给 callee (cps_foo),这样 cps_foo 就无须利用额外的工具(比如堆栈)去查询 caller 的世界在哪里,以便返回,而是直接进入这个世界:return_point (x)。 这便是 CPS 的初衷 —— 去掉层层嵌套的世界。行话讲就是 desugar(脱糖)。Syntax sugar 是为了方便人类的表达和理解,给编程语言的核心套上的一层好吃好看的外衣,而对机器对程序的解释,需要将其还原到最本质的结构,以便机械化处理和优化,这 就是脱糖的意义



以函数式编程的观点来看,return_point 是一个函数,以 C 观点来看,你可以把它理解为程序地址,或者,以 Matrix 来看,它是 key-maker 打开门进入新世界的那把钥匙。“世界”上只有一个巨大的程序(比如,你的程序不过是在 chrome 里面运行的一个小程序,而 chrome 又是在 OS 里面的一个小程序),return_point 将各种小程序窜连起来了。恩,差不多就是这个意思。只不过,在函数式程序里面(比如Scheme)里面,return_point 是函数,而在过程式程序(比如C)里面它更像是 0x4f36a0c4。

这段 40 多行代码是给 Scheme 程序脱糖的程序,属于解释器的代码,而不是应用代码。对其的客观评价显然只有设计解释器的人才能给出。对应用程序员的意义在于,发现每天上班时编写的代码多么无聊,此外并没有任何实用价值。


2. 运行结果

'x
'(lambda (x k) (k x))
'(lambda (x k) (x 1 k))
'(f x (lambda (v0) (if v0 a b)))
'(if x (f a (lambda (v0) v0)) b)
'(lambda (x k) (f x (lambda (v0) (if v0 (k a) (k b)))))
'(lambda (x k) (let ((k (lambda (v0) (if v0 (k c) (k d))))) (if x (f a k) (k b))))
'(lambda (x k) (let ((k (lambda (v0) (if v0 (k c) (k d))))) (if x (k (zero? a)) (k b))))
'(lambda (x k) (if t (if x (f a k) (k b)) (k c)))
'(lambda (x k) (let ((k (lambda (v0) (if v0 (k e) (k w))))) (if t (if x (f a k) (k b)) (k c))))
'(lambda (x k) (let ((k (lambda (v0) (h v0 k)))) (if x (f a k) (k b))))
'(lambda (x k) (let ((k (lambda (v0) (v0 c k)))) (if x (f g k) (k h))))
'(f a (lambda (v0) (g b (lambda (v1) (v0 v1 (lambda (v2) (f c (lambda (v3) (g d (lambda (v4) (v3 v4 (lambda (v5) (v2 v5 (lambda (v6) v6))))))))))))))
'(lambda (n k)
((lambda (fact k) (fact fact (lambda (v0) (v0 n k))))
(lambda (fact k)
(k
(lambda (n k)
(if (zero? n)
(k 1)
(fact
fact
(lambda (v1) (v1 (sub1 n) (lambda (v2) (k (* n v2))))))))))
k))
120

原代码中最后一句 ((eval fact-cps ) 5 (lambda (v) v)) 在 racket 中要修改为:
((eval fact-cps (make-base-namespace)) 5 (lambda (v) v)) 才能通过算得 120。


3. 注释


4. 要点

ctx: 函数在执行(apply)时候的上下文环境,可理解为 C 程序中运行时的栈。

整 个 cps 的(主要)过程就是 if 分支在不断制造新的 ctx, 而 apply 分支(最后一个分支)不断在新的 ctx 中 '计算' (实际上是生成 cps 函数的代码,而不是真的计算),并返回结果(到上一层 ctx)的过程。这个过程就是 scheme 的基本 eval-apply 过程。(参见SICP第四章)

这是一个解释器(解释成为 CPS 风格的代码),同时也是一个CPS转换器,正所谓 Compiling with Continuations. 另外,Scheme 这种代码即数据(字符串列表)的特性,使得编写生成代码的代码相对容易和简洁。

至于代码为何有 k 这个命名。呵呵,你可以叫它 kontinuation 或者 klosure.

5. 结论

以自然语言写作比喻,编写自解释器级别的代码,就像你在写一本小说,而小说的主角也在写一本小说,这位主角在描写你,对你的刻画会影响到你,你受到影响之后又会改变小说中的主角,从而影响到他对你的描写。你俩要相安无事,情节合符逻辑地发展,直到最后圆满的结尾。这比写一本普通小说可难多了。

Amazing & Fun !
谢谢邀请。我不算很熟悉Scheme,只能勉力为之。我知道我的解读也许有错,我也邀请了我熟悉的朋友来回答。他比我懂得更全,应该有帮助。

=== 07/29/2013 更新 ===
当事人到场了。我毕竟是个业余搞函数式编程的。大家还是不要看我这里,看@王垠 的原版解释吧。
===================

我大概读过这段代码:github.com/yinwang0/gem。简单地说,这段代码做了两件事,一件事是CPS,也就是自动尾递归,第二件事则是用Scheme语言写了一个Scheme的解释器。通过他给出的cps函数,我可以用Scheme这个语言的符号系统重新定义所有Scheme的关键字,并执行正确的程序语义。换言之,它可以让这个语言自己解释自己。本质上,他的代码是在模仿当初 John McCarthy 发明 Lisp 语言时给出的代码,但用了Scheme风格重写了一遍。

这段代码里有一些相当有技巧性的部分。主要是那个cps1函数。我承认我也没有完全看懂,但大概能理解它在保持语义的同时基本做到了语言元素的最小化。他的代吗的31行和37行就是最关键的部分,实现了条件分支和递归调用。基本的原理并不复杂,主要是利用了Scheme的列表解构拆解元素,最终落实到条件分支和函数调用。如果说得更Scheme风格一点,这个cps函数就是一个自己实现的eval函数。当然是简化了一些,没有实现一些更夸张的功能,比如call-with-current-continuation。

注:这个cps的实现中只包含了很少的几个语言特性:定义常量,定义函数,分支(if)和递归。这是满足一个有意义的最小化描述必需的。如果任意引入语言元素,比如while,循环,则可能就会出现语言元素爆炸的情况,陷入无限自证的逻辑怪圈里去。

对这段代码,我自己的建议是,大家可以不必太在乎王垠的宣言。能写出这段代码的人,无疑非常熟悉符号推理的一般规则,也具备相当深厚的数学功底,一般人确实是写不出来。这也符合我对王垠学识的印象。但我也得说,这段代码对多数工程师而言并没有实际价值。不懂也无妨。

======
对不熟悉编译原理和符号推理的朋友们来说,这里可能需要一些额外的说明。请参见下方。

在编译原理的世界里,自举是一个很重要的话题。一个很经典的例子:GCC语言的编译器是C语言写的,但第一个GCC编译器是用另一个编译器编译的;那么顺着这个根源向下跟踪,我们迟早必须回答这个问题,即世界上第一个编译器是什么语言写的——答案是汇编。那么这样下去,我们最终发现,任何程序设计语言都不能完全用自己描述自己。

从工程角度上说,这个问题倒不影响什么。但是从数学角度上看,这个缺陷则让很多人头疼不已,因为它破坏了所谓数学的「美」的原则。这里的「美」,实际的含义是自解释。很多符号逻辑研究者都热衷于找到一种符号体系,能够使用有限的符号系统描述自身。只要找到了这一点,整个解释器的设计可以成为一个自己证明自己的,封闭的体系

喜欢浪漫的文科朋友们可能会记得希腊神话中的乌洛波洛斯,一条首尾相连象征无穷无尽的蛇。是的,所谓自举就是符号推演世界的乌洛波洛斯,一种纯粹的数学上的和谐和优雅。

可惜对我这个哥德尔定理的信徒而言,这种数学上的美是毫无价值的东西。因为在我的逻辑体系里,这个世界里没有可以自证自身的公理体系。

大概就是这样。