软件形式化方法第2章 数学基础

第2章数学基础2.1命题和谓词演算

2.2集合和关系2.3函数2.4语法2.5结构归纳2.6

演算2.7论域理论基础注：本章部分内容具有复习性质2.1命题和谓词演算命名约定和注释定义和相等关系表达式中的辅助名字命题演算谓词演算命题逻辑的回顾合适公式的归纳定义

::=p|(

)|(

)|(

)|(

)推理规则（包括公理）

(i)

(e1) (e2)语法推论若从

1,2,…,n

可以证明

，表示成

1,2,…,n

|-

, 简写成|-

逻辑等价

|-

并且

|-

命题逻辑的回顾命题逻辑的语义定义真值集合（给p,q指派真值）把各逻辑连接词映射到真值集合上的运算（真值表方式）各推理规则在该模型中成立语义推论

若

1,2,…,n的值都为真,则

值也为真,写成

1,2,…,n

|=

, 简写成|=

语义等价

|=

并且

|=

可满足性

是可满足的，若存在一种指派使

的值为真命题逻辑的回顾命题逻辑是可靠的和完备的命题逻辑的可靠性

若

|-

是有效的（可证明的），则

|=

成立命题逻辑的完备性

若

|=

成立，则

|-

是有效的命题逻辑的可靠性和完备性

|-

有效，当且仅当

|=

成立谓词逻辑的回顾合式公式谓词符号集合

、函数符号集合

（包括常量符号）基于

定义项集

t::=x|c|f(t,…,t)归纳地定义基于（

,

）的合适公式

::=P(t1,t2,…,tn)|(

)|(

)|(

)|(

)|(x

)

|(x

) (P

)自由变量、约束变量、代换谓词逻辑的回顾新增推理规则（包括公理）项相等的证明规则全称量词证明规则存在量词证明规则量词间的等价规则语义模型、可靠性、完备性它们都可以基于命题逻辑相应概念进行拓展

|-

和

|=

的含义与前面的一致

|=

表示

在模型

中成立2.2集合和关系基本集合定义集合集合上的运算序列、元组和笛卡儿积关系的定义关系的论域和值域关系的逆和像集合集合的概念

构造性数学方法的基础。集合就是一组无重复的对象的全体。集合中的对象称为集合元素。集合的描述方法通常用大写字母表示集合，用小写字母表示元素描述集合的三种方法枚举法：列出所有元素的表示方法。如1至5的整数集合可表示为：

1，2，3，4，5

；外延表示法：当集合中所列元素的一般形式很明显时，可只列出部分元素，其他则用省略号表示。如斐波那契数列可表示为：{0，1，1，2，3，5，8，13，21，34，…}；谓词表示法：用谓词来概括集合中元素的属性。如斐波那契数列可表示为：{Fn|Fn+2=Fn+1+Fn，F0=0，F1=1，n≥0}

集合的运算

集合的并

设A、B为两个任意集合，所有属于A或属于B的元素构成的集合C，称为A和B的并集。可表示为：C＝A∪B＝｛x｜x∈A∨x∈B｝。求并集的运算称为并（运算）。例:若A={a，b，c，d}，B={b，d，e}，求集合A和B的并。解：A∪B＝｛a，b，c，d，e｝集合的运算集合的差设A、B为两个任意集合，所有属于A而不属于B的一切元素构成的集合S，称为A和B的差集。可表示为：S=A－B=｛x｜x∈A∨x∈B｝。求差集的运算称为差（运算）。例:若A={a，b，c，d}，B={b，d，e}，求集合A和B的差。解：A－B={a，c}集合的运算交集的交设A、B为两个任意集合，由和的所有相同元素构成的集合C，称为A和B的交集。可表示为：C＝A∩B＝｛x｜x∈A∧x∈B｝。求交集的运算称为交（运算）。例5.3若A={x|x>-5}，B={x|x<1}，求集合和B的交。解：A∩B＝｛x｜x>﹣5｝∩｛x｜x<1｝＝｛x｜–5<x<1｝集合的运算集合的补设I为全集，A为I的任意一子集，I–A则为A的补集，记为。可表示为

I–A=｛x｜x∈I，｝求补集的运算称为补（运算）求补集的运算称为补（运算）

例5.4若I=｛x｜–5﹤x﹤5｝，A=｛x｜0﹤x﹤1｝，求。解：=I–A=｛x｜–5﹤x﹤0∨1﹤x﹤5｝集合的运算集合的乘积集合A1，A2，…，An的乘积一般用法国数学家笛卡尔（ReneDescartes）的名字命名，即笛卡尔积。该乘积表示如下：A1×A2×…An={（a1，a2，…，an）｜ai∈Ai，i＝1，…，n}A1×A2×…An的结果是一个有序元组的集合。例5.5若A={1，2，3}，B={a，b}，求A×B。解：A×B={（1，a），（1，b），（2，a），（2，b），（3，a），（3，b）}关系关系是一个谓词，其定义域为k元组的集合。通常的关系为二元关系，其定义域为有序对的集合，在这个集合中，我们说有序对的第一个元素和第二个元素有关系。如学生选课：

学生

课程

成绩

张三

文学90

张三

哲学95

李四

数学80

李四

艺术85

王五

历史92

王五

文学88等价关系在关系中，有一种特殊的关系，即等价关系，它满足以下3个条件：自反性，即对集合中的每一个元素a，都有aRa；对称性，即对集合中的任意元素a，b，aRb成立当且仅当bRa成立；传递性，即对集合中的任意元素a，b，c，若aRb和bRc成立，则aRc一定成立。等价关系的一个重要性质是：集合A上的一个等价关系R可将A划分为若干个互不相交的子集，称为等价类。2.3函数函数的定义有限函数由表达式定义函数函数的交覆盖并限制合成中缀算符作为函数谓词和商运算逆和像泛函分派和平行作用curry函数函数又称映射，是指把输入转变成输出的运算，该运算也可理解为从某一“定义域”的对象到某一“值域”的对象的映射。函数是程序设计的基础，程序定义了计算函数的算法，而定义函数的方法又影响着程序语言的设计，好的程序设计语言一般都便于函数的计算。设f为一个函数，当输入值为a时输出值为b，则记作：函数的定义一般来说，给出X

