Projet CiME, action incitative jemSTIC C.N.R.S.

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 : 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.