形式语义-归纳原理.ppt

程序设计语言的形式语义,TheFormalSemanticsofProgrammingLanguages,第三章归纳原理,第二章遗留的问题：自然语义对任意的命令c和初始状态，至多存在一个终止状态使得？结构化操作语义对任意的命令c和初始状态，至多存在一个终止状态使得？自然语义描述与结构化操作语义描述的等价性？,第三章归纳原理,数学归纳法,结构归纳法的一般形式规则归纳法,以操作语义为例，使用归纳法证明一些与操作语义相关的性质，从而对操作语义有更深入的理解；并为指称语义的学习打下基础。,3.1数学归纳法,数学归纳法：自然数集是对0和后继运算封闭的最小集,3.1数学归纳法,设P(n)是与自然数N有关的性质,3.2良基归纳法,第二数学归纳法的正确性依赖于性质：自然数的每个子集都有最小元良基集,3.2良基归纳法,良基关系是反自反的，否则会有无穷下降链从极小元角度定义良基关系,3.2良基归纳法,如果某个集合上存在良基关系，则称其为良基集自然数之间的小于关系是良基关系（极小元等同于最小元）,3.2良基归纳法,良基归纳原理,3.2良基归纳法,良基归纳法,使用良基归纳法的关键是选择合适的良基关系第一数学归纳法良基关系定义为自然数上的后继关系第二数学归纳法良基关系定义为自然数上的小于关系,3.2良基归纳法,例：证明下面的Euclid算法求两个数的最大公约数程序对于任意大于0的自然数x，y都是终止的,即要证明：对任意的初始状态，若(x)0且(y)0，则存在使得,3.2良基归纳法,令：S=|(x)0且(y)0欲证：S，有下面性质P()成立：,良基关系：,是良基关系，(x)和(y)的值不会无穷减少而始终保持大于0极小元：(x)=1且(y)=1,3.2良基归纳法,良基归纳法证明：归纳基对极小元：(x)=1且(y)=1,归纳步归纳假设：对任意的状态S，若则有P()成立下面证明这时也有P()成立,3.2良基归纳法,归纳步归纳假设：对任意的状态S，若则有P()成立下面证明这时也有P()成立,设(x)=m，(y)=n，分两种情况：(1)m=n,则有=false,3.2良基归纳法,归纳步归纳假设：对任意的状态S，若则有P()成立下面证明这时也有P()成立,设(x)=m，(y)=n，分两种情况：(2)mn,则有=true，根据while和if语义规则，得到：,其中：,3.2良基归纳法,归纳步归纳假设：对任意的状态S，若则有P()成立下面证明这时也有P()成立,其中：,不管哪种情况都有：,至此证明了，对任意的S，有P(),即对任意的S，上述程序都是终止的,3.2良基归纳法,小结：良基归纳法是证明程序终止性的最重要的方法由于程序中存在循环和递归，程序可能无法正常终止如果能够证明执行程序的循环或递归会使良基集的值变小，则程序必会终止,3.3结构归纳法,归纳定义归纳基：给出集合A的基本元素归纳步：给出从已有元素构造新元素的构造方法最小化：集合A是对基本元素和构造方法封闭的最小集例如：,3.3结构归纳法,结构归纳法对归纳定义的集合A，要证明性质P对集合A的所有元素都成立，只要证明：归纳基：直接证明性质P对于A的基本元素都成立归纳步：对于构造A的某种构造方法，证明若a是由a1,a2,an用该方法构造得到的，证明若性质P对于a1,a2,an都成立蕴涵性质P对a也成立。（在归纳假设性质P对a1,a2,an都成立的情况下，证明P对a也成立）,这种证明方法的正确性基于：集合A是对于基本元素和构造方法封闭的最小集合。设：S=aA|性质P对于a成立S也对于基本元素和构造方法封闭,3.3结构归纳法,结构归纳法是良基归纳法的特例在归纳定义集合A上定义良基关系：,由于A是对基本元素和构造方法封闭的最小集合，A的每个元素，要么是基本元素，要么可根据某种构造方法进行分解为其前趋这种分解不可能无限进行下去，一定会得到基本元素而不可再分因此上述关系是良基关系,3.3结构归纳法,命题3.3对于所有的算术表达式a，状态和整数m，m，有：,令P是算术表达式的一个性质，要证明对所有的算术表达式a性质P(a)为真，只要这证明：对所有的原子表达式a性质P(a)为真对所有算术表达式的各种构成方法该性质也保持为真,分情形证明：,只有一条规则可用，所以m=m=n,根据加法规则，必存在m0、m1和m0、m1满足：,由归纳假设，m0=m0且m1=m1，所以m=m,同理可证明其他几种情况,3.4规则归纳法,规则归纳法为了将结构归纳法用于更为复杂的情况，将归纳定义的思想用规则的形式做更为数学化的描述规则归纳法是结构归纳法的一般形式,归纳定义的一般形式归纳定义集合的思想：基本元素+构造方法。使用规则的形式描述这种归纳定义,首先定义什么是规则,3.4规则归纳法,定义：给定集合X，X上的一个规则（rule）集是关系：,公理H=,H为有限集（包括空集）,3.4规则归纳法,例：算术表达式,3.4规则归纳法,例：也可明确写为：,3.4规则归纳法,定义：R推导树给定X上的规则R，R推导树是满足如下条件的有穷树（树的节点个数有穷）（1）所有的节点都由X中的元素标记，特别地，叶子节点由规则集R的基中的元素标记；（2）所有的内部节点（包括根）都满足：设标记该节点的元素是x0，而它的（直接）子节点由x1,x2,xn标记，则,是R的某个规则的实例,3.4规则归纳法,如果xX存在根由x标记的R推导树，则称x是R可推导的，记为：,简记为：,3.4规则归纳法,定义：给定X上的规则集R，称X的子集,为R归纳定义的集合。,规则集R定义的集合就是能够使用其中的规则有限步推导得到的元素。归纳定义可看作子集概括原理的一种特殊方式，它使用集合X上的一组规则概括出X的一个子集。指明集合X是为了避免悖论，所关注的是规则所定义的子集本身,IR是对R封闭的最小集,集合Q对规则集是R封闭的当且仅当对所有规则实例(H/x)，有HQxQ,归纳定义的正确性？（存在且惟一）3.6节再讨论,3.4规则归纳法,规则归纳法基本思想在一个推导中，如果一个性质在从所有规则实例的前提移动到结论的过程中保持为真，那么该推导的结论也具有该性质。因此，对由这些规则定义的集合中的所有元素该性质也为真。要证明对规则所定义的集合的所有元素某个性质为真，常常用到规则归纳法。,3.4规则归纳法,规则归纳法IR是规则集R定义的集合，P是某个性质，xIR.P(x)当且仅当：对任意规则实例(H/x)R，其中HIR有：(hH.P(h)P(x),证明：令Q=xIR|性质P对x成立显然有：QIR。为了证：IRQ，只要证明Q对R封闭（因为IR是对R封闭的最小集）；由定理给出条件表明Q对R封闭。因此，Q=IR。,3.4规则归纳法,规则归纳法是良基归纳法的特例：令T是所有R推导树构成的集合，在T上可定义关系“”为：对任意的R推导树t1,t2T,t1t2当且仅当t1是t2的直接子树T中任意R推导树都只有有穷个节点，而t1t2意味着t1的节点数比t2的节点数少，因此，对任意的tT不存在无穷下降链：tnt2t1,3.4规则归纳法,IR是对R封闭的最小集命题：给定X上的规则集R（1）IR是R封闭的，且（2）若Q对R封闭，则IRQ,证明：（1）显然。（2）用T上的良基归纳法证明。,对所有规则实例(H/x)，有HIRxIR,3.4规则归纳法,特殊的规则归纳法,考虑规则定义的子集的性质AIRaA.Q(a)对R中所有规则实例(X/y)，XIR，yA，有：(xXA.Q(x)Q(y)采取特殊归纳法，减少证明中使用的规则的数量。,3.5操作语义的证明规则,3.5操作语义的证明规则,3.5操作语义的证明规则,命令的规则小结,3.5操作语义的证明规则,例：对任意的程序S和初始状态，至多存在一个终止状态使得。即：对任意的程序S，及任意的状态,有：,3.5操作语义的证明规则,例：对任意的程序S和初始状态，至多存在一个终止状态使得。即：对任意的程序S，及任意的状态,有：,S是语句skip,=。若还有，则=,3.5操作语义的证明规则,例：对任意的程序S和初始状态，至多存在一个终止状态使得。即：对任意的程序S，及任意的状态,有：,S是语句x=a，=m/x。若还有，则只有这一种变迁规则，所以=m/x。因此=,3.5操作语义的证明规则,例：对任意的程序S和初始状态，至多存在一个终止状态使得。即：对任意的程序S，及任意的状态,有：,S是语句S0;S1，这时存在1使得：1且若还有，则只有该变迁规则得到，即存在1使得：1且。根据归纳假设，由1和1可得1=1进而可得：=,3.5操作语义的证明规则,例：对任意的程序S和初始状态，至多存在一个终止状态使得。即：对任意的程序S，及任意的状态,有：,S=ifbthenS0elseS1，且b为true。这时有：若还有，由于S=ifbthenS0elseS1，且b为true，则只有该变迁规则得到，即存在使得：。根据归纳假设，由和可得=因而：=同理可证b为false的情况。,3.5操作语义的证明规则,例：对任意的程序S和初始状态，至多存在一个终止状态使得。即：对任意的程序S，及任意的状态,有：,S=whilebdoS，且b为false。这时有=若还有，由于S=whilebdoS，且b为false，则只有该变迁规则得到，即=。因而：=,3.5操作语义的证明规则,例：对任意的程序S和初始状态，至多存在一个终止状态使得。即：对任意的程序S，及任意的状态,有：,S=whilebdoS1，且b为true。这时存在1使得：1且若还有，由于S=whilebdoS1，且b为true，则只有该变迁规则得到:1且根据将归纳假设应用于和，可得：=,3.5操作语义的证明规则,小结：规则归纳法是证明由规则表示的操作语义性质的有用工具证明规则定义的集合具有某性质，就是证明规则保持该性质（前提到结论）常常对各规则分别归纳特殊规则归纳法,3.6算子及其最小不动点,归纳定义的正确性,存在性？,惟一性？,3.6算子及其最小不动点,不动点（fixedpoint）定义：集合X上的函数f：XX的不动点是满足f(x)=x的元素xX。,进一步讨论IR的构造方式,3.6算子及其最小不动点,给定集合X上的规则集R，可定义算子(函数),对X的任意子集SX，,以子集S中的元素为前提能一步推导得到的元素构成的子集合,也可以用该算子表示一个集合是R封闭的：命题：一个集合B是R封闭的，当且仅当：,由定义直接可证,3.6算子及其最小不动点,引理3.6.1：给定集合X上的规则集R，函数：是单调的（monotonic），即对任意的S,TX,证明：此引理显然成立。因为对任意的按定义,存在HS，使得(H/x)R由于ST，有HT，从而,3.6算子及其最小不动点,将算子反复作用于空集上：,根据算子的单调性有：,3.6算子及其最小不动点,令：,有如下命题：,命题：1）A是R封闭的2）A是函数的不动点，即：3）A是最小R封闭集,3.6算子及其最小不动点,证明：,要证：,对任意的,根据前面的约定，H是有限集，即存在n使得H=h1,h2,hn,存在HA，使得(H/x)R。,对任意的hiH（1in），由于HA，因此hiA,根据A的定义，存在ji使得：hiAji，令：j=maxj1,j2,jn,hiAj,从而：HAj,根据定义,命题：1）A是R封闭的,3.6算子及其最小不动点,证明：,要证：,命题：2）,对任意的,根据A的定义，存在n使得:,也即存在HAn-1，使得(H/x)R。,又An-1A，因此存在HA使得(H/x)R。,根据算子的定义，,3.6算子及其最小不动点,证明：,即要证：如果B是另一个R封闭集，则AB,命题：3）A是最小R封闭集,设B是R封闭的，则：,用数学归纳法可证：对任意的n，AnB,A0=，A0B,若AnB，因为R是单调的且B是R封闭的，所以：,命题得证,3.6算子及其最小不动点,是的最小不动点,存在而且惟一,小结,归纳法是研究PL形式语义的最重要的技术数学归纳法良基归纳法结构归纳法,小结,举例：,条件：(x)6证明：6/x,令：wwhile(x5)dox:=x+1i=(6-i)/x(i)0=6/x,0