计算过程形式化

来自计算思维百科
跳转至: 导航搜索

人类对计算本质的真正认识取决于形式化的研究过程。形式化方法和理论研究起源于数学的基础研究。数学的基础研究是指对数学的对象、性质及其发生、发展的一般规律进行的科学研究。

形式化方法

德国数学家康托尔(G. Cantor,1845~1918)从1874年开始,对数学基础作了新的探讨,发表了一系列集合论方面的著作,从而创立了集合论。康托尔创立的集合论对数学概念作了重要的扩充,对数学基础的研究产生了重大影响,并逐步发展成为数学的重要基础。

然而不久,数学家们却在集合论中发现了逻辑矛盾,其中最为著名的是1901年罗素(B. Russell)在集合论概括原则的基础上发现的“罗素悖论”,从而导致了数学发展史上的第三次危机。

罗素悖论可以这样形式化地定义:Let R = {x|x∉x}  then R∊R ⇔R∉R。为了使人们更好地理解集合论悖论,罗素将“罗素悖论”改写成“理发师悖论”。其大意是,一个村庄的理发师宣布了这样一条规定:“给且只给村里那些不自己刮胡子的人刮胡子”。现在要问:理发师给不给自己刮胡子呢?如果理发师给自己刮胡子,他就属于那类“自己刮胡子的人”,按规定,该理发师就不能给自己刮胡子;如果理发师不给自己刮胡子,那么,他就属于那类“不自己刮胡子的人”,按规定,他就应该给自己刮胡子。由此可以推出两个相互矛盾的等价命题:(1)理发师自己给自己刮胡子,(2)理发师自己不给自己刮胡子。

为了消除悖论,奠定更加牢固的数学基础,20世纪初,逐步形成了关于数学基础研究的逻辑主义、直觉主义和形式主义三大流派。其中,形式主义流派的代表人物是大数学家希尔伯特(D. Hilbert)。他在数学基础的研究中提出了一个设想,其大意是:将每一门数学的分支形式化,构成形式系统或形式理论,并在以此为对象的元理论即元数学中,证明每一个形式系统的相容性,从而导出全部数学的相容性。希尔伯特的这一设想,就是所谓的“希尔伯特纲领”。

“希尔伯特纲领”的研究基础是逻辑和代数,主要源于19世纪,英国数学家乔治·布尔(G. Boole)所创立的逻辑代数体系(即布尔代数)。它的目标,其实质就是要寻找通用的形式逻辑系统,该系统应当是完备的,即在该系统中,可以机械地判定任何给定命题的真伪。

希尔伯特对实现自己的纲领充满信心。然而,1931年,奥地利25岁的数理逻辑学家哥德尔(K. Gödel)提出并证明了关于形式系统的“不完备性定理”,包括两条定量:(1) 任何一个相容的数学形式化理论中,只要它强到足以蕴涵皮亚诺算术公理,就可以在其中构造在体系中既不能证明也不能否证的命题。(2) 任何相容的形式体系不能用于证明它本身的相容性。该定理指出希尔伯特纲领中所描述的形式系统是不存在的,从而宣告了著名的“希尔伯特纲领”的失败。希尔伯特纲领的失败同时也暴露了形式系统的局限性,它表明形式系统不能穷尽全部数学命题,任何形式系统中都存在着该系统所不能判定其真伪的命题。

“希尔伯特纲领”虽然失败了,但它仍然不失为人类抽象思维的一个伟大成果,它的历史意义是多方面的。对计算学科而言,最具意义的是,希尔伯特纲领的失败启发人们应避免花费大量的精力去证明那些不能判定的问题,而应把精力集中于解决具有“能行性”的问题。

图灵计算模型

哥德尔指出完备的形式化数学系统是不存在的,在此研究成果的影响下,20世纪30年代后期,图灵(A. M. Turing)从计算一个数的一般过程入手,对计算的本质进行了研究,从而开始了对计算本质的真正认识。

