【專欄】康托爾、哥德爾、圖靈——永恒的金色對角線(13)
丘齊的lambda calculus其實就是數學推理系統的一個形式化。而圖靈機則是把這個數學概念物理化了。而也正因為圖靈機的概念隱含了實際的物理實現,所以馮?諾依曼才據此提出了奠定現代計算機體系結構的馮?諾依曼體系結構,其遵循的,正是圖靈機的概念。
希爾伯特第十問題結出的碩果
希爾伯特是在1900年巴黎數學家大會上提出著名的希爾伯特第十問題的,簡言之就是是否存在一個算法,能夠計算任意丟番圖方程是否有整根。要解決這個問題,就得先嚴格定義“算法”這一概念。為此圖靈和丘齊分別提出了圖靈機和lambda calculus這兩個概念,它們從不同的角度抽象出了“有效(機械)計算”的概念,著名的圖靈——丘齊命題就是說所有可以有效計算出來的問題都可以由圖靈機計算出來。實際上我們已經看到,丘齊的lambda calculus其實就是數學推理系統的一個形式化。而圖靈機則是把這個數學概念物理化了。而也正因為圖靈機的概念隱含了實際的物理實現,所以馮•諾依曼才據此提出了奠定現代計算機體系結構的馮•諾依曼體系結構,其遵循的,正是圖靈機的概念。而“程序即數據”的理念,這個發端于數學家哥德爾的不完備性定理的證明之中的理念,則早就在黑暗中預示了可編程機器的必然問世。
作者:劉未鵬 出版:電子工業出版社
對角線方法——回顧
我們看到了對角線方法是如何簡潔而深刻地揭示出自指或遞歸結構的。我們看到了著名的不完備性定理、停機問題、Y Combinator、羅素悖論等等等等如何通過這一簡潔優美的方法推導出來。這一誕生于康托爾的天才的手法如同一條金色的絲線,把位于不同年代的偉大發現串聯了起來,并且將一直延續下去……
1.lambda calculus里面的“停機問題”
實際上lambda calculus里面也是有“停機問題”的等價版本的。其描述就是:不存在一個算法能夠判定任意兩個lambda函數是否等價。所謂等價當然是對于所有的n,有f(n)=g(n)了。這個問題的證明更加能夠體現對角線方法的運用。仍然留給你吧。
2.負喧瑣話是個非常不錯的博客。g9的文字輕松幽默,而且有很多名人八卦可以養眼,真的非常不錯。此外g9老兄還是個理論功底非常扎實的牛。所以,anyway,看了他的blog就知道啦!最初這篇文章的動機也正是看了上面的一篇關于Y Combinator的鑄造過程的介紹,于是想揭示一些更深的東西,于是便有了本文。
3.文章起名《康托爾、哥德爾、圖靈——永恒的金色對角線》其實是為了紀念看過的一本好書GEB,即《Godel、Escher、Bach-An Eternal Golden Braid》中文譯名《哥德爾、埃舍爾、巴赫——集異璧之大成》——商務印書館出版。對于一本定價50元居然能夠在douban上賣到100元的二手舊書,我想無需多說。另,幸福的是,電子版可以找到。
4.其實很久前想寫的是一篇《從哥德爾到圖靈》,但那篇寫到1/3不到就擱下了,一是由于事務,二是總覺得少點什么。呵呵,如今把康托爾扯進來,也算是完成當時扔掉的那一篇吧。
5.這恐怕算是寫得最曲折的一篇文章了。不僅自己被這些問題搞得有點暈頭轉向(還好總算走出來),更因為要把這些東西自然而然的串起來,也頗費周章。很多時候是利用吃飯睡覺前或走路的時間思考本質的問題以及如何表達等等,然后到紙上一氣呵成。不過同時也鍛煉了不拿紙筆思考數學的能力。
6.關于圖靈的停機問題、Y Combinator、哥德爾的不完備性定理以及其它種種與康托爾的對角線之間的本質聯系,幾乎查不到完整系統的深入介紹,一些書甚至如《The Emperor’s New Mind》也只是介紹了與圖靈停機問題之間的聯系(已經非常的難得了),google和baidu的結果也是基本沒有頭緒。很多地方都是一帶而過讓人干著急。所以看到很多地方介紹這些定理和構造的時候都是弄得人暈頭轉向的,絕大部分人在面對如Y Combinator、不完備性定理、停機問題的時候都把注意力放在力圖理解它是怎么運作的上面了,卻使人看不到其本質上從何而來,于是人們便對這些東東大為驚嘆。這使我感到很不痛快,如隔靴搔癢般。這也是寫這篇文章的主要動機之一。
(此文的修訂版已收錄《暗時間》一書,由電子工業出版社2011年8月出版。作者于2009年7月獲得南京大學計算機系碩士學位,現在微軟亞洲研究院創新工程中心從事軟件研發工程師工作。)
網絡編輯:謝小跳