Вычислимость
Сложность и вычислимость на практике
«Почему мой линтер пропустил этот баг? Почему компилятор Rust не принял мой код?» - оба вопроса имеют один ответ: теорема Райса. Фундаментальные пределы вычислимости определяют, что может и не может делать инструментарий каждого разработчика.
- Rust borrow checker: sound analysis на основе теории типов
- ESLint/Pylint: неполный статический анализ с false positives
- Formal verification (Coq): доказательства правильности кода
- TypeScript: намеренно unsound для удобства разработчика
Теорема Райса: пределы статического анализа
**Теорема Райса:** Любое непростое семантическое свойство программ неразрешимо. Это значит: нет алгоритма, который для любой программы P правильно ответил бы, обладает ли P заданным свойством (кроме тривиальных «всегда да» / «всегда нет»).
**Следствие для разработчиков:** Статические анализаторы (ESLint, PMD, Coverity) используют приближения - sound (нет false negatives, но есть false positives) или complete (нет false positives, но пропускают баги). Полная точность недостижима.
Почему статические анализаторы не могут точно определить все memory leaks?
Проблема остановки в реальных системах
Несмотря на неразрешимость в общем случае, **приближённые решения** работают отлично на практике. Реальные системы используют ограниченные домены или эвристики.
**Coq и доказательства программ:** В Coq нельзя написать непроверяемую функцию - все функции должны завершаться. Это делает Coq неполным по Тьюрингу, зато все доказательства корректны. Компромисс: выразительность vs гарантии.
Почему Rust borrow checker иногда отклоняет валидный код?
Системы типов и их выразительность
**Иерархия выразительности** систем типов напрямую связана с вычислимостью. Чем выразительнее система - тем сложнее (или невозможнее) вывод типов.
**Практический вывод:** TypeScript намеренно не является sound - 'any' и type assertions позволяют «обмануть» тайп-чекер. Flow (от Facebook) тоже не sound. Полная корректность типов ценой удобства - выбор Haskell.
Чем выразительнее система типов, тем лучше язык: больше ошибок ловится на компиляции, больше инвариантов проверено.
Выразительность типов прямо упирается в неразрешимость вывода типов. Dependent types и system F-omega делают вывод неразрешимым (или экспоненциальным), поэтому промышленные языки (Rust, TypeScript) сознательно делают компромисс между мощностью и автоматическим выводом.
Интуиция «больше типов = безопаснее» верна для багов, но игнорирует стоимость: type inference в Haskell decidable, а в Coq/Agda требует ручных доказательств. TypeScript намеренно unsound (any, type assertions) именно потому что sound вариант сделал бы компиляцию невозможной на больших кодовых базах. Computability ставит жёсткий потолок поверх инженерных желаний.
Почему в System F вывод типов неразрешим?
Ключевые идеи
- Теорема Райса: любое непростое семантическое свойство программ - неразрешимо
- Статические анализаторы: либо sound (false positives), либо complete (false negatives)
- Иерархия систем типов: выразительность ↑ → разрешимость вывода ↓
- Hindley-Milner: золотой баланс - полный вывод типов и Turing-completeness
- Dependent types: максимальная выразительность, нетерминация запрещена
Связанные темы
Практическое применение теории вычислимости.
- Неразрешимость — Теорема Райса расширяет результаты о неразрешимости
- Сведения (Reductions) — Доказательства через сведение к Halting Problem
Вопросы для размышления
- Можно ли создать язык программирования, где все программы гарантированно завершаются? Какова будет цена?
- Почему Google использует Abseil (C++) вместо формальной верификации для критического кода?
- Как теорема Райса объясняет невозможность идеального антивируса?
Связанные уроки
- comp-09 — Неразрешимость - теоретическая основа для практических ограничений
- comp-12 — Сводимость показывает, какие практические задачи неразрешимы
- cplx-07 — NP-hard задачи: практические пределы, похожие на неразрешимость
- alg-22-backtracking — Когда верификатор существует - NP; когда нет - неразрешимость
- cplx-01