回首页 

载《广西民族学院学报》自然科学版11卷4期(2005)

迈向数学机械化:从塔斯基到王浩1

王磊
(上海交通大学科学史系,上海,200240)

 

摘 要:本文介绍了哥德尔不完备定理如何使希尔伯特定理判定问题研究陷入困境。评价了塔斯基在理论上给出了定理判定的方法意义。特别指出是王浩首次在计算机上实现了高效证明定理的方法,并明确提出“迈向数学机械化”。
关键词:数学机械化 塔斯基 王浩


一、 数学家的伟大设想

  机器使人从体力劳动中解放出来,数学家们因而设想用机器解决数学问题,代替人从事脑力劳动。17世纪,法国数学家笛卡尔就曾设想用机械解决数学问题。借助“通用数学”把一切问题化为数学问题,一切数学问题化为代数问题,一切代数问题化为代数方程求解问题。笛卡尔创立的解析几何,在空间形式和数量关系之间架起了一座桥梁。1637年出版的《方法论》的附录《几何》就是尝试如何将代数应用到几何上,利用代数的一般性,把推理程序机械化以减小解题工作量,依据笛卡尔的设想,所有的几何问题都可以归结为代数方程的求解问题,在给方程问题寻求了标准解法后,完全可以用一种程序化、标准化的方式解决所有的几何问题。
  德国数学家莱布尼茨在这一思想的基础上又前进了一步,他设想建立一种理想的“通用语言”,利用它来进行推理,使问题的正确性可以通过计算来验证。莱布尼茨计划创造两种工具,其一是通用语言;另一种是推理演算。前者的首要任务是消除现存语言的局限性、不规则性,使新语言成为世界上人人公用的语言;新语言使用简单明了的符号、合理的语法规则,便于逻辑的分析和综合。后一种,即推理演算,则用作推理的工具,它将处理通用语言,规定符号的演变规则,从而使逻辑的演算可以按照一条明确的道路进行下去。莱布尼茨还提出了直接进行机械乘法的思想。
  1899年,希尔伯特在《几何基础》中提出了从公理化走向机械化的数学构想。希尔伯特计划将数学知识纳入严格的公理体系中,并着力在公理化基础上寻找机械化的方法判定命题是否成立。希尔伯特同时指出,定理的判定问题应当是分类解决的,解决方法要同时强调简单性和严格性。以希尔伯特为代表的形式主义学派,希望通过形式逻辑的方法,构造一个有关数论(自然数)的有限公理集合,推出所有数论原理(完备性)且无矛盾(相容性),并以此出发构造整个形式主义的数学体系。
  1931年,哥德尔(Kurt G?del)发现并证明了著名的不完备定理,这条定理彻底粉碎了希尔伯特的形式主义理想。在形式逻辑中,数学命题及其证明都是用一种符号语言描述的,可以机械地检查每个证明的正确性,于是便能从一组公理开始无可辩驳地证明一条定理。哥德尔第一不完备定理,从根本上否定了这一设想。不完备定理实际上表明,这样的公理系统要么不完备,要么有矛盾。


