在上一篇文章中,提了三个问题,这篇文章就围绕上篇文章的三个问题来讨论。
Y组合子究竟干了什么?
所以Y组合子究竟干了点啥?为什么就可以递归了?我们人肉单步一下看一看,调用一下(Y f1)
看究竟发生了什么?
(Y f1)
;;; 用实参f1替换掉形参f
((lambda (g)
(g g))
(lambda (h)
(lambda (x)
((f1 (h h)) x))))
;;; 用实参
;; (lambda (h)
;; (lambda (x)
;; ((f1 (h h)) x)))
;;; 代替形参g
((lambda (h)
(lambda (x)
((f1 (h h)) x)))
(lambda (h)
(lambda (x)
((f1 (h h)) x))))
;;; 用实参
;; (lambda (h)
;; (lambda (x)
;; ((f1 (h h)) x)))
;;; 代替上面的形参h
(lambda (x)
((f1
((lambda (h)
(lambda (x)
((f1 (h h)) x)))
(lambda (h)
(lambda (x)
((f1 (h h)) x))))) x))
;;; 各部门注意,最牛B的人出现了,注意看上面的式子,式子中有这么一部分:
;; ((lambda (h)
;; (lambda (x)
;; ((f1 (h h)) x)))
;; (lambda (h)
;; (lambda (x)
;; ((f1 (h h)) x))))
;;; 往上翻翻,这个是不是就是(Y f1)?
上面可以看到,(h h)
实际上就是(Y f1)
。回顾一下之前的length,我们第一次的调用是:((Y length) list)
,结合上面的发现,第二次则是((length (Y length)) list)
。这可是递归啊,所以有什么结论?
(Y F) = (F (Y F))
(还记得第一篇文章中的系徽么?)
所以Y组合子干了什么?Y组合子干的事儿就是返回一个高阶函数的不动点,来试一试!
;;; Y Combinator
(define Y
(lambda (f)
((lambda (g)
(g g))
(lambda (h)
(lambda (x)
((f (h h)) x))))))
;;; 计算阶乘的测试函数
(define test
(lambda (f)
(lambda (n)
(if (< n 2) 1 (* n (f (- n 1)))))))
;;; and Tests
((Y test) 4)
((test (Y test)) 4)
((test (test (Y test))) 4)
结果都是24。
为什么我们推导出的Y组合子和Google出来的不一样?
如果把我们推导出的Y组合子用lambda演算的形式表达出来是什么样的呢?
Y := λf.(λxy.((f (x x)) y) λxy.((f (x x)) y))
如果Google一下Y组合子,你会发现是下面这个样子。
Y := λf.(λx.(f (x x)) λx.(f (x x)))
为什么会这样?让我们来用一种全新的思路去推导Y组合子,观察下面的式子:
(λx.x x) (λx.x x)
这是一个可以重新生成自己的程序,仔细看看是不是?我们想达到什么样的效果:
(f (f (f (f ...))))
是不是就是这样的?所以要怎么样?
λf.(λx.(f (x x)) λx.(f (x x)))
这不就是Google出来的Y组合子么?我们的函数还要调用参数啊,怎么办?把参数放后面。
λf.(λxy.((f (x x)) y) λxy.((f (x x)) y))
上面的就是我们一步步推导出来的Y组合子,也就是说如果我们写的递归程序是包含两个参数的,就应该是这样:
λf.(λxyz.((f (x x)) y z) λxyz.((f (x x)) y z))
能理解么?不理解的话慢慢消化:)。
写递归程序的终极要义?
说了这么多说点实用的吧,写递归程序的终极要义就是:
- 有递归出口。
- 调用自己。
- 每次至少改变一个参数。
为何要提停机问题?
我们研究Y组合子就Y组合子吧,为何要有停机问题?如果有兴趣的话可以去看看哥德尔不完备定理还有罗素悖论。我觉得罗素悖论、哥德尔不完备定理还有停机问题,说的事儿是差不多的。通过罗素悖论是可以直接推导出Y组合子的,所以它们之间是存在着某种联系的。究竟是什么把它们联系到了一起?是康托尔对角线法则么?我是想不清了,留给你们:)。
全文完。
2015.11.26更新:
看了王垠的一篇英文博客,恍然大悟,决定把这些写下来。
现在用lambda表达式来证明一下停机问题,还是假设存在这样的程序,那么我们假设为Halting(f, i)。f是函数,i是输入,对于一个函数f和一个输入i,Halting返回true和false来表示停机或者不停机。
Ok,我们利用这个函数在构造一个新的函数,λm.not(Halting(m, m))
。现在来思考一个问题,如果我们把这个函数本身作为自己的参数,那它会不会停机呢?
用表达式来表达就是这样的:
E: Halting(λ.not(Halting(m, m)), �λ.not(Halting(m, m)))
到了这一步这个问题就算证完了,因为矛盾已经构建出来了。我们只需要展开E,我们能够得到什么呢?
E = not(Halting(�λ.not(Halting(m, m)),� λ.not(Halting(m, m))))
最后我们得到E = not(E)
,矛盾产生。
你看表达式E,是不是和Y很像。