Петлевой инвариант линейного поиска

Question

Как видно на введении в алгоритмы (http://mitpress.mit.edu/algorithms),, в упражнении говорится следующее:

Ввод: массив A [1 ... n]

Вывод: i, где A [i] = v или NIL, если не найден

Написать псевдокод для LINEAR-SEARCH, который просматривает последовательность, ищу v. Использование инварианта цикла, докажите, что ваш алгоритм правильный. (Убедитесь, что ваш цикл инвариант выполняет три необходимых свойства - инициализация, обслуживание, прекращение.)

У меня нет проблем с созданием алгоритма, но я не могу понять, как я могу решить, что такое мой инвариант цикла. Мне кажется, я понял концепцию инварианта цикла, то есть условие, которое всегда истинно перед началом цикла, в конце / начале каждой итерации и по-прежнему верно, когда цикл заканчивается. Обычно это является целью, поэтому, например, при сортировке вставки, начиная с j, начиная с j = 2, элементы [1, j-1] всегда сортируются. Это имеет смысл для меня. Но для линейного поиска? Я не могу думать ни о чем, просто это звучит слишком просто, чтобы думать об инварианте цикла. Я понял что-то не так? Я могу думать только о чем-то очевидном (например, NIL или между 0 и n). Заранее большое спасибо!

Answer 1

После того как вы посмотрели на индекс i и еще не нашли v, что вы можете сказать о v относительно части массива до i и относительно части массивапосле i?

Answer 2

В случае линейного поиска вариант цикла будет резервным хранилищем, используемым для сохранения индекса (вывода).

Позволяет назвать хранилище резервных копий как index , которое изначально установлено в NIL. Вариант цикла должен соответствовать трем условиям:

• Инициализация: это условие выполняется для индексной переменной.since, оно содержит NIL, которое может быть результатом результата и истинно перед первой итерацией.
• Обслуживание: индекс будет удерживать NIL, пока не будет найден элемент v. Это также верно до итерации и после следующей итерации. Так как она будет установлена ​​внутри цикла после выполнения условия сравнения.
• Завершение: индекс будет содержать NIL или индекс массива элемента v.

.

Answer 3

Инвариант петли будет

forevery 0 <= i <k, где k - текущее значение переменной итерации цикла, A [i]! = V </p>

В конце цикла:

если A [k] == v, то цикл завершается и выдает k

если A [k]! = V и k + 1 == n (размер списка), то цикл завершается со значением nil

Доказательство правильности: оставлено как упражнение

Answer 4

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

Инвариант цикла: в начале i -ой итерации цикла for (строки 1–4),

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

Инициализация:

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

, которая является истинной, так как любое утверждение относительно пустого набора истинно ( бессмысленная правда ).

Обслуживание: давайте предположим, что инвариант цикла равен true в начале i -й итерации цикла for.Если A[i] == ν, текущая итерация является последней (см. Раздел окончание ), поскольку строка 3 выполняется;в противном случае, если A[i] ≠ ν, у нас есть

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

, что означает, что инвариантный цикл все еще будет истинным в начале следующей итерации (i+1 th).

Завершение: цикл for может закончиться по двум причинам:

1. return 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 5

Предположим, что у вас есть массив длины i, проиндексированный с [0 ... i-1], и алгоритм проверяет, присутствует ли v в этом массиве. Я не совсем уверен, но я думаю, что инвариант цикла выглядит следующим образом: Если j является индексом v, то [0..j-1] будет массивом, который не имеет v.

Инициализация: перед итерацией с 0..i-1 текущий проверенный массив (нет) не состоит из v.

Обслуживание: при нахождении v в j массив из [0..j-1] будет массивом без v.

Завершение: Поскольку цикл заканчивается при нахождении v в j, [0..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 мы ищем v при i = 0.

2) При последовательных итерациях мы ищем v, пока i

3) В конце - i = A.length и до A.length мы продолжали искать v.