二、 塔斯基:在否定中发现肯定

  哥德尔不完备定理的否定性结论给定理判定问题的发展蒙上了一层阴影。然而,关于判定方法的研究结果并不全是否定的。1921年,波斯特(E.L. Post)为真值表判定法的有效性给出了严格的证明。1921年,兰福德(C.H. Langford)给出了线性次序初等理论的判定法。1930年,普列斯博格(M. Presburger)为仅包含加法运算的整数运算找到了判定法。1943年,麦克铿赛(J.C.C. Mckinsey)给出了初等格论全称语句的判定法。但是,突破性的进展源自塔斯基(A. Tarski)的工作。1948年,在《初等代数和几何的判定法》(A Decision Method For Elementary Algebra And Geometry)中,塔斯基推广了关于代数方程实根数目的斯笃姆(Strum)法则从而证明了一条重要定理:初等几何和代数范围的命题都可以通过机械方法判定。就本质而言,塔斯基的判定方法是一种“消去量词”的方法。实际上,塔斯基自己指出,这一证明方法早在1930年就已经获得,只是没有机会发表,它既可用来判定实数的初等代数中语句的成立与否,亦能用来判定初等几何语句。
  在塔斯基看来,所谓初等代数,是指实数理论中的一个部分,其中仅用到表示实数的变量,表示个别数目的常数;表示施用于实数的初等运算和实数之间的初等关系的符号;还有初等的逻辑词项。在初等代数的公式中包含代数方程和不等式;用初等逻辑词项把方程、不等式连结起来,就得到初等代数的语句。另一方面,在初等代数中不存在用变量去代表的任意实数集合、实数序列或实数函数等等。塔斯基的“初等”概念是指不涉及集合论。
  塔斯基首先构建了一个初等代数的形式系统,并定义出语句类。系统由变项、代数常项、代数运算符号、代数项、代数关系符号、原子公式、语句连接词、(存在)量词和公式构成。原子公式包括等式和不等式。公式由原子公式用语句连接词和量词构造。以此形式系统为基础,塔斯基建立了初等代数的判定方法。方法分为两部分。第一部分实现变换:对于任意给定的公式,总能用机械的方法找到一个与其等值的公式,它满足实现判定所需要的形式。第二部分实现判定:对于任意给定的不含量词的语句,总能用机械的方法判定它是否为真。在这个形式系统中,塔斯基成功地引入了判定代数方程实根数目的斯笃姆定理,比照方程求根处理命题判定问题。塔斯基的判定法在内容与形式上和斯笃姆定理有着很密切的联系,并且进一步把定理推广到了多个未知数的任意方程和不等式系的情形。
  塔斯基指出,判定方法能告诉人们每一步做些什么,在运用它的时候不需要别的知识。只要能懂得判定方法并照着所指出的去做,就能进行定理判定。对于初等几何的判定问题,塔斯基坚持了将几何代数化的思想。初等几何语句就是指能够通过一个固定的坐标系把它变成初等代数语句的语句。塔斯基仔细考虑了二维欧氏几何的情况:欧氏平面中的任意点可以理解为多项式。利用三个常项表示点与点之间关系:二项关系“相等”用“=”表示;三项关系“在中间”用“B”表示;四项关系“等距离”用“D”表示。变项与原子公式也用形式化的方式表示。初等几何语句即表达关于点的某个事实以及点与点之间的关系。三角形、平面、圆、直线等等的概念都可以翻译为这个代数系统的语言。要得到初等几何的判定方法,只须给每个初等几何的语句A对应一个初等代数的语句A*。从解析几何可以知道,A是真的,其充分必要条件是A*是真的。由于可以用机械的方法判定A*的真确性,则A的真确性可以机械地判定。塔斯基认为,虽然存在普遍适用于初等代数和几何的判定方法不能被认为是必然的,但是判定方法的存在却是必然的。
  塔斯基给出的判定法是一种理论化的方法,在《初等代数和几何的判定法》一书中并无任何应用这种方法解题的例子。塔斯基得出的结论给定理判定问题的研究带来了曙光,虽然哥德尔不完备定理否定了希尔伯特的思路,但是在其他方向寻找判定方法是可行的。然而,尽管塔斯基的方法在理论上取得了成功,却因繁杂无比而难以在当时的计算机上证明稍有难度的定理。


