形式语义-归纳原理.ppt

《形式语义-归纳原理.ppt》由会员上传分享，免费在线阅读，更多相关内容在行业资料-天天文库。

1、程序设计语言的形式语义TheFormalSemanticsofProgrammingLanguages第三章归纳原理第二章遗留的问题：自然语义对任意的命令c和初始状态，至多存在一个终止状态使得→’？结构化操作语义对任意的命令c和初始状态，至多存在一个终止状态使得’？自然语义描述与结构化操作语义描述的等价性？第三章归纳原理数学归纳法良基归纳法结构归纳法结构归纳法的一般形式——规则归纳法以操作语义为例，使用归纳法证明一些与操作语义相关的性质，从而对操作语义有更深入的理解；并为指称语义的学习打下

2、基础。3.1数学归纳法数学归纳法：自然数集是对0和后继运算封闭的最小集3.1数学归纳法设P(n)是与自然数N有关的性质3.2良基归纳法第二数学归纳法的正确性依赖于性质：自然数的每个子集都有最小元良基集3.2良基归纳法良基关系是反自反的，否则会有无穷下降链从极小元角度定义良基关系3.2良基归纳法如果某个集合上存在良基关系，则称其为良基集自然数之间的小于关系是良基关系（极小元等同于最小元）3.2良基归纳法良基归纳原理3.2良基归纳法良基归纳法使用良基归纳法的关键是选择合适的良基关系第一数学归纳法良基关系定义为自然数上的后

3、继关系第二数学归纳法良基关系定义为自然数上的小于关系3.2良基归纳法例：证明下面的Euclid算法求两个数的最大公约数程序对于任意大于0的自然数x，y都是终止的即要证明：对任意的初始状态，若(x)＞0且(y)＞0，则存在’使得→’3.2良基归纳法令：S={

4、(x)＞0且(y)＞0}欲证：S，有下面性质P()成立：良基关系：是良基关系，(x)和(y)的值不会无穷减少而始终保持大于0极小元：(x)=1且(y)=13.2良基归纳法良基归纳法证明：归纳基对极小元：(x)

5、=1且(y)=1归纳步归纳假设：对任意的状态S，若’≺则有P(’)成立下面证明这时也有P()成立3.2良基归纳法归纳步归纳假设：对任意的状态S，若’≺则有P(’)成立下面证明这时也有P()成立设(x)=m，(y)=n，分两种情况：(1)m=n则有=false3.2良基归纳法归纳步归纳假设：对任意的状态S，若’≺则有P(’)成立下面证明这时也有P()成立设(x)=m，(y)=n，分两种情况：(2)m≠n则有=true，根据while和if语义规则，

6、得到：其中：3.2良基归纳法归纳步归纳假设：对任意的状态S，若’≺则有P(’)成立下面证明这时也有P()成立其中：不管哪种情况都有：因此：为真，即存在某个状态’，使得：至此证明了，对任意的∈S，有P(),即对任意的∈S，上述程序都是终止的3.2良基归纳法小结：良基归纳法是证明程序终止性的最重要的方法由于程序中存在循环和递归，程序可能无法正常终止如果能够证明执行程序的循环或递归会使良基集的值变小，则程序必会终止3.3结构归纳法归纳定义归纳基：给出集合A的基本元素归纳步：给出从已有元素构造新元素的构造方

7、法最小化：集合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={aA

8、性质P对于a成立

9、}S也对于基本元素和构造方法封闭3.3结构归纳法结构归纳法是良基归纳法的特例在归纳定义集合A上定义良基关系：由于A是对基本元素和构造方法封闭的最小集合，A的每个元素，要么是基本元素，要么可根据某种构造方法进行分解为其前趋这种分解不可能无限进行下去，一定会得到基本元素而不可再分因此上述关系是良基关系3.3结构归纳法命题3.3对于所有的算术表达式a，状态和整数m，m’，有：令P是算术表达式的一个性质，要证明对所有的算术表达式a性质P(a)为真，只要这证明：对所有的原子表达式a性质P(a)为真对所有算术表达式的各种构成方法

10、该性质也保持为真分情形证明：只有一条规则可用，所以m=m’=n根据加法规则，必存在m0、m1和m0’、m1’满足：由归纳假设，m0=m0’且m1=m1’，所以m=m’同理可证明其他几种情况3.4规则归纳法规则归纳法为了将结构归纳法用于更为复杂的情况，将归纳定义的思想用规则的形式做更为数学化的描述规则归纳法是结构归纳法的一般形式归纳