我在读CLRS的《算法导论》。在第二章中,作者提到了“循环不变量”。什么是循环不变量?
当前回答
简单地说,它是一个循环条件,在每次循环迭代中都为真:
for(int i=0; i<10; i++)
{ }
在这里,我们可以说i的状态是i<10并且i>=0
其他回答
简单地说,它是一个循环条件,在每次循环迭代中都为真:
for(int i=0; i<10; i++)
{ }
在这里,我们可以说i的状态是i<10并且i>=0
循环不变量属性是一个条件,适用于循环执行的每一步。For循环,while循环,等等)
这对于循环不变证明是必不可少的,如果在执行的每一步都保持循环不变属性,则可以证明算法正确执行。
对于一个正确的算法,循环不变量必须保持在:
初始化(开始)
维护(之后的每一步)
终止(当它完成时)
这被用来计算很多东西,但最好的例子是加权图遍历的贪婪算法。对于贪心算法产生最优解(穿过图的路径),它必须达到连接所有节点在最小权值路径可能。
因此,循环不变的性质是所选择的路径具有最小的权值。在开始时,我们没有添加任何边,所以这个属性为真(在这种情况下,它不是假的)。在每一步中,我们都遵循最小权值边(贪婪步),所以我们再次采用最小权值路径。最后,我们找到了最小加权路径,所以我们的性质也是成立的。
如果一个算法不这样做,我们可以证明它不是最优的。
之前的回答已经很好地定义了循环不变量。
以下是CLRS的作者如何使用循环不变量来证明插入排序的正确性。
插入排序算法(见书):
INSERTION-SORT(A)
for j ← 2 to length[A]
do key ← A[j]
// Insert A[j] into the sorted sequence A[1..j-1].
i ← j - 1
while i > 0 and A[i] > key
do A[i + 1] ← A[i]
i ← i - 1
A[i + 1] ← key
循环不变量在这种情况下: 子数组[1到j-1]始终被排序。
现在让我们检查一下,证明这个算法是正确的。
初始化:在第一次迭代j=2之前。所以子数组[1:1]就是要测试的数组。因为它只有一个元素,所以它是有序的。这样不变性就被满足了。
维护:这可以通过在每次迭代后检查不变量来轻松验证。在这种情况下,它被满足了。
终止:这是我们将证明算法正确性的步骤。
当循环结束时,j=n+1。循环不变量再次被满足。这意味着子数组[1到n]应该排序。
这就是我们想用算法做的。因此,我们的算法是正确的。
值得注意的是,循环不变量可以帮助迭代算法的设计,因为它被认为是一个断言,表示变量之间的重要关系,在每次迭代开始时和循环结束时,这些关系必须为真。如果这是成立的,计算是在有效的道路上。如果为false,则算法失败。
对不起,我没有评论权限。
正如你提到的@Tomas Petricek
另一个较弱的不变式也是成立的,即i >= 0 && i < 10(因为这是连续条件!)”
为什么它是循环不变量?
我希望我没有错,据我理解[1],循环不变将在循环开始时为真(初始化),它将在每次迭代(维护)之前和之后为真,它也将在循环结束后为真(终止)。但是在最后一次迭代之后,i变成了10。因此,条件i >= 0 && i < 10变为假值并终止循环。它违反了循环不变量的第三个性质(终止)。
[1] http://www.win.tue.nl/~kbuchin/teaching/JBP030/notebooks/loop-invariants.html