Terminaison de la récriture

La terminaison est la propriété que toute exécution (tout calcul) aboutit toujours à un résultat. Cette propriété est fondamentale dès qu’une récurrence est concernée. Elle sert dans de nombreux cas de préliminaire incontournable lorsqu’on souhaite exhiber d’autres comportements souhaitables des programmes. La confluence d’un système de récriture, par exemple, devient décidable si ce système termine. On peut également exhiber grâce à elle des propriétés de progression de processus répartis.

J’étudie cette propriété dans le cadre des systèmes de récriture. Ces systèmes sont des ensembles d’équations orientées appelées règles. Ils définissent un formalisme très simple et générique (le calcul s’effectue par remplacement syntaxique d’expressions par d’autres) et universel, toute machine de Turing pouvant être codée par un système de règles de récriture. Cette universalité entraîne de facto l’indécidabilité de la terminaison. Mes travaux de thèse se sont situés dans le cadre de la définition de méthodes forcément incomplètes mais correctes visant à prouver de manière entièrement automatique la terminaison des systèmes auxquels on est confronté dans la pratique.

Mes recherches ont porté sur la terminaison modulo associativité et commutativité et sur la modularité des preuves de terminaison. Mes résultats sont mis en œuvre dans le logiciel CiME.

1. Terminaison modulo AC

Le cas des systèmes de récriture comportant des symboles associatifs et commutatif (AC) est important en pratique : les opérations AC sont fréquentes, en outre elles permettent des gains importants en terme d’efficacité de calcul. Décrire la commutativité comme une règle de récriture est cependant inexploitable : x+y → y+x ne termine pas. On doit donc travailler sur les classes d’équivalence AC. Les ordres utilisés dans les preuves de terminaison doivent respecter celles-ci en évaluant de la même manière deux termes AC équivalents : on parle d’ordre compatible AC. Les contraintes sur les ordres sont alors très fortes et compliquent considérablement leur recherche automatique.

Destiner ces ordres à faire décroître strictement les règles du système est en fait trop restrictif. En 1997 Arts & Giesl ont proposé un nouveau critère, fondé sur une analyse structurelle plus fine des termes pouvant donner lieu à une réduction infinie. Il suffit cette fois de réclamer une décroissance large sur les règles et stricte sur les paires de dépendance. Ce critère est purement syntaxique et facilement implantable. Les conditions que doit vérifier l’ordre candidat sont plus nombreuses mais moins restrictives : il n’est plus utile de se limiter aux ordres de simplification et davantage de systèmes rencontrés en pratique peuvent bénéficier d’une preuve automatique de terminaison.

Contributions

J’ai proposé une définition de paires de dépendance pour le cas AC. L’extension du critère « sans marques », en collaboration avec Claude Marché, a été publiée dans les actes de la conférence internationale RTA (1998) [ps.gz].

La nette amélioration due à l’introduction de symboles marqués a été adaptée aux systèmes associatifs-commutatifs dans le cadre de la première partie de mon travail de thèse [ps.gz] et a fait l’objet d’un rapport de recherche [ps.gz].

Une notion plus générale a également été définie, voir le paragraphe Extensions.

2. Modularité des preuves de terminaison

La taille des programmes dont on est amené à vérifier les propriétés (en particulier la terminaison des systèmes de récriture) rend trop difficile et trop coûteuse une preuve globale pour le système dans sa totalité. De tels programmes (de tels systèmes) étant décomposés en plusieurs modules de taille réduite, il serait très intéressant d’avoir des outils permettant, à partir de résultats sur chacun de ces modules, de déduire des propriétés sur l’ensemble, menant ainsi à des preuves incrémentales et modulaires.

Je me suis intéressé, aux unions hiérarchiques, comparables en tous points aux liens entre les modules des programmes.

En effet, on est souvent amené, lorsqu’on programme de façon modulaire, à définir une hiérarchie entre les différentes parties du code : les opérations d’un module M1 seront par exemple utilisées dans les modules M2 et M3. On aimerait alors prouver une fois pour toutes une propriété (ici la terminaison) de M1, sans avoir à refaire cette preuve lors des ajouts de M2 et M3. De même, pour analyser un programme dépendant de M2, il serait utile de pouvoir utiliser les résultats déjà connus sur l’union M1 + M2 sans les établir de nouveau.

Obtenir l’incrémentalité est un objectif crucial, en conséquence ce problème a été très étudié. La plupart des travaux concernent les unions disjointes, c’est-à-dire les unions de systèmes ne partageant pas de symboles, un cas inutile dans la pratique, et peu de résultats sont probants. L’étude de propriétés des paires de dépendance permet d’établir certains résultats de modularité : en particulier les travaux de Gramlich ont été étendus à la méthode des paires de dépendance par Giesl & Ohlebusch, mais il s’agit là encore de travaux sur les unions disjointes de systèmes. Les résultats sur les unions hiérarchiques que j’ai étudiés sont, eux aussi, peu satisfaisants : les conditions imposées pour garantir la terminaison étant trop fortes ou peu adaptées à une automatisation de la preuve. Pour contourner cette difficulté, j’ai réclamé une propriété plus forte que la terminaison : la conservation de la terminaison sous projection quelconque. Cette propriété est satisfaite sur quasiment tous les exemples concrets auxquels on s’intéresse et se comporte mieux modulairement.

