Изменения
→Теорема Успенского-Райса: Fix html code issues
}}
'''Отметим''', что принадлежность программы <tex>p</tex> языку свойства <tex>A</tex> можно выразить двумя эквивалентными утверждениями: : <tex>L(p) \in A</tex> и :<tex>p \in L(A)</tex>. Далее в конспекте будет употребляться <tex>p \in L(A)</tex>.
{{Определение
|statement=
Язык никакого нетривиального свойства <tex>A</tex> не является разрешимым.
Пусть <tex>p_\infty</tex> {{---}} всегда зацикливающийся алгоритм.
Приведём доказательство от противного. Предположим, что <tex>A</tex> разрешимо.
Рассмотрим язык <tex>S</tex>, такой что <tex> S \in \overline{A}</tex> (такой язык существует, так как <tex>A</tex> {{- --}} нетривиально). Тогда <tex>p_S \in L(\overline{A})</tex>.
Рассмотрим также произвольное перечислимое неразрешимое множество <tex>X</tex>. Пусть <tex>p_X(n)</tex> {{---}} полуразрешитель <tex>X</tex>.
\end{cases} </tex>
'''function''' <tex>V_n</tex>(x):
'''if''' <tex>p_X</tex>(n) == 1
'''return''' <tex>p_S</tex>(x)
'''while''' ''true''
Получили, что если <tex>n \in X</tex>, то <tex>V_n \in L(\overline A)</tex>, а если <tex>n \notin X</tex>, то <tex>V_n \in L(A)</tex>. Таким образом, <tex>n \in X \iff V_n \in L(\overline A)</tex>.
Так как <tex>\overline{A}</tex> {{---}} нетривиально (как дополнение к нетривиальному множеству), то по первой части доказательства оно неразрешимо. Следовательно, <tex>A</tex> также неразрешимо.
===Альтернативное доказательство с использованием теоремы о рекурсии===
По [[Теорема о рекурсии | теореме о рекурсии]], программа может знать свой исходный код. Значит, в неё можно написать функцию <tex> \mathrm{getSrc()} </tex>, которая вернёт строку {{---}} исходный код программы.
<tex> A </tex> {{---}} разрешимое семейство языков.
<tex> L_A </tex> {{---}} множество программ, удовлетворяющих св-ву <tex> A </tex>.
Теперь допустим, что язык <tex> L_A </tex> разрешим. Тогда напишем такую программу:
<tex>propA(code){:}</tex>
// программа, разрешающее свойство языка <tex> A </tex>
<tex>f(x){:}</tex>
// такая программа <tex> f </tex>, что <tex>f \in A </tex>; существует потому что <tex> A </tex> {{---}} нетривиальное свойство
<tex>g(x){:}</tex>
// такая программа <tex> g </tex>, что <tex>g \notin A </tex>; существует потому что <tex> A </tex> {{---}} нетривиальное свойство
<tex>p(x){:}</tex>
'''if''' <tex>propA(\mathrm{getSrc()})</tex>
'''return''' <tex>g(x)</tex>
'''else'''
'''return''' <tex>f(x)</tex>
== См. также ==
