Теорема Клини о рекурсии - Kleene's recursion theorem

В теории вычислимости , теорема рекурсии Клини является парой основных результатов о применении вычислимых функций к их собственным описаниям. Эти теоремы были впервые доказаны Стивеном Клини в 1938 году и появились в его книге 1952 года « Введение в метаматематику» . Родственная теорема, которая строит неподвижные точки вычислимой функции, известна как теорема Роджерса и принадлежит Хартли Роджерсу младшему .

Теоремы о рекурсии могут применяться для построения фиксированных точек определенных операций над вычислимыми функциями , для генерации quines и для построения функций, определенных с помощью рекурсивных определений .

Обозначение

Утверждение теоремы относится к допустимой нумерации из частично рекурсивных функций , таким образом, что функция , соответствующая индекс является . ${\ displaystyle \ varphi}$${\ displaystyle e}$${\ displaystyle \ varphi _ {e}}$

Если и являются частичными функциями от натуральных чисел, обозначение указывает, что для каждого n либо и , либо определены и равны, либо иначе и оба не определены. ${\ displaystyle F}$${\ displaystyle G}$${\ Displaystyle F \ simeq G}$${\ Displaystyle F (п)}$${\ Displaystyle G (п)}$${\ Displaystyle F (п)}$${\ Displaystyle G (п)}$

Теорема Роджерса о неподвижной точке

Для данной функции , А фиксированная точка из является индекс таким образом, что . Роджерс описывает следующий результат как «более простую версию» (второй) теоремы Клини о рекурсии. ${\ displaystyle F}$${\ displaystyle F}$${\ displaystyle e}$${\ Displaystyle \ varphi _ {е} \ simeq \ varphi _ {F (е)}}$

Теорема Роджерса о неподвижной точке . Если это полная вычислимая функция, у нее есть фиксированная точка.${\ displaystyle F}$

Доказательство теоремы о неподвижной точке

В доказательстве используется конкретная полная вычислимая функция , определяемая следующим образом. Учитывая натуральное число , функция выводит индекс частично вычислимой функции, которая выполняет следующие вычисления: ${\ displaystyle h}$${\ displaystyle x}$${\ displaystyle h}$

Учитывая ввод , первая попытка вычислить . Если это вычисление возвращает результат , вычислите и верните его значение, если оно есть.${\ displaystyle y}$${\ Displaystyle \ varphi _ {х} (х)}$${\ displaystyle e}$${\ displaystyle \ varphi _ {e} (y)}$

Таким образом, для всех индексов частично вычислимых функций, если определено, то . Если не определено, то это функция, которая нигде не определена. Функция может быть построена из частичной вычислимой функции , описанной выше , и SMN теоремы : для каждого , является индексом программы , которая вычисляет функцию . ${\ displaystyle x}$${\ Displaystyle \ varphi _ {х} (х)}$${\ Displaystyle \ varphi _ {час (х)} \ simeq \ varphi _ {\ varphi _ {x} (x)}}$${\ Displaystyle \ varphi _ {х} (х)}$${\ Displaystyle \ varphi _ {ч (х)}}$${\ displaystyle h}$${\ Displaystyle г (х, у)}$${\ displaystyle x}$${\ Displaystyle ч (х)}$${\ Displaystyle у \ mapsto г (х, у)}$

Чтобы завершить доказательство, позвольте быть любой полной вычислимой функцией и построить, как указано выше. Позвольте быть индексом композиции , которая является полной вычислимой функцией. Тогда по определению . Но, так как это показатель , и , таким образом . По транзитивности это означает . Следовательно, для . ${\ displaystyle F}$${\ displaystyle h}$${\ displaystyle e}$${\ Displaystyle F \ circ h}$${\ displaystyle \ varphi _ {h (e)} \ simeq \ varphi _ {\ varphi _ {e} (e)}}$${\ displaystyle h}$${\ displaystyle e}$${\ Displaystyle F \ circ h}$${\ Displaystyle \ varphi _ {е} (е) = (F \ circ h) (е)}$${\ displaystyle \ varphi _ {\ varphi _ {e} (e)} \ simeq \ varphi _ {F (h (e))}}$${\ displaystyle \ simeq}$${\ Displaystyle \ varphi _ {ч (е)} \ simeq \ varphi _ {F (ч (е))}}$${\ Displaystyle \ varphi _ {п} \ simeq \ varphi _ {F (п)}}$${\ Displaystyle п = час (е)}$

