形式语义归纳原理

会计学1形式语义归纳原理形式语义归纳原理第三章第三章 归纳原理归纳原理n n第二章遗留的问题：第二章遗留的问题：n n自然语义自然语义n n对任意的命令对任意的命令对任意的命令对任意的命令c c c c和初始状态和初始状态和初始状态和初始状态，至多存在一个终止状，至多存在一个终止状态使得态使得c,？n n结构化操作语义结构化操作语义n n对任意的命令对任意的命令对任意的命令对任意的命令c c c c和初始状态和初始状态和初始状态和初始状态，至多存在一个终止状，至多存在一个终止状态使得态使得c,？n n自然语义描述与结构化操作语义描自然语义描述与结构化操作语义描述的等价性？述的等价性？第1页/共64页第三章第三章 归纳原理归纳原理数学归纳法数学归纳法良基归纳法良基归纳法结构归纳法结构归纳法结构归纳法的一般形式结构归纳法的一般形式规则归纳法规则归纳法 以操作语义为例，使用归纳法证明一些与操作语义相以操作语义为例，使用归纳法证明一些与操作语义相关的性质，从而对操作语义有更深入的理解；并为指称关的性质，从而对操作语义有更深入的理解；并为指称语义的学习打下基础。语义的学习打下基础。第2页/共64页3.1 数学归纳法数学归纳法n n数学归纳法：n n自然数集自然数集自然数集自然数集 是对是对是对是对0 0和后继运算封闭的最小集和后继运算封闭的最小集和后继运算封闭的最小集和后继运算封闭的最小集第3页/共64页3.1 数学归纳法数学归纳法设P(n)是与自然数N有关的性质第4页/共64页3.2 良基归纳法良基归纳法第二数学归纳法的正确性依赖于性质：自然数的每个子集都有最小元 良基集第5页/共64页3.2 良基归纳法良基归纳法良基关系是反自反的，否则会有无穷下降链 从极小元角度定义良基关系第6页/共64页3.2 良基归纳法良基归纳法n n如果某个集合上存在良基关系，则称其为良基集n n自然数之间的小于关系是良基关系（极小元等自然数之间的小于关系是良基关系（极小元等同于最小元）同于最小元）第7页/共64页3.2 良基归纳法良基归纳法n n良基归纳原理第8页/共64页3.2 良基归纳法良基归纳法n n良基归纳法v使用良基归纳法的关键是使用良基归纳法的关键是选择合适的良基关系选择合适的良基关系第一数学归纳法良基关系定义为自然数上的后继关系第二数学归纳法良基关系定义为自然数上的小于关系第9页/共64页3.2 良基归纳法良基归纳法例：证明下面的例：证明下面的EuclidEuclid算法求两个数的最大公约数程序对于任意算法求两个数的最大公约数程序对于任意大于大于0 0的自然数的自然数x x，y y都是终止的都是终止的v即要证明：对任意的初始状态即要证明：对任意的初始状态，若，若(x)0且且(y)0，则，则存在存在 使得使得 第10页/共64页3.2 良基归纳法良基归纳法v令：令：S=|(x)0且且(y)0 欲证：欲证：S，有下面性质，有下面性质P()成立：成立：良基关系：v是良基关系，是良基关系，(x)和和(y)的值不会无穷减少而始终保持大于的值不会无穷减少而始终保持大于0v极小元极小元 ：(x)=1且且(y)=1 第11页/共64页3.2 良基归纳法良基归纳法v良基归纳法证明：良基归纳法证明：归纳基对极小元：(x)=1且(y)=1归纳步 归纳假设：对任意的状态S，若则有P()成立 下面证明这时也有P()成立第12页/共64页3.2 良基归纳法良基归纳法归纳步 归纳假设：对任意的状态S，若则有P()成立 下面证明这时也有P()成立设(x)=m，(y)=n，分两种情况：(1)m=n 则有=false 第13页/共64页3.2 良基归纳法良基归纳法归纳步 归纳假设：对任意的状态S，若则有P()成立 下面证明这时也有P()成立设(x)=m，(y)=n，分两种情况：(2)mn 则有=true，根据while和if语义规则，得到：其中：第14页/共64页3.2 良基归纳法良基归纳法归纳步 归纳假设：对任意的状态S，若则有P()成立 下面证明这时也有P()成立其中：不管哪种情况都有：因此：为真，即存在某个状态，使得：至此证明了，对任意的S，有P(),即对任意的S，上述程序都是终止的第15页/共64页3.2 良基归纳法良基归纳法小结：小结：v良基归纳法是证明程序终止性的最重要的方法良基归纳法是证明程序终止性的最重要的方法由于程序中存在循环和递归，程序可能无法正常终止如果能够证明执行程序的循环或递归会使良基集的值变小，则程序必会终止 第16页/共64页3.3 结构归纳法结构归纳法n n归纳定义n n归纳基：给出集合归纳基：给出集合A A的的基本元素基本元素n n归纳步：给出从已有元素构造新元归纳步：给出从已有元素构造新元素的素的构造方法构造方法n n最小化：集合最小化：集合A A是对基本元素和构是对基本元素和构造方法封闭的造方法封闭的最小集最小集n n例如：例如：第17页/共64页3.3 结构归纳法结构归纳法n n结构归纳法对归纳定义的集合对归纳定义的集合A A，要证明性质，要证明性质P P对集合对集合A A的所有元素都成立，只要的所有元素都成立，只要证明：证明：n n归纳基归纳基：直接证明性质：直接证明性质P P对于对于A A的的基本元素都成立基本元素都成立n n归纳步归纳步：对于构造：对于构造A A的某种构造方的某种构造方法，证明若法，证明若a a是由是由a a1 1,a,a2 2,a,an n用该方用该方法构造得到的，证明若性质法构造得到的，证明若性质P P对于对于a a1 1,a,a2 2,a,an n都成立蕴涵性质都成立蕴涵性质P P对对a a也成也成立。（在归纳假设性质立。（在归纳假设性质P P对对a a1 1,a,a2 2,a,an n都成立的情况下，证明都成立的情况下，证明P P对对a a也成立）也成立）这种证明方法的正确性基于：集合A是对于基本元素和构造方法封闭的最小集合。设：S=aA|性质P对于a成立S也对于基本元素和构造方法封闭第18页/共64页3.3 结构归纳法结构归纳法n n结构归纳法是良基归纳法的特例n n在归纳定义集合在归纳定义集合A A上定义良基关系：上定义良基关系：由于由于A A是对基本元素和构造方法封闭的最小集合，是对基本元素和构造方法封闭的最小集合，A A的每个元素，要么是基本元素，要么可根据某种构的每个元素，要么是基本元素，要么可根据某种构造方法进行分解为其前趋造方法进行分解为其前趋这种分解不可能无限进行下去，一定会得到基本元这种分解不可能无限进行下去，一定会得到基本元素而不可再分素而不可再分因此上述关系是良基关系因此上述关系是良基关系第19页/共64页3.3 结构归纳法结构归纳法命题命题3.3 3.3 对于所有的算术表达式对于所有的算术表达式a a，状态，状态 和整数和整数mm，mm，有：，有：令P是算术表达式的一个性质，要证明对所有的算术表达式a性质P(a)为真，只要这证明：对所有的原子表达式a性质P(a)为真 对所有算术表达式的各种构成方法该性质也保持为真分情形证明：只有一条规则可用，所以m=m=n根据加法规则，必存在m0、m1和m0、m1满足：由归纳假设，m0=m0 且m1=m1，所以m=m同理可证明其他几种情况第20页/共64页3.4 规则归纳法规则归纳法规则归纳法规则归纳法n n为了将结构归纳法用于更为复杂的情况，将归纳定义的思想用规为了将结构归纳法用于更为复杂的情况，将归纳定义的思想用规为了将结构归纳法用于更为复杂的情况，将归纳定义的思想用规为了将结构归纳法用于更为复杂的情况，将归纳定义的思想用规则的形式做更为数学化的描述则的形式做更为数学化的描述则的形式做更为数学化的描述则的形式做更为数学化的描述n n规则归纳法是结构归纳法的一般形式规则归纳法是结构归纳法的一般形式规则归纳法是结构归纳法的一般形式规则归纳法是结构归纳法的一般形式v归纳定义的一般形式归纳定义的一般形式归纳定义集合的思想：基本元素归纳定义集合的思想：基本元素+构造方法。构造方法。使用规则的形式描述这种归纳定义使用规则的形式描述这种归纳定义首先定义什么是规则第21页/共64页3.4 规则归纳法规则归纳法定义：给定集合定义：给定集合X X，X X上的一个规则（上的一个规则（rulerule）集是关系：）集是关系：集合称为规则集R的基公理 H=H为有限集（包括空集）第22页/共64页3.4 规则归纳法规则归纳法例：算术表达式例：算术表达式第23页/共64页3.4 规则归纳法规则归纳法例：也可明确写为：例：也可明确写为：第24页/共64页3.4 规则归纳法规则归纳法定义：R推导树 给定给定X X上的规则上的规则R R，R R推导树是满足如下条件的有穷树（树的推导树是满足如下条件的有穷树（树的节点个数有穷）节点个数有穷）（1 1）所有的节点都由）所有的节点都由X X中的元素标记，特别地，叶子节点由中的元素标记，特别地，叶子节点由规则集规则集R R的基中的元素标记；的基中的元素标记；（2 2）所有的内部节点（包括根）都满足：设标记该节点的元）所有的内部节点（包括根）都满足：设标记该节点的元素是素是x x0 0，而它的（直接）子节点由，而它的（直接）子节点由x x1 1,x,x2 2,x,xn n标记，则标记，则是是R的某个规则的实例的某个规则的实例第25页/共64页3.4 规则归纳法规则归纳法如果xX存在根由x标记的R推导树，则称x是R可推导的，记为：简记为：简记为：第26页/共64页3.4 规则归纳法规则归纳法定义：给定X上的规则集R，称X 的子集为为R R归纳定义的集合。归纳定义的集合。规则集R定义的集合就是能够使用其中的规则有限步推导得到的元素。归纳定义可看作子集概括原理的一种特殊方式，它使用集合X上的一组规则概括出X的一个子集。指明集合X是为了避免悖论，所关注的是规则所定义的子集本身I IR R是对是对R封闭封闭的最小集的最小集集合Q对规则集是R封闭的当且仅当对所有规则实例(H/x)，有HQ xQ归纳定义的正确性？（存在且惟一）3.6节再讨论第27页/共64页3.4 规则归纳法规则归纳法n n规则归纳法基本思想n n在一个推导中，如果一个性质在从所有规则实在一个推导中，如果一个性质在从所有规则实例的前提移动到结论的过程中保持为真，那么例的前提移动到结论的过程中保持为真，那么该推导的结论也具有该性质。因此，对由这些该推导的结论也具有该性质。因此，对由这些规则定义的集合中的所有元素该性质也为真。规则定义的集合中的所有元素该性质也为真。n n要证明对要证明对规则所定义的集合规则所定义的集合的所有元素某个性的所有元素某个性质为真，常常用到规则归纳法。质为真，常常用到规则归纳法。第28页/共64页3.4 规则归纳法规则归纳法n n规则归纳法n nI IR R是规则集是规则集R R定义的集合，定义的集合，P P是某是某个性质，个性质，x x I IR R.P(.P(x x)当且仅当：当且仅当：对任意规则实例对任意规则实例 (H H/x x)R R，其，其中中 H H I IR R有：有：(h h H H.P P(h h)P P(x x)v证明：证明：令 Q=xIR|性质P对x成立显然有：Q IR。为了证：IR Q，只要证明Q对R封闭（因为IR是对R封闭的最小集）；由定理给出条件表明Q对R封闭。因此，Q=IR。第29页/共64页3.4 规则归纳法规则归纳法v规则归纳法是良基归纳法的特例：规则归纳法是良基归纳法的特例：令T是所有R推导树构成的集合，在T上可定义关系“”为：对任意的R推导树t1,t2T,t1t2 当且仅当 t1是t2的直接子树T中任意R推导树都只有有穷个节点，而t1t2意味着t1的节点数比t2的节点数少，因此，对任意的tT不存在无穷下降链：tn t2 t1第30页/共64页3.4 规则归纳法规则归纳法n nIR是对R封闭的最小集 命题：给定X上的规则集R（1 1）I IR R是是R R封闭的，且封闭的，且（2 2）若）若Q Q对对R R封闭，则封闭，则I IR R Q Qv证明：证明：（1）显然。（2）用T上的良基归纳法证明。对所有规则实例(H/x)，有H IR x IRtt1t2tn第31页/共64页3.4 规则归纳法规则归纳法n n特殊的规则归纳法考虑规则定义的子集的性质 A IRaA.Q(a)对R中所有规则实例(X/y)，X IR，y A，有：(xXA.Q(x)Q(y)采取特殊归纳法，减少证明中使用的规则的数量。第32页/共64页3.5 操作语义的证明规则操作语义的证明规则算术表达式的求值规则算术表达式的求值规则积第33页/共64页3.5 操作语义的证明规则操作语义的证明规则逻辑表达式的求值规则逻辑表达式的求值规则当t0为true且t1为true时t为true，否则为false当t0为true或t1为true时t为true，否则为false第34页/共64页3.5 操作语义的证明规则操作语义的证明规则命令的规则小结命令的规则小结第35页/共64页3.5 操作语义的证明规则操作语义的证明规则n n例：对任意的程序例：对任意的程序S S和初始状态和初始状态，至多存在一个终止状，至多存在一个终止状态使得态使得S,。即：对任意的程序。即：对任意的程序S S，及任意的状态，及任意的状态 ,有：有：第36页/共64页3.5 操作语义的证明规则操作语义的证明规则n n例：对任意的程序例：对任意的程序S S和初始状态和初始状态，至多存在一个终止状，至多存在一个终止状态使得态使得S,。即：对任意的程序。即：对任意的程序S S，及任意的状态，及任意的状态 ,有：有：S是语句skip,=。若还有，则=第37页/共64页3.5 操作语义的证明规则操作语义的证明规则n n例：对任意的程序例：对任意的程序S S和初始状态和初始状态，至多存在一个终止状，至多存在一个终止状态使得态使得S,。即：对任意的程序。即：对任意的程序S S，及任意的状态，及任意的状态 ,有：有：S是语句x=a，=m/x。若还有，则只有这一种变迁规则，所以=m/x。因此=第38页/共64页3.5 操作语义的证明规则操作语义的证明规则n n例：对任意的程序例：对任意的程序S S和初始状态和初始状态，至多存在一个终止状，至多存在一个终止状态使得态使得S,。即：对任意的程序。即：对任意的程序S S，及任意的状态，及任意的状态 ,有：有：S是语句S0;S1，这时存在1使得：1 且 若还有，则只有该变迁规则得到，即存在1使得：1 且 。根据归纳假设，由 1和 1可得1=1进而可得：=第39页/共64页3.5 操作语义的证明规则操作语义的证明规则n n例：对任意的程序例：对任意的程序S S和初始状态和初始状态，至多存在一个终止状，至多存在一个终止状态使得态使得S,。即：对任意的程序。即：对任意的程序S S，及任意的状态，及任意的状态 ,有：有：S=if b then S0 else S1，且b为true。这时有：若还有，由于S=if b then S0 else S1，且b为true，则只有该变迁规则得到，即存在使得：。根据归纳假设，由 和 可得=因而：=同理可证b为false的情况。第40页/共64页3.5 操作语义的证明规则操作语义的证明规则n n例：对任意的程序例：对任意的程序S S和初始状态和初始状态，至多存在一个终止状，至多存在一个终止状态使得态使得S,。即：对任意的程序。即：对任意的程序S S，及任意的状态，及任意的状态 ,有：有：S=while b do S，且b为false。这时有=若还有，由于S=while b do S，且b为false，则只有该变迁规则得到，即=。因而：=第41页/共64页3.5 操作语义的证明规则操作语义的证明规则n n例：对任意的程序例：对任意的程序S S和初始状态和初始状态，至多存在一个终止状，至多存在一个终止状态使得态使得S,。即：对任意的程序。即：对任意的程序S S，及任意的状态，及任意的状态 ,有：有：S=while b do S1，且b为true。这时存在1使得：1 且 若还有，由于S=while b do S1，且b为true，则只有该变迁规则得到:1 且 根据将归纳假设应用于 和 ，可得：=第42页/共64页3.5 操作语义的证明规则操作语义的证明规则n n小结：n n规则归纳法是证明由规则表示的操作语义性质的有用工具规则归纳法是证明由规则表示的操作语义性质的有用工具n n证明规则定义的集合具有某性质，就是证明规则保持该性质证明规则定义的集合具有某性质，就是证明规则保持该性质（前提到结论）（前提到结论）n n常常对各规则分别归纳常常对各规则分别归纳特殊规则归纳法特殊规则归纳法第43页/共64页3.6 算子及其最小不动点算子及其最小不动点n n归纳定义的正确性存在性？惟一性？第44页/共64页3.6 算子及其最小不动点算子及其最小不动点n n不动点（fixed point）n n定义：集合定义：集合X X上的函数上的函数 f f：XXXX的的不动点不动点是满足是满足f f(x x)=)=x x的元素的元素x x X X。进一步讨论IR的构造方式第45页/共64页3.6 算子及其最小不动点算子及其最小不动点给定集合X上的规则集R，可定义算子(函数)对X的任意子集SX，以子集S中的元素为前提能一步推导得到的元素构成的子集合n n也可以用该算子表示一个集合是也可以用该算子表示一个集合是R R封闭的：封闭的：n n命题：命题：一个集合一个集合B B是是R R封闭的，当且仅当：封闭的，当且仅当：由定义直接可证第46页/共64页3.6 算子及其最小不动点算子及其最小不动点引理引理3.6.1：给定集合X上的规则集R，函数：是单调的（monotonic），即对任意的S,TX,n n证明：n n此引理显然成立。此引理显然成立。因为对任意的因为对任意的按定义按定义,存在存在H H S S，使得，使得(H/(H/x x)R R由于由于S S T T，有，有H H T T，从而，从而第47页/共64页3.6 算子及其最小不动点算子及其最小不动点v将算子 反复作用于空集上：根据算子的单调性有：第48页/共64页3.6 算子及其最小不动点算子及其最小不动点v令：有如下命题：命题：命题：1）A是R封闭的2）A是函数 的不动点，即：3）A是最小R封闭集第49页/共64页3.6 算子及其最小不动点算子及其最小不动点证明：要证：要证：对任意的根据前面的约定，H是有限集，即存在n使得H=h1,h2,hn存在HA，使得(H/x)R。对任意的 hiH（1i n），由于HA，因此 hiA根据A的定义，存在ji使得：hiAji，令：j=maxj1,j2,jnhiAj从而：HAj根据定义命题：命题：1）A是R封闭的第50页/共64页3.6 算子及其最小不动点算子及其最小不动点证明：要证：要证：命题：命题：2）对任意的根据A的定义，存在n 使得:也即存在 HAn-1，使得(H/x)R。又 An-1 A，因此存在 HA 使得(H/x)R。根据算子的定义，第51页/共64页3.6 算子及其最小不动点算子及其最小不动点证明：即要证：如果即要证：如果B是另一个是另一个R封闭集，则封闭集，则A B命题：命题：3）A是最小R封闭集设B是R封闭的，则：用数学归纳法可证：对任意的n，An BA0=，A0 B若 An B，因为R是单调的且B是R封闭的，所以：命题得证第52页/共64页3.6 算子及其最小不动点算子及其最小不动点 是是 的最小不动点的最小不动点存在而且惟一第53页/共64页小结小结v归纳法是研究归纳法是研究PL形式语义的最重要的技术形式语义的最重要的技术n数学归纳法n良基归纳法n结构归纳法第54页/共64页小结小结v举例：举例：条件：(x)6证明：6/x令：wwhile(x 5)do x:=x+1 i=(6-i)/x (i)0=6/x 0 (i)第55页/共64页小结小结v举例：举例：条件：(x)6证明：6/x归纳基：i=0第56页/共64页小结小结v举例：举例：条件：(x)6证明：6/x归纳步：要证第57页/共64页小结小结v举例举例2-1：对任意的对任意的IMP程序程序S，以及状态，以及状态 和和，有：，有：即：如果在自然语义中，即：如果在自然语义中，S从状态从状态 开始终止于开始终止于，则在结构化操作语义中，它也终止于同一个状态。则在结构化操作语义中，它也终止于同一个状态。证明：对产生变迁关系证明：对产生变迁关系 的推导步进行归纳的推导步进行归纳第58页/共64页小结小结v举例举例2-2：对任意的对任意的IMP程序程序S，以及状态，以及状态 和和，有：，有：即：如果在结构化操作语义中，即：如果在结构化操作语义中，S从状态从状态 开始终止开始终止于于，则在自然语义中，它也终止于同一个状态。，则在自然语义中，它也终止于同一个状态。证明：对推导证明：对推导*中的中的n实施数学归纳法实施数学归纳法第59页/共64页讨论讨论第60页/共64页讨论讨论第61页/共64页讨论讨论第62页/共64页第63页/共64页