Problema de detención: un problema que me está molestando

Que yo sepa, el problema de detención pregunta si existe un programa que decida si un programa que se está probando, dados algunos datos de entrada (no importa qué programa sea, o qué datos de entrada proporcionamos) terminará o no. La respuesta a este problema es 'no'. En otras palabras, no existe un programa 'único' que pueda verificarlo para todos los pares posibles (algún algoritmo, algunos datos de entrada).

Pero eso no significa que no podamos decidir si un programa en particular X terminará o no.

Todavía no puedo comentar otras respuestas, pero una de ellas me llamó la atención:

En términos prácticos, es importante porque le permite decirles a sus jefes ignorantes que "lo que están pidiendo es matemáticamente imposible".

¿Quizás puedas decirme qué quería decir esa persona? En mi caso, mi jefe ignorante puede pedirme que verifique (en realidad, pruebe o refute) si mi programa (que es un programa en particular) terminará o no. Y, por supuesto, hay pares (algoritmo, datos de entrada) que se puede probar que terminan (o nunca terminan).

La pregunta es: ¿puedo probarlo para cada par (programa, datos de entrada) por separado? Incluso si la respuesta es sí, entonces hay un problema: puede haber infinitos 'datos de entrada'. Por lo tanto, es bastante natural preguntar: ¿puedo demostrar, para cada algoritmo, que este algoritmo terminará (o lo contrario), sin importar qué datos de entrada proporcione?

computability halting-problem user4205580
fuente

Ya sea que nos podemos encontrar todas estas pruebas es una cuestión de lógica, supongo, pero ciertamente hay muchos que no hemos encontrado todavía .

Raphael

El problema de detención se define como un algoritmo específico que puede determinar si algún programa se detendrá o no. Verificar un programa específico (o incluso varios programas específicos) con diferentes algoritmos si pueden detenerse o no es factible (el caso general no lo es)

Nikos M.

Respuestas:

No, no puede probar esto para cada algoritmo (máquina de Turing). Esto se convierte en una pregunta sobre la naturaleza de las pruebas en lugar de una pregunta sobre el cálculo.

Considere la siguiente máquina de Turing : verifique si existe una prueba para la declaración detiene, de longitud(para una explicación sobre la auto referencia, vea el teorema de recursión de Klenee). Si se encuentra dicha prueba, entre en un bucle infinito (de lo contrario, deténgase). $M(x)$ $\forall x \hspace{1mm} M(x)$ $\le |x|$

Claramente, no puede probar que detenga para todo , ya que si puede encontrar una prueba de longitud , no se detendrá para todas las entradas de tamaño . Además, no puede probar que no se detenga para algunas , ya que esto significaría que existe una prueba para detener en todas las entradas (contradicción). La situación aquí es que si nuestro sistema de axiomas es consistente, entonces detiene para todas las , pero no puede probarlo (lo que significa que puede probar en su teoría que si es consistente entonces $M(x)$ $x$ $p$ $\ge p$ $M(x)$ $x$ $M$ $M(x)$ $x$ $T$ $T$ $\forall x \hspace{1mm} M(x)$ se detiene, pero no puede demostrar que se detiene sin esta suposición, a menos que su sistema sea inconsistente).

Ariel
fuente

Esta es la respuesta a '¿puedo probar, para cada algoritmo, que este algoritmo terminará (o lo contrario), sin importar qué datos de entrada proporcione?' - solo por asegurar.

user4205580

Si. Necesito más personajes

Ariel

También puede interesarle los resultados incompletos de Godel : básicamente, en cualquier sistema lógico que sea lo suficientemente poderoso como para hablar de aritmética, hay afirmaciones que son verdaderas que no se pueden probar.

jmite

M

$M$ - máquina de Turing,

x

$x$ - su entrada. Luego lo ejecutamos con, digamos,

x = 2

$x=2$ . El programa se traduce como: "verificar si existe una prueba de la declaración: para todos

2

$2$ M (2) paradas, de longitud

\leq 2

$\le 2$ ... "No tiene mucho sentido decirlo para todos

2

$2$ . O tal vez no es la forma en que debería mirarlo.

user4205580

La variable cuantificada es nueva, piénselo como

\forall y M (y)

$\forall y M(y)$ se detiene

x

$x$ (la entrada) solo aparece como el límite en la longitud de la prueba.

Ariel

Para un programa específico, seguro que puedo demostrar que el programa se detendrá en todas las entradas: mi programa tiene "alto" como su primera instrucción.

Otro ejemplo: puedo tener un programa específico que es un simulador de máquina de Turing (es decir, una máquina de Turing universal). Interpreta su entrada como una descripción de una máquina de Turing, y el simulador simula la máquina que se ejecuta en una cinta en blanco. Por lo tanto, el simulador se detendrá si la máquina que se está ingresando se detiene y se ejecutará para siempre si la máquina que se ingresa se ejecuta para siempre. (Si la entrada no está en el formato correcto para describir una máquina Turing, el simulador se detiene).

Sabemos que es imposible decidir si una máquina arbitraria de Turing se detiene cuando se inicia en una cinta en blanco. Entonces, para mi máquina simuladora específica, no hay un algoritmo para decidir qué hace en una entrada arbitraria.

No sé si estos dos ejemplos ayudan.

Seguramente en muchos dominios problemáticos es razonable poder demostrar que los programas específicos terminan. Si mi programa multiplica dos matrices, esperaría poder demostrar que no hay forma de que pueda continuar para siempre.

usuario42735
fuente

Al menos puedo aclarar la pregunta hipotética que se supone que hace el jefe imaginario que lleva a esta respuesta:

¿Puede diseñar un programa que tome este otro programa / plantilla / consulta de base de datos / etc. que siempre determina si finaliza / genera una excepción / se queda sin memoria?

El punto de la prueba de imposibilidad es que tal tarea no se puede lograr. Por supuesto, hoy es de conocimiento común que dicha tarea puede aproximarse bastante bien, es decir, es posible proporcionar un algoritmo que determine si un programa generará una excepción, pero a veces las respuestas "podrían generar una excepción" aunque el programa no No lo hagas en la práctica .

Algunos de estos también son más difíciles de hacer en la práctica, por ejemplo, la terminación es más difícil de probar que la ausencia de una excepción de puntero nulo para "programas del mundo real" (pero equivalente en teoría).

cody
fuente