Изменения

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

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

3479 байт добавлено, 19:31, 4 сентября 2022
м
rollbackEdits.php mass rollback
== {{Определение образца =|definition='''Образцом''' (англ. ''pattern'') называется конечное множество слов, объединённое [[Свойства_перечислимых_языков._Теорема_Успенского-Райса|свойством]].}}
{{Определение
|definition=
Пусть '''Язык <tex>\gamma=\{L</tex> удовлетворяет свойству <x_1,y_1tex>,A<x_2,y_2/tex>''',\ldots ,если <x_n,y_ntex>L \}in A</tex>.<br />Тогда ( этот язык содержится в <tex>\gammaA</tex> называется образцом).
}}
 
== Свойство образца ==
{{Определение
|definition=
Пусть '''Язык <tex>A_{\gamma}=\{p | p(x_1)=y_1 \wedge p(x_2)=y_2 \wedge \ldots \wedge p(x_n)=y_n\}L</tex>, где удовлетворяет образцу <tex><x_i, y_i> \in \gammaX</tex>.<br />Тогда ''', если <tex>A_{\gamma}L</tex> называется свойством образца содержит все элементы <tex>\gammaX</tex>.
}}
 == Лемма о перечислимости свойства образца == {{ЛеммаОпределение|statement definition=Свойство '''Язык <tex>A_{\gamma}L</tex> перечислимо для любого образца удовлетворяет множеству образцов <tex>\gammaGamma</tex>.|proof =Очевидно, как строится программа, которая возвращает 1''', если <tex>p \in A_{\gamma}</tex> (запускаем <tex>pL</tex> на удовлетворяет хотя бы одному образцу <tex>xX \in \Gamma</tex>-ах и проверяем, что программа вернёт соответствующие <tex>y</tex>-ки).Такой программы достаточно для доказательства перечислимости.
}}
 
