Вычислимость
Проблема остановки
1936 год. Алан Тьюринг, 23 года, публикует статью 'On Computable Numbers'. Внутри - доказательство того, что существуют математические задачи, которые никакой компьютер никогда не сможет решить. Ни один. Ни через миллиард лет. Это не технические ограничения - это математическая невозможность. Проблема остановки: нельзя написать программу, которая для произвольной программы P и входа X определит, завершится ли P(X) или будет работать вечно. Инструменты верификации ПО, компиляторы, анализаторы кода - все упираются в это фундаментальное ограничение.
- **Static analysis**: Coverity, SonarQube не могут гарантировать отсутствие бесконечных циклов - это следствие Halting Problem
- **Антивирусы**: определить является ли программа вирусом в общем случае - неразрешимо (Rice's Theorem)
- **Компиляторы**: dead code elimination гарантированно не может найти весь мёртвый код
- **Формальная верификация**: Coq, Isabelle обходят ограничение требуя от программиста доказательств завершения
Тьюринг, Гёдель и предел вычислимости
В 1931 году Курт Гёдель доказал теоремы о неполноте: в достаточно мощной формальной системе существуют истинные утверждения, которые нельзя доказать. В 1936 году Алан Тьюринг независимо показал вычислительный аналог: существуют хорошо определённые задачи, которые нельзя решить алгоритмически. Его машина Тьюринга стала формальным определением 'алгоритма'. Доказательство неразрешимости Halting Problem использует диагонализацию Кантора - технику 1891 года для доказательства несчётности вещественных чисел. Тьюрингу было 23 года. Статья была написана ДО того, как существовали реальные компьютеры.
Доказательство неразрешимости Halting Problem
Halting Problem: существует ли алгоритм HALT(P, X), который для любой программы P и входа X возвращает true если P(X) завершается, и false если P(X) работает вечно?
**Структура доказательства:** Предположение (HALT существует) -> Конструкция (PARADOX) -> Применение к себе (PARADOX(PARADOX)) -> Противоречие в обоих случаях -> Опровержение предположения. Это Proof by Contradiction через Self-reference. Та же структура что и в парадоксе Рассела (множество всех множеств, не содержащих себя).
PARADOX(PARADOX) вызывает HALT(PARADOX, PARADOX). HALT возвращает false (предсказывает зависание). Что делает PARADOX дальше?
Диагонализация: техника доказательства
Диагонализация - техника Кантора (1891) для доказательства несчётности. В вычислимости: конструируем объект отличный от всех объектов счётного списка.
**Программы счётны, функции - нет.** Программы - конечные строки, их счётно много. Функции f: N -> {0,1} - несчётно много (мощность континуума). Значит, большинство функций невычислимы - нет программы для их вычисления. Halting Problem - конкретный пример невычислимой функции с практическим значением.
Почему в доказательстве Halting Problem PARADOX применяется к самому себе (PARADOX(PARADOX)), а не к произвольному входу?
Self-Reference и рекурсионная теорема
Self-reference - программа, которая использует собственный код как данные. Рекурсионная теорема Клини гарантирует, что такие программы всегда можно построить.
Quine - программа, выводящая собственный исходный код. Как это связано с доказательством Halting Problem?
Классы разрешимости
Теория вычислимости классифицирует задачи по разрешимости: decidable (всегда останавливается с ответом), semi-decidable (останавливается на 'да'), и undecidable (нет алгоритма).
**Практический вывод:** Статические анализаторы, компиляторы и верификаторы сталкиваются с теоремой Райса. Они используют аппроксимации: over-approximation (находят больше ошибок, включая false positives) или under-approximation (только гарантированные ошибки, пропускают часть). Абсолютной точности нет - это математический факт.
Если программа долго работает, значит она зависла - нужно убить процесс
Нельзя определить по конечному времени выполнения, завершится ли программа. Это следствие Halting Problem.
Для любого порога времени T существует программа, которая завершается после T+1 секунды. Нет алгоритма, который отличит 'долго работающую но завершимую' программу от 'бесконечной'. Поэтому kill по timeout - эвристика, а не решение.
Компания разрабатывает 'идеальный' статический анализатор, который точно определяет все бесконечные циклы. Почему это невозможно по теории вычислимости?
Ключевые идеи
- **Halting Problem**: не существует алгоритма HALT(P, X), который для произвольных P и X определит, завершится ли P(X)
- **Диагонализация**: техника доказательства - конструируем программу-парадокс, противоречащую предположению о существовании HALT
- **Self-reference**: парадокс лжеца в вычислительном контексте - программа применяет HALT к самой себе
- **Undecidable**: класс задач, для которых не существует алгоритма. Полуразрешимые (RE) - алгоритм останавливается на 'да', но может зависнуть на 'нет'
- **Rice's Theorem**: любое непрямолинейное семантическое свойство программ - неразрешимо
Вопросы для размышления
- Как Halting Problem объясняет, почему компиляторы не могут гарантированно найти весь мёртвый код?
- Теорема Райса говорит, что любое непрямолинейное семантическое свойство программ неразрешимо. Но antivirus-ы работают. Как они обходят это ограничение?
- Диагонализация Кантора доказала несчётность вещественных чисел в 1891. Тьюринг использовал ту же технику в 1936. Как именно они связаны?