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 es una propiedad relacionada con el 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 if-then-else ?"). Una propiedad no trivial es una que no es verdadera 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 verifique si un programa dado es correcto o incluso si se ejecuta sin errores.
El teorema debe su nombre a 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 "intenció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 determinar 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 de tipado dinámico que son Turing-completos , es imposible verificar la ausencia de errores de tipo. Por otro lado, los lenguajes de programación de tipado estático presentan un sistema de tipos que previene estáticamente los errores de tipo. En esencia, esto debe entenderse como una característica de la sintaxis (tomada en un sentido amplio) de esos lenguajes. Para verificar el tipo de un programa, se debe inspeccionar su código fuente; la operación no depende meramente de la semántica hipotética del programa.
En términos de verificación de software en general, esto significa que, aunque no se puede comprobar algorítmicamente si un programa determinado satisface una especificación dada, se puede exigir que los programas estén anotados con información adicional que demuestre que el programa es correcto, o que estén escritos en una forma restringida particular que haga posible la verificación, y solo aceptar programas que se verifiquen de esta manera. En el caso de la seguridad de tipos, lo primero corresponde a las anotaciones de tipos, y lo segundo 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 mediante anotaciones de pruebas, como en la lógica de Hoare .
Otra forma de evitar 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 para la verificación es la comprobación de modelos , que sólo puede aplicarse a programas de estados finitos, no a lenguajes Turing-completos.
Sea φ una numeración admisible de funciones computables parciales . Sea P un subconjunto de . Supóngase 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 no trivial, extensional y computable de números naturales. Hay un número natural y un número natural . Defina una función por cuando y cuando . Por el teorema de recursión de Kleene , existe tal que . Entonces, si , tenemos , contradiciendo la extensionalidad de ya que , y a la inversa, si , tenemos , lo que nuevamente contradice la extensionalidad ya que .
Supongamos, para ser más concretos, que tenemos un algoritmo para examinar un programa p y determinar de manera infalible si p es una implementación de la función de elevación al cuadrado, que toma un 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 da en general a continuación.
La afirmación es que podemos convertir nuestro algoritmo para identificar programas que elevan al cuadrado en uno que identifique funciones que se detienen. Describiremos un algoritmo que toma las entradas a e i 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 que toma un argumento n , que (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 solo si el paso (1) termina. Dado que hemos asumido que podemos identificar infaliblemente programas para calcular cuadrados, podemos determinar si t , que depende de a e i , es un programa de este tipo; por lo tanto, hemos obtenido un programa que decide si el programa a se detiene en la entrada i . Nótese que nuestro algoritmo de decisión de detención nunca ejecuta t , sino que solo pasa su descripción al programa de identificación de cuadrado, que por suposición siempre termina; Dado que la construcción de la descripción de t también puede hacerse de manera que siempre termine, la decisión de detención tampoco puede dejar de detenerse.
se detiene (a,i) { definir t(n) { ai) devuelve n×n } devuelve es_una_función_cuadrada(t) }Este método no depende específicamente de la capacidad de reconocer funciones que calculen cuadrados; siempre que algún programa pueda hacer lo que estamos tratando de reconocer, podemos agregar una llamada a a para obtener nuestro 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 que están representadas por cadenas. La función parcial calculada por el algoritmo representada por una cadena a se denota F a . Esta prueba procede por reductio ad absurdum : suponemos que hay una propiedad no trivial que se decide mediante un algoritmo, y luego demostramos que se sigue que podemos decidir el problema de detención , lo cual no es posible y, por lo tanto, 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 es válido para el algoritmo P que calcula la negación de la propiedad P . Ahora bien, 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í". Podemos entonces definir un algoritmo H ( a , i ) de la siguiente manera:
Ahora podemos demostrar que H resuelve el problema de detención:
Como 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.