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

第7章递归程序及其正确性证明 本课的内容 1 递归程序概述2 简化的递归程序模型3 递归程序的计算规则4 递归程序的正确性证明结构归纳法良序归纳法 递归与迭代程序 在程序设计中 处理重复性的计算常采用的方法是组织迭代循环和采用递归计算的方法 后者特别是在非数值领域中更是如此 可以证明每个迭代程序原则上总可以转换成与它等价的递归程序 反之不然 并不是每个递归程序都可以转换成与它等价的迭代程序 就效率而言 递归程序的实现往往比迭代程序耗费更多的时间与存储空间 在具体实现时 又希望尽可能把递归程序转化成等价的迭代程序 从而提高程序的时空效率 1 递归程序概述 递归是常用的编程技术 其基本思想是 自己调用自己 数学上最常见 最简单的递归问题就是自然数的阶乘 n 1n 1 n 1n n n 1 适合用递归方法求解的问题有一个初始状态后续的情况可由前面的状态推出如Fibonacci数列F1 F2 1 Fn Fn 1 Fn 2 1 递归程序概述 直接或间接调用自身的程序称为递归程序 递归实质上也是一种循环结构 它把 较复杂 情况的计算归结为 较简单 情况的计算 一直归结到 最简单 情况的计算为止 在数值计算领域可以采用递归计算 在非数值领域使用也非常广泛 例如 河内塔 HanoiTower 问题8皇后问题骑士巡游问题此外 递归是人工智能语言Lisp Prolog等进行问题求解的基本手段 2 一种简化的递归程序模型 递归程序f x1 x2 xn 可以描述为f x1 x2 xn Ifp1thenE1elseifp2thenE2 elseifpmthenEmelseEm 1其中pi和Ei中含有f 递归程序的例子 计算最大公约数GCD x y ifx 0thenyelseify xthenGCD 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 ifx 100thenx 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 4 3 递归程序的计算规则 上例说明 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 为false2 原子测试函数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 x 0 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 1 0 则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 也终止 命题成立 良序归纳法 例2 证明计算最大公约数的程序GCD x y 的正确性 x 0 y 0 x 0 y 0 GCD x y ifx 0thenyelseify xthenGCD y x elseGCD x y x 分析 GCD函数的基本性质 1 GCD 0 y y 2 GCD x y GCD y x 当y x时 3 GCD x y GCD x y x 当y x时 良序归纳法 证明 选取良序集 W 为