CLRS表示
我们必须显示关于循环不变式的三件事：
We must show three things about a loop invariant:
- 初始化：在循环的第一次迭代之前确实如此。
- 维护：如果在循环迭代之前为true，则在下一次迭代之前仍为true。
- Termination：当循环终止时，不变式为我们提供了一个
- Initialization: It is true prior to the first iteration of the loop.
- Maintenance: If it is true before an iteration of the loop, it remains true before the next iteration.
- Termination: When the loop terminates, the invariant gives us a useful property that helps show that the algorithm is correct.
我的问题是可以编辑步骤吗？并改为使用以下代码：
My question is can I edit the steps and make them these instead:
- 初始化：在循环的第一次迭代之后，它是正确的。
- 维护：如果在循环迭代后为true，则在下一次迭代后仍为true。
- 终止：当循环终止时，不变式为我们提供了一个有用的属性，该属性有助于表明算法是正确的。
- Initialization: It is true after the first iteration of the loop.
- Maintenance: If it is true after an iteration of the loop, it remains true after the next iteration.
- Termination: When the loop terminates, the invariant gives us a useful property that helps show that the algorithm is correct.
说明：基本上，我们使用数学归纳原理来证明正确性。使用初始化，我们证明该属性在第一次迭代后成立。使用维护，我们可以显示该属性对所有迭代均有效，因为初始化和维护共同创建了一个链。因此，该属性在最后一次迭代之后也保持不变。
Explanation: Basically we use Principle Of Mathematical Induction to prove correctness. Using "Initialization" we prove that the property holds after the 1st iteration. Using "Maintenance" we can show that the property holds for all iterations since "Initialization" and "Maintenance" together create a chain. And hence the property holds after the last iteration too.
示例：
RANDOMIZE-IN-PLACE(A) 1 n ← length[A] 2 for i ← to n 3 do swap A[i] ↔ A[RANDOM(i, n)]对于此算法，教科书中已经使用标准程序给出了证明（由于时间太长，因此未在此处包括）。
For this algorithm, there is already a proof given in the textbook using the standard procedure (I didn't include it here since it is too long).
我的建议：
- 循环不变式：在第2-3行的for循环的第i 次迭代之后，对于每个可能的（i）置换，子数组A [1 .. i]包含该（i）置换的概率（n-i）！/ n！。
- 初始化：在1 st 次迭代后，A [1]包含此排列的可能性（n-1）！/ n！= 1 / n，这是真的。
- 维护：在（i-1）之后使其为真迭代。在第（i） 次迭代后，A [1 ... i]包含此排列，概率为[（n-i + 1）！/ n！] * [1 /（n-i + 1） ）] =（ni）！/ n！
- 终结点：在结束时，i = n，子数组A [1 .. n]是给定的n -概率为（n-n）的排列！/ n！ = 1 / n!。因此，RANDOMIZE-IN-PLACE产生统一的随机排列。
- 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.
- Termination: At termination, i = n, and we have that the subarray A[1 .. n] is a given n-permutation with probability (n - n)!/n! = 1/n!. Thus, RANDOMIZE-IN-PLACE produces a uniform random permutation.
我的解释在逻辑上合理吗？
Is my explanation logically sound?
任何帮助将不胜感激。谢谢。
Any help would be greatly appreciated. Thanks.
推荐答案除了事实，您还必须执行其他步骤，该步骤涵盖了从未运行过的循环，您当然也可以证明不变量在第一次迭代后为真，而不必证明在第一次迭代之前为真。
Apart from the fact, that you have to make an additional step, which covers the loop never running at all, you can of course also prove that the invariant is true after the first iteration instead of proving that it is true before the first iteration.
但是我怀疑这是否经常有意义
However I doubt that this will often make much sense
- 首先，已经说过，您已经有一个特殊情况（如果根本不执行循环会发生什么情况），这可能会导致您想先跳过的证明，类似于初始化。
- 第二，在第一次迭代后不变量为真的证明很可能与Maintanance证明非常相似，因此您可能会编写两个非常相似的证明，只是跳过了Initialization，即可能很容易证明。
Analog
尽管这并不直接相关，但这个问题听起来很像试图优化以下（伪）代码：
Although this is not directly related, this question sounds a lot like trying to optimize the following (pseudo)code:
int product(int[] values) product = 1 for i = 0 to values.size - 1 product *= values[i] return product到此：
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 数组是否为空（我在上面的代码中没有）
just, that you now have to include the additional check, whether the values array is empty (which I did not in the above code)
更多推荐
我们是否可以使用循环不变式证明算法的正确性,在其中我们证明在第一次迭代之后而不是之前是正确的？
发布评论