Изменения

Перейти к: навигация, поиск
Теорема Успенского-Райса
|statement=
Язык никакого нетривиального свойства <tex>A</tex> не является разрешимым.
|proof}}===Доказательство===
Пусть <tex>p_\infty</tex> {{---}} всегда зацикливающийся алгоритм.
Так как <tex>\overline{A}</tex> {{---}} нетривиально (как дополнение к нетривиальному множеству), то по первой части доказательства оно неразрешимо. Следовательно, <tex>A</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>. Опять получили противоречие.
== См. также ==
313
правок

Навигация