高级搜索 书名 作者 ISBN

交互式定理证明与程序开发：Coq归纳构造演算的艺术

图书分类 　 计算机考试类图书 　 计算机等级考试 软件资格水平考试 计算机类认证考试 数学 　 基础数学教材 数学专业及研究生教材 教辅及考研图书 引进图书 专著、工具书及其他参考书 多媒体课件及网络教学资源 物理 　 基础物理教材 物理专业及研究生教材 教辅及考研图书 引进图书 专著、工具书及其他参考书 多媒体课件及网络教学资源 力学 　 基础力学教材 力学专业及研究生教材 教辅及考研图书 引进图书 专著、工具书及其他参考书 多媒体课件及网络教学资源 化学化工 　 基础化学 化学 化工 引进图书 专著、工具书及其他参考书 多媒体课件及网络教学资源 机械材料汽车能源 　 机械 仪器仪表 材料 汽车 能源与动力工程 引进图书 专著、工具书及其他参考书 多媒体课件及网络教学资源 工业工程 　 国外大学优秀教材-工业工程系列(影印版) 国外大学优秀教材-工业工程系列(翻译版) 物流供应链丛书 其他 普通高等学校物流管理专业系列教材 工业设计 　 工业设计 建筑土木水利 　 建筑学（教材） 建筑设计及建筑文化 土木工程 水利工程 工程管理 装饰装修 环境与给排水 　 环境科学与环境工程 给排水 引进图书 专著、工具书及其他参考书 多媒体课件及网络教学资源 生物与医学 　 医学与生物学教材 教学辅导及考试用书 引进版图书 专业工具书和手册 医学专业参考书 生物学专业参考书 大众读物 电工基础与电气工程 　 电工基础 电气工程 专著、工具书及其他参考书 多媒体课件及网络教学资源 科普读物 　 院士科普第一辑 院士科普第二辑 院士科普第三辑 院士科普第四辑 走进科学殿堂 华裔科学家科普文集 其他 辞书 　 辞书 社会职业培训 　 工程技术操作技能类 城市服务业基础技能类 就业素质教育类 其他 航空航天 　 航空航天 计算机基础 　 计算机文化基础 办公自动化 应用基础 公共基础 软件技术基础 计算机导论 计算机组成与原理 　 计算机组成 计算机原理 接口技术 操作系统 计算机硬件 嵌入式 算法与程序设计 　 C程序设计 数据结构 C++语言 编译原理 Visual Basic Java 汇编语言 FoxPro Delphi 算法 pb 其他 C# JSP 计算机技术及应用 　 计算机技术及应用 计算机网络 　 Internet TCP/IP 计算机网络 网页制作 电子商务 网络安全 网络工程 物联网 图形图像与多媒体 　 图形学 多媒体 图形图像 摄影 计算机辅助设计 　 计算机辅助设计 AutoCAD CATIA 数据库 　 SQL Server FoxPro Access Oracle 数据库原理 数据挖掘 PowerBuilder 数据统计 软件工程 　 软件工程导论 软件工程 软件测试 数理基础 　 数字逻辑 离散数学 线性代数 数理基础 信息安全 　 密码学 概论 病毒防护 电子信息 　 电子信息基础 通信工程 微电子 光电子 自动化 电子信息与计算机 计算机--其他 　 其他 经济管理 　 人力资源管理 物流 工商管理 市场营销 经济学 经济读物 金融学 财政学 国际经济贸易 会计学 旅游管理 公共管理 电子商务 考试用书 其他 管理科学与工程 人文社科 　 伦理学 教育学 心理学 哲学 语言文学 史学 新闻传播学 体育 其他 政治学 社会学 清华校史读物 综合 法律 　 司法考试用书 法律知识读物 宪法与行政法 法理法史 刑法 诉讼法 经济法 民商法 国际法 知识产权法 司法案例 比较法 艺术 　 服装艺术设计 工业设计 环境艺术设计 建筑 染织艺术设计 摄影艺术设计 视觉传达艺术设计 书法 陶瓷艺术设计 信息艺术与设计 绘画 雕塑 工艺美术 艺术设计学 艺术类基础教学 非英语专业本科教材 　 非英语专业本科教材 非英语专业研究生教材 　 非英语专业研究生教材 专升本教材 　 专升本教材 英语专业教材 　 英语专业教材 选修课系列教材 　 选修课系列教材 专门用途英语教材 　 商务英语 其他 学术类图书 　 学术类图书 考试类用书 　 国内考试用书 国外考试用书 工具书 　 工具书 娱乐休闲英语 　 娱乐休闲英语 英语学习方法 　 英语学习方法 非英语语种图书 　 日语 德语 外语--其他 　 其他 高职高专--公共基础课 　 公共基础课系列 高职高专--人文社科类 　 法律专业 新闻 高职高专--计算机类 　 计算机基础教育系列 计算机专业基础系列 计算机应用专业 网络专业 软件专业 数据库专业 多媒体技术专业 电子商务专业 嵌入式设计 高职高专--电子信息类 　 电子信息基础系列 微电子技术专业 通信技术专业 电气自动化专业 应用电子技术专业 高职高专--机电类 　 机电一体化专业 汽车专业 机械基础系列 机械设计与制造专业 数控技术专业 模具设计与制造专业 高职高专--工科类 　 建筑专业 工程管理专业 高职高专--经济管理类 　 经济管理基础系列 市场营销专业 财务会计专业 企业管理专业 物流管理专业 财政金融专业 电子商务专业 国际商务专业 人力资源管理专业 高职高专--服务类 　 旅游专业 饭店管理专业 文秘专业 艺术设计专业 物业管理专业 基础教育--英语 　 教材教辅 课外读物 综合知识 基础教育--信息技术 　 教材教参 课外读物 教师培训 科普读物 中职教育--计算机类 　 计算机基础教育系列 计算机专业基础系列 计算机应用专业 网络专业 软件专业 数据库专业 多媒体技术专业 中职教育--公共课 　 公共基础课系列 中职教育--经济管理类 　 经济管理基础类 物流管理专业 财政金融专业 市场营销专业 企业管理专业 国际商务专业 财务会计专业 中职教育--电子信息类 　 电子信息基础系列 微电子技术专业 通信技术专业 电气自动化专业 应用电子技术专业 中职教育--机电类 　 机械基础系列 机械设计与制造专业 数控技术专业 模具设计与制造专业 机电一体化专业 汽车专业 中职教育--服务类 　 旅游专业 饭店管理专业 文秘专业 艺术设计专业 交互式定理证明与程序开发：Coq归纳构造演算的艺术 作者：Yves Bertot,Pierre Casteran等 图书详细信息： ISBN：9787302208136 定价：59元 印次：1-1 装帧：平装 印刷日期：2009-11-25 图书简介： Coq 是一个用于验证定理的证明是否正确的计算机工具。这些定理可能涉及到普通数学、证明理论或程序验证。 我们的主要目标是从实践的角度来理解Coq 系统及其基本理论：归纳构造演算（the Calculus of Inductive Constructions）。因此，这本书中包含了大量的例子，所有这些例子都可以在计算机上执行。为了教学目的，一些例子解释了错误或笨拙的用法以及避免这些问题的准则。我们也尽量分解对话（dialogues）以便读者能够通过纸笔或直接在Coq 上对其进行重现。有时，我们会给出一些综合表达式；它们乍看起来让人生畏，但事实上也是在Coq 证明辅助工具的帮助下得到的。读者应该在试验时对它们进行分解、修改、了解其结构，并获得一种实际的感受。 本书有一个相关网站1，读者可以从该网站下载并执行所有证明的例子。我们也提供了书中200 个练习的答案，以备不时之需。这本书及其网站使用的工具都是2004 年初发布的Coq V82。 用户对Coq 中已证明的定理的信心来自于构造演算（Calculus of Inductive Constructions）的性质。构造演算是一个形式系统。以λ 演算和类型（typing ）的观点来看，它结合了逻辑中的一些最新进展。这个演算的主要性质已在此处给出，因为我们相信结合理论和实践的知识是使用Coq 全部表达能力的一条最好的路径。 前言： 029058-01.txt 译者序 定理证明是数学领域中一个古老的分支，它从公理出发，利用推理规则为定理寻找证明过程。但是，当我们把数学定理的手工证明和日常生活中的演绎推理变成一系列能在计算机上自动进行的符号演算的过程和技术时，定理证明就成为当今软件工程领域中一种非常重要的形式化技术，即定理证明系统。今天，定理证明系统已经被广泛应用于数学定理证明、协议验证以及软硬件的安全特性验证等方面，成为人们解决关键软件系统正确性、可信性的重要方法，也是继模型检测技术之后未来软件工程领域的一个重要发展方向。 为了帮助我国广大科技工作者和学生更好地学习、掌握和应用定理证明系统，我们CEREUS 小组翻译了《交互式定理证明和程序开发—–Coq 的艺术: 归纳构造演算》一书。选择翻译这本书主要基于如下几点考虑： 1. Coq 是目前国际上交互式定理证明领域的主流工具，它基于归纳构造演算，有着强大的数学模型基础和很好的扩展性，并有完整的工具集。 2. Coq 有一支强大的全职研发队伍，支持开源，这对于想学习和使用该系统的读者非常有益。 3. 本书的作者一直从事Coq 的研发，在书中提供了大量的示例和习题，可以帮助读者更快地掌握Coq，并理解Coq 背后的基础理论。 翻译从来就不是一件轻松的事，尤其是这种既有很深的理论高度，又有很强的实践要求的书，翻译难度就更大了。CEREUS 小组能够在一年内完成本书的翻译工作，不仅饱含了小组全体成员的辛勤劳动，也得到了国际学术界许多研究人员的帮助。参与本书翻译工作的是清华大学软件学院CEREUS 小组，其中第1～8 章由刘柳、周旻、张连怡负责；第9 章由王瑞负责；第10 章和第12 章由张荷花负责；第11 章、第13～14 章由万海负责；第15～16 章由陈钢负责；顾明、陈钢、宋晓宇、荔建琦负责全书的校稿工作。此外，在翻译这本书的过程中，我们得到了本书作者的全力支持，澳门科技大学张昱，中国科技大学“中科大-耶鲁”高可信软件联合研究中心的郭宇、李兆鹏、李勇、王僖和庄重，伦敦大学皇家霍洛威学院的冯扬悦，INRIA的罗正钦等做了本书的审稿工作，在此一并表示感谢。 我们希望这本书作为我国研究定理证明系统的一个新起点，能推动中国定理证明系统的发展，推动我国软件工程的健康发展。我们也希望读者在阅读本书的过程中，能够给我们多提意见。我们的联系方式是：cereus@tsinghua.edu.cn 。 最后，我们要感谢国家自然科学基金委，本书的翻译工作得到“可信软件基础研究”重大研究计划的支持。 前言 Coq 是一个用于验证定理的证明是否正确的计算机工具。这些定理可能涉及到普通数学、证明理论或程序验证。 我们的主要目标是从实践的角度来理解Coq 系统及其基本理论：归纳构造演算（the Calculus of Inductive Constructions）。因此，这本书中包含了大量的例子，所有这些例子都可以在计算机上执行。为了教学目的，一些例子解释了错误或笨拙的用法以及避免这些问题的准则。我们也尽量分解对话（dialogues）以便读者能够通过纸笔或直接在Coq 上对其进行重现。有时，我们会给出一些综合表达式；它们乍看起来让人生畏，但事实上也是在Coq 证明辅助工具的帮助下得到的。读者应该在试验时对它们进行分解、修改、了解其结构，并获得一种实际的感受。 本书有一个相关网站1，读者可以从该网站下载并执行所有证明的例子。我们也提供了书中200 个练习的答案，以备不时之需。这本书及其网站使用的工具都是2004 年初发布的Coq V82。 用户对Coq 中已证明的定理的信心来自于构造演算（Calculus of Inductive Constructions）的性质。构造演算是一个形式系统。以λ 演算和类型（typing ）的观点来看，它结合了逻辑中的一些最新进展。这个演算的主要性质已在此处给出，因为我们相信结合理论和实践的知识是使用Coq 全部表达能力的一条最好的路径。 在推理和编程方面，Coq 的语言都拥有足够强大的能力和表达能力。从构造简单的项，执行简单的证明，到建立完整的理论，学习复杂的算法，对读者能力有着不同层次的需求。按照所需的能力层次，我们对章节进行了标注： （没有标注）初次阅读即可理解， * 中等程度的实践者可以阅读， ** 有能力掌握复杂的推理和证明程序者可读， *** 为有兴趣探索Coq 形式系统所有可能性的专家预留。 练习也有着相同的标注，从基础的练习（可以在几分钟内解决）到非常困难的练习（可能需要几天的思考）。大多数的练习都是我们研究工作中遇到问题的简化版本。 在这本书的编写期间，许多人都给了我们热情的帮助。尤其要感谢Laurence Rideau，她总是非常友好地为我们提供帮助，并且认真地阅读了从最初草稿到最终版本中的每一个版本。Gérard Huet 和Janet Bertot 在帮助我们改进技术准确性和写作风格1 www.labri.fr/Perso/～casteran/CoqArt/。 2 coq.inria.fr。 方面也投入了大量的时间和精力。另外，我们还要特别感谢Gérard Huet 和Christine Paulin-Mohring 为这本书撰写前言。 感谢整个Coq 开发小组，研制了这么强大的工具。特别是要感谢：Christine Paulin-Mohring 、Jean-Christophe Filliatre 、Eduardo Gimenez 、Jacek Chrz.aszcz 和Pierre Letouzey ，在归纳类型的内在一致性、命令式程序表达、co-归纳类型、模块、抽取方面给我们提供的宝贵见解，此外，他们还为本书编写了几页内容和一些例子。除此以外，Hugo Herbelin 和Bruno Barras 和我们一起合作，帮助确保这本书中描述的所有例子都能被实现。 这里，还要感谢我们教过和一起工作过的学生，在与他们共同进行实验的过程中，我们的知识领域也得到了增长。尤其要指出的是，在里昂高师和波尔多第一大学执教时，和Davy Rouillard，Antonia Balaa，Nicolas Magaud，Kuntal Das Barman 和Guillaume Dufay 等合作研究解决一些问题后，才逐渐理解本书中描述的一些观点。 许多学生和研究人员花费了时间来阅读本书的初稿，并把本书作为教学资料使用。他们给我们提供了改进意见，并给出了一些候选的解决方法。我们想在这里感谢那些为我们宝贵的反馈意见的朋友，他们是：Hugo Herbelin 、Jean-Fran.ois Monin 、Jean Duprat Philippe Narbel 、Laurent Théry 、Gilles Kahn 、David Pichardie 、Jan Cederquist、Frédérique Guilhot 、James McKinna 、Iris Loeb 、Milad Niqui 、Julien Narboux 、Solange Coupet-Grimal 、Sébastien Hinderer 、Areski Nait-Abdallah 、Sim.o Melo de Sousa 。 除了以上的朋友外，我们各自的科研环境发挥了关键作用，感谢他们的支持让这个项目通过。特别要感谢INRIA 的Lemme 与Signes 小组和波尔多第一大学的支持，以及欧洲的Types 工作组为我们提供机会，让我们能与富有创新精神的年轻研究人员，如Ana Bove，Venanzio Capretta，Conor McBride 见面交流，本书中一些例子的灵感就来源于他们。 非常感谢Springer-Verlag 出版社的工作人员，他们的帮助使这本书最终能够完成，尤其是Ingeborg Mayer 、Alfred Hofman 、Ronan Nugent 、Nicolas Puech 、Petra Treiber 和Frank Holzwarth 。他们的鼓励，以及在内容、编排、编辑和排版等方面的建议是必不可少的。此外，还要感谢KünkelLopka GmbH 的Julia Merz 所设计的艺术品般的封面。 Sophia Antipolis Yves Bertot Talence Pierre Castéran 序言 Don Knuth 为充实计算机科学基础而写下数卷程序设计名著时，并没有把他的著作名选为《计算机程序设计科学》，而是叫做《计算机程序设计艺术》。此后，经过30 余年的研究，程序设计和算法才成为一门严格的科学。类似地，在形式化证明设计领域，目前正在构建一个严格的基础。尽管证明论的主要概念可以追溯到20 世纪30 年代的Gentzen 、G.del 和Herbrand，图灵本人就已表现出对自动构造数学证明的兴趣。然而，直到1960 年才首次出现进行一阶逻辑自动证明的实验，即系统地枚举Herbrand 域。40 年之后，Coq 证明环境已成为计算逻辑方面一系列探索中的一个最新成果，在某种意义上，它代表了这一领域的当今水平。然而，Coq 的实际使用依然处于一种艺术状态，难以掌握、难以改进。Yves Bertot 和Pierre Castéran 的这本书是一本很有价值的教材，它为初学者提供基础训练，为有经验的人提供必要的专业知识，帮助学习者开发有实用价值的数学证明。 一个简短的关于Coq 系统历史的介绍将帮助读者学习这个软件以及它所实现的数学概念。关于基础概念起源的知识将有助于读者了解用户必须掌握的工作机制，构造系统模型时的各种观点，以及在出现问题时的各种可能的处理方案。 Gérard Huet 在1970 年开始在自动定理证明方面进行工作，他使用LISP 语言实现了带等式的一阶逻辑证明器SAM。当时的研究水平只是把所有的逻辑命题翻译成由文字表（带符号原子公式的析取）组成的表（合取式），量化则由Skolem 函数代替。在这样的表示方法之下，推理过程被归结为基于例化的互补原子公式配对原理（通常称为合一消解原理），等式则产生出相对于合一（modulo uni.cation ）的单方向重写。重写的顺序由人为方法决定，既不保证收敛性，也不保证完备性。证明器是黑箱，它们产生出大量的不可读的逻辑推理结论。当时的常见情形是输入一个假设，然后是等待，直到存储空间用尽。只有在罕见的简单情形下，证明器才会给出答案。这一灾难性状况当时并没有得到充分的理解，人们把它看成是不完全性定理带来的恶魔。然而，复杂性研究很快显示出，哪怕是在可判定的领域，比如命题演算，自动定理证明也注定要撞上组合爆炸的墙。 一个决定性的突破出现在20 世纪70 年代，那是一个系统化方法的实现，它以终结序指导重写。这一进展的基础是Knuth 和Bendix 的奠基性研究工作。Jean-Marie Hullot 和Gérard Huet 在1980 年完成了一个KB 软件，它以一种自然的方式实现代数结构的自动判定过程和半可判定过程。同时，归纳证明领域也取得了稳步的进展，最著名的工作是Boyer 和Moore 的NQTHM/ACL 系统。另一项有重要意义的进展是把消解技术推广到高阶逻辑，方法是使用Gérard Huet 在1972 年所设计的基于简单类型理论的合一算法。该算法同Gordon Plotkin 独立研究的一个方程理论上的通用合一技术本质上一致。 同时，逻辑学家（Dana Scott ）和理论计算机科学家（Gordon Plotkin 、Gilles Kahn、Gérard Berry ）正在研究可计算函数的一种逻辑理论（可计算论域），以及有效可用公理化（可计算归纳），目的是为了定义程序语言的语义。当时人们希望用这个理论严格地处理可信软件的设计问题，这样的设计将采用形式化方法。一个程序相对于它的逻辑规范的正确性可以用数学理论中的定理来表达，算法的数据和控制结构在数学理论中进行描述。在爱丁堡大学，Robin Milner 领导的小组在这方面做出了引人注目的工作。他们的一项重要的成就是在1980 年实现了LCF 系统。该系统颇具智慧地引入了用于辅助证明的策略，后者可以用元语言ML 进行编程。公式不再被归结到无法理解的子句，用户可以使用他们的直觉和知识指导系统进行证明，自动证明（预定义的证明策略和用户使用ML 语言编写的特定证明策略的结合）和手工证明混合在一起。 哲学家Per MartinL.f 探索了另一条研究路线。这一方向从Brower 开创数学的构造性基础开始，经由Bishop 的构造性分析而扩展深化。以此为基础，Per MartinL.f 在80 年代设计了直觉主义类型理论，为数学结构的构造性公理化提供了一个优美的通用框架，而且适合于用作函数式程序设计的基础。康乃尔大学的Bob Constable 教授认真地继续了这一方向的研究，他实现了Nuprl 软件，用于从形式证明中进行软件设计。同时，在Gothenburg 的Chalmers 大学的Brengt Nordstr.m 领导的“程序设计方法组”也进行了类似的研究。 所有这些研究都依赖于最初由逻辑学家Alongzo Church 所设计的λ 演算记号，这一演算的纯粹形式相当于一个用于定义递归泛函的语言，它的带类型的版本相当于高阶谓词演算（即简单类型理论，它是最初在Whitehead 和Russell 的《数学原理》中提出的元数学系统的一个简单变种）。更进一步，λ 演算可用于表示自然推理中的证明，由此产生了著名的“Curry-Howard 对应关系”，它表示了证明结构的空间与函数空间的同构。λ 演算的这两个方面实际上已被用于Automath 系统，该系统是在1970 年由Eindhoven 大学的Niklaus de Bruijn 所设计，目的是为了实现数学的表示。在这个系统中，λ 表达式的类型不再是函数空间中的简单的层次结构。实际上，它们能够表达函数的输入变元同函数的输出结果之间的依赖关系。这可以类比于命题演算扩展到一阶谓词演算，在后一种情况下，谓词的输入项是它的定义域中的元素。 λ 演算的确是证明论中的主要工具。在1970 年，Jean-Yves Girard 证明了分析的一致性，他的证明使用了称为System-F 的多态λ 演算中证明的终止性。这一系统被推广到一个表示多态泛函的Fω 系统，因而可为一类超出了传统序数层次的算法进行编码。1974 年，John Reynolds 在推广ML 语言的受限制的多态结构时，又重新发现了这一系统。 20 世纪80 年代早期，在逻辑和计算机科学的前沿，类型理论获得长足进展。在1982 年，Gérard Huet 联合巴黎高等师范学院的Guy Cousineau 和Pierre-Louis Curien 在INRIA Rocquencourt 实验室启动了Formel 项目。这个小组在LCF 系统的启发之下，准备设计和开发一个更强的证明系统，尤其重要的是，他们准备把ML 语言不仅用于定义tactics，同时用于实现整个系统。这一项在函数式方面的研究和开发工作在 序言VII 几年后产生了CAML 语言族，最终导致了今天的Objective Caml 语言，它就是现在的 Coq 证明器的实现语言。 1984 年，Gilles Kahn 在Sophia Antipolis 组织了一个类型理论的国际会议，在会 上，Thierry Coquand 和Gérard Huet 展示了一个把依赖类型和多态类型综合在一起的系统，它把MartinL.f 的构造性理论融入了Automath 系统的一个扩展，该系统命名为构造演算（Calculus of Constructions）。Thierry Coquand 在博士论文中提供了对这一系统的λ 演算基础的元理论分析。他给出了这一演算终止性的证明，进而给出了关于该演算的逻辑可靠性的证明。这一演算就成了Formel 项目的证明系统的逻辑基础，Gérard Huet 对这个演算CoC 做出了第一个验证器，称为“构造引擎”（Constructive Engine) 。1985 年4 月，在Eurocal 会议上演示了在这个验证器上进行的 几个形式化数学的开发工作。 这就是Coq 系统的第一阶段：一个λ 表达式的类型验证器，在这个系统中，λ 表 达式表示逻辑系统的证明项，或者是数学对象的定义。这个证明助手的核心是与证明 综合工具完全独立的，后者的用途是构造需要验证的项，构造引擎的解释器是一个确 定性的程序。Thierry Coquand 实现了序列（Sequent ）风格的证明综合算法，它提供了 一组类似LCF 系统的证明策略，支持逐步求精方式构造证明项。Coq 第二阶段的开发 由Christine Mohring 完成，在Coq 系统中首次实现Prolog 风格的证明搜索，即著名的 Auto tactic。这可以看成是今天的Coq 系统的正式诞生。在现在的版本中，Coq 核心依 然重新检查用户调用tactic 所构造的证明项。这一架构有一个附加的优点，即简化了证 明搜索的机制，它实际上忽略了类型系统分层所要求的某些约束。 Formel 组很快意识到构造演算可用于综合出带有证书的程序（certi.ed program）， 这一机制与Nuprl 系统的做法相似。一个关键点是利用了多态类型的优势，把一个代数 结构用F 系统的类型表示出来，比如整数，这里系统性地利用了B.hm 和Berarducci 所提出的方法。Christine Mohring 专注于这一问题，她实现了一个复杂的tactic，在构 造演算中综合出归纳原理。以此为基础，她在1986 年6 月举行的“计算机科学中的逻 辑”（LICS）会议上展示了一种开发带证明算法的形式化方法。然而，当她完成了博士 论文之后，她意识到她所使用的impredicative 编码并不遵从常规模式，即把归纳类型 的项限制在类型构造子的复合。多态λ 演算的编码引入了寄生项，因而不能表示合适 的归纳原理。这个部分的失败实际上给了Christine Mohring 和Thierry Coquand 一个 动力，促使他们在1988 年设计了“归纳构造演算”，这是原来系统的一个扩展，增加了 归纳数据类型上的算法的公理化的一些良好的性质。 Formel 小组在理论研究和系统实验两方面始终保持着小心的平衡。他们用模型来 评价各种建议的可行性，用原型来验证系统的能力是否可以扩展到处理实际的证明，他 们提供免费的配备了良好的库和手册的越来越完整的系统，并努力在各版本之间维持 兼容性。这个小组开发的CoC 原型系统转变成Coq 系统，通过网上论坛发布的方式把 该软件提供给感兴趣的用户。同时，基础问题的研究也从不忽略。比如Gilles Dowek 系 统性地研究了合一理论和类型论中的证明搜索，这为以后的Coq 发展提供了坚实的基 础。 1989 年，Coq 4.1 版本发布，该版首次加入了由Benjamin Werner 所设计的从证明中抽取函数式程序（Caml 语法）的机制。此外，还有一组新的进行自动证明的tactics，以及一个小的数学和计算机科学方面的知识库。这一进展标志着一个新阶段（new era ）的开始。Thierry Coquand 在Gothenburg 获得了一个教学的位置，Christine Paulin-Mohring 加入了位于里昂的高等师范学院。此后，Coq 组的工作就在里昂和Rocquencourt 两地继续进行。同时，一个称为Cristal 的新项目开始了，它的主要课题是围绕函数式语言ML 展开研究工作。在Rocquencourt，刚在NuPRL 组完成了经典逻辑的构造性解释的博士论文的Chet Murthy 为Coq 带来了他的新贡献，在Coq 5.8 版本中引入了更复杂的体系结构。在欧洲支持的一项基础研究国际项目“逻辑框架”（Logical Framework） 下开始了国际合作研究，三年之后，又在“类型”项目之下继续进行。几个小组同时在称为“证明助手”（Proof assistant ）的证明工具方面进行开发，他们之间相互激励，分享经验。Coq 是这些证明工具中的一个。其他的“证明助手”有：爱丁堡大学的Randy Pollack 开发的LEGO 系统，剑桥大学的Larry Paulson 开发的Isabelle 系统，该系统后来由慕尼黑大学的Tobias Nipkow 继续，此外，还有Gothenburg 小组开发的Alf 系统等等。 1991 年推出的Coq 5.6 版提供了进行数学描述的统一语言（Gallina“vernacular”）， 原始归纳类型，从证明中抽取程序的机制，和一个图形化用户界面。这使Coq 成为一个可以有效使用的系统，并由此开始了同工业界的有成效的合作，尤其是同CNET 和Dassault-Aviation 的合作。由于出现了第一批学术界之外的用户，促使Coq 组写出了一个教学讲义和使用手册，此时Coq 的使用艺术对于新手依然神秘。Coq 依旧是一个研究性探索的工具和展开实验的场所。在Sophia Antipolis，Yves Bertot 在原来的Centaur 项目基础上开发了CTCoq 界面中的结构操作，使该系统能够利用鼠标进行交互式证明构造，这一技术称为“Proof-by-pointing”，即用户通过鼠标点击来调用tactics。在里昂，Catherine Parent 的博士论文研究了证明中抽取程序的问题，并把该问题转换成另一个问题，把加入不变式注解的程序作为它们自身正确性证明的框架。在波尔多，Pierre Castéran 的工作显示这一技术可被用于构造具有continuation 语义风格的带证明（certi.ed）算法库。在里昂，Eduardo Giménez 在他的博士论文中表明，能够以继承性（hereditarily）方式定义有限结构的归纳类型的框架可以被扩展到一个co-inductive 类型的框架，后者可用于对无限结构公理化。作为一个推论，他开发了涉及数据流操作的通讯协议的证明，这样就为通讯方面的应用打开了一条路。 在Rocquencourt，Samuel Boutin 在他的博士论文中研究了Coq 中自反推理的实现，这一技术在基于代数重写的自动证明中有重要的应用。他的Ring tactic 可用于简化多项式表达式，从而隐式地实现常用的算术表达式代数操作。另外一些判定过程也显著地改进了Coq 系统的自动证明能力：比如在Presburger 算术中使用的Omega （由CNET-Lannion 的Pierre Crégut 开发），在命题演算中使用的Tauto 和Intuition （由Rocquencourt 的César Muňoz 开发)。没有收缩规则（contraction ）的谓词演算中使用的Linear（由里昂的Jean-Christophe Filliatre 开发）。Amokrane Sa.bi 引入了表达继承和隐式强制（coercion ）的子类型的概念，这些概念可用于在广义代数中进行模块化证明开发，尤其是可以简练地表达范畴论的主要概念。 序言IX 1996 年11 月发布的Coq 6.1 版引入了所有上述理论成就，也包括了几项对提高效率有关键作用的技术，特别是Bruno Barras 的规约机制，Christina Cornes 的处理归纳定义的高级证明子。还有Yann Coscoy 的把证明翻译成自然语言（英语和法语）的翻译器，它把证明子构造的证明项用可读的方式表达出来。这是同类证明系统还没有具备的一项重要功能，它使我们能够对形式证明进行检查。 在程序验证的领域中，J.-C. Filliatre 在他1999 年的论文中展示了怎样在Coq 中进行命令式程序的证明。他重新采用了Floyd-Hoare-Dijkstra 倡导的在命令式语言中使用断言的方法，命令式程序被看作是从它们的指称语义所获得的函数表达式所对应的记号。Coq 系统是一个两级架构，核心是CoC 验证器。通过在Coq 中对构造演算的元理论进行形式化，可以从验证算法的正确性证明中抽取出验证器，这一点也显示了进行两级架构划分的意义。这是一项出色的技术成果，它在形式化方法的安全性方面迈出了一大步。为了在数学方面做开发工作，Judica.l Courant 在Objective Caml 的模块机制的启发之下，勾画了一个模块语言的基础，这也为库的可重用性和大规模软件验证开辟了道路。 新成立的Trusted Logic 公司使用Caml 组和Coq 组的技术进行智能卡系统的正确性验证。这也表明了Coq 研究的价值。其他应用项目也纷纷开始。 以后的Coq 系统经历了完全的重新设计，版本7拥有一个函数式核心，主要架构师是Jean-Christophe Filli.tre，Hugo Herbelin 和Bruno Barras 。一个用于tactics 设计的新语言由David Delahaye 开发出来，此后人们可以用高级语言为复杂的证明策略编程。为了对数值软件进行正确性验证，Micaela Mayero 研究了实数的公理化问题。同时，Yves Bertot 重新利用CtCoq 的思想，用Java 语言开发了一个复杂的图形界面PCoq 。 2002 年，也就是Judica.l Courant 完成论文之后的第四年，Jacek Chr.aszcz 采用了类似Caml 的方法把模块和函子系统整合在一起。作为理论开发环境中的一个平滑的结合，这一扩展显著地改进了库的通用性。Pieere Letouzey 提供了从证明中提取程序的一个新算法，它把整个Coq 语言都考虑了进去，包括模块系统。 在应用方面，Coq 已经足够强壮，并可用作实现特定证明工具的低层语言，比如用于时间自动机模拟和验证的CALIFE 平台，用于命令式程序证明的Why 工具，在欧洲项目VERIFICARD 中开发的用于Java 小应用程序（Java applet ）验证的Krakatoa 工具。这些工具使用Coq 语言描述和证明模型的特性，尤其是在自动工具不能处理的复杂情形，这些工具显得很有用。 在经过三年的努力之后，Trusted Logic 成功地完成JavaCard 语言的整个执行环境的形式化模拟。这项安全方面的工作获得EAL7 证书奖（公共标准下最高级别的奖励）。这一形式开发工作使用了121000 行Coq 代码，总共278 个模块。 Coq 也被用于开发先进的数学定理库，包括构造性数学和经典数学。在构造性数学领域中工作需要对Coq 的逻辑语言进行限制，以便同数学家常用的公理保持逻辑上的和谐一致。 在2003 年底，在经过对主要的输入语言进行重新设计之后发布了8.0 版本，这就是本书中采用的版本。 浏览一下Coq 用户群所作的贡献的目录（地址：http://coq.inria.fr/contribs/summary.html），读者将清楚地看到在Coq 中已经完成的数学开发工作的丰富性。开发组遵循Boyer 和Moore 提出的要求，在相继发布的Coq 版本之间保持库的兼容性。在必要的时候，提供一些工具把旧的证明脚本自动转换成新的证明脚本，以此确保用户的开发工作不会因新版本的出现而过时。许多这样的库是由Coq 组外的研究人员所开发的，有的在国外，有的在工业界。我们羡慕这个用户群体对Coq 的坚持，他们完成了非常复杂的证明开发。直到今天，使用Coq 总是带有一定的实验性质，尤其是缺乏一个足够全面细致，逐步深入的用户指导书。 有了本书，这一需求现在得到了满足。Yves Bertot 和Pierre Castéran 多年以来就是Coq 各个版本的专家级用户。他们是Coq 开发组之外的“客户”，正因为如此，他们并不回避Coq 中的潜在问题。他们也不会宣传一个尚不成熟的的解决方案。他们的所有例子都可以在当前的版本中进行验证。他们所写的这本书以渐进的方式介绍了Coq 系统的所有功能。这一陈述详尽的著作所付出的代价是它的厚度。希望初学者不会因此而后退，书中关于内容难度的指示可以帮助他们在学习时作出适合自己的选择，他们不需要从第一页读到最后一页。这本书可以作为一本参考书来使用。用户可以在长期使用Coq 的过程中，在遇到新困难时来查找解决方案。本书包含了大量精心选择循序渐进的例子，这也是此书比较厚的原因。读者常常愿意自己一步步重做一遍这些例子。事实上，我们也建议读者在读这本书的时候要同时使用一台装有Coq 证明器的计算机，一边看书一边操作书中的例子。这本书所展示的是经过30 年形式化方法研究所积累的成果，该领域的内在难度是不能忽略的，要成为使用Coq 的专家就不得不付出一定的代价。这本书经过了三年的编写和修改，这一过程促使了Coq 中的记号统一化，对证明工具的作用做出更简明的解释，并整理出让非专家也能够理解的出错信息。自然，我们承认以后还会有需要改进之处。愿读者在这个即困难又令人兴奋的世界里的探索获得成功。愿他们的努力能够在完成最后一个QED 时得到满足，这可能需要数周甚至数月的艰苦工作，能够到达终点的人会得到应有的收获。 Gérard Huet，Christine Paulin-Mohring 目录： 029058-01.txt 1 概述 ................................................................ 1 1.1 表达式、类型和函数.............................................. 1 1.2 命题和证明...................................................... 2 1.3 命题和类型...................................................... 3 1.4 规范说明和已验证的程序.......................................... 4 1.5 一个排序的例子.................................................. 4 1.5.1 归纳定义.................................................. 4 1.5.2 “包含相同元素”的关系..................................... 5 1.5.3 排序程序的规范说明........................................ 5 1.5.4 一个辅助函数.............................................. 6 1.5.5 排序函数主程序............................................ 6 1.6 学习Coq ........................................................ 7 1.7 本书内容........................................................ 8 1.8 词法约定........................................................ 9 2 类型和表达式 ....................................................... 11 2.1 第一步.......................................................... 11 2.1.1 项、表达式和类型.......................................... 11 2.1.2 解释辖域.................................................. 12 2.1.3 类型检查.................................................. 13 2.2 游戏规则........................................................ 15 2.2.1 简单类型.................................................. 15 2.2.2 标识符、环境、上下文....................................... 16 2.2.3 表达式及其类型............................................ 17 2.2.4 自由和约束变元；α-变换.................................... 24 2.3 声明和定义...................................................... 25 2.3.1 全局声明和定义............................................ 25 2.3.2 Section 和局部变量......................................... 26 2.4 计算............................................................ 29 2.4.1 替换...................................................... 30 2.4.2 归约规则.................................................. 30 2.4.3 归约序列.................................................. 32 2.4.4 可转换性.................................................. 32 2.5 类型、大类和类型空间............................................ 32 2.5.1 Set 大类.................................................. 33 2.5.2 类型空间.................................................. 34 2.5.3 规范说明的定义和声明...................................... 35 2.6 实现规范说明.................................................... 36 3 命题和证明 ......................................................... 39 3.1 最小命题逻辑.................................................... 41 3.1.1 命题和证明................................................ 41 3.1.2 目标和证明策略............................................ 42 3.1.3 第一个目标制导的证明...................................... 42 3.2 类型规则和证明策略的联系........................................ 46 3.2.1 命题构造规则.............................................. 46 3.2.2 推理规则和证明策略........................................ 47 3.3 一个交互式证明的结构............................................ 51 3.3.1 激活目标处理系统.......................................... 51 3.3.2 一个交互式证明的当前阶段.................................. 52 3.3.3 取消操作.................................................. 52 3.3.4 证明的正常结束............................................ 52 3.4 证明无关性...................................................... 53 3.4.1 Theorem 和De.nition 的分析比较............................ 53 3.4.2 证明策略有助于构造程序吗.................................. 54 3.5 Sections 和证明.................................................. 55 3.6 证明策略的结合.................................................. 56 3.6.1 泛证明策略................................................ 56 3.6.2 证明维护问题.............................................. 59 3.7 命题逻辑的完备性................................................ 61 3.7.1 一个完备的证明策略集...................................... 61 3.7.2 不可证命题................................................ 62 3.8 其他证明策略.................................................... 62 3.8.1 cut 和assert 策略........................................... 62 3.8.2 自动证明策略.............................................. 64 3.9 一种新的抽象方式................................................ 65 4 依赖积 .............................................................. 67 4.1 依赖类型的优点.................................................. 67 4.1.1 对A→B 类型的扩展........................................ 68 4.1.2 关于绑定.................................................. 71 目录XIII 4.1.3 一种新的构造.............................................. 72 4.2 类型规则和依赖积................................................ 74 4.2.1 函数应用的类型规则........................................ 74 4.2.2 关于抽象的类型规则........................................ 77 4.2.3 类型推导.................................................. 80 4.2.4 转换规则.................................................. 83 4.2.5 依赖积和可转换性次序...................................... 83 4.3 * 依赖积的表达能力.............................................. 83 4.3.1 积的构造规则.............................................. 84 4.3.2 依赖类型.................................................. 84 4.3.3 多态...................................................... 86 4.3.4 Coq 系统中的相等性........................................ 90 4.3.5 高阶类型.................................................. 91 5 常用逻辑 ............................................................ 95 5.1 依赖积的实用方面................................................ 95 5.1.1 exact 和assumption......................................... 95 5.1.2 intro 策略................................................. 96 5.1.3 apply 策略................................................. 98 5.1.4 unfold 策略................................................ 104 5.2 逻辑联结词...................................................... 105 5.2.1 引入和消去规则............................................ 106 5.2.2 反证法.................................................... 107 5.2.3 否定...................................................... 108 5.2.4 合取和析取................................................ 110 5.2.5 关于repeat 高阶策略........................................ 112 5.2.6 存在量词.................................................. 112 5.3 等价性与重写.................................................... 113 5.3.1 证明等式.................................................. 113 5.3.2 使用等式：重写证明策略.................................... 114 5.3.3 * pattern 策略............................................. 116 5.3.4 * 条件重写................................................ 117 5.3.5 搜索用于重写的定理........................................ 118 5.3.6 用于等式的其他证明策略.................................... 118 5.4 策略总结表...................................................... 119 5.5 *** 非直谓定义.................................................. 119 5.5.1 警告...................................................... 119 5.5.2 True 和False............................................... 119 5.5.3 莱布尼兹等价.............................................. 120 5.5.4 其他一些联结词和量词...................................... 122 5.5.5 书写非直谓定义的指导原则.................................. 123 6 归纳数据类型 ....................................................... 125 6.1 非递归类型...................................................... 125 6.1.1 枚举类型.................................................. 125 6.1.2 简单的推理与计算.......................................... 127 6.1.3 elim 策略.................................................. 128 6.1.4 模式匹配.................................................. 129 6.1.5 记录类型.................................................. 132 6.1.6 带变体的记录.............................................. 134 6.2 分情形推理...................................................... 135 6.2.1 case 证明策略.............................................. 135 6.2.2 矛盾等式.................................................. 137 6.2.3 单射的构造子.............................................. 140 6.2.4 归纳类型和等式............................................ 142 6.2.5 * case 的使用准则........................................... 143 6.3 递归类型........................................................ 147 6.3.1 一个归纳类型—–自然数..................................... 147 6.3.2 在自然数上做归纳证明...................................... 148 6.3.3 递归编程.................................................. 150 6.3.4 构造子的形态变化.......................................... 152 6.3.5 ** 具有函数域的类型....................................... 155 6.3.6 在递归函数上完成证明...................................... 157 6.3.7 匿名递归函数（.x）......................................... 159 6.4 多态类型........................................................ 159 6.4.1 多态列表.................................................. 160 6.4.2 option 类型................................................ 162 6.4.3 二元组类型................................................ 163 6.4.4 不相交和的类型............................................ 164 6.5 * 依赖归纳类型.................................................. 165 6.5.1 一阶数据做参数............................................ 165 6.5.2 可变依赖归纳类型.......................................... 165 6.6 * 空类型........................................................ 167 6.6.1 非依赖空类型.............................................. 167 6.6.2 依赖空类型................................................ 169 7 证明策略和自动化证明 ............................................... 171 7.1 用于归纳类型的证明策略.......................................... 171 7.1.1 分情况讨论和递归.......................................... 171 目录XV 7.1.2 变换...................................................... 172 7.2 auto 和eauto 证明策略............................................ 174 7.2.1 证明策略库管理命令：Hint................................... 174 7.2.2 * eauto 证明策略........................................... 177 7.3 针对重写的自动证明策略.......................................... 177 7.3.1 autorewrite 证明策略........................................ 177 7.3.2 subst 证明策略............................................. 178 7.4 和数相关的证明策略.............................................. 179 7.4.1 ring 证明策略.............................................. 179 7.4.2 omega 证明策略............................................ 181 7.4.3 .eld 证明策略.............................................. 182 7.4.4 fourier 证明策略............................................ 182 7.5 其他决策过程.................................................... 183 7.6 ** 策略定义语言................................................. 184 7.6.1 策略中的变元.............................................. 184 7.6.2 模式匹配.................................................. 185 7.6.3 在已经定义过的策略中使用归约.............................. 191 8 归纳谓词 ............................................................ 193 8.1 归纳属性........................................................ 193 8.1.1 几个例子.................................................. 193 8.1.2 归纳谓词和逻辑程序设计.................................... 195 8.1.3 对归纳定义的建议.......................................... 195 8.1.4 排序列表.................................................. 196 8.2 归纳属性和逻辑连接词............................................ 198 8.2.1 表示真值.................................................. 199 8.2.2 表示矛盾式................................................ 199 8.2.3 表示合取.................................................. 199 8.2.4 表示析取.................................................. 200 8.2.5 表示存在量词.............................................. 200 8.2.6 表示等价.................................................. 200 8.2.7 *** 异构等式............................................... 201 8.2.8 一个奇特的归纳原理? ....................................... 205 8.3 归纳特性的推理.................................................. 206 8.3.1 结构化intros ............................................... 206 8.3.2 constructor 策略............................................ 207 8.3.3 * 在归纳谓词上做归纳....................................... 207 8.3.4 * 对le 进行归纳............................................ 209 8.4 * 归纳关系和函数................................................ 213 8.4.1 表示阶乘函数.............................................. 213 8.4.2 ** 表示一个语言的语义...................................... 218 8.4.3 ** 语义属性证明............................................ 220 8.5 * elim 行为的详细阐述............................................ 223 8.5.1 实例化变元................................................ 223 8.5.2 转置...................................................... 225 9* 函数及其规范 ..................................................... 231 9.1 用于规范的归纳类型.............................................. 231 9.1.1 “子集”类型.............................................. 231 9.1.2 嵌套的子集类型............................................ 233 9.1.3 有认证的不相交和.......................................... 234 9.1.4 混合不相交和.............................................. 235 9.2 强规范.......................................................... 235 9.2.1 良规函数.................................................. 236 9.2.2 将函数构造为证明.......................................... 236 9.2.3 偏函数的前置条件.......................................... 237 9.2.4 ** 对前置条件的证明....................................... 238 9.2.5 ** 增强规范............................................... 239 9.2.6 *** 最小规范增强.......................................... 240 9.2.7 re.ne 策略................................................. 243 9.3 结构递归的变种形式.............................................. 245 9.3.1 多步结构递归.............................................. 245 9.3.2 简化步骤.................................................. 249 9.3.3 多参数递归函数............................................ 250 9.4 ** 二进制除法................................................... 254 9.4.1 弱规范的除法.............................................. 254 9.4.2 良规的二进制除法.......................................... 259 10 * 程序抽取和命令式程序设计 ......................................... 263 10.1 抽取到函数式语言程序............................................ 263 10.1.1 Extraction 命令............................................ 263 10.1.2 抽取机制.................................................. 264 10.1.3 Prop、Set 和抽取........................................... 272 10.2 描述命令式程序.................................................. 274 10.2.1 工具Why ................................................. 274 10.2.2 *** Why 的内部工作原理.................................... 277 目录XVII 11 * 实例分析 ......................................................... 285 11.1 二叉搜索树...................................................... 285 11.1.1 数据结构.................................................. 286 11.1.2 一个直接的存在判定方法.................................... 286 11.1.3 搜索树的描述.............................................. 287 11.2 描述程序........................................................ 289 11.2.1 查找...................................................... 289 11.2.2 插入一个数................................................ 289 11.2.3 ** 删除一个数............................................. 290 11.3 辅助引理........................................................ 290 11.4 规范说明的实现.................................................. 291 11.4.1 查找判定的实现............................................ 291 11.4.2 插入...................................................... 294 11.4.3 删除元素.................................................. 298 11.5 可能的改进...................................................... 299 11.6 另一个实例...................................................... 300 12 * 模块系统 .......................................................... 301 12.1 签名............................................................ 301 12.2 模块............................................................ 303 12.2.1 构造一个模块.............................................. 304 12.2.2 一个例子：Keys ............................................ 304 12.2.3 参数化模块（函子）......................................... 307 12.3 可判定序关系理论................................................ 310 12.3.1 用函子丰富理论............................................ 311 12.3.2 字典序函子................................................ 313 12.4 一个字典模块.................................................... 315 12.4.1 丰富了的实现.............................................. 315 12.4.2 用函子构造字典............................................ 316 12.4.3 一个简单的实现............................................ 316 12.4.4 一个高效的实现............................................ 318 12.5 结论............................................................ 321 13 ** 无穷对象和证明 ................................................. 323 13.1 余归纳类型...................................................... 323 13.1.1 CoInductive 命令........................................... 323 13.1.2 余归纳类型的特殊性质...................................... 323 13.1.3 无限列表（流）............................................. 324 13.1.4 惰性列表.................................................. 324 13.1.5 惰性二叉树................................................ 325 13.2 辅助余归纳类型的技术............................................ 325 13.2.1 构造有限对象.............................................. 325 13.2.2 模式匹配.................................................. 326 13.3 构造无穷对象.................................................... 327 13.3.1 一个失败的尝试............................................ 327 13.3.2 CoFixpoint 命令............................................ 328 13.3.3 余递归函数示例............................................ 329 13.3.4 一些错误的定义............................................ 331 13.4 展开技术........................................................ 332 13.4.1 系统性分解................................................ 333 13.4.2 分解引理的使用............................................ 334 13.4.3 化简对余归函数的调用...................................... 335 13.5 余归纳类型上的归纳谓词.......................................... 336 13.6 余归纳谓词...................................................... 338 13.6.1 无穷序列谓词.............................................. 338 13.6.2 构造无限证明.............................................. 338 13.6.3 违反Guard 约束............................................ 340 13.6.4 消去技术.................................................. 342 13.7 互模拟等价...................................................... 343 13.7.1 bisimilar 谓词.............................................. 344 13.7.2 互模拟等价的使用.......................................... 345 13.8 Park 原理....................................................... 346 13.9LTL............................................................ 347 13.10一个实例：状态迁移系统.......................................... 350 13.11结论............................................................ 351 14 ** 归纳类型基础 ................................................... 353 14.1 形成规则........................................................ 353 14.1.1 归纳类型.................................................. 353 14.1.2 构造子.................................................... 355 14.1.3 归纳原理的构造............................................ 358 14.1.4 递归子的类型.............................................. 360 14.1.5 谓词的归纳原理............................................ 366 14.1.6 Scheme 命令............................................... 368 14.2 *** 模式匹配和证明上的递归...................................... 369 14.2.1 模式匹配的约束............................................ 369 14.2.2 放宽约束.................................................. 370 14.2.3 递归...................................................... 372 14.3 互引归纳类型.................................................... 374 目录XIX 14.3.1 树和森林.................................................. 374 14.3.2 使用互引归纳证明.......................................... 376 14.3.3 *** 树和树列表............................................ 378 15 * 一般递归 .......................................................... 381 15.1 有界递归........................................................ 381 15.2 ** 良基递归函数................................................. 384 15.2.1 良基关系.................................................. 384 15.2.2 可访问性证明.............................................. 385 15.2.3 整合良基关系.............................................. 386 15.2.4 良基递归.................................................. 387 15.2.5 递归子well_founded_induction.............................. 387 15.2.6 良基欧氏除法.............................................. 388 15.2.7 嵌套递归.................................................. 391 15.3 ** 用迭代法实现通用递归......................................... 393 15.3.1 与递归函数相关的泛函...................................... 393 15.3.2 终止性证明................................................ 394 15.3.3 构造具体函数.............................................. 397 15.3.4 证明不动点方程............................................ 397 15.3.5 使用不动点方程............................................ 399 15.3.6 讨论...................................................... 399 15.4 *** 在人为谓词上递归............................................ 400 15.4.1 定义人为谓词.............................................. 400 15.4.2 逆转定理.................................................. 401 15.4.3 定义函数.................................................. 401 15.4.4 证明该函数的特性.......................................... 402 16 * 自反证明 ......................................................... 405 16.1 引言............................................................ 405 16.2 直接的计算证明.................................................. 406 16.3 ** 借助代数计算的证明........................................... 409 16.3.1 基于结合律的证明.......................................... 409 16.3.2 把类型和操作符通用化...................................... 413 16.3.3 *** 交换律：变量排序....................................... 416 16.4 结论............................................................ 419 附录 ................................................................... 421 插入排序............................................................ 421 参考文献 ............................................................... 427 索引 ................................................................... 433 Coq 及它的库........................................................ 433 书中的示例.......................................................... 437 样章： 029058-01.pdf 课件： 网络资源： 配套教学用书（配套教参、主课本等）： 可替代教学用书： 丛书名称：国外经典教材·计算机科学与技术 图书书评：

【欢迎来稿】 总编办：c-service@tup.tsinghua.edu.cn  【选题意向登记表】

客户服务：（010）62776969 c-service@tup.tsinghua.edu.cn

教师服务电话：010-62770175-3506

反盗版举报电话：(010) 62782989 bairsh@tup.tsinghua.edu.cn

质量反馈：(010) 62772015 zhiliang@tup.tsinghua.edu.cn

邮购电话：(010) 62786544 e-sale@tup.tsinghua.edu.cn

邮购地址：北京市海淀区清华大学出版社邮购组收 邮编:100084

读者服务部（购书）：(010) 62781733

通讯地址：清华大学学研大厦 A 座 邮编：100084

网管信箱：netadmin@tup.tsinghua.edu.cn

版权所有(C)2005 清华大学出版社有限公司

Copyrights @ 2005 by Tsinghua University Press. All Rights Reserved 京ICP备 05029640 号