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

Как видно из раздела Введение в алгоритмы ( 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). Заранее большое спасибо!

Источник

7 ответов

Решение

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

Источник 
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] ≠ ν,

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

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

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

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

Прекращение: 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 заканчивается, как и ожидалось.

Источник

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

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

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

,

Источник

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

forevery 0 <= i

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

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

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

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

Источник

Предположим, что у вас есть массив длины 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, и вышеприведенные условия будут по-прежнему выполняться.

Источник

Инвариант линейного поиска состоит в том, что каждый элемент перед i не равен ключу поиска. Разумным инвариантом для бинарного поиска может быть диапазон [low, high), каждый элемент перед low меньше ключа, а каждый элемент после high больше или равен. Обратите внимание, что есть несколько вариантов бинарного поиска с немного отличающимися инвариантами и свойствами - это инвариант бинарного поиска с "нижней границей", который возвращает самый низкий индекс любого элемента, равный или больший, чем ключ.

Источник: https://www.reddit.com/r/compsci/comments/wvyvs/what_is_a_loop_invariant_for_linear_search/

Кажется правильным для меня.

Источник

Алгоритм 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) В конце-я = A.length и до A.length мы продолжали искать v.

Источник
Другие вопросы по тегам