Участник:Shersh/Теорема о рекурсии — различия между версиями

Материал из Викиконспекты
Перейти к: навигация, поиск
(гёдель)
(Пример использования)
 
(не показано 17 промежуточных версий 4 участников)
Строка 1: Строка 1:
 +
По [[Теорема о рекурсии | теореме о рекурсии]], программа может знать свой исходный код. Значит, в неё можно написать функцию <tex> \mathrm{getSrc()} </tex>, которая вернёт строку {{---}} исходный код программы. Далее будем считать, что такая функция определена в каждой программе.
 
== Неразрешимость универсального языка ==
 
== Неразрешимость универсального языка ==
Считаем, что язык программ над тем же алфавитом, что и язык входных данных. Если это не так, то можно просто взять объединение алфавитов, это ничто не испортит.
 
 
Универсальная программа: <tex> u(p, x) = p(x) </tex>.
 
 
Универсальный язык: <tex> L_u = \{ <p, x> \mid u(p, x) = 1 \} </tex>
 
 
 
{{Утверждение
 
{{Утверждение
 
|id=proposalU.  
 
|id=proposalU.  
|statement=Универсальный язык неразрешим
+
|statement=[[Разрешимые (рекурсивные) языки#Пример неразрешимого множества | Универсальный язык]] неразрешим
 
|proof=
 
|proof=
Напишем такую программу:
+
Допустим, что он разрешим. Тогда напишем такую программу:
 
<code>
 
<code>
 
   p(x):
 
   p(x):
     '''if''' u(p, x) // можем так написать, потому что по теореме о рекурсии программа может знать свой код
+
     '''if''' u(getSrc(), x)
       '''return''' 0
+
       '''while''' ''true''
 
     '''else'''
 
     '''else'''
 
       '''return''' 1
 
       '''return''' 1
 
</code>
 
</code>
  
Если <tex> u(p, x) = 1 </tex>, тогда программа <tex> p </tex> на входе <tex> x </tex> возвращает <tex> 1 </tex>, но по условию <tex> if </tex> она должна вернуть 0, а следовательно, не принадлежит универсальному языку.
+
Если <tex> u(p, x) = 1 </tex>, тогда программа <tex> p </tex> на входе <tex> x </tex> должна вернуть <tex> 1 </tex>, но по условию <tex> if </tex> она зависает, а следовательно, не принадлежит универсальному языку.
  
Если же <tex> u(p, x) = 0 </tex>, то мы пойдём во вторую ветку условного оператора и вернём <tex> 1 </tex>, значит, пара <tex> <p, x> </tex> принадлежит универсальному языку, но <tex> u(p, x) = 0 </tex>, значит, пара не принадлежит. Опять получили противоречие.
+
Если же <tex> u(p, x) \neq 1 </tex>, то мы пойдём во вторую ветку условного оператора и вернём <tex> 1 </tex>, значит, пара <tex>  
 +
\langle p, x \rangle </tex> принадлежит универсальному языку, но <tex> u(p, x) \neq 1 </tex>, значит, пара не принадлежит. Опять получили противоречие.
 
}}
 
}}
 +
 
== Теорема Успенского-Райса ==
 
== Теорема Успенского-Райса ==
 
<tex> A </tex> {{---}} разрешимое семейство языков.
 
<tex> A </tex> {{---}} разрешимое семейство языков.
  
<tex> L_A </tex> {{---}} язык свойства языков. Допустим, что он разрешим. Тогда напишем такую программу
+
<tex> L_A </tex> {{---}} множество программ, удовлетворяющих св-ву <tex> A </tex>.
 +
 
 +
Теперь допустим, что язык <tex> L_A </tex> разрешим. Тогда напишем такую программу:
  
 
<code>
 
<code>
 +
  propA(code):
 +
    // программа, разрешающее свойство языка <tex> A </tex>
 +
  f(x):
 +
    // такая программа <tex> f </tex>, что <tex>f \in A </tex>; существует потому что <tex> A </tex> {{---}} нетривиальное свойство
 +
  g(x):
 +
    // такая программа <tex> g </tex>, что <tex>g \notin A </tex>; существует потому что <tex> A </tex> {{---}} нетривиальное свойство
 
   p(x):
 
   p(x):
     '''if''' p <tex> \in ~ L_A </tex>
+
     '''if''' propA(getSrc())
      '''return''' z(x)
+
        '''return''' g(x)
 
     '''else'''
 
     '''else'''
      '''while''' ''true''
+
        '''return''' f(x)
 
</code>
 
</code>
 +
 +
Если <tex> p </tex> не удовлетворяет свойству <tex> A </tex>, тогда будет выполняться всегда вторая ветка, и <tex> L(p) = L(f) </tex>. Но язык программы <tex> f </tex> принадлежит <tex> A </tex>. Получили противоречие.
 +
 +
Если <tex> p </tex> удовлетворяет свойству <tex> A </tex>, то <tex> L(p) = L(g) </tex>, а <tex> g \notin A </tex>. Опять получили противоречие.
 
== Колмогоровская сложность ==
 
== Колмогоровская сложность ==
 
{{Определение
 
{{Определение
Строка 40: Строка 49:
 
|definition='''Колмогоровской сложностью''' строки <tex> x </tex> называется функция <tex> K(x) </tex>, которая равна минимальной длине программы <tex> p : p(\varepsilon) = x </tex>.
 
|definition='''Колмогоровской сложностью''' строки <tex> x </tex> называется функция <tex> K(x) </tex>, которая равна минимальной длине программы <tex> p : p(\varepsilon) = x </tex>.
 
}}
 
}}
 +
Сложность считается в каком-то фиксированном языке программирования. Так, например, у языков C++ и Python будет разная колмогоровская сложность одной программы.
 +
 
=== Пример ===
 
=== Пример ===
Колмогоровская сложность программы, выводящей <tex> n </tex> нулей <tex> K(0^n) \leqslant \log{n} + c </tex>. Просто программа, в которой записано <tex> n </tex> нулей. Но можно записать и более короткую программу для больших <tex> n </tex>, например вот такую:
+
Колмогоровская сложность программы, выводящей <tex> n </tex> нулей <tex> K(0^n) \leqslant n + c </tex>. Просто программа, в которой записано <tex> n </tex> нулей. Но можно записать и более короткую программу для больших <tex> n </tex> со сложностью <tex> K(0^n) \leqslant \log{n} + c </tex>, например вот такую:
 
<code>
 
<code>
 
   <tex>p_n</tex>():
 
   <tex>p_n</tex>():
Строка 66: Строка 77:
 
Начиная с <tex> x_0 </tex>, <tex> f(x) > |p| </tex>.
 
Начиная с <tex> x_0 </tex>, <tex> f(x) > |p| </tex>.
 
}}
 
}}
 +
 
