Confluence properties of rewrite rules by decreasing diagrams
Propriétés de confluence des règles de réécriture par des diagrammes décroissants
Résumé
This thesis is devoted to the confluence of rewrite systems in the absence of termination, for applications in first-order functional languages like MAUDE or higher-order languages with dependent types, as Dedukti. In the first case, the computations on infinite data structures do not terminate, while in the second case, untyped computations do not terminate because of beta-reduction. In the case where the computations terminate, confluence is reduced to that of critical peaks, the "minimal diverging computations", made of a minimal middle term called "overlap" which computes in two different ways, resulting in a so-called "critical pair". In the case of non-terminating computations, a main result is that left-linear rewrite rules that have no critical pairs are always confluent. This suggests that the notion of critical pairs plays a key role there too, but a general understanding of the confluence of non-terminating computations in terms of critical pairs is still missing.Our investigation of confluence is based on the decreasing diagrams method due to van Oostrom, which generalizes the techniques used previously for both terminating and non-terminating computations. The method is abstract in the sense that it applies to arbitrary relations on an abstract set. It equips each step of computations with a label taken from a well-founded set. A diverging computation, called peak, has a decreasing diagram if its extremities can be joined by steps whose direction and labels satisfy some constraints with respect to the peak's rewrites and labels. The strength of this technique is its completeness, that is, any confluent relation can be equipped with a well-founded set of labels such that all peaks have decreasing diagrams. The proof of completeness is based on Klop's notion of cofinal derivations, which is an infinite derivation playing the role of a normal form when computations do not terminate.In the first part, we revise the results of van Oostrom, and propose an alternative proof that extends the method to the "modulo" case, in which computations mix rewrite steps and equational steps. The completeness result is extended as well, via a generalization of cofinal derivations and the notion of strong coherence due to Jouannaud and Kirchner.The second part of the thesis applies the decreasing diagrams method and its generalization to concrete systems rewriting terms, as well as to several open problems. The recent application to the problems of higher-order computations in dependent type theory is not part of the thesis.
Cette thèse étudie la confluence des systèmes de récriture en l'absence de propriété de terminaison, pour des applications aux langages fonctionnels de premier ordre comme MAUDE, ou aux langages d'ordre supérieur comportant des types dépendants, comme Dedukti. Dans le premier cas, les calculs opérant sur des structures de données infinies ne terminent pas. Dans le second, les calculs non typés ne terminent pas à cause de la beta-réduction. Dans le cas où les calculs terminent, la confluence se réduit à celle des pics critiques, divergences minimales du calcul, obtenues à partir d'un terme médian appellé superposition qui se récrit de deux manière différentes en une paire de termes appellée critique. Dans le cas où les calculs ne terminent pas, le résultat majeur est que les calculs définis par des règles linéaires à gauche et sans paires critiques confluent. Il s'agit donc d'étendre ce résultat aux systèmes dont les règles peuvent être non-linéaires à gauche et avoir des paires critiques.L'étude la confluence est faite à partir de la méthode des diagrammes décroissants, qui généralise les techniques utilisées antérieurement aussi bien pour des calculs qui terminent que pour des calculs qui ne terminent pas. Cette technique est abstraite, en ce sens qu'elle s'applique à des relations arbitraires opérant sur un ensemble abstrait. Elle consiste à équipper chaque étape de calcul d'un label pris dans un ensemble bien fondé. Un pic de calcul, composé d'un terme se récrivant de deux manières différentes, possède un diagramme décroissant lorsque ses extémités peuvent se récrire en un terme commun avec des étapes de calcul satisfaisant des conditions de comparaison avec les labels du pic. La force de cette technique est sa complétude, c-a-d que toute relation confluente peut-être équippée d'un système de labels (par des entiers) pour lequel tous ses pics possèdent des diagrammes décroissants. Ce résultat est basé sur un théorème assez ancien de Klop, qui définit pour les systèmes non-terminant, uneespèce de forme normale sous la forme d'une suite infinie de récritures élémentaires, appellée "dérivation cofinale".Dans une première partie, nous révisitons les résultats de van Oostrom, et en proposons une preuve différente dans le but de les généraliser au cas des calculs dits "modulo", c-a-d dans des quotients, qui mèlent des règles et deséquations. Cette généralisation inclue la complétude, en faisant intervenir une généralisation de lanotion de dérivation cofinale dans le cas des calculs cohérents au sens de Jouannaud et Kirchner.La second partie de la thèse applique le théorème de van Oostrom et sa généralisation à des système (concrets) de récriture de termes, ainsi qu'à plusieurs priblèmes ouverts du domaine. L'application récente à des problèmes d'ordre supérieur tirés de la théorie des types dépendants ne fait pas partie de la thèse.
Origine : Version validée par le jury (STAR)