== Лемма о перечислимости свойства перечислимого множества образцов ==
{{Лемма
|statement =Пусть <tex>\GammaA</tex> - перечислимое множество образцовсвойство языков, <tex>A_{\Gamma} = \bigcup\limits_{\gamma G \in \Gamma}{A_{\gamma}}A</tex>.Тогда верно следствие: <tex>A_{G \subset H \Rightarrow H \Gamma}in A</tex> - перечислимо.|proof =Приведём программу, выдающую 1, если Строим доказательство от противного. Пусть <tex>p G \in A_{\Gamma}A</tex>: , <tex>q(p):G \subset H</tex> for , <tex>k = 1H \ldots +\inftynotin A</tex> for , <tex>\gamma \in \Gamma[1..k]K</tex>— перечислимое неразрешимое множество. Построим следующую вычислимую функцию: if <tex>f(p x, y) = \begin{cases}x \in H & y \in K\\x \in A_{G & y \notin K\gamma})|_end{TL(k)cases}</tex> return 1Такой программы достаточно для доказательства перечислимости.}}
Вычисляется эта функция следующим образом: параллельно запускаем проверки <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>:
{{Теорема|statement = <tex>g(x):</tex>Свойство функций '''if''' <tex>Ax \in H</tex> перечислимо тогда и только тогда, когда '''return''' <tex>y \exists \Gamma: A = A_{\Gamma}in K</tex>, где '''if''' <tex>x \Gammain G</tex> - перечислимое множество образцов.|proof = '''return''' <tex>y \Leftarrownotin K</tex> Очевидно (перебор по TL).
После этого запустим параллельно проверки <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>\Rightarrow</tex>
Здесь нам потребуются две вспомогательные леммы.
{{Лемма
|statement =Пусть <tex>A</tex> - перечислимое свойство функций, <tex>g G \in A</tex>, . Тогда существует конечное множество <tex>hH \in A</tex> - продолжение , которое является подмножеством <tex>gG</tex>.Тогда |proof=Строим доказательство от противного. Пусть <tex>h G \in A</tex>, и любое конечное подмножество <tex>G</tex> не удовлетворяет свойству <tex>A</tex>, <tex>K</tex> — перечислимое неразрешимое множество.Определим следующую функцию:|proof * <tex>f(x, y) =false</tex>, если за <tex>x</tex> шагов перечисления <tex>K</tex> появилось слово <tex>y</tex>.Докажем от противного* <tex>f(x, y) = x \in G</tex> иначе.Пусть Заметим, что если <tex>g y \in AK</tex>, то <tex>hf(x, y)</tex> - продолжение распознаёт некоторое конечное подмножество <tex>gG</tex>, и всё множество <tex>h \notin AG</tex>иначеРассмотрим перечислимое и неразрешимое множество Эта функция тривиальным образом разрешима, построим с её помощью разрешитель <tex>K</tex> и следующую . Аналогично доказательству первой леммы, подготовим программу<tex>g</tex>:
<tex>V g(n, x) = \begin{cases}: h '''return''' f(x)\text{, if $n \in K$;}\\ g(xy)\text{, else.} \end{cases}</tex>
<tex>V</tex> - вычислимая (можно После этого параллельно запустить запустим проверки <tex>g(x)y \in K</tex> и проверку, принадлежит ли <tex>n</tex> множеству <tex>K</tex> L(просто перечисляя это множество); если <tex>g(x)</tex> успешно выполнится, то вернуть её результат). Пусть <tex>p(x)=V(n, x)</tex>. Тогда программа, которая запускает параллельно проверку, принадлежит ли <tex>n</tex> множеству <tex>K</tex> (просто перечисляя это множество), и проверку, принадлежит ли <tex>p</tex> множеству <tex>A</tex>, является разрешающей программой для множества <tex>K</tex> (так как если <tex>p \in A</tex>. Аналогично, то данная процедура разрешает множество <tex>n \notin K</tex> по построению <tex>V(n, x)</tex>).Противоречие, так как брали неразрешимое Но <tex>K</tex>не является разрешимым, получено противоречие.
}}
{{Лемма|statement =Если <tex>A</tex> '''Теорема Райса- перечислимое свойство функцийШапиро''' позволяет дать простое описание перечислимым свойствам языков. Заметим, <tex>g \in A</tex>что вычислимо работать с произвольными языками возможности нет, то <tex>\exists h</tex>поэтому далее неявно подразумевается, такое что <tex>|Dom(h)все рассматриваемые языки являются [[Перечислимые языки| < +\infty</tex>, <tex>g</tex> - продолжение <tex>h</tex>, <tex>h \in A</tex>перечислимыми]].|proof =Рассмотрим перечислимое и неразрешимое множество <tex>K</tex> и следующую программу:
<tex>V(nЗаметим, x) = \begin{cases} g(x)\text{что образцы являются конструктивными объектами, if (1);}\\ \perp\text{следовательно, else;} \end{cases}</tex>можно говорить о разрешимых и перечислимых множествах образцов.
где условие {{Теорема|about=Райса-Шапиро|statement=Свойство языков <tex>(1)A</tex> следующее: через перечислимо <tex>x</tex> шагов перечисления <tex>K\iff \exists\Gamma : L \in A \iff L \subseteq \Gamma.</tex> число <tex>n</tex> не появилось.}}
Если <tex>n \notin KLeftarrow</tex>, то <tex>V(n, x) = g(x)</tex>.
Если : Доказательство в одну сторону тривиально: пусть <tex>n \in KGamma</tex> — перечислимое множество образцов. Будем обозначать за <tex>\Gamma_i</tex> образец с номером <tex>i</tex>, то а за <tex>V(n, x) = g(x)\Gamma_{ij}</tex> — элемент с номером <tex>j</tex> образца с номером <tex>i</tex>. Далее приведён код полуразрешителя <tex>A</tex> при , который принимает на вход код полуразрешителя <tex>x = 0\ldots t-1L</tex> для какого-то и возвращает значение <tex>tL \in A</tex>.
Запустим параллельно проверку, принадлежит ли A(L): '''for''' t = 1 '''to''' <tex>n\infty</tex> множеству '''for''' i = 1 '''to''' t ok <tex>K=</tex> и проверку, принадлежит ли ''true'' '''for''' j = 1 '''to''' <tex>V|\Gamma_i|</tex> '''if''' <tex>\lnot L|_t (n, x\Gamma_{ij})</tex> множеству ok <tex>A=</tex>.''false'' '''if''' ok '''return''' ''true''
<продолжение tex>\Rightarrow</tex>:Для доказательства в другую сторону будем использовать две леммы, приведённые выше. Полуразрешитель для множества образцов, удовлетворяющих <tex>\Gamma</tex> строится следующим образом: для каждого образца <tex>\gamma</tex> строится текст программы f<tex>{}_\gamma</tex>(x): '''return''' x <tex>{}\in \gamma</tex>:Текст программы передаётся полуразрешителю <tex>A</tex>.
:Докажем, что данное построение корректно. Обозначим множество образцов, принимаемое построенным выше полурарешителем <tex>\Gamma</tex>. Пусть существует <tex>\gamma \in \Gamma</tex> такой, что <tex>L</tex> удовлетворяет <tex>\gamma</tex>. По определению <tex>\Gamma</tex>, язык <tex>\gamma</tex> удовлетворяет свойству <tex>A</tex>. Язык <tex>L</tex> удовлетворяет свойству <tex>A</tex> по первой лемме как надмножество <tex>\gamma</tex>.
Вернёмся к доказательству теоремы:Пусть <tex>L \in A</tex>. Тогда по второй лемме найдётся образец <tex>\gamma</tex>, который является подмножеством <tex>L</tex> и удовлетворяет свойству <tex>A</tex>. Следовательно, этот образец лежит в множестве <tex>\Gamma</tex> и язык <tex>A</tex> удовлетворяет множеству образцов <tex>\Gamma</tex>, что и требовалось доказать.
Функции с конечной областью определения записываются так:== См. также==
<tex>f(x)* [[m-сводимость]]* [[Примеры_неразрешимых_задач:</tex> if <tex>x = x_1</tex> return <tex>y_1</tex> <tex>\cdots</tex> if <tex>x = x_n</tex> return <tex>y_n</tex>_проблема_соответствий_Поста | Проблема соответствий Поста]] <tex>\perp</tex>* [[Неразрешимость исчисления предикатов первого порядка]]
Такие == Источники информации ==* ''Верещагин Н. К., Шень A.'' Лекции по математической логике и теории алгоритмов. Часть 3. Вычислимые функции перечислимы. Значит такие функции{{---}} М.: МЦНМО, 1999. С. 134. ISBN 5-900916-36-7* ''Хопкрофт Д., Мотвани Р., Ульман Д.'' Введение в теорию автоматов, языков и вычислений, удоволетворяющие <tex>A</tex>2-е изд. : Пер. с англ. {{---}} М.: Издательский дом «Вильямс», тоже перечислимы2008. {{---}} С. 528 {{---}} ISBN 978-5-8459-1347-0 (рус.)
<tex>A_{\Gamma} \subset A</tex> по первой вспомогательной лемме.[[Категория: Теория формальных языков]][[Категория: Теория вычислимости]]<tex>A \subset A_{\Gamma}</tex> по второй вспомогательной лемме. Значит <tex>A = A_{\Gamma}</tex>. Теорема доказана.}}[[Категория: Примеры неразрешимых задач]]
1632
правки

Навигация