Un théorème de la théorie de la calculabilité affirmant que toute propriété sémantique non triviale du langage reconnu par une machine de Turing est indécidable : aucun algorithme ne peut décider, pour une machine quelconque, si le langage qu'elle accepte possède cette propriété, si la propriété dépend seulement du langage et n'est pas triviale.

Principe

Les propriétés sémantiques des langages reconnus (propriétés ne dépendant que de l'ensemble de chaînes acceptées) sont soit triviales (vraies pour toutes les machines ou pour aucune) soit indécidables ; il n'existe pas de procédure générale pour les propriétés non triviales au niveau du langage.

Démonstration

Exemple concret : la propriété « le langage reconnu par la machine est régulier » est une propriété sémantique non triviale et, d'après le théorème de Rice, indécidable : on ne peut pas écrire un algorithme qui, pour une machine de Turing quelconque, décide correctement si son langage accepté est régulier.

Mauvaise application

Appliquer le théorème de Rice à des propriétés syntaxiques ou de ressources (par exemple « la machine a moins de 10 états » ou « la machine s'exécute en temps linéaire »), qui ne sont pas des propriétés sémantiques pures et peuvent être décidables ; ou conclure à tort que toute analyse de programmes est impossible en pratique.

Conséquence

Explique pourquoi de nombreuses propriétés non triviales des programmes (terminaison pour toutes les entrées, équivalence à une spécification, propriétés de correction non triviales) sont indécidables en général, orientant les attentes pour l'analyse statique et motivant des techniques approximatives, conservatrices ou limitées au domaine.

Inversion

Le cas inverse est que les propriétés syntaxiques ou les propriétés sémantiques triviales sont décidables ; restreindre la classe de machines ou de langages (par exemple aux automates finis) peut restaurer la décidabilité.

Limite

S'applique uniquement aux propriétés sémantiques des langages reconnaissables par une machine de Turing qui sont non triviales et extensives (dépendant uniquement du langage) ; il ne couvre pas les caractéristiques syntaxiques, les bornes de ressources, les garanties probabilistes ni les propriétés définies par rapport à une classe restreinte de machines.

Tension sémantique

Tension entre l'indécidabilité sémantique (ce que sont les langages) et l'analyse pratique de programmes qui se fonde sur des motifs syntaxiques, des heuristiques, des domaines restreints ou des approximations conservatrices pour éviter le cas indécidable général.

Synthèse

Le théorème de Rice formalisent une limite générale : toute question non triviale portant uniquement sur l'ensemble de chaînes qu'une machine de Turing accepte est indécidable, ce qui oblige l'analyse de programmes à recourir à des approximations, des restrictions ou à des informations non extensionales.