线性搜索的循环不变式

Question

正如算法简介 (http://mitpress.mit.edu/algorithms) 所示，该练习指出以下内容：

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

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

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

我创建算法没有问题，但我不明白的是我如何决定我的循环不变式是什么。我想我理解了循环不变的概念，即在循环开始之前、每次迭代结束/开始时始终为真的条件，并且在循环结束时仍然为真。这通常是目标，例如，在 插入排序< /a>，迭代 j，从 j = 2 开始，A[1..j-1] 元素始终已排序。这对我来说很有意义。但是对于线性搜索呢？我想不出任何东西，循环不变式听起来太简单了。我是不是理解错了什么？我只能想到一些明显的东西，比如（它要么是 NIL，要么是 0 到 n 之间）。预先非常感谢！

Answer 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] ≠ ν,

是真的，因为任何关于空集的陈述都是真的（空洞的真理）。

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

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

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

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

1. 返回i（第3行），如果A[i] == ν;

2. i == A.length + 1（for 循环的最后一次测试），在这种情况下，我们位于 A.length 的开头+ 第 1 次迭代，因此循环不变式为

   ∀ k ∈ [1, A.length + 1) A[k] ≠ ν ⟺ ∀ k ∈ [1, A.length] A[k] ≠ ν
   

   并且返回NIL值（第4行）。

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

Answer 2

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

Answer 3

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

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

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

。

Answer 4

循环不变式将

永远是 0 <= i < k，其中k是循环迭代变量的当前值，
A[i] != v

循环终止时：

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

if A[k] != v，且 k + 1 == n（列表的大小） then 循环以 nil 值终止

正确性证明：留作练习

Answer 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] 中的数组将是一个没有 v 的数组。 .j-1] 将是一个没有 j 的数组。

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

Answer 6

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

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

对我来说似乎是正确的。

Answer 7

我编写的 LS 算法是 -

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

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

1. 在初始化时 - 在 i = 0 处，我们在 i = 0 处搜索 v。

2. 在连续迭代中 - 我们在寻找 v 直到 i

   A.length-1

3. 终止时 - i = A.length 直到 A.length 我们一直在寻找 v。