Изменения

Пусть <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>конечное множество слов.

== Лемма о перечислимости свойства образца == {{Лемма|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Полуразрешителя достаточно для доказательства перечислимости.}}  == Теорема Райса-Шапиро ==

|about=Райса-Шапиро|statement =Свойство функций языков <tex>A</tex> перечислимо тогда и только тогда, когда <tex>\exists \Gamma: A = A_{\Gamma}</tex>, где <tex>\Gamma</tex> {{---}} существует перечислимое множество образцов.|proof =<tex>\Leftarrow</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 AGamma</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 hL</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>KL</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>.