El problema de la parada

Sería utilísimo: una herramienta que lea tu código y avise si ese ciclo termina o se cuelga para siempre. No es que todavía no se haya construido, ni que sea muy difícil. Se puede demostrar que no puede existir, y la demostración es corta.

Qué se está pidiendo, exactamente

El problema es este: dado un programa $P$ y una entrada $x$, decidir si $P$ ejecutado sobre $x$ termina. Se pide un procedimiento que siempre responda, y que siempre acierte.

Conviene notar por qué no alcanza con ejecutarlo y ver qué pasa: si termina, se sabe; pero si todavía no terminó, no hay forma de distinguir “va a terminar en un rato” de “no termina nunca”. Esa asimetría es la pista de que el problema es reconocible pero no decidible.

La demostración, por contradicción

La demostración es por contradicción. Supongamos que existe termina(P, x), que devuelve verdadero o falso y siempre acierta. Con ella construimos un programa nuevo:

diagonal(P):
    si termina(P, P):
        ciclar para siempre
    si no:
        terminar

Ahora la pregunta: ¿qué hace diagonal(diagonal)? Si termina dice que sí, el programa cicla para siempre, así que no termina. Si dice que no, termina de inmediato. En los dos casos termina se equivoca, y había supuesto que nunca lo hacía. Por lo tanto no existe.

La diagonalización, el mismo truco de Cantor

El truco es el mismo que usó Cantor para probar que los reales son incontables y Gödel para sus teoremas de incompletitud: la diagonalización. Se construye un objeto que difiere de cada elemento de una lista supuestamente completa, justo en el lugar que le corresponde.

Acá ese objeto es un programa que hace exactamente lo contrario de lo que se predice sobre él. La autorreferencia no es un juego de palabras: es posible porque un programa se puede pasar como dato a otro, que es la propiedad de la máquina universal.

Lo que el resultado no dice

Vale la pena ser preciso sobre el alcance, porque se exagera seguido. El resultado no dice que no se pueda analizar ningún programa: para muchísimos casos concretos se puede probar perfectamente bien si terminan.

Lo que no existe es el procedimiento general y siempre correcto. Un analizador puede responder “termina”, “no termina” o “no sé”, y ser utilísimo. Toda la industria del análisis estático vive en ese margen: los verificadores aceptan responder “no sé”, o restringen el lenguaje a construcciones donde la terminación sí es decidible.

Todo lo que se cae con él

Las consecuencias se propagan. Por reducción, se prueba que tampoco es decidible si dos programas calculan lo mismo, si un programa alguna vez escribe en cierta variable, o si un fragmento de código es alcanzable.

El teorema de Rice generaliza el golpe: toda propiedad no trivial del comportamiento de un programa es indecidible. No de su texto —contar líneas es decidible— sino de lo que computa. Un detector perfecto de virus, entendido como “este programa hace algo malicioso”, cae bajo esa prohibición.

Las tres formas de convivir con esto

Con eso se convive de tres formas. Aproximar: aceptar falsos positivos, como hace un type checker que rechaza programas correctos pero que no puede verificar. Restringir: usar lenguajes donde toda función termina por construcción, como los asistentes de demostración. O acotar: ejecutar con un límite de pasos y responder “no terminó en el presupuesto”.

Las tres son formas de cambiar la pregunta por una decidible. Ninguna resuelve la original, porque la original no tiene solución.

Lo que sí se puede hacer

Cierre

No hay decisor general de terminación, y la prueba es construir el programa que contradice cualquier decisor propuesto. El resultado no impide analizar programas concretos: impide el método universal, y por eso las herramientas reales aproximan, restringen o acotan.