Изменения

Перейти к: навигация, поиск
Альтернативное доказательство с использованием теоремы о рекурсии
== Свойства языков ==
 
Рассмотрим множество всех [[Перечислимые_языки|перечислимых]] языков <tex> \mathrm {RE} </tex>.
{{Определение
|definition='''Свойством языков''' (англ. ''property of languages'') называется множество <tex> A \subset \mathrm {RE} </tex>.
}}
{{Определение
|definition=Рассмотрим множество перечислимых языков <tex>RE</tex>.*Свойством языков называется множество <tex>A \subset RE</tex>.*Свойство <tex>A</tex> называется '''тривиальным''' (англ. ''trivial''), если <tex>A = \varnothing </tex> или <tex>A = \mathrm {RE} </tex>.*Языком }}{{Определение|definition='''Язык свойства называется ''' (англ. ''language of property'') <tex> A </tex> {{---}} множество программ, языки которых обладают этим свойством: <tex>L(A) \overset{\underset{\mathrm{def}}{}}{=} \lbrace p | \mid L(p) \in A \rbrace </tex>.*Свойство <tex>A</tex> называется разрешимым (перечислимым), если <tex>L(A)</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> является [[Разрешимые_(рекурсивные)_языки|разрешимым]].
}}
=== Примеры ===
'''Примеры свойств''':
# Язык должен содержать слово ''hello''.
# Язык должен содержать хотя бы одно простое число.
 
Псевдокод для разрешителя <tex>L(A)</tex>, где <tex>A = \mathrm {RE}: </tex>
<tex>p_A(p_X)</tex> <font color="green"> // <tex>p_X</tex> {{---}} полуразрешитель некоторого языка</font>
'''return''' ''true''
 
Псевдокод для программы в общем случае, то есть для проверки того, что язык удовлетворяет свойству :
<tex>p_A(p_X)</tex>
'''return''' <tex>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>\varnothing \notin AX</tex> . Пусть <tex>p_X(в противном случае перейдем к n)</tex>RE \setminus A{{---}} полуразрешитель <tex>X</tex>, которое также будет разрешимым и нетривиальным).
В то же время, поскольку Зафиксируем произвольное <tex>An \in \mathbb{N}</tex> непусто, найдется перечислимый язык и построим следующую функцию <tex>V_n(x) = \begin{cases} p_S(x), n \in X \in A</tex>. Пусть <tex>p_X</tex> - полуразрешитель <tex>\ p_\infty(x), n \notin X\\\end{cases} </tex>.
Рассмотрим вспомогательную программу:<code> '''function''' <tex>V_n</tex>g_{i,(x}(y): '''if''' <tex>p_X</tex> if U(i, xn) == 1 '''return ''' <tex>p_X(y)p_S</tex>(x) else '''while''' ''true'' зависнуть</code>
Нетрудно понятьПолучили, что в разумной модели вычислений номер этой программы можно вычислить по данным если <tex>in \in X</tex>,xто <tex>V_n \in L(\overline A)</tex>. Значит, можно рассмотреть такую программу: а если <tex>US(n \langle inotin X</tex>, x то <tex>V_n \rangle in L(A)</tex> return . Таким образом, <tex>p_A n \in X \iff V_n \in L( g_{i,x} \overline A) </tex>.
ЗаметимТак как <tex>\overline A</tex> {{---}} разрешимо, то можно проверить для любого <tex>V_n</tex>, чтолежит ли оно в <tex>L(g_\overline{i,xA}) = </tex>. Но это тоже самое, что и проверка <tex>n \begin{cases} in X & U(i</tex>. Тогда можно для каждого <tex>n</tex> проверить, x) = 1 \\ \varnothing & U(iлежит ли оно в <tex>X</tex>, x) \neq 1 \\\end{cases}а следовательно и построить разрешитель для <tex>X</tex>. Так как <tex>X</tex>{{---}} неразрешимо, получили противоречие.
'''Теперь рассмотрим случай, когда <tex>p_\infty \in L(\overline{A})</tex>.'''  Так как <tex>\overline{A}</tex> {{---}} нетривиально (как дополнение к нетривиальному множеству), то по первой части доказательства оно неразрешимо. Следовательно, <br/tex> A</tex> также неразрешимо.US(\langle i===Альтернативное доказательство с использованием теоремы о рекурсии===По [[Теорема о рекурсии | теореме о рекурсии]], программа может знать свой исходный код. Значит, x в неё можно написать функцию <tex> \rangle mathrm{getSrc() = p_A(g_} </tex>, которая вернёт строку {{i,x---}}) = \beginисходный код программы. <tex> A </tex> {{cases---}} разрешимое семейство языков. <tex> L_A </tex> {{---}} множество программ, удовлетворяющих св-ву <tex> A </tex>. Теперь допустим, что язык <tex> L_A </tex> разрешим. Тогда напишем такую программу: <code> p_A<tex>propA(p_Xcode) & U(i{:}</tex> // программа, x) = 1 \\разрешающее свойство языка <tex> A </tex> p_A(p_\varnothing ) & U<tex>f(i, x) \neq 1 \\{:}</tex> // такая программа <tex> f </tex>, что <tex>f \endin A </tex>; существует потому что <tex> A </tex> {cases{---} = \begin{cases}нетривиальное свойство 1 & U<tex>g(i, x) = 1 \{:}</tex> // такая программа <tex> g </tex>, что <tex>g \notin A </tex>; существует потому что <tex> A </tex> {{---}} нетривиальное свойство 0 & U<tex>p(i, x) \neq 1 \\{:}</tex> '''if''' <tex>propA(\endmathrm{casesgetSrc()})</tex> '''return''' <tex>g(x)</tex> '''else''' '''return''' <tex>f(x)</tex></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>. Опять получили противоречие. == См. также ==* [[Теорема о рекурсии]]* [[Теорема Райса- программаШапиро]] == Источники информации ==* [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.[[Категория: Теория формальных языков]][[Категория: Теория вычислимости]][[Категория: Разрешимые и перечислимые языки]]
313
правок

Навигация