В теории вычислимости теорема Райса утверждает, что все нетривиальные семантические свойства программ неразрешимы . Семантическое свойство — это свойство о поведении программы (например, « завершается ли программа для всех входных данных?»), в отличие от синтаксического свойства (например, «содержит ли программа оператор if-then-else ?»). Нетривиальное свойство — это свойство, которое не является ни истинным для каждой программы, ни ложным для каждой программы.
Теорема обобщает неразрешимость проблемы остановки . Она имеет далеко идущие последствия для осуществимости статического анализа программ. Она подразумевает, что невозможно, например, реализовать инструмент, который проверяет, является ли данная программа корректной или даже выполняется без ошибок (можно реализовать инструмент, который всегда переоценивает или всегда недооценивает, например, корректность программы, поэтому на практике приходится решать, что является меньшей проблемой).
Теорема названа в честь Генри Гордона Райса , который доказал ее в своей докторской диссертации 1951 года в Сиракузском университете .
Теорема Райса устанавливает теоретические границы того, какие типы статического анализа могут быть выполнены автоматически. Можно различать синтаксис программы и ее семантику . Синтаксис — это детали того, как написана программа, или ее «намерение», а семантика — это то, как программа ведет себя при запуске, или ее «расширение». Теорема Райса утверждает, что невозможно определить свойство программ, которое зависит только от семантики, а не от синтаксиса, если только свойство не является тривиальным (истинным для всех программ или ложным для всех программ).
Согласно теореме Райса, невозможно написать программу, которая автоматически проверяет отсутствие ошибок в других программах, принимая в качестве входных данных программу и спецификацию и проверяя, удовлетворяет ли программа спецификации.
Это не означает невозможности предотвратить определенные типы ошибок. Например, теорема Райса подразумевает, что в динамически типизированных языках программирования , которые являются полными по Тьюрингу , невозможно проверить отсутствие ошибок типов. С другой стороны, статически типизированные языки программирования имеют систему типов, которая статически предотвращает ошибки типов. По сути, это следует понимать как особенность синтаксиса ( взятого в широком смысле) этих языков. Чтобы проверить тип программы, необходимо просмотреть ее исходный код; операция зависит не только от гипотетической семантики программы.
С точки зрения общей проверки программного обеспечения это означает, что хотя невозможно алгоритмически проверить, удовлетворяет ли данная программа заданной спецификации, можно потребовать, чтобы программы были аннотированы дополнительной информацией, которая доказывает, что программа корректна, или были написаны в определенной ограниченной форме, которая делает проверку возможной, и принимать только программы, которые проверяются таким образом. В случае безопасности типов первое соответствует аннотациям типов, а второе соответствует выводу типов . Рассматриваемая за пределами безопасности типов, эта идея приводит к доказательствам корректности программ с помощью аннотаций доказательств, таких как в логике Хоара .
Другой способ обойти теорему Райса — это поиск методов, которые ловят много ошибок, не будучи при этом полными. Это теория абстрактной интерпретации .
Еще одним направлением верификации является проверка моделей , которая применима только к конечным программам, а не к полным по Тьюрингу языкам.
Пусть φ — допустимая нумерация частично вычислимых функций . Пусть P — подмножество . Предположим, что:
Тогда P неразрешима .
Более краткое утверждение можно сделать в терминах индексных множеств : единственными разрешимыми индексными множествами являются ∅ и .
Для данной программы P , которая принимает натуральное число n и возвращает натуральное число P ( n ), следующие вопросы неразрешимы:
Предположим от противного, что — нетривиальное, экстенсиональное и вычислимое множество натуральных чисел. Существует натуральное число и натуральное число . Определим функцию с помощью когда и когда . По теореме Клини о рекурсии существует такое, что . Тогда, если , то имеем , что противоречит экстенсиональности , так как , и наоборот, если , то имеем , что снова противоречит экстенсиональности, так как .
Предположим для конкретности, что у нас есть алгоритм для проверки программы p и безошибочного определения, является ли p реализацией функции возведения в квадрат, которая принимает целое число d и возвращает d 2 . Доказательство работает так же хорошо, если у нас есть алгоритм для определения любого другого нетривиального свойства поведения программы (т. е. семантического и нетривиального свойства), и в общем виде приведено ниже.
Утверждение заключается в том, что мы можем преобразовать наш алгоритм для идентификации программ возведения в квадрат в тот, который идентифицирует функции, которые останавливаются. Мы опишем алгоритм, который принимает входные данные a и i и определяет, останавливается ли программа a при заданном входном значении i .
Алгоритм для решения этого концептуально прост: он конструирует (описание) новой программы t , принимающей аргумент n , которая (1) сначала выполняет программу a на входе i (и a , и i жестко закодированы в определении t ), и (2) затем возвращает квадрат n . Если a ( i ) выполняется вечно, то t никогда не доходит до шага (2), независимо от n . Тогда ясно, что t является функцией для вычисления квадратов тогда и только тогда, когда шаг (1) завершается. Поскольку мы предположили, что можем безошибочно идентифицировать программы для вычисления квадратов, мы можем определить, является ли t , которая зависит от a и i , такой программой; таким образом, мы получили программу, которая решает, останавливается ли программа a на входе i . Обратите внимание, что наш алгоритм решения об остановке никогда не выполняет t , а только передает ее описание программе идентификации возведения в квадрат, которая по предположению всегда завершается; Поскольку построение описания t может быть выполнено таким образом, что оно всегда заканчивается, решение об остановке также не может не остановиться.
останавливается (a,i) { определить т(н) { а(я) вернуть n×n } вернуть is_a_squaring_function(t) }Этот метод не зависит конкретно от способности распознавать функции, которые вычисляют квадраты; пока какая-то программа может делать то, что мы пытаемся распознать, мы можем добавить вызов к a для получения нашего t . У нас мог бы быть метод для распознавания программ для вычисления квадратных корней, или программ для вычисления ежемесячной заработной платы, или программ, которые останавливаются при получении входных данных "Abraxas"; в каждом случае мы могли бы решить проблему остановки аналогичным образом.
Для формального доказательства предполагается, что алгоритмы определяют частичные функции над строками и сами представлены строками. Частичная функция, вычисленная алгоритмом, представленным строкой a, обозначается F a . Это доказательство осуществляется методом reductio ad absurdum : мы предполагаем, что существует нетривиальное свойство, которое определяется алгоритмом, а затем показываем, что из этого следует, что мы можем решить проблему остановки , что невозможно, и, следовательно, противоречие.
Теперь предположим, что P ( a ) — это алгоритм, который определяет некоторое нетривиальное свойство F a . Без потери общности мы можем предположить, что P ( no-halt ) = "no", где no-halt является представлением алгоритма, который никогда не останавливается. Если это не так, то это справедливо для алгоритма P , который вычисляет отрицание свойства P . Теперь, поскольку P определяет нетривиальное свойство, следует, что существует строка b , которая представляет алгоритм F b и P ( b ) = "yes". Затем мы можем определить алгоритм H ( a , i ) следующим образом:
Теперь мы можем показать, что H решает проблему остановки:
Поскольку известно, что проблема остановки неразрешима, это противоречие, и предположение о том, что существует алгоритм P ( a ), который определяет нетривиальное свойство для функции, представленной a, должно быть ложным.