Algoritmo para resolver el "problema de detención" de Turing

23

"Alan Turing demostró en 1936 que no puede existir un algoritmo general para resolver el problema de detención para todos los posibles pares de entrada de programa"

¿Puedo encontrar un algoritmo general para resolver el problema de detención de algunos posibles pares de entrada de programa?

¿Puedo encontrar un lenguaje de programación (o lenguajes), donde para cada tipo de programa en este lenguaje, pueda decidir si el programa finaliza o se ejecuta para siempre?

computability formal-methods halting-problem software-verification Kaveh
fuente
Pregunta similar: stackoverflow.com/questions/8412741/…
3
CACM tuvo un artículo muy interesante en mayo: Prueba de
finalización del
3
"un algoritmo general [...] para algunos posibles pares de entrada de programa", eso está cerca de ser contradictorio. ¿Supongo que quieres restringirte a una subclase infinita de todos los programas?
Raphael

Respuestas:

25

¿Puedo encontrar un algoritmo general para resolver el problema de detención de algunos posibles pares de entrada de programa?

Si seguro. Por ejemplo, podría escribir un algoritmo que devuelva "Sí, termina" para cualquier programa que no contenga ni bucles ni recursividad y "No, no termina" para cualquier programa que contenga un while(true)bucle que definitivamente se alcanzará y no contiene una declaración de ruptura, y "No sé" para todo lo demás.

¿Puedo encontrar un lenguaje de programación (o lenguajes), donde para cada tipo de programa en este lenguaje, pueda decidir si el programa finaliza o se ejecuta para siempre?

No si ese idioma es Turing completo, no.

Sin embargo, hay idiomas completos que no son de Turing, como por ejemplo Coq , Agda o Microsoft Dafny, para los cuales el problema de detención es decidible (y de hecho lo deciden sus respectivos sistemas de tipos, lo que los convierte en idiomas totales (es decir, un programa que podría no finalizar compilar)).

sepp2k
fuente
1
La clase de funciones primitivas-recursivas es un conocido "lenguaje de programación" para el cual el problema de detención es trivialmente decidible.
Raphael
Existen varios lenguajes de " programación funcional total " en los que todos los programas están terminando de manera demostrable.
Anderson Green
3

Creo que todas las respuestas aquí completamente y completamente pierden el punto. La respuesta a la pregunta es: suponiendo que el programa esté destinado a detenerse, entonces sí, será mejor que pueda mostrar que se detiene. Si no puede mostrar que se detiene fácilmente, entonces el Control de calidad debe considerar que el programa está muy mal escrito y rechazado como tal.

Si realmente puede escribir un algoritmo de máquina adecuado depende del lenguaje de programación de entrada y de lo ambicioso que sea. Es un objetivo de diseño razonable para un lenguaje de programación hacer posible probar la terminación fácilmente.

Si el lenguaje es C ++, es probable que no pueda escribir la herramienta, de hecho, es poco probable que pueda ejecutar el analizador, y mucho menos probar la terminación. Para un lenguaje mejor estructurado, debería poder generar una prueba, o al menos hacerlo con ciertos supuestos: en el último caso, la herramienta debería generar estos supuestos. Un enfoque similar sería incluir aserciones de terminación en el lenguaje y usarlas en situaciones complejas donde la herramienta confiaría en las aserciones.

La conclusión es que nadie parece entender que la prueba de que un programa se detenga es realmente posible porque los (buenos) programadores que intentan escribir tales programas de detención siempre lo hacen intencionalmente y con una imagen mental de por qué terminan y actúan correctamente: dicho código es deliberadamente escrito para que quede claro que se detienen y son correctos y si un algoritmo razonable no puede probar esto, posiblemente con algunos consejos, entonces el programa debe ser rechazado.

El punto: los programadores no escriben programas arbitrarios, por lo que la tesis del teorema de detención no se cumple y la conclusión no se aplica.

