[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]); пусть в этом случае разрешающая программа возвращает 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]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] не появилось.
Если [math]n \notin K[/math], то [math]V(n, x) = g(x)[/math].
Если [math]n \in K[/math], то [math]V(n, x) = g(x)[/math] при [math]x = 0\ldots t-1[/math] для какого-то [math]t[/math].
Запустим параллельно проверку, принадлежит ли [math]n[/math] множеству [math]K[/math] и проверку, принадлежит ли [math]V(n, x)[/math] множеству [math]A[/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} \subset A[/math] по первой вспомогательной лемме.
[math]A \subset A_{\Gamma}[/math] по второй вспомогательной лемме.
Значит [math]A = A_{\Gamma}[/math]. Теорема доказана. |