69
правок
Изменения
Нет описания правки
Так как <tex>U</tex> {{---}} универсальная, то для любой вычислимой всюду определенной <tex>n</tex> найдется такая вычислимая всюду определенная <tex>num</tex>, что <tex>n=U_{num(n)}</tex>. Тогда найдется такая <tex>h</tex>, что <tex>\forall n, x</tex> <tex>V(n, x) = U(h(num(n)), x)</tex>. <br >По доказанному найдется такое <tex>n_0</tex>, что <tex>U_{n_0} = U_{h(n_0)}</tex>. <br> Возьмем <tex>p=U_{n_0}</tex>. Тогда <tex>V(p, x) = V(U_{n_0}, x) = U(h(num(U_{n_0})), x) = U(h(n_0), x) = U(n_0, x) = p(x)</tex>.
}}
Можно привести '''конструктивное доказательство''' этой теоремы: <br>
Пусть есть вычислимая <tex>V(x,y)</tex>. Введем вспомогательную функцию <tex>getSrc()</tex> следующим образом: <br>
<code> <font size = "3em">
getSrc(){
"p(y) {\n return V(getSrc(), y)\n}";
}
</font> </code>
И определим функцию <tex>p(y)</tex> так:
<code> <font size = "3em">
p(y){
return V(getSrc(), y)
}
</font> </code>
Заметим, что функция <tex>getSrc()</tex> возвращает код функции <tex>p(y)</tex>, значит <tex>p(y)</tex> удовлетворяет требованию <tex>\forall y</tex> <tex>p(y) = V(p, y)</tex>. <br>
Если говорить неформально, теорема о рекурсии утверждает, что внутри программы можно использовать ее код. Это упрощает доказательство некоторых теорем.
