PM-06-Chap08 递归程序设计及其正确性证明.ppt

1 第8章递归程序设计及其正确性证明 1 概述2 递归程序的正确性证明3 递归程序向非递归程序的转换4 函数型程序设计简介 2 8 1概述 1 迭代与递归递归的概念一个函数 过程或者数据结构 如果在他们的定义内部又出现了定义本身的应用 则称这个函数 过程或者数据结构是递归的 或者是递归定义的 直接递归 若程序P包含着对自己的引用 则称为是直接递归的间接递归 若程序P包含着对另一程序Q的引用 而Q又直接或间接地引用P 则称为间接递归 例 3 8 1概述 递归的概念 续 intfact intn if n 0 return1 elsereturnn fact n 1 ProcedureB ProcedureCBeginBegin C B End End 4 8 1概述 递归实质是一种循环结构 他把较复杂情形的计算逐次地归结为 较简单 情形的计算 一直归结到 最简单 情形的计算 并得到计算结果为止 每个迭代程序原则上总可以转换成与它等价的递归程序 反之不然 并不是每个递归程序都可以转换成与他等价的迭代程序 递归程序的效率 时间和空间效率 比迭代程序低 递归程序较容易理解和阅读 实现直观 5 8 1概述 2 递归程序的一种模型一种简化的函数递归程序模型的一般形式如下 F x1 x2 xn ifp1thenE1elseifp2thenE2 elseifpmthenEmelseEm 1其中 pi i 1 2 m 是测试谓词 Ei i 1 2 m 1 是表达式 其中F可以在Ei和pi中出现 6 8 1概述 2 递归程序的一种模型例1 求非负整数x和y的最大公约数GCD x y GCD x y ifx 0thenyelseify xthenGCD y x elseGCD x y x 其中 x y 0 且不同时为0 例2 计算Fibonacci函数F x ifx 0then0elseifx 1then1elseF x 1 F x 2 其中 x为非负整数 7 8 1概述 3 递归计算的计算规则例1 F x1 x2 ifx1 0then0elseF 0 F x1 x2 其中 x1 x2 为非负整数对 计算F 1 2 1 规定先计算F的最外层调用F 1 2 F 0 F 1 2 0 2 规定先计算F的最内层调用F 1 2 F 0 F 1 2 F 0 F 0 F 1 2 8 8 1概述 3 递归计算的计算规则例2 Ackermann函数A x1 x2 ifx1 0thenx2 1elseifx2 0thenA x1 1 1 elseA x1 1 A x1 x2 1 其中 x1 x2 为非负整数对 计算A 1 2 1 规定先计算F的最外层调用A 1 2 A 0 A 1 1 A 1 1 1 A 0 A 1 0 1 A 1 0 1 1 A 0 1 2 2 2 4 2 规定先计算F的最内层调用A 1 2 A 0 A 1 1 A 0 A 0 A 1 0 A 0 A 0 A 0 1 A 0 A 0 2 A 0 3 4 9 8 1概述 3 递归计算的计算规则 1 递归程序可以采用不同的计算规则来计算 最内最左规则 先计算最内层的最左的调用最外最左规则 先计算最外层的最左的调用 2 采用不同的计算规则计算递归时 对相同的自变元 计算过程可能终止 也可能不终止 3 若对于不同计算规则 相应的递归程序 对相同的自变元计算过程都终止 则他们所得的计算结果一定相同 但计算效率不同 4 例 PASCAL Algol语言使用最内最左规则 10 8 2递归程序的正确性证明 结构归纳法1 1 结构归纳法 证明递归程序的部分正确性证明步骤 证明对于 最简单 的数据程序运行正确 假设对于 较简单 的数据 程序运行正确 归纳假设 在此基础之上 证明对于较复杂的数据 程序也运行正确 注释 这里的 数据 是指自变元所允许的取值 它可以是一般的数值 也可以是由数值 原子或表等组成的某种数据结构 11 8 2递归程序的正确性证明 结构归纳法2 例1 证明计算阶乘的程序F x ifx 1then1elsex F x 1 其中 x是大于0的整数 要证明对于所有正整数x F x x 该程序的规范为 P x x 0Q x z z x 12 8 2递归程序的正确性证明 结构归纳法3 证明 1 当x 1时 根据程序F x 1 1 正确 2 假设 对任意的正整数x F x x 成立 则对于x 1有 x是正整数 x 1 1根据程序F x 1 x 1 F x x 1 x 根据归纳假设 x 1 综上所述 证明了对于任何满足P x 的x 程序F x 执行结果将得到z x 即程序是部分正确的 对于程序的终止性 取良序集 N 归纳总会在有限步结束 否则与良序集 N 相矛盾 13 8 2递归程序的正确性证明 结构归纳法4 例2 证明程序Member x L ifL NILthenfalseelseifx CAR L thenTRUEelseMember x CDR L 的正确性 对于任意的原子 或表 和表L 即证明 Member x L false ifx不是L的元素true ifx是L的 顶层 元素注释 L是一个表 CAR L 是表L的第一个顶层元素 CDR L 是表L除了第一个顶层元素外的剩余子表 14 8 2递归程序的正确性证明 结构归纳法5 分析 当对Member x L 进行递归调用时 Member x CDR L 的第一个变元不变 但第二个变元CDR L 比L简单 因此 对第二个自变元L所包含顶层元素个数进行归纳 证明 1 证明对于含有0个元素的表L 程序运行正确 此时L NIL 根据程序有 Member x L false 程序运行正确 2 假设对于一切含有N个 N为非负正整数 顶层元素的表L 程序运行正确 即 Member x L true ifx是L 的顶层元素false else 15 8 2递归程序的正确性证明 结构归纳法6 证明对于含有N 1个顶层元素的表L 程序确 N 1 1 L不为NIL 根据程序有 Member x L true ifx CAR L Member x CDR L 否则 1 若x CAR L 则x是L的一个顶层元素 故Member x L true 程序运行正确 2 若x CAR L 则因L不为NIL 所以CDR L 有意义 根据程序Member x L Member x CDR L 16 8 2递归程序的正性证明 结构归纳法7 CDR L 是一个含有N个元素的表 根据假设有 Member x CDR L true ifx是L 的顶层元素 false else Member x L 正确地取值false或true 综上所述 程序是部分正确的 对于终止性 取良序集 N Member的第二个自变元L的长度每递归调用一次都减少 故可以终止 17 8 2递归程序的正性证明 结构归纳法8 结构归纳法小结关键是找出对什么进行归纳 找出 最小 数据对较复杂的数据作出正确假设对负杂数据证明正确性 18 8 2递归程序的正性证明 良序归纳法1 2 良序归纳法步骤 设 W 是一个良序集 P x 是一个命题 为了证明对于所有的x W P x 只要 1 证明P x0 为真 x0是W中 最小 元素 2 归纳假设 假设对于所有的x x P x 为真 在此基础上证明P x 为真 19 8 2递归程序的正性证明 良序归纳法2 例1 证明Ackermann函数A x1 x2 ifx1 0thenx2 1elseifx2 0thenA x1 1 1 elseA x1 1 A x1 x2 1 对任意非负整数对 x1 x2 计算终止 证明 选取良序集 W 其中W x1 x2 x1 0 x2 0 x1 x2是整数 为字典序 设命题P x1 x2 为A x1 x2 计算终止 返回下一页 返回下两页 20 8 2递归程序的正性证明 良序归纳法3 证明 1 对于W中最小元素 0 0 A 0 0 0 1 1 计算终止 即P 0 0 成立 2 归纳假设 假设对于所有的 x1 x2 x1 x2 P x1 x2 为真 在此基础上 证明P x1 x2 为真 分三种情况 a 若x1 0 则 A x1 x2 A 0 x2 x2 1 计算终止 b 若x1 0 x2 0 则 A x1 x2 A x1 1 1 x1 1 1 x1 x2 根据假设 A x1 1 1 计算终止 因而A x1 x2 计算也终止 见程序 21 8 2递归程序的正性证明 良序归纳法4 c 若x1 0 x2 0 则 A x1 x2 A x1 1 A x1 x2 1 根据 最内最左 规则 先计算A x1 x2 1 x1 x2 1 x1 x2 根据假设 A x1 x2 1 计算终止 设其结果为z 又 x1 1 z x1 x2 根据假设 A x1 1 z 计算终止 A x1 x2 计算终止总之 对于任意的对任意非负整数对 x1 x2 计算终止 见程序 22 8 2递归程序的正性证明 良序归纳法5 例2 证明程序GCD1 x y ifx 0thenyelseify xthenGCD1 x y y elseGCD1 x y x 对于x 0 y 0 x 0 y 0 的任意整数对x y是否正确 23 8 2递归程序的正性证明 良序归纳法6 证明 取良序集 W 其中W x y x 0 y 0 x 0 y 0 为字典序 1 对于W中的最小元素 0 1 有 GCD1 0 1 1 根据程序和GCD的性质 程序运行正确 2 假设对于W中 x y x y GCD1 x y 程序运行正确 依此证明对于 x y 程序运行正确 分三种情况 24 8 2递归程序的正性证明 良序归纳法7 1 当x 0时 GCD1 x y GCD1 0 y y 运行正确 2 当x 0 且y0 x y y W又 x 0 y 0 x x y x y y x y GCD1 x y y 不能保证其正常工作 因而GCD1 x y 不能正常工作 所以GCD1 x y 不能正确计算GCD x y 3 当x 0 且y x时 不再考虑 证毕 25 8 2递归程序的正性证明 良序归纳法8 良序归纳法小结选择良序集 根据问题根据证明要求 设计欲证明的命题 正确或终止根据问题和程序 找出最小数据在良序集的二元关系下 给出假定在证明复杂的情况 到底分几种情况讨论 需要根据程序进行 26 8 2递归程序的正性证明 练习 练习1 证明递归程序MacCarthy91函数M x ifx 100thenx 10elseM M x 11 对于所有整数x 其计算结果是 M x x 10 当x 100 91 当 1002 证明递归程序GCD x y ifx 0thenyelseify xthenGCD y x elseGCD x y x 对于满足x 0 y 0 x 0 y 0 的任意整数对x y的正确性 27 8 3程序变换技术 程序变换的基本思想程序变换方法递归向非递归的转换FP函数型程序的代数变换 28 1 程序变换的基本思想 概述程序的等价变换问题 受到越来越多的关注 是程序设计方法学和自动程序设计领域中的重要课题 递归程序变换为非递归程序 1966年Cooper着手研究递归程序的变换问题 Backus提出了函数型程序设计编译程序的目标程序的优化好结构的程序与程序效率间的矛盾 29 1 程序变换的基本思想 续 函数型程序文本 面向问题 注重可读性和正确性 可交付运行的程序文本 面向过程 注重运行效率 程序生成阶段 程序改进阶段 等价变换 P1 P2 在程序生成阶段 先用一种清晰和抽象的语言来描述算法 并在此基础上设计一个面向问题的 易于理解正确的函数型递归程序 此时不考虑效率问题 在程序改进阶段 将通过一系列保证正确性的变换规则 对程序的数据结构和算法进行求精 最终将该程序转换成一个具体的面向过程的且运行效率高的程序文本 30 1 程序变换的基本思想 续 讨论 程序变换的关键是 保证原程序P1和变换得到的程序P2的函数等价 程序变换技术可认为是结构化程序设计的进一步发展 吸取了结构程序设计中的分而治之和逐步求精的思想 可以通过模式识别等人工智能技术自动实现 程序变换技术尚处于发展阶段 尚有一系列的技术难关 31 1 程序变换的基本思想 续 程序变换的层次和过程 纯规范层的变换 由规范引进递归 简化递归 由一般递归向尾递归转换递归到过程型程序的转换过程型程序之间的转换 32 2 程序变换的基本规则 程序变换的实质是 根据一些变换规则把一个程序文本转换成另一个程序文本 而它们是函数等价的 尽管有各种各样的程序 表面上不仅相同 但其结构却具有某些共同的特性 把这些程序归并为某些抽象程序类 程序变换的具体规则通常是针对某类抽象程序而制定的 变换规则是对同一类变换的抽象描述 33 2 程序变换的基本规则 变换规则可表示为 S1S2S1表示输入模式S2表示输出模式B表示可用性条件 若省略 则称为无条件变换 变换一般是单方向的 即从上向下的 用 表示 如果变换是可以互逆 则用双箭头表示 规则的含义 当可用性条件成立时 输入模式S1可以用输出模式S2来代替 B 34 2 程序变换的基本规则 下面的规则可用于递归函数程序的变换规则 它们是由Burstall和Darlington最先引进和讨论的 故也称作B D变换规则 分 基本变换规则定义规则取样规则展开和折叠规则用定律规则抽象规则派生变换规则 35 定义 Defination 规则 f x G x 该规则表示可以根据需要引进新的函数定义 通常f x G x 可以通过其他变换而转换成递归形式 f x F f x 引进新的定义后 G x 就可以用f x 表示 36 取样 Instantiation 规则 f x y G x y f x 0 G x 0 该规则表示可以引进已知函数的一个代换实例 37 展开 Unfolding 折叠Folding规则 F F E S x F F E S x 该规则表示当F 中有某个E x 的一个实例E S x 出现时 则可以展开函数E 而用对应的E S x 代替 若F 中有E x 的一个实例出现时 可用对应的E x 的实例E S x 代替 而形成一个E的调用形式 例如 F x x3 x2 1 g x x3 E E x E x 38 用定律 Law 规则 E E E E 该定律表示如有定律 如交换率 结合率等 可推出E E 则E 和E 可以互换 例如 x x 0 0 a b c a b c a b c 有定律使得E E 39 抽象 Abstraction 规则 E E E E u1 F1 un Fn where ui Fi表示在E 中将所有Fi的出现用ui代替该规则表示可以引进where子句用新标识符抽象出函数中的公共子表达式 例如 IfBthenx E yelsex E yfi z E ifBthenx z yelsex z yfi ui不出现在Fi中 i j 1 n 40 例 斐波那契函数 f x ifx 0orx 1then1elsef x 1 f x 2 fi改写为 1 f 0 1给定2 f 1 1给定3 f x 2 f x 1 f x 给定4 g x 定义5 g 0 取样 展开1 26 g x 1 取样4 展开3 where 抽象 where g x 折叠47 f x 2 u vwhere 抽象 u vwhere g x 折叠4 41 斐波那契函数的新定义 f 0 1f 1 1f x 2 u vwhere g x g 0 g x 1 where g x 这样定义的函数 其计算时间耗费从原来的指数级下降到了线性级 参见运行程序 42 斐波那契数列计算 改进前 F1 x 27 393178115142298320401346269217830935245785702887922746514930352241578173908816963245986102334155 F1 stime seconds 0 0510000 0800000 1200000 2000000 3110000 5200000 8210001 3320002 1640003 4950005 6580009 15300014 821000 43 斐波那契数列计算 改进后 iF2 x 27 403178115142298320401346269217830935245785702887922746514930352241578173908816963245986102334155F2 stime 0 0000000 0000000 0000000 0000000 0000000 0000000 0000000 0000000 0000000 0000000 0000000 0000000 000000 44 B D规则说明 应用这些规则将保证程序正确性使用 折叠 规则有可能损失程序的终止性 例如用F的函数定义折叠F的函数体通过应用定律及抽象 通常可导致效率的改进取样规则和采样规则使效率保持不变假定代换中用到的方程 即函数定义 的参数在某一良序集下小于被变换方程的参数 则折叠规则至少能保持效率 45 应用B D规则的策略 引进任何必要的定义取样对每个取样得到的实例重复进行展开 在每级展开中 试图使用定律和抽象重复折叠说明 定义和取样一般需要有创造性 运用定律和where抽样行则需要进行判断 而展开和重复折叠行是较为机械的操作 46 程序变换系统 一个程序变换系统主要包括 变换规则集 基本的和派生的 直接影响到系统的能力策略和算法 包括应用规则的次序 步骤和方向 影响实现自动化的程度以及适用于在各级层次描述程序的程序语言程序变换系统 英国爱丁堡大学的程序自动变换系统Pop 2西德墨尼黑工业大学的程序变换系统cipBurstall Darlington的递归程序变换系统 47 3 递归程序向非递归程序的转换 一 尾递归型程序二 Copper变换三 改进的Copper变换四 其他变换 48 一 尾递归型程序 1 定义 如果递归程序中 含有递归调用的分支只递归调用一次 且都以递归调用结束 则将这类递归程序称为尾递归程序 它可以直接转换成迭代程序 它是一类具有特殊结构的递归程序 2 例 求两个非负整数x和y的最大公约数GCD2 x y ifx 0thenyelseGCD2 rem y x x 其中 rem y x 表示y除以x的余数 它转换成的非递归程序如下 49 一 尾递归型程序 intGCD2 x y Beginread x y L ifx 0thengotoL1 elsex y rem y x x gotoL L1 write y End 50 一 尾递归型程序 3 尾递归程序的转换模式F u ifp u theng u elseF h u read u L ifp u thenwrite g u elseu h u gotoL fi 51 二 Cooper变换 如何将递归程序转换成尾递归程序 1966年 Cooper提出了一种具体的等价变换 称为Cooper变换Cooper变换的思想 引入一个新变量 以便改变原递归算法的运算结构 从而把一类非递归程序归结为等价的尾递归程序 52 二 Cooper变换 输入模式f x ifb x thenh x elseF f k x g x 输出模式f x G x e G x y ifb x thenF h x y elseG k x F g x y 其中 x k Type1 k x xy G h g f F Type2b booleane F的右单位元 即F x e x 可用性条件F满足结合律 F F x y z F x F y z F有右单位元b h g h中不含有f 53 二 Cooper变换 例 阶乘函数FAC n 输入模式 FAC n ifn 1then1elsen FAC n 1 其中 b n n 1 h n 1 k n n 1 g n n F x y x y 取良序关系为通常的小于关系 n 1 n k n n可以验证 F x y x y满足结合律 F的右单位元为1b h g k中不含有FAC因此满足Cooper变换规则的可用性条件 有输出模式 54 二 Cooper变换 输出模式 FAC n G n 1 G x y ifx 1thenyelseG x 1 x y G x y 是一个尾递归型程序例 FAC 4 G 4 1 G 3 4 1 G 2 3 4 1 G 1 2 3 4 1 24 输入模式f x ifb x thenh x elseF f k x g x 输出模式f x G x e G x y ifb x thenF h x y elseG k x F g x y 其中 x k Type1 k x xy G h g f F Type2b booleane F的右单位元 即F x e x 输入模式 FAC n ifn 1then1elsen FAC n 1 其中 b n n 1 h n 1 k n n 1 g n n F x y x y 55 二 Cooper变换 引理1 G x y F f x y 证明 通过结构归纳法证明 1 当b x 为true时 G x y F h x y 输出模式 F f x y 输入模式 引理成立当b x 为false时 设 t x 引理成立 即G t y F f t y 可用条件有k x x 有 G x y G k x F g x y 输出模式 F f k x F g x y 假设 F F f k x g x y 结合律 F f x y 输入模式 综上所述 引理成立 56 二 Cooper变换 定理 Cooper变换的输出模式等价于输入模式 证明 由输出模式得 f x G x e ifb x thenF h x e elseG k x F g x e 输出模式 ifb x thenh x elseG k x g x e为F的右元 ifb x thenh x elseF f k x g x 引理1 57 二 Cooper变换 小结 Cooper变换的约束条件很强 3个可用条件 可用性条件2 即F具有右单位元e 是为了保证在一开始b x 就为真时变换的正确性 将上述输出模式增加一个分支 将上述情况预先分离 另做处理 则可用条件2可以略去 这样可以得到改进的Cooper变换 58 三 Cooper变换的改进型 将Cooper变换的可用性条件2省略输入模式 f x ifb x thenh x elseF f k x g x 输出模式f x ifb x thenh x elseG k x g x G x y ifb x thenF h x y elseG k x F g x y 其中 x k Type1 k x x y G h g f F Type2 b boolean 可用性条件 F满足结合律 F F x y z F x F y z b h g h中不含有f 59 三 Cooper变换的改进型 例 阶乘函数FAC n 输入模式 FAC n ifn 1then1elsen FAC n 1 可以验证其满足改进型Cooper变换的可用性条件输出模式 FAC n ifn 1then1elseG n 1 n G x y ifx 1thenyelseG x 1 x y 例 FAC 4 G 3 4 G 2 3 4 G 1 2 3 4 24特点 改进的Cooper变换只能处理含有一个递归分支的情形 可把它推广到含有多个递归分支的情形 但每个分支的运算相同 即形成拓广的Cooper变换 60 四 其它变换 T1变换可以处理一类含有两个递归分支 具有两种函数运算的递归程序 但分支条件中不能含有递归调用 例 f x1 x2 1 ifx2 0f x1 x2 1 x2 ifx2 x1f x1 1 x2 x1 ifx2 x1T2变换可以处理一类含有两个递归分支 具有两种函数运算的递归程序 且分支条件中可以含有递归调用 C变