第7章 递归程序的正确性证明

第7章递归程序及其正确性证明本课的内容1.递归程序概述2.简化的递归程序模型3.递归程序的计算规则4.递归程序的正确性证明结构归纳法良序归纳法递归与迭代程序在程序设计中，处理重复性的计算常采用的方法是组织迭代循环和采用递归计算的方法，后者特别是在非数值领域中更是如此。可以证明每个迭代程序原则上总可以转换成与它等价的递归程序；反之不然，并不是每个递归程序都可以转换成与它等价的迭代程序。就效率而言，递归程序的实现往往比迭代程序耗费更多的时间与存储空间。在具体实现时，又希望尽可能把递归程序转化成等价的迭代程序，从而提高程序的时空效率。1.递归程序概述递归是常用的编程技术，其基本思想是“自己调用自己”。数学上最常见、最简单的递归问题就是自然数的阶乘。n=1n!=1;n1n!=n*(n-1)!;适合用递归方法求解的问题有一个初始状态后续的情况可由前面的状态推出如Fibonacci数列F1=F2=1;Fn=Fn-1+Fn-21.递归程序概述直接或间接调用自身的程序称为递归程序。递归实质上也是一种循环结构，它把“较复杂”情况的计算归结为“较简单”情况的计算，一直归结到“最简单”情况的计算为止。在数值计算领域可以采用递归计算，在非数值领域使用也非常广泛。例如：河内塔（HanoiTower）问题8皇后问题骑士巡游问题此外，递归是人工智能语言Lisp/Prolog等进行问题求解的基本手段。2.一种简化的递归程序模型递归程序f(x1,x2,……,xn)可以描述为f(x1,x2,……,xn)≡Ifp1thenE1elseifp2thenE2……elseifpmthenEmelseEm+1其中pi和Ei中含有f。递归程序的例子计算最大公约数GCD(x,y):ifx=0thenyelseifyxthenGCD(y,x)elseGCD(x,y-x)GCD(8,4)=GCD(4,8)=GCD(4,4)=GCD(4,0)=GCD(0,4)=4计算F(x,y)=xyify=0then1elseifeven(y)thenF(x*x,y/2)elseF(x,y-1)*xF(4,3)=F(4,2)*4=F(16,1)*4=F(16,0)*64=1*64=64;递归程序的例子－多重递归计算McCarthy91函数M(x)ifx100thenx-10elseM(M(x+11))例如：M(105)=95M(99)=M(M(110))=M(100)=M(M(111))=M(101)=91递归程序－多重递归Ackermann函数A(x1,x2)Ifx1=0thenx2+1elseifx2=0thenA(x1-1,1)elseA(x1-1,A(x1,x2-1))计算方法2(最内层调用)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采用两种方法计算：A(1,2)计算方法1(最外层调用)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)+1)+1=(2+1)+1=43.递归程序的计算规则上例说明：1.递归程序可以采用不同的规则来计算。2.理论上已经证明，如果同一个递归程序的不同计算规则都终止，那么结果一定也相同。3.不同的计算过程虽然结果相同，但是时间复杂度和空间复杂度往往不同；实际工作的编译器往往使用“最左最内”规则。（总是先计算最内层的最左的一个）4.采用不同的计算规则来计算递归程序时，对相同的子变元，计算过程可能终止，也可能不终止。采用不同计算规则结果不同的例子F(x1,x2):ifx1=0then0elseF(0,F(x1,x2))先计算最外层调用F(1,2)=F(0,F(1,2))=0先计算最内层调用F(1,2)=F(0,F(1,2))=F(0,F(0,F(1,2)))=……简化LISP语言简化的LISP程序中做如下规定。１．基本的数据结构是原子和表(1)原子是指字母和数字组成的字符串，且字符之间不允许出现空格，并约定原子必须以字母A,B,C,D,E之一打头，而以其他字母打头的均指变量。(2)表是指由表元素组成的集合，表元素之间用空格隔开，整个集合用一对方括号［］括起来，表元素可以是原子或其他表。NIL表示空表。例，①［ABC］——具有３个表元素的表②[A[BA1[C]]D]——具有３个（顶层）表元素的表，其中A和D均为原子，［BA1[C]］是一个表，该表的第３个表元素［C］又是一个表。简化LISP语言五种基本函数1.“=”测试函数功能:检查两个原子或表是否相同，若相同，其值为true，否则其值为false。A=A为true[AB]=[AB]为true[AB]=[BA]为false[AB]=[A[B]]为false2.原子测试函数ATOM(x)功能:检查自变元x是否为原子或空表，若是，其值为true，否则，取值为false。ATOM(A)为trueATOM(NIL)为trueATOM([AB])为falseATOM([A])为false简化LISP语言3.函数CAR(L)功能:提取表的第一个元素，返回原子或者表。CAR([ABC])=ACAR([[AB]C])=[AB]CAR(A)和CAR(NIL)无定义4.函数CDR(L)功能:取删除表头元素后，余下的元素所组成的表。CDR([ABC])=[BC]CDR([A[BC]])=[[BC]]CDR([[AB]C])=[C]CDR([A])=NILCDR(A)与CDR(NIL)均无定义5.函数CONS(x，L)功能:将x加到表L中，作为表头元素得到的新表。CONS(A，[BC])=[ABC]CONS([A]，[BC])]=[[A]BC]CONS(A，B)无定义基于简化LISP语言的递归例子例1：求一个表L中的最大元素MAX(L):ifCDR(L)=NILthenCAR(L)elseifCAR(L)MAX(CDR(L))thenCAR(L)elseMAX(CDR(L))MAX([2564])=MAX([564])=MAX([64])=6基于简化LISP语言的递归例子例2：判断x是否是表L中的某个(顶层)元素MEMBER(x,L)：IfL=NILthenfalseelseifx=CAR(L)thentrueelseMEMBER(x,CDR(L))MEMBER(C,[ABCD])MEMBER(C,[AB[C]])=MEMBER(C,[BCD])=MEMBER(C,[B[C]])=MEMBER(C,[CD])=MEMBER(C,[[C]])=True=MEMBER(C,NIL)=False基于简化LISP语言的递归例子例3:将表L1和表L2合并成一个新表，且L1的元素置L2之前的递归程序APPEND(L1,L2):ifL1=NILthenL2elseCONS(CAR(L1),APPEND(CDR(L1),(L2)))例如：APPEND([AB],[CD])=CONS(A,APPEND([B],[CD]))=CONS(A,CONS(B,APPEND(NIL,[CD])))=CONS(A,CONS(B,[CD]))=CONS(A,[BCD])=[ABCD]请注意APPEND和CONS的区别：CONS([AB],[CD])=[[AB]CD]APPEND([AB],[CD])=[ABCD]4.递归程序的正确性证明思路：（1）证明对于“最简单”的数据，程序运行正确；（2）假设对于“较简单”的数据，程序运行正确[“归纳假设”]，在此基础上证明对于“较复杂”的数据，程序亦运行正确。注：其中的“数据”可以是一般的数值，也可以是由数值、原子或表等组成的某种数据结构。这种证明递归程序正确性的基本思想与通常的数学归纳法是很类似的－－结构归纳法。结构归纳法例1，求阶乘的递归程序F(x)：ifx=1then1elsex*F(x-1)证明：（对于所有正整数x,F(x)=x!）输入、输出断言为：I(x):x0(x为正整数)、O(x,z):z=x!。对正整数x进行归纳：（1）x=1时，F(1)=1=1!（2）归纳假设。设对任意正整数x，F(x)=x!。x是正整数，所以x+1=1为假，根据程序有F(x+1)=(x+1)*F((x+1)-1)=(x+1)*F(x)=(x+1)*x!（根据归纳假设）=(x+1)!程序的部分正确性得到了证明。结构归纳法在以上的归纳证明中，是对程序所操作的变量(正整数)进行归纳，然而许多程序并没有明确可归纳的整数，因此在大多数时候，需要对程序的数据结构进行归纳，这也是结构归纳法和一般的数学归纳法的区别所在。结构归纳法例2，将表L1和表L2合并为一个新表，且L1的元素置L2之前的递归程序APPEND(L1,L2)：ifL1=NILthenL2elseCONS(CAR(L1),APPEND(CDR(L1),L2))证明：对第一个自变元所包含元素的个数进行归纳。（1）证明对于含有0个元素的L1，程序运行正确。当L1=NIL时，APPEND(NIL,L2)=L2程序运行正确结构归纳法（2）归纳假设：假设对于任何含有N个元素的表L1’，程序运行正确，即APPEND(L1’,L2)是由L1’的元素后跟L2的元素组成的表。对于含有N+1个元素的表L1：设L1＝[l1l2…lN+1]，L2＝[l’1l’2…l’M]由于N+10，则APPEND(L1,L2)＝CONS(CAR(L1),APPEND(CDR(L1),(L2)))＝CONS(l1,APPEND(CDR(L1),(L2))结构归纳法由归纳假设，APPEND(CDR(L1),(L2))＝[l2…lN+1l’1l’2…l’M]所以CONS(l1,APPEND(CDR(L1),(L2))＝[l1l2…lN+1l’1l’2…l’M]良序归纳法良序归纳法是一种较强形式的结构归纳法，适合更为复杂的递归程序证明设(W,)是一个良序集，P(x)是一个命题，为了证明对于所有的x∈W，P(x)为真，只要1.证明P(x0)为真，其中x0是W中的“最小”元素2.归纳假设：对于所有的x’x，P(x’)都为真，在此基础上证明P(x)为真良序归纳法例1，证明Ackermann函数的正确性A(x1,x2):ifx1=0thenx2+1elseifx2=0thenA(x1-1,1)elseA(x1-1,A(x1,x2-1))对于任何非负整数对（x1,x2）计算终止。1.本例中，x1,x2在程序中都不断的减小，其中x2是在内层调用中减小。2.选取良序集（W,），其中W={(x1,x2)}，x1,x2是非负整数，为字典顺序。3.定义命题P(x1,x2)：A(x1,x2)计算终止。良序归纳法证明：1.对于W中的最小元素(0,0)，P(x1,x2)终止；2.如果，对于所有的(x1’,x2’)(x1,x2)，P(x1’,x2’)为真，在此基础上证明P(x1,x2)为真。对于W中的最小元素(0,0)，由于A(0,0)＝0＋1＝1，计算显然终止，因此，P(0,0)成立良序归纳法假设所有的(x1’,x2’)(x1,x2)，P(x1’,x2’)为真，在此基础上证明P(x1,x2)为真。1.当x1=0,x2≠0时，A(x1,x2)＝A(0,x2)＝x2+1，程序终止，命题成立；2.当x1≠0,x2=0时，A(x1,x2)＝A(x1,0)＝A(x1-1,1)，由于（x1-1,1）(x1,x2)，根据假设可知，命题成立；3.当x1≠0,x2≠0时，A(x1,x2)=A(x1-1,A(x1,x2-1)),按照“最内最左”原则，先计算A(x1,x2-1)，由于(x1,x2-1)(x1,x2),故z=A(x1,x2-1)终止；又由于(x1-1,z)(x1,x2)，所以A((x1-1),z）终止；因此A(x1,x2)也终止，命题成立。良序归纳法例