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

1,第8章 递归程序设计及其正确性证明,1. 概述 2. 递归程序的正确性证明 3. 递归程序向非递归程序的转换 4. 函数型程序设计简介,2,8.1 概述,1. 迭代与递归 递归的概念 一个函数、过程或者数据结构,如果在他们的定义内部又出现了定义本身的应用, 则称这个函数、过程或者数据结构是递归的,或者是递归定义的. 直接递归：若程序P包含着对自己的引用，则称为是直接递归的 间接递归：若程序P包含着对另一程序Q的引用，而Q又直接或间接地引用P，则称为间接递归。 例：,3,8.1 概述,递归的概念（续） int fact(int n) if (n=0) return 1; else return n*fact(n-1); ,Procedure B; Procedure C Begin Begin C; B; End; End;,4,8.1 概述,递归实质是一种循环结构，他把较复杂情形的计算逐次地归结为“较简单”情形的计算，一直归结到“最简单”情形的计算，并得到计算结果为止。 每个迭代程序原则上总可以转换成与它等价的递归程序；反之不然，并不是每个递归程序都可以转换成与他等价的迭代程序。 递归程序的效率(时间和空间效率)比迭代程序低。 递归程序较容易理解和阅读、实现直观,5,8.1 概述,2. 递归程序的一种模型 一种简化的函数递归程序模型的一般形式如下： F(x1,x2,xn) if p1 then E1 else if p2 then E2 else if pm then Em else Em+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) if x=0 then y else if yx then GCD(y,x) else GCD(x,y-x) 其中，x,y0,且不同时为0。 例2：计算Fibonacci函数 F(x) if x=0 then 0 else if x=1 then 1 else F(x-1)+F(x-2) 其中，x为非负整数。,7,8.1 概述,3. 递归计算的计算规则 例1. F(x1,x2) if x1=0 then 0 else F(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) if x1=0 then x2+1 else if x2=0 then A(x1-1,1) else A(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) if x=1 then 1 else x*F(x-1) 其中，x是大于0的整数。 要证明对于所有正整数x，F(x)=x! 该程序的规范为： P(x): x0 Q(x,z) : z = x!,12,8.2 递归程序的正确性证明-结构归纳法3,证明： 1) 当x=1时，根据程序F(x)=1=1!,正确。 2) 假设,对任意的正整数x，F(x) = x!成立， 则对于x+1有： x 是正整数 x+11 根据程序 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) if L=NIL then false else if x=CAR(L) then TRUE else Member(x, CDR(L) 的正确性（对于任意的原子（或表）和表L。即证明： Member(x,L) = false , if x不是L的元素 true , if x 是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 , if x是L的顶层元素 false, else,15,8.2 递归程序的正确性证明-结构归纳法6,证明对于含有N+1个顶层元素的表L，程序确： N+11 L不为NIL， 根据程序有： Member(x,L) = true, if x=CAR(L) = Member(x,CDR(L) , 否则 （1）若x=CAR(L)，则x是L的一个顶层元素，故Member(x,L) = true，程序运行正确； （2）若xCAR(L)，则因L不为NIL，所以CDR(L)有意义 根据程序 Member(x,L) = Member(x,CDR(L),16,8.2 递归程序的正性证明-结构归纳法7,CDR(L)是一个含有N个元素的表，根据假设有： Member(x, CDR(L) = true , if x是L的顶层元素 = false, else Member(x, L) 正确地取值false或true. 综上所述，程序是部分正确的。 对于终止性：取良序集（N,）, Member的第二个自变元L的长度每递归调用一次都减少，故可以终止。,17,8.2 递归程序的正性证明-良序归纳法1,2. 良序归纳法 步骤： 设(W，-)是一个良序集，P(x)是一个命题，为了证明对于所有的xW，P(x), 只要： （1）证明P(x0)为真，x0是W中“最小”元素； （2）归纳假设：假设对于所有的x-x, P(x)为真，在此基础上证明P(x)为真。,18,8.2 递归程序的正性证明-良序归纳法2,例1：证明Ackermann函数 A(x1,x2) if x1=0 then x2+1 else if x2=0 then A(x1-1,1) else A(x1-1,A(x1,x2-1) 对任意非负整数对(x1,x2) 计算终止. 证明：选取良序集(W,-), 其中W=(x1,x2)|x10x2 0 x1,x2是整数， -为字典序。 设命题 P(x1,x2)为A(x1,x2) 计算终止。,返回下一页,返回下两页,19,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)计算也终止,见程序,20,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) 计算终止.,见程序,21,8.2 递归程序的正性证明-良序归纳法5,例2：证明程序 GCD1(x,y) if x=0 then y else if yx then GCD1(x-y,y) else GCD1(x,y-x) 对于x0y0(x0y 0)的任意整数对x,y是否正确？,22,8.2 递归程序的正性证明-良序归纳法6,证明 ：取良序集(W,-), 其中W=(x,y)| x0y0(x0y 0), -为字典序。 1）对于W中的最小元素(0,1)有， GCD1(0,1) = 1 (根据程序和GCD的性质) 程序运行正确。 2）假设对于W中 (x,y)-(x,y), GCD1(x,y)程序运行正确，依此证明对于（x,y）程序运行正确，分三种情况:,23,8.2 递归程序的正性证明-良序归纳法7,(1) 当x=0时， GCD1(x,y) = GCD1(0,y) = y, 运行正确 (2) 当x0，且y0 (x-y,y)W 又x0 y0 x x-y (x-y,y) -(x,y) GCD1(x-y,y) 不能保证其正常工作。 因而GCD1(x,y)不能正常工作。 所以GCD1(x,y)不能正确计算GCD(x,y). (3) 当x0，且yx时，(不再考虑) 证毕,24,8.2 递归程序的正性证明-练习,练习 1. 证明递归程序MacCarthy91函数 M(x) if x100 then x-10 else M(M(x+11) 对于所有整数x，其计算结果是： M(x) = x-10 , 当x100 = 91 , 当100 2. 证明递归程序 GCD(x,y) if x=0 then y else if yx then GCD(y,x) else GCD(x,y-x) 对于满足x0y0(x0y 0)的任意整数对 x,y的正确性,25,8.3 程序变换技术,程序变换的基本思想 程序变换方法 递归向非递归的转换 FP函数型程序的代数变换,26,1. 程序变换的基本思想,概述 程序的等价变换问题，受到越来越多的关注，是程序设计方法学和自动程序设计领域中的重要课题。 递归程序变换为非递归程序。1966年Cooper着手研究递归程序的变换问题。 Backus提出了函数型程序设计 编译程序的目标程序的优化 好结构的程序与程序效率间的矛盾,27,1. 程序变换的基本思想（续）,函数型程序文本 （面向问题） 注重可读性和正确性,可交付运行的程序文本 （面向过程） 注重运行效率,程序生成阶段：,程序改进阶段：,等价 变换,P1,P2,在程序生成阶段，先用一种清晰和抽象的语言来描述算法，并在此基础上设计一个面向问题的、易于理解正确的函数型递归程序，此时不考虑效率问题。 在程序改进阶段，将通过一系列保证正确性的变换规则，对程序的数据结构和算法进行求精，最终将该程序转换成一个具体的面向过程的且运行效率高的程序文本。,28,1. 程序变换的基本思想（续）,讨论： 程序变换的关键是：保证原程序P1和变换得到的程序P2的函数等价。 程序变换技术可认为是结构化程序设计的进一步发展：吸取了结构程序设计中的分而治之和逐步求精的思想。 可以通过模式识别等人工智能技术自动实现。 程序变换技术尚处于发展阶段，尚有一系列的技术难关。,29,1. 程序变换的基本思想（续）,程序变换的层次和过程： 纯规范层的变换：由规范引进递归； 简化递归：由一般递归向尾递归转换 递归到过程型程序的转换 过程型程序之间的转换,30,2. 程序变换的基本规则,程序变换的实质是：根据一些变换规则把一个程序文本转换成另一个程序文本，而它们是函数等价的。 尽管有各种各样的程序，表面上不仅相同，但其结构却具有某些共同的特性。把这些程序归并为某些抽象程序类。 程序变换的具体规则通常是针对某类抽象程序而制定的。 变换规则是对同一类变换的抽象描述。,31,2. 程序变换的基本规则,变换规则可表示为： S1 S2 S1 表示输入模式 S2 表示输出模式 B 表示可用性条件，若省略，则称为无条件变换。变换一般是单方向的，即从上向下的，用“”表示，如果变换是可以互逆，则用双箭头表示。 规则的含义：当可用性条件成立时，输入模式S1可以用输出模式S2来代替。,B,32,2. 程序变换的基本规则,下面的规则可用于递归函数程序的变换规则，它们是由Burstall 和Darlington最先引进和讨论的，故也称作B&D变换规则，分： 基本变换规则 定义规则 取样规则 展开和折叠规则 用定律规则 抽象规则 派生变换规则,33,定义（Defination）规则,f(x) G(x) 该规则表示可以根据需要引进新的函数定义。通常f(x) G(x)可以通过其他变换而转换成递归形式： f(x) F(f(x) 引进新的定义后，G(x)就可以用f(x)表示,34,取样(Instantiation)规则,f(x,y) G(x,y) f(x,0) G(x,0) 该规则表示可以引进已知函数的一个代换实例,35,展开（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的调用形式。, E: E(x) E(x),36,用定律（Law）规则,E E E E” 该定律表示如有定律（如交换率、结合率等）可推出E=E”，则E和E”可以互换，例如： （x）x*0 = 0 （a,b,c）a*(b*c) = (a*b)*c,有定律使得E=E”,37,抽象（Abstraction）规则,E E E Eu1/F1, un/Fn where = ui/Fi表示在E中将所有Fi 的出现用ui代替 该规则表示可以引进where子句用新标识符抽象出函数中的公共子表达式，例如： If B then x:=E*y else x:=E+y fi z:=E; if B then x:=z*y else x:=z+y fi,ui不出现在Fi中, i, j = 1,n,38,例：斐波那契函数,f(x) if x=0 or x=1 then 1 else f(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,2 6）g(x+1) 取样4 展开3 where = 抽象 where = g(x) 折叠4 7) f(x+2) u+v where = 抽象 u+v where = g(x) 折叠4,39,斐波那契函数的新定义,f(0) 1 f(1) 1 f(x+2) u+v where = g(x) g(0) g(x+1) where = g(x) 这样定义的函数，其计算时间耗费从原来的指数级下降到了线性级。 参见运行程序。,40,斐波那契数列计算（改进前）,F1:x=2739 317811 514229 832040 1346269 2178309 3524578 5702887 9227465 14930352 24157817 39088169 63245986 102334155 F1s time: 0.051 0.080 0.12 0.200 0.311 0.52 0.821 1.332 2.164 3.495 5.658 9.153 14.821,41,斐波那契数列计算（改进后）,iF2: x=2740 317811 514229 832040 1346269 2178309 3524578 5702887 9227465 14930352 24157817 39088169 63245986 102334155 F2s time: 0.000000 0.000000 0.000000 0.000000 0.000000 0.000000 0.000000 0.000000 0.000000 0.000000 0.000000 0.000000 0.000000,42,B&D规则说明,应用这些规则将保证程序正确性 使用“折叠”规则有可能损失程序的终止性，例如用F的函数定义折叠F的函数体 通过应用定律及抽象,通常可导致效率的改进 取样规则和采样规则使效率保持不变 假定代换中用到的方程（即函数定义）的参数在某一良序集下小于被变换方程的参数，则折叠规则至少能保持效率,43,应用B&D规则的策略,引进任何必要的定义 取样 对每个取样得到的实例重复进行展开，在每级展开中： 试图使用定律和抽象 重复折叠 说明：定义和取样一般需要有创造性，运用定律和where抽样行则需要进行判断，而展开和重复折叠行是较为机械的操作。,44,程序变换系统,一个程序变换系统主要包括： 变换规则集（基本的和派生的）：直接影响到系统的能力 策略和算法（包括应用规则的次序、步骤和方向）：影响实现自动化的程度 以及适用于在各级层次描述程序的程序语言 程序变换系统： 英国爱丁堡大学的程序自动变换系统Pop-2 西德墨尼黑工业大学的程序变换系统cip Burstall & Darlington的递归程序变换系统,45,3. 递归程序向非递归程序的转换,一. 尾递归型程序 二. Copper变换 三.改进的Copper变换 四. 其他变换,46,一、 尾递归型程序,1. 定义：如果递归程序中，含有递归调用的分支只递归调用一次，且都以递归调用结束，则将这类递归程序称为尾递归程序。它可以直接转换成迭代程序。它是一类具有特殊结构的递归程序。 2. 例：求两个非负整数x和y的最大公约数 GCD2(x,y) if x=0 then y else GCD2(rem(y,x),x) 其中，rem(y,x)表示y除以x的余数。 它转换成的非递归程序如下：,47,一、 尾递归型程序,int GCD2(x,y) Begin read(x,y); L: if x=0 then goto L1; else x,y rem(y,x),x; goto L; L1: write(y); End;,48,一、 尾递归型程序,3. 尾递归程序的转换模式 F(u) if p(u) then g(u) else F(h(u) read(u); L: if p(u) then write(g(u); else uh(u); goto L fi;,49,二、 Cooper 变换,如何将递归程序转换成尾递归程序？ 1966年，Cooper提出了一种具体的等价变换，称为Cooper变换 Cooper变换的思想：引入一个新变量，以便改变原递归算法的运算结构，从而把一类非递归程序归结为等价的尾递归程序。,50,二、 Cooper 变换,输入模式 f(x) if b(x) then h(x) else F(f(k(x),g(x) 输出模式 f(x) G(x,e) G(x,y) if b(x) then F(h(x),y) else G(k(x),F(g(x),y) 其中，x , k : Type 1, k(x) -x y,G,h,g,f,F : Type2 b : boolean e: F的右单位元，即F(x,e)=x,可用性条件 F满足结合律：F(F(x,y),z)=F(x,F(y,z) F有右单位元 b, h, g, h 中不含有f,51,二、 Cooper 变换,例：阶乘函数FAC(n) 输入模式： FAC(n) if n=1 then 1 else n*FAC(n-1) 其中， b(n) : n=1, h(n)=1, k(n)=n-1, g(n)=n, F(x,y) = x*y; 取良序关系为通常的小于关系 n-1n k(n)n 可以验证： F(x,y) = x*y 满足结合律； F 的右单位元为1 b,h,g,k中不含有FAC 因此满足Cooper变换规则的可用性条件，有输出模式：,52,二、 Cooper 变换,输出模式： FAC(n) G(n,1) G(x,y) if x=1 then y else G(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) if b(x) then h(x) else F(f(k(x),g(x) 输出模式 f(x) G(x,e) G(x,y) if b(x) then F(h(x),y) else G(k(x),F(g(x),y) 其中，x , k : Type 1, k(x) -x y,G,h,g,f,F : Type2 b : boolean e: F的右单位元，即F(x,e)=x,输入模式： FAC(n) if n=1 then 1 else n*FAC(n-1) 其中， b(n) : n=1, h(n)=1, k(n)=n-1, g(n)=n, F(x,y) = x*y;,53,二、 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) (输入模式) 综上所述，引理成立,54,二、 Cooper 变换,定理：Cooper变换的输出模式等价于输入模式。 证明：由输出模式得： f(x) = G(x,e) = if b(x) then F(h(x),e) else G(k(x),F(g(x),e)(输出模式) = if b(x) then h(x) else G(k(x),g(x) (e为F的右元) = if b(x) then h(x) else F(f(k(x),g(x) (引理1),55,二、 Cooper 变换,小结： Cooper变换的约束条件很强（3个可用条件）； 可用性条件2，即F具有右单位元e，是为了保证在一开始b(x)就为真时变换的正确性。 将上述输出模式增加一个分支，将上述情况预先分离，另做处理，则可用条件2可以略去。这样可以得到改进的Cooper变换,56,三、 Cooper 变换的改进型,将Cooper变换的可用性条件2省略 输入模式： f(x) if b(x) then h(x) else F(f(k(x),g(x) 输出模式 f(x) if b(x) then h(x) else G(k(x),g(x) G(x,y) if b(x) then F(h(x),y) else G(k(x),F(g(x),y) 其中，x,k :Type 1, 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,57,三、 Cooper 变换的改进型,例： 阶乘函数FAC(n) 输入模式： FAC(n) if n=1 then 1 else n*FAC(n-1) 可以验证其满足改进型Cooper 变换的可用性条件 输出模式： FAC(n) if n=1 then 1 else G(n-1,n) G(x,y) if x=1 then y else G(x-1, x*y) 例：FAC(4) = G(3,4) =G(2,3*4)=G(1,2*3*4)=24 特点：改进的Cooper变换只能处理含有一个递归分支的情形，可把它推广到含有多个递归分支的情形，但每个分支的运算相同，即形成拓广的Cooper 变换,58,四、 其它变换,T1变换 可以处理一类含有两个递归分支，具有两种函数运算的递归程序,但分支条件中不能含有递归调用。例： f(x1,x2) = 1 , if x2=0 f(x1,x2-1)+x2 , if x2x1 f(x1-1,x2)*x1 , if x2=x1 T2变换 可以处理一类含有两个递归分支，具有两种函数运算的递归程序, 且分支条件中可以含有递归调用。 C变换：针对一类特殊的递归 RR变换：二重递归调用 例 f(