Description du projet scientifique
CiME est un logiciel
prototype développé à l'origine par Claude Marché pour mettre en
{\oe}uvre en pratique les algorithmes proposés dans sa thèse de
doctorat. L'objectif qui fédère notre groupe est le développement
d'une deuxième version de ce logiciel, qui ne sera plus un système
spécialisé à une application particulière, mais au contraire une «
boîte à outils logicielle », logiciel de type « calcul formel »
fournissant de multiples fonctionnalités liées à la récriture, la
logique équationnelle et la résolution de contraintes, ceci au travers
d'une interface utilisateur basée sur un langage de script général. Au
sein de cette boîte à outils sont ou seront implanté les multiples
méthodes de raisonnement automatique que nous proposons sur le papier,
de manière à faciliter le partage de certains algorithmes, la
réutilisation de ceux-ci, et l'interaction de la boîte à outils avec
d'autres systèmes.
Nous travaillons en collaboration avec quelques chercheurs (citons en
particulier Enno Ohlebusch de l'Université de Bielefeld, Thomas Arts
de la société Ericsson, Albert Rubio de l'Université de Barcelone) qui
souhaitent utiliser notre boîte à outils, et qui jouent pour nous le
rôle important d'utilisateurs testeurs. C'est pourquoi une version
préliminaire de CiME2 est d'ores et déjà disponible par le World
Wide Web, à http://cime.lri.fr/
Les fonctionnalités présentes ou prévues concernent les domaines
suivants :
- Méthodes de résolution des contraintes sur les entiers :
contraintes linéaires, contraintes non-linéaires sur des domaines
finis.
- Algorithmes de filtrage et d'unification de mots et de termes,
modulo des théories équationnelles de base (associativité,
commutativité, groupes abéliens, anneaux booléens).
- Techniques d'automates de mots et d'arbres, opérations ensemblistes,
test de vacuité, comptage du cardinal du langage reconnu.
- Systèmes de récriture de mots, test de confluence, complétion à
la Knuth-Bendix, calculs des langages de formes normales.
- Systèmes de récriture de termes, modulo associativité et/ou
commutativité, tests de confluence, complétions AC ou normalisée.
- Vérification ou recherche de preuve de terminaison de systèmes,
critères de paires de dépendances, collections d'ordres pour la
terminaison, techniques incrémentales.
- Familles de systèmes de récriture indexées par un ou plusieurs
entiers et contraintes entières, preuves uniformes de confluence et
de terminaison.
Ces deux derniers points concernent des méthodes qui sont actuellement
en cours d'étude théorique, dans le cadre des thèses de Xavier Urbain
et Benjamin Monate respectivement. L'implantation est donc en cours ou
à venir.
Enfin, nous souhaitons à l'avenir utiliser ces fonctionnalités comme
bases pour développer encore de nouvelles techniques. Les paragraphes
qui suivent donnent la liste des perspectives que nous avons en vue
actuellement.
Perspective 1 : Vérification de calculs communicants
concurrents
Thomas Arts, chercheur au sein de la société Ericsson, travaille sur
la vérification de processus communicants concurrents et modélise ces
processus par des systèmes de récriture de manière à ce que la
propriété de progression (c.-à-d. non-blocage) des
communications se traduise par la terminaison du système de récriture
associé. Ces traductions produisent des systèmes de plusieurs
milliers de règles, et nous voulons étudier si les techniques
incrémentales proposées par Xavier Urbain~\cite{urbain01ijcar}
peuvent être utiles.
Ce travail devra se matérialiser par l'implantation d'un traducteur du
langage de spécification muCRL~(http://www.cwi.nl/~mcrl) vers
la notation CiME.
Perspective 2 : Preuves de terminaison de programmes
logiques ou fonctionnels
Nous avons déjà étudié, en collaboration avec Enno Ohlebusch et Claus
Claves de l'université de Bielefeld, des méthodes de preuve de
terminaison de programmes logiques~\cite{ohlebusch00rta}. Cette étude
a donné lieu à un système implanté (TALP) qui utilise une des
procédures de preuve de terminaison de la version prototype actuelle
de la boîte à outils CiME. Sur des exemples classiques
de programmes logiques, les résultats obtenus sont tout à faits
compétitifs par rapport à des systèmes de preuve de terminaison
dédiés. Le passage à des programmes de grande taille sera étudié dès
que les critères incrémentaux mentionnés précédemment seront
parfaitement maîtrisés et implantés dans CiME.
Dans l'avenir, nous souhaitons trouver un codage analogue pour le cas
de la programmation fonctionnelle (à la ML). Nous envisageons de
proposer ce sujet comme stage de DEA, prolongé probablement en une
thèse. Si une telle méthode fonctionne de manière satisfaisante on
pourrait envisager dans l'avenir d'adjoindre à un compilateur comme
celui du langage CAML un outil de vérification de terminaison.
Perspective 3 : Familles paramétrées de systèmes de
règles
Il s'agit de familles de systèmes, indexées par un ou plusieurs
entiers, et pour lesquels on cherche à établir les propriétés
essentielles comme la terminaison mais aussi la confluence, ainsi que
le dénombrement des formes irréductibles, de manière uniforme pour
tous les systèmes de la famille.
Une motivation importante de ce travail est son application à certains
problèmes de physique théorique~\cite{contejean00rta}, et plus généralement le
sujet de la récriture paramétrée est depuis longtemps posé dans la communauté
scientifique du domaine, mais sur lequel il n'y a jamais eu pour l'instant de
résultats significatifs.
Le travail en cours est limité à des systèmes de récriture de mots.
Nous recherchons à établir un algorithme de vérification de la
confluence dans le cas où les contraintes utilisées dans l'indexation
sont linéaires. Dans l'avenir, pour le cas de contraintes non
linéaires, nous savons d'ores et déjà qu'un tel algorithme n'existe
pas car ce problème est indécidable, mais nous voudrions obtenir tout
de même une méthode suffisamment puissante pour traiter la classe des
problèmes rencontrés dans les applications en physique théorique.
À l'heure actuelle, un algorithme de vérification de la confluence est déjà
implanté dans la boîte à outils CiME2 pour des systèmes non paramétrés, et
nous nous en servons expérimentalement en l'appliquant à des systèmes d'une
famille exemple pour des valeurs particulières de plus en plus grandes des
paramètres, dans l'espoir de découvrir des régularités. À cette occasion nous
avons mis en place une technique de parallélisation de cet algorithme, qui
peut être utilisée pour d'autres cas.
Dans l'avenir, il nous faudra aussi être capable de prouver la terminaison des
systèmes de la famille considérée de manière uniforme. Mais surtout, il existe
des applications potentielles qui ne peuvent pas être traitées par des règles
de récriture de mots comme pour les groupes, qui nécessitent de généraliser
les algorithmes au cas de la récriture d'arbres.
Perspective 4 : Interface avec l'assistant de preuve COQ
Le logiciel d'aide à la preuve COQ
(http://pauillac.inria.fr/coq/coq-fra.html) est un outil
développé en partie par des membres de l'équipe DÉMONS du LRI (en fait
depuis l'arrivée de Christine Paulin dans l'équipe en 1997). Les
points forts d'un tel système sont d'une part un langage de
spécification très puissant, permettant en particulier d'exprimer dans
un même formalisme des assertions logiques et des programmes, et donc
des propriétés souhaitées de ces programmes ; et
d'autre part une procédure de vérification (c.-à-d. de test si une
preuve est correcte) très sûre. Par contre un point faible est le
manque d'automatisation dans la recherche d'une preuve.
Du fait de la proximité de COQ et CiME : développeurs dans une même
équipe, même langage d'implantation, il est très naturel de vouloir
utiliser des procédures automatiques de CiME (existantes ou bien à
ajouter), pour aider à la recherche de preuve en COQ. Plusieurs axes
sont possibles, tous nécessitant néanmoins une étude théorique
préalable.
Un premier axe est d'extension des méthodes du premier
ordre de CiME à l'ordre supérieur, pour pouvoir traiter toute la
puissance du langage de COQ. Evelyne Contejean s'est particulièrement
investie dans ce thème depuis trois ans.
Un deuxième axe est l'utilisation des techniques de terminaison de
CiME pour construire des définitions de fonctions en COQ : si de
telles définitions se font naturellement dans le langage COQ par
récurrence structurelle, dès qu'une fonction ne se définit plus
naturellement de cette façon, la tâche est bien plus
ardue et nécessite des obligations de preuve de la part de
l'utilisateur. Un tel axe nécessite au préalable de prouver les
critères de terminaison utilisés par CiME au sein du système
COQ. Sur un tel sujet on souhaiterait proposer un stage de DEA
poursuivi en une thèse.
Un troisième axe est l'utilisation de la récriture, en particulier
associative-commutative, pour permettre à COQ de raisonner
automatiquement sur des égalités qui, bien que de l'ordre du calcul
pour un être humain, demande actuellement à l'utilisateur COQ d'en
établir la preuve à chaque pas de récriture.