Monday 10 October 2016, 10:30, INRIA Saclay, room Gilles Kahn: Confluence of rewrite systems based on decreasing diagrams, PhD defense, Jiaxiang Liu (Ecole Polytechnique).

Abstract. Formal methods are increasingly used for developing critical software. Proof assistants based on type theories allow to formally prove properties of software, in particular partial or total correctness. In expressive type theories allowing for dependent types, computations based on rewriting play a fundamental role in identifying types up to computation, such as even(2 + 2) and even(4 + 0) which both compute to even(4). This is possible thanks to two crucial properties of rewrite rules, termination and confluence. A third essential, more semantical property, is type preservation. Confluence is the property of rewriting-based computations expressing that the associated extensional relation is functional, implying uniqueness of normal forms, which exist thanks to termination. In this thesis, we are interested in confluence.
Note that this problem is already present in weaker languages called algebraic specification languages, such as OBJ or the functional kernel of Maude. In those simply typed languages without functional types, type preservation is an easy property of the rules, and proving termination can be done independently of confluence. The confluence proof can therefore use the termination property. This is not possible in typed theories, for which termination , confluence of typed terms, and type preservation, depend on each other. Proving confluence on untyped terms is the usual way out, and can then be done first. The difficulty is that computations do not terminate on untyped terms, hence confluence must be proved for non-terminating computations.

Our interest in this thesis is therefore to develop confluence proof methods in the presence of non-terminating computations.

It is well-known that confluence of a set of rewrite rules is undecidable. In the sub-case where rewriting terminates, methods for showing confluence have been well developed, and are based on the computation of “minimal diverging computations” called critical peaks, 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, where a rule is left-linear when each one of its free variables cannot occur more than once in the left-hand side. 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.
Recently, van Oostrom proposed a framework based on decreasing diagrams, a notion that can capture the two main methods used in the literature for analyzing confluence, no matter whether the rewrite system is terminating or not. Based on that, Felgenhauer obtained a general result to solve the confluence problem of left-linear non-terminating systems via critical pairs, leaving the non-left-linear non-terminating case open.

This thesis is therefore devoted to the development of techniques that reduce confluence to the checking of critical pairs for rewrite systems that are possibly non-terminating and non-left-linear. To this end, we carry out a thorough investigation of the notion of decreasing diagrams, from the notion itself up to its applications.

The first part of this thesis focuses on the decreasing diagrams method itself, which is known to be complete: a relation on an abstract set is confluent if and only if it can be equipped with a (well-founded) set of labels such that every diverging computation, called peak, has a decreasing diagram, that is, its extremities can be joined by steps whose direction and labels satisfy some constraints with respect to the peak’s rewrites and labels. 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.
By giving an alternative simpler proof of the decreasing diagrams method, we succeed in extending the method and its completeness result to the modulo case, in which computations mix rewrite steps and equational steps which are strongly coherent, a notion due to Jouannaud and Munoz. A direct consequence is a new and concise proof of Toyama’s celebrated modularity result of confluence for rewrite systems that are built from disjoint signatures and its modulo extension by Jouannaud and Toyama.

A second achievement of the thesis lifts up the abstract decreasing diagrams method to a slightly more concrete level. By generalizing the method on abstract positional rewriting introduced by Jouannaud and Li, and by extending it by a multi-labelled version, we propose a general framework for proving confluence of term rewrite systems in an axiomatic way which captures all results from the literature that we know of, in particular those relying on a notion introduced by Huet and further developed under the name of parallel closedness, which all appear as particular cases of decreasing diagrams.

The rest of the thesis deals with confluence of syntactic classes of concrete rewrite systems that are possibly non-terminating and non-left-linear.
A first idea is to split a rewrite system into a terminating part RT and a left-linear, possibly non-terminating one RNT. Again, we assume two disjoint signatures, FT and FNT. RT is built from symbols in FT . RNT is built from arbitrary symbols, but assumed to be rank non-increasing, where the rank of a term is its maximal number of layers alternations. Then, the confluence of RT [ RNT can be reduced to the joinability of the critical pairs of RT and the existence of decreasing diagrams for the critical pairs of RT inside RNT, as well as for some parallel critical pairs of RNT with itself called rigid. The results, that are a strict generalization of Knuth-Bendix critical pair criterion for terminating computations, rely on a new rewriting relation, called “sub-rewriting”, which allows to apply an RT -rewrite provided the various possible instantiations of a non-linear variable can be (recursively) joined. This notion appears therefore as a restriction of conditional rewriting with left-linear conditional rewrite rules, in case the conditions are conjunctions of joinability predicates between variables.
The second idea investigated is a novel notion of rank, which is defined independentlyof any signature split: in essence, the maximum number of “linearized redexes” traversed from the root to a leaf in a term, where linearized redexes are instances of the linearized left-hand sides of rules. The main result here relies on two notions: subrewriting again, and “cyclic-unification”, in other words, unification “à la PROLOG” without occur-check. We then prove that a rank non-increasing rewrite system is confluent provided all its “cyclic critical pairs” have decreasing diagrams in which the cyclic equations obtained by unification can be used via their congruence closure. This result explains a variety of confluent and non-confluent examples due to Newman for its abstract version, Klop for its concrete version, and others for variations. We also show that our result is sharp, by showing that another more complex non-confluent rewrite system, due again to Klop, that happens to have no cyclic critical pair is indeed rank increasing.

We are currently investigating non-terminating higher-order computations as those we may find in Dedukti. This part of our work is still preliminary, hence will not be included in this thesis, despite the fact that it can be seen as a major practical application of these techniques.

Résumé. 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 appelé superposition qui se récrit de deux manière différentes en une paire de termes appelé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 à équiper 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 extré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'est à dire que toute relation confluente peut-être équipé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-terminants, une espèce de forme normale sous la forme d’une suite infinie de réécritures élémentaires, appelée "dérivation cofinale".
Dans une première partie, nous revisitons les résultats de van Oostrom, et en proposons une preuve différente simple dans le but de les généraliser au cas des calculs dits "modulo", c'est à dire dans des quotients, qui mêlent des règles et inéquations. Cette généralisation inclue la complétude, en faisant intervenir une généralisation de la notion de dérivation cofinale dans le cas des calculs fortement cohérents au sens de Jouannaud et Munoz. 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 problè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.