1935年,图灵开始对数理逻辑发生兴趣。数理逻辑又叫形式逻辑或符号逻辑,是逻辑学的一个重要分支。数理逻辑用数学方法,也就是用符号和公式、公理方法去研究人的思维过程、思维规律,其起源可追溯到17世纪德国的大数学家莱布尼兹,其目的是建立一种精确的、普遍的符号语言,并寻求一种推理演算,以便用演算去解决人如何推理的问题。在莱布尼兹的思想中,数理逻辑、数学和计算机三者均出于统一的目的,即人的思维过程的演算化、计算机化,以至在计算机上实现。但莱布尼兹的这些思想和概念还比较模糊,后续的许多数学家和逻辑学家沿着莱布尼兹的思路进行了大量实质性工作,使得数理逻辑逐步完善和发展起来,许多概念开始明朗起来。但是,“计算机”到底是怎样一种机器,应该由哪些部分组成,如何进行计算和工作,在图灵之前没有任何人清楚地说明过。

在听了剑桥大学组合拓扑学先驱纽曼(Maxwell H. A. Newman)教授的讲座之后,图灵进一步将兴趣明确为可判定问题,即能否至少从原理上证明,用确定的方法或步骤可以判断任何给定的数理命题。为了回答可判定问题,需要对“方法”加以定义,它不仅要精确,而且要令人信服。他分析了一个人能够完成哪些“机械的”步骤,估计了实现某些事物的思考应该有多大的规模,以及用理论机器如何表示这种分析。于是构想了“图灵机”模型。

简单来说,图灵机是一个逻辑机的通用模型。图灵机由一个控制器、一个读写头和一个无限长的存储带组成。处理器实际是有限状态控制器,能使读写头左移或右移,并对存储带进行修改或读出。于是通过有限指令序列就能实现各种演算过程。图灵机模型将可计算性这一概念与机械程序和形式系统的概念统一起来。

首先,可解性问题的讨论与算法的概念是分不开的。算法也称为能行方法或能行过程,是描述求解问题的方法和步骤,是对计算过程的精确描述,由一组明确定义且能机械执行的规则所组成。根据图灵的观点,他认为任一机械执行过程必须在一台机器上实现,通过引入机器状态,图灵机本质上具有指令特点的程序运算操作。

其次,根据图灵的研究,直观上讲,所谓计算就是计算者(人或机器)对一条两端可无限延长的纸带上的0和1执行操作,一步一步地改变纸带上的0或1的值,经过有限步骤最终得到一个满足预先要求的符号串的变换。他将此计算过程符号化为一个五元组,机器从给定的纸带上某起始点出发,其动作完全由初始状态及五元组来决定。图灵机是一种为可解问题设计的一种计算装置,它不是一台具体的现代意义上的计算机,但它却是一种操作十分简单且运算能力很强的计算装置,用其来计算所有可能想象到的可计算函数。

图灵机模型的实际意义在于:图灵证明,只有图灵机能解决的计算问题,实际计算机才能解决;如果图灵机不能解决的计算问题,则实际计算机也无法解决。即可计算性=图灵可计算性。因此,图灵机的能力概括了数字计算机的计算能力,对计算机的一般结构、可实现性和局限性产生了深远的影响。

图灵机与当时哥德尔、丘奇(A.Church)、波斯特(E. L. Post)等人提出的用于解决可计算问题的递归函数、λ演算和POST规范系统等计算模型在计算能力上是等价的。在这一事实的基础上,形成了著名的丘奇—图灵论题。

不过,图灵机等计算模型均是用来解决“能行计算”问题的,理论上的能行性隐含着计算模型的正确性,而实际实现中的能行性还包含时间与空间的有效性。伴随着电子学理论和技术的发展,在图灵机这个思想模型提出不到10年的时间里,世界上第一台电子计算机诞生了。