Разрешимость и проблема остановки
Вот она — самая знаменитая невозможность в информатике: нельзя написать программу, которая по любой программе скажет, остановится та или зациклится.
Проблема остановки: по описанию машины M и входу w определить, остановится ли M на w. Эта задача неразрешима — алгоритма, всегда дающего верный ответ, не существует.
Постановка
Кажется, что проверка «зациклится ли программа» — полезный инструмент, который кто-то да напишет. Тьюринг в 1936 году доказал: такой программы не существует и не может существовать. Это не «трудно» и не «пока не придумали» — это математически невозможно, как невозможно найти наибольшее простое число. Доказательство использует диагональный аргумент — тот самый приём Кантора, которым доказывают несчётность вещественных чисел.
Доказательство диагональю
Рассуждаем от противного. Предположим, существует машина H, которая по (M, w) всегда останавливается и говорит: H(M, w) = «остановится», если M на w останавливается, иначе «зациклится». Построим вредителя — машину D, которая берёт описание машины M и делает наоборот предсказанию H про M на самой себе:
D(⟨M⟩):
если H(M, ⟨M⟩) говорит «остановится»:
зациклиться навсегда ← делаем НАОБОРОТ
иначе (H говорит «зациклится»):
остановиться ← снова НАОБОРОТ
Теперь запустим D на ЕЁ ЖЕ описании: D(⟨D⟩).
Что скажет H(D, ⟨D⟩)?Получаем противоречие. Если H предсказывает, что D(⟨D⟩) остановится, то по своему коду D зацикливается — H ошиблась. Если H предсказывает, что D(⟨D⟩) зациклится, то D останавливается — H снова ошиблась. В обоих случаях H даёт неверный ответ. Но мы предположили, что H всегда права. Противоречие! Значит, H не существует. Проблема остановки неразрешима.
Почему диагональ
«Диагональ» — потому что D устроена так, чтобы отличаться от каждой машины в её собственной точке. Представьте таблицу: строки — машины, столбцы — входы, в клетке — останавливается ли. D смотрит на диагональ (машина на своём же описании) и инвертирует её. Поэтому D не совпадает ни с одной строкой таблицы — а должна бы, ведь она тоже машина. Это и есть диагональный парадокс, упакованный в доказательство.
Распознаваемо, но не разрешимо
Тонкость: проблема остановки распознаваема, но не разрешима. Можно написать программу, которая просто запускает M на w: если M остановится — ответим «да». Но если M зациклится, наша программа тоже зависнет и никогда не скажет «нет». Покажем эту асимметрию: «да» получить можно (если повезёт дождаться), «нет» — нельзя гарантировать.
# полу-разрешитель: ловит ТОЛЬКО остановку (за лимит шагов)
def halts_within(steps_fn, limit):
for n in range(limit):
if steps_fn(n): # машина просигналила остановку
return "остановилась на шаге " + str(n)
return "за " + str(limit) + " шагов не остановилась (не знаем!)"
# машина A останавливается на шаге 5
print(halts_within(lambda n: n == 5, 100))
# машина B не останавливается — мы НЕ можем сказать «зациклится»
print(halts_within(lambda n: False, 100))Вывод:
остановилась на шаге 5 за 100 шагов не остановилась (не знаем!)
Остановку мы поймали. Но «не остановилась за 100 шагов» — не доказательство зацикливания: вдруг остановится на шаге 101? Увеличение лимита не спасает — нет конечной границы. Вот граница между распознаваемым (поймать «да») и разрешимым (гарантировать да/нет).
Как работает под капотом
Проблема остановки — не единственная неразрешимая задача, а «мать» целого семейства. Теорема Райса обобщает: любое нетривиальное свойство языка, который распознаёт программа (например, «эта программа печатает 42», «эта функция чистая», «эти две программы эквивалентны»), неразрешимо. Поэтому идеального детектора вирусов, идеального оптимизатора, полного верификатора корректности произвольной программы быть не может — все они упёрлись бы в проблему остановки. Это фундаментальный предел автоматического анализа программ.
Частые ошибки
«Можно поставить таймаут». Таймаут даёт «не знаю», а не «зациклится». Никакой конечный лимит не решает проблему в общем виде.
«Это про конкретные сложные программы». Нет, неразрешимость про общий алгоритм для всех программ. Для многих конкретных программ остановку определить легко.
Путать неразрешимость и нераспознаваемость. Проблема остановки распознаваема (можно поймать «да»), но не разрешима. А вот её дополнение — уже не распознаваемо.
Итог
- Проблема остановки неразрешима: нет алгоритма, по (M, w) всегда верно говорящего, остановится ли M на w.
- Доказательство — диагональный аргумент: машина D противоречит предсказателю H на собственном описании.
- Проблема остановки распознаваема (поймать «да» запуском), но не разрешима (гарантировать «нет» нельзя).
- Теорема Райса: любое нетривиальное свойство поведения программ неразрешимо — предел автоматического анализа.