В теории вычислимости , теорема Райса утверждает , что все нетривиальные, семантические свойства программ неразрешимой . Семантическое свойство - это свойство поведения программы (например, завершается ли программа для всех входных данных), в отличие от синтаксического свойства (например, содержит ли программа оператор if-then-else ). Свойство является нетривиальным, если оно не истинно для каждой частично вычислимой функции или ложно для каждой частично вычислимой функции.
Теорема Райса также может быть выражена в терминах функций: для любого нетривиального свойства частичных функций ни один общий и эффективный метод не может решить, вычисляет ли алгоритм частичную функцию с этим свойством. Здесь свойство частичных функций называется тривиальным, если оно выполняется для всех частично вычислимых функций или ни для одной, а эффективный метод решения называется общим, если он принимает правильное решение для каждого алгоритма. Теорема названа в честь Генри Гордона Райса , который доказал ее в своей докторской диссертации 1951 года в Сиракузском университете .
Вступление
Пусть p - свойство формального языка , которое нетривиально, то есть
- существует рекурсивно перечислимый язык, обладающий свойством p ,
- существует рекурсивно перечислимый язык, не обладающий свойством p ,
(то есть p не является ни равномерно истинным, ни равномерно ложным для всех рекурсивно перечислимых языков).
Тогда для данной машины Тьюринга M невозможно определить, обладает ли распознаваемый ею язык - L (M) - свойством p .
На практике это означает, что не существует машины, которая всегда может решить, обладает ли язык данной машины Тьюринга определенным нетривиальным свойством. К особым случаям относятся, например, неразрешимость того, может ли язык, распознаваемый машиной Тьюринга, быть распознан нетривиальной более простой машиной, такой как конечный автомат (что означает, что непонятно, является ли язык машины Тьюринга регулярным ).
Важно отметить, что теорема Райса не касается свойств машин или программ; это касается свойств, функций и языков. Например, то, выполняет ли машина более 100 шагов на конкретном входе, является решаемым свойством, даже если это нетривиально. Две разные машины, распознающие один и тот же язык, могут потребовать разного количества шагов для распознавания одной и той же входной строки. Точно так же, имеет ли машина более 5 состояний, является решаемым свойством машины, так как количество состояний можно просто подсчитать. Для свойств такого рода, касающихся машины Тьюринга, но не распознаваемого ею языка, теорема Райса неприменима.
Используя характеристику приемлемых систем программирования Роджерса , теорему Райса можно по существу обобщить с машин Тьюринга на большинство языков компьютерного программирования : не существует автоматического метода, который бы решал в общем нетривиальные вопросы о поведении компьютерных программ.
В качестве примера рассмотрим следующий вариант проблемы остановки . Пусть P будет следующим свойством частичных функций F одного аргумента: P ( F ) означает, что F определено для аргумента «1». Это, очевидно, нетривиально, поскольку есть частичные функции, которые определены в 1, а другие не определены в 1. Проблема 1-остановки - это проблема определения любого алгоритма, определяет ли он функцию с этим свойством, т. Е. останавливается ли алгоритм на входе 1. По теореме Райса проблема 1-остановки неразрешима. Точно так же вопрос о том, завершается ли машина Тьюринга T на изначально пустой ленте (а не с начальным словом w, заданным в качестве второго аргумента в дополнение к описанию T , как в проблеме полной остановки), все еще остается неразрешенным.
Официальное заявление
Позволять обозначим натуральные числа , и пустьобозначают класс унарных (частичных) вычислимых функций. Позволятьбыть допустимой нумерации из вычислимых функций . Обозначим черезе й (частичная) вычислимая функция.
Мы идентифицируем каждое свойство, которым может обладать вычислимая функция, с подмножествомсостоящий из функций с этим свойством. Таким образом, учитывая набор, вычислимая функция имеет собственность если и только если . Для каждого объектаесть связанная проблема принятия решения о членстве определения, учитывая e , действительно ли.
Теорема Райса утверждает, что проблема решенияявляется разрешимым (также называется рекурсивным или вычислимой ) , если и только если или же .
Примеры
Согласно теореме Райса, если есть хотя бы одна частично вычислимая функция в конкретном классе частично вычислимых функций C и другая частично вычислимая функция не в C, то проблема определения того, вычисляет ли конкретная программа функцию в C, является неразрешимой. Например, теорема Райса показывает, что каждый из следующих наборов частично вычислимых функций неразрешим (то есть, набор не является рекурсивным или невычислимым ):
- Класс частично вычислимых функций, возвращающих 0 для каждого ввода, и его дополнение.
- Класс частично вычислимых функций, которые возвращают 0 по крайней мере для одного входа и его дополнения.
- Класс частично вычислимых постоянных функций и его дополнение.
- Класс частично вычислимых функций, которые идентичны заданной частично вычислимой функции, и его дополнение.
- Класс частично вычислимых функций, которые расходятся (т. Е. Не определены) для некоторого ввода, и его дополнение.
- Класс тотальных индексов вычислимых функций. [1]
- Класс индексов для рекурсивно перечислимых множеств , которые кофинитны.
- Класс индексов для рекурсивно перечислимых множеств, которые являются рекурсивными.
Доказательство теоремы Клини о рекурсии.
Следствие по рекурсии теоремы Клини утверждает , что для каждой нумерации Гёделя из вычислимых функций и каждой вычислимой функции, есть индекс такой, что возвращается . (Далее мы говорим, что "возвращается" если либо , или оба а также не определены.) Интуитивно - quine , функция, которая возвращает собственный исходный код (число Гёделя), за исключением того, что вместо того, чтобы возвращать его напрямую, передает свой номер Гёделя в и возвращает результат.
Позволять - набор вычислимых функций такой, что . Тогда есть вычислимые функции а также . Предположим, что набор индексов такой, что разрешима; тогда существует функция что возвращается если , а также иначе. По следствию теоремы о рекурсии существует индекс такой, что возвращается . Но тогда, если, тогда та же функция, что и , и поэтому ; и если, тогда является , и поэтому . В обоих случаях получаем противоречие.
Доказательство редукцией от проблемы остановки
Доказательство эскиза
Предположим, для конкретности, что у нас есть алгоритм для исследования программы p и безошибочного определения того, является ли p реализацией функции возведения в квадрат, которая принимает целое число d и возвращает d 2 . Доказательство работает так же хорошо, если у нас есть алгоритм для определения любого другого нетривиального свойства поведения программы (то есть семантическое и нетривиальное свойство), и в общих чертах оно дается ниже.
Утверждается, что мы можем преобразовать наш алгоритм идентификации программ возведения в квадрат в алгоритм, который идентифицирует останавливающиеся функции. Мы опишем алгоритм, который принимает входные данные a и i и определяет, останавливается ли программа при задании входа 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) { определить t (n) { а (я) вернуть 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 определяет нетривиальное свойство, отсюда следует, что существует строка 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 , i ) = "да".
- Предположим, что алгоритм, представленный a , не останавливается на входе i . В этом случае F t = F no-halt , т. Е. Частичная функция, которая никогда не определяется. Поскольку P ( no-halt ) = «no», а вывод P ( x ) зависит только от F x , отсюда следует, что P ( t ) = «no» и, следовательно, H ( a , i ) = «no».
Поскольку известно, что проблема остановки неразрешима, это противоречие, и предположение, что существует алгоритм P ( a ), который определяет нетривиальное свойство для функции, представленной a, должно быть ложным.
Теорема Райса и индексные множества
Теорема Райса может быть кратко сформулирована в терминах индексных множеств:
Позволять быть классом частично рекурсивных функций с набором индексов . потомявляется рекурсивным , если и только если или же .
Здесь - множество натуральных чисел , включая ноль .
Аналог теоремы Райса для рекурсивных множеств
Можно рассматривать теорему Райса как утверждение о невозможности эффективно решить для любого рекурсивно перечислимого множества, обладает ли оно определенным нетривиальным свойством. [2] В этом разделе мы приведем аналог теоремы Райса для рекурсивных множеств , а не рекурсивно перечислимых множеств. [3] Грубо говоря, аналог говорит, что если можно эффективно определить для каждого рекурсивного множества, имеет ли оно определенное свойство, то только конечное число целых чисел определяет, обладает ли рекурсивное множество этим свойством. Этот результат аналогичен исходной теореме Райса, поскольку оба результата утверждают, что свойство является «разрешимым» только в том случае, если можно определить, обладает ли набор этим свойством, исследуя не более конечного числа (нет , для исходной теоремы), если принадлежит набору.
Позволять быть классом (называемым простой игрой и рассматриваемым как свойство) рекурсивных множеств. Если является рекурсивным множеством, то для некоторых , вычислимая функция - характеристическая функция . Мы называемхарактеристический показатель для. (Таких бесконечно много.) Допустим, класс является вычислимой , если существует алгоритм (вычислимая функция) , которая решает для любого целого неотрицательного (не обязательно характеристический индекс),
- если является характеристическим индексом для рекурсивного множества, принадлежащего , то алгоритм дает «да»;
- если является характеристическим индексом для рекурсивного множества, не принадлежащего , то алгоритм дает «нет».
Множество расширяет строку нулей и единиц, если для каждого (длина ), й элемент равно 1, если ; и 0 в противном случае. Например, расширяет строку . Строкабудет выигрывать определения , если каждое рекурсивное множество расширения принадлежит . Строкаявляется потеря определения , если нет рекурсивного множества продлив принадлежит .
Теперь мы можем сформулировать следующий аналог теоремы Райса (Kreisel, Lacombe, and Shoenfield, 1959, [4] Kumabe and Mihara, 2008 [5] ):
Класс рекурсивных множеств вычислимо тогда и только тогда, когда существует рекурсивно перечислимое множество потери определяющих строк и рекурсивно перечислимого набора выигрышных определяющих строк, так что каждый рекурсивный набор расширяет строку в .
Этот результат был применен к фундаментальным проблемам вычислительного социального выбора (в более широком смысле, алгоритмической теории игр ). Например, Kumabe и Михару (2008, [5] 2008 [6] ) этот результат применяется к исследованию чисел Nakamura для простых игр в кооперативной теории игр и теории общественного выбора .
Смотрите также
- Теоремы Гёделя о неполноте
- Проблема с остановкой
- Теория рекурсии
- Теорема Райса – Шапиро
- Теорема Скотта – Карри , аналог теоремы Райса в лямбда-исчислении
- Доказательство Тьюринга
- Витгенштейн о правилах и частном языке
Заметки
- ^ Соаре, Роберт I. (1987). Рекурсивно перечислимые множества и степени . Springer. п. 21 .
- ^ Наборявляется перечислимым , если для некоторых , где это домен (набор входов такой, что определяется) из . Результат для рекурсивно перечислимых множеств может быть получен из результата для (частичных) вычислимых функций путем рассмотрения класса, где является классом рекурсивно перечислимых множеств.
- ^ Рекурсивно перечислимый наборявляется рекурсивным, если его дополнение рекурсивно перечислимо. Эквивалентно, рекурсивно, если его характеристическая функция вычислима.
- ^ Kreisel, G .; Lacombe, D .; Шенфилд-младший (1959). «Частично рекурсивные функционалы и эффективные операции». В Heyting, A. (ed.). Конструктивность в математике . Исследования по логике и основам математики. Амстердам: Северная Голландия. С. 290–297.
- ^ а б Кумабе, М .; Михара, HR (2008). «Вычислимость простых игр: характеристика и приложение до сути» . Журнал математической экономики . 44 (3–4): 348–366. arXiv : 0705.3227 . DOI : 10.1016 / j.jmateco.2007.05.012 .
- ^ Кумабе, М .; Михара, HR (2008). «Числа Накамуры для вычислимых простых игр» . Социальный выбор и благосостояние . 31 (4): 621. arXiv : 1107.0439 . DOI : 10.1007 / s00355-008-0300-5 .
Рекомендации
- Хопкрофт, Джон Э .; Ульман, Джеффри Д. (1979), Введение в теорию автоматов, языки и вычисления , Addison-Wesley , стр. 185–192.
- Райс, HG (1953), "Классы рекурсивно перечислимых множеств и их проблемы решения", Труды Американского математического общества , 74 (2): 358-366, DOI : 10,1090 / s0002-9947-1953-0053041-6 , JSTOR 1990888
- Роджерс, Хартли мл. (1987), Теория рекурсивных функций и эффективной вычислимости (2-е изд.), McGraw-Hill , §14.8
Внешние ссылки
- Вайсштейн, Эрик В. «Теорема Райса» . MathWorld .