计算的极限(十二):不会出错的程序

本文遵守首页的CC版权声明:署名-非商业性使用-禁止演绎,请自觉遵守,非授权请勿转载。

本文在科学松鼠会发表,地址:http://songshuhui.net/archives/93698

计算无处不在。

走进一个机房,在服务器排成的一道道墙之间,听着风扇的鼓噪,似乎能嗅出0和1在CPU和内存之间不间断的流动。从算筹算盘,到今天的计算机,我们用作计算的工具终于开始量到质的飞跃。计算机能做的事情越来越多,甚至超越了它们的制造者。上个世纪末,深蓝凭借前所未有的搜索和判断棋局的能力,成为第一台战胜人类国际象棋世界冠军的计算机,但它的胜利仍然仰仗于人类大师赋予的丰富国际象棋知识;而仅仅十余年后,Watson却已经能凭借自己的算法,先“理解”问题,然后有的放矢地在海量的数据库中寻找关联的答案。长此以往,工具将必在更多的方面超越它的制造者。而这一切,都来源于越来越精巧的计算。

计算似乎无所不能,宛如新的上帝。但即使是这位“上帝”,也逃不脱逻辑设定的界限。

第一位发现这一点的,便是图灵。

相信每个人都见识过Windows那令人忧郁的蓝屏或者黑屏吧。有时因为它,一个上午的工作一瞬间毁于一旦,这就不仅是令人忧郁而是令人抓狂了。在这个时候,你是否会在心中大声咒骂那帮写程序不小心让蓝屏一而再再而三出现的程序员呢?但程序员也不是铁打的,他们也会犯错误。而且对于商业软件来说,在上市之前会进行大量的测试,即使有程序错误溜过去了,大多也可以通过打补丁来修复。

但是对于某些软件来说,情况就麻烦得多了。


无妄之灾

在1996年的一个不能说的日子,欧洲航天局第一次发射了新研制的Ariane 5运载火箭。在起飞37秒之后,新火箭很想不开地开花了。这令砸了几亿欧元进去的欧洲航天局非常不爽。经过调查,专家组发现,事故的罪魁祸首竟然是短短的一段代码。

Ariane

在Ariane 5的软件中,有一部分代码是直接来自它的前辈Ariane 4。由于Ariane 4当时非常成功,所以大家觉得这样做没什么问题,根据新的参数稍微修改一下代码就好了。问题是,修改并不完全。有一行代码需要将64位浮点数转换成16位整数,他们认为不会出现什么问题,所以没有进行修改。也没有测试这段代码。

就是这行代码,因为Ariane 5比前辈Ariane 4强力得多,于是在Ariane 4上没有问题的这行代码,在Ariane 5上发生了溢出错误:那个64位的浮点数代表的数值超出了16位整数可以表达的范围。在出错后,备用代码系统被启动,其中包含着同样的一行代码。结果就是整个系统被锁死了。更为讽刺的是,这行代码所在的函数,对于Ariane 5来说是不必要的。这场事故完全就是人祸。

经过这场事故之后,欧洲航天局大为震怒,决定要一劳永逸地解决Ariane 5的问题。他们的要求相当大胆:Ariane 5的软件代码,正式使用前要证明它们不会出现毁灭性的错误,比如不会溢出,不会死循环等等。

这其实并非易事。


停机定理

我们复习一下停机问题:是否存在一种算法,给定任意的程序和输入,都能在有限的时间内判断该程序在给定的输入下是否会停止?正是图灵,证明了这一点是不可能做到的。于是,要编写一个能判断程序会不会进入死循环的算法,这是不可能的。但对于其他类型的程序错误,能否用算法判定呢?

很可惜,这也是不可能的。实际上,我们可以将停机问题规约为检测错误的问题。假设我们有一个程序P,能检测某段代码是否会出现除以零的错误,而我们想要借助这个程序判断某个图灵机在给定的输入下会不会停止。我们可以怎么做呢?首先,对于给定的图灵机和输入,我们可以机械化地将它们转化为一段不用除法但能够模拟该图灵机的代码,然后在模拟结束之后,强行计算1/0。我们将这段代码称为T。代码T在执行时会出现除以零的错误,当且仅当图灵机会停机。然后,我们将代码T输入程序P。于是,既然程序P能判定任意的代码会不会出错,那么就相当于它能判定任意的图灵机会不会停机,而这是不可能的。停机问题不存在普遍的算法,也就是说证明代码无误同样没有普遍算法。

但是,欧洲航天局的任务是否完全不可能完成呢?那倒也不是。停机定理只是说明了不存在程序能正确判定所有程序是否会停止,但欧洲航天局只需要证明Ariane 5的软件代码这一个程序不会出错,所以这条路也没有完全被堵死。

那么,有什么办法呢?


抽象释义

虽然我们不能判定所有程序是否不会出错,但我们能有效判定某些程序不会出错。比如说,如果一个程序没有任何循环语句或者跳转语句,那么这个程序最终肯定停止。但如果程序有循环语句又怎么办?这时,我们并不能确定程序会不会停止,而最保险的办法就是说“我不知道”。

这就是抽象释义(Abstract Interpretation)方法的根本:先抽象出程序的某些信息,再对这些信息进行自动分析,来尝试确定程序是否有着我们想要的性质,比如说不会死循环、不会溢出等等。我们不强求完美的分析,不强求能够识别出所有不出错程序。但为了安全起见,我们要求这种分析是可靠的,也就是说,如果分析的结果认为程序有着我们想要的性质,那么这个结论就不会出错。正是因为这样的权衡取舍,抽象释义方法才能正确有效地实行。

Galois Connection

根据抽象出来的信息多少,不同的抽象释义方法判断同一种性质的效果也不一样。一般来说,抽象出的信息越详细,能识别的拥有某种性质的程序就越多,相应地计算时间也越长。如何在性能和识别率之间做取舍,也是一门复杂的学问,对于不同的应用和数据结构,需要开发不同的抽象方法和自动分析算法。

多种抽象方法还有另一个优点。如果某个程序有着我们想要的性质,但是手头上的抽象释义方法又不能确定时,我们可以换用更精细的、利用更多信息的抽象方法。直接改写代码也是一种规避分析失败的方法。例如,我们想要证明某段代码不会出错,但某种抽象释义方法指示在某句代码上可能会有问题,那么我们可以通过修改代码,换用更加谨慎的处理方法,来保证抽象释义方法能确认新的代码不出问题。

抽象释义方法的奠基者是法国的Patrick Cousot和Radhia Cousot。这对夫妻档总结了一些对程序进行自动形式证明的方法,在此之上提出了抽象释义方法,将其形式化严格化。他们对抽象释义方法的推广也功不可没。除了Ariane 5的代码之外,在别的一些关键应用处的代码也利用抽象释义方法进行了至关重要的验证。一个例子是空中客车A380的控制代码,经过Patrick Cousot的一个小组开发的抽象释义软件Astrée验证,证明了这些控制代码运行时,不会产生像死循环、溢出或者被零除之类的一些软件问题,从而也给安全系数多加了一层保险。

Patrick CousotRadhia Cousot

不过,抽象释义方法只能证明程序有着某种我们想要的性质,不能说明程序是否完成了我们希望的任务。有没有办法做到这一点呢?


形式证明

有一种激进的做法:让程序员在编写代码的同时,给出这段代码确实完成了给定任务的数学证明

要给出这种证明,首先要解决的就是如何将“代码完成了给定任务”转换成数学命题。程序代码可以相当容易用逻辑表达,但代码需要完成什么任务,这只有程序员才知道。所以,要让程序员在编写代码的同时给出证明,为的是让程序员能用逻辑的形式确定这个函数的功能,如此才能得到要证明的命题。这种想法不仅仅是数学家的纸上谈兵。对于某些关键系统,多么微小的疏失都会导致极其严重的后果,人们愿意几乎不惜一切代价防止错误的发生,而对于计算机程序而言,又有什么比数学更坚实的基础呢?

要贯彻这种想法,在编写程序之前,必须先选择一种逻辑体系以及描述它的一种形式语言。这种形式语言必须贯穿整个代码编写的过程:先用形式语言描述程序的输入、输出、功能与限制,然后利用这种与形式语言相近的编程语言去具体编写代码,最后还要利用形式语言给出编写的代码能完美无瑕疵地实现所需功能的数学证明。这种做法又被称为演绎验证(deductive verification),是所谓的“形式化验证”(formal verification)的手段之一。

但数理逻辑毕竟不是一门容易的学科,数学证明对于很多人来说大概比编写代码要困难得多。所以,演绎验证多数也只会用在那些不容有失的关键系统,比如说牵涉人数众多的公共交通设施。例如,在1998年开始运营的巴黎地铁14号线,就是一条全自动的地铁,列车上没有司机,安全行驶也全靠传感器和软件,调度也只需要在控制室点点鼠标就能增加或减少投入运营的列车数量。于是,安全在很大程度上在于软件的可靠性。在控制列车的计算机中,某些与乘客安全休戚相关的关键代码是利用演绎验证编写的。在2012年,巴黎历史最悠久的地铁1号线也从人工运营转到与14号线同系列的全自动化系统。现在,这两条地铁线每天接待的人数加起来超过一百万,但从未因为自动化系统的错误导致乘客伤亡。从笔者的经验来说,它们可以算是巴黎最可靠的地铁线。

Paris Metro 14

但仅有代码的正确性可能还不足以保证程序同样正确,因为代码毕竟不是程序,计算机不能直接执行代码。我们需要另一种名为“编译器”的程序。编译器是将程序员写的代码翻译成计算机能读懂的、用机器语言写就的程序。即使代码是正确的,如果编译器有问题,得出的程序还是可能出错。要避免这个问题,我们同样需要利用数学方法加固编译器这一环。

贯彻这种设计理念的一个例子是一个叫CompCert的C编译器,它由法国计算机科学家Xavier Leroy和他的小组编写。编译器的任务就是进行忠实的代码翻译,确保源代码和目标代码的行为一致。这一点至关重要,否则即使代码是正确的,也不能保证编译生成的程序不出问题。然而,现代的编译器在优化模式下,其实并不能确保忠实的编译。CompCert要解决的就是这个问题。在编写CompCert的时候,对于编译程序的每一步操作,都附带一个数学证明,确保代码的语义不变。因此,数学证明的正确性保证了CompCert编译器会完全忠实地将代码翻译成机器语言。

但即使机器语言是正确的,也还不能完全保证最后执行结果的正确性,因为程序总需要输入输出,而这些功能是由操作系统保证的。如果操作系统本身有错误,即使执行的程序本身是正确的,由于操作系统的问题,也不能保证我们看到的结果是正确的。如果想将数学证明的保证贯彻到底,还需要对操作系统下工夫。这就是seL4所做的事情。seL4是一个微内核,可以看成操作系统的核心。它的每一个功能都附带一个数学证明,在对硬件做一定的假设之后,数学证明的正确性可以保证它提供的功能都会产生我们预先设定的行为。只要硬件不出错,seL4就会正确运行。

