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

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

Ответ 1

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

Ответ 2

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

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

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

Ответ 3

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

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

По завершении цикла:

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

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

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

Ответ 4

Алгоритм LS, который я написал, -

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

Я сделал свои собственные предположения для циклического инварианта для проверки правильности линейного поиска..... Может быть, это совершенно неправильно, поэтому мне нужны предложения по моим предположениям.

1) При инициализации - при я = 0 мы ищем v при я = 0.

2) При последовательных итерациях - мы ищем v до я < A.length-1

3) При завершении - я = A. length и до A.length мы продолжали искать v.

Ответ 5

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

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

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

Ответ 6

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

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

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

Прекращение: по мере того, как цикл заканчивается при поиске v в j, [0..j-1] будет массивом без j.

Если сам массив не имеет v, то j = i-1, и указанные выше условия будут сохраняться.