Yttrill
fuente
44
Creo que fuiste tú quien perdió el punto por completo. El primer párrafo de su respuesta no se aplica a la pregunta porque se trata de algoritmos, no de lo que un humano puede o no puede probar. El resto de la respuesta responde el primer párrafo de la pregunta, es decir, si un algoritmo podría probar la terminación de algunos programas. Todas las respuestas anteriores ya dijeron "sí" a esa.
sepp2k
3
Su afirmación de que es posible escribir un algoritmo que pueda probar la terminación de cada programa bien escrito en un lenguaje Turing-complete suficientemente simple es completamente falso. Por cada algoritmo posible que intente probar la terminación, hay problemas en los que no se puede demostrar que ese algoritmo detenga todos los programas que resuelvan ese problema. Entonces, a menos que esté diciendo que cada programa que resuelve ese problema está mal escrito por definición (lo cual sería absurdo), eso refuta su punto.
sepp2k
1
@Sam Si alguien me pregunta si se detiene algún código, miraré el código e intentaré resolverlo. Pero no soy un algoritmo. Y sí, es posible escribir un algoritmo que pueda verificar si un programa se detiene para muchos programas. Pero eso no es lo que dijo Yttrill. Yttrill dijo que es posible para todos los programas bien escritos. Y como dije en mi comentario anterior, eso es simplemente falso a menos que afirmes que ciertos problemas solo pueden resolverse con programas mal escritos (lo que nuevamente sería ridículo).
sepp2k
1
@Sam "me parece sencillo que los programas escritos intencionalmente para detenerse puedan analizarse fácilmente en busca de condiciones de detención". Si ese fuera el caso, ¿por qué no tenemos esas herramientas? No es como si la gente no lo intentara. (Un culpable es la anulación del método: en el momento de la compilación, no se conoce todo el código que se ejecutará).
Rafael
1
@Sam "hay un bucle infinito" es algo difícil de abordar, incluso para el bucle del mundo real. Por supuesto, me enseñaron cómo encontrar invariantes de bucle, pero eso no significa que pueda encontrar uno (fácilmente) en muchos casos. Hasta donde yo sé, adivinar y probar es el estándar de oro en estos días. Una vez más, si no eran algoritmos bastante generales, que sería de esperar que sean incluidos en las principales compilaciones o entornos de desarrollo (que hacen realizar algunas comprobaciones triviales, sintácticas). ¿Puedes dar una referencia a un algoritmo razonablemente fuerte?
Raphael
3

excelente y (prob. involuntariamente profunda) pregunta. De hecho, existen programas de detección de detención que pueden tener éxito en conjuntos limitados de entradas. Es un área activa de investigación. tiene vínculos muy fuertes con las áreas de prueba de teoremas (automatizadas).

sin embargo, la informática no parece tener un término exacto para "programas" que "a veces" tengan éxito. la palabra "algoritmo" generalmente está reservada para programas que siempre se detienen.

el concepto parece ser claramente diferente de los algoritmos probabilísticos donde los teóricos de CS insisten en que haya alguna probabilidad conocida o computable de su éxito.

hay un término semialgoritmos que se usa a veces, pero aparentemente es un sinónimo de recursivamente enumerable o no computable.

así que para propósitos aquí, llámalos llámelos cuasialgoritmos . El concepto es diferente de decidible vs indecidible.

se podría decir que no se pueden comparar los cuasialgoritmos. pero de hecho parece haber una jerarquía natural (un ordenamiento parcial) de estos cuasialgoritmos. Supongamos que un quasialgorithm puede detectar detención de un conjunto limitado de programas de entrada dicen X . otro B puede detectar detención de un conjunto Y . si X ⊂ Y es decir, X es adecuada subconjunto de Y entonces B es "más potente" que A .AXBYX⊂YXYBA

en CS, esta "jerarquía de cuasi algoritmo" parece estudiarse principalmente solo de manera informal hasta ahora.

aparece en la investigación de castores ocupados [1] y el problema PCP [2]. de hecho, un ataque informático basado en ADN en PCP puede verse como un quasialgoritmo. [3] y se ve en otras áreas ya señaladas, como la demostración de teoremas [4].

[1] Nuevo ataque del milenio al problema del castor ocupado

[2] Problema de correspondencia de Tackling Posts por Zhao (v2?)

[3] Utilizando el ADN para resolver el problema de la correspondencia posterior a los límites de Kari et al.

