Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
[go: Go Back, main page]


Activités antérieures d'enseignement, de recherche, et de responsabilité collective


Claude Marché

1   Activités d'enseignement

1985 et 1986

Deux stages pédagogiques d'un mois en première S et terminale C, en cours de mathématiques, au lycée Lakanal de Sceaux et au lycée Pascal d'Orsay.

1989-1990

Première année de monitorat à Orsay, service de 64h eqTD.

Travaux dirigés et travaux pratiques d'initiation au langage PASCAL, en MIAGE et en DESS (professeur  : Brigitte Rozoy). J'ai réalisé à cette occasion un polycopié d'initiation au PASCAL, adapté au système d'exploitation sur lequel on travaillait (VMS), destiné aux grands débutants.

1990-1991

Deuxième année de monitorat à Orsay, service de 64h eqTD.

Travaux dirigés et travaux pratiques d'initiation au langage PASCAL

Travaux dirigés d'algorithmique, en MIAGE première année (professeur : Michèle Soria). Le programme d'algorithmique contenait les algorithmes de recherche (dichotomie, par arbres binaires, hachage), les algorithmes de tri, et algorithmes de recherche de mots dans un texte. Ce cours a été sanctionné par un examen théorique et un projet (comptage du nombre d'occurrences de chaque mot dans un texte).

1992-1993

Troisième année de monitorat à Orsay, service de 64h eqTD.

Travaux dirigés du certificat calculabilité de la maîtrise de Mathématiques (professeur : Laurence Puel). Le programme comporte la théorie des langages formels, le l-calcul, le typage, et des notions de base de logique, ainsi que l'utilisation du langage fonctionnel CAML-light comme application.

1994-1995

ATER à l'ENS de Cachan, service d'enseignement de 192 heures statutaires.

1995-1996

Maître de Conférences Stagiaire, service d'enseignement de 192 heures statutaires et de 25.5 heures complémentaires.

1996-1997

Maître de Conférences Titulaire, service d'enseignement de 192 heures statutaires et de 42 heures complémentaires.

De plus, cette année j'ai été tuteur du moniteur de première année Quentin El-Haik. Les modules Principes d'Interprétation des Langages et Étude de cas Langages et Génie Logiciel étaient des cours entièrement nouveaux mis en place dans le cadre de la nouvelle formule du DEUG MIAS. La mise en place de ces cours a été coordonnée avec Jean-Pierre Jouannaud et Ralf Treinen pour le module PIL, avec réalisation d'un poly de cours de plus de cent pages ; et avec Ralf Treinen pour le module LGL, avec la réalisation d'un poly de mise à niveau en CAML d'une soixantaine de pages.

1997-1998

Service d'enseignement de 192 heures statutaires.

Cette année-là, j'ai été tuteur du moniteur de deuxième année Quentin El-Haik.

Avec Ralf Treinen et Benjamin Monate, nous avons mis en place un serveur sous Linux sur les ordinateurs du parc informatique du première cycle, destiné aux TP d'Informatique de DEUG MIAS. Réseau d'une centaine de machines à gérer. Pour cette première année, seuls les modules PIL et LGL avaient des TP sous Linux, ce qui représente une centaine de comptes utilisateurs à gérer.

1998-1999

Service d'enseignement de 192 heures statutaires (dont 30h de décharge) et de 13.2 heures complémentaires.

APOGÉE (Application POur la Gestion des Étudiants et des Enseignements) est un nouvel outil informatique mis en place cette année à l'université Paris 11, et je me suis chargé de la tâche de correspondant Apogée pour le département d'Informatique. J'ai mis en place dans la base de données APOGÉE les structures des enseignements jusqu'au niveau des unités d'enseignements capitalisables pour la Licence-Maîtrise et le C4/DU d'informatique. Édition des PV de jury pour la Licence-Maîtrise, La MIAGE (IUP et CFA), le C4/DU d'informatique, les DESS SCHM et II. Et j'ai assisté les secrétaires pédagogiques pour la saisie de s notes et l'édition des PV de jury.

Cette année, j'ai été aussi tuteur du moniteur de première année Benjamin Monate, tâche pour laquelle j'ai obtenu 4h de décharge l'année suivante.

Enfin, j'ai poursuivi ma tâche de gestion du serveur Linux des machines de TP du premier cycle, avec la mise à jour du serveur et du réseau, et toujours la gestion des comptes utilisateurs et de leurs environnements. Pour cette année, le module S1 avait des TP sous Linux. Vu le nombre d'étudiants (450), nous avons travaillé avec un compte partagé.

1999-2000

Service d'enseignement de 192 heures statutaires (dont 38h de décharge) et de 24.58 heures complémentaires.

En tant que correspondant Apogée pour le département d'Informatique : Mise à jour des structures des enseignements pour la Licence-Maîtrise et le C4/DU d'informatique. Mise en place des structures des enseignements jusqu'au niveau des unités d'enseignements capitalisables pour la MIAGE (IUP et CFA) et les DESS SCHM et II. Édition des PV de jury pour la Licence-Maîtrise, La MIAGE (IUP et CFA), le C4/DU d'informatique, les DESS SCHM et II, ainsi le PV de diplôme final de la NFI FIIFO.

Avec Ralf Treinen et Benjamin Monate, nous avons poursuivi la tâche de gestion du serveur Linux des machines de TP du premier cycle. Cette année a vu la mise en place de TP sous Linux en S@, avec plus de 200 comptes à gérer.

2000-2001

Service d'enseignement de 192 heures statutaires (dont 34h de décharge) et de 0.7 heures complémentaires.

De plus, j'ai assuré la coordination de tous les groupes de TER Génie Logiciel de Licence d'Informatique et de MIAGE IUP2.

En tant que correspondant Apogée, j'ai de nouveau assuré la mise à jour des structures des enseignements pour les filières du département. Pour la MIAGE, la structure des enseignements a été complétée pour descendre jusqu'au niveau des matières. Et j'ai continué à assister les secrétaires pédagogiques pour la saisie de s notes et l'édition des PV de jury.

Avec Ralf Treinen et Benjamin Monate, nous avons poursuivi la tâche de gestion du serveur Linux des machines de TP du premier cycle. Les TP de S1, S2, S3 PIL et S4 LGL se sont déroulés sous Linux. Pour cette tâche, cette année, Ralf Treinen et moi avons partagé une prime pédagogique.

2001-2002

Service d'enseignement de 192 heures statutaires (dont 34h de décharge) et de 13.67 heures complémentaires.

De plus, j'assure la coordination de tous les groupes de TER Génie Logiciel de Licence d'Informatique et de MIAGE IUP2, ainsi que la mise en place de l'utilisation du logiciel Rational Rose pour ce TER.

Ma tâche de coordination des TP sous Linux de DEUG est cette année matérialisée par 5h eqTD.

2   Activités d'administration et autres tâches d'utilité collective

Activités liées à l'enseignement

Organisation (avec Alain Denise, Laurence Devillers et Nathalie Drach) du stand du département d'Informatique à la journée portes ouvertes du centre d'Orsay de l'université Paris 11, au printemps 1996.


Organisation (avec Alain Denise, Rachid Gherbi et Ralf Treinen) du stand du département d'Informatique à la journée portes ouvertes du centre d'Orsay de l'université Paris 11, au printemps 1997.


Depuis l'année universitaire 1997-1998, avec Ralf Treinen et Benjamin Monate, j'ai participé à la mise en place puis à la maintenance d'un serveur sous le système d'exploitation Linux, au sein du parc informatique du premier cycle (bâtiment 336). Ce serveur permet à la centaine de PC sans disque de ce parc de démarrer sous Linux. Les TP d'informatique de DEUG MIAS se sont alors déroulés sous Linux. Au total, chaque année cela représente plusieurs centaines de comptes utilisateurs à gérer, avec les problèmes classiques d'oubli de mot de passe, de dépassement de quota disque, etc.


Depuis le mois de juin 1998, je suis chargé de la tâche de correspondant Apogée (Application POur la Gestion des Étudiants et des Enseignements) pour le département d'Informatique. Je me suis chargé de saisir puis de mettre à jour dans la base de données Apogée les structures des enseignements des différentes filières du département : Licence-Maîtrise, MIAGE (IUP et CFA), le C4/DU d'informatique, les DESS SCHM et II, la FIIFO. L'utilisation d'Apogée pour l'obtention des procès verbaux de diplôme nécessite également de saisir les modalités de collecte (règles de conservation de note, de capitalisation d'unité, etc.), les règles de calcul de notes et de résultats pour toutes ces filières. Enfin, l'utilisation de cette base de données posant très régulièrement des difficultés, j'ai consacré beaucoup de temps à assister les secrétaires pédagogiques pour les saisies d'inscriptions pédagogiques, les saisies des notes, les calculs de notes et de résultats et enfin l'édition tant attendue des PV de jury.


