Проблема остановки

Гипотетическая программа-оракул HALT(code, input): принимает код программы и входные данные, возвращает True/False - остановится ли программа. Если бы такой оракул существовал, можно было бы создать идеальный отладчик, идеальный антивирус, идеальный статический анализатор. Тьюринг доказал в 1936: такой оракул математически невозможен. И это навсегда ограничивает то, что могут делать программы.

• **ThreadSanitizer (TSan):** инструмент Google для обнаружения гонок данных в C++. Работает как динамический анализатор (аппроксимация). Точное обнаружение всех race conditions - неразрешимо по теореме Райса. TSan ловит реальные гонки в ценой небольшого overhead в runtime
• **Rust ownership system:** borrow checker доказывает отсутствие race conditions и use-after-free для подкласса программ. Это разрешимая задача (конкретный алгоритм). Ценой является отказ некоторых правильных программ - это принципиальный trade-off
• **TLA+ у Amazon:** Jeff Bezos написал memo о применении TLA+ в 2014. AWS использует для верификации алгоритмов S3, DynamoDB, EC2. Ключевое: проверяются конечные модели (не произвольные программы) - обход через ограничение домена
• **Полиморфные вирусы:** вирусы, изменяющие свой код при каждом запуске. Антивирусы с сигнатурами не работают. Эмуляция в sandbox - аппроксимация: запускаем на ограниченное число шагов. Halting problem гарантирует: идеального детектора нет

Доказательство через диагонализацию

HALT = {<M, w> : МТ M останавливается на w}. Тьюринг доказал в 1936: не существует алгоритма, решающего HALT. Доказательство - шедевр: предположим такой алгоритм H существует, построим машину D, которая при запуске на описании себя самой порождает противоречие. Техника называется **диагонализацией** - отсылка к диагональному методу Кантора.

Структура доказательства: **reductio ad absurdum** с самореференцией. Программа D «смотрит» на себя через H и делает противоположное тому, что H предсказывает. Это невозможно - ни для одного H. Именно самореференция (D запускается на D) создаёт непреодолимое противоречие. Аналог парадокса лжеца: «это утверждение ложно».

Диагонализация: метод и идея

Метод **диагонализации** придумал Георг Кантор в 1891-м для доказательства несчётности действительных чисел. Идея: предположим список всех вещественных чисел [0,1]. Строим число d: d_i отличается от i-го числа в позиции i. Значит d не совпадает ни с одним числом в списке - список неполный. Тьюринг применил ту же идею к программам.

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

Следствия и практические последствия

Из неразрешимости HALT немедленно следуют другие неразрешимые задачи. **A_TM** = {<M, w> : M принимает w} неразрешима (HALT ≤m A_TM). **E_TM** = {<M> : L(M) = ∅} неразрешима. **EQ_TM** = {<M1, M2> : L(M1) = L(M2)} неразрешима. Все они доказываются сведением к HALT или A_TM.

Частичные решения и обходы

Неразрешимость HALT - не конец. На практике используются **ограниченные версии**: проверка остановки для подклассов программ (терминирующие рекурсивные схемы, программы без циклов с переменными границами). Инструменты: Coq, Agda (доказательство завершимости), Z3 (ограниченная верификация), CBMC (bounded model checking).

Главный практический инструмент - **ограничение домена**. Coq и Agda требуют, чтобы рекурсия была **структурной** - только уменьшающей размер аргументов. Это гарантирует завершимость для большого класса программ. Rust async/await, Erlang supervisor trees - архитектурные паттерны, обходящие проблему остановки через ограничение структуры.

Ключевые идеи

• **HALT неразрешима:** доказательство через диагонализацию. Предположить H -> построить D -> D(D) противоречит H -> H не существует
• **Диагонализация Кантора:** та же техника доказывает несчётность ℝ и теорему Гёделя о неполноте. Самореференция создаёт неразрешимое противоречие
• **Следствия:** A_TM, E_TM, EQ_TM неразрешимы. Нет идеального антивируса, статического анализатора, оптимизатора
• **Обходы:** ограничение класса программ (Coq), аппроксимация (TSan, Coverity), bounded model checking (CBMC). Всегда trade-off между полнотой и звучностью

Связанные темы

Проблема остановки - центральная теорема теории вычислимости:

• Сведения — HALT используется как базовая неразрешимая задача для сведений к другим задачам
• Теорема Райса — Обобщение HALT: любое непрямолинейное семантическое свойство неразрешимо - доказывается сведением от HALT
• Тезис Чёрча-Тьюринга — HALT неразрешима для любой разумной модели вычислений, не только МТ

Вопросы для размышления

• Python-функция может вызвать сама себя (рекурсия). Является ли это самореференцией в смысле доказательства Тьюринга? В чём разница?
• Coq принимает только структурно рекурсивные программы. Какой класс программ он отвергает, и является ли это принципиальным ограничением языка?
• Если HALT неразрешима, как работают инструменты типа Valgrind и AddressSanitizer? Что именно они обнаруживают и почему не 100%?

Связанные уроки

• comp-18-type-checking