Voir la source de Théorème de Rice

{{Voir homonymes|Rice}}
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 des langages de programmation|sémantique]] non triviale d'un [[Programme informatique|programme]] est [[indécidable]]<ref>Ce théorème est la reformulation « intuitive » du corollaire B de la publication originale de [[Henry Gordon Rice]] (1953).</ref>{{,}}<ref name=":0">{{Ouvrage|auteur1=Pierre Wolper|titre=Introduction à la calculabilité|éditeur=[[Éditions Dunod|Dunod]]|année=2006|passage=p. 150, Théorème 7.3|isbn=}}</ref>{{,}}<ref name=":1" />. Le théorème de Rice généralise l'indécidabilité du [[problème de l'arrêt]]. Le théorème est classique<ref name=":3">{{Ouvrage|langue=en|prénom1=Rogers, Hartley, Jr.,|nom1=1926-2015.|titre=Theory of recursive functions and effective computability|lieu=Cambridge (Mass.)/London|éditeur=[[MIT Press]]|année=1987|pages totales=482|passage=p. 34|isbn=0-262-68052-1|oclc=15108070|lire en ligne=https://www.worldcat.org/oclc/15108070}}</ref>{{,}}<ref name=":6">{{Ouvrage|prénom1=Mandrioli,|nom1=Dino.|titre=Theoretical foundations of computer science|éditeur=[[John Wiley & Sons|Wiley]]|année=1987|passage=p.174-175|isbn=0-471-83834-9|oclc=15162953|lire en ligne=https://www.worldcat.org/oclc/15162953}}</ref>{{,}}<ref name=":2">{{Ouvrage|prénom1=Hopcroft, John E.,|nom1=1939-|prénom2=Ullman, Jeffrey D.,|nom2=1942-|titre=Introduction to automata theory, languages, and computation|éditeur=Pearson/Addison Wesley|année=2007|pages totales=535|passage=p.307|isbn=978-0-321-46225-1|isbn2=0-321-46225-4|oclc=69013079|lire en ligne=https://www.worldcat.org/oclc/69013079}}</ref>{{,}}<ref name=":4">{{Ouvrage|prénom1=Machtey,|nom1=Michael.|titre=An introduction to the general theory of algorithms|éditeur=North-Holland|année=1978|passage=p.102 et 106|isbn=0-444-00226-X|oclc=3168554|lire en ligne=https://www.worldcat.org/oclc/3168554}}</ref>{{,}}<ref>{{Ouvrage|prénom1=Pippenger,|nom1=Nicholas.|titre=Theories of computability|éditeur=[[Cambridge University Press]]|année=1997|passage=p. 148|isbn=0-521-55380-6|oclc=35593710|lire en ligne=https://www.worldcat.org/oclc/35593710}}</ref>{{,}}<ref name=":7">{{Ouvrage|prénom1=Davis, Martin,|nom1=1928-|prénom2=Weyuker, Elaine|nom2=J.|titre=Computability, Complexity, and Languages|sous-titre=Fundamentals of Theoretical Computer Science|éditeur=Academic Press, Harcourt, Brace|année=1994|pages totales=609|passage=p. 102-103|isbn=978-0-12-206382-4|oclc=28506245|lire en ligne=https://www.worldcat.org/oclc/28506245}}</ref> et fait l'objet d'exercices dans certains ouvrages de théorie de la calculabilité<ref>{{Ouvrage|langue=en|auteur1=Sipser|titre=Introduction to the Theory of Computation|éditeur=|année=|passage=p. 210 Ex. 5.22|isbn=}}</ref>.  Il a une certaine portée philosophique vis-à-vis de la calculabilité et est dû au logicien [[Henry Gordon Rice]].

== Explication de l'énoncé ==
[[Fichier:Théorème de Rice.gif|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.

{| class="wikitable"
!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 (programmation)|instruction conditionnelle si...alors]] »
* Le code source contient moins de 10 fonctions
|
* « le programme ne rend jamais de valeurs nulles<ref name=":1">{{Ouvrage|auteur1=Olivier Ridoux|auteur2=Gilles Lesventes|titre=Calculateurs, Calculs et Calculabilité|éditeur=|année=|passage=p. 53|isbn=}}</ref> »
* « 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 (informatique)|test]], y compris à des batteries de tests avec [[couverture de code]]. Mais comme l'a souligné [[Edsger Dijkstra]]  {{citation | Le test de programmes peut être une façon très efficace de montrer la présence de bugs, mais est désespérément inadéquat pour prouver leur absence}}<ref>{{Article|langue=en|auteur1=Edsger Dijkstra|titre=The Humble Programmer|périodique=Communications of the ACM|volume=15|numéro=10|année=1972|pages=859-866}}</ref>.

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<ref>{{Ouvrage|langue=en|auteur1=Traub|titre=Formal Verification of Concurrent Embedded Software|éditeur=|année=|passage=p. 16|isbn=}}</ref>{{,}}<ref>{{Lien web|langue=Anglais|titre=Cours sur les méthodes formelles par John Rushby|url=http://www.csl.sri.com/users/rushby/slides/fm-tut.pdf|site=p. 129|date=|consulté le=}}</ref> :
# 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 calculables<ref>Par exemple les fonctions normalisantes en calcul des constructions inductif, ne sont pas toutes fonctions calculables, mais couvrent toutes les fonctions utiles en mathématiques.</ref>.
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<ref>{{Lien web|langue=Français|titre=Cours sur le model checking par Gerard Berry au Collège de France|url=http://www.college-de-france.fr/site/gerard-berry/course-2015-03-25-16h00.htm|site=|date=|consulté le=}}</ref>) 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]]
[[Pas de balle en argent|« il n'y a pas de balle en argent »]]<ref> {{en}} {{Article 
| titre = No Silver Bullet 
| journal = ''[[IEEE]] Computer Magazine''
| date =  Avril 1987 }}</ref>.

== 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 <math>f</math> ; on dit aussi que le programme « [[réalisabilité |réalise]] » la fonction <math>f</math>.   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é à <math>f</math>.  Autrement dit, on veut savoir si la fonction calculée par le programme est la fonction <math>f</math> 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'[[Problème de l'arrêt|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 <math>x \mapsto x^2</math>.  Il faut que nous puissions décider si le programme
:: ''programmeCarré''_p (x) =
::: <math>p</math>(x);
::: x * x
où <math>p</math> est un programme quelconque, calcule effectivement la fonction <math>x \mapsto x^2</math> pour une valeur <math>a</math>, sans être non défini sur <math>a</math>.  Pour décider si le  programme ''programmeCarré''_p calcule la fonction ''carré'', il faut décider si <math>p</math> se termine sur <math>a</math>. Il faut donc décider l'arrêt de <math>p</math> sur <math>a</math>. 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 <math>f</math> quelconque au [[problème de l'arrêt]], il suffit de remplacer x * x par <math>f</math>(x), à savoir décider si le programme
:: ''truc''_p (x) =
::: <math>p</math>(x);
::: <math>f</math>(x)
calcule la fonction <math>f</math>.  On en conclut donc qu'étant donnée une fonction <math>f</math>, décider si un programme calcule la fonction <math>f</math> 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<ref name=":2" />{{,}}<ref>{{Ouvrage|langue=en|prénom1=Papadimitriou, Christos|nom1=H.|titre=Computational complexity|lieu=Reading (Mass)|éditeur=[[Addison-Wesley]]|année=1994|pages totales=523|passage=p. 62|isbn=0-201-53082-1|oclc=28421912|lire en ligne=https://www.worldcat.org/oclc/28421912}}</ref>. Wolper, dans son livre ''Introduction à la Calculabilité''<ref name=":0" />, énonce que toute propriété non triviale sur les langages [[Récursivement énumérable|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<ref>{{Ouvrage|auteur1=Olivier Ridoux|auteur2=Gilles Lesventes|titre=Calculateurs, Calculs et Calculabilité|éditeur=[[Éditions Dunod|Dunod]]|collection=Sciences Sup|année=2008|pages totales=204|passage=p. 54|isbn=}}</ref> 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<ref name=":3" />{{,}}<ref name=":1" />{{,}}<ref name=":5">{{Ouvrage|prénom1=Bridges, D. S. (Douglas S.),|nom1=1945-|titre=Computability|sous-titre=a mathematical sketchbook|éditeur=[[Springer Science+Business Media|Springer-Verlag]]|année=1994|passage=p. 78 et 85|isbn=0-387-94174-6|oclc=28891770|lire en ligne=https://www.worldcat.org/oclc/28891770}}</ref>. On suppose que l'on travaille avec un langage de programmation [[Turing-complet]].
Soit <math>\phi_p</math> la fonction calculée par le programme ''p''.  <math>\phi_p(y)</math> est donc
le résultat de l'évaluation du programme ''p'' sur l'entrée <math>y\in\mathbb{N}</math>. Si le programme ''p'' ne se termine pas sur l'entrée {{nobr|<math>y</math>,}} <math>\phi_p(y)</math> n'est pas défini.  Comme il existe des programmes qui ne se terminent pas, la fonction <math>\phi_p</math> est ''partielle''. Notons ''FC'' l'ensemble de toutes les fonctions calculables partielles de <math>\mathbb{N}</math> dans <math>\mathbb{N}</math>. Soit ''F'' <math> \subseteq</math> ''FC''. Notons ''P<sub>F</sub>'' l'ensemble {''p'' | <math>\phi_p \in</math> ''F''}, c'est-à-dire l'ensemble
des programmes ''p'' tels que la fonction <math>\phi_p</math> soit dans ''F''. Le théorème de Rice dit que ''P<sub>F</sub>'' est [[ensemble récursif|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é<ref name=":8">{{Ouvrage|prénom1=Kozen, Dexter,|nom1=1951-|titre=Automata and computability|éditeur=|année=2013|pages totales=400|passage=Lecture 34|isbn=978-3-642-85706-5|oclc=883383306|lire en ligne=https://www.worldcat.org/oclc/883383306}}</ref> du
point de vue des ensembles [[récursivement énumérable|récursivement énumérables]]. 
Notons ''RE'' la classe de tous les sous-ensembles de <math>\mathbb{N}</math> [[récursivement énumérable|récursivement énumérables]]. Soit ''E'' <math> \subseteq</math> ''RE''. Notons ''P'' l'ensemble des programmes ''p'' qui décident un ensemble ''A'' <math> \in</math> ''E'' (i.e. ''y'' <math> \in</math> ''A'' ssi l'exécution de ''p'' se termine sur l'entrée ''y'').
Le théorème de Rice dit que ''P'' est [[ensemble récursif|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 [[récursivement énumérable|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'' <math> \subseteq</math> ''B'', on a ''Prop(A)'' <math>\Rightarrow</math> ''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 ''E<sub>Prop</sub>'' <math> \subseteq</math> ''RE'' la classe des ensembles récursivement énumérables qui satisfont ''Prop''.
Notons ''P<sub>A</sub>'' l'ensemble des programmes ''p'' qui décident un ensemble ''A'' <math> \in</math> ''E'' (i.e. ''y'' <math> \in</math> ''A'' ssi l'exécution de ''p'' se termine sur l'entrée ''y'').
Cette variante du théorème de Rice<ref name=":5" />{{,}}<ref name=":4" />{{,}}<ref name=":8" /> dit que si ''P<sub>E<sub>Prop</sub></sub>'' 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érable]]s. 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éduction (complexité)|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 M<sub>A</sub> 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 M<sub>A</sub> 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 M<sub>A</sub>, 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|théorème de Rice pour les fonctions]] peut se démontrer<ref name=":6" />{{,}}<ref name=":7" /> par le [[Théorème de récursion de Kleene|théorème du point fixe de Kleene]].  Le [[Théorème de récursion de Kleene|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 (<math>\phi_p = \phi_{T(p)}</math>).

Soit une propriété <math>F</math> non triviale (<math>F \neq \emptyset</math> et <math>F \neq</math>''FC''). Supposons par l'absurde que ''P'' = {''p'' | <math>\phi_p \in</math> ''F''} est récursif.

Comme ''F'' est non triviale, il existe ''f'' <math>\in F</math> et ''g'' <math>\in FC \setminus F</math>. Les fonctions ''f'' et ''g'' étant calculables, il existe deux programmes ''p'' et ''q'' avec <math>\phi_p</math> = ''f'' et <math>\phi_q</math> = ''g''.  Définissons le transformateur de programmes ''T'' :

''T(x) = q''  si ''x'' <math>\in</math> ''P''

''T(x) = p''  si ''x'' <math>\not\in</math> ''P''

Comme ''P'' est récursif, ''T'' est une fonction totale calculable. Par le [[Théorème de récursion de Kleene|théorème du point fixe de Kleene]], il existe un programme ''n'' tel que <math>\phi_n = \phi_{T(n)}</math>. 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'' <math>\not\in</math> ''P''.  Comme <math>\phi_n = \phi_{T(n)}</math>, ''T(n)'' <math>\not\in</math> ''P''.  Or ''T(n)=p''<math>\in</math> ''P''.  Contradiction.
* Si ''T(n)=q'', alors ''n'' <math>\in</math> ''P''.  Comme <math>\phi_n = \phi_{T(n)}</math>, ''T(n)'' <math>\in</math> ''P''.  Or ''T(n)=q'' <math>\not\in</math> ''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 ''d<sup>2</sup>'' . 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 [[Problème de l'arrêt|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é.

Cet algorithme construit la description d'un nouveau programme ''t'' prenant un unique argument ''n'', et  :
# Premièrement exécute le programme ''a'' avec comme entrée ''i''. (Note: ''a'' et ''i'' sont tous deux décrits dans ''t'')
# Secondement retourne le carré de ''n''.
Si ''a(i)'' tourne à l'infini, alors ''t'' ne parvient jamais à l'étape (2) quelle que soit la valeur de ''n''.

Ainsi ''t'' est une fonction calculant les carrés de nombres si et seulement si l'étape (1) se termine.

Comme notre supposition de départ était que nous pouvions fermement identifier les programmes calculant des carrés, nous pouvons déterminer si ''f'', lequel dépend de ''a'' et ''i'', est un tel programme, et ceci pour n'importe quels ''a'' et ''i''. Par conséquent, nous avons obtenu un programme décidant si le programme ''a'' s'arrête pour une certaine entrée ''i''.

Notez que notre algorithme de décision d'arrêt n'exécute jamais ''t'', mais passe seulement sa description au programme d'identification des carrés, lequel par hypothèse se termine toujours. Dès lors, si la description de ''t'' est construite de façon qu'il se termine toujours, l'algorithme d'arrêt ne peut par conséquent pas échouer à s'arrêter.
  halts (a,i) {
    define t(n) {
      a(i)
      '''return''' n×n
    }
    '''return''' est_une_fonction_de_carre(t)
  }

Cette méthode de preuve ne se concentre pas sur des fonctions calculant des carrés. Tant que ''certains'' programmes peuvent faire ce que nous essayons de reconnaître, c.à.d. déterminer une propriété d'un programme, nous pouvons faire un appel à ''a'' pour obtenir notre ''t''. Nous pourrions avoir une méthode vérifiant des programmes calculant des racines carrées, ou des programmes calculant la paye mensuelle, ou des programmes qui s'arrêtent avec une entrée donnée "<tt>Abraxas</tt>". Pour chaque cas, nous sommes capables de résoudre le problème de l'arrêt de manière similaire.

==== Preuve formelle ====
[[Image:Rice reduction.svg|thumb|Si nous avons un algorithme qui décide une propriété non-triviale, nous pouvons construire une machine de Turing qui décide du problème de l'arrêt.]]

Pour la preuve formelle, on suppose que les algorithmes définissent les fonctions partielles comme des [[Chaîne de caractères|chaînes de caractères]] et sont eux-mêmes représentés par des chaînes. La fonction partielle calculée par l'algorithme représenté par une chaîne de caractères ''a'' est notée '''F'''''<sub>a</sub>''. Cette preuve procède par un [[raisonnement par l'absurde]] : nous supposerons d'abord qu'il y ait une propriété non-triviale qui est décidée par un algorithme ; nous démontrerons ensuite que par cette supposition nous pouvons montrer que le [[problème de l'arrêt]] est calculable, ce qui est impossible et par conséquent, une contradiction.

Supposons maintenant que ''P(a)'' est un algorithme décidant d'une propriété non-triviale de '''F'''''<sub>a</sub>''. Supposons ensuite que ''P(ne-sarrete_pas)'' = "non", avec ''ne-sarrete_pas'' la représentation d'un algorithme qui ne s'arrête jamais. Si ce n'est pas vrai, alors cela vaut pour la négation de la propriété. Comme ''P'' décide une propriété non-triviale, cela implique qu'il existe une chaîne de caractères ''b'' représentant un algorithme et ''P(b)'' = "oui". Nous pouvons alors définir un algorithme ''H(a, i)'' comme suit :
# Construire une chaîne de caractères ''t'' représentant un algorithme ''T(j)'' tel que :
##T simule en premier le calcul de '''F'''''<sub>a</sub>(i)''.
##T simule le calcul de '''F'''''<sub>b</sub>(j)'' et retourne son résultat.
# Retourne ''P(t)''.

Nous pouvons maintenant montrer que ''H'' décide du problème de l'arrêt :

* Si l'algorithme représenté par a s'arrête pour une donnée i, '''alors''', '''F'''<sub>''t''</sub> = '''F'''<sub>''b''</sub>.  Parce que ''P(b)'' = "oui" et le résultat de ''P(x)'' dépend seulement de '''F'''<sub>''x''</sub>, cela implique que ''P(t)'' = "oui" et donc que ''H(a, i) ='' "oui". 
* Si l'algorithme représenté par a ne s'arrête pas pour une donnée i, '''alors''', '''F'''''<sub>t</sub>'' = '''F'''''<sub>ne-sarrete-pas</sub>'', la fonction partielle qui n'est jamais définie. Comme ''P(ne-sarrete-pas)'' = "non" et le résultat de ''P(x)'' dépend seulement de '''F'''''<sub>x</sub>'', cela implique que ''P(t)'' = "non" et donc, ''H(a, i)'' = "non". 

Comme le problème de l'arrêt n'est pas calculable, il y a une contradiction et par conséquent, l'hypothèse qu'il existe un algorithme ''P(a)'' qui décide une propriété non-triviale pour la fonction représentée doit être fausse. CQFD.

=== Démonstration pour les ensembles (variante du théorème) ===
De manière analogue à la démonstration du théorème de Rice pour les ensembles, on montre<ref name=":5" />{{,}}<ref name=":4" /> que la semi décision de la négation du [[problème de l'arrêt]] peut se réduire à la semi-décision de toute propriété non-monotone sur les ensembles récursivement énumérables.

Soit P une propriété non-monotone et semi-décidable. Il existe donc deux ensembles récursivement énumérables A et B,  calculés respectivement par des machines de Turing MA et MB tels que : 
:*A est inclus dans B 
:*A satisfait P  
:*B ne satisfait pas P.
De plus, il existe une machine de Turing MP qui, pour toute représentation d'une machine de Turing, s'arrête et accepte si l'ensemble récursivement énumérable accepté par cette machine satisfait P.

Dès lors, on peut construire une machine de Turing H prenant en entrée la représentation d'une machine de Turing M suivie d'une entrée x dont l'algorithme est le suivant : 

:1 Construire la représentation d'une machine de Turing T qui, sur une entrée y :
::1 Exécute en parallèle
::*MA sur y
::*MB sur y
::*M sur x
::2 Accepte y si 
::*MA accepte y ou bien
::*MB accepte y ET M s'arrête sur x
:2 Exécuter MP sur la représentation de T et renvoyer le résultat.

Par ''« exécuter en parallèle »'', on entend que la machine T exécute un pas MA sur y, puis un pas de MB sur y, puis un pas de M sur x, puis un second pas de MA sur y, et ainsi de suite.  Autrement dit, on «entrelace» les pas de calcul d'une machine avec ceux de l'autre machine.

Si M s'arrête sur x, T accepte y si, et seulement si MA ou MB accepte y, et comme A est inclus dans B, cela revient à dire si et seulement si y appartient à B. Donc, T accepte exactement l'ensemble B, qui, par hypothèse, ne vérifie pas P.
Par conséquent, MP n'accepte pas T. (P étant supposé semi-décidable, MP peut même ne pas s'arrêter du tout)
Si M ne s'arrête pas sur x, T accepte y si et seulement si y appartient à A. T accepte donc exactement l'ensemble A qui, par hypothèse, satisfait P.
Par conséquent, MP accepte T (et finit donc par s'arrêter, par définition de la semi-décidabilité).
La machine H calcule donc la négation du problème de l'arrêt. Celui-ci n'étant pas semi-décidable, par contradiction, P ne peut donc pas être semi-décidable.

== Notes et références ==
=== Notes ===
{{Traduction/Référence|lang1=en|art1=Rice's theorem}}
<references />
=== Références ===
* {{en}} {{Lien|Hartley Rogers, Jr.}}, {{Langue|en|''Theory of Recursive Functions and Effective Computability''}}, [[MIT Press]], {{ISBN|0262680521}}, page 34
* {{en}} H. G. Rice, {{Langue|en|''Classes of Recursively Enumerable Sets and Their Decision Problems''}}, {{Langue|en|Transactions of the [[American Mathematical Society]]}}, volume 74, numéro 2, {{date-|mars 1953}} ([https://www.jstor.org/sici?sici=0002-9947(195303)74%3A2%3C358%3ACORESA%3E2.0.CO%3B2-N JSTOR])
* [[Pierre Wolper]], ''Introduction à la calculabilité'', [[InterÉditions]], 1991, {{ISBN|2100048538}}
* {{Langages formels, calculabilité et complexité}}
* {{en}} Neil D. Jones, {{Langue|en|''Computability and Complexity From a Programming Perspective''}}, {{Langue|en|MIT Press}}, {{ISBN|0262100649}}

* {{Calculateurs, calculs, calculabilité (Ridoux, Lesventes)}}, Chapitre 4
* {{en}} D. Mandrioli, C. Ghezzi, {{Langue|en|''Theoretical Foundations of Computer Science''}}, [[John Wiley & Sons]], 1987; {{ISBN|0-471-83834-9}}, pages 174-175
* {{en}} D.S. Bridges, {{Langue|en|''Computability, A Mathematical Sketchbook''}}, [[Springer Science+Business Media|Springer]], {{ISBN|0387941746}}, 1994, pages 78 et 85.
* {{en}} M. Machtey, P. Young {{Langue|en|''Introduction to the General Theory of Algorithms''}}, [[North Holland]], 1978, pages 102 et 106
* {{en}} Martin Davis, Ron Sigal Elaine Weyuker, {{Langue|en|''Computability, Complexity, and Languages (2nd ed)''}}, [[Morgan Kaufmann]], {{ISBN|9780122063824}}, 1994, p. 609, page 103
* {{en}} Nicholas Pippenger, {{Langue|en|''Theories of computability''}}, [[Cambridge University Press]], {{ISBN|0-521-55380-6}}, 1997, page 148
* {{en}} John E. Hopcroft, Rajeev Motwani, Jeffrey D. Ullman , {{Langue|en|''Introduction to Automata Theory, Languages, and Computation (3rd Edition)''}}, [[Addison-Wesley]], {{ISBN|0321462254}}, 2006, page 307

{{Portail|logique|informatique théorique}}

{{DEFAULTSORT:Theoreme De Rice}}
[[Catégorie:Logique mathématique]]
[[Catégorie:Théorème d'informatique|Rice]]
[[Catégorie:Calculabilité]]