三、 王浩:迈向数学机械化

  二十世纪50年代,电子计算机诞生了。与以往的计算器械不同,电子计算机不仅可以实现数学计算的机械化,而且可以处理逻辑关系。二进制代码与开关电路结合得更好,大幅提高了运算速度。程序由外插变为内存,当计算题目改变时,不必变换线路板而只需更换程序。上述特点使电子计算机成为了证明数学定理的有力工具。
  随着电子计算机逐步进入美国的大学校园和研究机构,利用电子计算机进行数学问题证明的研究蓬勃发展。1959年,美国洛克菲勒大学教授王浩设计了几个计算机程序,仅用3分钟,就在IBM 704型计算机上证明了罗素与怀特海《数学原理》中220条有关命题逻辑的定理,稍后又扩展到了400条,这一成果宣告了用计算机进行定理证明的可行性。王浩因此获得了1983年人工智能国际联合会和美国数学会联合颁发的“里程碑” (Milestone Prize)奖。 在1960年的《IBM研究与发展年报》(IBM Journal),王浩发表了《迈向数学机械化》(Toward Mechanical Mathematics),“数学机械化”一词即出自此处。这篇文章后收录于《数理逻辑总览》(A Survey of Mathematical Logic)的第9章,1959年由科学出版社出版。
  为了达到用机器证明定理的目的,首要的工作就是将定理形式化,使人们可以像调试程序一般,实现用机械化方法检验新数学结果。先将命题证明形式化,以期实现机械化。总结以往对判定问题的研究,王浩认为应当在形式化方面加以修改,以适应机器进行证明的需要。对于一个命题的完整证明-判定过程应当建立在牢固的逻辑基础上,也就是谓词演算。“利用在数理逻辑中强调形式化这一优点的一个自然的想法,就是试图系统地利用计算机证明定理。” 2
  王浩提出,研究的重点不应当局限于理论上的可判定性,而在于实际的可行性。同时,应当发展非构造性命题的构造性解释,把非构造性方法规约到构造性方法或用构造性方法来证明非构造性方法的正确性。存在两种不同的数学定理机器证明:一种是人利用计算机作为局部的辅助工具进行定理证明,这种方法以四色定理的证明为代表。四色定理的计算机证明在当时被认为是一个巨大的成就。但是王浩对此评价说,真正的数学机械化是要用电子计算机对整类的定理进行有效地判定。四色定理的机器证明有别于真正的定理机器证明,是在计算机辅助下的特例机证。如果按照证明四色定理的思路进行下去,那么虽然个别定理证明的部分脑力劳动被机器所替代,但是人们还需要为每个要证明的定理去设计程序。解决数学问题的难度与工作量并未有实质性的减轻。另一种方法就是以系统的机械化证明为特点的尝试。这种思想提出:要建立一种处理一类有关问题的一般方法,对于适用的问题能给出完全的解决。一个一般性的方法可以对给定的问题类找到判定过程,在应用这一证明方法时,这一类问题中的每一个都能够被判定,也就是说最终能确定它是不是定理。
  计算与证明存在明显的不同:首先,处理对象不同。计算处理的对象是数字,而证明处理的对象是命题。其次,规则精确性不同。计算规则的精确性远胜过证明规则。再次,计算是有限的。计算过程是可判定的,可以递归的,或者可以通过数学近似方法达到这一目标。然而,证明过程通常不是有限的,它是不可判定的。对于近似方法,在定理的证明中还没有形成一个清晰概念。最后,计算有行之有效的步骤,而在证明中,判定方法并不显然。在计算中,简捷的方法并不具有普遍性,更多强调规则。在证明领域,人们依赖的仍然是直觉、洞察力、经验以及其它模糊而难以模仿的原则。除非能发现它们之间的特定联系,否则想要消除证明过程的复杂和冗长是不可能办到的。
  数学研究处理的主要问题是计算和证明。计算器械的研制已经取得了许多伟大的成就,莱布尼茨、帕斯卡和巴贝基都曾进行过计算器的研制,电子计算机的出现更使得计算问题变得轻而易举。如果在数学研究中占有很大比重的定理证明工作不能实现机械化,无法用机器代替人脑,那么机械化的数学就不可能实现。毫无疑问,上述的不同之处是阻碍数学定理证明机械化的主要原因。王浩认为,数学定理的机器证明有赖于数理逻辑和计算机器的有力结合。
  如何处理计算与证明的不同之处,王浩给出了自己的看法:首先,哥德尔对于第一个问题已经在理论上给予了回答,人们已经实现了利用数字机械处理字符信息。第二个不同之处,大体上已经被数理逻辑的形式化研究在过去八十年取得的成就所解决。第三个问题的解决对于定理机器证明也很重要。但是,现在关心的应当是它的实际可行性,而不是理论上的可能性。哥德尔不完备定理的结论并不妨碍现在所进行的尝试。对于“近似证明”这一概念,指由构想逐步改进并最终达到具体证明,从这个意义上说,是可以更精确的形式化的。王浩认为,最后一个不同之处也许是最根本的。以往的工作夸大了这个问题的复杂程度,这一部分是由于抽象的判定很难现实化,另一部分则是由于没有选择有效的替代程序。人对于大量细小问题的处理是无能为力的,这在本质上限制了数学研究的对象,以及数学处理问题的方式。机器在这些方面的优越性,可能会产生很多令人惊喜的新成果,而这得益于它们引起的新的转折,这正是人们所要适应的。基于上述讨论,王浩认为算法的分析要有推理分析和数字分析作为支持,这样才能实现数学问题求解的机械化。
  早在1953年,王浩就已经开始思考用机器证明数学定理的可能性。1957年,在《对图灵计算机理论的改写》(A Variant to Turing's Theory of Computing Machines)一文中,他表达了自己对这一问题的初步的想法。1956年,认知心理学家在机器证明定理方面取得了举世瞩目的成就。纽维尔-肖-西蒙(Newell-Shaw-Simon)3的报告指出,在JOHNNIAC型计算机上,他们编制的程序LT(Logic Theorist)成功证明了罗素与怀特海的《数学原理》中第二章52条定理中的38条,对于其余14条定理,LT(Logic Theorist)程序没有找到证明。未能证明的定理绝大部分是由于超出了机器时间和存储空间的限制。1963年,他们在计算机上证明了全部52条定理。
  1958年的夏天,王浩在波启浦夕(Poughkeepsie)的IBM研究实验室(IBM Research Laboratory)利用IBM704型计算机上编写了三个程序。1959年,王浩又进一步对这些程序进行了修改。程序是用SAP(Shared Assembly Programming Language),即公用汇编语言写成的。第一个程序为命题计算提供了证明-判定过程,它可以依据给定命题是否为一个定理,而给出证明或反证。利用这个程序,《数学原理》前五章的200多条定理在37分钟内证明完毕,由于其中12/13的时间是用来进行读入-输出操作,所以实际上用来证明的时间不足3分钟。这些定理中包含了纽维尔-肖-西蒙所证明的52条定理,用时不足5分钟。如果除去输入-输出所占用的时间,那么实际证明时间将不足半分钟。对于纽维尔-肖-西蒙不能证明的命题,或者需要较多时间证明的定理,则在几秒钟就给出了证明。
  另外两个程序用来证明书中的其余定理。第二个程序用以指示机器利用基本符号形成命题,再从中选取出重要的命题。在一个小时之中,形成了1,4000条命题,并在磁盘上存储其中了选取的1000条定理。由于选取条件过于严格,所以选出定理不足十分之一。第三个程序作为一个大程序的组成部分,用来处理谓词演算。《数学原理》中关于谓词演算共有150条定理。王浩设计的程序在一个小时以内证明并打印了其中85%的定理。
  王浩在研究中还发现,虽然理论上的结果表明,一阶逻辑在总体上是不可判定的,但是研究的结果却出人意料。因为王浩的计算机程序在不到九分钟的时间里证明了《数学原理》中一阶逻辑部分的全部定理(350条以上)。这说明了《数学原理》中全部一阶逻辑的定理都是属于一个简单且可判定的子域中。
  虽然计算机运行得很快,但是粗糙的算法使问题的复杂性很快超出了计算机的能力。所谓算法,是指一组有穷的规则,它在任何时刻都能精确地告诉执行算法的人或机器,对某一类给定问题该做什么。如果给出某一问题类K的算法以及属于K的一个问题,那么只要执行算法所要求的操作,并精确地遵循已给规则,任何人都可以解决该问题。一个过程能够机械化,即能被一台机器或一个人用机械的、非创造型的方法执行。过程因素可以归纳为两个重要定理:有穷性定理和确定性定理。能够精确描述的任何过程都可编成计算机执行的程序,它应该是这样一个序列,即下一个状态由上一个状态的结果决定。由于理论的计算与可行的计算之间存在巨大的鸿沟,所以数学定理机器证明不应当仅仅停留于理论上的设想,而是要着手研究可以具体实施的方法。王浩意识到,应当注意通常的多项式复杂类,并认为有可能是取得突破的方向。
  判定理论上的研究为数学机械化的展开奠定了基础,然而更为重要的是对实际可行性的研究,也就是如何真正用程序在计算机上高效地实现数学定理的证明。塔斯基的方法在设计时并未考虑电子计算机的特性,难以适应实际的运行要求。电子计算机的优点在于强大的数据处理能力,具备高速性和准确性。因此,为了用电子计算机证明定理,必须有一种与之相适应方法,也就是要设计一种能借助其强大功能的算法,充分发挥计算机的巨大威力。
  王浩所取得的成就在当时震动了数学与数理逻辑学界,他的先驱性成就被人们誉为“一击落七蝇(Seven flies with one blow)”。这一现实的成功极大地激发了人们寻求用计算机高效证明定理的努力。正是王浩吹响了向数学机械化进军的号角。


参考文献
1. 塔斯基,初等代数和几何的判定法,科学出版社,1959
2. Feferman, Anita Burdman, Alfred Tarski:Life and logic, Cambridge University Press, 2004
3. Newell A., J. C. Shaw and H. A. Simon, Empirical Explorations of the Logic Theory Machine: A Case Study in Heuristics, Computers and Thought, McGraw-Hill, 1963,134-152 
4. Wang Hao, Toward mechanical mathematics, IBM Journal, 4 (1960), 2-22
5. Wang Hao, A Survey of mathematical logic, Science Press, Beijing (1962)
6. 王浩,数理逻辑通俗讲话,科学出版社,1981
7. 吴文俊,数学机械化,科学出版社,2003
8. 纪志刚,吴文俊与数学机械化,上海交通大学学报,2001,3,Vol.9

Toward Mechanical Mathematics: from Tarski to Wang Hao
Wang Lei
School of Humanities, Shanghai Jiao Tong University, Shanghai 20030, China

Abstract:This article explains the reasons why G?del's theorem of incompleteness made the research of theorem proving in difficult position and gives some comments on Tarski's theoretical method for theorem proving. The author points out that Wang Hao proposed "toward mechanical mathematics" firstly and practiced an efficient way in theorem proving on computer. 
Key Words: Mechanical Mathematics; Tarski; Wang Hao

作者简介:王磊,上海交通大学科学史系在读硕士研究生
基金项目:上海交通大学人文社科基金“吴文俊与数学机械化”
2 王浩,数理逻辑通俗讲话,科学出版社,9页
3 Empirical Explorations of the Logic Theory Machine: A Case Study in Heuristics, Report P-951, Computers and Thought, McGraw-Hill, 1963,134-152

 

20060219加入