Введение
Теорема в теории вычислимости
В теории вычислимости теоремы рекурсии Клини — это пара фундаментальных результатов об применении вычислимых функций к их собственным описаниям. Теоремы были впервые доказаны Стивеном Клини в 1938 году и опубликованы в его книге 1952 года «Введение в метаматематику». Связанная теорема, которая строит фиксированные точки вычислимой функции, известна как теорема Роджерса и принадлежит Хартли Роджерсу-младшему. Теоремы рекурсии могут быть применены для построения фиксированных точек определенных операций над вычислимыми функциями, для создания квинов и для построения функций, заданных рекурсивными определениями.
Обозначение
Заявление теорем относится к допустимой нумерации частичных рекурсивных функций, такой что функция, соответствующая индексу, есть…
Если f и g – частичные функции на натуральных числах, обозначение f = g означает, что для каждого n либо f(n) и g(n) оба определены и равны, либо f(n) и g(n) оба не определены.
If and are partial functions on the natural numbers, the notation indicates that, for each n, either and are both defined and are equal, or else and are both undefined.
Теорема о фиксированной точке Роджерса
Учитывая функцию , фиксированной точкой функции является индекс , такой что. Обратите внимание, что сравнение входных данных в и выходных данных здесь происходит не по числовым значениям, а по связанным с ними функциям. Роджерс описывает следующий результат как "более простую версию" второй теоремы рекурсии Клини.
Доказательство теоремы о фиксированной точке
В доказательстве используется определенная общая вычислимая функция, определенная следующим образом. Для заданного натурального числа, функция выводит индекс частичной вычислимой функции, которая выполняет следующее вычисление: для заданного ввода, сначала пытается вычислить . Если это вычисление возвращает результат, то вычисляет и возвращает его значение, если оно существует. Таким образом, для всех индексов частичных вычислимых функций, если определено, то если не определено, то это функция, которая нигде не определена. Функция может быть построена из описанной выше частичной вычислимой функции и теоремы s-m-n: для каждого , является индексом программы, которая вычисляет функцию . Чтобы завершить доказательство, пусть будет любой общей вычислимой функцией, и построим как описано выше. Пусть будет индексом композиции , которая является общей вычислимой функцией. Тогда, по определению , но, поскольку является индексом , , и, следовательно, по транзитивности , это означает, что для . Это доказательство является построением частичной рекурсивной функции, реализующей Y-комбинатор.
Given an input , first attempt to compute If that computation returns an output , then compute and return its value, if any. Thus, for all indices of partial computable functions, if is defined, then If is not defined, then is a function that is nowhere defined. The function can be constructed from the partial computable function described above and the s m n theorem: for each , is the index of a program which computes the function
To complete the proof, let be any total computable function, and construct as above. Let be an index of the composition , which is a total computable function. Then by the definition of But, because is an index of , , and thus By the transitivity of , this means Hence for
This proof is a construction of a partial recursive function which implements the Y combinator.
Функции без фиксированной точки
Функция, для которой не существует такого x, что f(x) = x для всех x, называется свободной от фиксированных точек. Теорема о фиксированной точке показывает, что никакая тотальная вычислимая функция не является свободной от фиксированных точек, но существует множество невычислимых функций, свободных от фиксированных точек. Критерий полноты Арсланова утверждает, что единственная рекурсивно перечислимая степень Тьюринга, вычисляющая функцию, свободную от фиксированных точек, — это 0′, степень проблемы останова.
Сравнение с теоремой Роджерса
Вторая теорема рекурсии Клини и теорема Роджерса могут быть доказаны друг из друга относительно просто. Однако прямое доказательство теоремы Клини не опирается на универсальную программу, что означает, что теорема верна для некоторых субрекурсивных систем программирования, не обладающих универсальной программой.
Рефлексивное программирование
Рефлексивное программирование — это использование самоссылок в программах. Джонс представляет взгляд на вторую теорему о рекурсии, основанный на рефлексивном языке. Показано, что определенный рефлексивный язык не превосходит язык, не поддерживающий рефлексию (поскольку интерпретатор для рефлексивного языка может быть реализован без использования рефлексии); далее демонстрируется, что теорема о рекурсии в рефлексивном языке практически тривиальна.
Пример
Как и вторая теорема рекурсии, первая теорема рекурсии может быть использована для получения функций, удовлетворяющих системам рекурсионных уравнений. Для применения первой теоремы рекурсии, уравнения рекурсии должны быть сначала преобразованы в рекурсивный оператор. Рассмотрим рекурсионные уравнения для факториальной функции f: соответствующий рекурсивный оператор Φ будет содержать информацию, указывающую, как получить следующее значение f из предыдущего значения. Однако рекурсивный оператор фактически определит граф f. Во-первых, Φ будет содержать пару Это указывает на то, что f(0) однозначно равно 1, и, таким образом, пара (0,1) принадлежит графу f. Далее, для каждого n и m, Φ будет содержать пару Это указывает на то, что если f(n) равно m, то f(n + 1) равно (n + 1)m, так что пара (n + 1, (n + 1)m) принадлежит графу f. В отличие от базового случая 1 = f(0) = 1, рекурсивный оператор требует некоторой информации о f(n) прежде чем он определяет значение f(n + 1). Первая теорема рекурсии (в частности, часть 1) утверждает, что существует множество F, такое что 1 = Φ(F) = F. Множество F будет состоять полностью из упорядоченных пар натуральных чисел и будет являться графом факториальной функции f, как и требуется. Ограничение на рекурсионные уравнения, которые могут быть преобразованы в рекурсивные операторы, гарантирует, что рекурсионные уравнения фактически определяют наименьшую фиксированную точку. Например, рассмотрим набор рекурсионных уравнений: нет функции g, удовлетворяющей этим уравнениям, потому что они подразумевают g(2) = 1 и также подразумевают g(2) = 0. Таким образом, нет фиксированной точки g, удовлетворяющей этим рекурсионным уравнениям. Можно построить оператор перечисления, соответствующий этим уравнениям, но это не будет рекурсивный оператор.
Next, for each n and m, Φ will contain the pair This indicates that, if f(n) is m, then f(n + 1) is (n + 1)m, so that the pair (n + 1, (n + 1)m) is in the graph of f. Unlike the base case 1=f(0) = 1, the recursive operator requires some information about f(n) before it defines a value of f(n + 1). The first recursion theorem (in particular, part 1) states that there is a set F such that 1=Φ(F) = F. The set F will consist entirely of ordered pairs of natural numbers, and will be the graph of the factorial function f, as desired. The restriction to recursion equations that can be recast as recursive operators ensures that the recursion equations actually define a least fixed point. For example, consider the set of recursion equations:There is no function g satisfying these equations, because they imply g(2) = 1 and also imply g(2) = 0. Thus there is no fixed point g satisfying these recursion equations. It is possible to make an enumeration operator corresponding to these equations, but it will not be a recursive operator.
Скетч доказательства первой теоремы рекурсии
Доказательство первой части теоремы о первой рекурсии получается путем итерации оператора перечисления Φ, начиная с пустого множества. Сначала строится последовательность Fk, где F0 – пустое множество. Продолжая индуктивно, для каждого k, полагаем Fk+1 равным. Наконец, F определяется как. Остальная часть доказательства состоит в проверке того, что F рекурсивно перечисляемо и является наименьшей фиксированной точкой Φ. Последовательность Fk, используемая в этом доказательстве, соответствует цепочке Клини в доказательстве теоремы о фиксированной точке Клини. Вторая часть теоремы о первой рекурсии вытекает из первой части. Предположение о том, что Φ является рекурсивным оператором, используется для доказательства того, что фиксированная точка Φ является графом частичной функции. Ключевой момент заключается в том, что если фиксированная точка F не является графом функции, то существует такое k, что Fk не является графом функции.
Сравнение со второй теоремой рекурсии
По сравнению со второй теоремой рекурсии, первая теорема рекурсии приводит к более сильному заключению, но только при выполнении более узких предпосылок. Роджерс называет первую теорему рекурсии "слабой теоремой рекурсии", а вторую – "сильной теоремой рекурсии". Одно из различий между первой и второй теоремами рекурсии состоит в том, что фиксированные точки, полученные с помощью первой теоремы рекурсии, гарантированно являются наименьшими фиксированными точками, в то время как фиксированные точки, полученные со второй теоремы рекурсии, таковыми могут не являться. Второе различие заключается в том, что первая теорема рекурсии применима только к системам уравнений, которые можно представить в виде рекурсивных операторов. Это ограничение аналогично ограничению на непрерывные операторы в теореме о неподвижной точке Клини в теории порядка. Вторая теорема рекурсии может быть применена к любой тотальной рекурсивной функции.