304
правки
Изменения
м
bugfixes
Теорема Райса-Шапиро позволяет дать простое описание перечислимым свойствам языков. Заметим, что вычислимо работать с произвольными языками возможности нет, поэтому далее неявно подразумевается, что все рассматриваемые языки являются перечислимыми.
{{Определение
|definition=
A(L)
'''for ''' t = 1 '''to ''' <tex>\infty</tex> '''for ''' i = 1 '''to ''' t
ok <tex>\leftarrow</tex> true
'''for ''' j = 1 '''to ''' <tex>|\Gamma_i|</tex> '''if ''' <tex>\lnot L|_t (\Gamma_{ij})</tex>
ok <tex>\leftarrow</tex> false
'''if ''' ok '''return ''' true
Для доказательства в другую сторону понадобятся следующие леммы:
g(x):
'''return ''' f(x, y)
После этого запустим параллельно проверки <tex>y \in K</tex> и <tex>L(g) \in A</tex>. Если <tex>y \in K</tex>, то первая проверка завершится. Иначе функция <tex>g</tex> задаёт язык <tex>G</tex>, который обладает свойством <tex>A</tex>, следовательно, вторая проверка завершится, сигнализируя о том, что <tex>y \notin K</tex>. Но <tex>K</tex> не является разрешимым множеством, получено противоречие.
|proof=
Строим доказательство от противного. Пусть <tex>G \in A</tex>, и любое конечное подмножество <tex>G</tex> не удовлетворяет свойству <tex>A</tex>, <tex>K</tex> — перечислимое неразрешимое множество. Определим следующую функцию:
* <tex>f(x, y) = 0</tex>false, если за <tex>x</tex> шагов перечисления <tex>K</tex> появилось слово <tex>y</tex> не появилось.
* <tex>f(x, y) = x \in G</tex> иначе.
Заметим, что если <tex>y \in K</tex>, то <tex>f(x, y)</tex> распознаёт некоторое конечное подмножество <tex>G</tex> и всё множество <tex>G</tex> иначе. Эта функция тривиальным образом разрешима, построим с её помощью разрешитель <tex>K</tex>. Аналогично доказательству первой леммы, подготовим программу <tex>g</tex>:
g(x):
'''return ''' f(x, y)
После этого параллельно запустим проверки <tex>y \in K</tex> и <tex>L(g) \in A</tex>. Аналогично, данная процедура разрешает множество <tex>K</tex>. Но <tex>K</tex> не является разрешимым, получено противоречие.
Полуразрешитель для множества образцов, удовлетворяющих <tex>A</tex> строится следующим образом: для каждого образца <tex>\gamma</tex> строится текст программы
f<tex>{}_\gamma</tex>(x):
'''return ''' x <tex>{} \in \gamma</tex>
Текст программы передаётся полуразрешителю <tex>A</tex>. Доказанные леммы говорят нам о том, что данное построение полуразрешителя корректно, то есть, язык удовлетворяет множеству образцов тогда и только тогда, когда язык удовлетворяет свойству <tex>A</tex>.
== Литература ==
* ''Верещагин Н. К., Шень A.'' Лекции по математической логике и теории алгоритмов. Часть 3. Вычислимые функции. {{---}} М.: МЦНМО, 1999. С. 134. ISBN 5-900916-36-7
* ''Хопкрофт Д., Мотвани Р., Ульман Д.'' Введение в теорию автоматов, языков и вычислений, 2-е изд. : Пер. с англ. {{---}} М.: Издательский дом «Вильямс», 2008. {{---}} С. 528 {{---}} ISBN 978-5-8459-1347-0 (рус.)