当然,一个自然的问题是,如果硬件出错怎么办?硬件的错误可以分为逻辑性错误和物理性错误。前者例如Intel当年在芯片上除法的错误,现在主流硬件厂商早已吸取教训,用演绎验证的方法加固他们的硬件设计;后者例如宇宙射线令硬盘数据出错,这即使是多复杂的证明也避免不了,只能自求多福。尽管数学方法不能保证错误不存在,但至少将可以避免的问题全数避免,这本身就有着莫大的价值。

Real programmers, xkcd
(或者可以利用宇宙射线……?)

概率:了解不确定性

本文已发表于《科学·24小时》2015年11月号,未经书面许可,禁止转载。本文同时在科学松鼠会发表,地址:http://songshuhui.net/archives/93539

“概率”这两个字,除了课本以外,最常出现的地方也许就是天气预报中的“降水概率”,也就是未来几天下雨的可能性有多大。在数学中,概率论是专门研究“可能性”的一门分支。它涉及的问题非常广泛,内容远远超出了中学课本里那些刻板的习题。一切随机或者不确定的事件,都是概率论研究的范畴。上至气象下至金融,甚至连“磁铁的磁性怎么来的”这种物理问题,都可以用概率的方法来研究。

但这门学科的诞生却有些“不太光彩”。


来自赌博的问题

在1654年的一天早上,法国数学家布莱兹·帕斯卡收到了他的朋友贡博的一封来信。这位朋友自称“来自梅雷的骑士”,也算是一位业余数学家。他向帕斯卡提出了类似如下的问题:

两位贵族A与B正在进行一场赌局,赌注是每人500法郎,两人轮流掷硬币,得到正面则A得一分,反面则B得一分,每一局两人得分的机会相等,谁先得到6分谁就得到1000法郎。两人激战正酣,比分达到2比4之际,B突然有事需要终止赌局。赌注应该如何分配才最公平。

这一类问题被称为点数分配问题,早在16世纪就被研究过,但数学家当时的答案并不令人满意,在一些极端情况下会给出非常不合理的分配方案。也许这位“梅雷骑士”也见识过现实中这种赌局引起的矛盾,他希望帕斯卡能够解决这个问题。

帕斯卡对这个问题也很感兴趣。他向另一位业余数学家皮埃尔·德·费马发去一封信讨论这个问题。作为“业余数学家之王”,费马很快就给出了一个答案。他认为,不能单靠赌局停止时的比分或者各自获胜需要的分数来决定赌注的分配,而是应该考虑所有比赛的可能性中,双方获胜的比例。但列举所有的可能性的计算量非常大,帕斯卡继而提出了一个简化算法,完美地解决了点数分配问题。

实际上,他们的解答相当于计算两位玩家胜利概率的大小。在研究中,帕斯卡提出了“数学期望”的概念和著名的“帕斯卡三角形”(杨辉三角)。某个结果为实数的随机事件的数学期望,也就是所有结果按照发生概率加权之后的平均值。数学期望这个概念,掀开了概率论研究的序幕。


什么是概率?

很多概率问题有着特别的结构。对于某个非常简单的随机事件,比如说掷硬币,我们知道每种结果出现可能性的大小,这样的事件被称为“基本事件”。我们可以多次重复这些基本事件,假定它们发生的可能性不会改变,而且这些重复没有相互影响。如果我们将这些基本事件以合适的形式组合起来,就能得到一个更为复杂而有趣的系统。许多概率问题实际上就是对这些随机系统的各种性质的研究。比如说,在点数分配问题中,基本事件就是硬币的投掷,而系统则是赌局的具体规则,最后我们希望知道的则是每一方胜利的可能性大小。

在概率论发展的早期,数学家研究的问题大多比较简单,基本事件只有有限几种结果,组合的方式也相对简单。这样构成的随机系统又叫古典概型。随着数学的发展,数学家开始考虑更复杂的模型。18世纪的法国数学家布丰提出了这样一个问题:在数条间隔相等的平行线之间,随机投下长度与间距相等的一根针,它与这些平行线相交的概率是多少?在这里,因为角度与距离都是连续的值,基本事件有无数不同的结果,这样的随机系统被称为几何概型。

早在19世纪,概率论已经成为了一门枝繁叶茂的数学分支。有趣的是,“概率”这个概念的严格定义要等到20世纪才出现。对于古典概型,因为结果数量有限,概率的定义并没有含糊之处,但几何概型的情况更为复杂。考虑这样的一个问题:圆中的一条随机的弦,它的长度比圆内接正三角形的边长更长的概率是多少?这个问题又叫贝特朗悖论,它奇怪的地方在于,对于不同的选取“随机的弦”的方法,得到的概率也不相同,到底谁是谁非?要等到1933年,俄国数学家柯尔莫哥洛夫为概率论建立公理体系之后,这个问题的解答才变得昭然若揭。柯尔莫哥洛夫将概率模型建立在某一类所谓的“σ代数上的测度”上,这样的测度可以有很多种,不同的测度对应着不同的“随机”。而在贝特朗悖论中,选取随机弦的方法实际上对应着不同测度的选取,也就是不同的“随机”概念,那自然会得到不同的结果。

而到了现在,概率模型的种类越来越多也越来越复杂,系统可以包含无限个基本事件,而具体的组织方式也更复杂更有趣。随机图、渗流模型、自回避行走,这些概率模型早已不能用古典概型和几何概型来概括。也正因为有了这些复杂的模型,我们才能用概率论解决现实世界的种种难题。


无处不在的分布

如果让数学家评选概率论中最重要的定理,桂冠可能非中心极限定理莫属。它不仅是概率论中许多重要结果的基石,在别的学科中,尤其是计算机科学,它也有重要的应用,而在现实生活中,它是整整一个行业赖以生存的理论基础。

中心极限定理其实不止一个,可以说它是一连串定理的总称。它可以看作所谓“大数定理”的细化与推广。假设我们有一枚硬币,它掷出正反面的概率相等。那么,如果我们连续抛掷这枚硬币一万次,常识告诉我们其中大概有五千次是正面。这就是大数定理:对于某个基本事件独立地重复多次的话,某个可能性发生的次数占总数的比例会趋近于这个可能性发生的概率。

与大数定理不同的是,中心极限定理处理的是那些结果是实数的随机基本事件。它告诉我们,如果将许多相同而又独立的基本事件的结果取平均的话,这个平均值会趋向某个概率分布。根据大数定理,这个分布的数学期望就是基本事件的数学期望。而中心极限定理额外告诉我们的,就是这个概率分布必定是一个所谓的“正态分布”,而它的方差,也就是概率分布的“分散”程度,是基本事件的方差除以事件数目的平方根。也就是说,基本事件越多,平均值的不确定性就越小。将这个正态分布画成曲线的话,它就像一个大钟,中间高,但两头呈指数衰减,这也为它赢得了“钟形曲线”这个形象的名字。中心极限定理可以推广到取值范围是高维空间中一点的情况,“相同的基本事件”这个要求也可以被更弱的条件代替,只需要基本事件满足某些要求,而不需要完全相同。

正态分布在自然界中随处可见,比如说人的身高和智力都服从正态分布。这是因为自然界中的很多现象都由各种因素千丝万缕的联系而决定,其中没有特别突出的因素。比如说人的身高,除了由许多不同的基因调控以外,后天的营养、环境、健康,甚至偶然的意外,都有着各自的影响。在这种情况下,如果将每个因素看成一个基本事件,并且假定这些因素各自的影响都差不多,将这些因素综合考虑,根据中心极限定理,得到的结果就非常接近正态分布。

中心极限定理也是保险这一整个行业的基础。每个人都会遇到各种各样的风险,比如事故、疾病等等,这些风险发生的概率都很低,但一旦发生,后果非常严重,并非每个人都能承受。而保险业,实际上就是通过保费与保险赔付的方式,将上千万人连结起来,每人付出相对小的代价,在万一不幸袭来时,就能获得一定的保障。由中心极限定理,这样由数量庞大的个案相加而成的保险业务,由于偶然因素导致无法赔付的概率非常小,而且参与的人数越多,风险就越小。为了确定保费与赔付,保险公司要做的就是根据大量统计数据精确地确定意外发生的概率,然后根据意外概率与收益确定保费与赔付的金额。这也是为什么现代的保险公司越来越重视概率与统计。


理解复杂世界

除了与不确定性相关的问题之外,概率论也与物理息息相关。法国物理学家皮埃尔·居里在攻读博士学位时,就发现了磁铁的一个有趣的性质:无论磁力多强的铁制磁铁,在加热到770摄氏度时,都会突然失去磁性。这个温度后来被称为铁的居里点。为什么磁铁会突然失去磁性?通过概率论与统计物理,我们现在明白,这种现象与冰雪消融、开水沸腾相似,都属于相变的范畴。

我们可以将磁铁里的铁原子想象成一个一个的小磁针。在磁铁还有磁性时,这些小磁针齐刷刷地指向同一个方向,但因为分子热运动的关系,每个小磁针都会时不时地动一下,但很快会被旁边的小磁针重新同化。物理学家将这个场景抽象成所谓的伊辛模型,通过对伊辛模型的研究,概率学家发现,当温度达到某个临界值时,整个体系就会由于热运动而不能保持统一的指向,也就是失去磁性。这个临界值就是居里点,而这样的对伊辛模型的研究也部分揭示了磁铁的一些微观结构的成因。

相变不仅仅局限于物理现象。流言的传播,传染病的爆发,还有微博的转发,都是一种相变过程,都存在某种临界值。比如说传染病,在适当的模型下,如果每个病人传染人数的平均值低于某个临界值,那么疾病就能被控制;如果高于临界值,就很可能导致疫病的全面爆发。对于疾病传播的研究,属于流行病学研究的范畴,而在概率论被引入流行病学研究之后,我们对如何防止与控制疫病爆发有了更深入的了解,这是能挽救成千上万人的知识。

概率论的应用远远不止这些,大至飞机失事搜救,小至垃圾邮件过滤,都能在其中找到概率论的身影。这个复杂的世界充满了不确定性,有些无伤大雅,有些却能致命。要驾驭这些不确定性,就要从了解它们开始。这就是概率论的意义。概率论不能为我们带来一个没有风险的世界,但它却能教会我们如何与风险和平共处。它带来的仅仅是关于不确定性的知识。

但知识,往往就是力量。

编织宇宙的三角形

本文已发表于《科学·24小时》2015年11月号,未经书面许可,禁止转载。本文同时在科学松鼠会发表,地址:http://songshuhui.net/archives/93549

这是一枚行将就木的恒星,在发出黯淡红光的虚胖外壳之下,犹如洋葱般一层套一层,而最深处核心中的燃料早已消耗殆尽,再也释放不出任何能量。外壳失去了支撑后,被恒星引力拉向核心,坍缩开始了。由铁组成的高密度内核不堪重负,电子被压进原子核,在弱相互作用力下,与质子结合变成中子,放出中微子。内核就此被压缩成由中子构成的中子星,而多余的能量被转化为高能粒子,形成一道向外的激波,直面向内坍缩的外层。两者冲击,迸发出摧毁整个恒星的力量,外层被吹散到星际空间之中,散发着媲美千亿个太阳的光芒。在这个过程中,由核反应产生的中子、质子和α粒子,克服着电磁斥力,射进了形形色色的原子核中,在强相互作用力下融合为更大更重的原子核,为生命提供了材料。

