Почему цикл обязан закончиться

Инвариант доказывает, что если цикл кончился, результат верен. Про «кончился» он не говорит ничего. Вторая половина доказательства выглядит проще, но именно её чаще всего пропускают - и получают программу, которая на одном входе из тысячи висит.

Как думаешь, какой из циклов не остановится

i = 0
while i < len(a):
    if a[i] < 0:
        a.pop(i)
    else:
        i = i + 1

i = len(a) - 1
while i >= 0:
    if a[i] < 0:
        a.pop(i)
    i = i - 1

Оба останавливаются, но по разным причинам, и первый из них - ловушка, знакомая всем, кто чистил список на месте. В первом i не растёт при удалении; зато уменьшается длина списка. Во втором i уменьшается всегда. У каждого есть величина, которая убывает и ограничена снизу, - и это единственное, что нужно доказать.

Мера убывания

Мерой называют целую неотрицательную величину, зависящую от переменных цикла, которая строго убывает на каждом круге. Если такая величина найдена, цикл конечен: убывать бесконечно целое число, ограниченное снизу нулём, не может.

Для второго цикла мера очевидна: i + 1. Для первого - len(a) - i: при удалении длина уменьшается, при переходе растёт i, и в обоих случаях разность падает на единицу.

Мера не обязана быть счётчиком. В алгоритме Евклида

while b != 0:
    a, b = b, a % b

мерой служит само b: остаток строго меньше делителя, значит b убывает и неотрицательно. Отсюда следует завершаемость, хотя число кругов заранее неизвестно.

Считаем вместе: сколько кругов делает Евклид

Меры хватило, чтобы доказать конечность. Она же часто даёт и оценку числа кругов. Посмотрим на два соседних круга Евклида: пара (a, b) превращается в (b, a mod b), а потом в (a mod b, b mod (a mod b)).

Если b ≤ a/2, то новое первое число уже не больше половины старого. Если b > a/2, то a mod b = a - b < a/2. В обоих случаях за два круга первое число уменьшается минимум вдвое.

Значит кругов не больше, чем 2·log₂ a. Для чисел до миллиарда это около шестидесяти кругов - вместо миллиарда у наивного перебора делителей. Логарифм по основанию два здесь означает ровно это: сколько раз число можно поделить пополам, пока не дойдёшь до единицы.

Разбор: цикл, у которого меры нет

n = 27
while n != 1:
    if n % 2 == 0:
        n = n // 2
    else:
        n = 3 * n + 1

Это гипотеза Коллатца. Величина n то падает вдвое, то растёт втрое с лишним, и никакой убывающей меры для неё не найдено. Проверено, что цикл кончается для всех начальных значений примерно до 2⁶⁸, но доказательства для всех нет уже почти сто лет.

Мораль не про Коллатца. Отсутствие меры - это не признак того, что цикл вечен; это признак того, что доказательства нет. Программа, у которой не получается назвать меру, требует либо перестройки, либо явного ограничения на число кругов.

Общий вопрос и почему он не решается

Напрашивается мысль: пусть машина сама проверяет, остановится ли программа. Такой проверки не существует - и это доказано, а не «пока не придумали». Утверждение называется неразрешимостью проблемы останова: нет алгоритма, который по тексту любой программы и её входу отвечает, завершится ли она. Полное доказательство разбирается в разделе про границы вычислимости; здесь достаточно следствия.

Следствие практическое: завершаемость доказывает автор, а не инструмент. Анализаторы кода ловят частные случаи (счётчик не меняется в теле цикла), но общего ответа не дают и дать не могут.

Что делать, когда мера не находится

Три честных выхода, все три используются в настоящем коде:

• перестроить цикл так, чтобы мера появилась: заменить «пока не сойдётся» на фиксированное число итераций;
• поставить потолок на число кругов и считать его превышение ошибкой - именно так устроена машина курса, и именно поэтому она отличает вечный цикл от верного, но слишком дорогого решения;
• доказать конечность через свойство задачи, а не через переменную цикла: если на каждом круге некоторая целая величина растёт хотя бы на единицу и сверху ограничена, то кругов не больше этой границы. Так доказывают конечность алгоритма Форда-Фалкерсона (это про сети и потоки, разберём в своём разделе): величина потока растёт на целое число каждый круг и ограничена пропускной способностью сети - значит круги кончатся.

Теперь сам

Найди меру для цикла двоичного поиска из прошлого урока:

levo = 0
pravo = len(a)
while levo < pravo:
    seredina = (levo + pravo) // 2
    if a[seredina] < x:
        levo = seredina + 1
    else:
        pravo = seredina