Y的一个关系r和一个对象x∈X，存在零个、一个或多个对象y∈Y，使得二元组<x，y>从属于r（甚至可能有无限多个这样的y）如果对每个x，最多只有一个这样的y，那么就把这样的关系叫做函数。关系finrel不是函数，但关系pm_double是函数。函数的定义X和Y间的函数关系的集合记为：

X→Y这个集合是X←→Y的一个子集，可以精确地定义为：

X→Y{r：X

Y|

x：X·givenimage_of_xr(·{x}·)thenfiniteimage_of_x

(cardimage_of_x≤1) end}函数的定义对于函数f：X→Y，如果domf＝X，我们说f是个全函数从X到Y的全函数的集合用

X→tY表示注意，本书中函数和全函数的定义分别对应到一些书上部分函数和函数的定义有限函数如果函数的论域有限，则把它们叫做有限函数，从X到Y的有限函数集合记为：定义为：

{f：X→Y|finite(domf)}定义有限函数的一种方式是列出对论域的每个变元所取的值这类似于由外延定义有限集合

由表达式定义函数对于集合，还可由概括定义，即由特征性质而不是由枚举来定义对于函数，等价的机制是，由形式变元上的表达式定义一个函数，对任何实在变元的值，由这个值代替形式变元可得到相应的函数值例子：函数的基调f：--对一个函数f：--对一个全函数注意不要把f：和S

相混淆前者给出f的基调，声明f是从X到Y的一个函数，而后者是把S定义为从X到Y的所有函数的集合函数的交前面把函数定义为特殊的关系，而关系是一类特殊的集合这使得有可能定义两个函数的交为一个函数，即同时属于两个函数的<变元，结果>二元组的集合两个函数的交定义如下：令f，g：，令h

，那么：

domh={x:domfdomg|f(x)=g(x)};对xdomh，h(x)=f(x)=g(x)函数的覆盖并

两个函数的并可能不是一个函数关系这种现象发生在两个函数的论域相交，并且它们中至少在一个变元上不一致的情况下例如，对于3.2节的f1和f2，它们对c的值有冲突，因此,不是一个函数（b的两个函数值不会引起问题，因为它们一样）

限制函数f到其源集的子集A的限制记为f\A，定义如下：令f：和A：P(X)，那么hf\A是一个函数h：

，使得：

domh=Adomf并且对adom

h，h(a)=f(a)换句话说，f\A和f是一样的函数，但是它的源集被限制到A函数的合成函数上的另一种运算是合成，它可以推广到关系上中缀算符作为函数在处理函数时，还有一种约定将是有用的在普通的数学和程序设计语言中，许多二元函数使用中缀记号，也就是说，一个算符放在两个变元的中间而不是它们的前面

谓词和商运算特征函数

函数的逆和像函数是特殊的关系，因此逆和像算符也可以定义在函数上泛函如上面合成的算符所示，泛函，也叫做高阶函数，是允许函数作为变元或结果（或同时作为变元或结果）的函数。术语“泛函”在本书中之用于高阶全函数。在指称语义中，泛函起着重要的作用，因此，必须熟悉泛函的使用分派分派是基调为：的泛函对于任意函数f：U—>X和g：U－>Y，f&g是函数：换句话说，f&g通过f把变元u到分派给X，同时通过g把u分派给Y。

平行作用平行作用是基调为：的泛函对任意函数f：U—>X和g：V—>Y，f＃g是函数:换句话说，f＃g平行地把f和g分别作用于出自U的一个变元和出自V的一个变元，产生X×Y的一个二元组。

curry另一个重要的泛函是curry（以数学家H.B.Curry命名）。这个泛函把任意的两个变元的函数翻译成一个变元的函数，后者的结果也是一个变元的函数。curry本身的基调是：

curry对于全函数，curry定义如下：对于任意的集合X、Y和Z，如果f是基调为：全函数。那么curry（f）是基调为:的函数g，使得对于任意x：X和y：Y，有：g（x）（y）＝f（x，y）

2.4语法具体语法抽象语法基于抽象语法的语义定义抽象语法的数学基础具体语法说明语言语法的习惯方法是用Backus-Naur形式（BNF）,使用BNF，可用文法描述语言的语法文法由一组产生式组成，每个产生式描述了某类程序结构的形式，如表达式、命令、例程等等例如，下面的产生式用标准的BNF表示法定义了某个语言中条件命令的语法：<conditional>::=if<boolen_expression>then<command>else<command>end具体语法BNF和它的各种衍变（尤其是NiklausWirth为定义Pascal语言而引入的图形表示）提供了广为接受的语法描述机制然而，它们不是更深入地研究语言的最好基础BNF产生式包括了许多无关紧要的细节，如关键字和其他的外部语法约定BNF规范实际描述的是程序员看见的程序的外部形式，而不是程序的结构抽象语法为了描述程序的内部结构而不是它们的外部形式，使用抽象语法比较合理抽象语法直接给出各种语言构造的各个成分，而无关其表示细节例如，条件命令的抽象语法描述将直截了当地说明条件命令有三个成分：两个命令和一个布尔表达式条件命令的其他东西称为“语法作料”，它们只影响人们读写程序Meta抽象文法Meta抽象文法由以下两部分组成：构造名的有限集合，为了方便起见，构造名用大写字母开头，如Command和Variable产生式的有限集合，每个产生式和一个构造对应Meta抽象文法由文法定义的语言是该文法的顶层构造（在下面定义）的所有实例的集合产生式的形式：

Tright_hand_side

聚集产生式一个聚集产生式定义一个构造，它的实例有固定数目的带标志成分例如，可以通过下面的Meta聚集产生式定义表示条件命令的抽象构造：

Conditional

thenbranch：Command；

elsebranch：Command；

