Lemme d'itération
En informatique théorique, et spécialement en théorie des langages, un lemme d'itération (pumping lemma en anglais) est un énoncé qui stipule que, dans un langage formel d'une classe particulière, tout mot assez long du langage possède un ou des facteurs qui peuvent être enlevés ou répétés, séparément ou de concert, tout en restant à l'intérieur du langage. Les preuves de ces lemmes utilisent, comme argument de base, le principe des tiroirs. Les principaux résultats sont :
- Lemme d'itération pour les langages rationnels
- Lemme d'itération pour les langages algébriques
- Lemme d'itération pour les langages linéaires
- Lemme d'itération pour les langages indexés
- Lemme d'itération pour les langages réguliers d'arbres
- Lemme d'itération pour les automates quantiques
Les plus importants sont le lemme de l'étoile pour les langages rationnels et le lemme d'itération pour les langages algébriques, parfois appelé improprement le lemme de la double étoile.
Le lemme d'Ogden est une version plus forte du lemme d'itération pour les langages algébriques.
Ces lemmes sont utilisés pour prouver qu'un langage particulier n'est pas dans la classe de langage considérée. Ils ne peuvent pas être utilisés pour vérifier qu'un langage est dans la classe donnée, puisque le lemme ne donne qu'une condition nécessaire, mais pas suffisante d'appartenance.
Bibliographie
- Olivier Carton, Langages formels, calculabilité et complexité, [détail de l’édition] (lire en ligne)