在上一篇文章中谈到在使用循环的算法中,可以利用循环不变量证明算法的正确性,那如果是使用递归的算法呢。
递归的算法在计算中会形成某种递归结构,因此可以利用结构归纳法来证明正确性。
结构归纳法(Structural induction)
看到这个名字,我们会自然想起数学归纳法。
其实它是数学归纳法的一般化,也就是说数学归纳法是它的特殊化。
它用于证明,某种递归结构 x(list or tree)满足命题 P (x),证明方法类似我们熟悉的数学归纳法。
首先提出一个命题 P (x),证明最小结构和子结构均满足命题 P (x),那么这种递归结构满足命题 P (x)。
而这个命题经过结构归纳法证明后,能用作证明相应算法的正确性。
例子
跟上一篇一样,我们使用归并排序(Merge sort)作为例子,不过这次用到的是它的递归函数。
1: int* merge_sort(int* d, int c)
2: {
3: if (c > 1)
4: {
5: int lc = c / 2;
6: int rc = c - lc;
7: int* sld = merge_sort(d, lc);
8: int* srd = merge_sort(d + lc, rc);
9: return merge(sld, srd, lc, rc);
10: }
11: return d;
12: }
了解归并排序的朋友会知道它使用了分治法
分治法的中心思想是把问题递归分割为子问题,一直到不能继续分割的最小子问题(base case),最小子问题的解决方法很简单明显,这时递归返回并将子问题的答案逐层合并,最后就是原问题的答案了。
归并排序的 3 个步骤分别如下:
- 分割:行 5 得出标记分半的数组索引(将数组分半)
- 解决:行 7, 8 将分半的数组分别递归解决并返回有序数组
- 合并:行 9 将 2 个有序数组合并为 1 个有序数组并返回
假设原数组为 [ 5 2 4 7 1 3 2 6 ]
,它在分割阶段呈现以下的二叉树结构
当数组大小为 1 时,为最小子问题,已经到达递归的 base case,且大小为 1 的数组显然为有序,此时停止递归。
在合并阶段由底部至顶部逐层合并子问题答案,最终数组是原数组的有序结果
[ 1 2 2 3 4 5 6 7 ]
,如下证明
首先提出命题
原数组大小为 n,使用归并排序递归分割的,高度为 m 的二叉树
第 m 层有 2 ^ (m-1) 个大小为 n / 2 ^ (m-1) 的数组。
然后使用结构归纳法证明:
- 高度为 1 的二叉树,显然根节点数组等于原数组,第 1 层有 1 个大小为 n 的数组。
- 假设高度为 m 的二叉树,第 m 层有 2 ^ (m-1) 个大小为 n / 2 ^ (m-1) 的数组为真。
归并排序的递归分割时,把子问题对半分割为更小的子问题,因此下一层子问题数增倍,子问题大小减半。
因此第 m + 1 层会有 2 x 2 ^ (m-1) = 2 ^ m 个大小为 n / 2 ^ (m-1) / 2 = n / 2 ^ m 的数组。
满足命题第 m + 1 层有 2 ^ ((m + 1) - 1) = 2 ^ m 个大小为 n / 2 ^ ((m + 1) - 1) = n / 2 ^ m 的数组。
因此当二叉树高度为最大值时,已递归分割至最底层(数组大小为1不能继续分割),停止递归并将子问题答案通过 merge 函数合并逐层返回,而 merge 函数在上一篇中已证明其正确性,因此归并排序算法的正确性得以证明。