Теорема о рекурсии — различия между версиями
(→Теорема о неподвижной точке) |
(→Теорема о неподвижной точке) |
||
| Строка 81: | Строка 81: | ||
|statement= Пусть <tex>U</tex> {{---}} [[Диагональный_метод|универсальная функция]] для класса вычислимых функций одного аргумента, <tex>h</tex> {{---}} всюду определённая [[Вычислимые_функции|вычислимая функция]] одного аргумента. Тогда найдется такое <tex>n</tex>, что <tex>U_n=U_{h(n)}</tex>, то есть <tex>n</tex> и <tex>h(n)</tex> - номера одной функции. | |statement= Пусть <tex>U</tex> {{---}} [[Диагональный_метод|универсальная функция]] для класса вычислимых функций одного аргумента, <tex>h</tex> {{---}} всюду определённая [[Вычислимые_функции|вычислимая функция]] одного аргумента. Тогда найдется такое <tex>n</tex>, что <tex>U_n=U_{h(n)}</tex>, то есть <tex>n</tex> и <tex>h(n)</tex> - номера одной функции. | ||
|proof= | |proof= | ||
| − | + | Введем на множестве натуральных чисел следующее отношение: <tex>x \equiv y \Leftrightarrow U_x = U_y</tex> и докажем вспомогательную лемму. | |
{{Лемма | {{Лемма | ||
| − | |statement= | + | |statement= Для всякой вычислимой функции <tex>f</tex> существует вычислимая и всюду определенная функция <tex>g</tex>, являющаяся ее <tex>\equiv</tex> {{---}} продолжением (это значит, что если <tex>f(n)</tex> определено, то <tex>g(n) \equiv f(n)</tex>). |
| − | + | |proof= Рассмотрим вычислимую функцию от двух аргументов <tex> V(n, x) = U(f(n), x)</tex>. Так как <tex>V</tex> — вычислимая, то существует вычислимая и всюду определенная функция <tex>s(n)</tex> такая, что: <tex>V(n, x) = U(s(n), x)</tex>. | |
| − | + | ||
| − | + | Покажем, что <tex>s(n)</tex> будет являться <tex>\equiv</tex> {{---}} продолжением функции <tex>f(n)</tex>. Если <tex>f(n)</tex> определено, то <tex>s(n)</tex> вернет другой номер той же вычислимой функции. Если же <tex>f(n)</tex> не определено, то <tex>s(n)</tex> вернет номер нигде не определенной функции. | |
| − | + | Таким образом, мы нашли <tex>\equiv</tex> {{---}} продолжение для произвольно взятой вычислимой функции <tex>f</tex>. | |
| − | |||
}} | }} | ||
| − | + | Для доказательства теоремы рассмотрим некоторую вычислимую функцию, от которой никакая вычислимая функция не может отличаться всюду. Такой будет, например <tex>f(x) = U(x, x)</tex> (действительно, если предположить, что существует вычислимая функция <tex>h(n)</tex>, всюду отличная от <tex>f(n) = U(n, n)</tex>, то нарушается определение универсальной функции.) | |
| − | + | ||
| + | Согласно доказанной нами лемме, существует вычислимая и всюду определенная функция <tex>g(x)</tex>, являющаяся <tex>\equiv</tex> {{---}} продолжением функции <tex>f(x)</tex>. Давайте зададим функцию <tex>t(x)</tex> следующим образом: <tex>t(x) = h(g(x))</tex>, где <tex>h(x)</tex> - всюду определенная, вычислимая функция, не имеющая <tex>\equiv</tex> {{---}} неподвижных точек. | ||
}} | }} | ||
| − | |||
==Пример использования== | ==Пример использования== | ||
Версия 13:46, 4 декабря 2016
Теорема о рекурсии
| Теорема (Клини, о рекурсии / 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