test：Boolean_expression不同成分的次序是无关紧要的，这是抽象语法和具体语法的一个区别聚集产生式一个构造的定义可能仅根据一个其它的构造，这种情况将被看成聚集产生式的特殊情况，如：

Variable

name:Identifier聚集构造定义类似于语言中记录类型的定义，即都是根据成分来描述它们选择产生式选择产生式通过一组选择定义一个构造，在一种语言中，各种可能的命令可以由产生式，来定义，例如，Command的实例是右部给出的某个构造的一个实例：

CommandΔSkip|Assignment|Compound|Loop表产生式

一个构造可以定义为另一个构造的实例序列的集合，序列长度大于或等于零，表产生式对应这种情况例如，Pascal中的复合语句可以有下面的产生式定义：

Compound

Command*Compound的实例是零个、一个或多个命令的序列如果一个构造的实例是至少有一个元素的表，那么星号由加号代替例如：

NumberΔDigit＋预定义的构造

如果文法定义的是实际语言，那么它的所有构造最终需要由最基本的且意义明确的集合（即终结构造）来定义在Meta中用的四个预定义的终结构造，对应到标准的数学集合：非负整数集：N整数集：Z布尔值集：B字符串集：S一个完整的抽象文法

下面是一个小的但有代表性的语言的抽象文法，它的结构类似于流行语言Pascal，Ada和C等的公共核心，该语言起名为KernelKernel的顶层构造是Program

这个文法是递归定义的例如，Command的一种选择是Conditional；后者是一个聚集，有两个Command成分这样的循环定义是否有意义？定义符号“Δ”在这里的使用是否正确？这些问题在后面回答Kernel的抽象文法

ProgramΔdecpart:Declaration_list;body:CommandDeclaration_listΔDeclaration*DeclarationΔv:Variable;t:TypeTypeΔBoolean_type|Integer_typeCommandΔSkip|Assignment|Compound|Conditional|LoopAssignmentΔtarget:Variable；source:expressionCompoundΔCommand*ConditionalΔthenbranch，elsebranch:Command；

test:ExpressionKernel的抽象文法

LoopΔbody:Command；test:ExpressionExpressionΔConstant|Variable|BinaryConstantΔInteger_constant|Boolean_constantBinaryΔterm1，term2:Expression；op:OperatorOperatorΔBoolean_op|Relationa_op|Arithmetic_opBoolean_opΔNot|And|OrRelational_opΔLt|Le|Eq|Ne|Ge|GtArithmetic_opΔPlus|Minus|Times|DivBoolean_constantΔvalue:BInteger_constantΔValue:ZVariableΔid:S抽象语法表达式我们需要一种方式描述和操作遵守某抽象文法的程序，为此，Meta提供了抽象语法表达式。各种抽象语法表达式对应到各类抽象语法产生式。

聚集构造实例的表达式选择构造实例的表达式表构造实例的表达式终结类型的表达式复杂语法的表达式

聚集构造实例的表达式我们需要一种方式描述和操作遵守某抽象文法的程序。为此，Meta提供了抽象语法表达式。各种抽象语法表达式对应到各类抽象语法产生式、先从聚集构造开始。考虑一个聚集产生时，例如，Kernel文法的第一个产生式

ProgramΔdecpart:Declaration_list;body:Command它描述了一类对象——程序，每个程序有两个成分：声明表和命令。假定声明dl和命令cmd给定，那么我们可以定义一个以dl和cmd为成分的程序p；

pΔProgram(decpart：dl;body：cmd)聚集构造实例的表达式更一般地，当要处理由聚集产生式定义的构造时，可以通过含构造名（这里是Program）和后随的扩号中成分表的表达式来描述这种构造的实例。必须在每个成分前放上相应的标志（这里是decpart和body），用冒号把各成分和它们的标志隔开，并用分号把各成分隔开。例如，语法类型Program的p。在Meta中，这样的对象的成分通过点记号作为它们的标志标识。这是借助于语言中引用记录的域的方式。例如，p的成分可以记为p.decpart和p.body。这些成分分别属Declaration_list类型和Command类型。对于p，相应的对象是dl和cmd。选择构造实例的表达式考虑选择产生式，例如：

CommandΔSkip|Assignment|Compound|Conditional|Loop为了构造Command的一个实例，首先必须有Skip或Assignment等的实例b，然后必须把b提升到Command状态。b提升后的版本记为Command(b)。例如，假定v是变量，e式表达式，那么下面的表达式描述一个命令：

Command(Assignment(target；v;source；e))在最外层栝号里面的表达式定义了Assignment的一个实例，其目标变量是v，源表达式是e。整个表达式代表同样的赋值命令，但是看成Command的实例。选择构造实例的表达式现在考虑选择构造的实例(如类型Command的i)，几乎所有定义在这样的对象上的表达式都依赖于这个对象的“子类型”，在Command的情况下，也就是依据它是Skip、Assignment还是其它情况。分情形表达式在Meta中用于区分子类型。在Meta的变量i上的分情形表达式有这样的形式：

caseiof

Skip->skip_expAssignment->assign_exp|Compound->comp_exp|Conditional->cond_exp|Loop->Loop_exp

end