Enfin, je me suis régulièrement occupé ces dernières années de la gestion de pages web pour les enseignements (notamment pour la mise à disposition des énoncés et des corrigés de TD/TP), en DEUG (modules S1, PIL, LGL) et en Licence d'Informatique (TER de Génie Logiciel).

Activités liées à la recherche

Organisation locale, avec Ralf Treinen, de l'école d'été CCL'99 (http://www.lri.fr/~ccl99/) et Workshop CCL'99 (http://www.lri.fr/~treinen/ccl/workshops/ccl99/) ; qui ont eu lieu respectivement du 5 au 8 septembre et du 9 au 10 septembre 1999, à Gif-sur-Yvette. Cette école et ce workshop étaient organisés dans le cadre du projet Esprit européen CCL2 (http://www.ps.uni-sb.de/ccl/). Les notes de cours de l'école ont été édités (éditeurs : Hubert Comon, Claude Marché et Ralf Treinen) chez Springer-Verlag dans les Lecture Notes in Computer Science [7].


Membre du comité de programme de la 25ème conférence internationale Mathematical Foundations of Computer Science, qui s'est déroulée du 28 août au 1er septembre 2000 à Bratislava (Slovaquie).


Encadrement de stages, DEA et thèses :


Parmi les autres tâches mineures dont je me suis occupé, on peut citer :

Divers

Pour mes besoins personnels, d'une part pour la production de pages Web, d'autre part pour l'écrire de la documentation de programmes CAML (CiME en particulier), je me suis impliqué dans des projets logiciels existants :

3   Activités de Recherche

Mon travail se situe à l'interface de l'informatique et des mathématiques. Mon domaine est la preuve automatique, soit de théorèmes mathématiques, soit de programmes informatiques, à l'aide d'un ordinateur. Les méthodes qui m'intéressent peuvent être parfois entièrement automatisées, quand il s'agit de domaines très spécifiques ; et d'autre fois combinent l'automatisation et l'interaction avec l'utilisateur, ce qu'on appelle une preuve assistée, preuve qui sera dans tous les cas vérifiée par l'ordinateur.

Plus spécifiquement, je me suis beaucoup concentré sur le traitement mécanisé d'axiomatiques spécifiées par des systèmes d'équations. L'importance des équations en mathématiques est connue : elles permettent de définir axiomatiquement les structures algébriques classiques comme les monoïdes, les groupes, les espaces vectoriels ou les algèbres. Elles sont également fondamentales en informatique : langages de programmation de haut niveau (programmation logique avec égalité, programmation fonctionnelle), spécifications algébriques (types abstraits), prototypage, l-calcul (logique des combinateurs), calcul symbolique formel, optimisation de code, inférence de type, géométrie algorithmique, etc.

Dans une première partie, je vais décrire les travaux qui ont concerné ma thèse de doctorat et un peu après, qui se concentrent, d'un point de vue théorique sur l'algorithme de complétion dite normalisée, et d'un point de vue appliqué, sur le logiciel CiME dans sa première version, distribuée en 1996 [9].

Dans une seconde partie, je vais décrire mes travaux plus récents, qui s'inscrivent dans un spectre plus large.

4   La complétion normalisée, le logiciel CiME version 1

Le calcul avec des équations passe traditionnellement par leur orientation en règles de réécriture, par exemple pour les utiliser comme méthode de simplification. On utilise alors ces règles pour réduire les expressions jusqu'à obtenir des formes normales (c-à-d irréductibles). Savoir si une règle peut être appliquée à une expression est l'enjeu du processus de filtrage, c'est-à-dire de la recherche de motifs. Deux grands types de problème se posent en réécriture : le premier est celui de la terminaison, autrement dit comment s'assurer que la réduction par les règles s'arrête en temps fini sur une forme normale. Ce type de problème se traite traditionnellement par l'utilisation d'ordres de réduction. Le second type de problème est celui de la confluence, c'est-à-dire de l'unicité du résultat quel que soit l'ordre d'application des règles. On traite le problème de la confluence en analysant les ambiguïtés possibles, ce qui passe par l'unification des membres gauches de règles, de manière à déterminer les expressions pouvant être instances de plusieurs règles à la fois.

Lorsqu'une axiomatique nous est donnée sous la forme d'un ensemble d'équations, nous cherchons donc à les orienter en règles, en choisissant pour membre gauche le plus grand des deux membres de l'équation pour un ordre de réduction donné. Si le système obtenu n'est pas confluent, on est amené à introduire de nouvelles équations (les paires critiques) : il s'agit là du processus de complétion, introduit en 1970 dans un fameux article de Knuth et Bendix [17], qui l'appliquait à la théorie des groupes.

Malheureusement, certains groupes d'axiomes, comme les axiomes permutatifs (la commutativité en particulier), ne peuvent pas être orientés en des règles de réécritures sans perdre la propriété essentielle de terminaison. Pour s'affranchir de ce problème, Peterson et Stickel [29] en 1981 ont proposé d'intégrer la commutativité dans le processus de réduction par l'utilisation du filtrage modulo commutativité. De plus, l'équation d'associativité n'étant à son tour plus orientable modulo commutativité, on a besoin également du filtrage associatif-commutatif. Le problème de la terminaison doit alors être traité à l'aide d'ordres de réductions compatibles avec l'associativité et la commutativité. Au niveau du test de confluence, ou dans l'algorithme de complétion du calcul des paires critiques, cela demande l'utilisation de l'unification associative-commutative.

Cette technique de réécriture modulo AC (associativité et commutativité) a ensuite été généralisée à une théorie E arbitraire sous les conditions que d'une part il existe des ordres de réduction non triviaux (c-à-d différents de l'égalité) compatibles avec E, et que d'autre part l'unification modulo E soit décidable et finitaire [12, 2]. Ces conditions sur la technique générale de réécriture modulo E excluent des cas fondamentaux très simples pour E : identité (x.1=x), inverse (x.x-1=1), idempotence (x.x=x), théorie des groupes, des anneaux.

