¿Es el problema de detención decidible para programas puros en una computadora ideal?

Es bastante simple entender por qué el problema de detención es indecidible para los programas impuros (es decir, aquellos que tienen E / S y / o estados dependientes del estado global de la máquina); pero intuitivamente, parece que la interrupción de un programa puro en una computadora ideal sería decidible, por ejemplo, mediante análisis estático.

¿Es éste de hecho el caso? Si no, ¿cuáles son algunos contraejemplos o documentos que refutan esta afirmación?

Aquí hay una prueba de indecidibilidad por reducción del problema de detención.

Reducción: Dada una máquina y una entrada x , construya una nueva máquina Turing H que no lea ninguna entrada, pero escriba M y x en la cinta y simule M en x hasta que M se detenga.$M$$x$$H$$M$$x$$M$$x$$M$

El comportamiento de esta nueva máquina es independiente de la cinta de entrada, por lo que es una máquina Turing pura en la que solo es aplicable el análisis estático. Si el análisis estático fuera suficiente, podría mostrar si H se detiene, lo que mostraría si M se detiene en x , lo que resolvería el problema de detención para máquinas impuras, lo que sabemos es indecidible, y por lo tanto su problema también es indecidible.$H$$H$$M$$x$

No, no lo es, y además no depende de E / S.

Contraejemplo simple: escriba un programa para encontrar un número impar perfecto (este es un problema abierto: aún no sabemos si existe): no toma ninguna entrada y no realiza ninguna tarea impura ; puede detenerse cuando encuentra uno, o puede funcionar infinitamente (en el caso de que tal número no exista). Ahora bien, si el análisis estático fuera lo suficientemente poderoso como para determinar el caso de detención, se usaría para responder esto (y muchas más preguntas) donde detener significaría la existencia positiva de dicho número y no detenerlo significaría que no existe dicho número, pero desafortunadamente el análisis estático No es tan poderoso.

La prueba clásica por diagonalización es una máquina pura , no solo es una máquina de Turing pura, sino que no se basa en "problemas abiertos".

Por ejemplo, una máquina de Turing que ejecuta la Conjetura de Collatz tiene un estado de detención desconocido, pero eso se basa en nuestra ignorancia sobre la Conjetura de Collatz, un día podríamos probar que Collatz tenía razón y luego podríamos decidir el estado de Detención de la conjetura. (O para algunas entradas no se detiene, o siempre se detiene).

Entonces, la Conjetura de Collatz ya podría responder a su pregunta (al menos temporalmente), pero se basa en algo que no sabemos . En cambio, la prueba clásica es un problema resuelto: ya sabemos que es indecidible .

Solo para el registro, la prueba estándar de la indecidibilidad del problema de detención se basa en la misma idea que quines: que es posible escribir un programa cuyo término se evalúe en el código fuente de todo el programa. Luego, si hubiera una función haltsque, dado el código fuente de un programa, devuelva True si ese programa se detuvo en todas las entradas y False, de lo contrario, este sería un programa legal:

prog() = if halts "prog" then prog() else ()

donde "prog"habría alguna expresión que evaluara el código fuente para prog; sin embargo, puede ver rápidamente que se progdetiene (para todas las entradas) si no se detiene, lo cual es una contradicción. Nada en esta prueba se basa en E / S de ninguna manera (¿necesita E / S para escribir una quine?).

Por cierto, es posible que desee buscar "E / S basadas en cuadros de diálogo" para obtener más evidencia de que la E / S es completamente irrelevante para su problema (básicamente, los programas que hacen E / S pueden reducirse a programas que toman datos como argumentos explícitos (explícitos) y resultados de retorno como resultados adicionales (explícitos) en un lenguaje vago). Desafortunadamente, no puedo encontrar una página razonable, imparcial (o pro-diálogo) en la web en este momento.