¿Decidir si una máquina de Turing * probablemente se ejecuta para siempre es equivalente al problema de detención?

Question

Asumir esta pregunta que la teoría de conjuntos ZF es el sonido.

Ahora pensemos en el lenguaje "PROVELOOP", que consiste en todas las descripciones de las máquinas de Turing M, para lo cual existe una ZF de prueba de que M se ejecuta siempre en una entrada en blanco.

Es claro que PROVELOOP es recursivamente-enumerable, y por lo tanto reducible a detener el problema. También puedo probar que PROVELOOP es indecidible (detalles más abajo). Pero yo no puedo ver cómo demostrar que PROVELOOP es Turing-equivalente a detener problema! (Esto es en contraste con, digamos, el conjunto de todas las descripciones de las máquinas de Turing que seguramente detener, que es la misma cosa como el conjunto de todas las descripciones de las máquinas de Turing que hacer parar!)

Estoy adivinando que hay una reducción de DETENER que no he pensado, aunque sería interesante si PROVELOOP iban a tener su grado medio como la Friedberg-Muchnik idiomas. En cualquier caso, sea cual fuere la respuesta, yo asumo que debe ser conocido! Por lo tanto esta pregunta.

---

La prueba de que PROVELOOP es indecidible. Considere el siguiente problema, que voy a llamar "Consistente Adivinar" (CG). Usted está dada como entrada una descripción de una máquina de Turing M. Si M acepta dada una entrada en blanco, entonces usted necesita para aceptar, mientras que si M rechaza debe rechazar. Si M funciona para siempre, entonces usted puede aceptar o rechazar, pero en cualquier caso, usted tiene que parar.

Mediante la adaptación de la undecidability prueba para DETENER, se puede mostrar fácilmente que CG es indecidible también. Es decir, supongamos que P resuelve CG. Vamos Q tome como entrada una máquina de Turing descripción $\langle M \rangle$, y resolver el CG para la máquina de $M(\langle M \rangle)$ llamando a P como una subrutina. A continuación, $Q(\langle Q \rangle)$ (es decir, Q se ejecutan en su propia descripción) debe detener, aceptar si se rechaza, y rechazar, si se acepta.

Vamos a probar ahora que CG es Turing-reducible a PROVELOOP. Dada una descripción de una máquina de Turing M para los que queremos resolver CG, simplemente cree una nueva máquina de Turing M', que hace lo mismo que M, excepto que si M acepta, entonces M' entra en un bucle infinito en su lugar. Entonces, si M acepta, entonces M' bucles, y además hay una ZF de prueba que M' bucles. Por otro lado, si M rechaza, entonces M' también se rechaza, y no hay ZF prueba de que M' bucles (por la suposición de que ZF es el sonido). Si M bucles, entonces no podría o no ser una ZF de prueba que M' bucles; pero, en cualquier caso, llamando PROVELOOP en M', podemos separar el caso de que M acepta en el caso que M rechaza, y, por tanto, resolver CG en M. por Lo $CG \le_{T} PROVELOOP$, y PROVELOOP es indecidible así.

Una nota más. En los comentarios de este blog, Andy Drucker suministra una prueba de que el CG es no equivalente a DETENER, sino que tiene Friedberg-Muchnik-como condición de intermediario. Así, la situación es

$0 \lt_{T} CG \le_{T} PROVELOOP \le_{T} HALT$

con al menos una de las dos últimas desigualdades estrictas. De nuevo, estoy seguro de que todo esto está implícito en algunos computabilidad de papel a partir de la década de 1960 o algo, pero no sé donde encontrarlo.

Answer 1

La primera cosa a notar es que si ZF es consistente, entonces es consistente con ZFC que lo que ustedes llaman ProveLoop es en realidad decidable. El la razón es que si ZF es consistente, entonces, por la imperfección teorema, es consistente con ZFC que $\neg$Con(ZF), en cuyo caso todo lo que es comprobable en ZF, en cuyo caso, cada programa está en ProveLoop.

Así, en la prueba de que ProveLoop es indecidible, lo que uno necesita para hacer una suposición adicional acerca de la fiabilidad de las pruebas en ZF para evitar este problema con el teorema de la incompletitud.

Mientras tanto, en virtud de tal consistencia de la asunción, ProveLoop es, de hecho, equivalente a detener el problema.

Teorema. Asumir Con(ZF). Luego ProveLoop es Turing equivalente a Detener el problema.

Prueba. En virtud de la Con(ZF) asunción, de ello se sigue que cuando ZF se demuestra que un programa no se detiene, entonces realmente no parar, ya que si lo hizo detener, este hecho también sería demostrable, contrario a la coherencia.

Claramente ProveLoop es c.e. y por lo tanto fácil de reducir a la detener el problema, como usted ha señalado. Por el contrario, vamos a reducir el detener problema para ProveLoop. Dado cualquier programa $p$, queremos decidir si $p$ se detiene en una cinta en blanco, con un oracle para ProveLoop.

