|
Un langage formel est un ensemble de mots, formé sur un alphabet de symboles. La théorie des langages formels est née des préoccupations:
- des logiciens qui souhaitaient définir formellement le discours mathématique
- des linguistes, qui souhaitaient modéliser les langues naturelles,
- des informaticiens qui voulaient spécifier rigoureusement les langages de programmation.
Ces motivations initiales ont conduit à l'élaboration de nouveaux concepts mathématiques tels que les grammaires et les automates qui permettent de définir des langages formels. Des liens entre ces notions et les notions plus classiques de formule logique ou de structure algébrique (celle de semi-groupe notamment) ont été établis.
La théorie s'est ensuite étendue à des objets plus complexes que les mots usuels: les mots infinis, les arbres, les graphes (finis ou infinis), les complexes simpliciaux ...
Pour chaque type de description et d'objet nous cherchons à déterminer quelles propriétés des langages peuvent être calculées et avec quelle efficacité. Un résultat générique, pour ce type de préoccupation serait: étant donné un langage L (présenté par une description finie "D" de taille n), et une propriété P (dans telle classe de propriétés), on peut décider, en temps O(f(n)), si L vérifie P. La comparaison des différentes méthodes de description est aussi un objectif de la théorie. Une question typique est la comparaison entre la classe des langages définissables dans une logique donnée et la classe des langages reconnaissables par une classe de monoïdes ou d'automates donnée.
Cette théorie trouve de nouvelles applications dans des domaines proches de ses origines (linguistique computationnelle, recherche documentaire, par exemple), et s'enrichit régulièrement au contact de problèmes issus d'autres domaines scientifiques: sémantique des processus, modélisation du parallélisme, vérification des systèmes informatiques, théorie des graphes, théorie combinatoire des groupes, topologie, génomique,...
Problèmes étudiés
Voici quelques problèmes particulièrement étudiés dans l'équipe Méthodes Formelles :
- Problèmes d'équivalence d'automates sur les mots; extension à la comparaison de transductions, d'arbres, de graphes.
- Réécriture de mots ou de termes: stratégies de réduction, langage des descendants, terminaison.
- Suites de nombres (entiers ou rationnels) reconnues par des automates à pile de piles ... de piles.
- Langages rationnels dans les monoïdes: reconnaissance par automates, propriétés de clôture, problèmes algorithmiques sur ces langages.
- Caractérisation de propriétés des sous-groupes des groupes libres par des propriétés des automates qui les représentent (représentation de Stallings)
- Semi-commutation et traces de Mazurkiewicz: construction d'automates distribués, problèmes de clôture, problèmes algorithmiques, algèbre et logique.
- Équations dans les monoïdes: problème de la satisfaisabilité, opérations sur les monoïdes conservant la décidabilité des systèmes d'équations, fragments décidables de la logique du premier ordre.
- Résolution du problème du mot dans des sous-monoïdes de monoïdes profinis libres.
- Topologie de monoïdes profinis particuliers: généralisation de propriétés comme celle de Ribes et Zalesskii (un produit de sous-groupes finiment engendrés du groupe libre est fermé pour la topologie profinie).
|
