Участник:Shersh/Теорема о рекурсии

Материал из Викиконспекты
Перейти к: навигация, поиск

Неразрешимость универсального языка

Утверждение:
[math]\triangleright[/math]

Допустим, что он разрешим. Тогда напишем такую программу: 

 p(x):
   if u(p, x) // можем так написать, потому что по теореме о рекурсии программа может знать свой код
     while true
   else
     return 1

Если [math] u(p, x) = 1 [/math], тогда программа [math] p [/math] на входе [math] x [/math] должна вернуть [math] 1 [/math], но по условию [math] if [/math] она зависает, а следовательно, не принадлежит универсальному языку.

Если же [math] u(p, x) \neq 1 [/math], то мы пойдём во вторую ветку условного оператора и вернём [math] 1 [/math], значит, пара [math] \langle p, x \rangle [/math] принадлежит универсальному языку, но [math] u(p, x) \neq 1 [/math], значит, пара не принадлежит. Опять получили противоречие.
[math]\triangleleft[/math]

Теорема Успенского-Райса

[math] A [/math] — разрешимое семейство языков.

[math] L_A [/math] — множество программ, удовлетворяющих св-ву [math] A [/math].

Допустим, что пустой язык [math] \varnothing [/math] принадлежит семейству [math] A [/math]. Если это не так, то мы можем перейти к рассмотрению дополнения семейства: к [math] \overline{A} [/math]. К тому же, так как свойство [math] A [/math] нетривиальное, то его дополнение содержит какой-то перечислимый язык. Пусть [math] q [/math] — полуразрешитель какого-то фиксированного непустого языка из [math] \overline{A} [/math], то есть [math] q \notin L_A [/math]. Тогда напишем такую программу: 

 p(x):
   if p [math] \in ~ L_A [/math] // можем так написать, потому что по предположению [math] L_A [/math] — разрешимый
     return q(x)
   else
     while true

Если [math] p [/math] не удовлетворяет свойству [math] A [/math], тогда будет выполняться всегда вторая ветка, и [math] p \equiv \varnothing [/math]. Но пустой язык принадлежит [math] A [/math]. Получили противоречие.

Если [math] p [/math] удовлетворяет свойству [math] A [/math], то [math] L(p) = L(q) [/math], а [math] q \notin A [/math]. Опять получили противоречие.

Колмогоровская сложность

Определение:
Колмогоровской сложностью строки [math] x [/math] называется функция [math] K(x) [/math], которая равна минимальной длине программы [math] p : p(\varepsilon) = x [/math].

Сложность считается в каком-то фиксированном языке программирования. Так, например, у языков C++ и Python будет разная колмогоровская сложность одной программы.

Пример

Колмогоровская сложность программы, выводящей [math] n [/math] нулей [math] K(0^n) \leqslant n + c [/math]. Просто программа, в которой записано [math] n [/math] нулей. Но можно записать и более короткую программу для больших [math] n [/math] со сложностью [math] K(0^n) \leqslant \log{n} + c [/math], например вот такую: 

 [math]p_n[/math]():
   for i = 1..n
     print(0)

Теорема (Невычислимость Колмогоровской сложности):
Колмогоровская сложность — невычислимая функция.
Доказательство:
[math]\triangleright[/math]

[math] \forall x \gt x_0: K(x) \gt f(x)[/math], если только [math]f \leqslant const [/math] или [math] f [/math] — невычислима.

Допустим, что [math] K [/math] вычислима, тогда напишем такую программу: 

 p([math]\varepsilon[/math]):
   foreach x [math]\in ~ \Sigma^* [/math] // перебираем слова по возрастанию длины
     if [math] K(x) \gt  |p|[/math] // теорема о рекурсии используется здесь
       print(x)
       exit

Начиная с [math] x_0 [/math], [math] f(x) \gt |p| [/math].
[math]\triangleleft[/math]

Busy beaver

Утверждение:
Функция Busy beaver невычислима.
[math]\triangleright[/math]

Предположим, что это не так. Тогда напишем такую программу 

 p():
   for i = 1..BB([math]|p|[/math]) + 1
     do smth

Такая программа всегда совершает больше шагов, чем функция [math] BB [/math] от этой программы. А это невозможно, так [math] BB(|p|) [/math] равна максимальному числу шагов как раз этой программы. Получили противоречие.
[math]\triangleleft[/math]

Аналог I теоремы Гёделя о неполноте

Теорема:
В любой "достаточно богатой системе" существует истинное недоказуемое утверждение.
Доказательство:
[math]\triangleright[/math]

Поясним, что это значит. Так как любой язык программирования эквивалентен машине Тьюринга, то всё связанное с ним кодируется в логике первого порядка с аксиомами Пеано (для этого достаточно, чтобы программа умела прибавлять к числу единицу и вызывать подпрограммы), поэтому можно в терминах программ получать утверждения, эквивалентные тем, что строил Гёдель.

Можно переформулировать теорему следующим образом: невозможно доказать, что [math] p(x) = \perp [/math].

Тогда напишем такую программу: 

 p(x):
   foreach q [math] \in ~ \Sigma^* [/math]
     if q proves "p(x) зависает"
       exit
[math]\triangleleft[/math]

Теорема о неподвижной точке

Зафиксируем главную нумерацию [math] W [/math]. Обозначим за [math] W_n [/math] множество слов, допускаемых программой с номером [math] n [/math].

Утверждение:
[math] \exists n : W_n = \{n\} [/math]
[math]\triangleright[/math]

Напишем такую программу: 

 p(q):
   if p == q // сравниваем как строки; так можно сделать, потому что программа знает свой код по теореме о рекурсии
     print number(p)
   else
     while true

Программа [math] p [/math] знает свой код, что то же самое, что и знает свой номер. Как видно из её кода, она допускает только одно число — свой номер.
[math]\triangleleft[/math]

Ссылки

Источник — «http://neerc.ifmo.ru/wiki/index.php?title=Участник:Shersh/Теорема_о_рекурсии&oldid=35540»