|
|
| Строка 1: |
Строка 1: |
| − | == Определение образца ==
| |
| − |
| |
| − | {{Определение
| |
| − | |definition=
| |
| − | Пусть <tex>\gamma=\{\langle x_1,y_1\rangle,\langle x_2,y_2\rangle,\ldots ,\langle x_n,y_n\rangle\}</tex>.<br />
| |
| − | Тогда <tex>\gamma</tex> называется образцом.
| |
| − | }}
| |
| − |
| |
| − | == Свойство образца ==
| |
| − |
| |
| | {{Определение | | {{Определение |
| | |definition= | | |definition= |
| − | Пусть <tex>A_{\gamma}=\{p | p(x_1)=y_1 \wedge p(x_2)=y_2 \wedge \ldots \wedge p(x_n)=y_n\}</tex>, где <tex>\langle x_i, y_i\rangle \in \gamma</tex>.<br />
| + | '''Образцом''' называется конечное множество слов. |
| − | Тогда <tex>A_{\gamma}</tex> называется свойством образца <tex>\gamma</tex>.
| |
| | }} | | }} |
| | + | Будем говорить, что язык удовлетворяет образцу <tex>A</tex>, если он содержит все слова <tex>A</tex>. Также будем говорить, что язык удовлетворяет множеству образцов, если он удовлетворяет хотя бы одному образцу из этого множества. |
| | | | |
| − | == Лемма о перечислимости свойства образца ==
| + | Заметим, что образцы являются конструктивными объектами, следовательно, можно говорить о разрешимых и перечислимых множествах образцов. |
| − | | |
| − | {{Лемма
| |
| − | |statement =
| |
| − | Свойство <tex>A_{\gamma}</tex> перечислимо для любого образца <tex>\gamma</tex>.
| |
| − | |proof =
| |
| − | Построим полуразрешитель <tex>A_{\gamma}</tex>. Он будет возвращать 1 для программы <tex>p</tex>, если <tex>p(x_i)</tex> завершится с результатом <tex>y_i</tex> для всех элементов образца <tex>\langle x_i, y_i\rangle</tex>. В противном случае полуразрешитель будет зависать.
| |
| − | <tex>q(p):</tex>
| |
| − | for <tex>\langle x_i, y_i\rangle \in \gamma</tex>
| |
| − | if <tex>p(x_i) \not= y_i</tex>
| |
| − | while True
| |
| − | return 1
| |
| − | Полуразрешителя достаточно для доказательства перечислимости.
| |
| − | }}
| |
| − | | |
| − | | |
| − | == Лемма о перечислимости свойства перечислимого множества образцов ==
| |
| − | | |
| − | {{Лемма
| |
| − | |statement =
| |
| − | Пусть <tex>\Gamma</tex> {{---}} перечислимое множество образцов, <tex>A_{\Gamma} = \bigcup\limits_{\gamma \in \Gamma}{A_{\gamma}}</tex>.
| |
| − | Тогда <tex>A_{\Gamma}</tex> является перечислимым.
| |
| − | |proof =
| |
| − | Построим полуразрешитель <tex>A_{\Gamma}</tex>. Он будет брать <tex>k</tex> первых образцов из <tex>\Gamma</tex> и для каждого их них проверять принадлежность программы <tex>p</tex> свойству этого образца с ограничением по времени <tex>k</tex> для всех <tex>k</tex> от 1 до бесконечности. При обнаружении образца со свойством, которому принадлежит <tex>p</tex>, полуразрешитель завершится и вернёт 1. В противном случае он останется зависшим.
| |
| − | <tex>q(p):</tex>
| |
| − | for <tex>k = 1\ldots +\infty</tex>
| |
| − | for <tex>\gamma \in \Gamma[1..k]</tex>
| |
| − | if <tex>(p \in A_{\gamma})|_{TL(k)}</tex>
| |
| − | return 1
| |
| − | Полуразрешителя достаточно для доказательства перечислимости.
| |
| − | }}
| |
| − | | |
| − | | |
| − | == Теорема Райса-Шапиро ==
| |
| | | | |
| | {{Теорема | | {{Теорема |
| − | |statement = | + | |about= |
| − | Свойство функций <tex>A</tex> перечислимо тогда и только тогда, когда <tex>\exists \Gamma: A = A_{\Gamma}</tex>, где <tex>\Gamma</tex> {{---}} перечислимое множество образцов. | + | Райса-Шапиро |
| − | |proof =
| + | |statement= |
| − | <tex>\Leftarrow</tex> | + | Свойство языков <tex>A</tex> перечислимо тогда и только тогда, когда существует перечислимое множество образцов <tex>\Gamma</tex>, такое, что <tex>L</tex> удовлетворяет <tex>A</tex> тогда и только тогда, когда <tex>L</tex> удовлетворяет <tex>\Gamma</tex>. |
| − | | |
| − | Очевидно (перебор по TL).
| |
| − | | |
| − | | |
| − | <tex>\Rightarrow</tex>
| |
| − | | |
| − | Здесь нам потребуются две вспомогательные леммы.
| |
| − | {{Лемма
| |
| − | |statement =
| |
| − | Пусть <tex>A</tex> {{---}} перечислимое свойство функций, <tex>g \in A</tex>, <tex>h</tex> {{---}} продолжение <tex>g</tex>.
| |
| − | Тогда <tex>h \in A</tex>.
| |
| − | |proof =
| |
| − | Докажем от противного.
| |
| − | Пусть <tex>g \in A</tex>, <tex>h</tex> {{---}} продолжение <tex>g</tex>, <tex>h \notin A</tex>.
| |
| − | | |
| − | Рассмотрим перечислимое и неразрешимое множество <tex>K</tex> и следующую программу:
| |
| − | | |
| − | <tex>V(n, x) =
| |
| − | \begin{cases}
| |
| − | h(x)\text{, if $n \in K$;}\\
| |
| − | g(x)\text{, else.}
| |
| − | \end{cases}</tex>
| |
| − | | |
| − | <tex>V</tex> {{---}} вычислимая (можно параллельно запустить <tex>g(x)</tex> и проверку, принадлежит ли <tex>n</tex> множеству <tex>K</tex> (просто перечисляя это множество); если <tex>g(x)</tex> успешно выполнится, то вернуть её результат).
| |
| − | | |
| − | Пусть <tex>p(x)=V(n, x)</tex>.<br>
| |
| − | Назовем (1) проверку на принадлежность <tex> n </tex> множеству <tex> K </tex> (просто перечисляя это множество), а (2) проверку на принадлежность <tex> p </tex> множеству <tex> A </tex>.
| |
| − | Тогда программа, которая параллельно запускает проверки (1) и (2), является разрешающей программой для множества <tex>K</tex>, так как:
| |
| − | * если <tex>n \in K</tex>, то проверка (1) завершится, а проверка (2) зависнет (<tex>p</tex> ведёт себя как <tex>h</tex>, которая не содержится в <tex>A</tex>); пусть в этом случае разрешающая программа для <tex>K</tex> возвращает 1;
| |
| − | * если <tex>n \notin K</tex>, то проверка (1) зависнет, а проверка (2) завершится (<tex>p</tex> ведёт себя как <tex>g</tex>, которая содержится в <tex>A</tex>); пусть в этом случае разрешающая программа для <tex>K</tex> возвращает 0.
| |
| − | | |
| − | Получили противоречие, так как брали <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>\not\exists h</tex>, которое удовлетворяет условию леммы.
| |
| − | | |
| − | Рассмотрим перечислимое и неразрешимое множество <tex>K</tex> и следующую программу:
| |
| − | | |
| − | <tex>V(n, x) =
| |
| − | \begin{cases}
| |
| − | g(x)\text{, if (0);}\\
| |
| − | \perp\text{, else;}
| |
| − | \end{cases}</tex>
| |
| − | | |
| − | где условие <tex>(0)</tex> следующее: через <tex>x</tex> шагов перечисления <tex>K</tex> число <tex>n</tex> не появилось.<br>
| |
| − | Назовем (1) проверку на принадлежность <tex> n </tex> множеству <tex> K </tex> (просто перечисляя это множество), а (2) проверку на принадлежность <tex> V(n, x) </tex> множеству <tex> A </tex>.
| |
| − | | |
| − | Тогда программа, которая параллельно запускает проверки (1) и (2), является разрешающей программой для множества <tex>K</tex>, так как:
| |
| − | * если <tex>n \notin K</tex>, то <tex>V(n, x) \equiv g(x)</tex> для <tex>\forall n</tex>, поэтому проверка (2) завершится. Проверка (1) зависнет. Пусть в этом случае разрешающая программа для <tex>K</tex> возвращает 0;
| |
| − | * если <tex>n \in K</tex>, то завершится проверка (1). Также, в этом случае <tex>|Dom(V(n, x))| < +\infty</tex>, так как <tex>V(n, x) = g(x)</tex> при <tex>x = 0\ldots t-1</tex> для какого-то <tex>t</tex>. <tex>g</tex> является продолжением <tex>V(n, x)</tex>. По предположению от противного <tex>V(n, x) \notin A</tex> <tex>\Rightarrow</tex> проверка (2) зависнет. Пусть в этом случае разрешающая программа для <tex>K</tex> возвращает 1.
| |
| − | | |
| − | Противоречие, так как брали неразрешимое <tex>K</tex>.
| |
| − | }}
| |
| − | | |
| − | | |
| − | Вернёмся к доказательству теоремы.
| |
| − | | |
| − | Функции с конечной областью определения записываются так:
| |
| − | | |
| − | <tex>f(x):</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>
| |
| − | | |
| − | Такие функции перечислимы. Значит, такие функции, удоволетворяющие <tex>A</tex>, тоже перечислимы.
| |
| − | | |
| − | <tex>A_{\Gamma} \subseteq A</tex> по первой вспомогательной лемме.
| |
| − | | |
| − | <tex>A \subseteq A_{\Gamma}</tex> по второй вспомогательной лемме.
| |
| − | | |
| − | Значит, <tex>A = A_{\Gamma}</tex>.
| |
| | }} | | }} |
| − |
| |
| | | | |
| | == Литература == | | == Литература == |
| | * ''Верещагин Н. К., Шень A.'' Лекции по математической логике и теории алгоритмов. Часть 3. Вычислимые функции. {{---}} М.: МЦНМО, 1999. С. 134. ISBN 5-900916-36-7 | | * ''Верещагин Н. К., Шень A.'' Лекции по математической логике и теории алгоритмов. Часть 3. Вычислимые функции. {{---}} М.: МЦНМО, 1999. С. 134. ISBN 5-900916-36-7 |
| | * ''Хопкрофт Д., Мотвани Р., Ульман Д.'' Введение в теорию автоматов, языков и вычислений, 2-е изд. : Пер. с англ. {{---}} М.: Издательский дом «Вильямс», 2008. {{---}} С. 528 {{---}} ISBN 978-5-8459-1347-0 (рус.) | | * ''Хопкрофт Д., Мотвани Р., Ульман Д.'' Введение в теорию автоматов, языков и вычислений, 2-е изд. : Пер. с англ. {{---}} М.: Издательский дом «Вильямс», 2008. {{---}} С. 528 {{---}} ISBN 978-5-8459-1347-0 (рус.) |
