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