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

В вычислимости теории теорема Райса утверждает, что все нетривиальные семантические свойства программ неразрешимы . Семантическое ли программа все входные данные?»), в отличие от синтаксического свойство определяет поведение программы (например, « завершает свойства (например, «содержит ли программа оператор if-then-else ?»). свойство Нетривиальное — это свойство, которое не является ни истинным для каждой программы, ни ложным для каждой программы.

Теорема обобщает неразрешимость проблемы остановки . Это имеет далеко идущие последствия для возможности статического анализа программ. Это означает, что невозможно, например, реализовать инструмент, который проверяет, корректна ли данная программа или даже выполняется ли она без ошибок.

Теорема названа в честь Генри Гордона Райса , который доказал ее в своей докторской диссертации 1951 года в Сиракузском университете .

Введение

Теорема Райса устанавливает теоретическое ограничение того, какие типы статического анализа могут выполняться автоматически. Можно различать синтаксис программы и ее семантику . Синтаксис — это детали написания программы, или ее «намерение», а семантика — это то, как программа ведет себя при запуске, или ее «расширение». Теорема Райса утверждает, что невозможно определить свойство программ, которое зависит только от семантики, а не от синтаксиса, если только это свойство не является тривиальным (истинным для всех программ или ложным для всех программ).

По теореме Райса невозможно написать программу, которая автоматически проверяет отсутствие ошибок в других программах, принимая на вход программу и спецификацию и проверяя, удовлетворяет ли программа спецификации.

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

С точки зрения общей проверки программного обеспечения это означает, что, хотя невозможно алгоритмически проверить, удовлетворяет ли данная программа заданной спецификации, можно потребовать, чтобы программы были аннотированы дополнительной информацией, подтверждающей корректность программы, или чтобы они были написаны в определенной ограниченной форме. это делает верификацию возможной, и мы принимаем только те программы, которые проверены таким образом. В случае безопасности типов первое соответствует аннотациям типа, а второе — выводу типа . Выйдя за рамки типовой безопасности, эта идея приводит к доказательству корректности программ с помощью аннотаций доказательств, таких как логика Хоара .

Другой способ обойти теорему Райса — найти методы, которые обнаруживают множество ошибок, но при этом не являются полными. Это теория абстрактной интерпретации .

Еще одним направлением проверки является проверка модели , которая может применяться только к программам с конечным числом состояний, а не к тьюринг-полным языкам.

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

Пусть ф частично — допустимая нумерация функций вычислимых . Пусть P — подмножество $\mathbb {N}$ . Предположим, что:

P нетривиален ни : P не является ни пустым, $\mathbb {N}$ сам.
P является экстенсиональным : для всех целых чисел и n , если φ _m = φ _n , то m ∈ P ⟺ n ∈ P. m

Тогда P неразрешимо .

Более краткое утверждение можно сделать в терминах наборов индексов : единственные разрешимые наборы индексов — это ∅ и $\mathbb {N}$ .

Примеры

Учитывая программу P , которая принимает натуральное число n и возвращает натуральное число P ( n ), следующие вопросы неразрешимы:

Завершается ли P на данном n ? (Это проблема остановки .)
Оканчивается ли P на 0?
Оканчивается ли P на всех n (т. е. является ли P полным )?
Завершается ли P и возвращает 0 на каждом входе?
завершает P работу и возвращает 0 на каком-то входе?
завершает P работу и возвращает одно и то же значение для всех входов?
Эквивалентен ли P данной программе Q ?

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

Предположим от противного, что $P$ — нетривиальный, экстенсиональный и вычислимый набор натуральных чисел. Существует натуральное число $a\in P$ и натуральное число $b\notin P$ . Определить функцию $Q$ к $Q_{e}(x)=\varphi _{b}(x)$ когда $e\in P$ и $Q_{e}(x)=\varphi _{a}(x)$ когда $e\notin P$ . По рекурсивной теореме Клини существует $e$ такой, что $\varphi _{e}=Q_{e}$ . Тогда, если $e\in P$ , у нас есть $\varphi _{e}=\varphi _{b}$ , что противоречит экстенсиональности $P$ с $b\notin P$ и наоборот, если $e\notin P$ , у нас есть $\varphi _{e}=\varphi _{a}$ , что снова противоречит экстенсиональности, поскольку $a\in P$ .

Доказательство редукцией проблемы остановки

Эскиз доказательства

Предположим, для конкретности, что у нас есть алгоритм для проверки программы p и безошибочного определения, является ли p реализацией функции возведения в квадрат, которая принимает целое число d и возвращает d ². Доказательство работает так же хорошо, если у нас есть алгоритм для определения любого другого нетривиального свойства поведения программы (т.е. семантического и нетривиального свойства), и в общих чертах оно приведено ниже.

Утверждается, что мы можем преобразовать наш алгоритм идентификации программ возведения в квадрат в алгоритм, который идентифицирует останавливающиеся функции. Мы опишем алгоритм, который принимает входные данные 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 также может быть выполнено способом, который всегда завершается, решение об остановке также не может не остановиться.

 halts (a,i) {
   define t(n) {
     a(i)
     return n×n
   }
   return is_a_squaring_function(t)
 }

Этот метод не зависит конкретно от способности распознавать функции, вычисляющие квадраты; пока какая-то программа может делать то, что мы пытаемся распознать, мы можем добавить вызов 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 ) следующим образом:

1. построить строку t , которая представляет алгоритм T ( j ), такой, что

T сначала моделирует вычисление F _a ( i ),
затем T моделирует вычисление F _b ( j ) и возвращает результат.

2. вернуть P ( t ).

Теперь мы можем показать, что H решает проблему остановки:

Предположим, что алгоритм, представленный a , останавливается на входе i . В этом случае F _t = F _b и, поскольку P ( b ) = «да» и выход P ( x ) зависит только от F _x , отсюда следует, что P ( t ) = «да» и, следовательно, H ( a , я ) = «да».
Предположим, что алгоритм, представленный a, не останавливается на входе i . В этом случае F _t = F _no-halt , т. е. частичная функция, которая никогда не определена. Поскольку P ( no-halt ) = «нет» и выход P ( x ) зависит только от F _x , отсюда следует, что P ( t ) = «нет» и, следовательно, H ( a , i ) = «нет».

Поскольку известно, что проблема остановки неразрешима, это противоречие, и предположение о том, что существует алгоритм P ( a ), который определяет нетривиальное свойство функции, представленной a, должно быть ложным.

См. также

Проблема с остановкой
Теорема Райса–Шапиро и теорема Крейзеля-Лакомба-Шенфилда-Цейтина , обобщения теоремы Райса
Теорема Скотта – Карри , аналог теоремы Райса в лямбда-исчислении.
Доказательство Тьюринга

Ссылки

Хопкрофт, Джон Э .; Уллман, Джеффри Д. (1979), Введение в теорию автоматов, языки и вычисления , Аддисон-Уэсли , стр. 185–192.
Райс, Х.Г. (1953), «Классы рекурсивно перечислимых множеств и проблемы их решения», Transactions of the American Mathematical Society , 74 (2): 358–366, doi : 10.1090/s0002-9947-1953-0053041-6 , JSTOR 1990888
Роджерс, Хартли младший (1987), Теория рекурсивных функций и эффективная вычислимость (2-е изд.), McGraw-Hill , §14.8