Théorème de Myhill-Nerode

En informatique théorique, et notamment en théorie des langages formels et des automates, le théorème de Myhill-Nerode donne une condition nécessaire et suffisante pour qu'un langage formel soit un langage rationnel, c'est-à-dire reconnaissable par un automate fini. Ce théorème porte les noms de  John Myhill et Anil Nerode qui l'ont prouvé en 1958 .

L'intérêt de cet énoncé est que la condition nécessaire et suffisante porte sur le langage lui-même, et ne fait pas appel à la construction d'un automate. La preuve est par contre constructive, et permet d'obtenir effectivement un automate qui s'avère de plus être minimal.

Énoncé du théorème 

Étant donné un langage  et deux mots  et , on dit qu'un mot  sépare  et  si un et un seul des mots  et  est dans le langage . Deux mots  et  sont inséparables (undistiguishable en anglais) s'il n'existe pas de mot  qui les sépare.

On définit une relation   sur les mots, appelée relation de Myhill-Nerode, par la règle :  si et seulement si  et  sont inséparables. Il est facile de montrer que la relation  est une relation d'équivalence sur les mots, et donc partitionne l'ensemble de tous les mots en classes d'équivalences. Le nombre de classes est appelé l'index de la relation. Il peut être fini ou infini.

Démonstration  
Soit  un langage rationnel. Il existe un automate fini déterministe complet  qui reconnaît . Pour chaque état  de cet automate, soit  l’ensemble des mots  qui mènent de l'état initial à . Si  et  sont deux mots de , alors pour tout mot , les mots  et  mènent au même état, qu'il soit acceptant ou non. Ainsi, aucun mot  ne peut séparer  et , et ils sont donc inséparables. Ceci montre que l'ensemble  est contenu dans une classe de l'équivalence , et comme tout mot est dans un des ensembles , l'index de la relation  est inférieur ou égal au nombre d'états de l'automate, et donc est fini.

Réciproquement, supposons que la relation de Myhill-Nerode  est d'index fini. Dans ce cas, on construit un automate fini reconnaissant  comme suit. Les états sont les classes de l'équivalence . L'état initial  est la classe d'équivalence du mot vide, et la fonction de transition mène, pour un état  et une lettre , à l'état  qui contient le mot  , où  est un mot quelconque de . La définition de l'équivalence  assure que la fonction de transition est bien définie : si , alors  pour toute lettre , car si un mot  était un séparateur de   et , alors  séparerait  et . Un état de l'automate est final s'il contient un mot de . Comme précédemment, la définition de la relation  implique alors que tous les éléments de cette classe sont dans , sinon le mot vide pourrait séparer des mots de cette classe.

Ainsi, l'existence d'un automate fini reconnaissant  implique que la relation  est d'index fini, et d'index au plus égal au nombre de d'états de l'automate, et la finitude de l'index de  implique l'existence d'un automate ayant ce nombre d'états.

Relation de Myhill-Nerode et résiduels 

Étant donné un langage  de  et un mot , le quotient gauche de  par , ou le résiduel de  par , est l'ensemble noté  défini par
 .
Avec cette notation, deux mots  et  sont inséparables si et seulement si . Les classes de l'équivalence de Myhill-Nerode sont donc en bijection avec les résiduels de . Il en résulte qu'un langage est rationnel si et seulement si l'ensemble de ses résiduels est fini. C'est sous cette forme que le théorème est énoncé dans le traité d'Eilenberg.

Applications 

On peut employer le théorème pour prouver qu'un langage est rationnel en démontrant que la relation  est d'index fini. Ceci se fait par une exploration systématique des mots à partir du mot vide : pour chaque mot, on cherche une classe déjà existante ou on crée une nouvelle classe. Par exemple, considérons le langage des mots binaires qui représentent des entiers divisibles par 3. Le mot vide (de valeur 0) et le mot 1 sont séparés par le mot vide, le mot 0 sépare le mot vide de 1. On a déjà trois classes correspondant aux nombres de reste 0, 1, et 2 modulo 3. Il reste à vérifier qu'il n'y a pas d'autre classe.

Un usage plus fréquent est la preuve qu'un langage n'est pas rationnel en montrant que l'index de la relation de Myhill-Nerode est infini. Si on prend par exemple le langage bien connu , alors deux mots  et , avec , sont séparables et séparés par le mot  (ou ). Ainsi, ce langage n'est pas rationnel.

Extension 
Le théorème de Myhill-Nerode se généralise aux arbres. Voir automate d'arbres.

Notes et références

Notes

Littérature 

La plupart les livres d'enseignement des langages formels exposent ce théorème. 
 

 

L'article original est :
.

Articles connexes 
Lemme d'itération, une autre méthode pour prouver qu'un langage n'est pas rationnel.
Monoïde syntaxique, le monoïde de transition de l'automate minimal.
Automate d'arbres.

Théorie des automates
Théorème d'informatique
Théorème de combinatoire