Введение

Теорема в теории вычислимости
В теории вычислимости теорема Райса утверждает, что все нетривиальные семантические свойства программ являются неразрешимыми. Семантическое свойство – это свойство, относящееся к поведению программы (например, "завершается ли программа для всех входных данных?"), в отличие от синтаксического свойства (например, "содержит ли программа оператор if-then-else?"). Нетривиальное свойство – это свойство, которое не является истинным для всех программ и не является ложным для всех программ. Теорема обобщает неразрешимость проблемы останова. Она имеет далеко идущие последствия для возможности статического анализа программ. Она подразумевает, что невозможно, например, создать инструмент, который проверяет, является ли данная программа корректной, или даже выполняется без ошибок. Теорема названа в честь Генри Гордона Райса, который доказал её в своей докторской диссертации 1951 года в Сиракузском университете.

Введение

Теорема Райса устанавливает теоретический предел для типов статического анализа, которые могут быть выполнены автоматически. Можно различать синтаксис программы и ее семантику. Синтаксис – это детали того, как программа написана, или ее «интенция», а семантика – это поведение программы при выполнении, или ее «экстенсия». Теорема Райса утверждает, что невозможно определить свойство программы, которое зависит только от семантики и не зависит от синтаксиса, если только это свойство не является тривиальным (истинным для всех программ или ложным для всех программ). Согласно теореме Райса, невозможно написать программу, которая автоматически проверяет отсутствие ошибок в других программах, принимая программу и спецификацию в качестве входных данных и проверяя, удовлетворяет ли программа спецификации. Это не означает, что предотвратить определенные типы ошибок невозможно. Например, теорема Райса подразумевает, что в динамически типизированных языках программирования, являющихся Тьюринг-полными, невозможно проверить отсутствие ошибок типов. С другой стороны, статически типизированные языки программирования обладают системой типов, которая статически предотвращает ошибки типов. По сути, это следует понимать как особенность синтаксиса (в широком смысле) этих языков. Для проверки типов программы необходимо проверять ее исходный код; эта операция не зависит исключительно от гипотетической семантики программы. В контексте общей верификации программного обеспечения это означает, что, хотя алгоритмически проверить, соответствует ли данная программа данной спецификации, невозможно, можно требовать, чтобы программы были снабжены дополнительной информацией, доказывающей их корректность, или были написаны в определенной ограниченной форме, делающей верификацию возможной, и принимать только верифицированные таким образом программы. В случае типобезопасности первое соответствует аннотациям типов, а второе – выводу типов. Выходя за рамки типобезопасности, эта идея приводит к доказательствам корректности программ посредством аннотаций доказательств, как, например, в логике Хоара. Другой способ обойти теорему Райса – поиск методов, обнаруживающих множество ошибок, но не являющихся полными. Это теория абстрактной интерпретации. Еще одним направлением верификации является проверка моделей, которая применима только к программам с конечным числом состояний, а не к Тьюринг-полным языкам.

Официальное заявление

Пусть φ — допустимая нумерация частично вычислимых функций. Пусть P — подмножество . Предположим, что: P нетривиально: P не пусто и не равно самому себе. P экстенсионально: для всех целых чисел m и n, если φm = φn, то m ∈ P тогда и только тогда, когда n ∈ P. Тогда P неразрешимо. Более краткое утверждение можно сформулировать в терминах множеств индексов: единственными разрешимыми множествами индексов являются ∅ и .

Доказательство теоремы рекурсии Клине

Предположим для противоречия, что является нетривиальным, экстенсиональным и вычислимым множеством натуральных чисел. Существует натуральное число *n* и натуральное число *m*. Определим функцию *f* следующим образом: *f(x) = n*, когда *x = m*, и *f(x) = m*, когда *x ≠ m*. По теореме рекурсии Клини, существует такое *e*, что *f(e) = f(f(e))*. Тогда, если *e = m*, у нас есть *f(e) = n*, а *f(f(e)) = f(n) = m*, что противоречит экстенсиональности *f*, поскольку *n ≠ m*, и наоборот, если *e ≠ m*, у нас есть *f(e) = m*, а *f(f(e)) = f(m) = n*, что снова противоречит экстенсиональности, поскольку *m ≠ n*.