Confluence properties of rewrite rules by decreasing diagrams

Abstract : 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.
Document type :
Theses
Complete list of metadatas

https://pastel.archives-ouvertes.fr/tel-01515698
Contributor : Abes Star <>
Submitted on : Friday, April 28, 2017 - 4:52:40 AM
Last modification on : Tuesday, April 16, 2019 - 9:08:35 AM
Long-term archiving on: Saturday, July 29, 2017 - 12:26:49 PM

File

54418_LIU_2016_archivage.pdf
Version validated by the jury (STAR)

Identifiers

  • HAL Id : tel-01515698, version 1

Citation

Jiaxiang Liu. Confluence properties of rewrite rules by decreasing diagrams. Computation and Language [cs.CL]. Université Paris-Saclay; Tsinghua University (Pékin), 2016. English. ⟨NNT : 2016SACLX044⟩. ⟨tel-01515698⟩

Share

Metrics

Record views

194

Files downloads

144