Это доказательство является построение частично рекурсивной функции , которая реализует Y Combinator .

Функции без фиксированной точки

Функция такая, что для всех называется свободной от неподвижной точки . Теорема о неподвижной точке показывает, что никакая полная вычислимая функция не свободна от неподвижной точки, но есть много невычислимых функций без неподвижной точки. Критерий полноты Арсланова утверждает, что единственная рекурсивно перечислимая степень Тьюринга, которая вычисляет функцию без неподвижных точек, - это 0 ′ , степень проблемы остановки . ${\ displaystyle F}$${\ displaystyle \ varphi _ {e} \ not \ simeq \ varphi _ {F (e)}}$${\ displaystyle e}$

Вторая теорема о рекурсии Клини

Вторая теорема о рекурсии является обобщением теоремы Роджерса со вторым входом в функцию. Одна неформальная интерпретация второй теоремы о рекурсии состоит в том, что можно строить самореференциальные программы; см. «Применение к лугам» ниже.

Вторая теорема о рекурсии . Для любой частично рекурсивной функции существует такой индекс , что .${\ Displaystyle Q (х, у)}$${\ displaystyle p}$${\ displaystyle \ varphi _ {p} \ simeq \ lambda yQ (p, y)}$

Теорема может быть доказана из теоремы Роджерса, если быть такой функцией, что (конструкция описывается теоремой Smn ). Затем можно проверить, что его фиксированная точка является требуемым индексом . Теорема конструктивна в том смысле, что фиксированная вычислимая функция отображает индекс Q в индекс p . ${\ Displaystyle F (p)}$${\ Displaystyle \ varphi _ {F (p)} (y) = Q (p, y)}$${\ displaystyle F}$${\ displaystyle p}$

Сравнение с теоремой Роджерса

Вторую теорему о рекурсии Клини и теорему Роджерса можно довольно просто доказать друг из друга. Однако прямое доказательство теоремы Клини не использует универсальную программу, что означает, что теорема верна для некоторых систем субрекурсивного программирования, которые не имеют универсальной программы.

Применение к лугам

Классическим примером использования второй теоремы о рекурсии является функция . Соответствующий индекс в этом случае дает вычислимую функцию, которая выводит собственный индекс при применении к любому значению. Выраженные в виде компьютерных программ, такие индексы известны как quines . ${\ Displaystyle Q (х, y) = х}$${\ displaystyle p}$

Следующий пример на Лиспе показывает, как из функции может быть эффективно получено следствие . Функция в коде - это функция с таким именем, созданная теоремой Smn . ${\ displaystyle p}$${\ displaystyle Q}$s11

Q может быть изменен на любую функцию с двумя аргументами.

