Изменения
→Пример использования
По [[Теорема о рекурсии | теореме о рекурсии]], программа может знать свой исходный код. Значит, в неё можно написать функцию <tex> \mathrm{getSrc()} </tex>, которая вернёт строку {{---}} исходный код программы. Далее будем считать, что такая функция определена в каждой программе.
== Неразрешимость универсального языка ==
{{Утверждение
|id=proposalU.
|statement=[[Разрешимые (рекурсивные) языки#Пример неразрешимого множества | Универсальный язык]] неразрешим
|proof=
Допустим, что он разрешим. Тогда напишем такую программу:
<code>
p(x):
'''if''' u(getSrc(), x)
'''while''' ''true''
'''else'''
'''return''' 1
</code>
Если <tex> u(p, x) = 1 </tex>, тогда программа <tex> p </tex> на входе <tex> x </tex> должна вернуть <tex> 1 </tex>, но по условию <tex> if </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> L_A </tex> {{---}} множество программ, удовлетворяющих св-ву <tex> A </tex>.
Теперь допустим, что язык <tex> L_A </tex> разрешим. Тогда напишем такую программу:
<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):
'''if''' propA(getSrc())
'''return''' g(x)
'''else'''
'''return''' f(x)
</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>. Опять получили противоречие.
== Колмогоровская сложность ==
{{Определение
|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> K(0^n) \leqslant \log{n} + c </tex>, например вот такую:
<code>
<tex>p_n</tex>():
p(<tex>\varepsilon</tex>):
'''foreach''' x <tex>\in ~ \Sigma^* </tex> // перебираем слова по возрастанию длины
'''if''' <tex> K(x) > |p|</tex>// теорема о рекурсии используется здесь
print(x)
exit
Начиная с <tex> x_0 </tex>, <tex> f(x) > |p| </tex>.
}}
== 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 теоремы Гёделя о неполноте ==
{{Теорема|id =thGI. |statement = Аналог II теоремы Гёделя о неполноте В любой "достаточно богатой системе" существует истинное недоказуемое утверждение.|proof =Поясним, что это значит. Так как любой язык программирования эквивалентен [[Машина Тьюринга | машине Тьюринга]], то всё связанное с ним кодируется в [[Теории первого порядка | логике первого порядка]] с [[Классы_чисел#Аксиомы_Пеано | аксиомами Пеано]] (для этого достаточно, чтобы программа умела прибавлять к числу единицу и вызывать подпрограммы), поэтому можно в терминах программ получать утверждения, эквивалентные тем, что строил Гёдель. Можно переформулировать теорему следующим образом: невозможно доказать, что <tex> p(x) =\perp </tex>. Таким образом напишем такую программу:<code> p(x): '''foreach''' q <tex> \in ~ \Sigma^* </tex> '''if''' q proves "p(x) зависает" exit </code>}}
== Теорема о неподвижной точке ==
Зафиксируем [[Главные нумерации | главную нумерацию]] <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 Дмитрий Ицыксон {{---}} Вычислимость и логика, Колмогоровская сложность]
[[Категория: Теория формальных языков]]
