Теорема о рекурсии — различия между версиями
Grechko (обсуждение | вклад) |
Grechko (обсуждение | вклад) |
||
Строка 3: | Строка 3: | ||
{{Теорема | {{Теорема | ||
|id=th1 | |id=th1 | ||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
|about=О рекурсии | |about=О рекурсии | ||
|statement= Пусть <tex>V(n, x)</tex> {{---}} вычислимая функция.Тогда найдется такая вычислимая <tex>p</tex>, что <tex>\forall y</tex> <tex>p(y) = V(p, y)</tex>. | |statement= Пусть <tex>V(n, x)</tex> {{---}} вычислимая функция.Тогда найдется такая вычислимая <tex>p</tex>, что <tex>\forall y</tex> <tex>p(y) = V(p, y)</tex>. | ||
|proof= | |proof= | ||
− | + | Приведем конструктивное доказательство теоремы. | |
− | |||
− | |||
Пусть есть вычислимая <tex>V(x,y)</tex>. Введем вспомогательную функцию <tex>getSrc()</tex> следующим образом: <br> | Пусть есть вычислимая <tex>V(x,y)</tex>. Введем вспомогательную функцию <tex>getSrc()</tex> следующим образом: <br> | ||
<code> <font size = "3em"> | <code> <font size = "3em"> | ||
Строка 40: | Строка 20: | ||
</font> </code> | </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> | Заметим, что функция <tex>getSrc()</tex> возвращает код функции <tex>p(y)</tex>, значит <tex>p(y)</tex> удовлетворяет требованию <tex>\forall y</tex> <tex>p(y) = V(p, y)</tex>. <br> | ||
+ | }} | ||
Если говорить неформально, теорема о рекурсии утверждает, что внутри программы можно использовать ее код. Это упрощает доказательство некоторых теорем. | Если говорить неформально, теорема о рекурсии утверждает, что внутри программы можно использовать ее код. Это упрощает доказательство некоторых теорем. | ||
+ | |||
+ | Приведем так же альтернативую формулировку теоремы, и альтернативное (неконструктивное) доказательство. | ||
+ | |||
+ | {{Теорема | ||
+ | |id=th2 | ||
+ | |about=о рекурсии | ||
+ | |statement= Пусть <tex>U</tex> {{---}} [[Диагональный_метод|универсальная функция]], <tex>h</tex> {{---}} всюду определённая [[Вычислимые_функции|вычислимая функция]]. Тогда найдется такое <tex>n</tex>, что <tex>U_n=U_{h(n)}</tex>. | ||
+ | |proof= | ||
+ | Начнём с доказательства леммы. | ||
+ | {{Лемма | ||
+ | |statement= Пусть на натуральных числах задано отношение эквивалентности <tex>\equiv</tex>. Тогда следующие два утверждения не могут быть выполнены одновременно: <br> | ||
+ | # Пусть <tex>f</tex> {{---}} вычислимая функция. Тогда существует всюду определённое вычислимое <tex>\equiv</tex> {{---}} продолжение <tex>g</tex> функции <tex>f</tex>, то есть такая <tex>g</tex>, что <tex>D(g)=N</tex> и <tex>\forall x</tex> такого, что <tex>f(x) \ne \perp</tex>, выполнено <tex>f(x) \equiv g(x)</tex>. | ||
+ | # Найдётся такая всюду определенная вычислимая <tex>h</tex>, что <tex>\forall n </tex> выполнено <tex>h(n) \not\equiv n</tex>. | ||
+ | |proof= | ||
+ | Приведем доказательство от противного. Пусть оба утверждения выполнены. <br> | ||
+ | Определим функцию <tex>f</tex> так: <tex>f(x)=U(x,x)</tex>. Заметим, что никакая всюду вычислимая функция не отличается от <tex>f</tex> всюду. <br> Согласно первому утверждению найдётся всюду определённое вычислимое <tex>\equiv</tex> {{---}} продолжение <tex>g</tex> функции <tex>f</tex>. <br> Определим функцию <tex>t</tex> так: <tex>t(x)=h(g(x))</tex>, где <tex>h</tex> {{---}} функция из второго утверждения. <br >Если <tex>f(x) \ne \perp</tex>, то <tex>f(x)=g(x) \ne h(g(x))=t(x)</tex>, то есть <tex>f(x) \ne t(x)</tex>. Если <tex>f(x)= \perp</tex>, то <tex>f(x) \ne t(x)</tex>, так как <tex>t</tex> всюду определена. Значит, <tex>f</tex> всюду отлична от <tex>t</tex>, получили противоречие. | ||
+ | }} | ||
+ | Теперь определим отношение <tex>\equiv</tex> так: <tex>x \equiv y \Leftrightarrow U_x = U_y</tex>. Покажем, что для него выполнено первое утверждение леммы. <br> Для заданной <tex>f</tex> определим <tex>V(n,x) = U(f(n), x)</tex>. <br> Так как <tex>U</tex> {{---}} универсальная функция, то найдётся такая всюду определенная вычислимая функция <tex>s</tex>, что <tex>V(n,x) = U(s(n), x)</tex>. <br> Тогда <tex>\forall x </tex> и <tex> n </tex> будет выполнено <tex>U(f(n), x) = U(s(n), x)</tex>. Значит, <tex>\forall n </tex> <tex> s(n) \equiv f(n)</tex>, то есть <tex>s</tex> {{---}} всюду определенное <tex>\equiv</tex> {{---}} продолжение <tex>f</tex>. | ||
+ | Значит, для нашего отношения эквивалентности второе утверждение леммы не верно, то есть для любого вычислимого всюду определенного <tex>h</tex> <tex> \exists n</tex> такое, что <tex>U_{h(n)} = U_n</tex>. | ||
+ | }} | ||
==Пример использования== | ==Пример использования== |
Версия 23:52, 23 января 2012
Теорема о рекурсии
Теорема (О рекурсии): |
Пусть — вычислимая функция.Тогда найдется такая вычислимая , что . |
Доказательство: |
Приведем конструктивное доказательство теоремы.
Пусть есть вычислимая getSrc(){ return "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