(setq Q '(lambda (x y) x))
(setq s11 '(lambda (f x) (list 'lambda '(y) (list f x 'y))))
(setq n (list 'lambda '(x y) (list Q (list s11 'x 'x) 'y)))
(setq p (eval (list s11 n n)))

Результаты следующих выражений должны быть такими же. ${\ displaystyle \ varphi}$ p(nil)

(eval (list p nil))

Q(p, nil)

(eval (list Q p nil))

Приложение для устранения рекурсии

Предположим, что и являются общими вычислимыми функциями, которые используются в рекурсивном определении функции : ${\ displaystyle g}$${\ displaystyle h}$${\ displaystyle f}$

${\ Displaystyle f (0, y) \ simeq g (y),}$

${\ Displaystyle е (х + 1, у) \ simeq ч (е (х, у), х, у),}$

Вторую теорему о рекурсии можно использовать, чтобы показать, что такие уравнения определяют вычислимую функцию, где понятие вычислимости не должно допускать, на первый взгляд, рекурсивных определений (например, оно может быть определено с помощью μ-рекурсии или Тьюринга). машины ). Это рекурсивное определение может быть преобразовано в вычислимую функцию, которая предполагает, что это индекс самого себя, для имитации рекурсии: ${\ Displaystyle \ varphi _ {F} (е, х, у)}$${\ displaystyle e}$

${\ Displaystyle \ varphi _ {F} (е, 0, y) \ simeq g (y),}$

${\ displaystyle \ varphi _ {F} (e, x + 1, y) \ simeq h (\ varphi _ {e} (x, y), x, y).}$

Теорема о рекурсии устанавливает существование вычислимой функции такой, что . Таким образом, удовлетворяет данному рекурсивному определению. ${\ displaystyle \ varphi _ {f}}$${\ Displaystyle \ varphi _ {е} (х, у) \ simeq \ varphi _ {F} (е, х, у)}$${\ displaystyle f}$

Рефлексивное программирование

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

Первая теорема о рекурсии

В то время как вторая теорема о рекурсии касается неподвижных точек вычислимых функций, первая теорема о рекурсии связана с неподвижными точками, определяемыми операторами перечисления, которые являются вычислимым аналогом индуктивных определений. Оператор перечисления представляет собой набор пара ( А , п ) , где является ( кодом для а) конечного множества чисел и п является единственным натуральным числом. Часто n будет рассматриваться как код для упорядоченной пары натуральных чисел, особенно когда функции определены с помощью операторов перечисления. Операторы перечисления имеют центральное значение при изучении сводимости перечисления .

Каждый оператор перечисления Φ определяет функцию от наборов натуральных чисел до наборов натуральных чисел, заданных формулой

${\ Displaystyle \ Phi (X) = \ {n \ mid \ exists A \ substeq X [(A, n) \ in \ Phi] \}.}$

Рекурсивный оператор является оператором перечисления, когда дается график частично рекурсивной функции, всегда возвращает график частично рекурсивной функции.

Неподвижная точка оператора перечисления Ф есть множество F такое , что Φ ( F ) = F . Первая теорема перечисления показывает, что неподвижные точки могут быть эффективно получены, если сам оператор перечисления вычислим.

Первая теорема о рекурсии . Имеют место следующие утверждения.

1. Для любого вычислимого оператора перечисления Φ существует рекурсивно перечислимое множество F такое, что Φ ( F ) = F и F - наименьшее множество с этим свойством.
2. Для любого рекурсивного оператора существует частично вычислимая функция φ такая, что Ψ (φ) = φ и φ - наименьшая частично вычислимая функция с этим свойством.

Пример

Как и вторая теорема о рекурсии, первая теорема о рекурсии может использоваться для получения функций, удовлетворяющих системам рекурсивных уравнений. Чтобы применить первую теорему о рекурсии, рекурсивные уравнения необходимо сначала преобразовать в рекурсивный оператор.

Рассмотрим рекурсивные уравнения для факториальной функции f :

${\ displaystyle f (0) = 1}$

${\ Displaystyle F (N + 1) = (N + 1) \ CDOT F (N)}$

Соответствующий рекурсивный оператор Φ будет иметь информацию, которая сообщает, как перейти к следующему значению f из предыдущего значения. Однако рекурсивный оператор фактически определяет график f . Во-первых, Φ будет содержать пару . Это указывает на то, что f (0) однозначно 1, и, следовательно, пара (0,1) находится в графике f . ${\ Displaystyle (\ varnothing, (0,1))}$

Затем для каждого n и m Φ будет содержать пару . Это означает, что если f ( n ) равно m , то f ( n  + 1) равно ( n  + 1) m , так что пара ( n  + 1, ( n  + 1) m ) находится на графике f . В отличие от базового случая f (0) = 1, рекурсивный оператор требует некоторой информации о f ( n ), прежде чем он определит значение f ( n  + 1). ${\ Displaystyle (\ {(п, т) \}, (п + 1, (п + 1) \ CDOT м))}$

Первая теорема о рекурсии (в частности, часть 1) утверждает, что существует множество F такое, что Φ ( F ) = F. Множество F будет полностью состоять из упорядоченных пар натуральных чисел и будет графиком факториальной функции f , по желанию.

Ограничение рекурсивных уравнений, которые могут быть преобразованы в рекурсивные операторы, гарантирует, что рекурсивные уравнения фактически определяют наименьшую фиксированную точку. Например, рассмотрим систему рекурсивных уравнений:

${\ displaystyle g (0) = 1}$

${\ Displaystyle г (п + 1) = 1}$

${\ displaystyle g (2n) = 0}$

Не существует функции g, удовлетворяющей этим уравнениям, поскольку из них следует, что g (2) = 1, а также g (2) = 0. Таким образом, не существует неподвижной точки g, удовлетворяющей этим рекурсивным уравнениям. Можно сделать оператор перечисления, соответствующий этим уравнениям, но он не будет рекурсивным оператором.

Схема доказательства первой теоремы о рекурсии

Доказательство части 1 первой теоремы рекурсии получается повторением оператора перечисления Φ, начиная с пустого множества. Сначала строится последовательность F _k , для . Пусть F ₀ - пустое множество. Действуя индуктивно, для каждого k пусть F _{k + 1} be . Наконец, F берется . Оставшаяся часть доказательства состоит из проверки того, что F рекурсивно перечислимо и является наименьшей неподвижной точкой в ​​Φ. Последовательность F _k, использованная в этом доказательстве, соответствует цепи Клини в доказательстве теоремы Клини о неподвижной точке . ${\ Displaystyle к = 0,1, \ ldots}$${\ Displaystyle F_ {k} \ чашка \ Phi (F_ {k})}$${\ displaystyle \ bigcup F_ {k}}$

Вторая часть первой теоремы о рекурсии следует из первой части. Предположение, что Φ - рекурсивный оператор, используется, чтобы показать, что неподвижная точка Φ является графиком частичной функции. Ключевым моментом является то, что если фиксированная точка F не является графиком функции, то существует некоторое k такое, что F _k не является графиком функции.

Сравнение со второй теоремой о рекурсии

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

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

Второе отличие состоит в том, что первая теорема о рекурсии применима только к системам уравнений, которые можно преобразовать в рекурсивные операторы. Это ограничение аналогично ограничение на непрерывные оператор в фиксированной точке теоремы Клини из теории порядка . Вторая теорема о рекурсии может быть применена к любой тотально рекурсивной функции.

Обобщенная теорема

В контексте своей теории нумерации Ершов показал, что теорема Клини о рекурсии верна для любой предполной нумерации . Гёделевская нумерация - это предполная нумерация на множестве вычислимых функций, поэтому обобщенная теорема дает теорему Клини о рекурсии как частный случай.

Если задана предполная нумерация , то для любой частично вычислимой функции с двумя параметрами существует полная вычислимая функция с одним параметром такая, что ${\ displaystyle \ nu}$${\ displaystyle f}$${\ displaystyle t}$

${\ Displaystyle \ forall n \ in \ mathbb {N}: \ nu \ circ f (n, t (n)) = \ nu \ circ t (n).}$

Смотрите также

• Денотационная семантика , где другая теорема о наименьшей фиксированной точке используется для той же цели, что и первая теорема о рекурсии.
• Комбинаторы с фиксированной точкой , которые используются в лямбда-исчислении с той же целью, что и первая теорема о рекурсии.

использованная литература

• Ершов, Юрий Л. (1999). «Часть 4: Математика и теория вычислимости. 14. Теория нумерации». В Гриффоре, Эдвард Р. (ред.). Справочник по теории вычислимости . Исследования по логике и основам математики. 140 . Амстердам: Эльзевир . С. 473–503. ISBN 9780444898821. OCLC  162130533 . Дата обращения 6 мая 2020 .
• Джонс, Нил Д. (1997). Вычислимость и сложность: с точки зрения программирования . Кембридж, Массачусетс : MIT Press . ISBN 9780262100649. OCLC  981293265 .
• Клини, Стивен С. (1952). Введение в метаматематику . Bibliotheca Mathematica. Издательство Северной Голландии . ISBN 9780720421033. OCLC  459805591 . Дата обращения 6 мая 2020 .
• Роджерс, Хартли (1967). Теория рекурсивных функций и эффективной вычислимости . Кембридж, Массачусетс : MIT Press . ISBN 9780262680523. OCLC  933975989 . Дата обращения 6 мая 2020 .

Сноски

дальнейшее чтение

• Jockusch, CG ; Лерман, М .; Соаре, Род-Айленд ; Соловай, Р.М. (1989). «Рекурсивно перечислимые множества по модулю повторных скачков и расширения критерия полноты Арсланова». Журнал символической логики . 54 (4): 1288–1323. DOI : 10.1017 / S0022481200041104 . ISSN  0022-4812 . JSTOR  2274816 .

внешние ссылки

• Запись Пьерджоржио Одифредди «Рекурсивные функции» в Стэнфордской энциклопедии философии , 2012 г.