Théorème de Kleene
From Wikipedia, the free encyclopedia
En informatique théorique, et plus précisément en théorie des automates, le théorème de Kleene affirme qu'un langage est rationnel (c'est-à-dire décrit par une expression rationnelle) si et seulement s’il est reconnu par un automate fini. C'est un théorème fondamental de la théorie des langages formels et des automates. La première formulation de ce théorème est due au mathématicien Stephen C. Kleene[1],[2].
Le début des automates finis, et notamment la genèse du théorème de Kleene est décrite par Dominique Perrin[2]. La première mention des automates finis remonte à un article McCulloch et Pitts en 1943[3]. C'est Stephen Kleene qui reprend cet article en 1956, et présente la première preuve de son théorème[1]. Le premier exposé complet est donné par Rabin et Scott en 1959[4].
Formulation contemporaine
Depuis le traité d'Eilenberg[5], le théorème de Kleene est formulé de façon plus concise comme suit.
L'ensemble des langages rationnels sur un alphabet est par définition le plus petit ensemble de parties de contenant les singletons et l'ensemble vide, et fermé par les opérations d'union, concaténation et étoile. Cet ensemble est noté .
On appelle langage reconnaissable sur un alphabet tout langage qui peut être reconnu par un automate fini sur . L'ensemble des langages reconnaissables est noté .
Le théorème de Kleene s'énonce alors comme suit.
Théorème de Kleene — Sur un alphabet fini , il y a égalité entre langages rationnels et langages reconnaissables. En d'autres termes, on a
Démonstrations
De nombreuses variantes de démonstrations de ce théorème existent[6]. La plupart des preuves sont constructives, c'est-à-dire que l'on donne des algorithmes qui calculent un automate à partir d'une expression rationnelle, et une expression rationnelle à partir d'un automate.
Inclusion Rat A* ⊂ Rec A*
- On prouve que l'ensemble des langages reconnaissables est fermé par les opérations d'union, produit et étoile en réalisant les constructions des automates appropriés (voir le paragraphe Construction d'automates finis à partir des expressions rationnelles de l'article Automate fini non déterministe) ; comme il contient de plus les singletons et l'ensemble vide, on conclut en utilisant la définition de .
- On prouve que les langages décrits par une expression rationnelle sont reconnus par automate fini. Les méthodes les plus répandues sont :
- la méthode de Thompson ;
- la méthode de Glushkov ;
- la méthode de Brzozowski.
Les applications pratiques ont suscité un intérêt pour le développement d'algorithmes efficaces pour réaliser les constructions qui interviennent dans la preuve.
Inclusion Rec A* ⊂ Rat A*
Il s'agit de donner une expression rationnelle pour le langage reconnu par un automate fini. Trois algorithmes sont courants :
- L'algorithme de McNaughton et Yamada : on calcule par itération les langages reconnus dont les chemins n'utilisent que certains états ;
- L'algorithme de Conway, dû à John Horton Conway : on calcule la matrice des langages reconnus par partition ;
- L'algorithme d'élimination ou méthode de Brzozowski et McCluskey : on élimine les états, et on remplace les étiquettes par des expressions rationnelles.
- Le lemme d'Arden.
Toutes ces méthodes sont des méthodes d'élimination d'états.