Теорема Райса-Шапиро — различия между версиями
Tsar (обсуждение | вклад) (→Теорема Райса-Шапиро: Описание разрешающей программы для K во вспомогательной лемме 1) |
м (rollbackEdits.php mass rollback) |
||
(не показано 48 промежуточных версий 8 участников) | |||
Строка 1: | Строка 1: | ||
− | + | {{Определение | |
+ | |definition= | ||
+ | '''Образцом''' (англ. ''pattern'') называется конечное множество слов, объединённое [[Свойства_перечислимых_языков._Теорема_Успенского-Райса|свойством]]. | ||
+ | }} | ||
{{Определение | {{Определение | ||
|definition= | |definition= | ||
− | + | '''Язык <tex>L</tex> удовлетворяет свойству <tex>A</tex>''', если <tex>L \in A</tex> ( этот язык содержится в <tex>A</tex>). | |
− | |||
}} | }} | ||
− | |||
− | |||
{{Определение | {{Определение | ||
|definition= | |definition= | ||
− | + | '''Язык <tex>L</tex> удовлетворяет образцу <tex>X</tex>''', если <tex>L</tex> содержит все элементы <tex>X</tex>. | |
− | |||
}} | }} | ||
− | + | {{Определение | |
− | + | |definition= | |
− | + | '''Язык <tex>L</tex> удовлетворяет множеству образцов <tex>\Gamma</tex>''', если <tex>L</tex> удовлетворяет хотя бы одному образцу <tex>X \in \Gamma</tex>. | |
− | {{ | ||
− | | | ||
− | |||
− | |||
− | |||
− | |||
}} | }} | ||
− | |||
− | |||
{{Лемма | {{Лемма | ||
− | |statement = | + | |statement= |
− | Пусть <tex> | + | Пусть <tex>A</tex> — перечислимое свойство языков, <tex>G \in A</tex>. Тогда верно следствие: <tex>G \subset H \Rightarrow H \in A</tex>. |
− | Тогда <tex> | + | |proof= |
− | |proof = | + | Строим доказательство от противного. Пусть <tex>G \in A</tex>, <tex>G \subset H</tex>, <tex>H \notin A</tex>, <tex>K</tex> — перечислимое неразрешимое множество. Построим следующую вычислимую функцию: |
− | + | <tex>f(x, y) = \begin{cases} | |
− | + | x \in H & y \in K\\ | |
− | + | x \in G & y \notin K | |
− | + | \end{cases}</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>: | |
− | + | <tex>g(x):</tex> | |
− | + | '''if''' <tex>x \in H</tex> | |
− | + | '''return''' <tex>y \in K</tex> | |
− | + | '''if''' <tex>x \in G</tex> | |
− | <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> не является разрешимым множеством, получено противоречие. | |
+ | }} | ||
− | |||
− | |||
− | |||
{{Лемма | {{Лемма | ||
− | |statement = | + | |statement= |
− | Пусть <tex>A</tex> | + | Пусть <tex>A</tex> — перечислимое свойство, <tex>G \in A</tex>. Тогда существует конечное множество <tex>H \in A</tex>, которое является подмножеством <tex>G</tex>. |
− | + | |proof= | |
− | + | Строим доказательство от противного. Пусть <tex>G \in A</tex>, и любое конечное подмножество <tex>G</tex> не удовлетворяет свойству <tex>A</tex>, <tex>K</tex> — перечислимое неразрешимое множество. Определим следующую функцию: | |
− | + | * <tex>f(x, y) = false</tex>, если за <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> | + | После этого параллельно запустим проверки <tex>y \in K</tex> и <tex>L(g) \in A</tex>. Аналогично, данная процедура разрешает множество <tex>K</tex>. Но <tex>K</tex> не является разрешимым, получено противоречие. |
− | + | }} | |
− | |||
− | |||
− | |||
− | |||
− | + | '''Теорема Райса-Шапиро''' позволяет дать простое описание перечислимым свойствам языков. Заметим, что вычислимо работать с произвольными языками возможности нет, поэтому далее неявно подразумевается, что все рассматриваемые языки являются [[Перечислимые языки|перечислимыми]]. | |
− | + | Заметим, что образцы являются конструктивными объектами, следовательно, можно говорить о разрешимых и перечислимых множествах образцов. | |
− | |||
− | |||
− | + | {{Теорема | |
+ | |about= | ||
+ | Райса-Шапиро | ||
+ | |statement= | ||
+ | Свойство языков <tex>A</tex> перечислимо <tex>\iff \exists\Gamma : L \in A \iff L \subseteq \Gamma.</tex> | ||
}} | }} | ||
+ | <tex>\Leftarrow</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>. | |
− | |||
− | |||
− | |||
− | |||
− | <tex> | + | A(L): |
− | + | '''for''' t = 1 '''to''' <tex>\infty</tex> | |
− | + | '''for''' i = 1 '''to''' t | |
− | + | ok <tex>=</tex> ''true'' | |
− | + | '''for''' j = 1 '''to''' <tex>|\Gamma_i|</tex> | |
+ | '''if''' <tex>\lnot L|_t (\Gamma_{ij})</tex> | ||
+ | ok <tex>=</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>, что и требовалось доказать. | |
− | + | == См. также== | |
− | + | * [[m-сводимость]] | |
− | + | * [[Примеры_неразрешимых_задач:_проблема_соответствий_Поста | Проблема соответствий Поста]] | |
− | + | * [[Неразрешимость исчисления предикатов первого порядка]] | |
− | |||
− | |||
− | |||
− | |||
− | + | == Источники информации == | |
+ | * ''Верещагин Н. К., Шень A.'' Лекции по математической логике и теории алгоритмов. Часть 3. Вычислимые функции. {{---}} М.: МЦНМО, 1999. С. 134. ISBN 5-900916-36-7 | ||
+ | * ''Хопкрофт Д., Мотвани Р., Ульман Д.'' Введение в теорию автоматов, языков и вычислений, 2-е изд. : Пер. с англ. {{---}} М.: Издательский дом «Вильямс», 2008. {{---}} С. 528 {{---}} ISBN 978-5-8459-1347-0 (рус.) | ||
− | + | [[Категория: Теория формальных языков]] | |
− | + | [[Категория: Теория вычислимости]] | |
− | + | [[Категория: Примеры неразрешимых задач]] | |
− | |||
− | |||
− |
Текущая версия на 19:31, 4 сентября 2022
Определение: |
Образцом (англ. pattern) называется конечное множество слов, объединённое свойством. |
Определение: |
Язык | удовлетворяет свойству , если ( этот язык содержится в ).
Определение: |
Язык | удовлетворяет образцу , если содержит все элементы .
Определение: |
Язык | удовлетворяет множеству образцов , если удовлетворяет хотя бы одному образцу .
Лемма: |
Пусть — перечислимое свойство языков, . Тогда верно следствие: . |
Доказательство: |
Строим доказательство от противного. Пусть , , , — перечислимое неразрешимое множество. Построим следующую вычислимую функцию:Вычисляется эта функция следующим образом: параллельно запускаем проверки и . Если , то , следовательно, функция возвращает единицу вне зависимости от . Если , то запускаем проверку .Разрешим множество с помощью этой функции. Для проверяемого элемента подготовим программу :После этого запустим параллельно проверки if return if return и . Если , то первая проверка завершится. Иначе функция задаёт язык , который обладает свойством , следовательно, вторая проверка завершится, сигнализируя о том, что . Но не является разрешимым множеством, получено противоречие. |
Лемма: |
Пусть — перечислимое свойство, . Тогда существует конечное множество , которое является подмножеством . |
Доказательство: |
Строим доказательство от противного. Пусть , и любое конечное подмножество не удовлетворяет свойству , — перечислимое неразрешимое множество. Определим следующую функцию:
Заметим, что если , то распознаёт некоторое конечное подмножество и всё множество иначе. Эта функция тривиальным образом разрешима, построим с её помощью разрешитель . Аналогично доказательству первой леммы, подготовим программу :g(x): return f(x, y)После этого параллельно запустим проверки и . Аналогично, данная процедура разрешает множество . Но не является разрешимым, получено противоречие. |
Теорема Райса-Шапиро позволяет дать простое описание перечислимым свойствам языков. Заметим, что вычислимо работать с произвольными языками возможности нет, поэтому далее неявно подразумевается, что все рассматриваемые языки являются перечислимыми.
Заметим, что образцы являются конструктивными объектами, следовательно, можно говорить о разрешимых и перечислимых множествах образцов.
Теорема (Райса-Шапиро): |
Свойство языков перечислимо |
- Доказательство в одну сторону тривиально: пусть — перечислимое множество образцов. Будем обозначать за образец с номером , а за — элемент с номером образца с номером . Далее приведён код полуразрешителя , который принимает на вход код полуразрешителя и возвращает значение .
A(L): for t = 1 tofor i = 1 to t ok true for j = 1 to if ok false if ok return true
- Для доказательства в другую сторону будем использовать две леммы, приведённые выше. Полуразрешитель для множества образцов, удовлетворяющих строится следующим образом: для каждого образца строится текст программы
f(x): return x
- Текст программы передаётся полуразрешителю .
- Докажем, что данное построение корректно. Обозначим множество образцов, принимаемое построенным выше полурарешителем . Пусть существует такой, что удовлетворяет . По определению , язык удовлетворяет свойству . Язык удовлетворяет свойству по первой лемме как надмножество .
- Пусть . Тогда по второй лемме найдётся образец , который является подмножеством и удовлетворяет свойству . Следовательно, этот образец лежит в множестве и язык удовлетворяет множеству образцов , что и требовалось доказать.
См. также
Источники информации
- Верещагин Н. К., Шень A. Лекции по математической логике и теории алгоритмов. Часть 3. Вычислимые функции. — М.: МЦНМО, 1999. С. 134. ISBN 5-900916-36-7
- Хопкрофт Д., Мотвани Р., Ульман Д. Введение в теорию автоматов, языков и вычислений, 2-е изд. : Пер. с англ. — М.: Издательский дом «Вильямс», 2008. — С. 528 — ISBN 978-5-8459-1347-0 (рус.)