CLRS 说
我们必须展示有关循环不变量的三件事：
-
初始化：在循环的第一次迭代之前这是正确的。
-
维护：如果在循环迭代之前为 true，则在下一次迭代之前它仍然为 true。
-
终止：当循环终止时，不变量为我们提供了一个有用的属性，有助于表明算法是正确的。
我的问题是我可以编辑这些步骤并将其改为：
-
初始化：在循环的第一次迭代之后这是正确的。
-
维护：如果在循环迭代后为 true，则在下一次迭代后仍为 true。
-
终止：当循环终止时，不变量为我们提供了一个有用的属性，有助于表明算法是正确的。
说明：基本上我们使用数学归纳原理来证明正确性。使用“初始化”，我们证明该属性在第一次迭代后成立。使用“维护”，我们可以表明该属性适用于所有迭代，因为“初始化”和“维护”一起创建了一条链。因此该属性在最后一次迭代后也保持不变。
例子：
RANDOMIZE-IN-PLACE(A)
1 n ← length[A]
2 for i ← to n
3 do swap A[i] ↔ A[RANDOM(i, n)]
对于这个算法，教科书上已经给出了使用标准程序的证明（由于太长，我没有将其包含在此处）。
我的建议：
-
Loop Invariant: Just after the ith iteration of the for loop of lines 2-3, for each possible (i)-permutation, the subarray A[1 .. i] contains this (i)-permutation with probability (n - i)!/n!.
-
Initialization: After 1st iteration A[1] contains this permutation with probability (n-1)!/n!=1/n which is true.
-
Maintenance: Let it be true after (i-1)th iteration. After (i)th iteration, A[1...i] contains this permutation with probability [(n-i+1)!/n!]*[1/(n-i+1)]=(n-i)!/n! which is what we want.
-
终止：终止时，i = n，并且子数组 A[1 .. n] 是给定的 n 排列，概率为 (n - n)!/n! = 1/n!.因此，RANDOMIZE-IN-PLACE 产生均匀的随机排列。
我的解释逻辑合理吗？
任何帮助将不胜感激。谢谢。
除了您必须执行额外的步骤（覆盖根本不运行的循环）这一事实之外，您当然还可以在第一次迭代之后证明不变量为真，而不是在第一次迭代之前证明它为真。
但我怀疑这通常是否有意义
- 首先，正如已经说过的，您已经有一个特殊情况（如果根本不执行循环会发生什么），这可能会导致一个类似于初始化的证明，您首先想跳过它
- 其次，第一次迭代后不变式为真的证明很可能与维护证明非常相似，因此您可能会编写两个非常相似的证明，只是为了跳过初始化，这很可能是一个相当大的过程。简单的证明。
Analogy
尽管这没有直接关系，但这个问题听起来很像尝试优化以下（伪）代码：
int product(int[] values)
product = 1
for i = 0 to values.size - 1
product *= values[i]
return product
To this:
int product(int[] values)
product = values[0] // to make the code quicker, start with the first item already
for i = 1 to values.size - 1 // start the loop at the second item
product *= values[i]
return product
只是，你现在必须包括额外的检查，是否values数组为空（我在上面的代码中没有）
本文内容由网友自发贡献，版权归原作者所有，本站不承担相应法律责任。如您发现有涉嫌抄袭侵权的内容，请联系:hwhale#tublm.com(使用前将#替换为@)
