Voir la source de Lemme d'Arden

{{Voir homonymes|Arden}}

En [[théorie des automates]], le '''lemme d'Arden''' est un résultat concernant les [[Langage rationnel|langages rationnels]].

Il décrit les solutions de l'équation :
:<math>X = A \cdot X \cup B</math>
où <math>A</math> et <math>B</math> sont deux langages formels et <math>X</math> est une inconnue. Le lemme d'Arden s'utilise notamment dans la méthode des équations linéaires gauches qui permet de calculer le langage reconnu par un [[automate fini]] donné.

Le lemme est nommé d'après Dean N. Arden qui l'a décrit en 1961<ref name="Arden"/>. C'est maintenant un résultat que l’on retrouve dans de nombreux manuels ou supports de cours.

== Énoncé ==

{{théorème|Lemme d'Arden|Soient <math>A</math> et <math>B</math> deux langages formels. Le langage
:<math>L = A^*B</math>
est le plus petit langage (pour l'inclusion ensembliste) qui est solution de l'équation
:<math>X = (A \cdot X )\cup B</math>
De plus, si <math>A</math> ne contient pas le [[mot vide]] <math>\varepsilon</math>, le langage <math>A^*B</math> est l'unique solution de cette équation.}}

On peut voir l'équation <math>X = A \cdot X \cup B</math> comme la définition récursive d'un langage : un mot de ce langage est soit dans <math>B</math>, soit formé d'un mot dans <math>A</math> suivi d'un autre mot du langage, et on peut interpréter la solution comme une définition itérative : un mot est formé d'une suite de mots dans <math>A</math>, puis d'un mot final dans <math>B</math>.

== Exemples ==

* L'équation <math>X=aX\cup b</math>, où <math>a</math> et <math>b</math> sont des lettres, a pour unique solution <math>a^*b=\{b,ab,aab,\ldots,a^nb,\ldots\}</math>.

* L'équation <math>X=X\cup B</math>, où <math>B</math> est un langage, a pour plus petite solution <math>B</math>. Ici  <math>A</math> est composé du mot vide, et <math>A^*=A</math>. En fait, tout langage contenant <math>B</math> est solution.

* L'équation <math>X=AX\cup B</math>, avec <math>A=a^*b</math> et <math>B=a^*</math> a pour unique solution <math>(a^*b)^*a^*=\{a,b\}^*</math>. En effet, l'équation signifie qu'un mot de la solution ou bien n'est formé que de lettres <math>a</math>, ou bien commence par un préfixe formé d'une suite de lettres <math>a</math> suivie d'un <math>b</math>, et d'un autre mot de la solution.

== Démonstration ==
1. Le langage <math>L=A^* \cdot B</math> est solution. En effet, on a :
:<math>AL\cup B = A(A^*B) \cup B = (AA^* \cup\{\varepsilon\})B = A^*B=L</math>.

2. Le langage <math>A^* \cdot B</math> est la plus petite solution. Soit en effet <math>L</math> une autre solution. Alors on a :
<math>L=AL\cup B=A(AL\cup B)\cup B=A^2L\cup AB\cup B</math>.
En continuant à remplacer <math>L</math> par <math>AL\cup B</math>, on obtient pour tout <math>n>0</math> l'équation
:<math>L=A^{n+1}L\cup A^nB\cup A^{n-1}B\cup\cdots\cup AB\cup B</math>,
ce qui montre que <math>L</math> contient tous les <math>A^nB</math>, donc <math>A^*B</math>.

3. Si <math>A</math> ne contient pas <math>\varepsilon</math>, alors cette solution est la seule. Soit en effet <math>L</math> une autre solution. On sait déjà que <math>L</math> contient <math>A^*B</math>. Par ailleurs, on a pour tout <math>n>0</math> l'équation
:<math>L=A^{n+1}L\cup A^nB\cup A^{n-1}B\cup\cdots\cup AB\cup B</math>.
Soit <math>w</math> un mot de <math>L</math> de longueur <math>n</math>. Il appartient alors au membre droit de l'équation, mais il n'est pas dans <math>A^{n+1}L</math> parce que tout mot de ce langage a longueur au moins <math>n+1</math> (puisque tout mot de <math>A</math> contient au moins une lettre). Donc le mot <math>w</math> appartient à un autre langage de l'union, donc à <math>A^*B.</math> Ceci prouve que <math>L</math> est contenu dans <math>A^*B</math>, donc l'égalité <math>L=A^*B</math>.

== Application ==
Le lemme d'Arden permet, par la résolution d'un système d'équation par substitution, de déterminer le langage reconnu par un 
[[automate fini]]. On procède comme dans la méthode d'élimination de Gauss : on exprime une variable en fonction des autres, on la remplace par cette expression, on résout le système à une variable de moins, et on explicite la valeur de la variable éliminée.

Soit <math>\mathcal{A} = (Q, \mathcal{F}, I, T)</math> un automate fini sur un alphabet <math>Z</math>. Pour chaque état <math>q \in Q</math>, soit <math>L_q</math> le langage reconnu à partir de l'état <math>q</math>, c'est-à-dire le langage reconnu en prenant <math>q</math> pour état initial. On pose enfin <math>Z_{q,r} = \{a\in Z \mid (q, a ,r) \in T\}</math>. Ce sont les étiquettes de transition de <math>q</math> à <math>r</math>. On a alors :
:<math>L_q =\bigcup_{r \in Q} Z_{q,r}\cdot L_r \cup F_q</math> 
où 
:<math>F_q = \begin{cases}\{\varepsilon\} & q \in F \\ \varnothing & q \notin F \end{cases}</math>

L'application du lemme d'Arden permet alors d'éliminer une à une les inconnues <math>L_q</math> des <math>n</math> équations de la forme précédente, et d'obtenir une expression explicite des <math>L_q</math> et notamment des <math>L_i, i \in I</math> qui permettent de déterminer le langage reconnu par l'automate <math>\mathcal{A}</math>.

Ce même procédé est le fondement de la [[méthode de Brzozowski et McCluskey]], ou de l'[[algorithme de McNaughton et Yamada]].

=== Exemple ===
[[Fichier:DFAexample.svg|alt=Un automate à deux états|thumb|]]
L'automate ci-contre donne le système d'équations :
:<math>\begin{array}{lcl}L_1&=&1L_1\cup 0L_2\cup \varepsilon\\
L_2&=&1L_2\cup 0L_1\end{array}</math>
Le lemme d'Arden donne 
:<math>L_2 = 1^*0 \cdot L_1</math>.
En injectant cette expression de <math>L_2</math> dans l'expression précédente de <math>L_1</math> et en factorisant, on obtient 
:<math>L_1 = (1\cup 01^*0) \cdot L_1 \cup \{\varepsilon\}</math>,
et par application du lemme d'Arden,
:<math>L_1 = (1 \cup 01^*0)^*</math>.

{{Clr}}

== Notes et références ==
=== Références ===
{{Références|références=
<ref name="Arden">
{{chapitre
| langue = en
| auteur1 = Dean N. Arden | titre chapitre = Delayed-logic and finite-state machines
| titre ouvrage = 2nd Annual Symposium on Switching Circuit Theory and Logical Design, (FOCS)|lieu=Detroit, Michigan, USA|date=17-20 octobre 1961
| éditeur = IEEE Computer Society| passage = 133-151|doi=10.1109/FOCS.1961.13}}.</ref>}}

=== Bibliographie ===
* {{Ouvrage
 | langue=fr
 | auteur1=Olivier Carton
 | titre=Langages formels, calculabilité et complexité
 | sous-titre=licence et master de mathématiques ou d'informatique, option informatique de l'agrégation de mathématiques
 | lieu=Paris
 | éditeur=[[Vuibert]]
 | année=2008
 | pages totales=237
 | isbn=978-2-7117-2077-4
 | présentation en ligne=http://www.liafa.jussieu.fr/~carton/Lfcc/
 | id=Carton2008
}}  
* {{Introduction to Automata Theory, Languages, and Computation}}

* {{Ouvrage| auteur=Jacques Sakarovitch| titre=Éléments de théorie des automates<!--| éditeur=Vuibert | année=2003 | isbn=978-2-7117-4807-5-->|titre vo =Elements of Automata Theory|éditeur=Cambridge University Press|année= 2009|isbn=9780521844253|id=Sakarovitch}}

=== Liens externes ===
* {{en}} [https://web.archive.org/web/20110607234020/http://lamp.epfl.ch/~emir/bqbase/2005/01/30/arden.html Sur le site de l'EPFL (École polytechnique fédérale de Lausanne)]

{{Portail|informatique théorique}}

[[Catégorie:Théorème d'informatique|Arden]]
[[Catégorie:Automates finis et langages réguliers]]