Теорема рекурсии Клини

Теорема в теории вычислимости

В теории вычислимости рекурсивные теоремы Клини представляют собой пару фундаментальных результатов о применении вычислимых функций к их собственным описаниям. Теоремы были впервые доказаны Стивеном Клини в 1938 году ^[1] и появились в его книге 1952 года «Введение в метаматематику» . ^[2] Связанная теорема, которая строит неподвижные точки вычислимой функции, известна как теорема Роджерса и принадлежит Хартли Роджерсу-младшему ^[3]

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

Обозначение

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

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

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

При наличии функции фиксированная точка — это индекс такой, что . Обратите внимание, что сравнение входов и выходов здесь выполняется не в терминах числовых значений, а в терминах связанных с ними функций. ${\displaystyle F}$ ${\displaystyle F}$ ${\displaystyle e}$ ${\displaystyle \varphi _{e}\simeq \varphi _{F(e)}}$

Роджерс описывает следующий результат как «более простую версию» (второй) теоремы Клини о рекурсии. ^[4]

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

По сути, это означает, что если мы применяем эффективное преобразование к программам (например, заменяем инструкции, такие как follower, jump, remove lines), то всегда будет программа, поведение которой не изменяется преобразованием. Поэтому эту теорему можно интерпретировать следующим образом: «при любой эффективной процедуре преобразования программ всегда существует программа, которая, будучи измененной процедурой, делает то же самое, что и раньше», или: «невозможно написать программу, которая изменяет экстенсиональное поведение всех программ».

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Применение к квинам

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

Следующий пример на Lisp иллюстрирует, как в следствии можно эффективно получить функцию . Функция в коде — это функция с этим именем, полученная с помощью теоремы 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 f(x+1,y)\simeq h(f(x,y),x,y),}$

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

${\displaystyle \varphi _{F}(e,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 _{f}(x,y)\simeq \varphi _{F}(f,x,y)}$ ${\displaystyle f}$

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

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

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

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

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

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

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

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

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

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

Первая теорема рекурсии также называется теоремой о неподвижной точке (теории рекурсии). ^[10] Существует также определение, которое можно применить к рекурсивным функционалам следующим образом:

Пусть — рекурсивный функционал. Тогда имеет наименьшую неподвижную точку , которая вычислима, т.е. ${\displaystyle \Phi :\mathbb {F} (\mathbb {N} ^{k})\rightarrow (\mathbb {N} ^{k})}$ ${\displaystyle \Phi }$ ${\displaystyle f_{\Phi }:\mathbb {N} ^{k}\rightarrow \mathbb {N} }$

1) ${\displaystyle \Phi (f_{\phi })=f_{\Phi }}$

2) такой, что выполняется следующее: ${\displaystyle \forall g\in \mathbb {F} (\mathbb {N} ^{k})}$ ${\displaystyle \Phi (g)=g}$ ${\displaystyle f_{\Phi }\subseteq g}$

3) вычислимо ${\displaystyle f_{\Phi }}$

Пример

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

Рассмотрим уравнения рекурсии для факториальной функции f : Соответствующий рекурсивный оператор Φ будет иметь информацию, которая сообщает, как получить следующее значение f из предыдущего значения. Однако рекурсивный оператор фактически определит график f . Во-первых, Φ будет содержать пару . Это указывает на то, что f (0) однозначно равно 1, и, таким образом, пара (0,1) находится в графике f . $${\displaystyle {\begin{aligned}&f(0)=1\\&f(n+1)=(n+1)\cdot f(n)\end{aligned}}}$$ ${\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 (\{(n,m)\},(n+1,(n+1)\cdot m))}$

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

Ограничение на уравнения рекурсии, которые могут быть переделаны в рекурсивные операторы, гарантирует, что уравнения рекурсии фактически определяют наименьшую неподвижную точку. Например, рассмотрим набор уравнений рекурсии: Нет функции g , удовлетворяющей этим уравнениям, потому что они подразумевают g (2) = 1 и также подразумевают g (2) = 0. Таким образом, нет неподвижной точки g, удовлетворяющей этим уравнениям рекурсии. Можно создать оператор перечисления, соответствующий этим уравнениям, но он не будет рекурсивным оператором. $${\displaystyle {\begin{aligned}&g(0)=1\\&g(n+1)=1\\&g(2n)=0\end{aligned}}}$$

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

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

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

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

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

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

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

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

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

Если задана предполная нумерация , то для любой частично вычислимой функции с двумя параметрами существует полностью вычислимая функция с одним параметром, такая что ${\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. Амстердам: Elsevier . С. 473–503. ISBN 9780444898821. OCLC  162130533 . Получено 6 мая 2020 г. .
• Джонс, Нил Д. (1997). Вычислимость и сложность: с точки зрения программирования . Кембридж, Массачусетс : MIT Press . ISBN 9780262100649. OCLC  981293265.
• Клини, Стивен С. (1952). Введение в метаматематику. Bibliotheca Mathematica. North-Holland Publishing . ISBN 9780720421033. OCLC  459805591 . Получено 6 мая 2020 г. .
• Роджерс, Хартли (1967). Теория рекурсивных функций и эффективная вычислимость . Кембридж, Массачусетс : MIT Press . ISBN 9780262680523. OCLC  933975989 . Получено 6 мая 2020 г. .

Сноски

1. Клини, Стивен К. (1938). «О нотации порядковых чисел» (PDF) . Журнал символической логики . 3 (4): 150–155. doi :10.2307/2267778. ISSN  0022-4812. JSTOR  2267778. S2CID  34314018 . Получено 6 мая 2020 г. .
2. Клини 1952.
3. Роджерс, 1967.
4. Роджерс 1967, §11.2.
5. Soare, RI (1987). Рекурсивно перечислимые множества и степени: исследование вычислимых функций и вычислимо генерируемых множеств . Перспективы математической логики. Берлин и Нью-Йорк: Springer-Verlag . стр. 88. ISBN 9780387152998. OCLC  318368332.
6. Джонс 1997, стр. 229–30.
7. Клини 1952, стр. 352–3.
8. Катланд, Найджел Дж. (1980). Вычислимость: Введение в теорию рекурсивных функций. Cambridge University Press . стр. 204. doi :10.1017/cbo9781139171496. ISBN 9781139935609. OCLC  488175597 . Получено 6 мая 2020 г. .
9. Джонс 1997.
10. Катланд, Найджел. Вычислимость: введение в теорию рекурсивных функций .
11. Барендрегт, Хенк ; Тервейн, Себастьян А. (2019). «Теоремы о неподвижной точке для предполных нумераций» . Анналы чистой и прикладной логики . 170 (10): 1151–1161. дои : 10.1016/j.apal.2019.04.013. hdl : 2066/205967 . ISSN  0168-0072. S2CID  52289429 . Проверено 6 мая 2020 г.стр. 1151.
12. См. Ершов 1999, §4.14 для обзора на английском языке.

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

• Jockusch, CG ; Lerman, M.; Soare, RI ; Solovay, RM (1989). «Рекурсивно перечислимые множества по модулю итерированных переходов и расширения критерия полноты Арсланова». The Journal of Symbolic Logic . 54 (4): 1288–1323. doi :10.1017/S0022481200041104. ISSN  0022-4812. JSTOR  2274816. S2CID  32203705.

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

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