[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 (0);}\\
\perp\text{, else;}
\end{cases}[/math]
где условие [math](0)[/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]. |