超新星遗迹

超新星爆发,宇宙中最壮丽的景象,但演员只有四个:引力、电磁力、强相互作用力、弱相互作用力。不仅如此,世界上所有的现象,不外乎是这四种力的演出。

苹果落地,瀑布激扬,在生活中最常察觉到引力,但引力却最难捉摸。对于其余三种力,物理学家都已经发展出近乎完美的理论,揭示出它们量子化的本质,这些理论能解释许多实验现象,但唯有引力格格不入。爱因斯坦的广义相对论是目前关于引力最好的理论,但数十年来物理学家绞尽脑汁,都无法将它与描述其余三种力的量子场论融合起来。这是当今物理学中最引人注目的难题:如何将广义相对论量子化。

广义相对论告诉我们,引力不过是时空的反映。要将它量子化,最自然的想法就是建立一个量子时空的模型。


平面上的引力

我们的时空有四维,三维空间加一维时间。要一下子建立四维的量子时空太困难,事情要从简单的做起,物理学家于是将目光投向了二维空间。要建立量子时空,第一步就是将时空分割成一个个很小的单元,也就是“时空量子”。量子力学的一大特点就是不确定性,在最小的普朗克长度之下,只有概率分布的存在。所以,时空量子的分割方式必须是概率性的,而量子时空在本质上必然不是一个确定的实体,而是不停改变的一种概率模型,这就是概率学家大显身手的地方。

最简单的想法,就是将二维平面分割成一个个小三角形,这又叫平面的三角剖分。时空无限,所以这样的剖分必定包含无数个小三角形,而由量子力学的不确定性,不同的分割方式出现的概率应该相等。但既然小三角形有无限个,分割方式也有无限种,怎么确保它们出现的概率相等呢?概率学家先从给定个数的三角形出发,这时剖分只有有限个,自然可以给它们赋予相同的概率。然后,只要让三角形的个数趋向无限,可以证明,在某种意义上,这些三角剖分的概率分布会趋向某个连续的极限。概率学家将这个极限称为“一致无限三角剖分”,简称UIPT,这就是物理学家们需要的模型。

三角剖分

概率学家们发现,UIPT拥有很多有趣的性质。首先,它拥有某种分形结构,如果将它的一部分适当地放大,会得到与原来相似的三角剖分,我们甚至可以计算它的分形维度。但这也仅仅是相似而已,因为如果任取一部分,其中几乎必然仅仅包含有限个小三角形,但原本的UIPT拥有无限个三角形。与此相对的是,即使很小的区域,其中也可能包含数量庞大的小三角形。如果将UIPT画成球状,它就像一只刺猬,凸出来的“刺”实际上就是这些三角形密集的地方。

你也许会问,为什么要分割成三角形,而不是四边形或者别的多边形?实际上,概率学家也研究别的分割模型,比如四角剖分。但物理学家认为,无论选取什么样的最小单元,最终得到的极限的物理性质都是相似的。也就是说,这些“无限剖分”模型的许多性质有着一种普适性,无论最小单元有着什么特殊的性质,一旦将镜头拉到无限远,整个空间拥有的性质并不因此改变。也就是说,概率学家可以选择任意的模型来研究,得出的结果大部分也能应用到其他模型。


从平面到时空

但时空量子化的方式不止一种。量子场论向来是物理学家手头的利器,引力之外的其余三种力都属于量子场论管辖的范畴。对于在二维平面上的量子引力,他们猜想它会遵循所谓的“共形量子场论”。虽然处理的对象仍然是空间中的某种概率分布,但在场论的框架下,物理学家手头能用的工具却要多得多。他们发现,有一种被称为“高斯自由场”的共形场论,它不仅能满足物理学上的要求,而且与UIPT有着许多共同的性质。概率学家家猜想,两者也许是同一种量子引力模型的不同表达,外表的分歧仅仅来源于侧重点的不同。对于物理学家来说,这也许已经是公认的事实,但目前还欠缺严格的数学证明。物理学家还有另外一个猜想:无论是高斯自由场还是UIPT,两者也许都服从同一个被称为KPZ关系的概率模型。这也许就是证明前一个猜想的钥匙。

高斯自由场

当然,我们生活在四维时空,而不是二维。研究者当然不会止步于二维量子引力。近年来,一些研究者正在向高维量子引力发起攻势。他们将三角剖分中处于平面内的小三角形,换成处于四维空间中的所谓“单纯复形”,然后用相似的方法将这些小砖块粘合成空间整体,构建起一个高维空间量子化的概率模型。因为维度更高,这样的概率模型研究起来更为复杂,需要解决许多技术性问题。

作为研究领域,量子引力还很年轻。它连接着概率论与物理学,现在已经成为热门的研究方向之一。这个领域有着光辉的前景,也有许多需要解决的难题。但我们相信终有一天,物理学家与概率学家会携手告诉我们,宇宙是由什么样的概率结构编织而成的。


所有图片来自Wikipedia

计算的极限(十一):黄金时代

本文遵守首页的CC版权声明:署名-非商业性使用-禁止演绎,请自觉遵守,非授权请勿转载。

本文在科学松鼠会发表,地址:http://songshuhui.net/archives/93368

计算无处不在。

走进一个机房,在服务器排成的一道道墙之间,听着风扇的鼓噪,似乎能嗅出0和1在CPU和内存之间不间断的流动。从算筹算盘,到今天的计算机,我们用作计算的工具终于开始量到质的飞跃。计算机能做的事情越来越多,甚至超越了它们的制造者。上个世纪末,深蓝凭借前所未有的搜索和判断棋局的能力,成为第一台战胜人类国际象棋世界冠军的计算机,但它的胜利仍然仰仗于人类大师赋予的丰富国际象棋知识;而仅仅十余年后,Watson却已经能凭借自己的算法,先“理解”问题,然后有的放矢地在海量的数据库中寻找关联的答案。长此以往,工具将必在更多的方面超越它的制造者。而这一切,都来源于越来越精巧的计算。

计算似乎无所不能,宛如新的上帝。但即使是这位“上帝”,也逃不脱逻辑设定的界限。

第一位发现这一点的,便是图灵。

计算的极限(零):逻辑与图灵机
计算的极限(一):所有机器的机器,与无法计算的问题
计算的极限(二):自我指涉与不可判定
计算的极限(三):函数构成的世界
计算的极限(四):机械计算的圭臬
计算的极限(五):有限的障壁
计算的极限(六):无穷的彼岸
计算的极限(七):宛如神谕
计算的极限(八):符号的框架
计算的极限(九):叹息与奋斗
计算的极限(十):无限绵延的层级


“我要借了阿尔志跋绥夫的话问你们:‘你们将黄金时代的出现豫约给这些人们的子孙了,但有什么给这些人们自己呢?’”

——鲁迅

黄金时代

但波斯特并没有能够亲眼在《数学年报》看到他和克林的这篇论文。

双相情感障碍一直困扰着他,即使每天只工作三小时,即使用尽办法平伏情绪,每得到一些新的数学结果,这些发现和创造都让他激动不已,处于症状发作的边沿。对于数学家来说,这可能是最扭曲最恶毒的诅咒。数学家的使命在于发现新的数学,这种发现必然带来的喜悦,对于波斯特来说,却会危及他为了发现数学所必须的清醒头脑。

