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

Не путать с теоремой Клини для регулярных языков.

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

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

Обозначения

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Следующий пример в Лиспе иллюстрирует, как $p$ в следствии можно эффективно получить из функции $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)))

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

(eval (list p nil))

Q(p, nil)

(eval (list Q p nil))

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

Предположим, что $g$ и $h$ — это полностью вычислимые функции, которые используются в рекурсивном определении функции $f$:

$f(0,y)\simeq g(y),$

$f(x+1,y)\simeq h(f(x,y),x,y),$

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

2) $\forall g\in \mathbb {F} (\mathbb {N} ^{k})$ такой, что $\Phi (g)=g$ он утверждает, что $f_{\Phi }\subseteq g$

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

Пример

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

$\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). Введение в метаматематику . Библиотека Математика. Издательство Северной Голландии . ISBN  9780720421033 . OCLC   459805591 . Проверено 6 мая 2020 г.
• Роджерс, Хартли (1967). Теория рекурсивных функций и эффективная вычислимость . Кембридж, Массачусетс : MIT Press . ISBN  9780262680523 . OCLC   933975989 . Проверено 6 мая 2020 г.

Сноски

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

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

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

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