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

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

Определение:

Пусть [math]\gamma=\{\langle x_1,y_1\rangle,\langle x_2,y_2\rangle,\ldots ,\langle x_n,y_n\rangle\}[/math]. Тогда [math]\gamma[/math] называется образцом.

Свойство образца

Определение:

Пусть [math]A_{\gamma}=\{p | p(x_1)=y_1 \wedge p(x_2)=y_2 \wedge \ldots \wedge p(x_n)=y_n\}[/math], где [math]\langle x_i, y_i\rangle \in \gamma[/math]. Тогда [math]A_{\gamma}[/math] называется свойством образца [math]\gamma[/math].

Лемма о перечислимости свойства образца

Лемма:

Свойство [math]A_{\gamma}[/math] перечислимо для любого образца [math]\gamma[/math].

Доказательство:

[math]\triangleright[/math]

Очевидно, как строится программа, которая возвращает 1, если [math]p \in A_{\gamma}[/math] (запускаем [math]p[/math] на [math]x[/math]-ах и проверяем, что программа вернёт соответствующие [math]y[/math]-ки). Такой программы достаточно для доказательства перечислимости.

[math]\triangleleft[/math]

Лемма о перечислимости свойства перечислимого множества образцов

{{Лемма |statement = Пусть [math]\Gamma[/math] {{---} перечислимое множество образцов, [math]A_{\Gamma} = \bigcup\limits_{\gamma \in \Gamma}{A_{\gamma}}[/math]. Тогда [math]A_{\Gamma}[/math] — перечислимо. |proof = Приведём программу, выдающую 1, если [math]p \in A_{\Gamma}[/math]:

[math]q(p):[/math]
  for [math]k = 1\ldots +\infty[/math]
      for [math]\gamma \in \Gamma[1..k][/math]
          if [math](p \in A_{\gamma})|_{TL(k)}[/math]
              return 1

Такой программы достаточно для доказательства перечислимости. }}

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

Теорема:

Свойство функций [math]A[/math] перечислимо тогда и только тогда, когда [math]\exists \Gamma: A = A_{\Gamma}[/math], где [math]\Gamma[/math] - перечислимое множество образцов.

Доказательство:

[math]\triangleright[/math]

[math]\Leftarrow[/math] Очевидно (перебор по TL). [math]\Rightarrow[/math] Здесь нам потребуются две вспомогательные леммы. Лемма: Пусть [math]A[/math] - перечислимое свойство функций, [math]g \in A[/math], [math]h[/math] - продолжение [math]g[/math]. Тогда [math]h \in A[/math]. Доказательство: [math]\triangleright[/math] Докажем от противного. Пусть [math]g \in A[/math], [math]h[/math] - продолжение [math]g[/math], [math]h \notin A[/math]. Рассмотрим перечислимое и неразрешимое множество [math]K[/math] и следующую программу: [math]V(n, x) = \begin{cases} h(x)\text{, if $n \in K$;}\\ g(x)\text{, else.} \end{cases}[/math] [math]V[/math] - вычислимая (можно параллельно запустить [math]g(x)[/math] и проверку, принадлежит ли [math]n[/math] множеству [math]K[/math] (просто перечисляя это множество); если [math]g(x)[/math] успешно выполнится, то вернуть её результат). Пусть [math]p(x)=V(n, x)[/math]. Тогда программа, которая запускает параллельно проверку (1), принадлежит ли [math]n[/math] множеству [math]K[/math] (просто перечисляя это множество) и проверку (2), принадлежит ли [math]p[/math] множеству [math]A[/math], является разрешающей программой для множества [math]K[/math], потому что: если [math]n \in K[/math], то проверка (1) завершится, а проверка (2) зависнет (так как [math]p[/math] ведёт себя как [math]h[/math], которая не содержится в [math]A[/math]); пусть в этом случае разрешающая программа для [math]K[/math] возвращает 1; если [math]n \notin K[/math], то проверка (1) зависнет, а проверка (2) завершится (так как [math]p[/math] ведёт себя как [math]g[/math], которая содержится в [math]A[/math]); пусть в этом случае разрешающая программа для [math]K[/math] возвращает 0. Противоречие, так как брали неразрешимое [math]K[/math]. [math]\triangleleft[/math] Лемма: Если [math]A[/math] - перечислимое свойство функций, [math]g \in A[/math], то [math]\exists h[/math], такое что [math]|Dom(h)| \lt +\infty[/math], [math]g[/math] - продолжение [math]h[/math], [math]h \in A[/math]. Доказательство: [math]\triangleright[/math] Докажем от противного. Пусть [math]\not\exists h[/math], удоволетворяющая условию леммы. Рассмотрим перечислимое и неразрешимое множество [math]K[/math] и следующую программу: [math]V(n, x) = \begin{cases} g(x)\text{, if (1);}\\ \perp\text{, else;} \end{cases}[/math] где условие [math](1)[/math] следующее: через [math]x[/math] шагов перечисления [math]K[/math] число [math]n[/math] не появилось. Тогда программа, которая запускает параллельно проверку (1), принадлежит ли [math]n[/math] множеству [math]K[/math] (просто перечисляя это множество) и проверку (2), принадлежит ли [math]V(n, x)[/math] множеству [math]A[/math], является разрешающей программой для множества [math]K[/math], потому что: если [math]n \notin K[/math], то [math]V(n, x) \equiv g(x)[/math] для [math]\forall n[/math], поэтому проверка (2) завершится. Проверка (1) зависнет. Пусть в этом случае разрешающая программа для [math]K[/math] возвращает 0; если [math]n \in K[/math], то завершится проверка (1). Также, в этом случае [math]|Dom(V(n, x))| \lt +\infty[/math], так как [math]V(n, x) = g(x)[/math] при [math]x = 0\ldots t-1[/math] для какого-то [math]t[/math]. [math]g[/math] является продолжением [math]V(n, x)[/math]. По предположению от противного [math]V(n, x) \notin A[/math] [math]\Rightarrow[/math] проверка (2) зависнет. Пусть в этом случае разрешающая программа для [math]K[/math] возвращает 1. Противоречие, так как брали неразрешимое [math]K[/math]. [math]\triangleleft[/math] Вернёмся к доказательству теоремы. Функции с конечной областью определения записываются так: [math]f(x):[/math] if [math]x = x_1[/math] return [math]y_1[/math] [math]\cdots[/math] if [math]x = x_n[/math] return [math]y_n[/math] [math]\perp[/math] Такие функции перечислимы. Значит такие функции, удоволетворяющие [math]A[/math], тоже перечислимы. [math]A_{\Gamma} \subseteq A[/math] по первой вспомогательной лемме. [math]A \subseteq A_{\Gamma}[/math] по второй вспомогательной лемме. Значит [math]A = A_{\Gamma}[/math].

[math]\triangleleft[/math]