Teorema de Rice

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 finaliza para todas las entradas?"), a diferencia de una propiedad sintáctica (por ejemplo, "¿el programa contiene una instrucción if-then-else ?"). Una propiedad no trivial es aquella que no es verdadera ni falsa para todos los programas.

El teorema generaliza la indecidibilidad del problema de la parada . Tiene implicaciones de gran alcance en 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 (es posible implementar una herramienta que siempre sobreestime o siempre subestime, por lo que en la práctica hay que decidir qué representa un problema menor).

El teorema recibe su 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 para los tipos de análisis estático que pueden realizarse automáticamente. Se puede distinguir entre la sintaxis de un programa y su semántica . La sintaxis describe cómo está escrito el programa, o su "intensión", y la semántica describe cómo se comporta el programa al ejecutarse, o su "extensión". El teorema de Rice afirma que es imposible determinar una propiedad de los programas que dependa únicamente de la semántica y no de la sintaxis, a menos que la propiedad sea trivial (verdadera 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 como entrada un programa y una especificación , y comprobando si el programa cumple con la especificación.

Esto no implica la imposibilidad de prevenir ciertos tipos de errores. Por ejemplo, el teorema de Rice implica que en los 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 cuentan con un sistema de tipos que previene estáticamente los errores de tipo. En esencia, esto debe entenderse como una característica de la sintaxis (en un sentido amplio) de dichos lenguajes. Para verificar el tipo de un programa, es necesario 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, si bien no se puede comprobar algorítmicamente si un programa determinado cumple con una especificación dada, se puede exigir que los programas estén anotados con información adicional que demuestre su corrección, o que estén escritos en una forma restringida específica que posibilite 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 tipo, y lo segundo a la inferencia de tipos . Más allá de la seguridad de tipos, esta idea conduce a pruebas de corrección de programas mediante anotaciones de prueba, como en la lógica de Hoare .

Otra forma de sortear el teorema de Rice es buscar métodos que detecten muchos errores, sin llegar a ser completos. Esta es la teoría de la interpretación abstracta .

Otra vía para la verificación es la comprobación de modelos , que solo se puede aplicar a programas de estados finitos, no a lenguajes Turing-completos.

Dejar${\displaystyle \varphi }$Sea una numeración admisible de las funciones computables parciales , y sea${\displaystyle P}$ser un subconjunto de${\displaystyle \mathbb {N} }$Supongamos que:

1. ${\displaystyle P}$no es trivial :${\displaystyle P}$no está ni vacío ni${\displaystyle \mathbb {N} }$sí mismo.
2. ${\displaystyle P}$es extensional : para todos los enteros${\displaystyle m}$y${\displaystyle n}$, si${\displaystyle \varphi _{m}=\varphi _{n}}$, entonces${\displaystyle m\in P\iff n\in P}$.

Entonces${\displaystyle 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${\displaystyle \varnothing }$y${\displaystyle \mathbb {N} }$.

Dado un programa P que toma un número natural n y devuelve un número natural P ( n ), las siguientes preguntas son indecidibles:

• ¿ Termina P en un n dado ? (Este es el problema de la parada ).
• ¿ P termina en 0?
• ¿ P termina en todos los n (es decir, P es total )?
• ¿ El programa P finaliza y devuelve 0 con cada entrada?
• ¿La función P finaliza y devuelve 0 con alguna entrada?
• ¿El algoritmo P finaliza y devuelve el mismo valor para todas las entradas?
• ¿Es P equivalente a un programa Q dado ?

Supongamos por contradicción que${\displaystyle P}$es un conjunto no trivial, extensional y computable de números naturales. Dado que${\displaystyle P}$no es trivial, hay un número natural${\displaystyle a\in P}$y un número natural${\displaystyle b\notin P}$. Defina la función computable total${\displaystyle Q}$de${\displaystyle e}$y${\displaystyle x}$por${\displaystyle Q_{e}(x)=\varphi _{b}(x)}$cuando${\displaystyle e\in P}$y${\displaystyle Q_{e}(x)=\varphi _ {a}(x)}$cuando${\displaystyle e\notin P}$. Por el teorema de recursión de Kleene , existe${\displaystyle e}$de tal manera que${\displaystyle \varphi _ {e} = Q_ {e}}$. Entonces, si${\displaystyle e\in P}$, tenemos${\displaystyle \varphi _{e}=\varphi _{b}}$, contradiciendo la extensionalidad de${\displaystyle P}$desde${\displaystyle b\notin P}$y a la inversa, si${\displaystyle e\notin P}$, tenemos${\displaystyle \varphi _ {e} = \varphi _ {a}}$, lo cual contradice nuevamente la extensionalidad ya que${\displaystyle a\in P}$.

• Problema de parada
• Teorema de Rice-Shapiro y teorema de Kreisel-Lacombe-Shoenfield-Tseitin , generalizaciones del teorema de Rice.
• Teorema de Scott-Curry , análogo al teorema de Rice en cálculo lambda.
• Demostración de Turing

• Hopcroft, John E.; Ullman , Jeffrey D. ( 1979), Introducción a la teoría de autómatas, lenguajes y computación , Addison-Wesley , págs. 185–192 
• Rice, HG (1953), "Clases de conjuntos recursivamente enumerables y sus problemas de decisión", Transactions of the American Mathematical Society , 74 (2): 358–366 , doi : 10.1090/s0002-9947-1953-0053041-6 , JSTOR 1990888 
• Rogers, Hartley Jr. (1987), Teoría de las funciones recursivas y la computabilidad efectiva (2.ª  ed.), McGraw-Hill , §14.8