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