王垠的「40 行代码」真如他说的那么厉害吗?
2014-11-25 09:59
323 查看
"我有什么资格说话呢?如果你要了解我的本事,真的很简单:我最精要的代码都放在 GitHub 上了。但是除非接受过专门的训练,你绝对不会理解它们的价值。你会很难想象,这样一片普通人看起来像是玩具的 40 行 cps.ss 代码,融入了我一个星期的日日夜夜的心血,数以几十计的推翻重写。这段代码,曾经耗费了一些顶尖专家十多年的研究。一个教授告诉我,光是想看懂他们的论文就需要不止一个月。而它却被我在一个星期之内闷头写出来了。我是在说大话吗?代码就摆在那里,自己去看看不就知道了。当我死后,如果有人想要知道什么是我上半生最重要的“杰作”,也就是这 40 行代码了。它蕴含的美,超越我给任何公司写的成千上万行的代码。"
有没有人来说说这个东西,我想知道他有没有说大话。
附代码:
;; A simple CPS transformer which does proper tail-call and does not ;; duplicate contexts for if-expressions. ;; author: Yin Wang (yw21@cs.indiana.edu) (load "pmatch.scm") (define cps (lambda (exp) (letrec ([trivial? (lambda (x) (memq x '(zero? add1 sub1)))] [id (lambda (v) v)] [ctx0 (lambda (v) `(k ,v))] ; tail context [fv (let ([n -1]) (lambda () (set! n (+ 1 n)) (string->symbol (string-append "v" (number->string n)))))] [cps1 (lambda (exp ctx) (pmatch exp [,x (guard (not (pair? x))) (ctx x)] [(if ,test ,conseq ,alt) (cps1 test (lambda (t) (cond [(memq ctx (list ctx0 id)) `(if ,t ,(cps1 conseq ctx) ,(cps1 alt ctx))] [else (let ([u (fv)]) `(let ([k (lambda (,u) ,(ctx u))]) (if ,t ,(cps1 conseq ctx0) ,(cps1 alt ctx0))))])))] [(lambda (,x) ,body) (ctx `(lambda (,x k) ,(cps1 body ctx0)))] [(,op ,a ,b) (cps1 a (lambda (v1) (cps1 b (lambda (v2) (ctx `(,op ,v1 ,v2))))))] [(,rator ,rand) (cps1 rator (lambda (r) (cps1 rand (lambda (d) (cond [(trivial? r) (ctx `(,r ,d))] [(eq? ctx ctx0) `(,r ,d k)] ; tail call [else (let ([u (fv)]) `(,r ,d (lambda (,u) ,(ctx u))))])))))]))]) (cps1 exp id)))) ;;; tests ;; var (cps 'x) (cps '(lambda (x) x)) (cps '(lambda (x) (x 1))) ;; no lambda (will generate identity functions to return to the toplevel) (cps '(if (f x) a b)) (cps '(if x (f a) b)) ;; if stand-alone (tail) (cps '(lambda (x) (if (f x) a b))) ;; if inside if-test (non-tail) (cps '(lambda (x) (if (if x (f a) b) c d))) ;; both branches are trivial, should do some more optimizations (cps '(lambda (x) (if (if x (zero? a) b) c d))) ;; if inside if-branch (tail) (cps '(lambda (x) (if t (if x (f a) b) c))) ;; if inside if-branch, but again inside another if-test (non-tail) (cps '(lambda (x) (if (if t (if x (f a) b) c) e w))) ;; if as operand (non-tail) (cps '(lambda (x) (h (if x (f a) b)))) ;; if as operator (non-tail) (cps '(lambda (x) ((if x (f g) h) c))) ;; why we need more than two names (cps '(((f a) (g b)) ((f c) (g d)))) ;; factorial (define fact-cps (cps '(lambda (n) ((lambda (fact) ((fact fact) n)) (lambda (fact) (lambda (n) (if (zero? n) 1 (* n ((fact fact) (sub1 n)))))))))) ;; print out CPSed function (pretty-print fact-cps) ;; => ;; '(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)) ((eval fact-cps) 5 (lambda (v) v)) ;; => 12017 条评论分享 按票数排序按时间排序
16 个回答
陈甫鸼,生长于闽,求学入秦,漂泊适燕,实秦人也。
iamsile、知乎用户、十八哥 等人赞同 谢谢邀请。我不算很熟悉Scheme,只能勉力为之。我知道我的解读也许有错,我也邀请了我熟悉的朋友来回答。他比我懂得更全,应该有帮助。=== 07/29/2013 更新 ===
当事人到场了。我毕竟是个业余搞函数式编程的。大家还是不要看我这里,看@王垠 的原版解释吧。
===================
我大概读过这段代码:https://github.com/yinwang0/gems/blob/master/cps.ss。简单地说,这段代码做了两件事,一件事是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编译器是用另一个编译器编译的;那么顺着这个根源向下跟踪,我们迟早必须回答这个问题,即世界上第一个编译器是什么语言写的——答案是汇编。那么这样下去,我们最终发现,任何程序设计语言都不能完全用自己描述自己。
从工程角度上说,这个问题倒不影响什么。但是从数学角度上看,这个缺陷则让很多人头疼不已,因为它破坏了所谓数学的「美」的原则。这里的「美」,实际的含义是自解释。很多符号逻辑研究者都热衷于找到一种符号体系,能够使用有限的符号系统描述自身。只要找到了这一点,整个解释器的设计可以成为一个自己证明自己的,封闭的体系。
喜欢浪漫的文科朋友们可能会记得希腊神话中的乌洛波洛斯,一条首尾相连象征无穷无尽的蛇。是的,所谓自举就是符号推演世界的乌洛波洛斯,一种纯粹的数学上的和谐和优雅。
可惜对我这个哥德尔定理的信徒而言,这种数学上的美是毫无价值的东西。因为在我的逻辑体系里,这个世界里没有可以自证自身的公理体系。
大概就是这样。
相关文章推荐
- 王垠的「40 行代码」真如他说的那么厉害吗?
- 王垠的「40 行代码」真如他说的那么厉害吗?
- 王垠的「40 行代码」真如他说的那么厉害吗?
- 那么厉害的个人所得税计算器代码你竟然不点开看看,你膨胀了!
- 王垠的「40 行代码」
- Java - try{}里有一个return语句,那么紧跟在这个try后的finally{}里的代码会不会被执行,什么时候被执行,在return前还是后?
- 有了jsRender,妈妈再也不用担心我用jq拼接DOM拼接的一团糟了、页面整齐了、其他伙伴读代码也不那么费劲了
- 基于visual c++之windows核心编程代码分析(40)实现屏幕截取
- C#代码像QQ的右下角消息框一样,无论现在用户的焦点在哪个窗口,消息框弹出后都不影响焦点的变化,那么有两种方法
- 他没你想象的那么厉害!
- 在与 SQL Server 建立连接时出现与网络相关的或特定于实例的错误,未找到或无法访问服务器。错误代码:40
- 关于 OnCloseQuery: 顺序、不能关机等(所有的windows的广播消息都是逐窗口传递的)——如果一个窗体的OnCloseQuery事件中如果写了代码那么WM_QUERYENDSESSION消息就传不过去了msg.result会返回0,关机事件也就停止了
- try{}里有一个return语句,那么紧跟在这个try后的finally{}里的代码会不会被执行,什么时候被执行,在return前还是后?【Java面试题】
- 让你提前认识软件开发(40):既要写好代码,又要写好文档
- win10 1709 华为ensp ar1启动失败 代码40 处理小记
- 解决由于升级的Win10周年版本后Oracle VM VirtualBox无法运行导致的eNSP V390里面的路由器和防火墙等设备无法启动的问题(错误代码40)
- 在中国,有多少程序员干到40了?那么其他人去干什么了?
- 博客代码大全的主页,厉害厉害
- 最大公约数与最小公倍数算法题代码实现【NYOJ题目40】
- 黑客破译android开发代码真就那么简单?