Como agujeros negros en informática. Solo podemos saber que existen, pero cuando tengamos uno de ellos, nunca sabremos que es uno de ellos.
halting-problem
correctness-proof
Otakar Molnár López
fuente
fuente
if T is true then halt else loop forever
if T is true
?For each string S in the (countable) universe of possible strings: If S is a syntactically valid proof of T, halt.
Respuestas:
De hecho, hay programas como este. Para probar esto, supongamos lo contrario que por cada máquina que no se detiene, hay una prueba de que no se detiene.
Estas pruebas son cadenas de longitud finita, por lo que podemos enumerar todas las pruebas de longitud menor que para algunos enteros s .s s
Luego podemos usar esto para resolver el problema de detención de la siguiente manera: Dada una máquina Turing y una entrada x , usamos el siguiente algoritmo:METRO X
Si detiene en la entrada x , entonces se detiene en un número finito de pasos s , por lo que nuestro algoritmo termina.METRO X s
Si no se detiene en la entrada x , entonces, por nuestra suposición, hay algunas pruebas de longitud s donde hay una prueba de que M no se detiene. Entonces, en este caso, nuestro algoritmo siempre termina.METRO X s METRO
Por lo tanto, tenemos un algoritmo para decidir el problema de detención que siempre termina. Pero sabemos que esto no puede existir, por lo que nuestra suposición de que siempre hay una prueba de no detenerse debe ser falsa.
fuente
Para un ejemplo algo más concreto, supongamos que la teoría que estamos utilizando para nuestras pruebas tiene las siguientes características (bastante razonables, IMO):
Con esos supuestos, el siguiente programa nunca se detendrá, pero no se puede probar (dentro del alcance de la teoría que estamos usando) que no se detenga:
El detalle clave aquí es la primera suposición anterior, a saber, que la teoría que estamos utilizando para nuestras pruebas es consistente. Obviamente, debemos asumir esto, para que nuestras pruebas valgan algo, pero el segundo teorema de incompletitud de Gödel dice que, para cualquier teoría razonablemente expresiva y efectivamente axiomatizada, no podemos probar esto (excepto posiblemente en alguna otra teoría, cuya consistencia entonces Necesito asumir, etc. etc.).
fuente