第六课 递归程序的正确性证明.ppt

本课的内容 1.递归程序概述 2.简化的递归程序模型 3.递归程序的计算规则 4.递归程序的正确性证明 结构归纳法 良序归纳法 递归程序的一种模型 递归程序f(x1,x2,……,xn)可以描述为 其中，pi(i=1,2,….m)是测试谓词，Ei(i=1,2,…..m+1)是表达式。 递归程序的一种模型 这种函数型递归程序的基本含义是 为了计算自变元为(x1,x2,…,xn)的递归函数F(x1,x2…,xn)的值，先测试P1的值，若P1为真，则F的值为E1的值；若P1为假，则接下去测试P2，若P2为真，则F的值为E2的值。 按这种方式继续进行测试，直至找到第一个为真的Pi,，这时F的值为相应的Ei的值。倘若没有一个Pi(i=1,2,…m)为真，则F的值规定为Em+1的值。 这里所谓的递归，是指F可以在Ei和Pi中出现，这种出现称为F的递归调用。 递归程序的例子… 例１ 阶乘函数 F(x)?if x=1 then 1 else x*F(x-1) 其中，x为任意正整数。 现在就自变元x的某个具体值(例如x=4)来考察一下 F(x)的计算过程。 F(4)=4*f(3)=4*3*f(2)=4*3*2*f(1)=4*3*2*1=4!=24 可以证明，对任意正整数x有 F(x)=x! 递归程序的例子… 例２求非负整数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) 其中，x0,y0,且x,y不同时为零。 可以证明GCD(x,y)确实计算了x和y的最大公约数。例如: GCD(8,4)= GCD(4,8)= GCD(4,4) = GCD(4,0)= GCD(0,4)=4 递归计算的计算规则 计算A(1,2)的上述两种计算过程虽然不同，但却导致相同的结果，即A(1,2)＝4. 可以证明：就同一个递归程序而言，如果对相同的自变元采用不同的计算过程，只要计算过程都终止，则所得结果将是相同的。 但是，可能出现这样的情况，一个计算过程不终止，而另一个计算过程却将终止。下面的例子就能说明这点。 递归程序的计算规则 上述讨论表明： (1)??递归程序可以采用不同的计算规则来进行计算； (2)??采用不同的计算规则来计算递归程序时，对相同的变元，计算过程可能终止，也可能不终止； (3)??如果对于不同的计算规则，相应的递归程序(对相同的自变元)的计算过程都终止，则它们所得的结果一定相同； (4)?? 在(3)的情况下，因为计算过程不同，所以虽然得到的结果相同，但其效率(计算时间和存储量)却可能差别大。 递归程序的计算规则 总之，在递归程序的执行过程中，计算规则的选取是很重要的。本章及后面的章节中，将统一规定： 采用”最左，最内”的计算规则，即在计算过程中，总是先计算最内层的F中最左的一个。 例如，在例6中，计算A(1,2)的第一种计算顺序就是按”最左，最内”的计算规则进行的。但在例7中，按”最左，最内”的计算规则去计算F(1,2)却是不终止的，故不能认为F(1,2)＝0. 虽然”最左，最内”的规则未必是最佳的，但现今具有处理递归调用功能 的程序设计语言大都采用这种计算规则。 采用不同计算规则结果不同的例子 F(x1,x2): if x1=0 then 0 else F(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中的有关规定是相似的。不过为了讨论方便起见，我们对LISP语言做了很大的简化，即下面所讨论的只是一种简化的LISP程序。 原子和表 简化的LISP程序中，基本的数据结构是原子和表 原子是指字母和数字组成的字符串，且字符之间不允许出现空格并约定原子必须以字母A,B,C,D,E之一打头，而以其他字母打头的均指变量。 表是指由表元素组成的集合 表元素之间用空格隔开 整个集合用一对方括号［］括起来 表元素可以是原子或其他表(在后面的一些例子中，有时也用数字作为表元素) NIL表示