分析基础机器证明系统

作者：郁文生//付尧顺//郭礼权

页数：396

出版社：科学出版社

出版日期：2022

ISBN：9787030706713

电子书格式：pdf/epub/txt

内容简介

本书利用交互式定理证明工具Coq，在朴素集合论的基础上，从Peano五条公设出发，完整实现Landau有名的《分析基础》中实数理论的形式化系统，包括对该专著中全部5个公设、73条定义和301个定理的Coq描述，其中依次构造了自然数、分数、分割、实数和复数，并建立了Dedekind实数完备性定理，从而迅速且自然地给出数学分析的坚实基础。在分析基础形式化系统下，给出Dedekind实数完备性定理与它的几个有名等价命题间等价性的机器证明，这些命题包括确界存在定理、单调有界定理、Cauchy-Cantor闭区间套定理、Heine-Borel-Lebesgue有限覆盖定理、Bolzano-Weierstrass聚点原理、Bolzano-Weierstrass列紧性定理及Bolzano-Cauchy收敛准则等，基于实数的完备性定理，作为应用，进一步给出闭区间上连续函数的重要性质——有界性定理、很值定理、介值定理、一致连续性定理——的机器证明。另外，还给出张景中院士提出的第三代微积分——不用极限的微积分——的形式化系统实现。在我们开发的系统中，全部定理无例外地给出Coq的机器证明代码，所有形式化过程已被Coq验证，并在计算机上运行通过，体现了基于Coq的数学定理机器证明具有可读性和交互性的特点，其证明过程规范、严谨、可靠。该系统可方便地应用于数学分析相关理论的形式化构建。
本书可作为数学与计算机科学、信息科学相关专业的高年级本科生或研究生教材，也可供从事人工智能相关科研工作者参考。

目录

节选

