Mapping Reductions

SonarQube не может гарантировать обнаружение всех SQL-инъекций. Rust borrow checker отклоняет некоторые безопасные программы. Ни один компилятор не может всегда определить бесконечный цикл. Это не баги - это теоремы. Теорема Райса доказывает: любой нетривиальный статический анализ программ неполон. Mapping reductions - математический аппарат который объясняет эти пределы и позволяет доказывать что одна задача 'не легче' другой.

• **Facebook Infer** - статический анализатор на Bi-abduction (приближение к недостижимому идеалу); обнаруживает утечки памяти и null dereferences; false negative rate ~20% - из-за теоремы Райса
• **Rust Borrow Checker** - разрешимое приближение к ownership analysis; отклоняет ~5% безопасных программ (false positives); ограничение из-за неразрешимости общей задачи
• **Google Closure Compiler** - type inference для JavaScript; приближённый анализ (undecidable точно); 'может' пропустить ошибки типов - это математически неустранимо

Сведение многие-к-одному (m-reducibility)

Доказано: проблема остановки (Halting Problem) неразрешима. Как доказать что другая задача тоже неразрешима? Инструмент - сведение (reduction): если задача A сводится к задаче B (A <=_m B), то из разрешимости B следует разрешимость A. Контрапозитивно: если A неразрешима, то B тоже неразрешима.

**m-reduction** (many-one reduction) A <=_m B: существует вычислимая функция f такая что x ∈ A <=> f(x) ∈ B. Свойства: транзитивность (A <=_m B, B <=_m C => A <=_m C); если B разрешима и A <=_m B, то A разрешима; если A неразрешима и A <=_m B, то B неразрешима.

Сведение по Тьюрингу (T-reducibility)

m-reduction строгая: f(x) отвечает на вопрос об A через один запрос к B. Иногда нужна более гибкая форма: алгоритм для A делает много запросов к оракулу B. Это Turing reduction (T-reduction) - более мощный, но менее структурированный инструмент.

**T-reduction** A <=_T B: машина Тьюринга с оракулом для B разрешает A. Оракул отвечает на вопрос '∈ B?' мгновенно. Разница: m-reduction - один запрос к B, ответ определяет принятие; T-reduction - произвольное число запросов, произвольная логика. Если A <=_m B то A <=_T B (обратное неверно). **HP <=_T HP-complement** (через T-reduction, но не через m-reduction).

RE-полнота и полнота по Post

Halting Problem не просто неразрешима - она **RE-полна**: любая полуразрешимая (r.e.) задача сводится к HP через m-reduction. HP - 'самая трудная' задача среди r.e. Аналогично: COMPLEMENT(HP) - co-RE-полна. Задачи выше RE образуют арифметическую иерархию.

**RE-complete**: A ∈ RE и для всех B ∈ RE: B <=_m A. **HP является RE-полной**: HP ∈ RE (универсальная МТ симулирует M на w) и для любой r.e. задачи L: L <=_m HP через стандартную конструкцию. Аналогично **EMPTINESS**, **EQUIVALENCE**, **REGULARITY** задач для МТ - RE или co-RE полны по теореме Райса.

Иерархия степеней неразрешимости

Не все неразрешимые задачи одинаково 'трудны'. HP неразрешима, но хотя бы полуразрешима (RE). Задача TOTALHP = {<M> | M останавливается на всех входах} неразрешима и не полуразрешима. Задача 'истинна ли теорема Гёделя?' ещё труднее. Существует бесконечная иерархия степеней неразрешимости.

**Арифметическая иерархия**: Σ_0 = Π_0 = Δ_0 = разрешимые. **Σ_1** = RE (полуразрешимые: существует вычислимое предикат). **Π_1** = co-RE. **Σ_2** = {A | A разрешима с HP-оракулом}. Σ_1 ⊂ Σ_2 ⊂ ... - строгие включения. HP является Σ_1-полной. TOTALHP является Π_2-полной.

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

• **m-reduction** A <=_m B: вычислимая f с x∈A <=> f(x)∈B; неразрешимость A => неразрешимость B; транзитивна
• **T-reduction** A <=_T B: алгоритм с B-оракулом; мощнее m-reduction (произвольно много запросов); A <=_m B => A <=_T B
• **Теорема Райса**: любое непрямолинейное свойство языка МТ неразрешимо; объясняет пределы статического анализа
• **Арифметическая иерархия**: Σ_1=RE (HP), Π_1=co-RE, Σ_2 (TOTALHP), ...; бесконечная иерархия степеней неразрешимости

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

Redutions - основной инструмент теории вычислимости:

• Арифметическая иерархия — Sigma_n и Pi_n классы строятся через оракульные редукции и уточняют структуру неразрешимых задач
• Разрешимость и полуразрешимость — RE и co-RE - основа иерархии; HP как прототип RE-полной задачи

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

• Теорема Райса говорит что определить 'завершается ли программа всегда' неразрешимо. Как тогда Rust ownership checker доказывает отсутствие use-after-free - разве это не свойство программы?
• SonarQube находит SQL-инъекции в Java коде. По теореме Райса это неразрешимо точно. Какую именно аппроксимацию делает Sonar и что пожертвовано ради разрешимости (soundness или completeness)?
• m-reduction A <=_m B доказывает что B не легче A. Но иногда нужно доказать что A и B одинаково трудны (m-эквивалентны). Как доказать что HP и ACCEPTANCE PROBLEM (принимает ли M слово w) m-эквивалентны?

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

• cplx-01