¿Es más fácil resolver el problema de detención de lo que la gente piensa?

Question

Aunque el caso general es indecidible, muchas personas aún resuelven problemas que son lo suficientemente equívocos para el uso diario.

En la tesis doctoral de Cohen sobre virus informáticos, mostró cómo el escaneo de virus es equivalente al problema de detención, sin embargo, tenemos toda una industria basada en este desafío.

También he visto el proyecto de terminación de Microsoft - http://research.microsoft.com/Terminator/

que me lleva a preguntar - se sobrestima el problema de la parada - ¿tenemos que preocuparnos por el caso general?

¿Se volverán los tipos de turing completos con el tiempo? ¿Los tipos dependientes parecen un buen desarrollo?

O, para mirar hacia otro lado, ¿comenzaremos a utilizar lenguajes no completos para obtener los beneficios del análisis estático?

Answer 1

El problema de Detención es realmente interesante solo si se lo mira en el caso general, ya que si el problema de Detención fuese decidible, todos los demás problemas indecidibles también serían decidibles mediante reducción.

Por lo tanto, mi opinión sobre esta pregunta es, no, no es fácil en los casos que importan. Dicho esto, en el mundo real, puede que no sea tan importante.

Consulte también: http://en.wikipedia.org/wiki/Halting_problem#Importance_and_consequences

Answer 2

Como programador del día a día, yo diría que vale la pena seguir lo más abajo que el caminopara resolver los problemas de estilo detención, incluso si sólo se acerca a ese límite y nunca lo alcances Como señaló, la detección de virus es valiosa. La búsqueda en Google no pretende ser la respuesta absoluta para "encontrarme la mejor X para Y", pero también es especialmente útil. Si desato un virus novedoso (muwahaha), ¿eso crea un conjunto de soluciones más grande, o simplemente arroja luz sobre un área problemática existente? Independientemente de la diferencia técnica, algunos desarrollarán y cobrarán pragmáticamente los servicios de "detección y eliminación" de seguimiento.

espero con interés reales científicos respuestas para sus otras preguntas ...

Answer 3

está resolviendo el problema de la parada más fácil que la gente piensa?

Creo que es exactamente tan difícil como la gente piensa.

¿Los tipos se vuelven completos con el tiempo?

My dear, they already are!

tipos dependientes parecen como un buen desarrollo?

Mucho.

Creo que podría haber un crecimiento en lenguajes no-Turing completos pero demostrables. Durante bastante tiempo, SQL estaba en esta categoría (ya no es así), pero esto realmente no disminuyó su utilidad. Ciertamente hay un lugar para tales sistemas, creo.

Answer 4

Por cierto, creo que la completitud de Turing de las plantillas muestra que la detención está sobrevalorada. La mayoría de los lenguajes garantizan que sus compiladores se detendrán; no tan C++. ¿Esto disminuye C++ como un idioma? No lo creo; tiene muchos defectos, pero las compilaciones que no siempre se detienen no son una de ellas.

Answer 5

No sé lo difícil que la gente piensa que es, así que no puedo decir si es más fácil. Sin embargo, tiene razón en su observación de que la indecidibilidad de un problema (en general) no significa que todas las instancias de ese problema sean indecidibles. Por ejemplo, puedo decirle fácilmente que un programa como while false do something finaliza (asumiendo la semántica obvia de while y false).

Los proyectos como el proyecto Terminator que mencionas obviamente existen (y probablemente incluso funcionen en algunos casos), por lo que está claro que no todo es inútil. También hay un concurso (creo que todos los años) para las herramientas que intentan probar la terminación para los sistemas de reescritura, que son básicamente un modelo de computación. Pero es el caso que la terminación en muchos casos es muy difícil de probar.

La manera más fácil de verlo es tal vez ver la indecidibilidad como un máximo en la complejidad de las instancias de un problema. Cada instanciación está en algún lugar en la escala de trivial a este máximo y con un máximo más alto normalmente se tiene que las instancias son más difíciles en promedio también.

Answer 6

Existen muchos programas para los cuales se puede resolver el problema de detención y muchos de esos programas son útiles.

Si tuviera un compilador que diga "Alto", "No se detiene" o "No sé", podría indicar qué parte del programa provocó el "Alto" o "Don". saber "condición". Si realmente deseaba un programa que definitivamente se detuviera o no se detuviera, entonces arreglaría esas unidades de "no sé" de la misma manera en que nos deshacemos de las advertencias del compilador. Creo que todos nos sorprenderíamos de la frecuencia con la que resultó útil intentar resolver este problema generalmente imposible.

Answer 7

Guau, esta es una pregunta confusa.

Primero: El problema de la detención no es un "problema" en un sentido práctico, como en "un problema que debe ser resuelto". Es más bien una afirmación sobre la naturaleza de las matemáticas, análoga al Teorema de Incompletitud de Gödel.

Segundo: El hecho de que construir un escáner de virus perfecto es intratable (debido a que es equivalente al problema de detención) es precisamente la razón por la que existe "toda una industria construida en torno a este desafío". Si se pudiera diseñar un algoritmo para el escaneo de virus perfecto, simplemente sería cuestión de que alguien lo haga una vez, y entonces ya no hay necesidad de una industria. Historia más.

Tercero: trabajar en un lenguaje Turing Complete no elimina "los beneficios del análisis estático", simplemente significa que hay límites para el análisis estático. Está bien, de todos modos, hay límites para casi todo lo que hacemos.

Finalmente: Si el problema de la detención pudiera ser "resuelto" de alguna manera, definitivamente sería "más fácil de lo que la gente piensa", ya que Turing demostró que no tiene solución. El caso general es el único caso relevante, desde un punto de vista matemático. Los casos específicos son cuestiones de ingeniería.

Answer 8

El hecho de que un problema sea indecidible no significa que no sea interesante: ¡al contrario! Así que sí, el hecho de que no tenemos un procedimiento eficaz y uniforme para abordar la terminación de todos los programas (así como muchos otros problemas sobre el software) no significa que no valga la pena buscar soluciones parciales.En cierto sentido, esta es la razón por la que necesitamos ingeniería de software: porque no podemos simplemente delegar la tarea a las computadoras.

El título de su pregunta es, sin embargo, un poco engañoso. Estoy de acuerdo con DrPizza: el problema de terminación es exactamente tan difícil como la gente piensa. Además, el hecho de que no necesariamente tengamos que preocuparnos por el caso general no implica que el problema de terminación esté sobrevalorado: vale la pena buscar soluciones parciales porque sabemos que la solución general es difícil.

Finalmente, las cuestiones sobre los tipos dependientes y los lenguajes subrepresivos, aunque parcialmente relacionadas, son realmente preguntas diferentes, y no estoy seguro de ver el punto de mezclarlas todas juntas.