Изменения
→Теорема о рекурсии
Приведем конструктивное доказательство теоремы.
Пусть есть вычислимая <tex>V(x,y)</tex>. Будем поэтапно строить функцию <tex>p(y)</tex>. <br> Предположим, что у нас в распоряжении есть функция <tex>\mathrm{getSrc()}</tex>, которая вернет код <tex>p(y)</tex>. Тогда саму <tex>p(y)</tex> можно переписать так:
'''function''' p('''T''' y) {: '''T''' V('''T''' x, '''T''' y) { :
...
'''void''' main() {:
'''return''' V(getSrc(), y)
'''string''' getSrc() { :
...
Теперь нужно определить функцию <tex>\mathrm{getSrc()}</tex>. Предположим, что внутри <tex>p(y)</tex> мы можем определить функцию <tex>\mathrm{getOtherSrc()}</tex>, состоящую из одного оператора <tex>return</tex>, которая вернет весь предшествующий ей код. Тогда <tex>p(y)</tex> перепишется так.
'''function''' p('''T''' y) {: '''T''' V('''T''' x, '''T''' y) {:
...
'''void''' 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>
'''function''' p('''T''' y) {: '''T''' V('''T''' x, '''T''' y) {:
...
'''void''' main() {:
'''return''' V(getSrc(), y)
'''string''' getSrc() {:
'''string''' src = getOtherSrc()
'''return''' src + "string getOtherSrc() {:" + "\n" + "return" + src + "\n" + "}"; }
main() {:
return V(getSrc(), y)
string getSrc() {:
string src = getOtherSrc();
return src + "string getOtherSrc() {:" + "\n" + "return" + src + "\n" + "}"; }"; } }
}}
Если говорить неформально, теорема о рекурсии утверждает, что внутри программы можно использовать ее код. Это упрощает доказательство некоторых теорем.
