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

1951 год. Henry Gordon Rice, аспирант Сиракузского университета, публикует результат из двух страниц. Вывод: нельзя написать программу, которая проверяет любое непрямолинейное свойство другой программы. Ни одно. Ни завершается ли она, ни что вычисляет, ни содержит ли баг. Через 70 лет GitHub Copilot генерирует код - но не может проверить, правилен ли он. GPT-4 пишет функции, но не гарантирует их корректность. Claude анализирует программы, но не может дать точный ответ на семантический вопрос. Не потому что плохо обучены. Потому что теорема Райса 1951 + теорема Тьюринга 1936 = математический запрет.

• GitHub Copilot не может верифицировать собственный вывод - undecidability в продакшне: любая попытка точной проверки семантики упирается в теорему Райса
• Антивирус Kaspersky: эвристика = намеренное нарушение полноты из-за теоремы Райса; точное определение 'является ли программа вредоносной' - неразрешимо
• LLVM constant folding работает потому что это syntactic (structural) свойство, а не semantic - теорема Райса не применяется
• Формальная верификация (TLA+, Coq): работает только для конечных state spaces или с явными доказательствами завершения от программиста

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

1953 год. Статья Rice выходит в Transactions of the American Mathematical Society. Первый шаг: формализовать, что значит 'свойство программы'. Синтаксическое свойство - видно в тексте: длина кода, наличие цикла while, количество функций. Семантическое свойство - зависит от того, что программа вычисляет: завершается ли на всех входах, возвращает ли чётные числа, эквивалентна ли другой программе. Граница принципиальна. Синтаксические свойства разрешимы - парсер справится. Семантические - нет.

**Формальное определение через index sets.** Пусть $\varphi_i$ - программа с номером $i$ (по нумерации Гёделя). Свойство P задаёт множество индексов $\mathcal{C} = \{i \mid \varphi_i \text{ имеет свойство P}\}$. Свойство **семантическое**, если $\mathcal{C}$ - index set: $\varphi_i = \varphi_j \Rightarrow (i \in \mathcal{C} \Leftrightarrow j \in \mathcal{C})$. Две программы, вычисляющие одно и то же, либо обе имеют свойство, либо обе нет.

Тест: является ли свойство семантическим? Спросить: если взять две программы с одинаковым поведением на всех входах, одинаково ли это свойство для обеих? Если да - семантическое. Если нет (одна с циклом, другая без, но результат тот же) - синтаксическое.

Непрямолинейность и доказательство теоремы Райса

Второй шаг: непрямолинейность. Свойство P является **тривиальным**, если оно истинно для всех программ или ложно для всех. Тривиальные свойства разрешимы - ответ всегда один и тот же, алгоритм: 'всегда возвращать true' или 'всегда возвращать false'. Непрямолинейное свойство: хотя бы одна программа имеет его, хотя бы одна - нет. **Теорема Райса**: если P непрямолинейное семантическое свойство программ, то задача 'имеет ли программа M свойство P' неразрешима.

Доказательство предполагает случай P(пустая_функция) = false. Если P(пустая_функция) = true, конструкция симметрична: берём M_no с P(M_no) = false, строим G_Mx которая ведёт себя как пустая функция если M(x) завершается, и как M_no иначе. Оба случая редуцируются к HALT.

Расширения: Rice-Shapiro и связи с теоремой Гёделя

Теорема Райса - начало, не конец. Rice-Shapiro (1959) уточняет: для полуразрешимых (RE) свойств частичных рекурсивных функций разрешимость наступает тогда и только тогда, когда свойство монотонно и компактно. Интуиция: можно проверить, что функция делает на конечном числе входов - нельзя проверить, что она делает на всех. Параллельно: теоремы о неполноте Гёделя (1931) и теорема Райса (1951) - два проявления одного ограничения. Гёдель: в формальной системе есть истины без доказательства. Райс: в вычислениях есть свойства без алгоритма проверки.

**Теорема Райса для оракулов.** Если добавить оракул для задачи H (HALT), теорема Райса по-прежнему работает для свойств программ с H-оракулом: любое непрямолинейное свойство H-вычислимых функций неразрешимо относительно H. Иерархия Поста строит бесконечную лестницу: каждый уровень имеет неразрешимые свойства, не решаемые оракулом предыдущего уровня.

Применения: антивирусы, верификаторы, нейросети

Теорема Райса не академический артефакт - она объясняет архитектурные решения реальных систем. Антивирус не может точно определить вредоносность - вместо этого эвристики и сигнатуры (false negatives неизбежны). LLVM static analyzer находит ~60% реальных багов за счёт false positives: soundness выбрана вместо completeness. Type checkers (TypeScript, mypy) sound: отвергают некоторые корректные программы, но принимают только безопасные. Ни один из этих инструментов не нарушает теорему Райса - все работают с ограниченным классом свойств или с аппроксимациями.

**LLVM и constant folding.** Constant folding (`2 + 3 -> 5` в compile time) работает несмотря на теорему Райса - потому что это синтаксическое преобразование. Компилятор видит в AST два числа и оператор - это структура, не поведение. Семантика не нужна. Теорема Райса запрещает только семантические проверки; структурные трансформации по-прежнему разрешимы.

Практический диагностический вопрос: инструмент проверяет что-то, что нельзя увидеть без запуска программы? Если да - он либо неполный, либо не всегда точен. Это не баг инструмента - это математическое следствие теоремы Райса.

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

• **Семантическое свойство** - зависит от того, что вычисляет программа (функция), а не от её синтаксической структуры
• **Непрямолинейность** - свойство P непрямолинейно, если хотя бы одна программа имеет P и хотя бы одна - не имеет
• **Теорема Райса** - любое непрямолинейное семантическое свойство программ неразрешимо; доказывается редукцией от Halting Problem
• **Практический вывод** - статические анализаторы, антивирусы, компиляторы работают с аппроксимациями: soundness vs completeness - компромисс, вынужденный математически

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

• IDE подсвечивает ошибки типов - это не нарушает теорему Райса? Почему type checking разрешим, а проверка семантики - нет?
• LLVM находит dead code в простых случаях. Как это соотносится с теоремой Райса - она ведь говорит, что это невозможно?
• Формальная верификация (Coq, TLA+) работает и доказывает свойства программ. Где граница между тем, что верификация может и не может?

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

• comp-04
• comp-01
• comp-02
• comp-03
• cplx-05
• fl-05-regex
• alg-01-big-o
• fl-01-intro