在上一篇文章中顶伞，提了三個問題，這篇文章就圍繞上篇文章的三個問題來討論势誊。
Y組合子究竟干了什么呜达？
所以Y組合子究竟干了點啥？為什么就可以遞歸了粟耻？我們人肉單步一下看一看查近，調用一下(Y f1)看究竟發(fā)生了什么？
(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的人出現(xiàn)了霜威，注意看上面的式子，式子中有這么一部分：
;; ((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)次哈，結合上面的發(fā)現(xiàn)胎署，第二次則是((length (Y length)) list)。這可是遞歸啊窑滞，所以有什么結論琼牧？
(Y F) = (F (Y F)) （還記得第一篇文章中的系徽么？）
所以Y組合子干了什么哀卫？Y組合子干的事兒就是返回一個高階函數(shù)的不動點巨坊，來試一試！
;;; Y Combinator
(define Y
(lambda (f)
((lambda (g)
(g g))
(lambda (h)
(lambda (x)
((f (h h)) x))))))
;;; 計算階乘的測試函數(shù)
(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組合子共啃，你會發(fā)現(xiàn)是下面這個樣子占调。
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組合子么言津？我們的函數(shù)還要調用參數(shù)啊，怎么辦取试？把參數(shù)放后面纺念。
λf.(λxy.((f (x x)) y) λxy.((f (x x)) y))
上面的就是我們一步步推導出來的Y組合子，也就是說如果我們寫的遞歸程序是包含兩個參數(shù)的想括，就應該是這樣：
λf.(λxyz.((f (x x)) y z) λxyz.((f (x x)) y z))
能理解么陷谱？不理解的話慢慢消化:）。
寫遞歸程序的終極要義瑟蜈？
說了這么多說點實用的吧烟逊，寫遞歸程序的終極要義就是：
- 有遞歸出口。
- 調用自己铺根。
- 每次至少改變一個參數(shù)宪躯。
為何要提停機問題？
我們研究Y組合子就Y組合子吧位迂，為何要有停機問題访雪？如果有興趣的話可以去看看哥德爾不完備定理還有羅素悖論。我覺得羅素悖論掂林、哥德爾不完備定理還有停機問題臣缀，說的事兒是差不多的。通過羅素悖論是可以直接推導出Y組合子的泻帮，所以它們之間是存在著某種聯(lián)系的精置。究竟是什么把它們聯(lián)系到了一起？是康托爾對角線法則么锣杂？我是想不清了脂倦，留給你們:）。
全文完元莫。
2015.11.26更新：
看了王垠的一篇英文博客赖阻，恍然大悟，決定把這些寫下來踱蠢。
現(xiàn)在用lambda表達式來證明一下停機問題火欧，還是假設存在這樣的程序，那么我們假設為Halting(f, i)朽基。f是函數(shù)布隔，i是輸入离陶，對于一個函數(shù)f和一個輸入i稼虎，Halting返回true和false來表示停機或者不停機。
Ok招刨，我們利用這個函數(shù)在構造一個新的函數(shù)霎俩，λm.not(Halting(m, m))。現(xiàn)在來思考一個問題，如果我們把這個函數(shù)本身作為自己的參數(shù)打却，那它會不會停機呢杉适？
用表達式來表達就是這樣的：
E: Halting(λ.not(Halting(m, m)), ?λ.not(Halting(m, m)))
到了這一步這個問題就算證完了，因為矛盾已經(jīng)構建出來了柳击。我們只需要展開E猿推，我們能夠得到什么呢？
E = not(Halting(?λ.not(Halting(m, m)),? λ.not(Halting(m, m))))
最后我們得到E = not(E)捌肴，矛盾產(chǎn)生蹬叭。
你看表達式E，是不是和Y很像状知。
