Decreasing diagrams with two labels are complete for confluence of countable systems

Research output: Chapter in Book / Report / Conference proceedingConference contributionAcademicpeer-review

Abstract

Like termination, confluence is a central property of rewrite systems. Unlike for termination, however, there exists no known complexity hierarchy for confluence. In this paper we investigate whether the decreasing diagrams technique can be used to obtain such a hierarchy. The decreasing diagrams technique is one of the strongest and most versatile methods for proving confluence of abstract reduction systems, it is complete for countable systems, and it has many well-known confluence criteria as corollaries. So what makes decreasing diagrams so powerful? In contrast to other confluence techniques, decreasing diagrams employ a labelling of the steps ? with labels from a well-founded order in order to conclude confluence of the underlying unlabelled relation. Hence it is natural to ask how the size of the label set influences the strength of the technique. In particular, what class of abstract reduction systems can be proven confluent using decreasing diagrams restricted to 1 label, 2 labels, 3 labels, and so on? Surprisingly, we find that two labels su ce for proving confluence for every abstract rewrite system having the cofinality property, thus in particular for every confluent, countable system. We also show that this result stands in sharp contrast to the situation for commutation of rewrite relations, where the hierarchy does not collapse. Finally, as a background theme, we discuss the logical issue of first-order definability of the notion of confluence.

Original languageEnglish
Title of host publication3rd International Conference on Formal Structures for Computation and Deduction, FSCD 2018
PublisherSchloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
Pages1-15
Number of pages15
Volume108
ISBN (Electronic)9783959770774
DOIs
Publication statusPublished - 1 Jul 2018
Event3rd International Conference on Formal Structures for Computation and Deduction, FSCD 2018 - Oxford, United Kingdom
Duration: 9 Jul 201812 Jul 2018

Conference

Conference3rd International Conference on Formal Structures for Computation and Deduction, FSCD 2018
CountryUnited Kingdom
CityOxford
Period9/07/1812/07/18

Keywords

  • Confluence
  • Decreasing diagrams
  • Weak diamond property

Fingerprint Dive into the research topics of 'Decreasing diagrams with two labels are complete for confluence of countable systems'. Together they form a unique fingerprint.

Cite this