Изменения
Нет описания правки
|proof=
Приведем конструктивное доказательство теоремы.
Пусть есть вычислимая <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">
p(y){
</font></code>
}}
Если говорить неформально, теорема о рекурсии утверждает, что внутри программы можно использовать ее код. Это упрощает доказательство некоторых теорем.
