4

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次迭代之后，对于每个可能的 (i)-排列，子数组 A[1 .. i] 包含这个 (i)-排列，概率为 (n - i )!/n!。
  • 初始化：在第 1次迭代之后，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 产生一个统一的随机排列。

我的解释合乎逻辑吗？

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

4

1 回答 1

1

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

但是我怀疑这通常会很有意义

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

比喻

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

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

于 2014-06-24T20:38:08.610 回答