Теорема о рекурсии
Теорема о рекурсии
Теорема (Клини, о рекурсии / Kleene's recursion theorem): |
Пусть вычислимая функция. Тогда найдётся такая вычислимая , что . — |
Доказательство: |
Приведем конструктивное доказательство теоремы.
Пусть есть вычислимая
p(y){ V(x,y) {...} main() { return V(getSrc(), y) } string getSrc() {...} }
Теперь нужно определить функцию p(y){ V(x,y) {...} main() { return V(getSrc(), y) } string getSrc() { string src = getOtherSrc(); return src + "string getOtherSrc() {" + "\n" + "return" + src + "\n" + "}"; } string getOtherSrc() {...} }
Теперь p(y){ V(x,y) {...} main() { return V(getSrc(), y) } string getSrc() { string src = getOtherSrc(); return src + "string getOtherSrc() {" + "\n" + "return" + src + "\n" + "}"; } string getOtherSrc() { return " p(y){ // Возвращаем весь предыдущий код V(x,y) {...} main() { return V(getSrc(), y) } string getSrc() { string src = getOtherSrc(); return src + "string getOtherSrc() {" + "\n" + "return" + src + "\n" + "}"; }"; } } |
Если говорить неформально, теорема о рекурсии утверждает, что внутри программы можно использовать ее код. Это упрощает доказательство некоторых теорем.
Приведем так же альтернативую формулировку теоремы и альтернативное (неконструктивное) доказательство.
Теорема о неподвижной точке
Введем на множестве натуральных чисел следующее отношение:
и докажем вспомогательную лемму.Лемма: |
Для всякой вычислимой функции существует вычислимая и всюду определенная функция , являющаяся ее — продолжением (это значит, что если определено, то ). |
Доказательство: |
Рассмотрим вычислимую функцию от двух аргументов . Так как — вычислимая, то существует вычислимая и всюду определенная функция такая, что: .Покажем, что Таким образом, мы нашли будет являться — продолжением функции . Если определено, то вернет другой номер той же вычислимой функции. Если же не определено, то вернет номер нигде не определенной функции. — продолжение для произвольно взятой вычислимой функции . |
Теорема (Роджерс, о неподвижной точке / Rogers' fixed-point theorem): |
Пусть универсальная функция для класса вычислимых функций одного аргумента, — всюду определённая вычислимая функция одного аргумента. Тогда найдется такое , что , то есть и - номера одной функции. — |
Доказательство: |
Будем доказывать теорему от противного: предположим, что существует всюду определенная вычислимая функция , такая, что для любого . В терминах введенного нами отношения, это значит, что не имеет — неподвижных точек.Рассмотрим некоторую вычислимую функцию, от которой никакая вычислимая функция не может отличаться всюду. Такой будет, например Согласно доказанной нами лемме, существует вычислимая и всюду определенная функция (действительно, если предположить, что существует вычислимая функция , всюду отличная от , то нарушается определение универсальной функции.) , являющаяся — продолжением функции . Давайте зададим функцию следующим образом: , где - искомая всюду определенная, вычислимая функция, не имеющая — неподвижных точек. Тогда всюду отличается от (в силу того, что не имеет неподвижных точек.) Получили противоречие, из чего следует, что такой функции не существует. |
Пример использования
Используя теорему о рекурсии, приведём простое доказательство неразрешимости языка
.Лемма: |
Язык неразрешим. |
Доказательство: |
Предположим обратное, тогда существует программа p(x) if r(p) return 1 while true Пусть . Тогда условие выполняется и . Противоречие. Если , то не выполняется и . Противоречие. |
Доказательство теоремы Успенского-Райса с использованием теоремы о рекурсии:
Теорема: |
Язык никакого нетривиального свойства не является разрешимым. |
Доказательство: |
Пусть Q(x,y) if d(x) return g(y) else return f(y) По теореме о рекурсии, .Если , то .Если же В обоих случаях получаем противоречие. , то . |
Источники
- Wikipedia — Kleene's recursion theorem
- Верещагин Н. К., Шень А. Лекции по математической логике и теории алгоритмов. Часть 3. Вычислимые функции — М.: МЦНМО, 1999 - С. 176
- Kleene, Stephen On notation for ordinal numbers - The Journal of Symbolic Logic, 1938 - С. 150-155