陈意云编译原理全套陈意云编译原理全套chap1

第1章 引 言 1.1 基本概念 1.1.1 模型语言 对程序设计语言进行数学分析通常是从设计模型语言开始，而且模型语言的设计一般要突出感兴趣的程序构造，忽略一些无关的细节。例如，若想分析过程调用机制，可先设计一个简单的程序设计语言，它的主要构造是过程声明和调用。然后分析该简化语言。这种方法不仅对分析现行的程序设计语言有用，而且有助于新语言的设计。因为实际的程序设计语言是非常庞大和复杂，语言的设计必须包括仔细地和分离地考虑各个子语言。当然，必须记住，从简化语言可能会得出一些错误印象。因此，在进行程序设计语言的理论分析和把理论分析用于实际情况时，不要忘记所做的简化及这些简化对结论的影响。 上世纪60年代，人们发现，可以把一个复杂的程序设计语言形式化为两部分：一部分是能抓住该语言本质机制的一个非常小的核心演算；另一部分是一组导出形式，它们的行为可以通过把它们翻译成这个核心演算来理解。通过这种方式来理解语言要深刻得多。这个核心语言就是(演算（lambda calculus）。 (演算是上世纪20年代确立的一种形式系统，它源于可计算理论，是奠定函数定义和程序设计语言中命名约定的基本机制。在这种系统中，所有的计算都归约到函数定义和函数应用这样的基本操作。上世纪60年代以来，(演算已广泛用于 规范 编程规范下载gsp规范下载钢格栅规范下载警徽规范下载建设厅规范下载 程序设计语言的特征、语言设计和实现、和类型系统的研究中。它的重要性在于它同时可以看成一种简单的程序设计语言（用于描述计算）和看成一个数学对象（有关它的一些严格的陈述可以证明）。 本书将用类型化(演算（typed lambda calculus）的框架来研究程序设计语言的各种概念。用不同方式来扩充基本的类型化(演算，可以设计出多种模型语言，它们包含历史的、现代的、甚至将来的语言特征。盯在类型化(演算上的一个优点是，所建立的理论有某种程度的“模块性”。类型化(演算的许多扩充可以组合在一起，一般来说这种组合不会出现出乎意料的叠加影响（当然也会有例外）。例如，在分别调查了多态性和 记录 混凝土 养护记录下载土方回填监理旁站记录免费下载集备记录下载集备记录下载集备记录下载 后，很容易定义出含多态性和记录的语言，并且指出它的很多性质。 本书研究程序设计语言的概念和特征的目的是透过表面的语法，对各种程序短语（表达式、命令和声明等）理解到一个适当详细的程度。 本章介绍一个非常简单的，以自然数和布尔值作为基本类型的，基于类型化(演算的语言，介绍该语言的语法、操作语义和它在程序设计中的能力。该语言是第2章介绍的可计算函数程序设计（Programming Computable Functions，简称PCF）语言的一个简化版本。通过这个简要介绍，读者可以对本书将要采用的技术和方法有一个浅显的了解。 本章的主要议题如下： ( (表示法和(演算系统概述； ( 类型和类型系统的扼要讨论； ( 基于表达式的归纳、基于证明的归纳和良基归纳法。 本书以后各章也按此风格，即每一章有一节导言，导言中包含该章的主要议题。 1.1.2 (表示法 在描述、分析和实现程序设计语言时，(演算已被证明是非常有用的。梢加练习，读者很快就会熟悉这种表示法，并且可以明白，C、Pascal和Ada的程序短语都是在(表达式的基础上做了语法美化。这就使得本书描述的理论更加有用，而且使得程序设计语言的多样性更容易理解。语言PCF将直接使用(表示法，就象Lisp语言那样；所不同的是，PCF没有表和原子，但它有相对严格的编译时的定类 规则 编码规则下载淘宝规则下载天猫规则下载麻将竞赛规则pdf麻将竞赛规则pdf 。 (表示法的主要特征是(抽象和(应用，前者用于定义函数，后者允许使用定义的函数。用(表示法写出的表达式叫做(表达式或(项。(表示法既可用于类型化(演算，也可用于无类型(演算。 在类型化(演算中，函数的论域（domain）由给出形式参数的类型来指定。如果变元x的类型是(，M是基于这个假定的合式（well formed）表达式，那么(x:(.M定义一个函数，它把( 类型的任何x映射到由M给定的一个值。一个简单的(抽象的例子是： (x : nat.x 它是自然数上的恒等函数。记号x : nat说明该函数的论域是nat，即自然数类型。在该表达式中，点后面的部分是函数体。因为该例的函数体也是x，因此该函数的值域也是nat。 每一种形式的类型化(演算，都有精确的规则来说明，在一个给定的变量类型的假设下，什么样的表达式是合式的。这些规则表明怎样从函数体M的形式去确定(x : (.M的值域。例如，表达式(x : nat.x ( true不是合式的，因为true和自然数相加是没有意义的。 用程序设计语言定义恒等函数，最熟悉的形式可能是 Id ( x : nat ) = x 但是这种形式迫使为每个函数起一个名字，而(表示法给出了直接定义函数的一种简洁方式。例如， (x : nat.x ( 1 定义了自然数上的后继函数。 (x : nat.10 是自然数上的一个常函数，该函数的值恒为10。 在(抽象中，(是一个约束算子，这意味着在(项(x : (.M中，变元x是一个占位符，就像在谓词演算公式 (x : A.( 中的变元x那样。因此可以重新命名(约束变元而不改变表达式的含义，只要所选择的新变元与其它已经使用的变元没有冲突便可以了。仅仅约束变元名字不同的项称为(等价的。如果M和N是(等价的，可以写成M (( N。如果x出现在表达式M中，并且它出现在形式为(x:(.N的子表达式中，那么称x的这个出现是约束的（bound），否则是自由的。注意，在一个表达式中，x可能既有约束出现也有自由出现。不含自由变元的表达式称为闭表达式。 在(表示法中，用项的并置来表示函数应用，并且用括号来说明运算对象的结合。例如，把恒等函数应用于5可写成 ((x : nat.x) 5 这个函数应用的结果是5，即 ((x : nat.x) 5 ( 5 下一节将看到，可以有几种不同的方式来计算(表达式的值或证明(表达式间的等式。 (表示法中有两个约定，以省略(表达式中的大量括号。第一个约定是函数应用是左结合的，即MNP应看成(MN)P。第二个约定是每个(的约束范围尽可能地大，一直到表达式的结束或碰到不能配对的右括号为止。例如，(x:(.MN解释为(x:(.(MN)，而不是((x:(.M)N。同样地，(x:(.(y:(. MN是(x:(.((y:(.(MN))的简写。这两个约定当然可以一起使用。例如，多元函数应用可写成 ((x:(.(y:(.(z:(.M)NPQ 它是 ((((x:(.((y:(.((z:(.M)))N)P)Q 的简写。 1.1.3记号和约定 本书用到的数学基础主要是集合论的知识，包括关系和函数，这些是大家已经熟悉的，本书不再重复。本书用到的各种归纳法另用一节专门介绍。 本书使用几种形式的相等符号，这些符号及它们的含义如下： ( 两个表达式有相同的值。 ( 除了约束变元的名字可能不同以外，两个表达式语法上相同。 =def 用M =def N来表示符号或表达式M被定义成等于N。 ((( 该符号在文法中用来表示表达式的可能形式。 ( 表示（集合、代数等的）同构。 本书使用的逻辑符号如下： ( 全称量词。公式(x.(可以读成“对所有的x，(为真”。 ( 存在量词。公式(x.(可以读成“存在一个x使得(为真”。 ( 合取。公式( ( ( 可以读成“( 合取(”。 ( 析取。公式( ( ( 可以读成“( 析取(”。 ( 否定。公式(( 可以读成“非(”。 ( 蕴涵。公式( ( ( 可以读成“( 蕴涵(”。（不使用(作为蕴涵，因为(用于类型表达式，并用于表达式的归约（计算）。） iff 当且仅当。 本书中使用的集合运算符号如下： ( 属于。 ( 并集。 ( 交集。 ( 子集。 ( 笛卡儿积。 1.2 等式、归约和语义 在历史上，(表示法是(演算（lambda calculus）的一部分，(演算是关于(表达式的一个推理系统。除了语法外，这个形式系统有三个主要部分。按照现代程序设计语言的术语，它们分别叫做公理语义、操作语义和指称语义。逻辑学家可能把前二者叫做证明系统，而把第三者叫做一种模型论。公理语义是推导表达式之间等式的一个形式系统。操作语义是一种基于一个方向的等式推理，叫做归约。按计算机科学术语，归约可看成符号计算的一种形式。指称语义，或模型论，本质上类似于其它逻辑系统（如等词逻辑或一阶逻辑）的模型论。一个模型是一组集合，每种类型一个集合，这个集合就是对应类型的解释域，并且每个良类型（无类型错误）的表达式都可以解释为相应集合上的一个元素。 本节是对本书常用的语义方法做一个扼要的介绍，让读者有一个粗浅的认识。 1.2.1 公理语义 公理语义用逻辑系统来描述程序的性质，即它是一个证明系统，可用来推导程序及其组成部分的性质。这些性质可以是项之间的等式、给定输入下有关程序输出的断言、或其它性质。 现在这里给出的是一个等式公理系统，它有约束变元改名公理，还有把函数应用联系到代换的一个公理。为了表示这些公理，需要使用记号(N(x(M，它表示M中的自由变元x用表达式N代换的结果。代换时需要注意的一件事是不能把M中的自由变元变成约束的。把M中的自由变元x用N代换的最简单办法是，首先将M中所有的约束变元改名，使得它们和N中的自由变元都有区别，然后再将x的自由出现用N代替。第2章将给出更详细的定义。使用代换，约束变元改名公理可写成 (x:(.M ( (y:(.(y(x(M， M中无自由出现的y (() 例如，(x:(.x ( (y:(.y。 因为项(x:(.M定义了一个函数，因此可以通过用N代替x来计算该函数应用于N的结果。例如，将函数(x:nat.x+4应用于4的结果是 ((x:nat.x+4) 4 ( [4/x](x+4) ( 4 + 4 更一般而言，等式公理 ((x:(.M)N ( [N/x]M (()eq 被称为( 等价公理。本质上，( 等价是说，计算函数应用就是在函数体中用实在变元代替形式变元。除了这些公理和个别其它公理外，等式系统还包含对称性规则、传递性规则和同余规则。同余规则是说，相等的函数作用于相等的变元产生相等的结果，可以写成 当然，为了完全精确，还应说明它们的类型，以保证每个项都有意义。和其它逻辑证明系统一样，类型化(演算的等式证明规则允许推导任何一组等式前提的逻辑推论。 1.2.2 操作语义 语言的操作语义可用不同的方式给出，一种接近实际实现的方式是定义一个抽象机，它是一种理论上的计算机，然后通过一系列的机器状态变换来计算程序。操作语义最实际的表示就是语言的解释器。操作语义比较抽象的表示是演绎出最终结果的证明系统，或者说是通过一系列步骤变换一个表达式的证明系统。本书集中于操作语义的后一种形式，即定义完备的或一步一步计算的证明系统。 前面所列的等式公理的单向形式给出了(演算的归约规则。直观上讲，基本归约规则描述了单步符号计算，它们可以反复用于表达式的计算，直至得到表达式的最简形式，或因无最简形式而计算不终止。符号计算过程给出了(演算的计算特征。因为归约是非对称的，箭头(通常用于一步归约，双箭头(( 用于任意步（包括零步）归约。 最核心的归约规则是(()eq的单向形式，叫做( 归约，写成 ((x:(.M)N (( [N/x]M (()red 因为在代换时约束变元可能需要改名，因此归约是定义在(等价上的。即( 归约的结果依赖于新约束变元的选择，它不是唯一确定的。但是归约产生的任何两个项仅在约束变元的名字上有区别，因此是(等价的。 除了 (()eq规则外，还有一些其它的归约规则。完整的归约系统及其性质在后面章节讨论。 1.2.3 指称语义 用指称方法定义语言语义的基本 思想 教师资格思想品德鉴定表下载浅论红楼梦的主题思想员工思想动态调查问卷论语教育思想学生思想教育讲话稿 是：先确定指称物，然后给出语言成分到指称物的语义映射，这个映射要满足： （1）每个成分都有对应的指称物； （2）复合成分的指称只依赖于它的子成分的指称。 在类型化(演算的指称语义中，每个类型表达式对应到一个集合，称为该类型的值集。类型( 的项解释为其值集上的一个元素。类型( (( 的值集是函数集合，因此项(x:(.M解释为一个数学函数。纯类型化(演算的语义是简单的，而它的各种扩充的语义可能会比较复杂。具有挑战性的特征有函数的递归定义、类型的递归定义和多态函数等。除了不讨论递归定义的类型的指称语义外，其它两个概念的指称语义在后面都会详细讨论。 对于熟悉无类型(演算的读者来说，值得一提的是，无类型(演算可以从类型化(演算中派生出来。事实上，考虑无类型(演算的语义的最自然方式之一是从类型化(演算的语义开始。基于这个原因，类型化(演算被看成是更加基本的系统，更适于作为研究的起点。 1.3 类型和类型系统 在计算机科学和数理逻辑的一般文献中，单词“类型”在不同的上下文中有不同的含义。在本书中，类型是一个基本术语，它的含义由类型系统的精确定义给出。在任何类型系统中，类型提供了所有可能值的全体的一种分类：一个类型是一群有某些公共性质的值。对于不同的类型系统，类型的多少和值所属的类型可能不同。 本节扼要介绍类型系统的有关概念和应用。 1.3.1 类型和类型系统 一个程序变量在程序执行期间的值可以设想为有一个范围，这个范围的一个界叫做该变量的类型。例如，类型bool的变量x在程序每次运行时的值只能是该类型的值。如果x有类型bool，那么布尔表达式not (x)在程序每次运行时都有意义。变量都被给定（非平凡）类型的语言叫做类型语言。 语言若不限制变量值的范围，则被称作未类型化的语言（untyped language），它们没有类型，或者说仅有一个包含所有值的泛类型。在这些语言中，一个运算可以作用到任意的运算对象，其结果可能是一个有意义的值、一个错误、一个异常或一个未做说明的结果。 类型语言的类型系统是该语言的一个组成部分，它始终监视着程序中变量的类型，通常还包括所有表达式的类型。一个类型系统主要由一组定型规则（typing rule）构成，这组规则用来给各种语言构造（程序、语句、表达式等）指派类型。 在计算机科学中，类型系统的研究有两个分支：比较实际的一支是类型系统在程序设计语言中的应用；比较抽象的一支关心“纯类型化(演算”和不同逻辑之间的对应关系。本书主要研究前面一个分支。 为语言设计类型系统的目的是什么？简单讲，类型系统的根本目的是用来证明程序不会出现不良行为，例如将整数和布尔值相加。只有那些顺从类型系统的程序才被认为是类型语言的真正程序，其它的程序在它们运行前都应该被抛弃。 当用一种程序设计语言所能表示的所有程序运行时都没有不良行为出现时，就说该语言是类型可靠的（type sound），类型可靠的语言又称为安全语言。显然，希望通过适当的分析来对程序设计语言的类型可靠性做出准确的回答。这种分析将基于语言的类型系统，这样，类型系统的研究也需要形式化的方法。 类型系统的形式化需要研究精确的表示法和定义，需要一些形式性质的详细证明，这是本书的一个重要内容。形式化的类型系统提供了概念上的工具，用它们可以评判语言定义的一些重要方面的适当性。非形式语言的描述通常不能把语言的类型结构详细规范到不会出现歧义实现的程度，因此经常会出现，同一个语言的不同编译器实现了略有区别的类型系统。而且，许多语言定义被发现不是类型可靠的，甚至经过类型检查（type check）后接受的程序也会崩溃。理想的状况是，形式化的类型系统应该是类型化程序设计语言的定义的一部分。这样，依靠精确的规范，证明语言是类型可靠的才有可能。 一种语言由一个实质存在的类型系统来类型化，而不在乎类型是否实际出现在程序的语法中。一种语言，如果类型是语法的一部分，那么该语言是显式类型化的；否则是隐式类型化的。主流语言中不存在纯隐式类型化的语言，但是ML和Haskell这样的语言支持编写忽略类型信息的程序片段，这些语言的类型系统会自动地给这些程序片段指派类型。 1.3.2 类型语言的优点 从工程的观点看，类型语言有下面一些优点： （1）开发时的实惠 有了类型系统可以较早发现错误，例如整数和串相加。若类型系统很好地设计时，类型检查可以发现大部分日常的程序设计错误，剩下的错误也很容易调式，因为大部分错误已经被排除。 对于大规模的软件开发来说，接口和模块有方法学上的优点, 类型信息在这里可以组织到程序模块的接口中。程序员可以一起讨论要实现的接口，然后分头编写要实现的对应代码。这些代码之间的相互依赖最小，并且代码可以局部地重新安排而不用担心对全局造成影响。 程序中的类型信息还具有文档作用。程序员声明标识符和表达式的类型，也就是告诉了所期望的值的部分信息，这对阅读程序是很有用的。 （2）编译时的实惠 程序模块可以相互独立地编译，例如Modula-2和Ada的模块，每个模块仅依赖于其它模块的接口。这样，大系统的编译可以更有效，因为改变一个模块并不会引起其它模块的重新编译，至少在接口稳定的情况下是这样。 （3）运行时的实惠 在编译时收集类型信息，保证了在编译时就能知道数据占空间的大小，因而可得到更有效的空间安排和访问方式，提高了目标代码的运行效率。例如，像Pascal的记录、C的结构和对象，其域或成员的偏移可以根据它们的类型信息静态地确定。 另外，一般来说，精确的类型信息在编译时可以保证运行时的运算都作用到适当的对象并且不需要昂贵的运行时的测试，从而提高程序运行的效率。例如在ML中，精确的类型信息可以删除在指针脱引用（dereference）中的nil检查。 上面提到，类型信息具有文档作用，但是它和其它形式的程序评注不同。一般来说，关于程序行为的评注可以从非形式的注解一直到用于定理证明的形式规范。类型处在该范围的中间：它们比程序注解精确，比形式规范容易理解。另外，类型系统应该是透明的：程序员应该能够很容易预言一个程序是否可通过类型检查，如果它不能通过类型检查，那么其原因应该是明显的。 除了这些传统的应用外，在计算机科学和有关学科中，类型系统现在还有许多应用，这里列举其中一些。 （1）类型系统一个越来越重要的应用领域是计算机和网络安全。在网络计算中出现的安全问题，像移动代理的资源访问、信任管理，也能够依赖类型系统来解决。例如，编译时收集的类型信息附加在移动代码中，可供移动代码接受方检查该代码是否符合基本安全策略：类型安全、控制流安全和内存安全等。还有，静态定型处于Java安全模型的核心。 （2）除了编译器外，还有许多程序分析工具使用类型检查或类型推断算法，例如，一些别名分析工具使用类型推断技术。 （3）在自动定理证明方面，类型系统（尤其是基于依赖类型的类型系统）用来表示逻辑命题和证明，一些著名的定理证明辅助工具都是直接基于类型论。 有些语言将类型检查推迟到程序运行的时候。例如，虽然Lisp程序在编译时没有类型检查，但是运行时的检查保证表操作只能用于表。因为运算对象的准确值在运行时是知道的，因此运行时的检查更加精确，而且只有那些在运行时真正会出现的错误才会被查出。举个简单的例子说明动态检查和静态检查的区别。例如，对于条件表达式 if B then 3 else 4 + “polyglot” 在运行时，若B的值为true，那么它不含运行时的错误。但是大多数编译时的检查器会拒绝这个表达式。因为一般而言，表达式的值在编译时是确定不了的，因而编译时的类型检查只能用稳妥的策略，从而拒绝了一些不含运行错误的程序。基本递归论的一个结论是：预测运行时类型错误是程序的一个不可判定性质。 本书将集中在可静态确定类型的语言上，即每个程序短语必须有一个类型。除了极端情况外，类型可以从其语法形式有效地确定。第4章讨论的语言将由一组确定类型的规则来定义。每个合式短语有一个类型，一遍扫描可确定短语的类型。其中没有局部声明的标识符的类型可以从某个符号表得到。 集中于静态类型语言的原因是，把注意力集中到正确的程序上，不必管有错的程序，因而不必考虑运行时类型错误的检查。只考虑良类型的程序可以使理论比较简单。考虑静态类型语言的另一个理由是，类型允许以某种方式推导表达式的值，这对非类型语言或运行时才能检查类型的语言是不可能的。 1.4 归纳法 1.4.1 表达式上的归纳 本书包含许多归纳证明。最常用的是基于表达式结构的归纳和基于证明的长度或结构的归纳。本节介绍一些归纳法，对于大家已经熟悉的两种自然数归纳法（见下面表1.1），略去不作介绍。 可以使用自然数归纳法来证明树的性质，只要有方法把每一棵树联系到一个自然数。也可以为树和一些其它数学对象类阐明独立的归纳原理，最关键的问题是，要能够为一类数学对象安排一个适当的次序，使得每个对象可以从最小对象经过有限步的构造得到。直观上，这种次序允许写出一种形式的无限证明，最终覆盖关心的每一个对象。首先考虑表达式上的归纳。 通常用文法来定义表达式集合，如： e ::= 0 | 1 | v | e + e | e ( e 假定V是变量符号的无限集合，该文法中的v 表示V的任何元素都是一个表达式。由这个文法产生的表达式都有一棵分析树，可以由对分析树的高度进行归纳来证明表达式的性质。更精确地说，如果P是表达式的一种性质，可以定义自然数的一种性质Q如下： Q(n) =def (树t.如果height(t) = n 并且t是e的分析树，那么P(e)为真。 注意，即使某些表达式的分析树多于一棵时，这也是一个合理的自然数性质。要想得到更加清楚的证明方式，还是为表达式使用一种专门的归纳形式。使用自然数归纳证明的本质步骤来解释这种形式的归纳证明。 假设从表达式上的性质P开始，并且象上面那样定义了自然数上的一个性质Q。如果使用自然数归纳法来证明(n.Q(n)，那么首先必须为高度是0的分析树直接证明P。然后，对于高度至少为1的树，假定对于分析树的高度较小的表达式，P都成立。就上面所给的文法而言，对于0，1和变量v，必须直接证明P。对于形式为（e + e）和（e ( e）的复合表达式，可以假定P对子表达式e1和e2都成立。由此分析可以得出基于表达式结构的归纳，其形式如下： 结构归纳，形式1 为了证明对某个文法产生的任意表达式e，P(e)为真，只要完成下面两步证明就足够了。 （1）对每个原子表达式e，证明P(e)； （2）对直接子表达式为e1,…, ek的任何复合表达式e，证明，如果P(ei)（i=1,…, k）都为真，那么P(e) 也为真。 对于上面所给出的文法，则有下面的 模板 个人简介word模板免费下载关于员工迟到处罚通告模板康奈尔office模板下载康奈尔 笔记本 模板 下载软件方案模板免费下载 ： 目标：对每个表达式e，证明P(e)。 归纳基础：证明P(0)和P(1)，并对任何变量v证明P(v)。 归纳步骤：证明，对任何表达式e1和e2，如果P(e1)和P(e2)为真，那么P(e1 + e2)和P(e1 ( e2)也为真。 还有另一种形式的结构归纳，它在归纳假设中包含了所有的子表达式，只不过这种区别不象自然数归纳那样强调。 结构归纳，形式2 为了证明对某个文法产生的任意表达式e，P(e)为真，只要完成下面的证明就足够了： 对任何表达式e，如果P(e()对e的任何子表达式e(都成立，那么P(e)也成立。 形式1和形式2的区别在于，形式2的归纳假设包含了所有的子表达式，并非只是直接子表达式。 可以把自然数归纳的两种形式看成是结构归纳对应形式的特别情况。请看文法 n ::= 0 | succ n 直观上说，n的后继succ n是n (1。每个自然数都可以用这个文法写出来，并且该文法的表达式上的两种归纳形式正好对应到自然数上的两种归纳形式。 1.4.2 证明上的归纳 基于证明结构的归纳和基于表达式结构的归纳本质上是一样的。在许多方面，两者都是树上的归纳形式。在论述证明结构上的归纳之前，先回顾一般证明系统的一些公共的基本概念。 希耳伯特风格的证明系统由公理和推理规则组成。证明系统的公理是一个公式，它被定义成可证明的。推理规则用来断言：如果某一组公式是可证明的，那么另一个公式也是可证明的。证明是一个结构化的对象，它由公式来构造，这些公式遵循由一组公理和推理规则奠定的约束。下面将完整地描述证明。 公理和推理规则代表一种给定形式的所有公式或证明步骤，通常写成模板。例如，相等的自反公理 e = e (ref) 叫做“带元变量e 的模板”。这个公理模板断言，每个形式为e = e的等式是一个公理。例如，只要x，y和3都是合式表达式，那么x = x，y = y和3 =3都是公理。通常，推理规则模板的形式是 其含义是，如果有形式是A1, …, An的公式的证明，那么把它们合起来可以得到公式B的证明。例如，相等的传递性规则可以写成 (trans) 这意味着如果有3 + 5 = 8的证明和8 = 23的证明，那么把它们合起来可以形成等式3 + 5 =23的证明。横线上面的公式叫做证明规则的前提，横线下面的公式叫做结论。 形式地讲，证明可以定义为一个公式序列，该序列中的每个公式都是公理或者是由前面的公式通过一个推理规则得到的结论。证明的这种形式定义是非常有用的，它使得可以基于证明的长度（也就是该序列的长度），用自然数归纳法来讨论证明的性质。另一种观点显得更有见识，推理规则通常由一组前提和一个结论组成，很容易把证明看成是某种形式的树，其叶结点和内部结点由公式标记。也就是把证明所用的公理看成叶结点，把所用的推理规则 看成树的内部结点，其子树必须是A1, …, An的证明。为了和推理规则通常的图示方向一致，画证明树时一般把树根放在底部。这样，如果从A1, …, An的证明构造B的证明，其证明树的形式见图1.1。在图1.1中，在横线上的每个三角形代表一棵证明树，它的结论是本证明规则的一个前提。把证明看成树的一个好处是，它提示了一种归纳形式，它本质上同树的结构归纳是一样的。 如果基于证明树的高度进行归纳，那么归纳基础是：每个公理具备某性质；归纳步骤是：假定任何较短的证明都有这个性质，然后证明，结束于各个推理规则的证明也都具有这个性质。这就形成了证明上的结构归纳，其形式如下： 证明上的结构归纳 在某个证明系统中，为了证明对每个证明(，P(()为真，只要完成下面两步就足够了： （1）对该证明系统中的每个公理，证明P成立； （2）假定对证明(1, …, (k，P成立，证明P(()也为真。(是这样的证明，它结束于用一个推理规则，并且是从证明(1, …, (k延伸出来的一个证明。 例1.1 本例用一个简单的证明系统来介绍证明结构上的归纳，它是表达式小于或等于关系（e ( e(）的一个简单证明系统，其中e和e(由下面的文法产生： e ::= 0 | 1 | v | e + e | e ( e 该证明系统有两个公理，其一是说(是自反的： e ( e (ref) 另一个是说0小于或等于任何表达式： 0 ( e (0 () 该系统有一个传递性推理规则，另有两条规则表示加和乘的单调性。 (trans) (+mon) ((mon) 对于自然数上平常的序，这是一个相对弱的证明系统，但是对于举例说明基本概念来讲是足够了。 对一个证明系统来说，需要确立的一个非常普通的性质是，在公式的某种特定解释下，每个可证明的公式为真。这叫做证明系统的可靠性（soundness）。现在证明该证明系统对(是可靠的，以此为例来说明证明结构上的归纳，其中该文法的算术表达式按通常的方式解释。具体说，需要证明下面的性质对任何证明(都成立： P(() =def 如果(是e ( e(的一个证明，那么e的值 ( e(的值，不管其中的变量怎样取值。 归纳基础是为所有的公理证明该性质。这是非常容易的。不管e的变量怎样取值，e的值总是某个自然数。因此总有e ( e和0 ( e。 本证明的归纳有三步，这里证明（+mon）和（(mon）两种情况，而把（trans）留给读者。假定可以证明e1 ( e2和e3 ( e4。任意选择e1, …, e4中变量的值，并把这四个表达式的值叫做n1, …, n4。由归纳假设，有n1 ( n2和n3 ( n4。很容易看出n1 + n3 ( n2 + n4，同样有n1 ( n3 ( n2 ( n4。因为这个推理可用于变量所有可能的取值，因此该性质对终止于（+mon）和（(mon）的证明都成立。（trans）由读者自己给出，该归纳证明结束。 ( 1.4.3 良基归纳 前面所介绍的归纳都是更一般的基于良基关系的归纳的实例。良基关系在计算机科学中是重要的，在很多地方要用到它，例如它和程序终止的证明方法有联系。 集合A的良基关系（well-founded relation）是A上的一个二元关系(，它具有这样的性质：A上不存在无穷递减序列a0 ( a1 ( a2 ( …（在此定义b ( a当且仅当a( b）。例如，在自然数上，如果j ( i +1，则i ( j，则这个关系是一个良基关系。从这个例子看出，良基关系不一定有传递性。也很容易看出，每个良基关系都是非自反的，即对任何a(A，a ( a不成立。其理由是，如果a ( a，那么存在无穷递减序列a ( a ( a ( …。 一个等价的定义是，A上的二元关系(是良基的，当且仅当A的每个非空子集B有一个极小元。（a(B是极小元，如果不存在a((B使得a(( a。）它的证明在下面的引理中。 引理1.1 如果(是集合A上的二元关系，那么(是良基的当且仅当A的每个非空子集都有一个极小元。 证明 首先，假定(是集合A上的良基关系，令B(A是任意非空子集。用反证法证明B有极小元。如果B无极小元，那么对每个a(B，可以找到某个a((B使得a(( a。这样，可以从任意的a0(B开始，构造一个无穷递减序列a0 ( a1 ( a2 ( …。这就证明了该引理的前一半。 反过来，假定每个子集有一个极小元，那么不可能存在无穷递减序列a0 ( a1 ( a2 ( …，因为这样的序列给出了无极小元的集合{a0, a1, a2, …}，这就完成了整个证明。  命题1.2（良基归纳） 令(是集合A上的一个良基关系，令P是A上的某个性质。若每当所有的P(b) (b ( a)为真则P(a)为真，那么，对所有的a(A，P(a)为真。 证明 假定对每个a(A有，如果所有的P(b) (b ( a)为真则P(a)为真。（用符号表示的话，即假定(a. ((b.( b ( a ( P(b)) ( P(a))。）用反证法来证明对所有的a(A，P(a)为真。 如果存在某个x(A使得( P(x)成立，那么集合 B ( { a(A | ( P(a)} 非空。由引理1.1，B一定有极小元a (B。但是，对所有的b ( a，P(b)一定成立（否则a不是B的极小元），这就和假定(b.( b ( a ( P(b)) ( P(a)矛盾。所以该命题成立。 ( 表1.1列出了本书中与常用归纳形式相联系的良基关系。良基关系的一个重要性质是，良基关系的传递闭包也是良基关系。这对于理解表1.1中两种形式的自然数归纳和两种形式的结构归纳的相似性是有帮助的。在这两种情况下，和第二种归纳形式相联系的良基关系正是和第一种归纳形式相联系的良基关系的传递闭包。（不难看出，表1.1所列的关系都是良基关系。） 表1.1 常用归纳形式的良基关系 归纳形式 良基关系 自然数归纳（形式1） m ( n，如果m +1 ( n 自然数归纳（形式2） m ( n，如果m ( n 结构归纳（形式1） e ( e(，如果e是e(的直接子表达式 结构归纳（形式2） e ( e(，如果e是e(的子表达式 基于证明的归纳 ( ( ((，如果(是证明((的最后一步推导规则的某个前提的证明 下面写出表1.1所说的自然数归纳的两种形式，读者自己不难写出结构归纳的两种形式。 自然数归纳（形式1）：为证明对所有自然数n，P(n)为真，只需证明P(0)以及证明对任何自然数m，如果P(m)为真则P(m +1)必定为真。 自然数归纳（形式2）：为证明对所有自然数n，P(n)为真，只需证明对任何自然数m，如果所有的P(i) (i ( m)为真则P(m)必定为真。 一类十分有用且更加复杂的良基关系是字典序，它们本质上是从基于某个有序集合得出的序列集合上的像字典一样的序。为简单起见，仅考虑自然数序列上的序。 自然数二元组上的一个自然序是 (n, m( ( (n(, m(( iff n < n( 或者 n ( n(且 m < m( 如果仅考虑单数字的数0,…,9，并且把二元组(n, m(看成两位数nm，那么这个序就是数值序。可以把二元组上的这个序加以推广，给长度为3, 4, … 的序列排序。还可以把这个序推广到不同长度的序列上。把自然数写成序列(n1, n2, …, nk(这样的形式，可以定义更一般的序为： (n1, n2, …, nk( ( (m1, m2, …, ml( iff k < l 或者k ( l并且存在一个 i ( k，使得对所有的 j < i有 nj ( mj 并且ni < mi。 习 题 1.1 用(表示自然数乘法，为平方函数写一个(表达式。 1.2 在表达式((y : nat.(z : nat.y+z) 5 3中插入括号，使得它是不省略括号的(表达式。 1.3 在表达式(y : nat.(z : nat.y+z中，把约束变元y重新命名为x不会改变该表达式定义的函数。为什么把y重新命名为z会改变此表达式的含义？可以把(y : nat.y+z中的y重新命名为z吗？ 1.4 使用(()red两次，把(表达式((f : nat ( nat.f 10) ((x : nat.x+x)化简到两个自然数的和。 1.5如果把树看成是由下面的文法产生的： t ::= nil | leaf | node(t, t) 使用树上的结构归纳来证明，一棵二叉树的大小最多是2h-1个结点，其中h是树的高度。 1.6 字母表(上的串s是(的元素的有穷序列。在这个习题中使用大写英文字母作为字母表，因此任何串s可以写成s ( a1a2…ak，其中每个ai是26个大写字母中的一个。一种特别的情况是空串，写成(。下面在串上定义了三个关系，两个是良基的，另一个不是。对于良基关系，简单解释它为什么是良基的；对于那个非良基关系，举出一个无穷的递减序列。 (a) 关系(1是串上的字典序，它由下面两个公理刻画： ( (1 s iff s ( ( a1s (1 a2 t iff 在字母表中a1在a2的前面或者( a1 ( a2且s (1 t( (b) 第二个关系由串的长度定义： a1…ak (2 b1…bl iff k( l (c) 第三个关系(3组合前面两个关系，由(2来定义不同长度的串的关系，而由(1来定义相同长度的串的关系。 a1…ak (3 b1…bl iff k( l或者( k ( l且a1…ak (1 b1…bl ( � EMBED Equation.3 ��� A1 - - - A2 B 图1.1 证明树示意图 1 1 _1061314684.unknown _1061314803.unknown _1061314947.unknown _1061314753.unknown _1061228352.unknown _1061314395.unknown _961609770.unknown