[4] prueba de terminación del programa por Cook et al, Comm. de la ACM

(así que esta es realmente una pregunta muy profunda que definitivamente merece estar en TCS.SE, en mi opinión ... tal vez alguien pueda volver a preguntarla de tal manera que se ajuste y permanezca)

vzn
fuente
ps como un impresionante ejemplo de cuán poderosos pueden ser los cuasialgoritmos, el ACM señala que la función de ackermanns puede ser detenida por un cuasialgoritmo, pero es más grande que (no computable por) todas las funciones recursivas primitivas.
vzn
1
"la palabra" algoritmo "generalmente se reserva para programas que siempre se detienen". - No estoy seguro de que sea cierto. Hay muchos algoritmos de terminación parcial (especialmente en la verificación) y nunca he oído a nadie que no diga "algoritmo".
Raphael
Hay usos informales del "algoritmo". "Terminar parcialmente" está bien, pero probablemente no es estándar. como se indicó, todavía no parece haber un término estándar. wikipedia define un algoritmo como un método efectivo, es decir, decidible con las siguientes características (1) siempre da alguna respuesta en lugar de dar una respuesta; (2) siempre dé la respuesta correcta y nunca dé una respuesta incorrecta; (3) siempre se completará en un número finito de pasos, en lugar de en un número infinito; (4) trabajar para todos los casos de problemas de la clase.
vzn
y luego en el mismo artículo dice "Una aclaración adicional del término" método efectivo "puede incluir el requisito de que, cuando se presenta un problema externo a la clase para la cual el método es efectivo, el método puede detenerse o repetirse para siempre sin detenerse , pero no debe devolver un resultado como si fuera la respuesta al problema ". es decir, casi se contradice a sí mismo así que claramente, notablemente, existe cierta confusión real sobre el tema clave y la terminología existente no es estricta. tenga en cuenta que la palabra "algoritmo" tiene más de un milenio de antigüedad y ha cambiado sustancialmente ...
vzn
Es cierto: el significado tradicional es probablemente "método efectivo" en la forma en que Wikipedia lo dice (no hay contradicción en la oración que cita; sin embargo, es un poco confuso): las personas no concibieron funciones / algoritmos que no terminaron (por algunas entradas). Creo que esto ha cambiado desde la década de 1950; como dije, hoy la gente claramente llama a un algoritmo de método de terminación parcial "algoritmo".
Raphael
2

Mientras el lenguaje de programación en cuestión sea lo suficientemente complejo (es decir, si está completo en Turing), siempre hay programas en el lenguaje que ningún programa puede terminar.

Dado que todos los lenguajes, excepto los más primitivos, son completos de Turing (solo se necesitan algo como variables y condicionales), en realidad solo puede construir lenguajes de juguete muy pequeños para los que pueda resolver el problema de detención.

Editar: luz de los comentarios, permítanme ser más explícito: cualquier lenguaje que pueda diseñar para el que pueda resolver el problema de detención necesariamente tendrá que ser Turing incompleto. Esto descarta cualquier lenguaje que contenga un conjunto adecuado de ingredientes básicos (por ejemplo, "variables, condicionales y saltos", o como dice @ sepp2k, un bucle genérico "while").

Aparentemente existen varios lenguajes "simples" prácticos como ese (por ejemplo, solucionadores de teoremas como Coq y Agda). Si estos satisfacen su noción de un "lenguaje de programación", puede investigar si satisfacen algún tipo de completitud o si el problema de detención es solucionable para ellos.