选择构造实例的表达式右部表达式(skip_exp，assign_exp等）可以叫做“分支表达式”，这种分支表达式通常引用分情形变量I例如，assign_exp可以引用i.target和i.source。为了使这样的记号有意义，必须把assign_exp中出现的i看成是Assignment类型而不是Command类型表构造实例的表达式考虑表产生式，例如：

CompoundΔCommand*构造复合命令Compound的实例的最明显方式是列出若干数目的基构造Command的对象如选择构造的实例那样，最终对象的类型由Compound显式地说明用这种方式说明的对象可以是空，记为Compound(<>)终结类型的表达式因为终结构造没有进一步的描述，构造名将代表这种构造的实例而不加以进一步说明例如，Kernel的Skip命令就记为Skip复杂的语法表达式反复使用上面的机制，可以构造出各种表达式，它们表示抽象的语法结构对于复杂表达式，使用辅助表达式可以使它们更清楚例:见讲义P22-23从上面的例子可以看出，对于复杂表达式，抽象语法记号显得有些笨拙。注意：抽象语法是对程序进行推理的形式工具，而不是程序的可读性的表示方法。对于后者，很显然，标准的具体语法是恰当的选择。下面介绍抽象语法的两个重要应用。

结构编辑器

结构编辑器是一种软件工具，也叫做语法制导编辑器。结构编辑器是构造和处理如程序、程序设计或形式规范这样的结构文档的系统。和标准的正文编辑器（它把任何正文堪称是无结构的字符序列）不同，结构编辑器知道被处理的文档的结构。例如，Pascal的结构编辑器知道Pascal的语法，因而能维持程序的语法合法性。结构编辑器

对用户来说，结构编辑器免除了许多和语法有关的琐碎事务。例如，Pascal编辑器可以为用户输入的begin配上end。结构编辑器便于自动的程序处理和系统的变换，可用于软件工程环境。所有这样的工具依靠基于抽象语法的语言描述，用于表示程序的内部数据结构是对应的抽象语法树。语言和系统的设计

软件的设计者经常需要设计语言，以便用户和他们的系统通讯。在这个活动中的一个典型错误是过早地把注意力集中到交互的具体形式上，其结果是模糊了问题的焦点，过早地处理细节问题。语言和系统的设计

许多系统实际上需要三个接口，以不同的形式提供相同的功能，此时，这样的错误危害更大，这三种接口是：(1)批命令接口，它使系统通过封装的命令序列成为可用；(2)交互接口，用户在终端给出命令并立即见到结果；(3)例程接口，通常通过例程库，使得其它程序可用系统的功能。语言和系统的设计

这三种接口虽然在功能上等价，但使用的“语言”在外部形式上区别相当大。抽象语法提供了一种便利的形式，使我们能先集中注意力于重要的方面，而推迟具体细节的设计。静态语义和动态语义静态语义是对不能由语法描述妥善地刻画的程序结构约束的描述。动态语义是对程序执行效果的描述。静态语义覆盖了形式体系和实际语言结构描述需要间的间隙。当我们无法用抽象语法产生式表达一个结构性质时，可以将其作为静态语义来处理。为什么需要静态语义在Kernel文法中，Conditional和Loop的产生式使语言描述的公共问题显得突出。和普通的语言一样，Kernel中的一个循环或条件的test分支必须是布尔表达式。可能已注意到，对应的产生式中只把test申明为Expression，并且Expression的产生式包括了整数表达式和布尔表达式。这意味着值为整数的test作为循环的成分是遵守该文法的，虽然它明显不该被接受。为什么需要静态语义可由修改此文法来纠正这个缺陷：用两个不同的构造Boolean_expression和Integer_expression来代替Expression，在条件和循环命令的产生式中，让Boolean_expression作为test的构造，但是这种修改将使得文法大大地膨胀，很多Boolean_expression的产生式将简单地重复Integer_expression的产生式。另一种方法是，仍保持简单的文法，但是用非语法的机制来覆盖类型规则和其它的约束。为什么需要静态语义对于test表达式的类型规则，把约束分离出来是为了方便和简单，原则上他们可以表达为该文法的一部分，但是，有些约束不能用纯语法的记号来描述。例如：在Kernel中，变量不允许在一个程序中声明两次，这是一个不能用Meta抽象语法记号或BNF这样的纯语法形式体系表示的条件。任何实际的语言规范都包含这类约束，他们构成了语言的静态语义。基于抽象语法的语义定义

抽象语法可以用作定义静态语义和动态语义函数的基础。使用抽象语法的主要优点是可以把语义嫁接到语法躯干上，这个语法躯干已剪去了只反映程序外部形式的细节。语义函数的源集是构造，也叫做语法论域。它们的目标集合叫做语义论域，其实例指称可能的“含义”。例：见讲义P25抽象语法的数学基础

前面的抽象语法用非形式的定义引入了构造和抽象语法表达式等概念及相应的Meta表示法下面讨论它们的数学含义对于三类产生式的每一种，我们不仅应为对应的产生式的右部提供数学模型，而且应为定义在相应构造的实例上的运算提供适当的解释模型基于初等集合论，它们把每种构造解释为一个集合，它的成员是该构造的实例，每种在实例上的运算看成是在对应集合成员上的运算基于抽象语法的语义定义

聚集可以表示为“带标记的笛卡儿积”。这种集合对处理元组是方便的，因为元组的每个成分都被命名，增强了可读性。例：见讲义P20基于抽象语法的语义定义

选择可以表示为“不相交的并

”，使得结果集合的每个成员能指示它自己源于哪个集合。

例：见讲义P20基于抽象语法的语义定义

表可以采用“递归定义”例：见讲义P22复杂的语法表达式

反复使用上面的机制，可以构造出各种表达式来表示抽象的语法结构。对于复杂的表达式，使用辅助表达式可以使它们更清楚。例：见讲义P22从上面的例子可以看出，对于复杂的表达式，抽象语法记号显得有些笨拙。抽象语法是对程序进行推理的形式工具，而不是程序的可读性的表示方法。对于后者，很显然，标准的具体语法是恰当的选择。2.5结构归纳

用于定义复杂对象的集合和证明这样的对象的性质，叫做结构归纳对定义语言的结构并证明其性质特别有用Lisp的S表达式（作为该语言的数据和程序结构的基础）提供了由结构归纳到对象的典型例子结构归纳：例子

由结构归纳定义S表达式如下：原子是S表达式；如果s1和s2是S表达式，那么(s1.s2)是S表达式。例如：(atom1.atom2)和((atom1.atom2).(atom3.(atom4.atom5)))都是S表达式结构归纳定义的一般形式

更一般地，一个结构归纳定义定义一个集合S，其成员属于下面两种情况之一：

(1)一个或多个预定义的集合的成员（如上面的原子集合）；

(2)由S先前的成员，经一种或多种明确定义的机制推导出来（如上面带括号和点的形式）。这样的定义有清楚的数学解释，定义的这个集合S是一个无限集合族的并

S≜其中的Si由普通的归纳定义。S0是所有从(1)中得到的对象的集合；每个Si+1由所有如下的对象构成：它们由Sj(0≤j≤i)的成员经(2)导出结构归纳定义的一般形式

例如，在S表达式中，S0是原子的集合；S1是形式为(a.b)的对象的集合，其中a和b是原子，S2也是形式为(a.b)的对象的集合，但是其中a和b在原子集中或者在S1中；等等某些对象可能出现在不同的Si中（事实上，在S表达式的例子中，每个Si是Si+1的子集），这不会引起问题。因为S定义为所有Si的并，因而S的成员来自哪个Si是无关紧要的。按这种观点，结构归纳是通常的自然数归纳的直截了当的应用，归纳定义的是集合Si的序列。结构归纳证明

由结构归纳定义的集合有助于按同样的方式组织证明。为了用结构归纳证明S的所有成员满足某个性质p，可以按下面两步进行：

(1)（基本步）基集的所有成员满足p；

(2)（归纳步）如果一组来自可能不同的Sj(0≤j≤i)的对象满足p，那么用任何定义Si+1的构造机制由它们得到的对象满足p。结构归纳证明

这种归纳技术的有效性可以从普通的自然数归纳证明的有效性得出：“一个结构归纳证明直截了当地相当于用自然数归纳法证明性质：p(i；N)p(i；N)≜“Si的所有成员满足某个性质p”结构归纳证明：例

用结构归纳证明每个S表达式有相等个数的开括号和闭括号。这个证明包含两部分：

(1)原子没有括号，因此满足这个性质；

(2)考虑两个S表达式e1和e2，它们都满足该性质。令p1和p2分别是它们的开括号数。由假设，它们的闭括号数也分别是p1和p2。从e1和e2，构造机制只能产生一个新的S表达式n≜(e1.e2)。n的开括号和闭括号数都是p1+p2+1。结构归纳定义是递归的简单情况。自然数归纳形式1：为证明对所有自然数n，P(n)为真，只需证明P(0)以及证明对任何自然数m,如果P(m)为真则P(m+1)必定为真。形式2：为证明对所有自然数n，P(n)为真，只需证明对任何自然数m，如果所有的P(i)(im)为真则P(m)必定为真字典序（以自然数序列为例）

n1,n2,

…,nk

m1,m2,

…,mliffk<l或者k

l并且存在一个

i

k，使得对所有的

j<i有

nj

mj

并且ni

<mi

表达式上的归纳(2015-5-13)表达式文法

e::=0|1|v|e+e|e

e表达式都有一棵分析树如果P是表达式的性质，Q是自然数的性质Q(n)

=def

树t.如果height(t)=n并且t是e的分析树，那么P(e)为真首先必须为高度是0的分析树直接证明P然后，对于高度至少为1的树，假定对于分析树的高度较小的表达式，P都成立结构归纳形式1对每个原子表达式e，证明P(e)对直接子表达式为e1,…,ek的任何复合表达式e，证明，如果P(ei)（i=1,…,k）都为真，那么P(e)也为真。

形式2证明:对任何表达式e，如果P(e)对e的任何子表达式e

都成立，那么P(e)也成立。形式2的归纳假设包含了所有的子表达式，并非只是直接子表达式证明上的归纳证明系统由公理和推理规则组成证明是一个公式序列，该序列中的每个公式都是公理或者是由前面的公理通过一个推理规则得到的结论基于证明的长度，用自然数归纳法来讨论证明的性质另一种观点把证明看成是某种形式的树

证明上的归纳BA2---A1证明树示意图证明上的结构归纳对该证明系统中的每个公理，证明P成立假定对证明

1,…,

k，P成立，证明P(

)也为真。

是这样的证明，它结束于用一个推理规则，并且是从证明

1,…,

k延伸出来的一个证明良基归纳定义：集合A的良基关系是A上的一个二元关系

，它具有这样的性质：A上不存在无穷递减序列a0

a1

a2

…例：在自然数上定义，如果j

i+1，则i

j，则这个关系是一个良基关系良基关系的一些特点良基关系不一定有传递性良基关系都是非自反的，即对任何a

A，a

a不成立；否则会出现无穷递减序列a

a

a

…良基归纳引理1:如果

是集合A上的二元关系，那么

是良基的，当且仅当A的每个非空子集都有一个极小元证明:令B

A是任意非空子集，用反证法证明B有极小元如果B无极小元，那么对每个a

B，可以找到某个a

B使得a

a。这样，可以从任意的a0

B开始，构造一个无穷递减序列a0

a1

a2

…反过来，假定每个子集有一个极小元，那么不可能存在a0

a1

a2

…，因为该序列给出了无极小元的集合{a0,a1,a2,…}

良基归纳命题（良基归纳）：令

是集合A上的一个良基关系，令P是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，B一定有极小元a

B

但是，对所有的b

a，P(b)一定成立（否则a不是B的极小元），这和假定

b.(b

a

P(b))P(a)矛盾归纳法总结表1.1常用归纳形式的良基关系归纳形式良基关系自然数归纳（形式1）m

n，如果m+1

n自然数归纳（形式2）m

n，如果m

n结构归纳（形式1）e

e

，如果e是e

的直接子表达式结构归纳（形式2）e

e

，如果e是e

的子表达式基于证明的归纳

，如果

是证明

的最后一步推导规则的某个前提的证明2.6

演算

演算是1941年Church定义的形式系统，可以作为一个可计算性模型的精确定义；可以看作是一个简单的、语义清楚的形式语言；具有简单而又有强大的描述能力，与Turing机等价，描述能力相同；可以描述任何一个部分递归函数的计算过程；适合用来描述程序设计语言的语义；是函数型程序设计语言及指称语义的理论基础；LISP语言就是基于

演算(JohnMcCarthy)

演算组成Lambda演算通常包括两个部分：合法表达式(表达式)的形式系统(语法)变换规则的形式系统(语义)

表达式：定义

表达式由变量名、抽象符号，.以及括号等符号构成，其语法为：

<表达式>::=<变量名> |<表达式><表达式>|<变量名>.<表达式>|(<表达式>)没有类型；没有常量；变量名不仅可以代表变量，还可以代表函数；

表达式：施用型和抽象型施用型表达式(APPLY):E1E2

：函数调用，E1是函数定义，E2是实参抽象型表达式(Abstraction):x.E：定义无名函数，x对应形参,E是函数体

举例：xx;x.xy;x(y.xy);x.y.x；

表达式：施用型和抽象型抽象表达式

x.E用来表示无名函数通常，定义函数的方法是首先定义函数名，然后再使用它，因此函数都有名，而抽象表达式则表示一无名函数假设有函数定义：funcf(x)=x+1则定义了这样一个函数，既函数名是f，自变量（形参）是x，函数值是x+1的值当然也可用别的方式定义出上述函数，例如

funcf=x.x+1这种表示法也能方便地表示哪个是函数名，哪个是自变量名，哪部分是函数体，其中表示其后的变量为自变量

表达式：施用型和抽象型假设有f(a*b)，则它应等价于(x.x+1)(a*b)，而其中(x.x+1)和(a*b)都是表达式，这样在Lambda表达式的定义中出现了E1E2形式的表达式从语义角度来说其中的E1必须是函数，而E1E2的含义是把函数E1作用于表达式E2称x.E中的E表达式为函数x.E的体部分，而称x为该函数的自变量

表达式：记法约定施用型表达式的左结合规则：

E1E2E3

…En=(((E1E2)E3)…)En抽象型表达式的右结合规则：

x1.x2.…xn.E=x1.(x2.(…(xn.E)…))x1x2…xn.E=x1.x2.…xn.Ex1.x2.…xn.E1E2E3…En

=x1.x2.…xn.(E1E2E3…En)

表达式：语义单从Lambda表达式的结构本身看不出任何意义，因为其中既没有常量，也没有函数名，无法知道如何进行计算究竟如何计算表达式值，将由Lambda变换部分来决定如果说Lambda表达式相当于程序，则Lambda变换部分就相当于程序的解释系统

表达式：子表达式子表达式（针对不同的表达式形式）设E是一个表达式，则E的子表达式定义为：Ex，x就是E的子表达式；EE1E2，E1和E2以及它们的子表达式都是E的子表达式；Ex.E’，x.E’以及E’的子表达式都是E的子表达式；E(E’)，E’及其子表达式都是E的子表达式；用SUB(E)表示E的子表达式集；

表达式：作用域

表达式中变量的作用域：

x.E表达式中的变量x是被绑定的，它的作用域是体表达式E中去掉所有形如x.E’子表达式后的表达式部分；

x.E表达式中x.部分可以看作是变量x的定义点，在E中x的定义域中出现变量x为其使用点；举例：表达式：y(xy.y(x.xy))(z(x.xx))x的作用域是

y；y的作用域是

y(x.xy)；x的作用域是

xy；x的作用域是

xx；

表达式：自由出现在表达式中相同的变量名，可以出现在表达式的不同位置，它们的含义可能不同；自由出现/约束出现：表达式E中变量名x的一次出现称为自由出现，如果E中没有任何一个形如x.E’的子表达式包含该出现；如果存在一个x.E’的子表达式包含该出现，称为约束出现；y(xy.y(x.xy))(z(x.xx))

自由约束约束自由约束出现出现出现出现出现

表达式：自由变量自由变量：称x为表达式E的自由变量，如果E中至少包含一个x的自由出现；需要区分的概念：变量：<变量名，含义>，定义点确定变量名：标识符变量的出现：<变量名，位置>自由变量集合：用FV(E)表示E的自由变量集合，则其具体定义为：Ex，FV(x)={x}；EE1E2

，FV(E1E2)=FV(E1)FV(E2)；Ex.E’，FV(x.E’)=FV(E’)–{x}；E(E’)，FV((E’))=FV(E’)

计算自由变量集合例子表达式E=y(xy.y(x.xy))(z(x.xx))FV(E)=FV(y(xy.y(x.xy)))FV((z(x.xx)))

=FV(y)FV((xy.y(x.xy)))

FV(z)FV((x.xx))={y}

(

FV(y(x.xy))-{x,y}){z}(FV(xx)-{x})={y,z}

表达式：闭型表达式和开型表达式闭型表达式：如果一个表达式E不包含自由变量，即FV(E)=

,则称E为闭型表达式；开型表达式：如果一个表达式E包含自由变量，即FV(E)

,则称E为开型表达式；

表达式：替换替换(Substitution)：设E和E0是表达式，x是变量名，

替换E[E0/x]是表示把E中的所有x的自由出现替换成E0。代换的表示形式有多种：[E0/x]E；[E0/x，E]；[x

E0，E]E[E0/x]的计算规则为：S1:Ex，x[E0/x]=E0

；S2:Ey，y[E0/x]=y

，x

y

；S3:E(E’)，(E’)[

E0/x]=(E’[

E0/x])S4:EE1E2，E1E2[E0/x]=(E1[E0/x])(E2[E0/x])；S5:Ex.E’，x.E’[

E0/x]=x.E’

；

表达式：替换S6:Ey.E’，x

y如果E0中没有y的自由出现，那么直接对E’进行替换即，如果yFV(E0)，则

s6-1:(y.E’)[

E0/x]=y.(E’

[

E0/x])注：（y.E’）中的y和E0中的y是不同的；如果E’中没有x的自由出现，则表示E’没有可替换即如果xFV(E’)，则

s6-2:(y.E’)[

E0/x]=y.(E’[

E0/x])=y.E’

表达式：替换S6:Ey.E’，x

y，如果E0中有y的自由出现，E’中有可替换的x,则需要对y进行改名，改变后的变量名z是不同于y的E0的非自由出现。即如果yFV(E0)xFV(E’)，则

s6-3:(y.E’)[

E0/x]=z.((E’

z/y])[E0/x])，

