Теорема о рекурсии — различия между версиями
(→Теорема о рекурсии) |
|||
| Строка 7: | Строка 7: | ||
|proof= | |proof= | ||
Приведем конструктивное доказательство теоремы. | Приведем конструктивное доказательство теоремы. | ||
| − | Пусть есть вычислимая <tex>V(x,y)</tex>. | + | Пусть есть вычислимая <tex>V(x,y)</tex>. Будем поэтапно строить функцию <tex>p(y)</tex>. Предположим что у нас в распоряжении есть функция <tex>getSrc()</tex> которая вернет код <tex>p(y)</tex>. Тогда саму <tex>p(y)</tex> можно переписать так: |
| + | |||
| + | <code><font size = "3em"> | ||
| + | p(y){ | ||
| + | V(x,y) {...} | ||
| + | |||
| + | main() { | ||
| + | return V(getSrc(), y) | ||
| + | } | ||
| + | |||
| + | string getSrc() {...} | ||
| + | </font></code> | ||
| + | Теперь нужно определить функцию <tex>getSrc()</tex>. Предположим что внутри <tex>p(y)</tex> мы можем определить функцию <tex>getOtherSrc()</tex> состоящюю из одного оператора <tex>return</tex>, которая вернет весь предшествующий ей код. Тогда <tex>p(y)</tex> перепишется так. | ||
| + | <code><font size = "3em"> | ||
| + | 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() {...} | ||
| + | } | ||
| + | </font></code> | ||
| + | |||
| + | Теперь <tex>getOtherSrc()</tex> определяется очевидным образом, и мы получаем '''итоговую версию''' функции <tex>p(y)</tex> | ||
<code><font size = "3em"> | <code><font size = "3em"> | ||
p(y){ | p(y){ | ||
| Строка 37: | Строка 67: | ||
</font></code> | </font></code> | ||
| − | |||
}} | }} | ||
Если говорить неформально, теорема о рекурсии утверждает, что внутри программы можно использовать ее код. Это упрощает доказательство некоторых теорем. | Если говорить неформально, теорема о рекурсии утверждает, что внутри программы можно использовать ее код. Это упрощает доказательство некоторых теорем. | ||
Версия 07:05, 24 января 2012
Теорема о рекурсии
| Теорема (О рекурсии): |
Пусть — вычислимая функция. Тогда найдётся такая вычислимая , что . |
| Доказательство: |
|
Приведем конструктивное доказательство теоремы. Пусть есть вычислимая . Будем поэтапно строить функцию . Предположим что у нас в распоряжении есть функция которая вернет код . Тогда саму можно переписать так:
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" + "}";
}";
}
}
|
Если говорить неформально, теорема о рекурсии утверждает, что внутри программы можно использовать ее код. Это упрощает доказательство некоторых теорем.
Приведем так же альтернативую формулировку теоремы и альтернативное (неконструктивное) доказательство.
| Теорема (о рекурсии): | ||||||
Пусть — универсальная функция, — всюду определённая вычислимая функция. Тогда найдется такое , что . | ||||||
| Доказательство: | ||||||
|
Начнём с доказательства леммы.
Теперь определим отношение так: . Покажем, что для него выполнено первое утверждение леммы. | ||||||
Пример использования
Используя теорему о рекурсии, приведём простое доказательство неразрешимости языка .
| Лемма: |
Язык неразрешим. |
| Доказательство: |
|
Предположим обратное, тогда существует программа разрещающая .
Рассмотрим следущую программу:
p(x)
if r(p)
return 1
while true
Пусть . Тогда условие выполняется и . Противоречие. Если , то не выполняется и . Противоречие. |
Источники
- Верещагин Н. К., Шень А. Лекции по математической логике и теории алгоритмов. Часть 3. Вычислимые функции — М.: МЦНМО, 1999 - С. 176