El problema de la parada (también llamado problema del halting o problema de detención/interrupción) es un problema fundamental de la informática teórica. Consiste en decidir, dado un programa P y una entrada I, si P finalizará (se detendrá) cuando se ejecute con la entrada I, o si por el contrario ejecutará para siempre.

De forma informal: ¿existe un programa que pueda tomar cualquier otro programa y su entrada y garantizar decir siempre correctamente “se detiene” o “no se detiene”? La respuesta es no: no existe un algoritmo general que resuelva este problema para todos los programas. A continuación se expone una demostración accesible por contradicción (la idea original de Alan Turing, 1936) y se explican sus consecuencias.

Ejemplos simples

Para entender la diferencia entre detenerse y ejecutarse para siempre, fíjate en estos dos fragmentos:

 while True:     continue  # bucle eterno  while False:     continue  # no se ejecuta nunca; el programa continúa inmediatamente

El primer programa nunca termina; el segundo termina rápidamente porque la condición es siempre falsa y el bucle no se ejecuta.

Esquema de la prueba por contradicción

Supongamos, por contradicción, que existe un programa hipotético P que decide si un programa F con entrada I se ejecuta para siempre. Para ser concretos, imaginemos que P(F, I) devuelve True si F(I) se ejecuta para siempre y False si F(I) termina.

Con P construimos dos programas auxiliares:

 def Q(F):     return P(F, F)

Q pregunta a P si el programa F, cuando se ejecuta con una copia de sí mismo como entrada, se ejecutaría para siempre.

 def R(F):     if Q(F):         return   # terminar     else:         while True:             continue  # bucle para siempre

R recibe un programa F y actúa así: si Q(F) dice que F(F) se ejecuta para siempre, entonces R(F) termina; si Q(F) dice que F(F) no se ejecuta para siempre (es decir, termina), entonces R(F) entra en un bucle infinito.

Ahora pregúntate qué sucede cuando ejecutamos R con una copia de sí mismo, es decir, consideremos R(R). Hay sólo dos posibilidades, y ambas conducen a contradicción:

  • Si R(R) no se ejecuta para siempre (es decir, termina), entonces, por la definición de R, Q(R) tuvo que ser True. Pero Q(R) = P(R,R) = True significa que R(R) se ejecuta para siempre. Contradicción.
  • Si R(R) se ejecuta para siempre, entonces, por la definición de R, Q(R) tuvo que ser False. Pero Q(R) = False significa que R(R) no se ejecuta para siempre. También contradicción.

Ambas opciones son imposibles, por tanto la suposición inicial —que existe un programa P que decide correctamente para cualquier programa F e input I si F(I) se ejecuta para siempre— es falsa. Con esto queda demostrado que el problema de la parada es indecidible: no existe un algoritmo general que lo resuelva para todos los programas.

Observaciones formales y matices

  • Indecidible vs. semi-decidible: aunque no hay un decidor total del problema de la parada, hay un procedimiento semidecidible (recursivamente enumerable): podemos simular la ejecución de F(I) paso a paso; si F(I) termina, la simulación lo detectará algún momento y podremos responder “se detiene”. Sin embargo, si F(I) no termina, la simulación tampoco terminará y no obtendremos una respuesta “no se detiene”. Por eso se dice que el conjunto de pares (F,I) que terminan es enumerable pero no decidible.
  • Forma formal: Turing demostró esto usando máquinas de Turing y una técnica de autorreferencia/diagonalización; la prueba mostrada arriba es una versión intuitiva de ese argumento.
  • Variantes: La forma concreta del autocontrato (cómo definimos Q y R) puede cambiar —por ejemplo, P podría devolver True si el programa termina—, pero el argumento por contradicción funciona igual, sólo hay que adaptar las condiciones.

Consecuencias e implicaciones

  • Muchos problemas naturales sobre programas son indecidibles. A partir del problema de la parada se obtiene, por reducción, que otras propiedades (por ejemplo, si un programa imprime un símbolo concreto en algún punto, o si dos programas son equivalentes en todo input) no son decidibles en general. Rice's theorem formaliza y amplía este tipo de resultados.
  • En la práctica implica límites para el análisis automático: no existe una herramienta que, para cualquier programa arbitrario, pueda garantizar decidir todas las propiedades no triviales del comportamiento (como “¿puede este programa alcanzar este punto de código?”) en tiempo finito y correcto para todos los programas.
  • Aun así, sí existen muchas técnicas útiles en práctica: análisis estático conservador (que da respuestas seguras pero puede ser inconcluyente), verificación con restricciones (por ejemplo, sobre programas simples o acotados), y heurísticas que funcionan bien en la mayoría de los casos reales.

Breve nota histórica

La demostración original del resultado fue dada por Alan Turing en 1936, en el contexto de las máquinas de Turing, y es uno de los pilares de la teoría de la computabilidad. Junto con trabajos de Church, Gödel y otros, estableció límites fundamentales sobre lo que es computable.

Resumen

El problema de la parada pregunta si existe un algoritmo que pueda decidir, para cualquier programa y entrada, si el programa terminará o ejecutará indefinidamente. La prueba por contradicción basada en autorreferencia muestra que tal algoritmo no puede existir: el problema es indecidible. Esto no invalida todas las técnicas de análisis y verificación, pero sí pone un límite teórico que condiciona lo que es posible lograr de forma automática y completa.