zFV(E0)，zy基本规则：只有自由出现的变量才允许被替换，而且替换不应该把变量的自由出现变为约束出现。要避免出现(y.x+y)[y/x]=(y.y+y)，正确的替换，自动改名：(y.x+y)[y/x]=z.y+z

表达式：替换例子x[xy/x]=xyS1y[M/x]=yS2x.xy[E/x]=x.xyS3;S5x.xz[w/y]=x.xzS6-2

表达式：替换例子((x.xyb.xy[a.ab/y]=x.xy[a.ab/y]b.xy[a.ab/y]S4=x.xa.abz.xy[z/b][a.ab/y]S6-1;S6-3=x.xa.abz.xy[a.ab/y]S6-2=x.xa.abz.xa.abS6-1

演算小结

演算的语法–

表达式形式定义一些相关概念子表达式作用域规则自由变量替换：是Lambda演算中最重要的一个概念；后面定义的转换系统都是基于替换的；

演算通常包括两个部分：合法表达式(表达式)的形式系统(语法)语法结构；自由变量；替换变换规则的形式系统(语义)回顾

演算的变换系统变换系统给出了如何从一个表达式转换成和其等价的另外一个表达式；变换系统定义了演算的语义；实际上给出了一种计算规则；不同的演算系统由不同的变换规则确定；变换规则应当是保结构和保值的；

演算的变换系统给了一个表达式即可根据演算系统的变换规则进行一系列的变换，其结果有两种可能:一是不能进一步的归约二是变换无终止地进行下去(相当于程序不终止)不同的Lambda演算系统具有不同的变换规则，有的可能只有两个变换规则，有的可能有三个变换规则，有的甚至可能有更多的变换规则这里介绍最常见的Lambda变换规则

演算的变换系统

--

变换

变换：设E是表达式，x是变量，则称下面变换为α变换（其中y不在FV(x.E)中）

x.Ey.E[y/x]

变换只是改变了x.E型表达式的形参名；

x.x+y、z.z+y、w.w+y在变换下是等价的，它们定义的是同一个函数；条件：新的形参不是体表达式的自由变量，否则会改变函数的含义；

演算的变换系统

--

变换例子合法的变换

X.(ZX)Y.(ZY)

X.((Y.YX)X)Z.((Y.YZ)Z)

非法的变换

X.(Z(Y.X))Y.(Z(Y.Y))

X.(ZY)Y.(ZY)

演算的变换系统--变换

变换：设(x.E)和E0为表达式，则称下面的变换为β变换（称β变换规则的左部表达式为β基）

(x.E)E0E[E0/x]β变换是最重要的变换，所有演算系统都有β变换。β变换规则实际上定义了函数调用的语义。

演算的变换系统

--变换的例子(X.XY)XXY(X.XX)YYY(X.(Y.(Z.XYZ)))ABC(Y.(Z.AYZ))BC (Z.ABZ)C ABC

演算的变换系统

--变换

变换：设x.Mx是一个表达式，且满足条件xFV(M)，则称下面变换为η变换: (x.Mx)M

变换主要依据函数的外延(保值)等价性定义，即如果对于任意x,都有f(x)=h(x)，则认为f和h

等价；对于任意y,xFV(M),(x.Mx)yMyη变换不是演算系统所必需的变换规则

演算的变换系统

--变换的例子合法变换

X.(Y.YY)X(Y.YY)非法变换

X.(Y.YX)X(Y.YX)

不满足条件：XFV((Y.YX))

演算的变换系统

--归约归约基：(1)β变换的左部表达式(x.E)E0称为β基(2)η变换的左部表达式(x.Mx)称为η基(3)β基和η基统称为归约基归约：对表达式中的某一归约基施行某种变换称为归约；一个表达式中可以同时有多个归约基；归约过程不唯一；不同的归约过程得到的结果不一定相同；

演算的变换系统

--归约过程例子举例不同的归约过程得到相同的结果：表达式：(

y.y((a.xa)(

a.a))))(b.b)归约过程1：

(

y.y((a.xa)(

a.a))))(b.b)

