Изменения

Перейти к: навигация, поиск

Теорема Райса-Шапиро

296 байт добавлено, 00:04, 16 января 2017
Нет описания правки
{{Определение
|definition=
'''Свойством программ''' (англ. ''property'') называется подмножество перечислимых языков.
}}
{{Определение
|definition=
'''Образцом''' (англ. ''pattern'') называется конечное множество слов, объединённое определённым общим свойством.
}}
{{Определение
Свойство языков <tex>A</tex> перечислимо тогда и только тогда, когда существует перечислимое множество образцов <tex>\Gamma</tex>, такое, что <tex>L</tex> удовлетворяет <tex>A</tex> тогда и только тогда, когда <tex>L</tex> удовлетворяет <tex>\Gamma</tex>.
}}
 
1) <tex>\Rightarrow</tex>
 
Доказательство в одну сторону тривиально: пусть <tex>\Gamma</tex> — перечислимое множество образцов. Будем обозначать за <tex>\Gamma_i</tex> образец с номером <tex>i</tex>, а за <tex>\Gamma_{ij}</tex> — элемент с номером <tex>j</tex> образца с номером <tex>i</tex>. Далее приведён код полуразрешителя <tex>A</tex>, который принимает на вход код полуразрешителя <tex>L</tex> и возвращает значение <tex>L \in A</tex>.
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 2) <tex>\Leftarrow</tex>
Для доказательства в другую сторону понадобятся следующие леммы:
Вычисляется эта функция следующим образом: параллельно запускаем проверки <tex>x \in G</tex> и <tex>y \in K</tex>. Если <tex>x \in G</tex>, то <tex>x \in H</tex>, следовательно, функция возвращает единицу вне зависимости от <tex>y</tex>. Если <tex>y \in K</tex>, то запускаем проверку <tex>x \in H</tex>.
С помощью этой функции можно разрешить Разрешим множество <tex>K</tex> следующим образом: для с помощью этой функции. Для проверяемого элемента <tex>y</tex> подготовим программу <tex>g</tex>:
g(x): if <tex>x \in H</tex> '''return''' f(<tex>y \in K</tex> if <tex>x, \in G</tex> '''return''' <tex>y)\notin K</tex>
После этого запустим параллельно проверки <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> не является разрешимым множеством, получено противоречие.
Заметим, что если <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>\Gamma</tex> строится следующим образом: для каждого образца <tex>\gamma</tex> строится текст программы
f<tex>{}_\gamma</tex>(x): '''return''' x <tex>{} \in \gamma</tex>
Текст программы передаётся полуразрешителю <tex>A</tex>.
Пусть <tex>L \in A</tex>. Тогда по второй лемме найдётся образец <tex>\gamma</tex>, который является подмножеством <tex>L</tex> и удовлетворяет свойству <tex>A</tex>. Следовательно, этот образец лежит в множестве <tex>\Gamma</tex> и язык <tex>A</tex> удовлетворяет множеству образцов <tex>\Gamma</tex>, что и требовалось доказать.
 == Литература См. также==  == Источники информации ==
* ''Верещагин Н. К., Шень A.'' Лекции по математической логике и теории алгоритмов. Часть 3. Вычислимые функции. {{---}} М.: МЦНМО, 1999. С. 134. ISBN 5-900916-36-7
* ''Хопкрофт Д., Мотвани Р., Ульман Д.'' Введение в теорию автоматов, языков и вычислений, 2-е изд. : Пер. с англ. {{---}} М.: Издательский дом «Вильямс», 2008. {{---}} С. 528 {{---}} ISBN 978-5-8459-1347-0 (рус.)
192
правки

Навигация