Теорема (о неразрешимости проблемы останова). Не существует алгоритма (машины Тьюринга) $H$, который для произвольной пары $⟨M,w⟩$ надёжно отвечает «да» тогда и только тогда, когда машина $M$ останавливается на входе $w$. Формально: множество
$$\mathrm{HALT}=\{⟨M,w⟩\mid M\text{останавливается на}w\}$$ неразрешимо.
Доказательство (классическое диагональное, противоречие). Предположим противное: существует разрешающий алгоритм $H$, который на входе $⟨M,w⟩$ возвращает «да», если $M$ останавливается на $w$, и «нет» иначе.
Построим программу (машину) $D$, которая на входе строковой код $x$ делает следующее:
- запускает $H$ на паре $⟨x,x⟩$;
- если $H$ ответил «да» (то есть $x$ останавливается на входе $x$), то $D$ входит в бесконечный цикл (не останавливается);
- если $H$ ответил «нет», то $D$ немедленно останавливается.
Пусть $d=⟨D⟩$ — код полученной машины $D$. Рассмотрим поведение $D$ на собственном коде $d$:
- если $H$ говорит, что $D$ останавливается на $d$, то по конструкции $D(d)$ войдёт в бесконечный цикл — противоречие;
- если $H$ говорит, что $D$ не останавливается на $d$, то по конструкции $D(d)$ немедленно остановится — тоже противоречие.
В обоих случаях получаем противоречие с корректностью $H$. Следовательно, наше предположение ложно: такого алгоритма $H$ не существует. Теорема доказана.
Короткие дополнительные факты:
- Множество $\mathrm{HALT}$ перечислимо (recursively enumerable): симулируя $M$ на $w$ мы обнаружим и зафиксируем остановку, но в общем случае не можем доказать её отсутствие.
- По теореме Райса любое нетривиальное свойство семантики программы (связанное с её поведением) также неразрешимо.
Практические следствия для разработки и верификации ПО
- Отсутствие универсального анализатора: не существует общего автоматического инструмента, который для любых программ гарантированно и точно скажет, остановятся ли они или обладают другой нетривиальной поведением. Любой практический анализ должен быть неполным или ограниченным по expressiveness.
- Концептуальные стратегии:
- звуковые, но неполные анализаторы (conservative): дают только безопасные выводы (например, «гарантированно безопасно»), но могут отвечать «неизвестно» для многих корректных программ;
- эвристические и статистические методы (фреймворки анализа, статический анализ, анализ по шаблонам): работают в большинстве практических случаев, но без теоретической гарантии полного охвата;
- ограничение языка/модели (например, обрезанные языки, терминирующие подсистемы, типовые системы с доказательством уменьшения меры): делает задачу разрешимой в ограниченном классе программ;
- интерактивные доказательства и формальные верификаторы (Coq, Isabelle, Dafny): требуют человеческого участия или аннотаций, но дают полные доказательства для проверяемых фрагментов.
- Конкретные методы в промышленности:
- проверка на конечном ресурсе (bounded model checking, тестирование, fuzzing): эффективны, но дают частичную уверенность;
- абстрактная интерпретация и анализ потоков управления/значений: даёт практические предупреждения и ошибки, но периодически выдаёт ложные срабатывания или «неизвестно»;
- анализ роста метрик/ранживая функция (termination provers) и типы размеров: позволяют доказывать прекращение для многих реальных алгоритмов, но не для всех.
- Последствия для проектирования: модульность, явные контрактные спецификации, ограничение негарантированных мощностей (например, избегание сложной динамической генерации кода в критичных модулях), использование формальных методов для критичных частей и комбинирование статического анализа с тестированием и мониторингом времени выполнения.
Вывод: фундаментальный теоретический предел (неразрешимость останова) не запрещает практическую верификацию, но требует компромиссов: ограничение класса программ, звуковые/неполные методы, интерактивные доказательства и эмпирические техники.