(

y.y((x(

a.a)))(b.b)

(

b.b)(x(a.a))

x(a.a)

演算的变换系统

--归约过程例子举例不同的归约过程得到相同的结果：表达式：(

y.y((a.xa)(

a.a))))(b.b)归约过程2：

(

y.y((a.xa)(

a.a))))(b.b)(

b.b)((

a.xa)(

a.a))

(

a.xa)(

a.a)

x(

a.a)

演算的变换系统

--范式范式：设E是一个表达式，且其中没有任何归约基，则称该表达式为范式。如果一个表达式经过有限次变换能归约成范式，则称该表达式有范式举例：

X，XX，X.XX，X(X.XX)是范式

X.X((Y.X)Y)不是范式，因为有归约基((Y.X)Y)

表达式有很多，范式是具有相同解释的最简表示；

演算的变换系统

--归约过程一个表达式中可包含多个归约基，因此，归约过程不一定唯一，而且不同的归约过程也可能得到不同的计算结果，也可能都得到同一个结果。下面是多个归约过程得到同一结果的例子。

x(

a.a)(

b.b)(x(

a.a))(

b.b)(x(

a.a))(

a.xa)(

a.a)(

b.b((

a.xa)(

a.a))(

y.y((

a.xa)(

a.a)))(

b.b)(

y.y((x((

a.a)))(

b.b)

演算的变换系统

--归约过程下面是多个归约过程，并且不同归约过程得到不同结果的例:(x.y)((x.xx)(x.xx))如果先归约(x.xx)(x.xx)，则将无休止地变换下去，但如果先归约(x.y)(....)部分，则归约一次即可得到范式y原因是函数(x.y)并不真正用到实参值，但如果一定要先计算实参，然后再计算函数体的值，就会出现以上问题

演算的变换系统

--归约过程下面是无范式的例子:(1)(x.xx)(x.xx)(x.xx)(x.xx) ...(不终止)(2)(x.xxx)(x.xxx)(x.xxx)(x.xxx)(x.xxx)(x.xxx)...(不终止)

演算的变换系统

--范式的性质定理（Church-Rosser）：如果Ax和Ay成立，则一定存在z使得xz和yz成立。(合流性)证明：(略)定理（范式唯一性）：如果把通过α变换可互换的表达式视为同一表达式，那么如果Lambda表达式E存在范式，则其范式一定唯一证明：设表达式E有两个范式x和y，则根据Church-Rosser定理，一定存在表达式z，使得xz和yz成立。因为x和y是范式，只能xz，yz。而α变换是双向的，因此有xy，也就是说范式x和y是同一种Lambda表达式。

演算的变换系统

--范式的性质定义2.16(标准归约)：如果每次归约最左的归约基，则称这种归约为标准归约。定理2.17：如果表达式E有范式，则按标准归约一定能求到其范式。证明:略

演算的变换系统

--范式的性质表示法：XY:经过有限次变换(α，β，η)，X变换为Y。XrY:经过有限次归约(β，η)，X变换为Y。X

Y:经过有限次α变换，X变换为Y。表达式不一定都有范式范式的唯一性：如果有范式，则在变换下一定唯一范式的存在性：如果有范式，则最左归约法一定能求出范式标准归约：最左归约，按归约基中符号的出现顺序

演算总结需要掌握的知识点表达式自由变量替换三种变换归约范式范式的唯一性范式的存在性

演算作为计算模型Lambda演算系统由Lambda表达式和Lambda变换规则组成Lambda变换的主要作用是用来导出表达式的范式Turing机系统能够描述部分递归函数的计算过程的事实，在可计算理论里已得以证实那么Lambda演算系统有无同样的功能?结论是：能

演算作为计算模型在Turing机系统里有所谓的“带”，它是Turing机的操作对象，操作结果将改变带的内容带由有序“方格”组成，在每个方格里可写所允许的符号带的内容究竟表示什么意思?系统本身并不知道，系统只知道在什么状态下做什么动作系统只提供一种用于演算的形式规则，带的内容究竟表示什么只有用户才知道

演算作为计算模型在

演算系统中，

表达式相当于Turing机中的带，它们扮演着操作对象的角色Lambda表达式的结构非常简单，但它的功能和当代计算机的功能一样强大！！

演算作为计算模型用

演算模拟整数用

演算模拟加法运算

演算的描述能力用

演算模拟整数正整数n的表达式：

n=ab.a(a(……(a(ab))……))n个简写为：

ab.anb0的表达式：0=ab.b1的表达式：1=ab.ab2的表达式：2=ab.a(ab)=ab.a2b

……用

演算模拟加法运算加法的表达式：PLUS=xy.ab.(xa)((ya)b)验证方法：PLUSmn=〉m+nPLUSmn=(xy.ab.(xa)((ya)b))m

n

=〉(y.ab.(m

a)((ya)b))

n

=〉ab.(m

a)((na)b))

=〉

ab.((ab.amb)

a)((na)b))=〉

ab.((b.amb))(((ab.anb)a)b))=〉

