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 (Nerode 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.

Théorème de Myhill-Nerode  Un langage est rationnel si et seulement si la relation est d'index fini ; dans ce cas, le nombre d'états du plus petit automate déterministe complet reconnaissant est égal à l'index de la relation. En particulier, ceci implique qu'il existe un automate déterministe unique avec un nombre minimal d'états.

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[1].

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 rest 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

  1. Eilenberg 1974, Théorème 8.1 (The Quotient Criterion), page 55.
(en) Cet article est partiellement ou en totalité issu de l’article de Wikipédia en anglais intitulé « Myhill–Nerode theorem » (voir la liste des auteurs).

Littérature

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

  • Olivier Carton, Langages formels, calculabilité et complexité : licence et master de mathématiques ou d'informatique, option informatique de l'agrégation de mathématiques, Paris, Vuibert, , 237 p. (ISBN 978-2-7117-2077-4, présentation en ligne)
  • Jacques Sakarovitch, Éléments de théorie des automates, Vuibert, , 816 p. (ISBN 978-2-7117-4807-5)Traduction anglaise avec corrections : Elements of Automata Theory, Cambridge University Press 2009, (ISBN 9780521844253).
  • (en) Samuel Eilenberg, Automata, Languages and Machines, Vol. A, New York, Academic Press, coll. « Pure and Applied Mathematics » (no 58), , xvi+451 (ISBN 978-0-12-234001-7)

L'article original est :

  • Anil Nerode, « Linear Automaton Transformations », Proceedings of the American Mathematical Society, vol. 9, no 4, , p. 541-544.

Articles connexes

  • Portail de l'informatique théorique
Cet article est issu de Wikipedia. Le texte est sous licence Creative Commons - Attribution - Partage dans les Mêmes. Des conditions supplémentaires peuvent s'appliquer aux fichiers multimédias.