Le cas des anneaux représente un enjeu pourtant particulièrement important car il est lié à un algorithme bien connu dans le domaine du calcul algébrique formel : le calcul des bases standard d'idéaux de polynômes. Un certain nombre de chercheurs avaient déjà remarqué que cet algorithme s'apparentait avec l'algorithme de complétion de Knuth et Bendix [15, 5, 6] mais le problème de pouvoir les considérer comme deux instances particulières d'un seul et même algorithme restait ouvert. Une analyse de l'algorithme de calcul de bases standard montre que pour considérer cet algorithme comme un algorithme de complétion modulo une certaine théorie E, il faudrait prendre pour E la théorie définie par l'anneau de base, celui dans lequel vivent les coefficients des polynômes. Or justement une telle théorie ne satisfait pas les conditions voulues. Ma thèse a donné une réponse à ce problème, grâce à une nouvelle technique dite de complétion normalisée, que je vais détailler dans la suite.

En 1989, Peterson, Baird et Wilkerson [3] ont proposé une méthode pour faire de la réécriture modulo ACU (associativité, commutativité et unité) par l'utilisation de la réécriture contrainte [16]. Pour mon stage de DEA, j'ai donné un algorithme de complétion adapté au cas de E=ACU, ce qui a nécessité d'introduire un nouveau type d'inférence en plus de l'orientation et du calcul de paires critiques : le calcul des instances critiques. Ce travail mené conjointement avec Jean-Pierre Jouannaud a fait l'objet d'une publication dans le journal Theoretical Computer Science (numéro 1 dans la liste de publications jointe) [13, 14]. Cette approche n'a malheureusement pas pu s'appliquer telle quelle aux autres cas précités.

