Теорема Райса

2004 год. Facebook запускает статический анализатор Infer. Они обнаруживают тысячи реальных багов в коде iOS и Android приложений. Но Infer также выдаёт ложные срабатывания. Инженеры тратят время на разбор предупреждений, которые не являются ошибками. Это не недостаток реализации Infer - это математическая теорема 1953 года.

• **Facebook Infer:** статический анализатор на базе Bi-abduction (форма abstract interpretation). Используется в Meta для анализа миллионов строк кода. Находит реальные утечки памяти и null pointer. Ложные срабатывания неизбежны по теореме Райса
• **Антивирусные движки (VirusTotal):** более 70 антивирусных движков проверяют файлы. Разные движки дают разные ответы на одном файле - потому что каждый использует разную аппроксимацию неразрешимого свойства
• **TypeScript strict mode:** без strict mode TypeScript часто выводит 'any', пропуская ошибки типов (liberal). С strict mode требует явных аннотаций там, где вывод невозможен (conservative). Выбор между полнотой и звучностью
• **Rust compiler error messages:** Rust borrow checker - возможно лучшие сообщения об ошибках в компиляторах. Команда Rust вложила огромные усилия именно потому, что borrow checker отвергает больше программ чем необходимо - ложные 'ошибки' нужно объяснять

Семантические свойства программ

**Семантическое свойство** программы P - свойство, зависящее от того, что P вычисляет (её языка L(M)), а не от того, как она написана (синтаксиса). Примеры: 'P принимает строку w', 'P принимает хотя бы одну строку', 'P вычисляет функцию f'. Эти свойства не зависят от конкретного кода - только от поведения.

Нетривиальные свойства

Свойство P называется **нетривиальным** если существует хотя бы одна программа с этим свойством и хотя бы одна программа без него. Тривиальные свойства: 'программа является программой' (все программы), 'программа сортирует числа эффективнее O(1)' (ни одна программа). Тривиальные свойства разрешимы прямолинейно - всегда 'да' или всегда 'нет'.

**Теорема Райса (1953):** любое непрямолинейное свойство языка МТ (семантическое свойство) неразрешимо. Формально: пусть P - непрямолинейное свойство частично вычислимых функций (т.е. существует МТ M1 с этим свойством и M2 без него). Тогда язык {<M> : M имеет свойство P} неразрешим.

Доказательство теоремы Райса

Доказательство через сведение от A_TM. Пусть P - непрямолинейное свойство. Пусть M_empty - машина с L(M_empty) = ∅. Два случая: ∅ не имеет свойства P (или имеет). В обоих случаях строится вычислимая функция f такая, что M принимает w ⟺ f(<M, w>) имеет свойство P.

Идея: конструкция M_f «переносит» вопрос «принимает ли M строку w» на вопрос «имеет ли M_f свойство P». M_f - это программа, которая 'запоминает' M и w в своём коде и использует их чтобы принять решение о своём языке. Та же техника что в доказательстве неразрешимости E_TM.

Приложения теоремы Райса

Теорема Райса - это теоретическая граница для **всей индустрии инструментов анализа кода**. Она объясняет фундаментальные ограничения, с которыми разработчики сталкиваются ежедневно, не зная их причины.

Практический вывод из теоремы Райса: **полнота, звучность, завершаемость** - выбрать можно не все три. Звучный (sound) анализатор: не пропускает реальных ошибок, но может давать ложные. Полный (complete): не даёт ложных, но может пропустить. Завершаемый: всегда останавливается. Нет инструмента, обладающего всеми тремя для произвольных программ.

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

• **Теорема Райса:** любое непрямолинейное семантическое свойство программы неразрешимо. Непрямолинейное = есть программы с этим свойством И без него
• **Доказательство:** сведение от A_TM. Строится M_f, которая 'переносит' вопрос о принятии w на вопрос о свойстве языка
• **Семантическое vs синтаксическое:** синтаксические свойства (структура кода) разрешимы. Семантические (поведение) - по теореме Райса нет
• **Практическое следствие:** нет идеального (звучного + полного + завершимого) анализатора для произвольных программ. Инструменты выбирают компромисс

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

Теорема Райса - обобщение неразрешимости для всех свойств программ:

• Сведения — Теорема Райса доказывается через mapping reduction от A_TM
• Разрешимость — Синтаксические свойства разрешимы; теорема Райса - граница для семантических
• Формальная верификация — TLA+, Coq, SPIN работают в разрешимых подклассах - обход ограничений теоремы Райса

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

• TypeScript иногда выводит тип 'any' вместо конкретного. Является ли это нарушением теоремы Райса или её подтверждением?
• Rust borrow checker отвергает правильный код. Является ли это семантическим или синтаксическим свойством? Почему Rust не может быть одновременно sound и complete?
• Можно ли обойти теорему Райса, ограничив язык программирования? Какие языки это делают и какую цену платят?

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

• comp-05