Изменения
→Теорема о рекурсии
Приведем конструктивное доказательство теоремы.
Введем новые обозначения для псевдокода. Внутри блока '''functionprogram''' располагаются функции, среди которых есть функция <tex>\mathrm{main}</tex>: '''functionprogram int''' p('''int''' x):
...
Пусть есть вычислимая <tex>V(x,y)</tex>. Будем поэтапно строить функцию <tex>p(y)</tex>. <br> Предположим, что у нас в распоряжении есть функция <tex>\mathrm{getSrc()}</tex>, которая вернет код <tex>p(y)</tex>. Тогда саму <tex>p(y)</tex> можно переписать так:
'''functionprogram int''' p('''int''' y):
'''int''' V('''string''' x, '''int''' y):
...
...
Теперь нужно определить функцию <tex>\mathrm{getSrc()}</tex>. Предположим, что внутри <tex>p(y)</tex> мы можем определить функцию <tex>\mathrm{getOtherSrc()}</tex>, состоящую из одного оператора <tex>\mathrm{return}</tex>, которая вернет весь предшествующий ей код. Тогда <tex>p(y)</tex> перепишется так.
'''functionprogram int''' p('''int''' y):
'''int''' V('''string''' x, '''int''' y):
...
...
Теперь <tex>\mathrm{getOtherSrc()}</tex> определяется очевидным образом, и мы получаем '''итоговую версию''' функции <tex>p(y)</tex>:
'''functionprogram int''' p('''int''' y):
'''int''' V('''string''' x, '''int''' y):
...
