Att*_*lah 250 algorithm terminology definition clrs loop-invariant
我正在阅读CLRS的"算法简介".在第2章中,作者提到了"循环不变量".什么是循环不变量？
Tom*_*cek 324
简单来说,循环不变量是一个谓词(条件),它适用于循环的每次迭代.例如,让我们看一个如下所示的简单for循环:
int j = 9;
for(int i=0; i<10; i++)
j--;
在这个例子中,它是真实的(对于每次迭代)i + j == 9.一个较弱的不变量也是如此
i >= 0 && i <= 10.
TNi*_*TNi 113
我喜欢这个非常简单的定义:( 来源)
循环不变量是[程序变量中的]条件,它必须在循环的每次迭代之前和之后立即生效.(注意,这在迭代的某个部分没有说明它的真实性或虚假性.)
循环不变本身并没有多大作用.但是,给定适当的不变量,它可以用来帮助证明算法的正确性.CLRS中的简单示例可能与排序有关.例如,让你的循环不变,就像在循环开始时,i对这个数组的第一个条目进行排序.如果你可以证明这确实是一个循环不变量(即它在每次循环迭代之前和之后保持),你可以用它来证明排序算法的正确性:在循环终止时,循环不变量仍然满足,计数器i是数组的长度.因此,第一个i条目被排序意味着整个数组被排序.
一个更简单的例子:循环不变量,正确性和程序派生.
我理解循环不变量的方式是作为推理程序的系统的,正式的工具.我们做一个单独的陈述,我们专注于证明是真的,我们称之为循环不变量.这组织了我们的逻辑.虽然我们也可以非正式地讨论某些算法的正确性,但使用循环不变量会迫使我们仔细思考并确保我们的推理是不透明的.
Rob*_*nes 36
在处理循环和不变量时,有许多人没有立即意识到这一点.他们在循环不变量和循环条件(控制循环终止的条件)之间感到困惑.
正如人们所指出的,循环不变量必须是真的
(虽然在循环体中它可能暂时是假的). 另一方面,循环 终止后循环条件必须为假,否则循环永远不会终止.
因此,循环不变量和循环条件必须是不同的条件.
复杂循环不变量的一个很好的例子是二进制搜索.
bsearch(type A[], type a) {
start = 1, end = length(A)
while ( start <= end ) {
mid = floor(start + end / 2)
if ( A[mid] == a ) return mid
if ( A[mid] > a ) end = mid - 1
if ( A[mid] < a ) start = mid + 1
}
return -1
}
所以循环条件看起来非常简单 - 当开始>结束时循环终止.但为什么循环正确？什么是循环不变量证明它的正确性？
不变量是逻辑陈述:
if ( A[mid] == a ) then ( start <= mid <= end )
这个陈述是一个逻辑重言式 - 在我们试图证明的特定循环/算法的上下文中总是如此.它提供了有关循环终止后循环正确性的有用信息.
如果我们返回,因为我们在数组中找到了元素,那么语句显然是正确的,因为如果A[mid] == a那么a在数组中并且mid必须在start和end之间.如果循环终止,因为start > end再不可能有数量,使得start <= mid 和 mid <= end,因此我们知道这种说法A[mid] == a肯定是假的.但是,因此整体逻辑语句在空意义上仍然是正确的.(在逻辑中,语句if(false)then(something)总是如此.)
那么当循环终止时,我所说的循环条件必然是假的呢？看起来当在数组中找到元素时,当循环终止时,循环条件为真!它实际上不是,因为隐含的循环条件确实是真的,while ( A[mid] != a && start <= end )但是我们缩短了实际测试,因为第一部分是隐含的.无论循环如何终止,这个条件在循环后显然都是假的.
Tus*_*ria 32
以前的答案以非常好的方式定义了循环不变量.
现在让我试着解释CLRS的作者如何使用Loop Invariants来证明Insertion Sort的正确性.
插入排序算法(如书中所示):
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
在这种情况下循环不变(来源:CLRS书):子 阵列[1到j-1]总是排序.
现在让我们检查一下并证明算法是正确的.
初始化:在第一次迭代之前j = 2.所以Subarray [1:1]是要测试的数组.因为它只有一个元素所以它被排序.因此Invariant是满意的.
维护:通过在每次迭代后检查不变量可以很容易地验证这一点.在这种情况下,它是满意的.
终止:这是我们证明算法正确性的步骤.
当循环终止时,则j = n + 1的值.再次满足循环不变量.这意味着应该对子阵列[1到n]进行排序.
这就是我们想要用算法做的事情.因此我们的算法是正确的.
Vah*_*iei 16
除了所有的好答案之外,我想Jeff Edmonds的"如何思考算法"这个很好的例子 可以很好地说明这个概念:
例1.2.1"Find-Max双指算法"
1)规格:输入实例由列表L(1..n)元素组成.输出由索引i组成,使得L(i)具有最大值.如果有多个具有相同值的条目,则返回其中任何一个.
2)基本步骤:您决定使用双指方法.你的右手指向下跑.
3)进度测量:进度的度量是你的右手指在列表上的距离.
4)循环不变:那你的左边手指指向最大的条目之一遇到迄今为止你的右手手指的循环不变的状态.
5)主要步骤:每次迭代,您将右手指向下移动到列表中的一个条目.如果你的右手手指正指向的是更大的,则左手指的条目的条目,然后将你的左手手指与你的右手手指.
6)取得进步:你的进步因为你的右手移动了一个条目.
7)维护循环不变量:您知道循环不变量已按如下方式维护.对于每个步骤,新的左手指元素是Max(旧左手指元素,新元素).通过循环不变量,这是Max(Max(更短列表),新元素).在数学上,这是Max(更长的列表).
8)建立循环不变量:最初通过将两个手指指向第一个元素来建立循环不变量.
9)退出条件:当你的右手指完成遍历列表时,你就完成了.
10)结束:最后,我们知道问题解决如下.在退出状态下,右手指已经遇到所有条目.通过循环不变量,你的左手指指向这些的最大值.退回此条目.
11)终止和运行时间:所需的时间是列表长度的一些常数.
12)特殊情况:检查当多个条目具有相同值或n = 0或n = 1时会发生什么.
13)编码和实施细节:......
14)形式证明:算法的正确性来自上述步骤.
应当注意,循环不变量在被认为是表达变量之间的重要关系的断言时可以帮助设计迭代算法,所述变量在每次迭代开始时和循环终止时必须为真.如果这种情况成立,则计算是在实现有效性的道路上.如果为false,则算法失败.