Изменения

Перейти к: навигация, поиск
Теорема Успенского-Райса: 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> <font color="green"> // <tex>p_A</tex> {{---}} полуразрешитель, так как <tex>X</tex> {{---}} перечислимый язык в общем случае</font> '''return''' <tex>L(p_X) \in L(A)</tex>
Псевдокод полуразрешителя для языка свойства из первого примера:
<tex>p_A(p_X)</tex> <font color="green"> // <tex>X</tex> {{---}} перечислимый язык в общем случае, поэтому <tex>p_A</tex> {{---}} полуразрешитель (по [[Теорема Райса-Шапиро |теореме Райса-Шапиро]])</font>
'''return''' <tex>p_X</tex>('hello')
{{Теорема
|statement=
Язык никакого нетривиального свойства <tex>A</tex> не является разрешимым.|proof}}===Доказательство===Пусть <tex>p_\infty</tex> {{---}} всегда зацикливающийся алгоритм.  '''Рассмотрим случай, когда <tex>p_\infty \in L(A)</tex>.'''  Приведём доказательство от противного. Предположим, что <tex>A</tex> разрешимо. ПредположимРассмотрим язык <tex>S</tex>, такой что <tex>S \in \overline{A}</tex> разрешимо и нетривиально(такой язык существует, так как <tex>p_AA</tex> {{---}} программа, разрешающая нетривиально). Тогда <tex>p_S \in L(\overline{A})</tex>. Рассмотрим также произвольное перечислимое неразрешимое множество <tex>X</tex>. Пусть <tex>p_X(n)</tex> {{---}} полуразрешитель <tex>X</tex>.
Не умаляя общности, можно считать, что Зафиксируем произвольное <tex>n \varnothing in \notin A</tex> (в противном случае перейдём к <tex> \mathrm mathbb{REN} \setminus A</tex>, которое также будет разрешимым и нетривиальным, так как построим следующую функцию <tex> V_n(x) = \mathrm begin{REcases} p_S(x), n \setminus A in X \neq \varnothing </tex> и <tex> p_\infty(x), n \mathrm {RE} notin X \setminus A \neq \mathrm end{REcases} ) </tex>.
Поскольку '''function''' <tex>AV_n</tex> непусто, то найдётся перечислимый язык <tex>X \in A</tex>. Пусть (x): '''if''' <tex>p_X</tex> {{---}} полуразрешитель (n) == 1 '''return''' <tex>Xp_S</tex>.(x) '''while''' ''true''
Рассмотрим вспомогательную программу: Получили, что если <tex>n \in X</tex>, то <tex>V_n \in L(\overline A)</tex>, а если <tex>n \notin X</tex>, то <tex> UV_n \in L(iA)</tex>. Таким образом,x<tex>n \in X \iff V_n \in L(\overline A)</tex> {{---}} [[Универсальная функция | универсальная функция]].
Тогда Так как <tex>\overline A</tex> {{---}} разрешимо, то можно проверить для произвольных любого <tex>V_n</tex>, лежит ли оно в <tex>iL(\overline{A})</tex> . Но это тоже самое, что и проверка <tex> x n \in X</tex> можем написать такую программу. Тогда можно для каждого <tex>g_{in</tex> проверить,x}(y):лежит ли оно в <tex>X</tex> '''if''' , а следовательно и построить разрешитель для <tex>U(i, x)X</tex> == 1 '''return''' . Так как <tex>p_X(y)X</tex> '''else''' '''while''' ''true''{{---}} неразрешимо, получили противоречие.
Нетрудно понять'''Теперь рассмотрим случай, что в разумной модели вычислений номер этой программы можно вычислить по данным когда <tex>i</tex> и <tex>x</tex>. Значит, можно рассмотреть такую программу: <tex>USp_\infty \in L(\langle i, x \rangle overline{A})</tex> '.''return''' <tex>p_A ( g_{i,x} ) </tex>
Заметим, чтоТак как <tex>L(g_\overline{i,xA}) = \begin</tex> {{cases---} X} нетривиально (как дополнение к нетривиальному множеству), & U(iто по первой части доказательства оно неразрешимо. Следовательно, x) <tex>A</tex> также неразрешимо.===Альтернативное доказательство с использованием теоремы о рекурсии=== 1; \\ \varnothingПо [[Теорема о рекурсии | теореме о рекурсии]], & U(iпрограмма может знать свой исходный код. Значит, x) \neq 1; \в неё можно написать функцию <tex> \\endmathrm{casesgetSrc()}</tex>, которая вернёт строку {{---}} исходный код программы.
Исключение пустого множества нам нужно чтобы различать <tex> XA </tex> и пустое{{---}} разрешимое семейство языков.Следовательно<tex> L_A </tex> {{---}} множество программ, удовлетворяющих св-ву <tex> A <br/tex>. Теперь допустим, что язык <tex> L_A </tex> разрешим. Тогда напишем такую программу:US <tex>propA(\langle icode){:}</tex> // программа, разрешающее свойство языка <tex> A </tex> <tex>f(x \rangle ) = p_A(g_{i:}</tex> // такая программа <tex> f </tex>,x}) = что <tex>f \beginin A </tex>; существует потому что <tex> A </tex> {cases{---}} нетривиальное свойство p_A<tex>g(p_Xx){:}</tex> // такая программа <tex> g </tex>, & U(i, x) = 1что <tex>g \notin A </tex>; \\существует потому что <tex> A </tex> {{---}} нетривиальное свойство p_A(p_\varnothing ), & U<tex>p(i, x) \neq 1; \\\end{cases:} = </tex> '''if''' <tex>propA(\beginmathrm{casesgetSrc()})</tex> 1, & U '''return''' <tex>g(i, x) = 1; \\</tex> '''else''' 0, & U '''return''' <tex>f(i, x) \neq 1; \\</tex>\end{cases}Если <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>. Опять получили противоречие.
== См. также ==
== Источники информации ==
* [https://en.wikipedia.org/wiki/Rice%27s_theorem Wikipedia — Rice's theorem]
* Rice, H. G. "{{---}} Classes of Recursively Enumerable Sets and Their Decision Problems." {{---}} Trans. Amer. Math. Soc. 74, 358-366, 1953.* Хопкрофт Д., Мотванн Р., Ульманн Д. {{---}}Введение в теорию автоматов, языков и вычислений страница {{---}} стр. 397.[[Категория: Теория формальных языков]]
[[Категория: Теория вычислимости]]
[[Категория: Теория формальных языковРазрешимые и перечислимые языки]]
Анонимный участник

Навигация