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