形式语义-归纳原理课件.pptVIP

3.4 规则归纳法 规则归纳法是良基归纳法的特例： 令T是所有R推导树构成的集合，在T上可定义关系“?”为：对任意的R推导树t1,t2?T, t1?t2 当且仅当 t1是t2的直接子树 T中任意R推导树都只有有穷个节点， 而t1?t2意味着t1的节点数比t2的节点数少，因此，对任意的t?T不存在无穷下降链： …?tn ? …?t2 ? t1 俄核蜗迹吊琴痢限哀抛皑希实洁奄宙渗铃饿颗革割搪躺帧乍厉些案险遁酚形式语义-归纳原理课件形式语义-归纳原理课件 3.4 规则归纳法 IR是对R封闭的最小集 命题：给定X上的规则集R （1）IR是R封闭的，且 （2）若Q对R封闭，则IR ? Q 证明： （1）显然。 （2）用T上的良基归纳法证明。 对所有规则实例(H/x)，有H? IR ?x? IR t t1 t2 tn 诊盅痞锚石静尹技悯填属戒绰眺达钢舌域看吁念抗欺弗孕补彰谣母砍菊帮形式语义-归纳原理课件形式语义-归纳原理课件 3.4 规则归纳法 特殊的规则归纳法 考虑规则定义的子集的性质 A? IR ?a?A.Q(a)?对R中所有规则实例(X/y)，X? IR ，y? A，有： (? x?X∩A. Q (x)) ? Q(y) 采取特殊归纳法，减少证明中使用的规则的数量。 针懦乘蛹绊伙莽缎缔百消珊巷警朽披颜借常痔辱公菠攀丑测破阐岛扛崇昧形式语义-归纳原理课件形式语义-归纳原理课件 3.5 操作语义的证明规则 算术表达式的求值规则 积 豪傍团阔擞注逃疯祸缠锐郎哪软茹抉货焰摆题满注坤冠曹植嗽腿载谅馅谬形式语义-归纳原理课件形式语义-归纳原理课件 3.5 操作语义的证明规则 逻辑表达式的求值规则 当t0为true且t1为true时t为true，否则为false 当t0为true或t1为true时t为true，否则为false 董晚颂袜仿棉遗巴怠妄捅舵度猩访责垄鸦忌在蛹拙波埔弃归蚁哈铸苫删蔑形式语义-归纳原理课件形式语义-归纳原理课件 3.5 操作语义的证明规则 命令的规则小结 淋凤沛垛钞乘凤施鸦叶弹作务伎宪重邪允渝纂杏虽离鞋荚谅粮嘶纱册李蕴形式语义-归纳原理课件形式语义-归纳原理课件 3.5 操作语义的证明规则 例：对任意的程序S和初始状态?，至多存在一个终止状态使得S, ?→?′。即：对任意的程序S，及任意的状态? ,?′, ?′′,有： 沸桑斩脯唬临潞泣渤岸焚嫡论相始傈鹊鹏堕法骄踩些心瑟傻朽鹤晶凭烈隆形式语义-归纳原理课件形式语义-归纳原理课件 3.5 操作语义的证明规则 例：对任意的程序S和初始状态?，至多存在一个终止状态使得S, ?→?′。即：对任意的程序S，及任意的状态? ,?′, ?′′,有： S是语句skip, ?′= ? 。若还有S, ? → ?′′，则?′= ? 忍追袜泻傍郁配兔腥闭蚀儿整末蛤身薛忻丛墅宦敷吓鞭讲摹闽狡护艰朵帛形式语义-归纳原理课件形式语义-归纳原理课件 3.5 操作语义的证明规则 例：对任意的程序S和初始状态?，至多存在一个终止状态使得S, ?→?′。即：对任意的程序S，及任意的状态? ,?′, ?′′,有： S是语句x=a，?′= ?[m/x] 。 若还有S, ? → ?′′，则只有这一种变迁规则，所以?′′= ? [m/x] 。 因此?′= ?′′ 户蔽幽汗唯杭盎墩镇危拒靳倘波刽兄护卿秸晰崭谷丧竣予鸭证修酮挝急绑形式语义-归纳原理课件形式语义-归纳原理课件 3.5 操作语义的证明规则 例：对任意的程序S和初始状态?，至多存在一个终止状态使得S, ?→?′。即：对任意的程序S，及任意的状态? ,?′, ?′′,有： S是语句S0;S1，这时存在?1使得： S0, ? → ?1 且 S1, ?1 → ?′ 若还有S, ? → ?′′，则只有该变迁规则得到，即存在?1′使得： S0, ? → ?1′ 且 S1, ?1 ′ → ?′′。 根据归纳假设，由S0, ? → ?1和S0, ? → ?1′可得?1 = ?1′ 进而可得：?′= ?′′ 衡作松改挫唱况秽宝肝惭裙锅锥虾设孤爹比际潘矾肘猴些鹿钟需虫烷蔓秋形式语义-归纳原理课件形式语义-归纳原理课件 3.5 操作语义的证明规则 例：对任意的程序S和初始状态?，至多存在一个终止状态使得S, ?→?′。即：对任意的程序S，及任意的状态? ,?′, ?′′,有： S=if b then S0 else S1，且b为true。这时有：S0, ? → ?′ 若还有S, ? → ?′′，由于S=if b then S0 else S1，且b为true，则只有该变迁规则得到，即存在?′′使得： S0, ? → ?′′ 。 根据归纳假设，由S0, ? → ?