Voir la source de Théorème de Kleene

{{Confusion|Théorème de récursion de Kleene|Théorème du point fixe de Kleene}}

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 [[Langage rationnel|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 [[Langage formel|théorie des langages formels]] et des automates.
La première formulation de ce théorème est due au mathématicien [[Stephen Cole Kleene|Stephen C. Kleene]]<ref name="K"/>{{,}}<ref name="P"/>.

== Historique ==

Le début des automates finis, et notamment la genèse du théorème de Kleene est décrite par [[Dominique Perrin (universitaire)|Dominique Perrin]]<ref name="P">{{harvsp|Perrin|1995|texte=Perrin (1995)}}</ref>. La première mention des automates finis remonte à un article [[Warren McCulloch|McCulloch]] et [[Walter Pitts|Pitts]] en 1943<ref>{{harvsp|McCullogh et Pitts (1943)|réf=McCulloghPitts}}</ref>. C'est Stephen Kleene qui reprend cet article en 1956, et présente la première preuve de son théorème<ref name="K">{{harvsp|Kleene (1956)|réf=Kleene1956}}</ref>. Le premier exposé complet est donné par [[Michael Rabin|Rabin]] et [[Dana S. Scott|Scott]] en 1959<ref>{{harvsp|Rabin et Scott (1959)|réf=RabinScott1959}}</ref>.

== Formulation contemporaine ==

Depuis le traité d'[[Samuel Eilenberg|Eilenberg]]<ref>{{harvsp|Eilenberg (1984)|réf=EilenbergA}}</ref>, le théorème de Kleene est formulé de façon plus concise comme suit.

L'ensemble des [[langage rationnel|langages rationnels]] sur un alphabet <math>A</math> est par définition le plus petit ensemble de parties de <math>A^*</math> contenant les [[Singleton (mathématiques)|singletons]] et l'[[ensemble vide]], et fermé par les opérations d'[[Union (mathématiques)|union]], [[concaténation]] et [[étoile de Kleene|étoile]]. Cet ensemble est noté <math>\text{Rat } A^*</math>.

On appelle ''langage reconnaissable'' sur un alphabet <math>A</math> tout langage qui peut être reconnu par un automate fini sur <math>A</math>. L'ensemble des langages reconnaissables est noté <math>\text{Rec } A^*</math>.

Le théorème de Kleene s'énonce alors comme suit.

{{Théorème|Théorème de Kleene|Sur un alphabet fini <math>A</math>, il y a égalité entre langages rationnels et langages reconnaissables. En d'autres termes, on a
:<math>\text{Rat } A^* = \text{Rec } A^*</math>}}

== Démonstrations ==

De nombreuses variantes de démonstrations de ce théorème existent<ref name=Sakarovitch>voir {{harvsp|Sakarovitch (2003)|réf=Sakarovitch}}</ref>. La plupart des [[Démonstration (logique et mathématiques)|preuves]] sont constructives, c'est-à-dire que l'on donne des [[Algorithme|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 [[Automate fini non déterministe#Construction d'automates finis à partir des expressions rationnelles|''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 <math>\text{Rat } A^*</math>.
* 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 [[Algorithme de Thompson|Thompson]] ;
** la méthode de [[Construction de Glushkov|Glushkov]] ;
** la méthode de [[Dérivée de Brzozowski|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 (mathématiques)|matrice]] des langages reconnus par [[Partition d'un ensemble|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.

== Généralisations et extensions ==

=== Théorème de Kleene-Schützenberger ===

On doit au mathématicien [[Marcel-Paul Schützenberger]] l'extension du théorème de Kleene aux [[Série formelle|séries formelles]] (respectivement aux [[Automate pondéré|automates pondérés]]). Le théorème affirme qu'une série formelle en variables non [[Loi commutative|commutatives]] à coefficients dans un [[semi-anneau|demi-anneau]] est rationnelle si et seulement si elle est reconnue par un automate fini pondéré, dont les poids respectifs des étiquettes sont des éléments de ce demi-anneau<ref>Pour des extensions et variantes, voir {{harvsp|Droste et al. (2009)|réf=DrosteEtAl2009}}</ref>.

=== Extensions aux monoïdes ===
{{loupe|amorce=Voir aussi|ensemble rationnel}}
Le théorème de Kleene a fait l'objet de tentatives d'extension aux [[Monoïde|monoïdes]] généraux, pas nécessairement libres. Étant donné 
un monoïde <math>M</math>, les ''parties rationnelles'' de <math>M</math> sont la plus petite famille de parties de <math>M</math> contenant les singletons et l'ensemble vide, et fermée par union, produit et passage au sous-monoïde engendré (l'analogue de l'étoile de Kleene dans les monoïdes). On note <math>\text{Rat } M</math> l'ensemble des parties rationnelles de <math>M</math>.

Il convient d'exprimer de façon plus algébrique la notion de partie reconnaissable d'un monoïde. Une partie <math>H</math> d'un monoïde <math>M</math> est une ''partie reconnaissable'' de <math>M</math> si elle est saturée par une congruence d'index fini, en d'autres termes s'il existe un monoïde ''fini'' <math>N</math>, et un [[morphisme]] [[Surjection|surjectif]] <math>f:M\to N</math> tel que <math>H=f^{-1}(K)</math>, où <math>K=f(H)</math>. On note <math>\text{Rec } M</math> l'ensemble des parties reconnaissables de <math>M</math>.

Avec ces définitions, l'égalité <math>\text{Rec } M=\text{Rat } M</math> est par exemple vraie dans les monoïdes finis. McKnight a prouvé que si <math>M</math> est un monoïde finiment engendré, alors <math>\text{Rec } M\subset \text{Rat } M</math>. L'égalité n'est pas vraie en général. En particulier, dans le produit de deux monoïdes libres, les parties rationnelles sont les transductions rationnelles, alors que les parties reconnaissables sont, d'après un théorème de Mezei, des unions finies de produits de parties reconnaissables des deux monoïdes composants<ref name=Sakarovitch/>.

==== Le cas des groupes ====

Un sous-groupe <math>H</math> d'un [[Groupe (mathématiques)|groupe]] <math>G</math> est une partie reconnaissable de <math>G</math> si et seulement s'il est d'index fini.

Un sous-groupe <math>H</math> d'un groupe <math>G</math> est une partie rationnelle de <math>G</math> si et seulement s'il est finiment engendré.

Si <math>G</math> lui-même est finiment engendré, le théorème de McKnight cité plus haut implique que tout sous-groupe d'index fini est finiment engendré, un résultat habituellement attribué à Howson.

=== Théorèmes de Kleene pour les monoïdes partiellement commutatifs ===

Le théorème de Kleene reste valide, sous réserve d'une restriction de l'étoile de Kleene, dans les 
[[Monoïde des traces|monoïdes des traces]] ou monoïdes partiellement commutatifs libres<ref>Ce paragraphe est tiré de {{harvsp|Diekert et Métivier (1997)|réf=DiekertMetivier1997}}.</ref>.

Soit <math>A</math> un alphabet. Une ''[[Relation (mathématiques)|relation]] d'indépendance'' ou ''relation de commutation'' <math>I</math> est une partie <math>I</math> de <math>A\times A</math> qui est [[Relation réflexive|irréflexive]] et [[Relation symétrique|symétrique]]. Une relation d'indépendance <math>I</math> définit une ''relation de dépendance'' réflexive et symétrique <math>D</math> par <math>D=A\times A\setminus I</math>, et réciproquement.

Une relation d'indépendance induit une [[relation binaire]] <math>\sim</math> sur <math>A^*</math>, où <math>u\sim v</math> si et seulement si <math>u = xaby</math> et <math>v = xbay</math> pour des mots <math>x,y\in A^*</math> et une paire <math>(a,b)\in I</math>. On note <math>\equiv</math> est la fermeture réflexive, symétrique et [[Relation transitive|transitive]] de <math>\sim</math>. Le monoïde des [[Trace (théorie des ensembles)|traces]] est le monoïde quotient de <math>A^*/{\equiv}</math>. Les [[Appartenance (mathématiques)|éléments]] de <math>A^*/{\equiv}</math> sont des '''traces'''.
Pour un mot ou une trace <math>w</math>, on note <math>\text{alph}(w)</math> l'ensemble des lettres qui apparaissent dans <math>w</math>. Deux traces <math>u</math> et <math>v</math> sont ''indépendantes'' si toute lettre de <math>u</math> commute avec toute lettre de <math>v</math>. Une trace <math>u</math> est ''[[Graphe connexe|connexe]]'' si <math>\text{alph}(u)</math> induit un [[sous-graphe]] dont les sommets sont les lettres et les arêtes sont les éléments de <math>D</math>.

L'''étoile de Kleene concurrente'' (''concurrent star'' en anglais) d'une partie <math>X</math> de <math>A^*/{\equiv}</math> est l'ensemble <math>(c(X))^*</math>, où <math>c(X)</math> est l'ensemble des traces connexes non vides qui commutent avec une trace de <math>X</math>.
Notons <math>\text{Rat}^c (A^*/{\equiv})</math> le plus petit ensemble de parties de <math>A^*/{\equiv}</math> contenant les singletons et l'ensemble vide, et fermé par les opérations d'union, produit et l'étoile de Kleene concurrente. 
On a alors l'égalité suivante, due à Ochmański :
:<math>\text{Rat}^c (A^*/{\equiv})\ =\ \text{Rec} (A^*/{\equiv}).</math>

== Notes ==

{{Références|colonnes=2}}

=== Articles ===

* {{Article
| nom1 = Warren S. McCulloch
| nom2 =  Walter Pitts
| titre = A logical calculus of the ideas immanent in nervous activity
| journal = Bull. Math. Biophys. 
| volume = 5
| année = 1943
| pages= 115-133
| id=McCulloghPitts}}
* {{Article
| auteur = Robert McNaughton et H. Yamada
| titre = Regular Expressions and State Graphs for Automata
| journal = IEEE Transactions on Electronic Computers
| volume = 9
| numéro=1
| année = 1960
| pages= 39-47
| id=McNaughtonYamada}}

* {{Article
| auteur = Stephen C. Kleene
| titre = Representation of events in nerve nets and finite automata. Automata studies
| journal = Annals of Mathematics Studies
| numéro = 34
| éditeur = Princeton University Press
| année = 1956
| pages= 3-41
| id=Kleene1956}}
* {{Article
| auteur = Dominique Perrin
| titre = Les débuts de la théorie des automates
| journal = Technique et science informatiques
| volume = 14
| numéro = 4
| année = 1995
| pages= 409-433
| url texte = http://www-igm.univ-mlv.fr/~perrin/Recherche/Publications/Loi/copie3.ps
| id=Perrin1995}}
* {{Article
| auteur = Michael O. Rabin et Dana Scott
| titre = Finite automata and their decision problems
| journal = IBM J. Res. Develop.
| volume = 3
| année = 1959
| pages= 114-125
| id=RabinScott1959}}
* {{chapitre 
|auteur1 = Michaël Cadilhac | auteur2 = Dmitry Chistikov | auteur3 = Georg Zetzsche
|titre = Rational Subsets of Baumslag-Solitar Groups
|titre ouvrage = Actes de ICALP 2020
|auteur ouvrage = Artur Czumaj Anuj Dawar Emanuela Merelli (éditeurs)
|collection = LIPIcs
|numéro dans collection = 168
|passage = 116:1-116:16
|éditeur = Schloss Dagstuhl - Leibniz-Zentrum für Informatik
|année = 2020
|url       = https://doi.org/10.4230/LIPIcs.ICALP.2020.116
|doi       = 10.4230/LIPIcs.ICALP.2020.116
|arxiv = 2006.11898 (version détaillée)
}}

=== Bibliographie ===

* {{Langages formels, calculabilité et complexité}}

* {{chapitre
| langue =  en
| prénom1 = Volker
| nom1 = Diekert
| prénom2 = Yves 
| nom2=Métivier
| titre chapitre = Partial Commutation and Traces
| auteurs ouvrage = G. Rozenberg, A. Salomaa (éditeurs)
| titre ouvrage = Handbook of Formal Languages
| éditeur = Springer Verlag
| année = 1997
| volume = 3
| titre volume = Beyond Words
| page début chapitre = 457-533
| isbn = 978-3-5406-0649-9
| id = DiekertMetivier1997
}}

* {{Ouvrage|langue=en|auteur1=Manfred Droste|auteur2=Werner Kuich|auteur3=Heiko Vogler|titre=Handbook of Weighted Automata|éditeur=[[Springer Science+Business Media|Springer-Verlag]]|année=2009|pages totales=608|isbn=978-3-642-01491-8|id=DrosteEtAl2009}}

* {{Ouvrage|langue=en|auteur1=Samuel Eilenberg|titre=Automata, Languages and Machines, Vol. A|lieu=New York|éditeur=[[Academic Press]]|année=1974|isbn=978-0-12-234001-7|id=EilenbergA}}

* {{Introduction to Automata Theory, Languages, and Computation}}

* {{Ouvrage| auteur1=Jacques Sakarovitch| titre=Éléments de théorie des automates| éditeur=[[Vuibert]]| année=2003| pages totales=816| isbn=978-2-7117-4807-5| id=Sakarovitch}}{{Commentaire biblio|Traduction anglaise avec corrections : ''Elements of Automata Theory'', Cambridge University Press 2009, {{ISBN|978-0-52184425-3}}}}

== Articles connexes ==

* [[Lemme de l'étoile]]
* [[Théorie des automates]]
* [[Hiérarchie de Chomsky]]
* [[Langage rationnel]]
* [[Automate fini déterministe]]
* [[Automate fini non déterministe]]
* [[Automate fini]]
* [[Monoïde syntaxique]]
* [[Expression rationnelle]]

{{Palette Informatique théorique}}
{{Portail|mathématiques|informatique|informatique théorique}}

{{DEFAULTSORT:Theoreme De Kleene}}
[[Catégorie:Théorème d'informatique|Kleene]]
[[Catégorie:Théorème de logique mathématique|Kleene]]
[[Catégorie:Langage formel|Theoreme de Kleene]]
[[Catégorie:Stephen Cole Kleene|Theoreme de Kleene]]
[[Catégorie:Théorie des automates]]
[[Catégorie:Automates finis et langages réguliers]]