我们是否可以使用循环不变量来证明算法的正确性，在其中我们证明它在第一次迭代之后而不是之前是正确的？

Question

CLRS 说

我们必须展示关于循环不变量的三件事：

• 初始化：在循环的第一次迭代之前为真。
• 维护：如果在循环的一次迭代之前为真，则在下一次迭代之前保持为真。
• 终止：当循环终止时，不变量为我们提供了一个有用的属性，有助于证明算法是正确的。

我的问题是我可以编辑这些步骤并改为：

• 初始化：循环第一次迭代后为真。
• 维护：如果循环一次迭代后为真，下一次迭代后仍为真。
• 终止：当循环终止时，不变量为我们提供了一个有用的属性，有助于证明算法是正确的。

解释：基本上我们使用数学归纳原理来证明正确性。使用“初始化”，我们证明该属性在第一次迭代后成立。使用“维护”，我们可以证明该属性适用于所有迭代，因为“初始化”和“维护”一起创建了一个链。因此，该属性在最后一次迭代后也成立。

例子：

RANDOMIZE-IN-PLACE(A) 
1 n ← length[A] 
2 for i ← to n
3 do swap A[i] ↔ A[RANDOM(i, n)]

对于这个算法，在教科书中已经有使用标准程序给出的证明（因为太长了，我没有在这里列出）。

我的建议：

• 循环不变量：就在第 2-3 行 for 循环的第 i^th 次迭代之后，对于每个可能的 (i)-排列，子数组 A[1 .. i ] 包含这个 (i)-排列，概率为 (n - i)!/n!。
• 初始化：在第 1^st 次迭代后，A[1] 包含这个排列，概率为 (n-1)!/n!=1/n，这是真的。
• 维护：让它在 (i-1)^th 次迭代后为真。在 (i)^th 次迭代之后，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 产生一个统一的随机排列。

我的解释合乎逻辑吗？

任何帮助将不胜感激。谢谢。

Answer 1

除了你必须做一个额外的步骤，它涵盖了永远不会运行的循环之外，你当然也可以在第一次迭代之后证明不变量是真的，而不是在迭代之前证明它是真的第一次迭代。

但我怀疑这通常是否有意义

• 首先，如前所述，您已经有一个特殊情况（如果根本不执行循环会发生什么），这可能会导致一个类似于初始化的证明，您想首先跳过它
• 其次，第一次迭代后不变量为真的证明，很可能与Maintanance证明非常相似，所以你很可能会写两个非常相似的证明，只是略过Initialization，这很可能是一个很容易的证明。

---

类比

虽然这没有直接关系，但这个问题听起来很像尝试优化以下（伪）代码：

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 数组是否为空（我在上面的代码中没有）