Теорема о рекурсии — различия между версиями
(→Пример использования) |
|||
Строка 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