Contributions

J’ai tout d’abord proposé un nouveau formalisme présentant un système de récriture comme une hiérarchie de modules qu’on peut déterminer de façon complètement automatique. Les différentes unions rencontrées dans la pratique (disjointes, à constructeurs partagés, composables…) peuvent toutes n’être exprimées qu’en tant qu’extensions de modules uniquement.

J’ai ensuite défini sur ces modules une notion de paires de dépendance profitant à plein de la nature hiérarchique des extensions et une classe d’ordres (les ordres π-extensibles) respectant la projection. Ces notions fournissent une méthode alliant les atouts d’un critère par paires de dépendance, purement syntaxique et implantable, à la puissance d’ordres comprenant strictement les ordres de simplification. Cette méthode permet de prouver incrémentalement la terminaison d’extensions modulaires sans se soucier des ensembles de règles localement non pertinents, ce qui n’était pas le cas auparavant. On retrouve grâce à elle certains résultats antérieurs.

Ce travail, dont une partie a été présentée à la conférence internationale IJCAR 2001, [ps.gz] a fait l’objet d’une publication au Journal of Automated Reasoning [réf] [pdf].

Depuis ma thèse, Claude Marché et moi-même avons proposé une généralisation du concept de paires de dépendance modulo AC permettant d’exprimer toutes les définitions connues de paires adaptées à cette théorie. Cette nouvelle notion ainsi que son intégration au cadre des modules ont paru au Journal of Symbolic Computation [réf] [ps.gz].

3. Mise en œuvre

Ces résultats sont mis en œuvre au sein de l’outil logiciel CiME. CiME est une boîte à outils comprenant un mécanisme efficace de résolution de contraintes diophantiennes, la manipulation des systèmes de récriture (de mots, de termes, C ou AC, etc.) et leur complétion (Knuth-Bendix). Elle permet en outre de prouver automatiquement la terminaison des systèmes de récriture à l’aide de différentes méthodes. Certaines de ses composantes ont été intégrées à des outils de preuves de programmes logiques comme Talp et les résultats sont tout à fait compétitifs avec ceux de systèmes de preuves de terminaison dédiés.

CiME est capable de trouver seul des ordres convenables grâce à une méthode à base de résolution de contraintes issue d’une collaboration avec Claude Marché, Evelyne Contejean (L.R.I.) et Ana-Paula Tomás (Université de Porto) et une version préliminaire de ce travail a été présentée lors du Workshop international sur les contraintes CCL'99. Il paru au Journal of Automated Reasoning [réf] [pdf].

J’ai implanté au sein de CiME notre nouveau critère de terminaison pour les systèmes AC ainsi qu’une méthode efficace de calcul d’un ensemble correct de paires de dépendance. J’ai également intégré les mécanismes de modularité que j’ai proposés, y compris dans le cas AC.

Ces mécanismes permettent un passage à l’échelle des critères dont nous disposons ; à titre d’application une preuve de terminaison d’un système de plusieurs centaines de règles (une cinquantaine de modules) issu d’une spécification µcrl de processus communicants peut désormais être trouvée de façon totalement automatique en quelques secondes.

J’ai en particulier implanté l’outil mucrltocime de typage et compilation des spécifications µcrl vers CiME, afin de permettre une automatisation des preuves de leurs propriétés.

4. Récriture multisortée, conditionnelle et avec stratégies

Dans le cadre d’une action bilatérale entre le CNRS et l’université de l’Illinois à Urbana-Champaign (UIUC) et afin de permettre la preuve de terminaison de programmes exprimés dans un langage fondé sur la logique de récriture comme Maude (SRI & UIUC) ou sur le ρ-calcul comme ELAN (LORIA) à l’aide d’outils de terminaison comme CiME qui requièrent des spécifications plus restrictives (non typées, sans conditions, etc.), j’ai travaillé avec F. Duran (Univ. Malaga, Espagne), S. Lucas (Univ. Valence, Espagne), C. Marché (LRI-PCRI) et J. Meseguer (UIUC, États-Unis) à la définition de transformations successives vers des théories de plus en plus simples (quoiqu’avec stratégies) telles que la terminaison du programme transformé entraîne la terminaison de l’original.

Contributions

Nous avons défini une suite de transformations éliminant successivement les sortes, sous-sortes et prédicats d’appartenance (Membership Rewriting) puis les conditions d’application des règles et enfin les annotations de stratégies d’évaluation. Ces travaux ont paru au journal Higher Order and Symbolic Computation[réf] [pdf]. Ils ont ouvert la voie à une architecture commune de preuve de terminaison pour différents outils et langages (Maude + Mu-Term + CiME).

En ce qui concerne les stratégies locales de type Context-Sensitive (CS), j’ai travaillé avec Gutierrez et Lucas à la définition de règles utilisables (une méthode d’élimination de règles non pertinentes s’appuyant sur mes résultats de thèse) pour une notion de paires de dépendance CS (Alarcon, Gutierrez, Lucas). Nous obtenons une définition correcte de règles utilisables et délimitons une classe syntaxique de systèmes pour lesquels ils est possible d’appliquer une approche moins coûteuse mais inapplicable dans le cas général. Ces travaux ont été présentés à la conférence internationale RTA [réf.] [pdf] et sont implantés dans l’outil Mu-Term.