第1章　引言 人工智能研究是当前科技发展的热点和前沿方向，夯实人工智能基础理论尤为重要，数学定理机器证明是人工智能基础理论的深刻体现，参见文献[4-6，9，10，13，16，26，59，67-69，78-80，87，134，139，175，180，184186，189，198，201，220]. 1.1　概述 1.1.1　证明辅助工具Coq 数学定理的计算机形式化证明，近年来随着计算机科学的迅猛发展，特别是证明辅助工具Coq、Isabelle及HOL等[14，35，71，86，92，105，145，148，183]的出现，取得了长足的进展[10，67-69，78-80，87，99，201].Coq是一个交互式定理证明与程序开发系统平台，是一个用于描述定理内容、验证定理证明的计算机工具.这些定理可能涉及普通数学、证明理论或程序验证等[14，35，105，148]多个方面.在推理和编程方面，Coq都拥有足够强大的表达能力，从构造简单的项、执行简单的证明，直至建立完整的理论、学习复杂的算法等，对学习者的能力有着不同层次的要求[14，35，105，148]. Coq是一个交互式的编译环境[14，35，105，148]，用户以人机对话的方式一问一答，用户可以边设计、边修改，使证明中的错误及时得到补证.Coq系统的基本原理是归纳构造演算[14，35，105，148]，是一个形式化系统.Coq支持自动推理程序.Coq通过命令式程序进行逻辑推导，可以利用已证命题进行自动推理.Coq中的归纳类型扩展了传统程序设计语言中有关类型定义的概念，类似于大多数函数式程序设计语言中的递归类型定义[14，35，105，148].Coq有一支强大的全职研发队伍，支持开源.前，Coq已成为数学定理证明与计算逻辑领域的一个重要工具[7，9，30，148，180].2005年，国际著名计算机专家Gonthier和Werner成功基于Coq给出了著名的“四色定理”的计算机证明[67]，进而，Gonthier等又经过六年努力，于2012年完成对“有限单群分类定理”的机器验证(该证明过程约有4300个定义和15000条定理，约170000行Coq代码)[10，68，69]，使得证明辅助工具Coq在学术界得到广泛认可.2015年，Hales等又HOLLight和Isabelle/HOL[71，145]上完成了对“Kepler猜想”的机器验证[87]，Wiedijk在文章[183]中指出，全球各相关研究团队已经或计划完成包括G.del第一不完备性定理、Jordan曲线定理、素数定理以及Fermat大定理等在内的100个著名数学定理的计算机形式化证明.这些成果使得证明辅助工具Coq、Isabelle及HOL等[14，35，71，86，92，105，145，148，183]在学术界的影响日益增强 1.1.2形式化数学 形式化数学在20世纪初对于数学基础的深入讨论中受到重视，对整个20世纪数学的发展产生了深远的影响，参见文[2，18，23，39，46，54-56，73，75-77，85，94，95，97，106，109，111，113，115，117，143，159，166，170，173，179，201，209，213]，虽然有时也饱受过于“形式”的诟病[46，85，111，115，153，167]，但20世纪90年代，特别是进入21世纪以来，随着计算机形式化工具的出现，尤其是上述一系列著名数学难题形式化证明的实现，使得形式化数学与形式化证明辅助工具的结合在学术界得到极大重视. 著名数学家和计算机专家Wiedijk认为当前正在进行的形式化数学是一次数学革命，他在文章[183]中指出，“数学历史上发生过三次革命.第一次是公元前3世纪，古希腊数学家Euclid在《几何原本》引入数学证明方法;第二次是19世纪Cauchy等引入‘严格’数学方法，以及后来的数理逻辑和集合论;第三次就是当前正在进行的形式化数学”[26，183].2002年菲尔兹奖获得者Gowers[72]和Voevodsky[169]、2010年菲尔兹奖获得者Villani[168]以及1987年沃尔夫奖和2005年阿贝尔奖获得者Lax都大力倡导发展可信数学[98].Gowers在文章[72]中指出，“21世纪计算机在证明定理的过程中会起到巨大作用，理论数学研究的模式将会彻底改观，计算机的作用有可能超出我们现在的想象”，甚至预测[72，129]“2099年之前，计算机或可完成所有重要的数学.计算机会提出猜想、找到证明.而数学家的工作，是试着去理解和运用其中的一些结果”.Lax认为“(高速计算机)对于应用数学和纯粹数学的影响可以与望远镜对天文学和显微镜对生物学的影响相比拟”[98]. 当今数学论证变得如此复杂，而计算机软件能够检查卷帙浩繁的数学证明正确性，人类的大脑无法跟上数学不断增长的复杂性，计算机检验将是唯一的解决方案[168，169].今后，每一本严谨的数学专著，甚至每一篇数学论文，都可由计算机检验其细节的正确性，这正发展为一种趋势.英国帝国理工学院的数学教授Buzzard在剑桥举办的一次研讨会上表示:证明是一种很高的标准，我们不需要数学家像机器一样工作，而是可以要他们去使用机器à！关于数学定理的形式化证明，必然涉及国际著名的布尔巴基(Bourbaki)学派[18-21].布尔巴基是一群以法国人为主的数学家的共同名字，他们的思想对于20世纪中叶以来的数学发展具有深刻影响[111，115，173].该学派提出数学结构的概念，并用此概念统一现代数学[18，111，115，173].按照布尔巴基学派的观点，数学中有三大母结构，即序结构[21]、代数结构[19]和拓扑结构[20].基于这三种结构相互交融形成了现代数学的主体内容.利用交互式定理证明工具Coq，可以完整构建这三大母结构的机器证明系统，在此方面国内外都开始进行了一些有益的研究工作[9，11，47，57，78-80，83，84，99，130，160-164，180，188，201，203，207]. 1.1.3分析基础 数学史上最使人惊奇的事实之一，是实数系的逻辑基础竟迟至19世纪后叶才建立起来的[115].而自然数理论公理体系的建立更是基于Dedekind总结出的五条基本性质[95，173]，以Peano[113]发表于1889年的《算术原理——用一种新方法展现》为标志. 经历无数失败和挫折之后，为分析数学寻找基础的工作逐渐有了眉目，这个过程就是19世纪分析算术化的实现，于19世纪末期完成，大体包括三个阶段，见文献[2，54，74-77，85，97，106，111，113，115，173]:第一阶段——极限论建立，主要以法国数学家Cauchy与德国数学家Weierstrass的工作为标志;第二阶段——实数理论建立，主要以德国数学家Dedekind、Cantor与Weierstrass等的实数构造理论为标志;第三阶段——算术化过程完成，以德国数学家Dedekind与意大利数学家、逻辑学家Peano的自然数理论为标志[173].可以看到，分析算术化的过程与克服数学史著名的三次危机，即无理数的发现、分析的严密化、集合论中悖论的消解[179]，是密切相关的[115]. 德国著名数学家Landau发表于1929年的《分析基础:整数、有理数、无理数和复数的运算(微积分补充教材)》[117](简称《分析基础》)，从Peano五条公设[113]出发，依次构造了自然数、分数、分割、实数和复数，并建立了Dedekind实数完备性定理，即Dedekind基本定理，从而迅速且自然地给出数学分析的坚实基础[117]. Landau的名著在世界范围内影响了几代数学家，德文本即出版有四个版次，英文翻译本也至少出版有三个版次[117].在我国，1958年高等教育出版社曾出版有刘绂堂先生翻译的中文版[117].图1.1是Landau《分析基础》的德文-英文版和中文版封面.老一辈数学家丁石孙[211]、严士健[196]、张恭庆[211]等都深受此书影响，并推荐学生研读.Landau的名著[117]问世以来，又有多部论述实数理论的专著，例如[49，142，159，177]，相继出版. 众所周知，Dedekind基本定理与实数完备性的几个著名命题等价，这些命题包括确界存在定理、单调有界定理、Cauchy-Cantor闭区间套定理、Heine-Borel-Lebesgue有限覆盖定理、Bolzano-Weierstrass聚点原理、Bolzano-Weierstrass列紧性定理及Bolzano-Cauchy收敛准则等，而闭区间上连续函数的重要性质——有界性定理、最值定理、介值定理、一致连续性定理——本质上也依赖于实数完备性理论.实数完备性各命题间等价性及闭区间上连续函数性质的人工证明散见于国内外“数学分析”的标准教材，参见文献[1，3，24，25，27，28，36，42，43，48，50，51，58，64，66，89，100-103，107，119，120，131，149，150，152，165，178，187，191，194，211，223，225-228].实数完备性是极限论的基础，上述内容一直是数学分析的重点和难点.近年来仍有人在各类期刊上讨论有关实数完备性定理的证明，特别指出，广州大学袁文俊教授在文献[204，205]中，从上述八大实数完备性定理中的任何一个定理出发，放射性地推出其他七个定理，系统总结了八大实数完备性定理的相互等价性. 图1.1Landau《分析基础》的德文-英文版和中文版封面 20世纪70年代，vanBenthemJutting[13]基于Automath软件平台[22，41，144，182]完成Landau《分析基础》[117]的全部形式化实现.这是数学理论计算机形式化领域里程碑式的工作，影响深远. Automath[13，22，41，144，182]是为实现数学的表示，1970年由荷兰Eindhoven大学deBrujin教授设计的基于λ类型[135，136]理论的数学定理证明器，与基于归纳构造演算的现代类型理论[9，14，30，35，105，148，180]存在较大差异.基于Automath[22，41，144，182]完成的Landau《分析基础》[117]形式化代码[13]，目前看来，在可读性方面也不能令人满意[182]. 2011年，德国Saarland大学著名教授Brown[22]提出，将vanBenthemJutting[13]基于Automath[22，41，144，182]完成的Landau《分析基础》[117]形式化代码用计算机忠实“翻译”成Coq代码的构想，这项“翻译”主要是针对Landau《分析基础》中公理、定义和定理的形式化描述而言的，针对定理机器证明代码的“翻译”难度较大，尚未见报道，相关的研究似仍在进行中.2011年，Smolka和Brown指导的学生Hornung[99]还给出了基于Coq的Landau《分析基础》[117]前四章形式化代码的一个版本.早期关于实数理论形式化的工作还包括:Chirimar和Howe[31]基于Nuprl[33]利用Cauchy序列定义实数，Harrison[90，91]基于Isabelle/HOL[71，145]对实数的构造，Ciaffaglione和DiGianantonio[32]基于Coq直接用无穷序列表达实数，以及Geuvers和Niqui[60]基于Coq利用Cauchy完备性构造实数等. 1.1.4第三代微积分 微积分是数学史上最伟大的成就之一，开启了近代科技的新纪元，对物理学、天文学等其他学科的发展也起到了重要的促进作用.微积分的创立距今已有三百多年的历史[111，115，12