Просмотр исходного текста страницы Теорема Райса-Шапиро

== Определение образца ==

{{Определение
|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=
Пусть <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>:
 <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>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 =
Свойство функций <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 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>.
}}