Теорема о рекурсии — различия между версиями
(→Пример использования) |
(→Теорема о рекурсии) |
||
| Строка 9: | Строка 9: | ||
Приведем конструктивное доказательство теоремы. | Приведем конструктивное доказательство теоремы. | ||
Пусть есть вычислимая <tex>V(x,y)</tex>. Будем поэтапно строить функцию <tex>p(y)</tex>. <br> Предположим, что у нас в распоряжении есть функция <tex>\mathrm{getSrc()}</tex>, которая вернет код <tex>p(y)</tex>. Тогда саму <tex>p(y)</tex> можно переписать так: | Пусть есть вычислимая <tex>V(x,y)</tex>. Будем поэтапно строить функцию <tex>p(y)</tex>. <br> Предположим, что у нас в распоряжении есть функция <tex>\mathrm{getSrc()}</tex>, которая вернет код <tex>p(y)</tex>. Тогда саму <tex>p(y)</tex> можно переписать так: | ||
| − | + | '''function''' p(y) { | |
| − | + | V(x, y) { | |
| − | p(y){ | + | ... |
| − | + | } | |
| − | + | main() { | |
| − | + | '''return''' V(getSrc(), y) | |
| − | + | } | |
| − | + | ||
| − | + | getSrc() { | |
| − | + | ... | |
| − | + | } | |
| + | } | ||
Теперь нужно определить функцию <tex>\mathrm{getSrc()}</tex>. Предположим, что внутри <tex>p(y)</tex> мы можем определить функцию <tex>\mathrm{getOtherSrc()}</tex>, состоящую из одного оператора <tex>return</tex>, которая вернет весь предшествующий ей код. Тогда <tex>p(y)</tex> перепишется так. | Теперь нужно определить функцию <tex>\mathrm{getSrc()}</tex>. Предположим, что внутри <tex>p(y)</tex> мы можем определить функцию <tex>\mathrm{getOtherSrc()}</tex>, состоящую из одного оператора <tex>return</tex>, которая вернет весь предшествующий ей код. Тогда <tex>p(y)</tex> перепишется так. | ||
| − | + | '''function''' p(y) { | |
| − | + | V(x, y) { | |
| − | + | ... | |
| + | } | ||
| + | |||
| + | main() { | ||
| + | '''return''' V(getSrc(), y) | ||
| + | } | ||
| − | + | '''string''' getSrc() { | |
| − | + | '''string''' src = getOtherSrc() | |
| − | + | '''return''' src + "string getOtherSrc() {" + "\n" + "return" + src + "\n" + "}"; | |
| − | + | } | |
| − | + | } | |
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
Теперь <tex>\mathrm{getOtherSrc()}</tex> определяется очевидным образом, и мы получаем '''итоговую версию''' функции <tex>p(y)</tex> | Теперь <tex>\mathrm{getOtherSrc()}</tex> определяется очевидным образом, и мы получаем '''итоговую версию''' функции <tex>p(y)</tex> | ||
| − | + | '''function''' p(y) { | |
| − | + | V(x, y) { | |
| − | + | ... | |
| + | } | ||
| − | + | main() { | |
| − | + | '''return''' V(getSrc(), y) | |
| − | + | } | |
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | + | '''string''' getSrc() { | |
| − | + | '''string''' src = getOtherSrc() | |
| − | + | '''return''' src + "string getOtherSrc() {" + "\n" + "return" + src + "\n" + "}"; | |
| − | + | } | |
| − | + | } | |
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
}} | }} | ||
Если говорить неформально, теорема о рекурсии утверждает, что внутри программы можно использовать ее код. Это упрощает доказательство некоторых теорем. | Если говорить неформально, теорема о рекурсии утверждает, что внутри программы можно использовать ее код. Это упрощает доказательство некоторых теорем. | ||
Версия 22:09, 14 декабря 2016
Теорема о рекурсии
| Теорема (Клини, о рекурсии / Kleene's recursion theorem): |
Пусть — вычислимая функция. Тогда найдётся такая вычислимая , что . |
| Доказательство: |
|
Приведем конструктивное доказательство теоремы.
Пусть есть вычислимая . Будем поэтапно строить функцию . function p(y) {
V(x, y) {
...
}
main() {
return V(getSrc(), y)
}
getSrc() {
...
}
}
Теперь нужно определить функцию . Предположим, что внутри мы можем определить функцию , состоящую из одного оператора , которая вернет весь предшествующий ей код. Тогда перепишется так. function p(y) {
V(x, y) {
...
}
main() {
return V(getSrc(), y)
}
string getSrc() {
string src = getOtherSrc()
return src + "string getOtherSrc() {" + "\n" + "return" + src + "\n" + "}";
}
}
Теперь определяется очевидным образом, и мы получаем итоговую версию функции function 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): |
Пусть — универсальная функция для класса вычислимых функций одного аргумента, — всюду определённая вычислимая функция одного аргумента. Тогда найдется такое , что , то есть и - номера одной функции. |
| Доказательство: |
|
Будем доказывать теорему от противного: предположим, что существует всюду определенная вычислимая функция , такая, что для любого . В терминах введенного нами отношения, это значит, что не имеет — неподвижных точек. Рассмотрим некоторую вычислимую функцию, от которой никакая вычислимая функция не может отличаться всюду. Такой будет, например (действительно, если предположить, что существует вычислимая функция , всюду отличная от , то нарушается определение универсальной функции.) Согласно доказанной нами лемме, существует вычислимая и всюду определенная функция , являющаяся — продолжением функции . Давайте зададим функцию следующим образом: , где - искомая всюду определенная, вычислимая функция, не имеющая — неподвижных точек. Тогда всюду отличается от (в силу того, что не имеет неподвижных точек.) Получили противоречие, из чего следует, что такой функции не существует. |
См. также
Источники
- Wikipedia — Kleene's recursion theorem
- Верещагин Н. К., Шень А. Лекции по математической логике и теории алгоритмов. Часть 3. Вычислимые функции — М.: МЦНМО, 1999 - С. 176
- Kleene, Stephen On notation for ordinal numbers - The Journal of Symbolic Logic, 1938 - С. 150-155