License: 
Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSCD.2018.14
URN: urn:nbn:de:0030-drops-91848
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2018/9184/
Endrullis, Jörg ;
Klop, Jan Willem ;
Overbeek, Roy
Decreasing Diagrams with Two Labels Are Complete for Confluence of Countable Systems
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 suffice 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.
BibTeX - Entry
@InProceedings{endrullis_et_al:LIPIcs:2018:9184,
author = {J{\"o}rg Endrullis and Jan Willem Klop and Roy Overbeek},
title = {{Decreasing Diagrams with Two Labels Are Complete for Confluence of Countable Systems}},
booktitle = {3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)},
pages = {14:1--14:15},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-077-4},
ISSN = {1868-8969},
year = {2018},
volume = {108},
editor = {H{\'e}l{\`e}ne Kirchner},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2018/9184},
URN = {urn:nbn:de:0030-drops-91848},
doi = {10.4230/LIPIcs.FSCD.2018.14},
annote = {Keywords: confluence, decreasing diagrams, weak diamond property}
}
|
Keywords: |
|
confluence, decreasing diagrams, weak diamond property |
|
Collection: |
|
3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018) |
|
Issue Date: |
|
2018 |
|
Date of publication: |
|
04.07.2018 |
