在上一篇文章中，提了三个问题，这篇文章就围绕上篇文章的三个问题来讨论。
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很像。
网友评论