在1954年初,又一次的发作将他带到了纽约的一家精神病院。当时治疗精神疾病的主要疗法有两种,波斯特接受的是电休克疗法(http://songshuhui.net/archives/7382),而同样受精神疾病困扰的另一位数学家纳什接受的则是胰岛素休克疗法。电休克疗法在当时还很原始,虽然以相当高的症状缓解率得到了医生的青睐,但原始的疗法过程痛苦可怕,也有一定的副作用。

在1954年4月21日,波斯特接受了又一个疗程的电休克治疗。在他不停抽搐之时,他的心脏失去了控制。

他没有挺过去。

刊登着他和克林的论文的《数学年报》,则是在5月出版,只差不到一个月。

除了波斯特以外,可计算性理论这个领域的其他开拓者,哥德尔、图灵、丘奇这些先驱,他们的结局又如何呢?

由于二战即将爆发,哥德尔在1939年偕同家人移居到了普林斯顿,恰好在图灵回英国之后。之后,他一直作为普林斯顿的教授活跃在数理逻辑学界。但在四十年代后期,他的关注点渐渐从数理逻辑转移到了哲学,也不再发表他的数学工作。可以说,这就是他的数学生涯的终点。而他的人生的终点要等到近四十年之后。在晚年,他的心理变得不稳定,总是怀疑别人要毒害他。在他的妻子因病入院六个月时,他竟然不接受任何人的食物,活活饿死在普林斯顿的医院里。

图灵在1939年博士毕业后回到剑桥,旋即被英国军方聘用,专注破译德军密码,为二战胜利立下了汗马功劳。在战争结束后,他尝试制造一台计算机,但在英国政府的不作为,被在美国的冯·诺依曼抢了先。除此之外,图灵还提出了有关人工智能的图灵测试,并且一直思考前沿的数学问题。作为一名同性恋者,在被警方发现之后,图灵被迫接受治疗。最后在1954年6月8日,他的生命永远地终止了,床边放着一个沾着氰化物的苹果。

丘奇可能是最幸运的人。他一直在数理逻辑这个领域里奋斗,直到生命的尽头,并且硕果累累。这也许是一名数学家能希望拥有的最好结局。他也是一位优秀的博士导师,门下的31位博士中,就有图灵、克林和罗瑟这样的大师。在生命中困扰着他的,也只有晶状体混浊导致的视力问题,与其他几位先驱相比,实在无足轻重。

正因为丘奇卓越的成果,以及其他人的缺席,他以及他的学生在当时的数理逻辑学界中有着举足轻重的影响。自然,丘奇那种过分追求严谨的作风以及他的λ演算在当时也支配了整个学界。但作为计算模型,λ演算不仅不直观,而且过分形式化,很多实际上很简单的结论,用λ演算证明的话会无比繁复。数理逻辑本来就是一门艰深的学科,证明稍稍复杂一些也相对正常。但当图灵机这样直观的模型出现之后,许多定理换用图灵机模型就能被更直观更容易理解地证明,但许多人由于惯性仍然使用λ演算做研究,即使他们对此也颇有微词。

λ演算在当时的影响之大,就连图灵当时在丘奇门下攻读博士时,毕业论文中用到的计算模型也完全是丘奇的那一套λ演算,尽管他自己提出的图灵机概念更加清晰直观。有些数理逻辑学家甚至认为,图灵的序数逻辑当时不受关注,部分原因要归结于用到了λ演算这套形式语言。就连克林,他自己作为丘奇的学生,也对λ演算很不满意,可能是因为他的文章总是遭到读者的冷遇。他在1935年之后很快就抛弃了λ演算,改为用递归函数的模型来阐述结果,读者的反响果然迅速改善。而丘奇过分严谨的作风对学界的统治,使得图灵和波斯特那种诉诸直观(但能被轻易严格化)的证明,在当时被视为异类。

学界的惯性是强大的。丘奇在1935年提出λ演算,而他追求完全严谨的作风对学界的统治要直到五十年代中后期才开始慢慢松动。其中有两个原因:第一是随着可计算性理论的发展,这个领域的定理越趋复杂,λ演算这个框架在严谨性方面带来的好处,逐渐被它的复杂性所抵消;第二是随着基于图灵机模型的现代计算机的发展,人们对图灵机越来越熟悉,对图灵机的研究也越来越深入,人们对于图灵机模型的使用也越来越得心应手。这两个因素一推一拉,渐渐改变了学界的风气。时至今天,在可计算性理论中,人们更偏向于使用图灵机,而λ演算早已不见踪影。但λ演算并没有就此消失于学术界,人们很快就发现它的另一个用武之地,但这是后话,留待后文详述。

哥德尔、图灵、丘奇、波斯特、克林……这些开创者们,告诉了我们“计算”到底是什么,而计算之外又有什么。我们今天能惬意地躺在床上用平板电脑看视频打游戏,能与千里之外的朋友互通消息,也都部分地归功于他们打下的理论基础。但平心而论,我们给这些开拓者的颂扬还远远不够。在一般人心中,他们仍然寂寂无名。这些开拓者们,生前大多没有什么好的结局,就连死后也没有得到多少廉价的赞赏。他们为我们开拓了一个信息化自动化的黄金时代,但他们又得到了什么呢?

但也许他们也并不在乎。就像少年的波斯特那样,也许在他们眼里,数学比尘世间的一切都要美丽,只有万亿光年外宇宙的奇迹才能与之媲美。

这就是信息时代开拓者们的故事。

当然,数学家并不会停止他们探索的脚步。可计算性理论的下一篇章,将会在大洋彼岸被揭开。但在继续追寻之前,我们先来看看,这些开拓者们的遗产到底给我们的生活带来了什么。

计算的极限(十):无限绵延的层级

本文遵守首页的CC版权声明:署名-非商业性使用-禁止演绎,请自觉遵守,非授权请勿转载。

本文在科学松鼠会发表,地址:http://songshuhui.net/archives/93311

在图灵诞辰100周年之际,献给这位伟大的开拓者。

计算无处不在。

走进一个机房,在服务器排成的一道道墙之间,听着风扇的鼓噪,似乎能嗅出0和1在CPU和内存之间不间断的流动。从算筹算盘,到今天的计算机,我们用作计算的工具终于开始量到质的飞跃。计算机能做的事情越来越多,甚至超越了它们的制造者。上个世纪末,深蓝凭借前所未有的搜索和判断棋局的能力,成为第一台战胜人类国际象棋世界冠军的计算机,但它的胜利仍然仰仗于人类大师赋予的丰富国际象棋知识;而仅仅十余年后,Watson却已经能凭借自己的算法,先“理解”问题,然后有的放矢地在海量的数据库中寻找关联的答案。长此以往,工具将必在更多的方面超越它的制造者。而这一切,都来源于越来越精巧的计算。

计算似乎无所不能,宛如新的上帝。但即使是这位“上帝”,也逃不脱逻辑设定的界限。

第一位发现这一点的,便是图灵。

计算的极限(零):逻辑与图灵机
计算的极限(一):所有机器的机器,与无法计算的问题
计算的极限(二):自我指涉与不可判定
计算的极限(三):函数构成的世界
计算的极限(四):机械计算的圭臬
计算的极限(五):有限的障壁
计算的极限(六):无穷的彼岸
计算的极限(七):宛如神谕
计算的极限(八):符号的框架
计算的极限(九):叹息与奋斗


交错的存在所有

波斯特在演讲中谈到了关于自然数集之间归约的问题,而克林当时也正在研究类似的问题:用不同的逻辑公式定义的自然数集,它们是否不同,又有什么不同?如果在一个关于自然数的逻辑公式P(x)中,只有一个自由变元x,那么,使这个公式成立的所有值组成的集合就是P(x)定义的自然数集。每个自然数集又对应一个判定问题:某个自然数n在这个自然数集中吗?

用这种方法定义的自然数集,它们有着什么样的性质呢?

我们知道,在逻辑公式中,除了我们熟悉的变量和加减乘除,还有一种符号叫“量词”。量词分两种,存在量词\exists 和全称量词\forall ,每个量词都带着一个变元。不要将它们视为洪水猛兽,它们不过是又一些符号而已。存在量词的意思是,只要对应变元的某一个取值能满足命题余下的部分,那么整个命题就为真。比如说,“存在一道菜肴,我可以就着吃三碗饭”,那么只要举出一个例子(当然例子很多,白切鸡、清蒸鱼,不一而足),就能说明这个命题为真。而全称量词的意思恰好相反,它需要对应变元的每个取值都能满足命题余下的部分,那么整个命题才是真的。只要有一个反例,命题就被否定了。比如说,“对于所有的菜肴,我可以就着吃三碗饭”,只要举出一个例子(比如仰望星空派),就能否定整个命题。如果我们否定一个开头是存在量词的命题,得到的命题开头就是全称量词,反之亦然。而克林要研究的,就是这些量词会如何影响命题定义的自然数集。

我们知道,所有一阶逻辑的命题都可以将所有量词整理到命题的开头,对于现在的数学系学生来说,这只不过是一道小小的练习题。所以,我们可以假定所有命题都有着这样的形式。按照开头量词的具体形式,克林将所有有关自然数的命题分成了无穷个类别。没有量词的命题被称为零阶命题,而有量词的命题,它们开头必定由存在量词和全称量词交错组成,这样交错的段数,就是命题的阶数。对于一个n阶命题,如果它的开头是存在量词,我们就称它为n阶存在命题,反之则是n阶全称命题。根据这个定义,我们能轻易看出一个性质:n+1阶存在命题,其实就是n阶全称命题开头加上一些存在量词得到的。而在这个性质中,将“存在”和“全称”两个词反过来,它仍然成立。

(注:在关于自然数的逻辑命题中,还有一种特殊的量词,被称为“有界存在量词”。在n阶命题的定义中,我们忽略这些有界存在量词。)

来自Wikimedia

来自Wikimedia

我们来看一个实际的例子。著名的哥德巴赫猜想说的是,对于每一个大于等于4的自然数,都能被写成两个素数的和。对于某个特定的偶数2n+4,我们能将“2n+4能写成两个素数的和”写成以下的逻辑命题:
\forall a \forall b \forall c \forall d \exists p \exists q. n*2=p+q \wedge (\neg (p+2=a*b) \vee (a = 1) \vee (b=1)) \wedge (\neg (q+2=c*d) \vee (c=1) \vee (d=1))
这个命题是一个2阶全称命题,因为它的量词分两截,而开头是一个全称量词。

克林考虑了所有这些类别的命题能定义的自然数集。他将0阶命题定义的自然数集组成的集合称为\Delta_0 ,而将n阶存在命题和n阶全称命题定义的自然数集组成的集合分别称为\Sigma_n \Pi_n 。克林证明了,这些集合组成了一个向上无限绵延的层级,每一层都是自然数集组成的集合,阶数越高,命题能定义的自然数集也越多,表达能力也越强。对于每一层,总有存在这样的集合,它只能被这一层及以上的命题定义,而不能被下方更弱的层定义。也就是说,层级之间的包含关系是严格的。

也许不出大家的意料,克林证明这一切的方法,仍然是康托尔的对角线法。他定义的这个层级,今天被称为算术层级(Arithmetic Hierarchy),是数理逻辑中的一个重要概念。

arith-hierarchy

克林的这项工作,给了波斯特非常大的启发。这是为什么呢?

我们先来看看\Delta_0 到底是什么。假设集合S是\Delta_0 中的元素,那么存在一个只有单个自由变元的但没有量词的命题P(x),某个自然数x属于S当且仅当P(x)为真。那么,对于某个特殊的自然数,比如说42,要判断它是否属于S,只需要将42代入命题P(x)中检查即可。既然P(x)没有量词,那么只要硬算,就必然能得到答案。也就是说,我们有一个算法,它一定会停止,而当它停止时,就能得到答案。记忆力好的读者能观察到,这种算法就是所谓的递归函数。

那么,\Sigma_1 是什么呢?它涉及的命题拥有\exists a. P(x,a) 的形式,其中P(x,a)是一个\Delta_0 中的命题,如果将a看成一个符号的话。那么,要判断这个命题对于某个特殊的x值是对是错,最直接的方法就是先将x值代入命题中,然后对于存在量词中的变量a,从0开始枚举每一个值,然后将这个值代入P(x,a)中,命题中就再也没有自由变量,可以直接硬算它是对是错。一旦找到了某个a的值,使得P(x,a)为真,那么根据存在量词的定义,我们就能判定整个命题为真;但如果命题对于我们的x值来说不为真,那么这样的a值不存在,我们就得一直枚举下去。这是一个不一定会停止的算法,但它仍然是一个算法,而它定义的集合也就是可计算的。

那么,不可计算的问题,比如说停机问题,它又在哪个层级呢?可以证明,停机问题相关的命题可以在更高的\Sigma_2 层级中表达出来。既然层级无限绵延,那么我们自然会提出这样的问题:更高的层级中的问题到底是什么?换句话说,既然有些问题的层级比包含停机问题的\Sigma_2 更高,那么,这是否说明有些问题比停机问题更难?

波斯特之前的工作聚焦于难度处于可计算问题与停机问题之间的问题,但克林的工作促使他将目光投向另一个方向:难度比停机问题更高的计算问题,在图灵归约之下,它们有着怎样的结构?


无法触及的世界

我们先复习一下图灵归约的概念:考虑一台谕示机M,假设它带有问题A的谕示,如果它能解决某个问题B,那么我们说问题B能被图灵归约到A,记作B \leq_T A 。这跟开卷考试很类似,一位学生如果参加关于问题B的开卷考试,却带错了关于问题A的参考书,如果这位学生仍然能借助这本参考书完美地完成考试,那么我们可以说问题B不比问题A难。如果问题B能被图灵归约到A(B \leq_T A ),同时A也能被图灵归约到B(A \leq_T B ),那么我们说A和B是图灵等价的,记作B =_T A

图灵等价是一种等价关系:如果A图灵等价于B,而B图灵等价于C,那么A也图灵等价于C。我们可以将那些相互之间图灵等价的问题归为同一类(数学术语是等价类)。这些类别,被称为“图灵度”,它们之间可以通过图灵规约来比较难度,可以说,在同一个图灵度中的判定问题,在图灵规约的意义下,难度都是相同的,而带有其中任意一个问题的谕示,给谕示机带来的能力都是相同的,可以互相置换。

那么,这些图灵度到底看起来是什么样子的呢?

显然所有的可计算的判定问题都是图灵等价的,因为“可计算”的定义就是“存在图灵机可以解答”,既然一般的图灵机足以解答,那么任意的谕示机当然也可以。因为这些判定问题对于图灵机来说过于简单,不需要谕示就能完成,所以谕示的内容反而变得不重要,带有一个可计算谕示与没有谕示,对于图灵机来说是一样的。同样,任意的可计算判定问题都能图灵规约到任意的判定问题。可以说,在图灵规约的框架下,可计算判定问题就是那些最“简单”的问题,它们组成了最“容易”的图灵度,被记作\boldsymbol{0}

那么,停机问题又如何呢?图灵证明了任意的图灵机都不能解决停机问题,同样,带有一个可计算谕示的谕示机当然也不能解决,因为这样的谕示机与一般的图灵机的计算能力是相同的。也就是说,停机问题不能规约到任何一个可计算的判定问题,也就是说,停机问题比那些可计算的问题要严格地难,或者说,停机问题与可计算问题不在同一个图灵度。所以,我们至少有两个图灵度,一个是可计算的\boldsymbol{0} ,另一个是停机问题所在的图灵度,记作\boldsymbol{0}'

那么,如何构筑更难的问题呢?

图灵在他的博士论文中发现,在停机问题不可计算的证明中,将所有的“图灵机”全部换成“带有‘数论问题’的谕示机”,其他部分不易一字,得到的证明仍然正确。从而他证明了所谓的“数论问题”并不包含所有的计算问题。在这里,图灵选取了“数论问题”这个谕示,但实际上,无论选取什么计算问题的谕示,将它代入原来的证明,得到的证明仍然成立。也就是说,对于任意的判定问题A,带有问题A谕示的谕示机是否会停机,这个判定问题是不能用带有问题A谕示的谕示机解决的。如果问题A是某个图灵度\boldsymbol{a} 中的判定问题之一,刚刚的判定问题必定属于某个更高的图灵度,我们将它记作\boldsymbol{a'}

(注:顺带一提,类似这样可以将“图灵机”换成“谕示机”的证明被称为可相对化的证明(relativizable proof)。这个概念的变体在P与NP问题中占据着重要的地位。更精确地说,在所谓的“多项式归约”的概念下,解决P与NP问题的证明不可能是可相对化的。这个结论又被称为“可相对化障碍”。)

这就是波斯特构筑越来越难的图灵度的方法。对于某个图灵度\boldsymbol{a} ,考虑带有其中问题之一的谕示的谕示机,有关的停机问题处于另一个更高的图灵度\boldsymbol{a'} ,这个图灵度被称为原来图灵度的图灵跳跃(Turing jump)。从可计算问题\boldsymbol{0} 开始,通过图灵跳跃,波斯特能够一步步构建与克林的算术层级相似的图灵度层级,除了最底层的\boldsymbol{0} 以外,每一个层级都对应着那些不可计算的问题,而且层级越高,问题越难。

实际上,波斯特的图灵度层级与克林的算术层级之间的联系,比我们想象中的更深刻。我们定义\boldsymbol{0}^{(n)} 为从最底层的\boldsymbol{0} 出发,经过n次图灵跳跃得到的图灵度。波斯特证明了,如果将判定问题与自然数集等同起来,那么可以说\boldsymbol{0}^{(n)} 恰好处于\Sigma_{n+1} \Pi_{n+1} 的交集之中。也就是说,图灵度层级实际上与算术层级紧密地缠结着,图灵度层级中的每一层恰好处于算术层级的两层之间。

但图灵度层级实际上比算术层级延伸得更远。在算术层级的定义中,第n层是由那些拥有n段不同量词的命题构成的,因为命题的长度有限,所以n只能是自然数。在这里,n表达的是数量,也就是基数。但在图灵度层级中,定义的方法则是通过图灵跳跃,是一种顺序关系。在\boldsymbol{0}^{(n)} 这一层中,编号n实际上是一个序数。实际上,与康托尔的导集以及图灵的序数逻辑相似,图灵度层级实际上可以延伸到“无穷之外”,只有用超穷的序数才能表达所有这些层级。

也就是说,尽管人力能及的只有可计算的问题,但通过逻辑推演,我们能认识到,在那些我们无法解答的问题中,竟然还存在着一个精巧的结构。而正是波斯特,向我们首次展示了这个无法触及的世界。


无限绵延的层级

波斯特很快就将他的部分发现以摘要的形式发表在1948年的《美国数学学会通报》上。克林读到了这篇摘要,自然为波斯特的新发现而兴奋,但他对这份摘要并非毫无意见。

数学家尽管做的都是数学,但他们的处事方式却是各式各样。在提笔写作方面,有的数学家勤于下笔,每获得了新的结果,就会很快写出论文,并通过期刊或者私下流通预印本的形式让同行尽快知道他的结果;有的数学家却惜字如金,即使有了一整套新结果,也记录了相关的定理和证明,但却迟迟不肯下笔,也许是希望更好地打磨这些结果。著名数学家埃尔德什和欧拉是前者的典型代表,两者分别是数学史上发表论文第一和第二多的数学家。而同样著名的高斯和怀尔斯则是后者的典型代表。高斯是个完美主义者,他希望他的著作中毫无瑕疵,“将所有的脚手架去掉”,于是他发现的结果往往在抽屉里一躺就是几年,直到高斯终于满意他的写作,或者别的数学家再次发现这个结果为止。而怀尔斯独自一人在八年时间内钻研,完成费马大定理的证明主体,这早已传为佳话,被认为是怀尔斯坚韧性格的证明。这些不同的风格,也许在不同的环境下有着不同的适应性,但却没有绝对的对与错之分。

波斯特属于惜字如金的那个类别,但与高斯和怀尔斯不同,他喜欢在发表的论文中提及他已经得到的结果,承诺会写出相关的论文,但这个承诺却迟迟不见兑现的踪影。在他发表的这篇摘要里,他除了提到上述超穷的层级结构之外,还提示了更多的结果。也许波斯特是想吊一下别的数学家的胃口,但对于同样在这个领域工作的人,这很不公平。如果你也是研究这个方向的学者,你读了波斯特的这篇文章,可能希望在这些结论上生发出更深入的定理。但因为这些结论的证明并没有正式发表,你并不知道波斯特的这些结论到底是有凭有据,还是仅仅是虚张声势,从而陷入想用但没法用的两难境地。更糟糕的是,如果你发现了相同的结论,希望发表的话,又会出现优先权之争,而这是大家都不希望看到的。无论如何,仅仅提示结果而长久拖延正式论文的发表,对学术整体的发展相当不利。

克林对波斯特这篇摘要的意见也正在于此。他给波斯特写了一封信,除了赞扬他的结果以及一些讨论之外,还提及了不发表的这个问题。克林的信也许使波斯特的良心有些不安,他很快给克林寄去了一份包含他的新结果的手稿。这份手稿延续着波斯特一直以来的风格:依赖直觉,不太严谨,结构也很凌乱。因为这是一份手稿,混乱程度更甚。波斯特自己可能也知道这一点,他给克林的建议是:找个研究生,让他把内容整理出来,然后以合作者的身份一起发表这篇文章。克林依计行事,但这份手稿实在是太难理解,克林找来的研究生实在无能为力,最后克林只好捋起袖子自己动手。

克林是丘奇的学生,也继承了丘奇的那种追求严谨的研究风格。当年丘奇对严谨性的要求曾经让更依赖直觉的图灵吃了不少苦头,这次轮到克林被波斯特的手稿中的各种直觉描述所困扰了。但最终,克林还是将手稿中的内容整理出来,将缺少的证明补齐,并且做了一些延伸的研究,最后写成了一篇论文:

《递归不可解度的上半格》(The upper semi-lattice of degrees of recursive unsolvability)。

所谓的“递归不可解度”,其实就是不可计算的那些图灵度。而“上半格”是一种序结构。波斯特与克林证明了,所有图灵度其实组成了一个非常复杂但有序的结构。我们此前看到,通过图灵跳跃得到的图灵度层级与算术层级关系非常密切,但与算术层级不同的是,在每个图灵度层级之间,还有更加令人惊讶的结构存在,也就是说,阶梯与阶梯之间并不是空无一物,还有更多的结构蕴含其中。这也是显然的,因为自然数的子集有不可数无穷个,但每个图灵度中最多包含可数个子集。所以,图灵度的个数是不可数的,比我们想象中的无穷还要多得多。图灵度层级必然不能概括所有图灵度的结构,那么,必然有更多的结构存在于层级之间。

假设\boldsymbol{a} 是一个图灵度,而\boldsymbol{a'} 是它的图灵跳跃,我们来看看这两层阶梯之间到底有些什么。波斯特与克林证明了,\boldsymbol{a} \boldsymbol{a'} 之间,存在可数无穷个图灵度,它们之间互相不能比较,但都处于两层阶梯之间(用数学术语来说,就是两个图灵度之间至少存在一条可数无穷的反链)。同样在这两层阶梯之间,存在至少一条由图灵度构成的链,其中每个图灵度都可以相互比较,而更有趣的是,对于其中任意两个不同的图灵度,比如说\boldsymbol{c} \boldsymbol{d} ,假设\boldsymbol{c} \boldsymbol{d} 要难,那么这条链之中必定存在另一个图灵度,它的难度处于两者之间,比\boldsymbol{c} 要简单,但比\boldsymbol{d} 要难。用数学的术语来说,就是这条链是稠密的。也就是说,在图灵度层级之中的每两层之间,不仅存在着无数种方法从一层逐级攀登到另一层,而且在某些路径上,有一部分的路程不是常见的一级一级分立的阶梯,而是连续的无可割裂的斜坡。所有图灵度组成的结构,比我们能想像的还要复杂得多。

这篇论文,最终发表在久负盛名的《数学年刊》(Annals of Mathematics)上。可以说,它开创了图灵度研究这个新领域。到现在,图灵度理论已经成为了数理逻辑中非常活跃的一门分支,而其中主要的研究方法——被称为“优先方法”——它的一种雏形同样起源于这篇文章。

这就是作为数学家的波斯特,他的数学研究的顶峰。

计算的极限(九):叹息与奋斗

本文遵守首页的CC版权声明:署名-非商业性使用-禁止演绎,请自觉遵守,非授权请勿转载。

本文在科学松鼠会发表,地址:http://songshuhui.net/archives/93245

在图灵诞辰100周年之际,献给这位伟大的开拓者。

计算无处不在。

走进一个机房,在服务器排成的一道道墙之间,听着风扇的鼓噪,似乎能嗅出0和1在CPU和内存之间不间断的流动。从算筹算盘,到今天的计算机,我们用作计算的工具终于开始量到质的飞跃。计算机能做的事情越来越多,甚至超越了它们的制造者。上个世纪末,深蓝凭借前所未有的搜索和判断棋局的能力,成为第一台战胜人类国际象棋世界冠军的计算机,但它的胜利仍然仰仗于人类大师赋予的丰富国际象棋知识;而仅仅十余年后,Watson却已经能凭借自己的算法,先“理解”问题,然后有的放矢地在海量的数据库中寻找关联的答案。长此以往,工具将必在更多的方面超越它的制造者。而这一切,都来源于越来越精巧的计算。

计算似乎无所不能,宛如新的上帝。但即使是这位“上帝”,也逃不脱逻辑设定的界限。

第一位发现这一点的,便是图灵。

计算的极限(零):逻辑与图灵机
计算的极限(一):所有机器的机器,与无法计算的问题
计算的极限(二):自我指涉与不可判定
计算的极限(三):函数构成的世界
计算的极限(四):机械计算的圭臬
计算的极限(五):有限的障壁
计算的极限(六):无穷的彼岸
计算的极限(七):宛如神谕
计算的极限(八):符号的框架


时代逝去的叹息

波斯特断言,存在一些形式系统,我们无法在有限的时间内知道其中某个命题能不能被证明或否证。可以说,他的断言与10年后哥德尔的不完备性定理非常相似。那么,为什么在数学史中,“不完备性定理”前面的名字不是波斯特,而是哥德尔呢?因为波斯特虽然在1921年得到这个结果,但要等到1943年,在哥德尔、图灵、丘奇的黄金时代过去之后,才得以在极省略的篇幅下发表。

他没有跟上时代的节拍。

当时的美国数学界普遍对数理逻辑没有太大的兴趣,波斯特与他的导师凯泽在当时算是异类。要等到第二次世界大战前夕欧洲数学家大幅迁移到美国,这种状况才开始改变。波斯特曾经将他的想法写成上下两篇论文,并且将上篇提交到《数学年刊》(Annals of Mathematics)。但他得到的回复十分令人失望,同行评议的报告对是否应该发表各执一词,而编辑部也没有给出具体的决定。如果没有上篇的理论奠基,那么下篇就仅仅是空谈。

但无人问津还不是最致命的问题。实际上,波斯特根本没有一个实打实的证明。也就是说,他并没有实际证明他的结论,那只是一种推测再加上关于证明的一些想法而已。虽然以我们的后见之明来看,他的结论与想法都是正确的,但他毕竟没有一个能让别人详细检验的证明。

在数学界,证明就是一切。没有证明,即使看上去再确定无误的结论,哪怕拥有再多的间接证据,哪怕是最优秀的数学家的想法,都只能是猜想,而不是定理。要确立一个定理,就必须有一个滴水不漏的证明。这就是数学界的规则。而很不巧,波斯特的研究风格比图灵更依赖直觉,换种说法就是更不严谨。波斯特的直觉足以预见超越时代的结论,但他却没有对应的能力来将他的直觉在当下整理为严谨而有条理的证明。他的雄心壮志超越了哥德尔,甚至超越了图灵与丘奇,但他当时没有足够的工具,也没有足够的能力来完成这样远大的目标。

但也许波斯特多花些时间整理他的思路,就能写出完整的证明来说服数学界。可惜命运没有给他这样的机会。

就在波斯特取得突破之后不久,也许是由于这个结果的冲击性太大,他的心理失去了平衡。而论文未能成功发表更是为这种失常雪上加霜。他患上的是双相情感障碍,患者会在无端愉悦与无故抑郁中震荡。此后十多年,他一直受双相情感障碍的困扰,在数学上毫无产出,申请到的大学教职也因为发作而不得不放弃。这段时期,他只能当一名中学教师聊以糊口。直到1935年,他才算是回到了学术界。

从1921到1935,波斯特错过了哥德尔,错过了图灵和丘奇。在他迷惘之时,时代巨轮已经呼啸而过,他错过了数理逻辑的黄金年代。在1941年,他写了一篇文章,详细叙述了他此前在逻辑的不完备性方面的工作,投往了《美国数学期刊》。时任编辑赫尔曼·外尔(Hermann Weyl)拒绝了这篇文章:

我毫不怀疑在二十年前你的工作,部分由于它的革命性,没有得到应有的尊重。但我们无法将时针往回拨;在这段时间,哥德尔、丘奇与其他人完成了他们的工作,而美国数学期刊并不是发表历史回顾的地方。

作为编辑,外尔的决定是正确的。探索的前线并不是向迷失者施予救济的地方,历史才是。历史不会忘记这些被忽视的探索者,他们所有的功绩、辛劳与忧伤。波斯特厚厚的研究笔记,就是历史的见证。当时发生的一切将化为铅字,被人们一遍一遍以不同的形式复述,成为集体记忆的一部分。

为传说撰写诗篇,并一直传颂下去,这就是我们能做的一切。

来自Wikipedia

来自Wikipedia


衡量难度的归约

对波斯特来说,错过时代节拍还不算是最大的打击。

当时人们对精神疾病的认识尚浅,没有确实有效的药物,没有确实有效的疗法,一切只能靠摸索。波斯特的双相情感障碍,同样没有标准疗法。当时的想法是,既然发作时出现的是狂喜和抑郁的极端情绪,那么就应该尽量避免这种极端情绪的发生,最好的方法就是限制会导致极端情绪的活动,对于波斯特来说就是数学。他的医生开出的疗法,就是限制波斯特做数学的时间:从下午四点到下午五点,用餐,然后从晚上七点到晚上九点,每天共计三小时。对热爱数学的数学家来说,这简直是能与精神疾病媲美的折磨,就像让美食家用牙签吃最爱的肉酱意粉,我不知道波斯特是如何忍受这种焦灼感的。

幸而波斯特并没有止步不前。他在症状缓解后很快重新投入到数理逻辑的研究中。在图灵刚发表他论述图灵机的论文后,波斯特在对图灵的研究毫不知情的情况下,发表了另一个与图灵机非常相似的模型,现在被称为波斯特机,它与我们常用的计算机更相似,驱动计算的与其说是状态的转移,不如说是语句的执行。他猜想波斯特机的计算能力与λ演算相同,这是个正确的猜测,但他当时无法证明这一点。图灵的桂冠并未因此旁落。而波斯特在看到图灵的构造与证明后也心服口服,他的探索再次失去了意义。他后来也考虑过图灵机在多维上的扩展,与后来的“元胞自动机”颇有相似之处。著名的“生命游戏”就是元胞自动机的一个例子。可惜他并没有发表这个想法。

之后,波斯特转到了布尔函数的研究,也就是那些变量与值都是“真”或者“假”的函数。在1941年,他发表了一个非常重要的结果:对于函数复合封闭的布尔函数类的分类定理。这些类别构成了一个被称为“格”的数学结构,现在被称为波斯特格。对于当时的研究者来说,波斯特的这个结果虽然很有意义,但研究的对象有些偏门,再加上波斯特典型的那种含混晦涩的行文风格,波斯特格这项成果在当时并没有得到太多的重视。要等到几十年后,人们研究约束满足问题时,波斯特格才重新回到人们的视线中。

来自Wikipedia

来自Wikipedia

这项结果虽然一开始不太受重视,但毕竟也是正经的研究结果。就这样,通过不懈的努力,波斯特一点一点重新追上了当时数理逻辑的研究潮流,即使每天只能做三个小时的研究。

在1944年,波斯特应邀在美国数学协会做了一场演讲。后来他将演讲的内容写成了论文并发表。他自己可能没有想到,这篇论文会成为他最有影响力的论文之一。这篇论文的题目是《递归可枚举的正整数集合与它们的判定问题》(Recursive enumerable sets of positive integers and their decision problems),它希望回答的问题非常简洁:停机问题有多难?有比停机问题容易的不可计算问题吗?

有时候错过时代节拍可能也是一件好事,起码对于波斯特而言,与主流的疏离给他带来了一种与众不同的视角。对他而言,判定问题的计算就是形式系统的推演证明,而形式系统的相互包含是一个非常自然的问题。比如说定义自然数的皮亚诺公理体系,就是一种形式系统,而这个系统中的所有命题都能翻译到集合论的策梅洛-弗兰克(ZF)公理体系中,能用皮亚诺公理证明的数学命题,在翻译后都能在ZF中证明。可以说,ZF体系包含了皮亚诺公理体系。那么,给定两个不同的公理体系A和B,我们自然希望考察它们的包含关系,比如说B是否包含A。也就是说,我们希望知道,是否存在一种方法,能将A中的命题翻译到B中,并且希望翻译后,在A中能证明的命题在B中仍然能证明。

波斯特的另一个优势,就是他之前的研究已经涉及到这样一些具体的翻译问题,只不过用的术语不是翻译,而是归约。从一般的形式系统到正则形式A,再到正则形式B,再到一种非常特殊的推演规则,这些都是归约。在关于形式系统不完备性的研究中,波斯特早已自己构造过许多这样的归约。从特殊的归约到一般的“归约”这个概念,对于数学家来说,仅仅是一步之遥。

为了简洁起见,波斯特并没有使用他的正则形式的概念,而是将计算问题表达为一个个由自然数组成的集合。对于数理逻辑学家来说,无论是形式系统、判定问题还是自然数组成的集合,本质上并没有什么不同。形式系统的命题可以用字符串表达,所以可以化为自然数,判断某个命题是否能从公理推演出来,也就相当于判断对应的自然数是否属于可推演命题对应的集合。而一个集合对应的判定问题,就是某个输入作为自然数是否处于这个集合中,所以,指定一个由自然数组成的集合,与指定一个判定问题是等价的。在这个框架下,归约的定义更方便更直观。

归约也有很多不同的种类,它们有强有弱。波斯特在研究形式系统是用到的归约,也就是上面所说的“公理体系之间的翻译”,是其中能力比较弱的一种,又叫“多一归约”(many-one reduction)。而最强的图灵归约在判断A中命题的正误时,可以在可计算的范围内任意生成B中的命题并得到解答,再从这些任意多的解答中提取结论。能获取的解答数目多了,自然也能解决更多问题,也就是说能力越强。

图灵归约是波斯特研究的最终目标,但它的能力太强,很难研究。所以在1944年的这篇论文中,波斯特主要研究的是更简单的多一归约和另一种稍微更强大的“真值表归约”。他证明了,在这两种归约方法定义的难度概念下,存在这样的计算问题,它们是不可计算的,但却比停机问题更容易。也就是说,如果按照这些归约定义的难度来排序,在可计算问题与停机问题之间,存在无数的“中间层级”。从可计算问题到停机问题迈出的这一步,实际上跨过了无数的层级。

波斯特在论文的结尾猜想,对于更强大的图灵归约,这样的“中间层级”也存在,不仅如此,其中有无数个中间层级是计算可枚举的。这并不显然,因为越强大的归约,越能填补不同问题之间难度的差距。比如说,多一归约认为问题A比问题B要难,但这可能是因为它本身太弱,如果换用图灵归约,也许就能通过多问几个问题得出答案。波斯特关于计算可枚举的“中间层级”是否存在的这个问题,又被称为波斯特问题。

波斯特的这篇论文的新观点和新结果最终引起了美国逻辑学家的注意,他终于获得了作为一个数理逻辑学家应有的赞赏。也许,他并不需要什么救济。

在那场演讲之后,在美国数学协会的聚会上,有个人叫住了波斯特。这个人叫克林,也是一位数理逻辑学家(一些读者可能还记得提出λ演算的丘奇就是他的博士导师)。他对波斯特说,有些东西想让他看看,并将波斯特邀请到了他的家中。

这就是波斯特与克林伟大合作的开端。

来自Wikipedia

来自Wikipedia

计算的极限(八):符号的框架

本文遵守首页的CC版权声明:署名-非商业性使用-禁止演绎,请自觉遵守,非授权请勿转载。

本文在科学松鼠会发表,地址:http://songshuhui.net/archives/93188

在图灵诞辰100周年之际,献给这位伟大的开拓者。

计算无处不在。

走进一个机房,在服务器排成的一道道墙之间,听着风扇的鼓噪,似乎能嗅出0和1在CPU和内存之间不间断的流动。从算筹算盘,到今天的计算机,我们用作计算的工具终于开始量到质的飞跃。计算机能做的事情越来越多,甚至超越了它们的制造者。上个世纪末,深蓝凭借前所未有的搜索和判断棋局的能力,成为第一台战胜人类国际象棋世界冠军的计算机,但它的胜利仍然仰仗于人类大师赋予的丰富国际象棋知识;而仅仅十余年后,Watson却已经能凭借自己的算法,先“理解”问题,然后有的放矢地在海量的数据库中寻找关联的答案。长此以往,工具将必在更多的方面超越它的制造者。而这一切,都来源于越来越精巧的计算。

计算似乎无所不能,宛如新的上帝。但即使是这位“上帝”,也逃不脱逻辑设定的界限。

第一位发现这一点的,便是图灵。

计算的极限(零):逻辑与图灵机
计算的极限(一):所有机器的机器,与无法计算的问题
计算的极限(二):自我指涉与不可判定
计算的极限(三):函数构成的世界
计算的极限(四):机械计算的圭臬
计算的极限(五):有限的障壁
计算的极限(六):无穷的彼岸
计算的极限(七):宛如神谕


如果说图灵的经历只是时运不济,那么埃米尔·波斯特(Emil Post)的遭遇只能说是造化弄人。


梦想与现实

波斯特在1897年出生于当时属于俄罗斯帝国的奥古斯图夫(今属波兰),年幼时就随同家人移民到了美国。与你我之中的许多人一样,波斯特自幼就迷恋着璀璨的星空,一心希望长大后能当个天文学家,研究那些遥不可及的星体,揭露自然之伟力塑造这些巨大结构的法则。这对于一位少年来说,无疑是个珍贵的梦想。

拍摄者:P. Calcidese–Fondazione C. Fillietroz, ONLUS/ESO

拍摄者:P. Calcidese–Fondazione C. Fillietroz, ONLUS/ESO

但13岁时的一场意外,夺去了他的左臂。

在信息技术发达的今天,天文学家的工作几乎完全在计算机上进行,而各种各样的辅助设施更是让几乎所有人都能便利地使用计算机。但在波斯特的年代,天文观测仍然处于完全机械化的时期,许多观测任务都需要天文学家亲力亲为,曝光、校准、调整,这并不是按几个按钮就能完成的工作,需要捋起袖子动手做。只有一只手,连调整镜筒方向都做不到。尽管残疾的大天文学家并非没有先例,比如说开普勒,但这是例外,并非常态。

年少的波斯特为此曾写信到哈佛天文台与美国海军天文台。面对少年的来信,两个天文台给出了不同的回复。哈佛天文台的回复像是一种鼓励和安慰:“没有什么理由会阻止你在天文学中出人头地”;而美国海军天文台的回复更加务实直白:“依我之见,失去左臂是你成为职业天文学家的一大障碍。在这个天文台,用仪器观测时必须用到双手”。两种意见都非常合乎情理:少年的梦想应该呵护,但冰冷的现实也不能忽视。选择的权利,仍然掌握在波斯特的手心上。

他选择了放弃。

梦想是可贵的,更是昂贵的,尤其在波斯特的时代。放弃未必是错误的选择,关键是放弃之后如何选择。波斯特选择了数学,并且走了下去,走得很远。


初试身手

在完成高中与大学学业之后,在1917年,波斯特成为了哥伦比亚大学的一名博士生,跟随卡修斯·凯泽(Cassius Keyser)学习。这位凯泽也有过人之处,在当时美国数学界普遍偏向实用的氛围下,他却十分关心欧洲大陆关于数理逻辑的研究,这样的人在当时并不多。这大概因为凯泽自身非常关心哲学,甚至在哲学上也有不少的著作,于是他对于数学哲学与数理逻辑也是爱屋及乌。

凯泽对数理逻辑的热忱对波斯特影响很大,而那种更广泛的对数学与哲学的热情,可以在波斯特的师兄埃里克·贝尔(Eric Bell)身上看到。贝尔在数学研究上的贡献不大不小,在组合数学中,含有n个元素的集合拆分成子集的方法数被称为贝尔数,也有对应的贝尔多项式,这也许就是他最为人知的数学贡献了。但贝尔对数学的贡献远远超出了他的研究。他写了一本叫《Men of Mathematics》(中文译本叫《数学精英》或者《数学大师》)的书,讲述了众多知名数学家的故事。虽然这本书的描写过分夸张,而且过于关注数学家生活中的戏剧性,因而常常为数学家与数学史研究者所诟病,但这种写法同时也吸引了一代又一代的数学爱好者,有许多著名的数学家在少年时都深受这本书的影响。贝尔给少年带来了数学的梦想,这项贡献甚至比他的研究更重要。

出处:http://angelustenebrae.livejournal.com/15908.html

出处:http://angelustenebrae.livejournal.com/15908.html

在凯泽的指引下,波斯特在哥伦比亚大学简直如鱼得水。凯泽开设了一门研讨班,专门研究当时刚刚出版没几年的《数学原理》。这是一套厚厚的三卷本,但对于作者罗素(Bertrand Russell)与怀特黑德(Alfred North Whitehead)的宏大目标——将数学建立在毫无疑义的符号推演的基础上——来说,三卷实在有点薄。证据就是,他们等到第二卷,才证明了“1+1=2”,并且加上了评注:“以上命题有时会有用”(The above proposition is occasionally useful)。

这本数理逻辑的开山之作,不仅第一次展现了数学家追求确切无误的决心,也是类型论的首次登场。类型论不单是避免矛盾的工具,它触碰了计算的某些本质。那将是一个更颠覆常识的故事,但我们暂且按下不表。波斯特于是也开始研究《数学原理》的内容,作为博士论文的题目。

可以说,在数理逻辑这条道路上,波斯特一开始几乎是在独自前行。导师凯泽虽然对数理逻辑很有兴趣,但算是半路出家,除此之外,《数学原理》就是波斯特唯一的参照物。可以说,波斯特与丘奇一样,是美国土生土长的数理逻辑学家,他甚至比丘奇早几年进入这个领域,算是前辈。

三年如白驹过隙,但足以让波斯特深入当时数理逻辑的前沿。在他的博士论文中,他证明了《数学原理》中的命题演算是完备的,也就是说,在该系统内,真等价于可证明。作为逻辑系统,命题演算从属于一阶逻辑,所以波斯特的结果可以说是十年后的哥德尔完备性定理的前奏。

但波斯特的博士论文,价值远不止于此。

在《数学原理》中,罗素和怀特黑德殚精竭力建立了一个逻辑体系,这是他们的智力结晶,他们相信这是唯一的体系,所有其他数学都能奠基于此。但作为局外人的波斯特却看不到这种“唯一性”到底从何而来。在他眼中,逻辑体系可以是任意的,不一定要符合什么规则,可以拥有或多或少的代表不同意义的符号,甚至连“真”与“假”的二元对立都可以放弃。在论文的后半段,他研究了这一类“任意的”命题演算甚至是多值逻辑的一致性与完备性。虽然在现代,这种逻辑的自由观念已经深深融入了数理逻辑研究的精神,但在当时,这种想法可以说是开风气之先。

也许是因为这篇高质量的博士论文,刚毕业的波斯特获得了普林斯顿的垂青。图灵申请了两次才成功的同一份奖学金,波斯特甫一毕业就拿到了手。

接下来这博士后的一年硕果累累。


符号的框架

到了普林斯顿,波斯特继续研究一般的逻辑体系。追寻着希尔伯特的想法,他问了相同的问题:对于任意的逻辑体系,我们能否判定某个命题是否这个体系的定理呢?

要回答这个问题,就要先做定义:什么是“逻辑体系”?

出处:http://www.cs.nott.ac.uk/~txa/g53cfr/

出处:http://www.cs.nott.ac.uk/~txa/g53cfr/

要知道,逻辑体系种类繁多,从弗雷格电路图一般的“概念文字”,到罗素和怀特黑德的《数学原理》中略显奇异的近代逻辑符号,再到现代一般使用的一阶逻辑,又到更复杂的模态逻辑与线性逻辑,甚至到现代如雨后春笋层出不穷的新逻辑体系,它们无论是符号、意义还是表达范围都千奇百怪,要找到一个能囊括过去、现在甚至未来出现的定义,这无疑是个令人挠头的工作。如果考虑到波斯特当年见过的逻辑体系并没有现在那么多种多样,要去定义“逻辑体系”这个概念,无疑难上加难。

但数学工作者都习惯了推广各种概念,波斯特也不例外。他的任务,就是从一阶逻辑这个范本出发,找到一种能涵盖一切“逻辑体系”的定义。那么,一个自然的问题就是,当我们在用逻辑体系做推理或者证明的时候,我们到底在干什么?

我们先从比较简单的系统开始。所谓“一阶直觉主义命题演算”,可能是最简单而有实际意义的逻辑系统。虽然名字的长度和内容都很吓人,但实际上它非常简单。除了表示不同命题的变量之外,它只有三个符号(合取号\land  ,析取号 \lor  与蕴涵号\to  ,算上括号就是五个),加上仅仅8条“不言自明”的公理,还有单单一条推理规则:肯定前件规则(Modus ponens)。那些公理并不是什么复杂的东西,不过是将合取(家鸡不是野生动物而且炸鸡很好吃)、析取(我想吃云吞或者面条,当然云吞面也可以)和蕴涵(要是我今晚叫外卖,那么晚上就不用洗碗了)这些日常生活中的概念,在符号世界中的表达而已,实际上的确不言自明。而“肯定前件规则”虽然名字同样吓人,但意思很简单:如果我们能推演出命题P  与命题P \to Q  (读作“P推出Q”或者“P蕴涵Q”),那么我们就能据此推演出命题Q  。这也是显然的:要是我今晚叫外卖,那么晚上就不用洗碗;我今晚的确叫了外卖(是云吞面);从此可以推出,我今晚显然不用洗碗了。可以说,“一阶直觉主义希尔伯特命题演算”这个逻辑系统,其实就是一些日常的概念和规则的一种完全符号化、形式化的表达。

那么,当我们在使用这个逻辑体系进行数学推理的时候,我们在做什么?如果我们用这个体系证明了某个命题,这个“证明”到底又是什么?

正如初中几何证明一样,任何证明都要先列出它使用的公理,也就是说,它默认了什么是“真”的命题。然后,我们知道在肯定前件规则中,如果P  P \to Q  都是真的,那么Q也是真的,所以我们可以推出Q。那么,只要从公理出发,不停地应用这个规则,因为我们的出发点都是“真命题”,我们通过规则得到的命题也必然是真命题。从真理走向真理,这就是证明,难道不是吗?

的确,一个证明,就是一个从真理走向真理的过程,但这建立于符号的意义之上。如果我们不知道这些符号的意义的话,一个证明又是什么?因为我们已经知道一阶直觉主义命题演算实际上只是日常生活的形式化,所以我们能堂堂正正地说那些公理都是真的。但对于一个从来不知道这些符号的意义的人,甚至是几分钟前的我们来说,这些符号、命题、规则又是什么?当我们遇到一个全新的逻辑体系的时候,我们不知道新体系中的符号、命题、规则到底有着什么意义,这时我们又应该如何看待新体系中的一个证明呢?

不同的逻辑体系有着不同的符号,即使是相同的符号,在不同的体系中也不一定有着相同的意义。如果我们希望找到一个能囊括所有逻辑体系的定义,那么,这个定义中显然不能包含“意义”。但一个剥除了意义的形式体系到底是什么?当“P  P \to Q  可以推演出Q  ”的这个规则剥除了它的意义,剩下的又是什么?一个证明,如果剥去它“证明某项真的陈述”的这一重意义,它又是什么?

但如果将形式证明的意义剥除,剩下的不就仅仅是一些无意义的、盲目的符号推演么?当我们看到P  P \to Q  ,我们就能写出Q  ,仅此而已。本来这个逻辑体系是为了将日常生活中的推理形式化、精确化而存在的,现在要将“日常生活推理”这一意义抽去,只剩下符号搭成的框架,这不是舍本逐末吗?

的确,符号搭成的框架本身没有任何意义。但也正因如此,它可以承载任何意义。已有的逻辑体系蕴含着形形色色的意义,未有的逻辑体系可能蕴含着我们现在无法想象的意义。它们唯一的共同点,就是那个符号搭成的框架。公理就是作为起点的,由符号组成的公式;推理规则就是将一些符号串写成另一些符号串的机械规则;证明就是从公理出发,通过推理规则的不断改写,得到一个新公式的过程。如果有P  P \to Q  ,就写出Q  ,丝毫不需要思考意义。而在另外一个逻辑体系,如果有P  P \to Q  ,就写出Q \to P  ,这又有何不可?

这就是波斯特的答案:逻辑体系,不过是由一些符号、变量、起始符号串(公理)以及将这些符号串不断改写的规则(推理规则)。它们没有意义,但可以承载任何意义。通过对它们的研究,即使我们完全不知道某个逻辑体系的意义,也能通过对这些符号以及变换的研究,来得到关于这个逻辑体系的一些结论,比如它的一致性(是否存在一些不能写出的符号串),还有它的完备性(是否存在一个符号串,将它添加到起始符号串中就能改写出所有符号串)。只要研究这种完全形式化的符号系统,就能得出关于最广泛、最一般的逻辑体系的结论,无论它们的意义是什么。

作者David Rosenthal,来自http://facpub.stjohns.edu/~rosenthd/

作者David Rosenthal,来自http://facpub.stjohns.edu/~rosenthd/


形式的迷宫

波斯特这么想了,也这么做了。他将这种符号改写的规则构成的系统称为“规范形式A”(canonical form A,涵盖了现代所谓的“字符串重写系统”),然后证明了所有取规范形式A的系统都能写成另一种包含更多约束的“规范形式B”。规范形式B允许的改写规则更简单也更弱,但它的“表达能力”与更强大的规范形式A相同。然后,波斯特证明了《数学原理》中的逻辑系统,实际上也能用这个弱得多的规范形式B表达出来,是规范形式B的一个特例。这意味着,做数学需要的推理规则,实际上要比罗素与怀特黑德想象的要简单得多。

虽然规范形式B很简单,但波斯特觉得它还不够简单,因为它仍然需要有无穷个表示变量的符号。他又定义了另一个“规范形式C”,它只需要有限个符号,但却能表达出规范形式B所表达的一切逻辑体系。在规范形式C中,波斯特又定义了所谓“正则形式”,在正则形式表达的逻辑体系中,只允许一种改写规则:如果符号串的开头是某一串特定的符号,那么将这些符号删去,然后在末尾添加另外一串符号。同样,所有能用规范形式C表达的逻辑体系,都能转化为正则形式。

我们来看一个正则形式的例子。符号有三个:a和b;起始符号串只有一条:“bb”;而规则仅仅有三条:

(1) a$ -> $a
(2) b$ -> $aba
(3) b$ -> $b

这里,$的意思是剩下的符号串,比如说a$ -> $a,就是说如果开头读到一个a,那么就去掉这个a,然后在符号串末尾加上一个a。如果开头是b,我们可以选择应用第二或者第三条规则,去掉b,然后续上aba或者b。很简单吧?

那么,通过这些规则,从公理开始,能改写出来的字符串又有哪些呢?

我们来看一个改写的例子:

bb -> baba (2)
-> abaaba (2)
-> baabaa (1)
-> aabaab (3)
-> abaaba (1)
-> baabaa (1)
-> aabaaaba (2)
-> abaaabaa (1)

也许你已经察觉到了这个简单的规律。我们注意到,每一条规则左右两边b的数量是相同的,因为公理只有“bb”,所以所有改写得到的符号串必然有两个符号b,它们将其余的a分成了扇段。再仔细观察上面的例子,容易发现两头a的数目加起来恰好是中间一段的a的数目。不难证明,所有可以写出来的符号串,恰好是形如a^m b a^{m+n} b a^{n}  的符号串,其中m与n都是正整数。或者可以说,这个形式系统表达了正整数的加法。很简单吧?

正则形式也许已经简单得不能再简单了,波斯特认为,这么简单的系统,要判断某个符号串是否能够写出来,看来也不是什么难事吧?但不要忘记,《数学原理》这本三卷本的巨著,它使用的逻辑体系也能归化为正则形式。就像图灵机一样,正则形式看似简单,但能力惊人。

波斯特甚至猜测,一切能用一个本质上有限的系统生成的符号串组成的集合,必定可以用一个正则形式体系生成;也就是说,正则形式体系涵盖了一切有限的符号生成系统,无论是已知的、未知的、过去的、未来的。这个猜测被称为“波斯特论题”(Post’s thesis)。这是一个大胆的猜测,要知道,数学家日常使用的逻辑,也只是一种有限的符号生成系统,只不过我们将这个系统生成的符号串称为“定理”,并且能给它们赋予“真”的意义而已。波斯特的猜测,实际上说的是正则形式体系覆盖了所有可能的数学推理体系。

这么大胆的猜测,难道不会隐藏着显而易见的问题吗?

我们可以假定所有考虑的正则形式系统都只有两个符号,因为通过两个符号的二进制组合我们可以表达别的符号。因为正则形式体系非常简单,我们能很容易地用自然数给它们编号,从1、2到无穷。给定某个编号,我们能机械地写出对应的正则形式体系。考虑一个集合D,它的元素是这样的符号串:用二进制的眼光来看,这个符号串对应一个自然数n,而编号为n的正则形式系统无法写出这个符号串。那么,是否存在一个正则形式体系T,它能写出的符号串的集合恰好就是D呢?

如果这样的T存在的话,它必定对应着一个编号n,而这个编号对应一个符号串S。S不可能属于D,否则按照D的定义,当S属于D时,对应的正则形式体系T必定无法生成S,而T应该写出D中的所有符号串,包括S,矛盾;而S又一定属于D,否则按照D的定义,当S不属于D时,T必定可以写出S,但T不应该写出D以外的任何符号串,包括S,矛盾。无论S是否属于D,引出的都是矛盾。于是,错误必定出现在一开始的假定上,也就是说,必然不存在这样的T,它恰好生成集合D。

来自Wikipedia

来自Wikipedia

记忆力好的读者一定察觉到了,这就是康托尔的对角线法,与图灵所用的如出一辙!

但如果对于任意的正则形式体系T与字符串S,我们都能证明T能否写出S的话,那么集合D必定可以用一个有限的系统生成,我们只需要针对所有自然数n,考察编号n的正则形式体系是否能写出n对应的字符串,这可以在有限的体系与有限的时间内做到。这又是一对矛盾。我们的论证中,必定有什么地方出了问题。

我们回过头来看看,这个矛盾用到了什么假设。仔细察看之后,我们能找到两个没有证明的假设:

假设一:一切本质上有限的系统生成的符号串集合,必定能用某个正则形式体系生成。

假设二:对于任意的正则形式体系T与符号串S,我们都能在有限时间内知道T能否写出S。

假设一是波斯特论题,假设二则源于因为我们认为正则形式非常简单。两个假设看上去都很有道理,假设一甚至更大胆一些。但如果将这两个假设放在一起,则不可避免地会导致矛盾。数学是不应该有矛盾的,二者必须择其一,甚至两者都可能是错的。那么,应该先放弃哪一个呢?

正则形式系统看上去是这么简单,毕竟眼见为实,要证明某个符号串能否写出来,似乎不是什么难事。但“本质上有限的系统”,涵盖的范围非常广阔,而正则形式看上去又那么简单,谁知道会不会有别的什么系统能做到正则形式做不到的事情呢?保险的做法,大概是放弃假设一,保留假设二。

但波斯特却反其道而行之。在此前对另一种同样简单的符号重写系统——所谓的“标记系统”(tag system)——的研究中,他发现对于很多看上去简单的问题,要找到答案不是那么容易的事。他猜想对于正则形式系统,也许我们原本认为的“简单问题”,实际上非常难解决。这些形式系统,并不像草原那样一览无遗,而更像是由形式操作构成的迷宫。他认为,实际上要放弃的应该是假设二,要保留的反而是他的假设一。

事实证明,他的选择是正确的。如果你对放弃假设二还有疑问的话,不妨试试以下的正则形式系统:

aa$ -> $bc
ab$ -> $bc
bc$ -> $a
ca$ -> $aaa
cb$ -> $aaa

如果你能找到一个起始符号串,使得这个形式系统可以写出无穷个不同的符号串的话,我可以保证,你的大名将会留在数学史上。

但放弃假设二也就相当于断言:存在某个正则形式体系T与符号串S,我们无法在有限时间内证明T能否写出S。可以说,这就是正则形式体系中的某种哥德尔不完备性定理:有些东西,我们不可能知道。

这是一个伟大的成就,波斯特在哥德尔之前10年就预见到了相似的结论。如果说哥德尔开创了一个新时代,那么波斯特当时则远远超越了时代。

可惜这个成就,于他而言过于沉重。

The Scream