文档介绍：一种构造性的计算理论通用计算——计算通用通用计算: 起源于莱布尼兹,将各种问题符号化数字化之后,进入计算过程。计算通用:万物之所以可以计算,是因为万物本来就是在计算。区别只是在于是不是使用数字进行计算。一切皆计算……将构造进行到底计算科学的特点是:构造性,能行性和潜无穷。然而计算理论的研究框架却具有以下的特点:非构造性,非能行性和实无穷。例如数理逻辑的语义部分,例如计算理论的停机问题等等。提出的问题:有没有另一种可能性,使用构造性的框架来思考构造性的计算科学。回顾历史为了重新思考计算理论,有必要回顾计算科学历史。罗素悖论引起了第三次数学危机,在这次危机中走出了计算科学。康托尔对角线方法 1891 年,康托尔使用对角线方法证明实数集是不可数的。康托尔集合论:实无穷。当时许多数学家只承认,有穷事物的发展过程是无穷尽的,无穷只是潜在的,是就发展说的。他们不承认已经完成的、已经存在着的无穷整体, 例如集合论里的各种超穷集合。潜无穷论者:高斯, 克罗内克, 彭加莱。罗素悖论理发师悖论:在一个小镇上有一位理发师,这位理发师遵守这样的规则: “给而且只给那些不给自己理发的人理发”。现在问理发师是否要给自己理发。如果理发师不给自己理发,那么根据定义,他要给自己理发;如果理发师给自己理发, 那么根据定义他不能给自己理发。直觉主义布劳维尔:荷兰数学家, 提出了直觉主义思想, 反对康托尔集合,认为罗素悖论是根源于非构造性的数学,强调构造性证明,反对基于无穷集的排中律。构造性的数学, 才是可靠的数学。优点:可靠,计算科学先驱缺点:杀伤力太强形式主义为了捍卫古典数学的尊严, 1904 年, 希尔伯特在数学家大会上又提出一个证明算术无矛盾性的思路。这个思路也称为形式主义纲领,它的核心思想是将算术表达为一种形式系统或称公理系统, 然后用有穷步骤证明该系统的无矛盾性。哥德尔定理哥德尔研究了希尔伯特纲领, 给出否定的答案,宣告希尔伯特纲领的失败。 193 0年提出的哥德尔第二不完备性定理说,任何包含一阶算术的形式系统,该形式系统的无矛盾性,在该形式系统内无法通过有穷的步骤得到证明。在定理的证明中,哥德尔还提出了很多有用的理论,比如如何把符号编码为自然数,还有使用递归函数来研究有穷证明的能力范围。图灵哥德尔不完备定理出世后,在剑桥大学的图灵设想:能否有这样一台机器,通过某种一般的机械步骤,能够解决所有可以解决的数学问题。他提出了图灵机与图灵可计算。后来,他应邀到美国与丘奇教授一起工作,进一步研究了图灵不可计算的问题。形式主义成为主流至今,数学教科书都以康托尔对角线方法来证明实数集不可数。即使是以构造性为特征的计算科学,也被纳入康托尔集合论的框架中进行理解。奇怪: 没有成功的纲领成为后来的主流? 可能的原因:形式主义继承和发展了构造性,取得巨大的成果。被忽视的维特根斯坦维特根斯坦是罗素学生,上世纪最伟大思想家之一。他听了布劳威尔的讲座,大受震动,又开始思考。他深刻分析了对角线方法,哥德尔定理和各种悖论。他的相关思想长期被忽视。有人评论他是哲学家,而不是数学家,但是数学基础,在很大程度上, 恰恰正是哲学问题。归结到对角线方法后来的研究表明,这些问题密切关联: 康托尔对角线方法罗素悖论等诸多悖论哥德尔定理停机定理等不可计算问题一些研究工作关于对角线方法和哥德尔定理:《基于直觉主义对哥德尔不完