Definir una función computable $f$, por lo que el $f(q)$ es el programa de tal manera que, en el trivial de entrada, si $p$ se detiene en la cinta en blanco, entonces $f(q)$ salta de inmediato un bucle infinito, y otra cosa, mientras se espera para $p$ a detener, el programa de $f(q)$ se detiene sólo en caso de encontrar alguna prueba de que $q$ no se puede detener. Por el teorema de recursión, hay un programa que se $r$ tal que $r$ y $f(r)$ calcular la misma función, y se puede encontrar esta $r$ efectivamente. Además, por medio de la $r$ a partir de la prueba del teorema de recursión, también podemos suponer que en ZF se demuestra que $r$ e $f(r)$ calcular la misma función. Observe que no puede ser nunca que $r$ se detiene en la cuenta de encontrar una prueba de que $r$ no se puede detener, por nuestra suposición de que asegura la exactitud de las pruebas de no detener, y por lo que definitivamente $r$ no se puede detener en cualquier caso. Mientras tanto, si $p$ se detiene, a continuación, $r$ no se puede detener, pero por un motivo trivial que se puede demostrar en ZF, es decir, el hecho de que $p$ detenido; y lo contrario, cuando se $p$ no se detiene, a continuación, $r$ va a correr para siempre, pero este hecho no va a ser comprobable (por si fuera demostrable, a continuación, $r$ sería detener, contrario a consecuencia de nuestra suposición de que tales pruebas son fiables). Así que lo que tenemos es exactamente una reducción de la detención problema para ProveLoop, como se desee. QED

Answer 2

Este es un complemento a las otras respuestas, dando algunos "nivel superior" razones por las $PROVELOOP$ debe ser completa.

Para un recursivamente enumerable set $A$, los siguientes son equivalentes:

1. $A$ es Turing completo (es decir,$A \equiv_T 0'$).
2. $A$ calcula un punto fijo libre (FPF) función (es decir, un total de función $f$ tal que $\varphi_e \neq \varphi_{f(e)}$ para todos los índices de $e$).
3. $A$ calcula un diaginally no recursivo (DNR) función (es decir, un total de función $g$ que si $\varphi_e(e)$ se detiene, a continuación,$\varphi_e(e) \neq g(e)$).

La equivalencia de (1) y (2) es el Arslanov Integridad Criterio y la equivalencia con la (3) se observó por Jockusch [Grados de funciones sin puntos fijos, en la Lógica, metodología y filosofía de la ciencia, VIII (Moscú, 1987), 191 a 201]. Las condiciones (2) y (3) son muy útiles las pruebas para la integridad de la recursivamente enumerable conjuntos.

Una variación de Scott $CG$ argumento muestra que el $PROVELOOP$ calcula la separación de la función de los distintos recursivamente enumerable conjuntos $$A_0 = \lbrace e : \varphi_e(e){\downarrow} = 0\rbrace, \qquad A_1 = \lbrace e : \varphi_e(e){\downarrow} = 1\rbrace.$$ That is $PROVELOOP$ computes a $\lbrace0,1\rbrace$-valued function $h$ such that $h(e) = 0$ if $e \en A_0$ and $h(e)= 1$ if $e \en A_1$. Then $g(e) = 1-h(e)$ is easily seen to be DNR. Since $g \leq_T h \leq_T PROVELOOP$ and $PROVELOOP$ is recursively enumerable, it follows that $PROVELOOP$ es completa.

Answer 3

Es tarde, así que yo podría estar cometiendo un error, o varios, pero creo que esto funciona:

Asumiendo $ZF$ es consistente (no creo que la solidez necesaria para esta parte), te voy a mostrar PROVELOOP puede calcular el conjunto de $\Pi^0_1$ teoremas de $ZF$.

Dado un $\Pi^0_1$ frase en el lenguaje de la teoría de conjuntos $\varphi$, construir en la forma habitual de una máquina $M$ que se ejecuta hasta que encuentre un contraejemplo a $\varphi$; $M$ seguramente bucles iff $ZF$ demuestra $\varphi$. En una dirección, si $ZF$ demuestra $\varphi$,, a continuación, $M$ tiene un bucle para siempre, ya $ZF$ es consistente; y lo que es más, mientras la construcción de $M$ era lo suficientemente transparente, $ZF$ puede demostrar esto, por lo $\ulcorner M\urcorner\in PROVELOOP$. En la otra dirección, si $ZF$ demuestra $\neg\varphi$,, a continuación, $ZF$ demuestra que $M$ se detiene; si $ZF$ es consistente, entonces eso quiere decir $ZF$ no prueba que $M$ no se puede detener, por lo $\ulcorner M\urcorner\not\in PROVELOOP$.

Ahora, todo lo que necesitas hacer es mostrar que el conjunto de $\Pi^0_1$ teoremas de $ZF$ es equivalente a detener problema, $H$. Por alguna razón, estoy teniendo problemas para hacer esto en el momento, pero creo que esto es sencillo (¿alguien puede llenar este vacío?). Creo que es en este segundo paso, que la Solidez (o $\Sigma_1$-Solidez) será necesario.