L'idée qui a guidé mon travail a été d'étudier le fonctionnement de l'algorithme de calcul des bases standard d'idéaux de polynômes. En s'inspirant du travail sur la complétion ACU contrainte et sur ce qui serait nécessaire pour traiter le cas des bases standard, nous avons introduit une nouvelle notion de réécriture, la réécriture normalisée, dont l'idée fondamentale est que l'on doit réduire uniquement les expressions en forme normale pour la théorie E, ce qui nécessite de présenter E par un système de réécriture S qui soit convergent (c-à-d qui termine et qui soit confluent). Les résultats obtenus font partie de ma thèse [22] et se résument en quatre grands points :

  1. Introduction de la réécriture normalisée modulo S, où S est un système convergent (modulo AC éventuellement). La réduction a lieu uniquement sur les formes normales pour S. J'ai montré que cette réduction englobe le cas de la réécriture modulo AC habituelle (S=Ø), la réécriture ACU contrainte (S=ACU), mais également la réduction des polynômes telle qu'on la trouve dans le calcul des bases standard sur Z (S=CR, théorie des anneaux commutatifs), ou sur les corps finis (S=FF(p), corps fini à p éléments). Le résultat fondamental est que pour montrer la terminaison de la réécriture normalisée modulo S, on n'a pas besoin d'un ordre de réduction compatible avec S, mais avec AC seulement.

  2. Description de l'algorithme de complétion normalisée général, pour un S arbitraire. Cet algorithme utilise le calcul des couples normalisants (généralisation de la notion d'instances critiques introduite pour le cas ACU). Le résultat fondamental est le théorème de complétude. Le calcul des couples normalisants est suffisamment paramétrique pour pouvoir obtenir une complétion très efficace dans certain cas, en particulier dans le cas des groupes et des anneaux commutatifs, ceci par l'utilisation de la technique de symétrisation, inspirée du travail de Le Chenadec [19].

  3. Résultats de terminaison de la complétion pour certaines classes de théories. La terminaison de la complétion modulo AC lorsque les équations à compléter sont sans variables, était connue depuis 1991 [27, 20]; et d'autre part, la terminaison des algorithmes de calcul de bases standards était connue depuis leur existence. J'ai montré par une méthode uniforme la terminaison de la complétion normalisée close modulo S dans toute une famille de théories S (Ø, C, AC, ACU, ACI, ACI1, AG, CR, BR, FF(p)), résultats qui contiennent donc les résultats précédents. Une conséquence importante est la décidabilité de l'égalité pour toutes les théories définies par des équations closes arbitraires plus l'une quelconque des théories précédentes. Enfin, j'ai montré au contraire un résultat d'indécidabilité de l'égalité modulo une théorie close plus les axiomes d'associativité, de commutativité et de distributivité qui a été publié indépendamment dans International Journal of Foundations of Computer Science (numéro 2 dans la liste de publications jointe) [21].

  4. Implantation de la complétion normalisée : j'ai réalisé un prototype appelé CiME, qui a été et est toujours disponible par le Web (http://cime.lri.fr) et qui permet de compléter des théories en travaillant modulo un choix de théories S possibles, ce qui donne un logiciel paramétrique pouvant faire aussi bien de la complétion de Knuth-Bendix (S=Ø), de la complétion associative-commutative (S=AC) ou du calcul de bases standards (S=CR, S=FF(p)), de la complétion ACU contrainte Jouannaud-Marché (S=ACU, et d'autres complétions nouvelles : modulo idempotence (S=ACUI utile pour définir les ensembles), les groupes (S=AG), les anneaux booléens (S=BR), etc.
