Формальные языки
Разрешимость и неразрешимость
GitHub Copilot предлагает код. Coverity анализирует на баги. TypeScript проверяет типы. Всё это алгоритмы - и у всех есть граница. TypeScript иногда не может вывести тип и просит явную аннотацию. Coverity иногда выдаёт ложные срабатывания. Это не баги реализации - это математическая необходимость. Граница между разрешимым и неразрешимым определяет, где заканчивается 'можно автоматизировать' и начинается 'нужен человек'.
- **TypeScript type inference:** вывод типов частично неразрешим для полного Hindley-Milner с зависимыми типами. TypeScript намеренно ограничивает алгоритм вывода, делая его разрешимым ценой неполноты (некоторые правильные программы требуют явных аннотаций)
- **Coverity / PVS-Studio:** статические анализаторы используют abstract interpretation - консервативную аппроксимацию семантики программы. Ложные срабатывания неизбежны по теореме Райса: точная проверка любого непрямолинейного свойства неразрешима
- **Rust borrow checker:** конкретный алгоритм (NLL - Non-Lexical Lifetimes) решает разрешимый подкласс задачи проверки безопасности памяти. Некоторые правильные программы отвергаются - это цена разрешимости
- **TLA+ model checker:** проверяет свойства конечных моделей распределённых систем. Amazon использует для верификации S3, DynamoDB, EC2. Ограничение: конечное число состояний - обход неразрешимости через ограничение области
Разрешимые языки
Задача разрешима если существует алгоритм, который на любом входе останавливается и даёт правильный ответ. Не 'иногда останавливается', не 'останавливается на большинстве входов' - **всегда**. Язык L разрешим если существует МТ-децайдер: принимает w ∈ L и отвергает w ∉ L без зависания.
**Разрешимые языки (Decidable / Recursive):** для языка L существует МТ M такая, что для всех w ∈ Σ*: если w ∈ L, то M принимает w; если w ∉ L, то M отвергает w. M никогда не зависает. Разрешимые языки - подкласс распознаваемых (RE). Обозначение: Rec или DTIME(f(n)) для конкретной сложности.
Почему эти задачи разрешимы для DFA, но не для МТ? DFA **всегда останавливается** - симуляция конечна. МТ может зависнуть - симуляция может не завершиться. Переход от DFA к МТ - переход от разрешимости к потенциальной неразрешимости. Это фундаментальное различие между конечными автоматами и полными МТ.
Почему A_DFA = {<M, w> : DFA M принимает w} разрешим?
Распознаваемые языки (RE и co-RE)
Язык **распознаваемый (Turing-recognizable, RE)** если существует МТ, принимающая все его строки. На строках не из языка МТ может отвергать **или зависать**. Язык **co-RE** если его дополнение RE. Разрешимый = RE ∩ co-RE. Ключевой пример: A_TM = {<M, w> : M принимает w} распознаваем (запускаем M), но неразрешим.
**Dovetailing** - техника параллельной симуляции: для проверки w ∈ L₁ ∩ L₂ запускаем распознаватели M₁ и M₂ поочерёдно по одному шагу. Если оба принимают - принимаем. Если хотя бы один отвергает - отвергаем. Если один зависает - мы тоже зависаем. Dovetailing - основной инструмент для работы с RE-языками.
L ∈ RE и L̄ ∉ RE (дополнение не распознаваемо). Что можно сказать о L?
Методы доказательства неразрешимости
Два основных метода доказательства неразрешимости: **диагонализация** (прямое построение языка, противоречащего любому предполагаемому алгоритму) и **сведение** (если задача A сводится к задаче B, и A неразрешима, то B неразрешима). Диагонализация используется для halting problem, сведение - для всего остального.
**Mapping reduction (m-reduction):** функция f: Σ* → Σ* вычислима и для всех w: w ∈ A ⟺ f(w) ∈ B. Обозначение: A ≤m B. Если A ≤m B и B разрешима, то A разрешима. Если A ≤m B и A неразрешима, то B неразрешима. Это стандартный инструмент теории вычислимости и теории NP-полноты.
A ≤m B означает что A mapping-reduces к B. Если A неразрешима, что следует?
Карта разрешимых и неразрешимых задач
Понимание того, какие задачи разрешимы, критично для инженерной практики. Статические анализаторы, компиляторы, формальная верификация - всё работает в рамках разрешимых подзадач. Попытка решить неразрешимую задачу точно - обречена на неполноту или зависание.
| Задача | Разрешима? | Инструмент |
|---|---|---|
| DFA M принимает w | Да | Симуляция DFA |
| Язык DFA M пуст? | Да | DFS/BFS по состояниям |
| Два DFA эквивалентны? | Да | Произведение автоматов |
| КС-грамматика порождает w? | Да | CYK-алгоритм O(n³) |
| Язык КС-грамматики пуст? | Да | Перебор нетерминалов |
| МТ M принимает w? | Нет (A_TM) | Нет алгоритма |
| МТ M останавливается на w? | Нет (HALT_TM) | Нет алгоритма |
| Язык МТ M пуст? | Нет (E_TM) | Нет алгоритма |
| Программа P эквивалентна Q? | Нет (теорема Райса) | Нет алгоритма |
Статические анализаторы (Coverity, PVS-Studio, Facebook Infer) работают с **аппроксимациями**: они либо консервативны (могут давать ложные срабатывания, зато не пропускают ошибки) либо либеральны (могут пропускать ошибки, зато не ложные срабатывания). Точное решение невозможно - это прямое следствие теоремы Райса.
Формальная верификация может доказать что программа правильна в любом смысле
Формальная верификация доказывает соответствие программы формальной спецификации. Полнота ограничена: нельзя автоматически проверить произвольное свойство (теорема Райса)
TLA+ проверяет конечные модели систем. Coq доказывает теоремы о программах, написанных на его языке. SPIN верифицирует конечные протоколы. Все они работают в разрешимых подклассах. Общая задача 'докажи правильность произвольной программы' неразрешима.
Статический анализатор кода выдаёт предупреждение о возможном null pointer. Программист уверен, что ошибки нет. Почему оба могут быть правы?
Ключевые идеи
- **Разрешимый язык:** существует МТ, которая всегда останавливается и даёт правильный ответ. Три класса: Decidable ⊂ RE (распознаваемые) ⊂ все языки
- **Метод сведения:** A ≤m B + A неразрешима -> B неразрешима. Основной инструмент доказательства неразрешимости
- **Карта задач:** задачи о DFA разрешимы (DFA останавливается). Задачи о МТ - как правило неразрешимы (МТ может зависнуть)
- **Практическое следствие:** статические анализаторы используют аппроксимации. Точная проверка произвольного свойства программы неразрешима (теорема Райса)
Связанные темы
Разрешимость - фундамент теории вычислимости:
- Проблема остановки — Первый доказанный пример неразрешимой задачи - основа для всех сведений
- Теорема Райса — Обобщение: все нетривиальные семантические свойства программ неразрешимы
- Сведения — Mapping reduction - основной метод доказательства неразрешимости
Вопросы для размышления
- TypeScript иногда просит явную аннотацию типа там, где программист считает тип очевидным. Как это связано с разрешимостью вывода типов?
- Задача 'проверить, содержит ли программа бесконечный цикл' неразрешима. Как Rust избегает неразрешимости в borrow checker?
- Если формальная верификация программы принципиально ограничена, зачем её использовать в критических системах (ядерные реакторы, авионика)?