En la teoría de la computabilidad , el teorema de Rice establece que todas las propiedades semánticas no triviales de los programas son indecidibles . Una propiedad semántica se refiere al comportamiento del programa (por ejemplo, "¿el programa termina para todas las entradas?"), a diferencia de una propiedad sintáctica (por ejemplo, "¿el programa contiene una declaración si-entonces-si no ?"). Una propiedad no trivial es aquella que no es verdadera para todos los programas ni falsa para todos los programas.
El teorema generaliza la indecidibilidad del problema de detención . Tiene implicaciones de largo alcance sobre la viabilidad del análisis estático de programas. Implica que es imposible, por ejemplo, implementar una herramienta que compruebe si un programa determinado es correcto , o incluso se ejecuta sin errores.
El teorema lleva el nombre de Henry Gordon Rice , quien lo demostró en su tesis doctoral de 1951 en la Universidad de Syracuse .
El teorema de Rice establece un límite teórico sobre qué tipos de análisis estático se pueden realizar automáticamente. Se puede distinguir entre la sintaxis de un programa y su semántica . La sintaxis es el detalle de cómo está escrito el programa, o su "intensión", y la semántica es cómo se comporta el programa cuando se ejecuta, o su "extensión". El teorema de Rice afirma que es imposible decidir una propiedad de los programas que depende sólo de la semántica y no de la sintaxis, a menos que la propiedad sea trivial (verdadera para todos los programas o falsa para todos los programas).
Según el teorema de Rice, es imposible escribir un programa que verifique automáticamente la ausencia de errores en otros programas, tomando un programa y una especificación como entrada y verificando si el programa satisface la especificación.
Esto no implica la imposibilidad de prevenir ciertos tipos de errores. Por ejemplo, el teorema de Rice implica que en lenguajes de programación tipados dinámicamente que son completos en Turing , es imposible verificar la ausencia de errores de tipo. Por otro lado, los lenguajes de programación de tipo estático cuentan con un sistema de tipos que evita errores de tipo de forma estática. En esencia, esto debe entenderse como una característica de la sintaxis (en sentido amplio) de esas lenguas. Para verificar el tipo de programa, se debe inspeccionar su código fuente; la operación no depende simplemente de la semántica hipotética del programa.
En términos de verificación general de software, esto significa que, aunque no se puede comprobar algorítmicamente si un programa determinado satisface una especificación determinada, se puede exigir que los programas estén anotados con información adicional que demuestre que el programa es correcto, o que se escriban en una forma restringida particular. que hace posible la verificación, y sólo acepta programas que estén verificados de esta manera. En el caso de la seguridad de tipos, la primera corresponde a las anotaciones de tipo y la segunda corresponde a la inferencia de tipos . Llevada más allá de la seguridad de tipos, esta idea conduce a pruebas de corrección de programas a través de anotaciones de prueba como en la lógica de Hoare .
Otra forma de solucionar el teorema de Rice es buscar métodos que detecten muchos errores, sin ser completos. Esta es la teoría de la interpretación abstracta .
Otra dirección más para la verificación es la verificación de modelos , que sólo puede aplicarse a programas de estados finitos, no a lenguajes completos de Turing.
Sea φ una numeración admisible de funciones computables parciales . Sea P un subconjunto de . Suponer que:
Entonces P es indecidible .
Se puede hacer una afirmación más concisa en términos de conjuntos de índices : los únicos conjuntos de índices decidibles son ∅ y .
Dado un programa P que toma un número natural n y devuelve un número natural P ( n ), las siguientes preguntas son indecidibles:
Supongamos por contradicción que es un conjunto de números naturales no trivial, extensional y computable. Hay un número natural y un número natural . Definir una función por cuándo y cuándo . Según el teorema de recursividad de Kleene , existe tal que . Entonces, si tenemos , lo que contradice la extensionalidad de desde , y a la inversa, si tenemos , lo que nuevamente contradice la extensionalidad desde .
Supongamos, para ser más concretos, que tenemos un algoritmo para examinar un programa p y determinar infaliblemente si p es una implementación de la función de elevación al cuadrado, que toma un número entero d y devuelve d 2 . La prueba funciona igual de bien si tenemos un algoritmo para decidir cualquier otra propiedad no trivial del comportamiento del programa (es decir, una propiedad semántica y no trivial), y se presenta en general a continuación.
La afirmación es que podemos convertir nuestro algoritmo para identificar programas de cuadratura en uno que identifique funciones que se detienen. Describiremos un algoritmo que toma las entradas aey y determina si el programa a se detiene cuando se le da la entrada i .
El algoritmo para decidir esto es conceptualmente simple: construye (la descripción de) un nuevo programa t tomando un argumento n , el cual (1) primero ejecuta el programa a en la entrada i (tanto a como i están codificados en la definición de t ), y (2) luego devuelve el cuadrado de n . Si a ( i ) se ejecuta para siempre, entonces t nunca llega al paso (2), independientemente de n . Entonces, claramente, t es una función para calcular cuadrados si y sólo si termina el paso (1). Como hemos asumido que podemos identificar infaliblemente programas para calcular cuadrados, podemos determinar si t , que depende de aey , es tal programa; así hemos obtenido un programa que decide si el programa a se detiene en la entrada i . Tenga en cuenta que nuestro algoritmo de decisión de parada nunca ejecuta t , sino que sólo pasa su descripción al programa de identificación de cuadratura, que, por supuesto, siempre termina; Dado que la construcción de la descripción de t también puede realizarse de manera que siempre termine, la decisión de detenerse tampoco puede dejar de detenerse.
se detiene (a,i) { definir t(norte) { ai) devolver n×n } devolver es_una_función_cuadrada(t) }Este método no depende específicamente de poder reconocer funciones que calculan cuadrados; Siempre que algún programa pueda hacer lo que intentamos reconocer, podemos agregar una llamada a a para obtener nuestra t . Podríamos haber tenido un método para reconocer programas para calcular raíces cuadradas, o programas para calcular la nómina mensual, o programas que se detienen cuando se les da la entrada "Abraxas"; en cada caso, podríamos resolver el problema de la detención de manera similar.
Para la prueba formal, se supone que los algoritmos definen funciones parciales sobre cadenas y ellos mismos están representados por cadenas. La función parcial calculada por el algoritmo representado por una cadena a se denota por F a . Esta prueba procede por reducción al absurdo : suponemos que hay una propiedad no trivial que se decide mediante un algoritmo, y luego demostramos que se deduce que podemos decidir el problema de detención , lo cual no es posible y, por lo tanto, es una contradicción.
Supongamos ahora que P ( a ) es un algoritmo que decide alguna propiedad no trivial de F a . Sin pérdida de generalidad, podemos suponer que P ( no-halt ) = "no", siendo no-halt la representación de un algoritmo que nunca se detiene. Si esto no es cierto, entonces esto es válido para el algoritmo P que calcula la negación de la propiedad P. Ahora, dado que P decide una propiedad no trivial, se deduce que hay una cadena b que representa un algoritmo F b y P ( b ) = "sí". Entonces podemos definir un algoritmo H ( a , i ) de la siguiente manera:
Ahora podemos demostrar que H decide el problema de detención:
Dado que se sabe que el problema de detención es indecidible, esto es una contradicción y la suposición de que existe un algoritmo P ( a ) que decide una propiedad no trivial para la función representada por a debe ser falsa.