ab.((b.amb))(((b.anb))b))=〉

ab.((b.amb))((anb))=〉

ab.(amanb)

=〉

ab.(am+nb)=m+n其他例子乘法布尔值true和false布尔运算AND,OR,NOT减法；比较运算条件函数最小不动点算子见讲义P36-39

演算系统的扩充前面介绍了最基本的

演算系统，同时表明了它能够描述部分递归函数的计算过程。其中实际上只有一种操作，即函数的施用，即β归约。但其中连常数都没有，因此，用起来很不方便，因此需要扩充原来的

演算系统，扩充后即可变成可使用的函数式抽象语言。

演算系统的扩充扩充的方法：扩充表达式常数：布尔常量true和false;整数引进标准函数：add,mul,and,or,equ其他：条件表达式扩充变换系统扩充数据结构:INT,BOOL,REAL……

演算系统的扩充一种扩充的表达式见讲义P40

2.8论域理论基础目的：描述类型的数学模型；论域理论主要应用于函数式语言中的类型定义，并应用于指称语义学主要内容基本概念：半序集合；完全半序集；平坦集Scott论域及其构造问题的提出递归定义的解函数的递归定义；类型的递归定义；如何确定一个递归（函数）定义是否有解？确定唯一的解---最小不动点什么样的函数有最小不动点（解）？连续函数什么样的函数是连续函数？定义域和值域是论域满足一定的条件什么样的集合是论域，如何得到？完全半序集论域构造符最小不动点连续函数论域完全半序集基本概念半序集(partial-orderedset)最小(大)上(下)界(least(upper)bound)完全半序集(CPO)平坦集半序集定义设D是一个集合，是定义在D上的二元关系，满足下面性质：

