1. 循环不变式和数学归纳法

在数学中，数学归纳法常用于证明给定命题在自然数范围内的正确性，它是一种严谨的演绎推理法。而在计算机科学中，循环不变式同样作为一种演绎推理法用于理解和证明算法的正确性。从下文的介绍中可以看出，循环不变式和数学归纳法有着许多的相似之处。

2. 循环不变式的三条性质

循环不变式用于理解和证明算法的正确性。实际上，循环不变式并不是狭义上的一个式子，而是一个在命题，一个在算法的起始状态、运行过程中和算法结束时始终保持为真的一个命题。通过下文中的例子可以更加清晰的认识到循环不变式的意义，下面是循环不变式的三条性质：

初始化：循环的第一次迭代之前，它为真。
保持：如果循环的某次迭代之前它为真，那么下次迭代之前它仍为真。
终止：在循环终止时，不变式为我们提供一个有用的性质，该性质有助于证明算法时正确的。

注意：循环不变式的前两条性质类似于数学归纳法，证明了一个基本情况和一个归纳步。此外，终止性不同于数学归纳法的做法，在归纳法中，归纳步是无限地使用的，这里当循环终止的时候，归纳随之终止。

3. 利用循环不变式分析插入排序

插入排序是一个简单的原址排序算法，也是一种稳定的排序算法。下面给出插入排序的伪代码，然后利用循环不变式来分析算法的正确性。

INSERT-SORT(A)for j = 2 to A.lengthkey = A[j]// 将第j个数插入到前j-1个已排序的数中i = j - 1while i > 0 and A[i] > keyA[i + 1] = A[i]i = i - 1A[i + 1] = key

循环不变式：在for循环的每次迭代开始时，子数组A[1…j-1]由原来在A[1…j-1]中的元素组成，但已按升序排列。

下面证明循环不变式的三条性质成立：
初始化：循环的第一次迭代之前，循环不变式成立。当第一次迭代之前(j = 2),A[1…j-1]就是A[1]，即初始的第一个元素，循环不等式显然成立。
保持：如果循环的某次迭代之前它为真，那么下次迭代之前它仍为真。这里假设A[1…j-1]由原来的A[1…j-1]中元素组成，且已按升序排列。那么在此次循环中，将A[j-1]、A[j-2]、A[j-3]等元素逐个向右移动一个位置，直到找到A[j]的适宜位置为止，然后将A[j]的值插入该位置。此时，A[1…j]仍有原来在A[1…j]中的元素组成，且已按升序排列。因此，在下次迭代之前，循环不变式仍然为真。
终止：循环终止时j = A.length + 1。由循环不变式可知，A[1…A.length]由原来在A[1…A.length]中的元素组成，但已按升序排列。由于A[1…A.length]就是整个数组，因此整个数组已按升序排列，算法正确。

注意：循环不变式的判定是在每次迭代之前，在上例中我们以for循环中对循环变量j赋值之后，对循环变量判断终止条件之前这一时刻为迭代之前的时刻。因此，在循环终止之前时，循环变量j = A.length+1，此时数组A[1…A.length]由原来在A[1…A.length]的元素组成，且按升序排序。

4. 练习题

2.1.3

考虑以下查找问题：
输入：n个数的一个序列A=<a1,a2,...,an>和一个值v。A=<a_1, a_2, ..., a_n>和一个值v。A=<a1,a2,...,an>和一个值v。
输出：下标i使得v=A[i]v=A[i]v=A[i]或者当vvv不在A中出现时，iii为特殊值NIL。
写出线性查找的伪代码，它扫描整个序列来查找vvv。使用一个循环不变式来证明你的算法是正确的。确保你的循环不变式满足三条必要的性质。

1.伪代码：

LINEAR-SEARCH(A, v)for j = 1 to A.lengthif v == A[j]return jreturn NIL

2.循环不变式：在for循环的每次迭代开始，子数组A[1..j−1]A[1..j-1]A[1..j−1]中不存在值vvv。
3.证明：
初始化：第一次迭代前j=1，A[1..0]j=1，A[1..0]j=1，A[1..0]为空，循环不变式显然成立。
保持：假设第kkk次迭代前循环不等式成立，即A[1..k−1]A[1..k-1]A[1..k−1]中不存在值vvv。在此次循环中，如果A[j]=vA[j]=vA[j]=v，则算法结束，返回当前值的下标j；如果A[j]≠vA[j]≠vA[j]̸=v，则子数组A[1..k]A[1..k]A[1..k]中不存在值vvv，在下一次迭代开始之前，循环不变式成立。
终止：循环终止存在两种情况，一种就是迭代过程中查找到目标元素，则返回该元素在数组种的下标。另一种是数组种不存在目标元素，在循环终止前j=A.length+1，由循环不变式得数组A[1..A.length]A[1..A.length]A[1..A.length]种不存在值vvv，即vvv不存在与数组A中，于是程序运行到最后返回特殊值NIL。

算法导论学习笔记1_循环不变式相关推荐

算法导论中C语言代码,算法导论-学习笔记与进度
算法导论阅读进度第一部分基础知识第一章计算中算法的角色 Done 1.1 算法输入与输出算法可以解决哪些问题数据结构技术一些比较难的问题 1.2 作为一种技术的算法效率算法和其 ...
算法导论学习笔记第2章算法基础
本章介绍了一个贯穿本书的框架,后续的算法设计都是在这个框架中进行的. 本章通过插入排序和归并排序两种常见的算法来说明算法的过程及算法分析,在分析插入排序算法时,书中是用了循环不变式证明了算法的正确性, ...
【算法导论学习笔记】第3章：函数的增长
原创博客,转载请注明: http://www.cnblogs.com/wuwenyan/p/4982713.html 当算法的输入n非常大的时候,对于算法复杂度的分析就显得尤为重要,虽然有时我们能通 ...
算法导论学习笔记第7章快速排序
对于包含n个数的输入数组来说,快速排序是一种时间复杂度为O(n^2)的排序算法.虽然最环情况的复杂度高,但是快速排序通常是实际应用排序中最好的选择,因为快排的平均性能非常好:它的期望复杂度是O(nlg ...
算法导论学习笔记第6章堆排序
在本章中介绍了另一种排序算法:堆排序(heapsort).与归排序一样,但不同于插入排序的是,堆排序的时间复杂度式(Onlgn).而与插入排序相同,但不同于归并排序的是,堆排序同样具有空间原址性(我理 ...
【转】算法导论学习笔记一分治算法
分治策略是一种常见的算法.在分治策略中,我们递归的求解一个问题,在每层递归中应用如下三个步骤: 1. 分解,将问题分解成规模更小但解决方案相同的子问题 2. 解决,递归的求解子问题,如果子问题足够小则 ...
算法导论学习笔记 6.5 优先队列
优先队列(priority queue)是一种用来维护由一组元素构成的集合S的数据结构,其中的每一个元素都有一个相关的值,称为关键字(key).一个最大优先队列支持一下操作: INSERT(S, x) ...
生日悖论问题——《算法导论学习笔记》
1 生日悖论问题 1.1 原始问题一个房间里的人数必须达到多少,才能使两个人生日相同的机会达到50%?不考虑闰年情况,也就是一年按照365天来计算. 解答: 假设房间里的人数是k,我 ...
计算机视觉算法——Transformer学习笔记
算机视觉算法--Transformer学习笔记计算机视觉算法--Transformer学习笔记 1. Vision Transformer 1.1 网络结构 1.2 关键知识点 1.2.1 Self ...

算法导论学习笔记1_循环不变式

循环不变式