Muchos problemas en el análisis del programa son ‘reducibles’ al problema de detención *, lo que significa que podemos demostrar que cierta propiedad solo puede deducirse de manera confiable si el problema de detención es solucionable. Esto no desalienta a las personas a realizar análisis de programas, pero cambia la forma en que se aborda el análisis.
Para entender esto, debemos mirar un poco más de cerca lo que significa que un problema sea indecidible. Queremos saber si algo (un programa, por ejemplo) tiene alguna propiedad P (que podría ser “siempre se detiene”, o algo más). Si la propiedad es indecidible, esto solo significa que no siempre podemos obtener la respuesta correcta para cada programa concebible. Lo que podemos hacer (y debemos, si no queremos simplemente levantar las manos y alejarnos), es aceptar algunas restricciones o imprecisiones. Por lo general (pero no siempre) aceptamos una aproximación que puede estar equivocada en una dirección u otra, pero no en ambas.
Supongamos que el análisis que realmente queremos, pero que no podemos tener, siempre dirá Verdadero o Falso cuando se le pregunte si un programa tiene una propiedad (y siempre sería correcto). Si la propiedad es indecidible, podríamos escribir un algoritmo de análisis que devuelva Verdadero o Quizás. Tal análisis a veces se llama ‘conservador’ o ‘seguro’, porque si dice Verdadero, puede contar con él, pero a veces dice Quizás cuando la propiedad se mantiene. O podríamos escribir un análisis que devuelva Quizás o Falso … si dice que la propiedad no es válida, podemos estar seguros de ello, pero nunca nos da una garantía completa de que la propiedad es válida.
- ¿Cuál es la diferencia entre una función de costo y una función de pérdida en el aprendizaje automático?
- ¿Cómo se determina la depreciación de las computadoras?
- ¿Las computadoras son lo suficientemente rápidas?
- ¿Qué quieres decir con memoria de computadora?
- ¿Cuáles son ejemplos de computadoras híbridas?
La prueba es un ejemplo del tipo de aproximación que devuelve Quizás o Falso con respecto a la propiedad “el programa obedece su especificación”: si encontramos un error, que es una violación de una propiedad de corrección, entonces sabemos que la propiedad de corrección no espera, pero ninguna cantidad de pruebas nos puede dar una garantía completa de corrección. Muchos de los llamados análisis de programas “estáticos”, por otro lado, son “conservadores” o “seguros”. Necesitamos ambos tipos de análisis porque la indecidibilidad del problema de detención (y, por lo tanto, de todas las propiedades que pueden mostrarse tan difíciles como el problema de detención) significa que nunca podemos eliminar los ‘Maybes’ de ningún lado.
Puede notar que dejé de lado otro margen de maniobra: la indecidibilidad del problema de detención (y de otros problemas demostrablemente difíciles) significa que no siempre podemos obtener una respuesta definitiva para los programas arbitrarios . Entonces, ¿por qué no restringimos los programas y decimos “Te daré una respuesta definitiva, pero solo para los programas que siguen ciertas reglas”? A veces ese es un enfoque fructífero. Por ejemplo, aunque la posibilidad de un error de tipo en tiempo de ejecución en un lenguaje como Python o Javascript es indecidible, las reglas de tipo estático en un lenguaje como Java restringen los programas de una manera que permite dar rápidamente una respuesta definitiva a la pregunta ‘¿Este programa obedece las reglas de tipo estático de Java?’ El precio es que las restricciones necesarias tienden a ser bastante pesadas; por ejemplo, las reglas de tipo estático de Java rechazarán muchos programas que no podrían generar errores de tipo en tiempo de ejecución.
* Con respecto a ‘reducible al problema de detención’, a menudo es así como lo decimos informalmente, pero en realidad es al revés. Para mostrar que decidir la propiedad P es tan difícil como resolver el problema de detención, en realidad necesitamos reducir el problema de detención a una instancia de P. Por ejemplo, para demostrar que determinar si se puede alcanzar cada enunciado de un programa es un problema indecidible, demostramos que podemos hacer que la accesibilidad de una declaración dependa de si algún otro programa se detiene … por lo tanto, si no podemos decidir si ese otro programa se detiene, tampoco podemos decidir si todas las declaraciones del programa en cuestión son accesibles.
