【专栏】康托尔、哥德尔、图灵——永恒的金色对角线(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月获得南京大学计算机系硕士学位,现在微软亚洲研究院创新工程中心从事软件研发工程师工作。)

网络编辑:谢小跳

{{ isview_popup.firstLine }}{{ isview_popup.highlight }}

{{ isview_popup.secondLine }}

{{ isview_popup.buttonText }}