== Busy beaver ==
 
== Busy beaver ==
 +
{{Утверждение
 +
|id=proposalU.
 +
|statement=Функция [[Busy beaver]] невычислима.
 +
|proof= Предположим, что это не так. Тогда напишем такую программу
 +
<code>
 +
  p():
 +
    '''for''' i = 1..BB(<tex>|\mathrm{getSrc()}|</tex>) + 1
 +
      do smth
 +
</code>
 +
 +
Такая программа всегда совершает больше шагов, чем функция <tex> BB </tex> от этой программы. А это невозможно, так <tex> BB(|p|) </tex> равна максимальному числу шагов как раз этой программы. Получили противоречие.
 +
}}
 +
 
== Аналог I теоремы Гёделя о неполноте ==
 
== Аналог I теоремы Гёделя о неполноте ==
 
{{Теорема
 
{{Теорема
Строка 72: Строка 97:
 
|statement = В любой "достаточно богатой системе" существует истинное недоказуемое утверждение.
 
|statement = В любой "достаточно богатой системе" существует истинное недоказуемое утверждение.
 
|proof =
 
|proof =
Можно переформулировать теорему следующим образом: невозможно доказать, что <tex> p(x) = \pepr </tex>.
+
Поясним, что это значит. Так как любой язык программирования эквивалентен [[Машина Тьюринга | машине Тьюринга]], то всё связанное с ним кодируется в [[Теории первого порядка | логике первого порядка]] с [[Классы_чисел#Аксиомы_Пеано | аксиомами Пеано]] (для этого достаточно, чтобы программа умела прибавлять к числу единицу и вызывать подпрограммы), поэтому можно в терминах программ получать утверждения, эквивалентные тем, что строил Гёдель.
 +
 
 +
Можно переформулировать теорему следующим образом: невозможно доказать, что <tex> p(x) = \perp </tex>.
  
Тогда напишем такую программу:
+
Таким образом напишем такую программу:
 
<code>
 
<code>
 
   p(x):
 
   p(x):
Строка 82: Строка 109:
 
</code>
 
</code>
 
}}
 
}}
== Аналог II теоремы Гёделя о неполноте ==
+
 
 
== Теорема о неподвижной точке ==
 
== Теорема о неподвижной точке ==
Зафиксируем
+
Зафиксируем [[Главные нумерации | главную нумерацию]] <tex> W </tex>. Обозначим за <tex> W_n </tex> множество слов, допускаемых программой с номером <tex> n </tex>.
 +
{{Утверждение
 +
|id=идентификатор (необязательно), пример: proposalF.
 +
|statement = <tex> \exists n : W_n = \{n\} </tex>
 +
|proof=
 +
Напишем такую программу:
 +
<code>
 +
  p(q):
 +
    '''if''' p.getSrc() == q.getSrc()
 +
      '''return''' 1
 +
    '''else'''
 +
      '''while''' ''true''
 +
</code>
 +
Программа <tex> p </tex> знает свой код, что то же самое, что и знает свой номер. Как видно из её кода, она допускает только одно число {{---}} свой номер.
 +
}}
 +
 
 +
== Ссылки ==
 +
* [[wikipedia:Kolmogorov_complexity | Wikipedia {{---}} Kolmogorov_complexity]]
 +
* [http://people.cs.uchicago.edu/~fortnow/papers/kaikoura.pdf Kolmogorov Complexity]
 +
* [http://www.lektorium.tv/lecture/?id=13494 Дмитрий Ицыксон {{---}} Вычислимость и логика, Колмогоровская сложность]
 +
 
 +
[[Категория: Теория формальных языков]]

Текущая версия на 23:56, 2 января 2017

По теореме о рекурсии, программа может знать свой исходный код. Значит, в неё можно написать функцию [math] \mathrm{getSrc()} [/math], которая вернёт строку — исходный код программы. Далее будем считать, что такая функция определена в каждой программе.

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

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

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

 p(x):
   if u(getSrc(), 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] L_A [/math] разрешим. Тогда напишем такую программу:

 propA(code):
   // программа, разрешающее свойство языка [math] A [/math]
 f(x):
   // такая программа [math] f [/math], что [math]f \in A [/math]; существует потому что [math] A [/math] — нетривиальное свойство
 g(x):
   // такая программа [math] g [/math], что [math]g \notin A [/math]; существует потому что [math] A [/math] — нетривиальное свойство 
 p(x):
   if propA(getSrc())
       return g(x)
   else
       return f(x)

Если [math] p [/math] не удовлетворяет свойству [math] A [/math], тогда будет выполняться всегда вторая ветка, и [math] L(p) = L(f) [/math]. Но язык программы [math] f [/math] принадлежит [math] A [/math]. Получили противоречие.

Если [math] p [/math] удовлетворяет свойству [math] A [/math], то [math] L(p) = L(g) [/math], а [math] g \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]|\mathrm{getSrc()}|[/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.getSrc() == q.getSrc()
     return 1
   else
     while true

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

Ссылки