Изменения

Перейти к: навигация, поиск
Теорема Успенского-Райса: Fix html code issues
|definition='''Язык свойства''' (англ. ''language of property'') <tex> A </tex> {{---}} множество программ, языки которых обладают этим свойством: <tex>L(A) \overset{\underset{\mathrm{def}}{}}{=} \lbrace p \mid L(p) \in A \rbrace </tex>.
}}
 
'''Отметим''', что принадлежность программы <tex>p</tex> языку свойства <tex>A</tex> можно выразить двумя эквивалентными утверждениями:
:<tex>L(p) \in A</tex>
:<tex>p \in L(A)</tex>
Далее в конспекте будет употребляться <tex>p \in L(A)</tex>.
 
{{Определение
|definition=Свойство <tex> A </tex> называется '''разрешимым''' (англ. ''recursive''), если <tex>L(A) </tex> является [[Разрешимые_(рекурсивные)_языки|разрешимым]].
Псевдокод для программы в общем случае, то есть для проверки того, что язык удовлетворяет свойству :
<tex>p_A(p_X)</tex>
'''return''' <tex>L(p_X) \in L(A)</tex>
Псевдокод полуразрешителя для языка свойства из первого примера:
|statement=
Язык никакого нетривиального свойства <tex>A</tex> не является разрешимым.
|proof}}===Доказательство===Приведём доказательство от противного. Предположим, что Пусть <tex>Ap_\infty</tex> разрешимо{{---}} всегда зацикливающийся алгоритм.
Пусть '''Рассмотрим случай, когда <tex>p_\infty\in L(A)</tex>.'''  Приведём доказательство от противного. Предположим, что <tex>A</tex> {{---}} всегда зацикливающийся алгоритмразрешимо.
'''Рассмотрим случайязык <tex>S</tex>, когда такой что <tex>p_S \in \infty overline{A}</tex> (такой язык существует, так как <tex>A</tex> {{---}} нетривиально). Тогда <tex>p_S \in L(\overline{A})</tex>.'''
Рассмотрим <tex>p_a</tex> {{---}} программу, такую что <tex>a \in \overline A</tex> (такое <tex>a</tex> существует, т.к. <tex>A</tex> {{---}} нетривиально), а также произвольное перечислимое неразрешимое множество <tex>X</tex>. Пусть <tex>p_X(n)</tex> {{---}} полуразрешитель <tex>X</tex>.
Зафиксируем произвольное <tex>n \in \mathbb{N}</tex> и построим следующую функцию
<tex>V_n(x) = \begin{cases}
p_ap_S(x), n \in X \\
p_\infty(x), n \notin X \\
\end{cases} </tex>
<code>
'''function''' <tex>V_n</tex>(x):
'''if''' <tex>p_X</tex>(n) == 1
'''return''' <tex>p_ap_S</tex>(x)
'''while''' ''true''
</code>
Получили, что если <tex>n \in X</tex>, то <tex>V_n \in L(\overline SA)</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>aV_n</tex>, лежит ли оно в <tex>L(\overline{A})</tex>. Но это тоже самое, что и проверка <tex>n \in X</tex>. Тогда можно для каждого <tex>n</tex> проверить, лежит ли оно в <tex>X</tex>, а следовательно и построить разрешитель для <tex>X</tex>. Так как <tex>X</tex> {{---}} неразрешимо, получили противоречие.
'''Теперь рассмотрим случай, когда <tex>p_\infty \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> Если <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>. Опять получили противоречие.
== См. также ==
Анонимный участник

Навигация