fuente
3
"Dado que todos los lenguajes, excepto los más primitivos, son Turing completos (solo se necesitan algo como variables y condicionales)" Eso no es cierto. En primer lugar, al menos necesitaría recurrencia o alguna forma de construcción de bucle (que debería ser tan potente como un bucle while; un simple bucle de conteo no es suficiente). En segundo lugar, no creo que haya mucha gente que llame idiomas como el Coq o el Agda (que son totales y, por lo tanto, no completos), idiomas primitivos o de juguete.
sepp2k
@ sepp2k: Bueno, sí. La aritmética de peano también es bastante útil y no está completa. Una declaración simplificada, supongo. Si el OP está suficientemente familiarizado con el problema, es de esperar que pueda completar los detalles técnicos.
3
Hay una gran brecha entre ser "suficientemente complejo" y ser Turing completo. Coq es realmente complejo y es adecuado para una amplia gama de tareas prácticas.
1
@Kerrek SB Bueno, es posible que el lenguaje completo de Turing se use de manera que pueda demostrarse hasta la finalización. Si puede probar que una fórmula recursiva siempre se acerca a su condición de terminación (como la función factorial), podría probar que termina aunque no pueda manejar todo tipo de recursión.
@ArtB: Claro, siempre hay algunos programas que se puede probar que terminan. La primera pregunta del OP podría insinuar eso, aunque no estoy seguro de seguirla por completo. Por ejemplo, no podría tener un "algoritmo genérico" que determine si una determinada familia de programas termina, mientras que, por el contrario, probablemente podría construir una familia restringida de funciones de modo que suponiendo que una función pertenezca a esa familia, podría decir algorítmicamente si termina (Sin embargo, no estoy seguro de si esa familia puede ser no trivial. Supongo que sí, pero no puedo dar un ejemplo.)
2

TT

Esto es bastante trivial. Si tomamos la unión de cualquier subconjunto ce de TM detenidas y cualquier subconjunto ce de TM no detenidas, el resultado será un conjunto de TM para las cuales el problema de detención es decidible (ejecute ambas máquinas en paralelo, si el primero acepta la TM se detiene, si el segundo acepta, entonces la máquina no se detiene). Sin embargo, esto no conducirá a idiomas muy interesantes.

UNALosolTyometromidoMETRO

Kaveh
fuente
1

Sí, puedes, pero dudo que sea útil. Probablemente tendría que hacerlo mediante análisis de casos y luego solo podría buscar los casos más obvios. Por ejemplo, podría grep un archivo para el código while(true){}. Si el archivo tiene ese código, nunca terminará ^. En términos más generales, podría decir que un programa sin bucle o recursión siempre terminará y hay varios casos que podría hacer para garantizar que un programa terminará o no, pero incluso para un programa de tamaño medio esto sería muy difícil y en muchos casos no podría darle una respuesta.

tl; dr: Sí, pero no podrá hacer que sea útil para la mayoría de los programas útiles.

^ Sí, técnicamente si ese código no está en la ruta del código o si hay otros subprocesos, podría terminar, pero estoy haciendo un comentario general aquí.


fuente
44
¿Por qué crees que Coq y Agda no son útiles? Estás sobreestimando el valor de la integridad de Turing.
He usado Coq, pero mi reclamo permanece ya que la mayoría del software comercial está escrito en Java / C ++ / Ruby / C # para el cual mis reclamos son ciertos. El tipo de programas que el 90% de las personas están interesadas en escribir no se beneficiaría. Básicamente, si no conoce Coq / Agda, etc., no es el mercado objetivo.
55
Yo diría que el 99% de los programas del mundo real se beneficiarían si se implementan en un subconjunto de un lenguaje que no sea Turing completo. No implementará, digamos, la función de Ackermann todos los días. El 100% de CRUD no necesita un lenguaje "real". El procesamiento de datos es casi siempre trivial. Vea el proyecto Terminator: incluso están sirviendo un subconjunto decente de posibles programas de C ++, que es más que suficiente para el mundo real (incluidos los controladores y otros códigos de bajo nivel).
La mayoría de los proyectos del mundo real quieren reutilizar bibliotecas que están escritas en idiomas completos de Turing y usan sus IDEs, depuradores y tutoriales. Sí, podría lograr cosas en idiomas que no sean de Turing, pero no puedo imaginar que algunos digan realmente "Quiero hacer X" y mi respuesta sea "Usar Coq". PD: gracias por presentarme al Proyecto Terminator .
44
Ya se implementa una proporción inimaginablemente enorme de la lógica empresarial en un SQL no completo de Turing. Y las DSL y las eDSL están en aumento ahora. Entonces, pronto la mayoría de los programadores de aplicaciones empresariales se olvidarán de todos los lenguajes de "propósito general".