线性搜索的循环不变量答案

【问题标题】：Loop invariant of linear search线性搜索的循环不变量
【发布时间】：2011-07-31 21:33:30
【问题描述】：

从算法简介 (http://mitpress.mit.edu/algorithms) 中可以看出，该练习陈述如下：

输入：数组A[1..n]和一个值v

输出： 索引i，其中A[i] = v 或NIL 如果在v 中找不到A

为 LINEAR-SEARCH 编写伪代码，它扫描序列，寻找 v. 使用循环不变量，证明你的算法是正确的。（确保你的循环不变满足三个必要的属性 – 初始化、维护、终止。）

我创建算法没有问题，但我不知道如何确定我的循环不变量。我想我理解了循环不变量的概念，即在循环开始之前、每次迭代的结束/开始时始终为真并且在循环结束时仍然为真的条件。这通常是目标，例如，在insertion sort，迭代j，从j = 2 开始，A[1..j-1] 元素总是被排序的。这对我来说很有意义。但是对于线性搜索？我什么都想不出来，想一个循环不变量听起来太简单了。我理解错了吗？我只能想到一些明显的东西（它不是 NIL 就是介于 0 和 n 之间）。提前非常感谢！

【问题讨论】：

标签： algorithm invariants loop-invariant

【解决方案1】：

LINEAR-SEARCH(A, ν)
1  for i = 1 to A.length
2      if A[i] == ν 
3          return i
4  return NIL

循环不变量：在for 循环的第i 次迭代开始时（第1-4 行），

∀ k ∈ [1, i) A[k] ≠ ν.

初始化：

i == 1 ⟹ [1, i) == Ø ⟹ ∀ k ∈ Ø A[k] ≠ ν,

这是正确的，因为任何关于空集的陈述都是正确的（vacuous truth）。

维护：让我们假设循环不变量在i 循环的第i 次迭代开始时为真for 循环。如果A[i] == ν，当前迭代是最后一个（参见termination部分），因为第3行被执行；否则，如果A[i] ≠ ν，我们有

∀ k ∈ [1, i) A[k] ≠ ν and A[i] ≠ ν ⟺ ∀ k ∈ [1, i+1) A[k] ≠ ν,

这意味着不变循环在下一次迭代（i+1th）开始时仍然为真。

终止：for 循环可能因两个原因而结束：

return i（第 3 行），如果 A[i] == ν;
i == A.length + 1（for 循环的最后一次测试），在这种情况下，我们处于A.length + 1th 迭代的开始，因此循环不变量是
```
∀ k ∈ [1, A.length + 1) A[k] ≠ ν ⟺ ∀ k ∈ [1, A.length] A[k] ≠ ν
```
并返回 NIL 值（第 4 行）。

在这两种情况下，LINEAR-SEARCH 都按预期结束。

【讨论】：

漂亮！数学上精确且曝光良好。谢谢你的回答！

【解决方案2】：

在你查看了索引i，但还没有找到v 之后，关于v 关于i 之前的数组部分以及关于数组的部分你能说什么？在i之后？

【讨论】：

v 不是从 1 到 i 而是可能在 i 之后，这可以是循环不变量吗？
好的，这没有意义...怎么样，v 不是来自 [1...i]，但这对于循环的初始化无效，因为 i=1我不能保证 v 不是第一个元素。但我也不能使用负边界，对吧？
@Clash：你的第一次尝试看起来很明智。我的提示最好表述为“在查看A[i] ...之前”，以便不变量在循环的开始处成立。
@Clash：您的练习文本似乎暗示了一个基于 1 的数组。 i 然后从 1 变为 n。如果将i 初始化为1，然后检查A[i]，最后增加i，则循环不变量适用于任何小于i 的数组索引。如果没有小于i 的有效数组索引，则它通常成立——对于空集而言，任何事情都是正确的。
@Clash：这不是真正的问题。请记住，这是伪代码和数学，而不是实际机器上的实际代码。如果您假设符号 A[l...u] 表示 { A[i], ∀i i>=l ∧ i <= u }，那么 A[0...-1] 将表示一个空集。说 v 不在空集上是真的，所以它在开始时成立。

【解决方案3】：

在线性搜索的情况下，循环变体将是用于保存索引（输出）的后备存储。

让我们将后备存储命名为 index，它最初设置为 NIL。循环变体应符合三个条件：

初始化：此条件适用于索引变量。因为它包含 NIL，这可能是结果结果，并且在第一次迭代之前为真。
维护：索引将保持 NIL 直到找到项目 v。在迭代前和下一次迭代后也是如此。因为比较条件成功后会在循环内设置。
终止：索引将包含 NIL 或项目 v 的数组索引。

.

【讨论】：

【解决方案4】：

循环不变量将是

forevery 0

循环终止时：

如果 A[k] == v，则循环终止并输出 k

如果 A[k] != v，并且 k + 1 == n（列表大小），则循环以 nil 值终止

正确性证明：留作练习

【讨论】：

这是否适用于初始化？ 0
我无法证明这一点，因为我没有您的代码。但是，我会在我的循环中有一个 if-then-else 语句，比如 if A[i[ == v, return i.然后我可以证明我的代码的初始化情况：k = 0。要么 A[i] == v，在这种情况下我的循环终止并输出 k。相反，如果 A[i] != v，则对于所有 0
0 <= i < k 在循环的初始迭代中成立，因为您将得到一个空数组，实际上，它不包括 v，因此条件为真 在初始之前循环的执行.

【解决方案5】：

假设您有一个长度为 i 的数组，从 [0...i-1] 开始索引，并且算法正在检查此数组中是否存在 v。我不完全确定，但我认为，循环不变量如下： 如果 j 是 v 的索引，那么 [0..j-1] 将是一个没有 v 的数组。

初始化：从 0..i-1 迭代之前，当前数组检查（无），不包含 v。

维护：在 j 处找到 v 时，来自 [0..j-1] 的数组将是一个没有 v 的数组。

终止：当循环在 j 处找到 v 时终止，[0..j-1] 将是一个没有 j 的数组。

如果数组本身没有v，那么j = i-1，以上条件依然成立。

【讨论】：

【解决方案6】：

线性搜索的不变量是 i 之前的每个元素都不等于搜索键。二分搜索的合理不变量可能是范围 [low, high)，low 之前的每个元素都小于 key，high 之后的每个元素都大于或等于。请注意，二分搜索有一些变体，不变量和属性略有不同 - 这是“下限”二分搜索的不变量，它返回等于或大于键的任何元素的最低索引。

来源：https://www.reddit.com/r/compsci/comments/wvyvs/what_is_a_loop_invariant_for_linear_search/

对我来说似乎是正确的。

【讨论】：

【解决方案7】：

我写的LS算法是-

LINEARSEARCH(A, v)
  for i=0 to A.length-1
    if(A[i] == v)
      return i
  return NIL

我对循环不变量做了自己的假设，以检查线性搜索的正确性：

在初始化时-在 i = 0 处，我们在 i = 0 处搜索 v。
在连续迭代中——我们一直在寻找 v 直到 i
在终止时 - i = A.length 直到 A.length 我们一直在寻找 v。

【讨论】：