Теорема о рекурсии — различия между версиями
Vincent (обсуждение | вклад) |
Grechko (обсуждение | вклад) |
||
Строка 26: | Строка 26: | ||
Так как <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>. | Так как <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> | ||
Если говорить неформально, теорема о рекурсии утверждает, что внутри программы можно использовать ее код. Это упрощает доказательство некоторых теорем. | Если говорить неформально, теорема о рекурсии утверждает, что внутри программы можно использовать ее код. Это упрощает доказательство некоторых теорем. | ||
Версия 23:32, 23 января 2012
Теорема о рекурсии
Теорема (о рекурсии): | ||||||
Пусть универсальная функция, — всюду определённая вычислимая функция. Тогда найдется такое , что . — | ||||||
Доказательство: | ||||||
Начнём с доказательства леммы.
Теперь определим отношение | ||||||
Теорему о рекурсии можно переформулировать следущим образом.
Теорема (О рекурсии): |
Пусть — вычислимая функция.Тогда найдется такая вычислимая , что . |
Доказательство: |
Так как По доказанному найдется такое , что . Возьмем . Тогда . | — универсальная, то для любой вычислимой всюду определенной найдется такая вычислимая всюду определенная , что . Тогда найдется такая , что .
Можно привести конструктивное доказательство этой теоремы:
Пусть есть вычислимая . Введем вспомогательную функцию следующим образом:
getSrc(){ "p(y) {\n return V(getSrc(), y)\n}"; }
И определим функцию
p(y){ return V(getSrc(), y) }
Заметим, что функция
Если говорить неформально, теорема о рекурсии утверждает, что внутри программы можно использовать ее код. Это упрощает доказательство некоторых теорем.
Пример использования
Используя теорему о рекурсии, приведём простое доказательство неразрешимости языка
.Утверждение: |
Язык неразрешим. |
Предположим обратное, тогда существует программа p(x) if r(p) return 1 while true Пусть . Тогда условие выполняется и . Противоречие. Если , то не выполняется и . Противоречие. |
Источники
- Верещагин Н. К., Шень А. Лекции по математической логике и теории алгоритов. Часть 3. Вычислимые функции — М.: МЦНМО, 1999 - С. 176