Project topics and materials
Get Complete Project Material File(s) Now! »
Decreasing Diagrams and Modularity
In Chapter 3, we revise the proof of van Oostrom’s decreasing diagrams method following the work by Jouannaud and van Oostrom [JvO09], via a technique called diagram rewriting. The diagram rewriting technique replaces a local peak in a conversion by its associated decreasing diagram to obtain a new conversion. When diagram rewriting terminates on all conversions of a rewrite relation, then the rewrite relation must be confluent. We give a new, simple order on conversions that establishes the confluence of rewriting under the assumption that every local peak has a decreasing diagram.
A generalization of decreasing diagrams is then proposed for rewrite modulo relations hS;Ei, made of a rewrite relation !S and a symmetric relation $E. When considering rewriting modulo, confluence should be generalized to the Church-Rosser modulo property: a rewrite modulo relation hS;Ei is Church-Rosser modulo E if every (S [ E)-conversion u $ S[E v is (S-)joinable modulo E (or say up to E), that is, u ! S $ E S v. We show that the decreasing diagrams method scales to the modulo case, thanks to a generalization of our order on conversions.
This chapter builds as well on a fundamental notion that characterizes confluence of possibly non terminating relations, Klop’s cofinal derivations [Klo80]. A cofinal derivation of a convertibility class is a possibly infinite derivation that each element of the convertibility class can rewrite to some element in the derivation. It plays the role of a normal form when the relation is non-terminating. Cofinal derivations were used by van Oostrom to obtain the completeness of his decreasing diagrams method, by labelling each rewrite step u ! v with the minimum number of steps from v to the cofinal derivation of its convertibility class [vO94b]. We show that cofinal derivations can be used to give a new, concise proof of Toyama’s celebrated modularity theorem [Toy87] and its recent extensions to rewriting modulo [JT08] in the case of strongly-coherent systems, an assumption discussed in depth within the chapter. This is done by generalizing cofinal derivations to cofinal streams, allowing us in turn to generalize van Oostrom’s completeness result to the modulo case.
Decreasing Diagrams on Abstract Positional Rewriting
Shown to be complete via Klop’s notion of cofinal derivations [Klo80], the decreasing diagrams method becomes a hammer for tackling confluence problems. When applying the method to show the confluence of a particularrewrite relation, the key is now to find a labelling that makes the relation satisfy the decreasing diagrams condition. Since cofinal derivations are nonconstructive, the completeness result indeed gives us little information about how to construct a local labelling, which is a function from rewrite steps to labels. Common labellings such as self-labelling and rule-labelling [vO08a] have no relationship whatsoever with the completeness result. Indeed, finding good labellings in practice has shown to be a hard task. Another problem pops up when applying the abstract decreasing diagrams technique to a concrete rewrite relation on a term structure. Our experience is that difficulties come essentially from ancestor (local) peaks, which are joinable in various ways depending on linearity assumptions of the relation. The technicalities to make them decreasing get much more complex in the absence of linearity assumptions. In Chapter 4, inspired by the work of Jouannaud and Li [JL12a], we lift the notion of decreasing diagrams to abstract positional rewriting, a level intermediate between abstract rewriting and term rewriting. Positional rewriting carries information about an abstract notion of positions, while remaining a relation on an abstract set whose elements have no structure. We further give different ways to define decreasing diagrams for abstract positional rewriting, which are guidelines on how to label a relation and to check its confluence.
Labelled rewriting modulo
We now turn our attention to a labelled rewrite system modulo (a labelled rewrite system for short) hS;Ei, made of a labelled rewrite relation !S as before (S for short), and a symmetric labelled relation $E (E for short). Note that E and S need not be disjoint. In this section, we are interested in the Church-Rosser property of their union S [ E. At this point, it is important to understand that !S is not meant to be generated by a set of rules. Both !S and $E denote relations. It turns out that $E will later denote the one-step equality relation generated by a set E of equations, but in general, !S will not denote the rewrite relation generated by a set R of rules, but rewriting with R modulo E defined later. We need not refer to R in this section.
We shall now need several convertibility relations that will be distinguished by indexing the labelled relation in use: we use $!E for E-conversion and $!S[E for (S [ E)-conversion. We reserve the notation s for the Econvertibility class of the element s. Conversations are as expected. We use !!S[E for the derivation relation of !S [ $E, while reachability is now defined as !!S $!E. Similarly, joinability modulo E of the pair hv;wi is now defined as v !!S s $!E t S w for some s; t, expressing the existence of a joinability proof modulo E.
Table of contents :
Abstract
Résumé
Acknowledgements
Contents
List of Figures
List of Tables
1 Introduction
1.1 Confluence
1.2 Decreasing Diagrams
1.3 This Thesis
1.3.1 Decreasing Diagrams and Modularity
1.3.2 Decreasing Diagrams on Abstract Positional Rewriting
1.3.3 Confluence of Rewrite Unions
1.3.4 Confluence of Layered Rewrite Systems
1.3.5 Confluence in Dependent Type Theories
1.4 Contributions and Organization of This Thesis
1.5 Publications
2 Preliminaries
2.1 Abstract Rewriting
2.2 Decreasing Diagrams
2.2.1 Labelled Rewriting
2.2.2 Local Diagrams
2.2.3 Diagram Rewriting
2.3 Term Rewriting
2.3.1 Term Algebras
2.3.2 Term Rewrite Systems
3 Decreasing Diagrams and Modularity
3.1 Diagrammatic Church-Rosser Property
3.1.1 Plain Labelled Rewriting
3.1.2 Diagram Rewriting
3.1.3 Labelled rewriting modulo
3.1.4 Diagram rewriting modulo
3.2 Cofinal Derivations and Streams
3.2.1 Cofinal Derivations
3.2.2 Cofinal Streams
3.3 Completeness
3.3.1 Plain Rewriting
3.3.2 Strongly-Coherent Rewriting Modulo
3.3.3 Need for Strong Coherence
3.4 Modularity
3.4.1 Plain Term Rewriting
3.4.2 Plain Modularity
3.4.3 Term Rewriting Modulo Equations
3.4.4 Modularity Modulo
3.5 Conclusion
4 Decreasing Diagrams on Abstract Positional Rewriting
4.1 Labelled Positional Rewriting
4.1.1 Domains
4.1.2 Rewriting
4.1.3 Rewriting Axioms
4.1.4 Local Diagrams
4.2 Terminating Systems
4.3 Linear Systems
4.4 Left-Linear Systems
4.4.1 First-Order Left-Linear Systems
4.4.2 When Plain Critical Pairs Suffice
4.5 Conclusion
5 Confluence of Rewrite Unions
5.1 Rewriting and Decomposition
5.1.1 Rewriting
5.1.2 Decreasing Diagrams
5.1.3 Decomposition
5.2 From Church-Rosser to Critical Pairs
5.2.1 Proof Strategy
5.2.2 A Hierarchy of Decompositions
5.2.3 Main Result
5.3 Relaxing Assumptions
5.3.1 Finite Constructor Lifting
5.3.2 Infinite Constructor Lifting
5.4 Related Work
5.5 Conclusion
6 Confluence of Layered Rewrite Systems
6.1 Terms and Rewriting
6.2 Sub-Rewriting
6.3 Cyclic Unification
6.4 Layered Systems
6.4.1 Layering
6.4.2 Closure properties
6.4.3 Testing Confluence of Layered Systems via Cyclic Critical Pairs
6.5 Conclusion
7 Conclusion
Bibliography