Mes travaux de thèse ont été ensuite publiés dans les actes de la conférence LICS'94 [23], puis dans une version complète et améliorée, dans le Journal of Symbolic Computation [24]. Les améliorations en question concernent en particulier un résultat technique sur l'algorithme d'unification modulo une théorie, travail réalisé avec Alexandre Boudet et Evelyne Contejean et publié dans les actes de la conférence RTA'96 [4]. Dans le même temps, le prototype CiME de ma thèse est devenu un logiciel distribué (http://cime.lri.fr) et nous en avons fait une démonstration lors de cette même conférence [9].

5   La preuve automatique de terminaison, la réécriture paramétrée, CiME version 2

À partir de l'année 1996 approximativement, j'ai commencé à élargir mon spectre d'activités de recherche, mais en gardant toujours un fil conducteur, qui a été l'implantation des nouvelles méthodes et algorithmes de preuve décrits en théorie. Pour ce faire, j'avais souhaité utiliser le logiciel CiME comme base de départ, mais pour qu'une nouvelle méthode inventée soit facilement implantable dans CiME, il a été nécessaire de revoir complètement l'interface utilisateur de CiME. En fait, ce logiciel, spécialisé au départ dans la complétion normalisée, est devenu une véritable « boîte à outils logicielle », que l'on a appelée CiME2 [10]. L'interface utilisateur est devenue très proche d'un logiciel de type « calcul formel » fournissant de multiples fonctionnalités par l'intermédiaire de fonctions prédéfinies, formant une collection aisément extensible.

Mes activités de recherche qui suivent, soutendues par l'implantation dans CiME, ont alors grosso-modo correspondu à l'encadrement scientifique d'étudiants en thèse, et on concerné deux thèmes principaux.

Le premier thème est celui de la terminaison : il s'agit de montrer qu'un processus de calcul donné va s'arrêter en temps fini quels que soient les paramètres qu'on lui donne en entrée.

Le second thème est celui de la réécriture dite paramétrée : il s'agit d'étudier des familles de processus de calcul par règles de réécriture, familles indexées par des paramètres entiers, et de chercher à établir des propriétés de ces processus de manière uniforme pour toute la famille ainsi considérée.

5.1   Preuve automatique de terminaison

Il existe deux aspects tout à fait différents de la recherche sur le thème de la terminaison. Le premier consiste à rechercher des techniques mathématiques nouvelles afin de résoudre des conjectures difficiles, dont certaines sont très célèbres comme le problème de Syracuse : à partir d'un nombre entier x0 arbitraire, on calcule la suite définie par
xn+1 = xn/2 si xn est pair
xn+1 = 3xn+1 sinon
La conjecture affirme que l'on obtient toujours 1 au bout d'un nombre fini d'étapes, par exemple en partant de 7 :
  7 ® 22 ® 11® 34® 17 ® 52® 26® 13® 40
    ® 20® 10 ® 5 ® 16® 8 ® 4 ® 2 ® 1

Mais l'aspect qui m'intéresse n'est pas celui-là. Au contraire, je m'intéresse à des problèmes de terminaison qui seraient considérés plutôt comme « faciles » pour un chercheur spécialiste en preuve de terminaison. Il s'agit de programmes (ou plus abstraitement de processus de calcul) dont le programmeur souhaite vérifier la terminaison, afin de garantir la correction de ces programmes. On souhaite ainsi que de telles preuves soient établies automatiquement par un logiciel de vérification. Dans cette optique, l'objectif n'est pas de prouver la terminaison pour des cas difficiles, mais de prouver automatiquement par ordinateur la terminaison dans des cas que l'on rencontre dans la pratique courante de la programmation.

Parmi les classes de processus dont on souhaite prouver la terminaison, les systèmes de réécriture jouent un rôle central. En effet, ils forment à la fois un formalisme très simple et générique (remplacement syntaxique d'expressions par d'autres) et universel (toute machine de Turing peut être codée par un système de règles de réécriture). Aussi, il est important dans un premier temps de construire des algorithmes de preuves de terminaison pour les systèmes de réécriture. Ensuite, les preuves de terminaison pour d'autres classes de formalismes de calcul s'opèrent par un codage préalable en système de réécriture, codage devant préserver la terminaison.

Des algorithmes permettant d'établir automatiquement la terminaison de systèmes de réécriture peuvent être utilisés directement dans des environnements de spécification et vérification de programmes basés sur la logique équationnelle : OBJ, CafeOBJ, Maude, etc...

L'approche que j'ai utilisé maintenant pour construire de tels algorithmes est basée sur la séparation en étapes bien distinctes indiquées figure 1, la correction de chacune de ces étapes pouvant être prouvées indépendemment. Cette structure se retrouve exactement dans l'implantation dans CiME.


Figure 1: Étapes d'une preuve automatique de terminaison

La première étape est la phase de codage dont on voit un exemple ci-après pour la programmation logique. La deuxième étape consiste à voir un critère de terminaison comme une transformation qui à un système de réécriture donné associe des contraintes de terminaison, la satisfiabilité de ces contraintes entraînant la terminaison du système de départ. La troisième étape est le résolveur, qui à partir des contraintes recherche un ordre bien fondé qui les rende vraies. Une quatrième étape, qui peut sembler superflue au premier abord mais s'avère très importante en pratique, est une vérification : à partir de contraintes de terminaison et d'un ordre bien fondé, elle vérifie que cet ordre valide effectivement les contraintes. Cette dernière étape est utile pour une question de sûreté : il est en effet beaucoup plus facile de vérifier que de résoudre, et il est difficile de faire entièrement confiance aux algorithmes de résolution qui requièrent des codes complexes et volumineux. De plus, la vérification est beaucoup moins coûteuse en temps de calcul et en pratique une fois qu'un ordre à été trouvé prouvant la terminaison d'un système, on en garde la trace.

Amélioration des critères de terminaison
En 1997, Arts et Giesl ont découvert un nouveau critère de terminaison, dit des paires de dépendances [1]. Ce critère s'est avéré très intéressant car à la fois facilement automatisable et suffisamment puissant pour traiter de nombreux cas concrets qu'il n'était pas possible de traiter auparavant. Avec Xavier Urbain, j'ai proposé [25, 18] des généralisation de ce critère à la réécriture modulo associativité et commutativité.

L'étape suivante, qui fait l'objet de la thèse de Xavier Urbain [30], a eu pour objectif de traiter des systèmes de réécriture de grande taille. Nous avons proposé un critère qui s'applique à des systèmes présentés modulairement, pour lesquels il est très important de pouvoir prouver la terminaison de manière incrémentale. Ce travail est essentiel pour permettre le « passage à l'échelle » de cette technique, et donc sa large application au sein des systèmes de spécifications mentionnés précédemment. Xavier a ensuite implanté cette méthode dans CiME, et comme exemple convaincant il a réussi à prouver automatiquement la terminaison d'un système issu d'une modélisation µ-CRL de processus communicants --- système proposé par Thomas Arts, chercheur chez Ericsson --- comportant environ quatre cents règles, et formant une hiérarchie d'une cinquantaine de modules.

Lors de l'application pratique de ces techniques, on constate très vite que la phase de résolution des contraintes est la plus coûteuse en complexité, mais aussi incomplète, car la satisfiabilité de ces contraintes est indécidable. Les algorithmes se proposent de rechercher un ordre vérifiant les contraintes au sein d'une classe particulière d'ordre. La plus utilisée et la plus maîtrisée à l'heure actuelle est la classe des ordre récursifs sur les chemins. Nous avons travaillé, Avec Evelyne Contejean, Ana-Paola Tomàs et Xavier Urbain, sur la résolution de contraintes de terminaison dans le cas des ordres basés sur les interprétations polynomiales [11] et dans le futur il sera nécessaire de l'étendre en particulier au cas des interprétations exponentielles, mais aussi à la recherche d'ordre construit par les méthodes de filtrage des arguments (AFS), et plus généralement de schéma de programme récursif (RPS).

Comme mentionné précédemment, l'application des techniques de preuve de terminaison de la réécriture à d'autres formalismes de calcul passe par la construction de codages préservant la terminaison. En 2000, j'ai étudié avec Enno Ohlebusch et Claus Claves, de l'université de Bielefeld, le cas de la programmation logique [28] et cette étude a donné lieu à un système implémenté (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.

5.2   Systèmes de réécriture paramétrés

Il s'agit en fait de classes 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. Ce travail est une collaboration avec Evelyne Contejean (chargée de Recherche CNRS) et Benjamin Monate (étudiant en thèse). Il se poursuit encore actuellement.

Une motivation importante de ce travail est son application à certains problèmes de physique théorique [8], 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, avant la thèse de Benjamin Monate [26], de résultats significatifs.

Le travail déjà réalisé est limité à des systèmes de réécriture de mots, qui forment des présentations de groupe. Des algorithmes de vérification de la confluence ont été décrit et prouvés dans le cas où les contraintes utilisées dans l'indexation sont linéaires. Ces algorithmes sont implantés dans la boîte à outils CiME2, et en cours de test depuis janvier 2002.

References

[1]
Thomas Arts and Jürgen Giesl. Termination of term rewriting using dependency pairs. Theoretical Computer Science, 236:133--178, 2000.

[2]
Leo Bachmair and Nachum Dershowitz. Completion for rewriting modulo a congruence. Theoretical Computer Science, 67(2&3):173--201, October 1989.

[3]
Timothy Baird, Gerald Peterson, and Ralph Wilkerson. Complete sets of reductions modulo Associativity, Commutativity and Identity. In Proc. 3rd Rewriting Techniques and Applications, Chapel Hill, LNCS 355, pages 29--44. Springer-Verlag, April 1989.

[4]
Alexandre Boudet, Evelyne Contejean, and Claude Marché. AC-complete unification and its application to theorem proving. In Harald Ganzinger, editor, 7th International Conference on Rewriting Techniques and Applications, volume 1103 of Lecture Notes in Computer Science, pages 18--32, New Brunswick, NJ, USA, July 1996. Springer-Verlag.

[5]
Bruno Buchberger. History and basic features of the critical pair / completion procedure. Journal of Symbolic Computation, 3(1), February 1987.

[6]
Reinhard Bündgen. Simulating Buchberger's algorithm by a Knuth-Bendix completion procedure. In Ronald. V. Book, editor, 4th International Conference on Rewriting Techniques and Applications, volume 488 of Lecture Notes in Computer Science, Como, Italy, April 1991. Springer-Verlag.

[7]
Hubert Comon, Claude Marché, and Ralf Treinen, editors. Constraints in Computational Logics, volume 2002 of Lecture Notes in Computer Science. Springer-Verlag, 2001.

[8]
Evelyne Contejean, Antoine Coste, and Benjamin Monate. Rewriting techniques in theoretical physics. In Leo Bachmair, editor, 11th International Conference on Rewriting Techniques and Applications, volume 1833 of Lecture Notes in Computer Science, pages 80--94, Norwich, UK, July 2000. Springer-Verlag.

[9]
Evelyne Contejean and Claude Marché. CiME: Completion Modulo E. In Harald Ganzinger, editor, 7th International Conference on Rewriting Techniques and Applications, volume 1103 of Lecture Notes in Computer Science, pages 416--419, New Brunswick, NJ, USA, July 1996. Springer-Verlag. System Description available at http://cime.lri.fr/.

[10]
Evelyne Contejean, Claude Marché, Benjamin Monate, and Xavier Urbain. Cime version 2, 2000. Prerelease available at http://cime.lri.fr/.

[11]
Evelyne Contejean, Claude Marché, Ana-Paola Tomás, and Xavier Urbain. Solving termination constraints via finite domain polynomial interpretations. Unpublished draft, International Workshop on Constraints in Computational Logics, Gif-sur-Yvette, France, September 1999.

[12]
Jean-Pierre Jouannaud and Hélène Kirchner. Completion of a set of rules modulo a set of equations. SIAM Journal on Computing, 15(4), November 1986.

[13]
Jean-Pierre Jouannaud and Claude Marché. Completion modulo associativity, commutativity and identity. In Alfonso Miola, editor, Proc. Int. Symposium on Design and Implementation of Symbolic Computation Systems, LNCS 429, pages 111--120, Capri, Italy, April 1990. Springer-Verlag.

[14]
Jean-Pierre Jouannaud and Claude Marché. Termination and completion modulo associativity, commutativity and identity. Theoretical Computer Science, 104:29--51, 1992.

[15]
Abdelilah Kandri-Rody, Deepak Kapur, and Franz Winkler. Knuth-Bendix procedure and Buchberger algorithm --- a synthesis. In Proc. of the 20th Int. Symp. on Symbolic and Algebraic Computation, Portland, Oregon, pages 55--67, 1989.

[16]
Claude Kirchner and Hélène Kirchner. Constraint equational reasoning. In Proc. of the 20th Int. Symp. on Symbolic and Algebraic Computation, Portland, Oregon, 1989.

[17]
Donald E. Knuth and Peter B. Bendix. Simple word problems in universal algebras. In J. Leech, editor, Computational Problems in Abstract Algebra, pages 263--297. Pergamon Press, 1970.

[18]
Keiichirou Kusakari, Claude Marché, and Xavier Urbain. Termination of associative-commutative rewriting using dependency pairs criteria. Research Report 1304, LRI, 2002.

[19]
Philippe Le Chenadec. Canonical forms in finitely presented algebras. Pitman, London, 1986.

[20]
Claude Marché. On ground AC-completion. In Ronald. V. Book, editor, 4th International Conference on Rewriting Techniques and Applications, volume 488 of Lecture Notes in Computer Science, Como, Italy, April 1991. Springer-Verlag.

[21]
Claude Marché. The word problem of ACD-ground theories is undecidable. International Journal of Foundations of Computer Science, 3(1):81--92, 1992.

[22]
Claude Marché. Réécriture modulo une théorie présentée par un système convergent et décidabilité des problèmes du mot dans certaines classes de théories équationnelles. Thèse de doctorat, Université Paris-Sud, Orsay, France, October 1993.

[23]
Claude Marché. Normalised rewriting and normalised completion. In Proceedings of the Ninth Annual IEEE Symposium on Logic in Computer Science, pages 394--403, Paris, France, July 1994. IEEE Comp. Soc. Press.

[24]
Claude Marché. Normalized rewriting: an alternative to rewriting modulo a set of equations. Journal of Symbolic Computation, 21(3):253--288, 1996.

[25]
Claude Marché and Xavier Urbain. Termination of associative-commutative rewriting by dependency pairs. In Tobias Nipkow, editor, 9th International Conference on Rewriting Techniques and Applications, volume 1379 of Lecture Notes in Computer Science, pages 241--255, Tsukuba, Japan, April 1998. Springer-Verlag.

[26]
Benjamin Monate. Propriétés uniformes de familles de systèmes de réécriture de mots paramétrées par des entiers. Thèse de doctorat, Université Paris-Sud, Orsay, France, January 2002.

[27]
Paliath Narendran and Michaël Rusinowitch. Any ground associative-commutative theory has a finite canonical system. In Ronald V. Book, editor, Proc. 4th Rewriting Techniques and Applications, LNCS 488, Como, Italy, April 1991. Springer-Verlag.

[28]
Enno Ohlebusch, Claus Claves, and Claude Marché. TALP: A tool for the termination analysis of logic programs. In Leo Bachmair, editor, 11th International Conference on Rewriting Techniques and Applications, volume 1833 of Lecture Notes in Computer Science, pages 270--273, Norwich, UK, July 2000. Springer-Verlag. Available at http://bibiserv.techfak.uni-bielefeld.de/talp/.

[29]
Gerald E. Peterson and Mark E. Stickel. Complete sets of reductions for some equational theories. Journal of the ACM, 28(2):233--264, April 1981.

[30]
Xavier Urbain. Approche incrémentale des preuves automatiques de terminaison. Thèse de doctorat, Université Paris-Sud, Orsay, France, October 2001.
This document was translated from LATEX by HEVEA.