En informatique théorique, plus précisément en théorie de la calculabilité, le théorème de Rice énonce que toute propriété sémantique non triviale d'un programme est indécidableCe théorème est la reformulation « intuitive » du corollaire B de la publication originale de Henry Gordon Rice (1953).. Le théorème de Rice généralise l'indécidabilité du problème de l'arrêt. Le théorème est devenu un classique et fait l'objet d'exercices dans certains ouvrages de théorie de la calculabilité. Il a une certaine portée philosophique vis-à-vis de la calculabilité et est dû au logicien Henry Gordon Rice.
Explication de l'énoncé vignette|L'animation montre une machine impossible : d'après le théorème de Rice, il n'existe pas de machine qui lit des codes sources de fonctions et qui prédit si la fonction ne renvoie jamais un entier non nul. Les propriétés sémantiques concernent le comportement d'un programme et s'opposent aux propriétés syntaxiques sur le code source du programme. Une propriété est non triviale si elle n'est ni vraie pour toute fonction calculable, ni fausse pour toute fonction calculable. La table suivante donne des exemples de propriétés non triviales syntaxiques et des propriétés non triviales sémantiques. Le théorème de Rice ne s'applique qu'aux propriétés sémantiques.
Propriétés syntaxiques (attention, le théorème de Rice ne s'applique pas)Propriétés sémantiques (et donc indécidables par le théorème de Rice) Le code source contient une instruction conditionnelle si...alors » Le code source contient moins de 10 fonctions « le programme ne rend jamais de valeurs nulles » « le programme ne termine jamais par une erreur d'exécution » « le programme calcule le même résultat qu'un programme donné », autrement dit « le programme calcule une fonction calculable donnée ». « le programme calcule un résultat correct par rapport à sa spécification » autrement dit « la fonction calculée par le programme est bien celle définie par la spécification ». C'est une variante du précédent. « le programme contient un virus » « le programme accède à un site Web »
Impact en vérification de programmes
Pour vérifier qu'un programme est correct, on peut recourir au test, y compris à des batteries de tests avec couverture de code. Mais comme l'a souligné Edsger Dijkstra .
La formulation pragmatique du théorème de Rice est qu'aucune méthode automatique d'analyse statique de programmes ne permet de décider, à partir du code source d'un programme, si la fonction qui associe les entrées à la sortie de ce programme satisfait ou non une propriété intéressante (non triviale) donnée.
En pratique, on adopte des stratégies pour contourner les limitations du théorème de Rice : Vérification de programmes avec seulement un nombre fini d'états. Méthode de vérification partiellement automatisée. Méthodes à base d'approximations. Méthodes restreignant l'ensemble des programmes sur lesquels on veut démontrer la propriété. Restrictions raisonnables de l'ensemble des fonctions calculablesPar exemple les fonctions normalisantes en calcul des constructions inductif, ne sont pas toutes fonctions calculables, mais couvrent toutes les fonctions utiles en mathématiques.. Ces stratégies ont donné lieu à différentes approches pour vérifier des programmes : l'interprétation abstraite, la vérification de modèles (model checking) et la preuve semi-automatisée de programmes par assistant de preuve. Aucune de ces méthodes n'a une portée universelle. Des recherches en cours visent à étendre les domaines d'application des vérificateurs, donc à diminuer les restrictions citées ci-dessus, mais le théorème de Rice dit que le vérificateur absolu n'existe pas ou comme disait Frederick Brooks « il n'y a pas de balle en argent » .
Un cas particulier introductif : la fonction réalisée par un programme Comme introduction au théorème de Rice, considérons le cas spécifique où la propriété du programme soumise à décision est le fait que le programme calcule une fonction donnée ; on dit aussi que le programme « réalise » la fonction . Par rapport à ce que nous avons dit dans l'introduction et le premier paragraphe, la propriété à décider sur la fonction associée au programme est l'égalité à . Autrement dit, on veut savoir si la fonction calculée par le programme est la fonction ou non. Nous allons considérer trois cas de généralité croissante.
La fonction est la fonction nulle part définie Si la fonction calculée par le programme est celle qui n'est pas définie, cela signifie que le programme ne se termine jamais, quelle que soit la valeur en entrée. Décider cette propriété n'est pas possible en application du théorème de l'indécidabilité de l'arrêt qui peut se formuler en disant qu'il n'y a pas d'algorithme pour décider si un programme réalise la fonction nulle part définie.
La fonction est la fonction carré
Supposons que nous souhaitions décider si un programme réalise la fonction carré, autrement dit, réalise la fonction . Il faut que nous puissions décider si le programme programmeCarré_p (x) = (x); x * x où est un programme quelconque, calcule effectivement la fonction pour une valeur , sans être non défini sur . Pour décider si le programme programmeCarré_p calcule la fonction carré, il faut décider si se termine sur . Il faut donc décider l'arrêt de sur . C'est ni plus ni moins le problème de l'arrêt, qui, comme l'on sait, est indécidable. Donc décider si un programme calcule le carré de la valeur qu'on lui donne en entrée est indécidable.
La fonction est une fonction quelconque On peut dans ce cas aussi ramener la décision de la fonction calculée par un programme pour une fonction quelconque au problème de l'arrêt, il suffit de remplacer x * x par (x), à savoir décider si le programme truc_p (x) = (x); (x) calcule la fonction . On en conclut donc qu'étant donnée une fonction , décider si un programme calcule la fonction est indécidable.
Différentes présentations Dans cette section, nous exposons différentes versions du théorème de Rice dans la littérature.
Version avec des machines de Turing Dans les ouvrages de théorie de la calculabilité, le théorème de Rice est souvent énoncé avec l'appui des machines de Turing. Wolper, dans son livre Introduction à la Calculabilité, énonce que toute propriété non triviale sur les langages récursivement énumérables est indécidable. On rappelle qu'un langage est récursivement énumérable s'il est accepté par une machine de Turing. Wolper insiste bien qu'il s'agit d'une propriété sur les langages acceptés par les machines de Turing et non pas sur les machines de Turing, c'est-à-dire une propriété sémantique et non pas syntaxique.
Version avec des programmes Olivier Ridoux et Gilles Lesventes proposent une propriété dite « extensionnelle » (i.e., sémantique) et non triviale sur des programmes.
Théorème de Rice pour les fonctions Le théorème de Rice peut être exprimé du point de vue des fonctions calculées par les programmes. On suppose que l'on travaille avec un langage de programmation Turing-complet. Soit la fonction calculée par le programme p. est donc le résultat de l'évaluation du programme p sur l'entrée . Si le programme p ne se termine pas sur l'entrée n'est pas défini. Comme il existe des programmes qui ne se terminent pas, la fonction est partielle. Notons FC l'ensemble de toutes les fonctions calculables partielles de dans . Soit F FC. Notons PF l'ensemble {p | F}, c'est-à-dire l'ensemble des programmes p tels que la fonction soit dans F. Le théorème de Rice dit que PF est récursif si et seulement si F=∅ ou F=FC.
Théorème de Rice pour les ensembles Le théorème de Rice pour les fonctions calculables peut également être exprimé du point de vue des ensembles récursivement énumérables. Notons RE la classe de tous les sous-ensembles de récursivement énumérables. Soit E RE. Notons P l'ensemble des programmes p qui décident un ensemble A E (i.e. y A ssi l'exécution de p se termine sur l'entrée y). Le théorème de Rice dit que P est récursif si et seulement si E = ∅ ou E=RE.
Le théorème de Rice ci-dessus exprime l'indécidabilité de propriétés portant sur les ensembles récursivement énumérables. Il est cependant possible de caractériser parmi de telles propriétés celles qui sont semi-décidables. Une propriété Prop sur les ensembles récursivement énumérables est dite monotone si, pour tous ensembles récursivement énumérables A et B tels que A B, on a Prop(A) Prop(B). Par exemple, « A est un ensemble fini » n'est pas monotone, alors que « A contient l'élément x » l'est. Soit Prop une propriété sur les ensembles récursivement énumérables et EProp RE la classe des ensembles récursivement énumérables qui satisfont Prop. Notons PA l'ensemble des programmes p qui décident un ensemble A E (i.e. y A ssi l'exécution de p se termine sur l'entrée y). Cette variante du théorème de Rice dit que si PEProp est récursivement énumérable, alors Prop est monotone.
Démonstration du théorème de Rice
Démonstration pour les ensembles
Soit P une propriété non triviale sur les ensembles récursivement énumérables. Sans perte de généralité, supposons que P(∅) est fausse (si ce n'est pas le cas, on raisonne pareillement avec la négation de P). Montrons que le problème de l'arrêt se réduit à la décision de P. Nous définissons une réduction qui transforme toute instance (M, w) du problème de l'arrêt, où M est une machine de Turing et w est un mot, en une machine de Turing M', instance de la décision de P.
Il existe un ensemble récursivement énumérable A qui satisfait P, et une machine MA qui accepte A. Dès lors, on construit de manière effective la machine de Turing M' suivante à partir de (M, w) : M'(u) Lancer M sur w Lancer MA sur u La démonstration s'achève avec la correction de la réduction : M s'arrête sur w, si et seulement si P(L(M')). En effet : Si M s'arrête sur w, le langage de M' est exactement le langage de MA, c'est-à-dire A et P(A). Si M ne s'arrête pas sur w, le langage de M' est le langage vide et P(∅) est fausse. Le théorème de Rice pour les fonctions peut se démontrer de façon similaire.
Démonstration pour les fonctions (par le théorème du point fixe de Kleene)
Le théorème de Rice pour les fonctions peut se démontrer par le théorème du point fixe de Kleene. Le théorème du point fixe de Kleene dit que pour tout transformateur de programme T qui est une fonction totale, il existe un programme p tel que les programmes p et T(p) calculent la même fonction ().
Soit une propriété non triviale ( et FC). Supposons par l'absurde que P = {p | F} est récursif.
Comme F est non triviale, il existe f et g . Les fonctions f et g étant calculables, il existe deux programmes p et q avec = f et = g. Définissons le transformateur de programmes T :
T(x) = q si x P
T(x) = p si x P
Comme P est récursif, T est une fonction totale calculable. Par le théorème du point fixe de Kleene, il existe un programme n tel que . Procédons maintenant par étude de cas sur la valeur de T(n) : Si T(n)=p, par définition de T, on a n P. Comme , T(n) P. Or T(n)=p P. Contradiction. Si T(n)=q, alors n P. Comme , T(n) P. Or T(n)=q P. Contradiction.
Preuve par réduction du problème de l'arrêt
Brouillon de preuve Avant d'établir une preuve formelle, tentons d'abord une approche par un cas pratique. Supposons que nous ayons un algorithme qui détermine de manière infaillible qu'un programme p est une implémentation correcte de la fonction de mise au carré. Celle-ci prend un entier d et retourne d2 . Il est à noter que la preuve fonctionne pour n'importe quel algorithme vérifiant une propriété non-triviale d'un programme.
L'intuition pour la preuve est de convertir notre algorithme vérifiant les programmes de mise au carré en un algorithme identifiant les fonctions qui s'arrêtent, faisant alors intervenir le problème de l'arrêt. Construisons pour ce faire un algorithme prenant comme entrées a et i et qui détermine si le programme a s'arrête pour un i donné.