Теорема о рекурсии — различия между версиями
Grechko (обсуждение | вклад) |
Vincent (обсуждение | вклад) |
||
| Строка 4: | Строка 4: | ||
|id=th1 | |id=th1 | ||
|about=О рекурсии | |about=О рекурсии | ||
| − | |statement= Пусть <tex>V(n, x)</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>V(x,y)</tex>. Введём вспомогательную функцию <tex>getSrc()</tex> следующим образом: <br> |
<code> <font size = "3em"> | <code> <font size = "3em"> | ||
getSrc(){ | getSrc(){ | ||
| Строка 19: | Строка 19: | ||
} | } | ||
</font> </code> | </font> </code> | ||
| − | Заметим, что функция <tex>getSrc()</tex> возвращает код функции <tex>p(y)</tex>, | + | Заметим, что функция <tex>getSrc()</tex> возвращает код функции <tex>p(y)</tex>, поэтому <tex>p(y)</tex> удовлетворяет требованию <tex>\forall y</tex> <tex>p(y) = V(p, y)</tex>. <br> |
}} | }} | ||
Если говорить неформально, теорема о рекурсии утверждает, что внутри программы можно использовать ее код. Это упрощает доказательство некоторых теорем. | Если говорить неформально, теорема о рекурсии утверждает, что внутри программы можно использовать ее код. Это упрощает доказательство некоторых теорем. | ||
| − | Приведем так же альтернативую формулировку теоремы | + | Приведем так же альтернативую формулировку теоремы и альтернативное (неконструктивное) доказательство. |
{{Теорема | {{Теорема | ||
Версия 00:05, 24 января 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