В теории вычислимости теорема Райса утверждает , что все нетривиальные семантические свойства программ неразрешимы . Семантическое свойство определяет поведение программы (например, « завершает ли программа все входные данные?»), в отличие от синтаксического свойства (например, «содержит ли программа оператор 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) { определить t(n) { а (я) вернуть n×n } вернуть is_a_squaring_function (т) }Этот метод не зависит конкретно от способности распознавать функции, вычисляющие квадраты; пока какая-то программа может делать то, что мы пытаемся распознать, мы можем добавить вызов a для получения нашего t . У нас мог бы быть метод распознавания программ для вычисления квадратных корней, или программ для расчета ежемесячной заработной платы, или программ, которые останавливаются при получении входных данных "Abraxas"; в каждом случае мы сможем решить проблему остановки аналогичным образом.
Для формального доказательства предполагается, что алгоритмы определяют частичные функции над строками и сами представляются строками. Частичная функция, вычисленная алгоритмом, представленная строкой a, обозначается F a . Это доказательство проводится методом доведения до абсурда : мы предполагаем, что существует нетривиальное свойство, которое определяется алгоритмом, а затем показываем, что из этого следует, что мы можем решить проблему остановки , что невозможно и, следовательно, противоречит.
Давайте теперь предположим, что P ( a ) — это алгоритм, который определяет какое-то нетривиальное свойство F a . Без ограничения общности мы можем предположить, что P ( no-halt ) = «нет», причем no-halt представляет собой представление алгоритма, который никогда не останавливается. Если это не так, то это справедливо для алгоритма P , который вычисляет отрицание свойства P. Теперь, поскольку P определяет нетривиальное свойство, отсюда следует, что существует строка b , которая представляет алгоритм F b и P ( b ) = «да». Затем мы можем определить алгоритм H ( a , i ) следующим образом:
Теперь мы можем показать, что H решает проблему остановки:
Поскольку известно, что проблема остановки неразрешима, это противоречие, и предположение о том, что существует алгоритм P ( a ), который определяет нетривиальное свойство функции, представленной a , должно быть ложным.