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