Математическая логика
Теория вычислимости
Тьюринг в 1936 году доказал: есть вещи, которые нельзя вычислить. Это стало основой теоретической информатики. Диагональный аргумент Тьюринга и диагонализация Гёделя - один и тот же математический приём, примененный к разным объектам.
- Статический анализ кода (Coverity, PVS-Studio): полная верификация произвольных свойств невозможна, анализаторы работают только с разрешимыми аппроксимациями
- Антивирусные программы: полное определение вредоносного кода неразрешимо по теореме Райса, поэтому антивирусы используют эвристики
- Верификация аппаратуры (model checking): задача проверки моделей конечна и разрешима именно потому, что модели конечны; для бесконечных систем задача неразрешима
- Компиляторы: оптимизации типа устранения мёртвого кода в общем случае неразрешимы, реализуются только консервативные аппроксимации
Машины Тьюринга и проблема остановки
Алан Тьюринг в 1936 году доказал: не существует алгоритма, определяющего для произвольной программы и входных данных, остановится ли программа. Это первый формально доказанный предел вычислений. Результат получен одновременно с теоремами Гёделя и использует тот же диагональный метод.
Какой метод использует Тьюринг для доказательства неразрешимости HALT?
Тьюринг использует диагональный метод: конструирует машину D, делающую противоположное предсказанию гипотетического H при запуске на себе, создавая логическое противоречие - как парадокс лжеца в форме алгоритма.
Иерархия неразрешимости и теорема Райса
Не все неразрешимые задачи равносложны. Иерархия Клини-Мостовского (арифметическая иерархия) классифицирует подмножества натуральных чисел по сложности их определений: Sigma^0_1 (полуразрешимые), Pi^0_1 (косполуразрешимые), Sigma^0_2, и так далее. HALT принадлежит Sigma^0_1 - оно полуразрешимо, но не разрешимо.
Теорема Райса - мощный инструмент для доказательства неразрешимости. Любое непрямолинейное свойство P множеств слов, принимаемых машинами Тьюринга, неразрешимо. 'Непрямолинейное' означает: некоторые машины имеют это свойство, другие - нет. Следствие: автоматическая верификация произвольных программ невозможна.
Что утверждает теорема Райса?
Теорема Райса: если P - непрямолинейное свойство (P subset RE, P не пусто, P ne RE), то {<M> : L(M) in P} неразрешимо. Это делает автоматическую верификацию произвольных программ невозможной.
Итоги
- Машина Тьюринга: формальная модель вычислений, эквивалентная современным компьютерам (тезис Чёрча-Тьюринга)
- HALT неразрешима: диагональный метод - предположение о решателе H порождает машину D с самопротиворечивым поведением
- Полуразрешимость: HALT in RE (полуразрешима) - машина останавливается на 'да', но не обязана на 'нет'
- Теорема Райса: любое непрямолинейное семантическое свойство языков TM неразрешимо - автоматическая верификация невозможна в полном объёме
- m-сводимость A <=_m B: разрешимость B влечёт разрешимость A; HALT является Sigma^0_1-полной задачей
- Арифметическая иерархия: уровни Sigma^0_n, Pi^0_n, Delta^0_n классифицируют сложность вычислительных задач