自反性：

xD,有xx；传递性：

x,y,zD,如果存在xy和yz,则必有xz；反对称性：

x,yD,如果存在xy和yx,则必有x=y； 称

为半序关系(partialorder)，(D，

)为半序集半序集例子D={1，2}，pow(D)是D的所有子集构成的集合，是定义在D上的子集关系，pow(D)={,{1},{2},{1,2}};

是pow(D)上的半序关系；(pow(D)

，

)为半序集；可以用图表示：

{1}{2}{1，2}最小上界(2015-5-15)上/下界：设(D,

)为任意半序集，而且D’

D,d

D,则子集D’的上界和下界的定义如下：上界：若对任意d’D’,都有d’d,则称d为D’的上界；下界：若对任意d’D’,都有dd’,则称d为D’的下界；最小上界/最大下界：设(D,

)为任意半序集，而且D’

D,则子集D’的最小上界和最大下界的定义如下：最小上界：设d是D’的一个上界，若对D’的任意一个上界d’,都有dd’,则称d为D’的最小上界，并记为D’；最大下界：设d是D’的一个下界，若对D’的任意一个下界d’,都有d’d,则称d为D’的最大下界，并记为D’；最小上界最小上界唯一性：设(D,

)为任意半序集，而且D’

D。如果子集D’存在最小上界，则定唯一。最大下界也是。最小元