Decreasing Diagrams for Confluence and Commutation
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 te...
| Main Authors: | , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Logical Methods in Computer Science e.V.
2020-02-01
|
| Series: | Logical Methods in Computer Science |
| Subjects: | |
| Online Access: | https://lmcs.episciences.org/5145/pdf |
| _version_ | 1827322834018369536 |
|---|---|
| author | Jörg Endrullis Jan Willem Klop Roy Overbeek |
| author_facet | Jörg Endrullis Jan Willem Klop Roy Overbeek |
| author_sort | Jörg Endrullis |
| collection | DOAJ |
| description | 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 rewrite 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 rewrite 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.
Secondly, we show that this result stands in sharp contrast to the situation
for commutation of rewrite relations, where the hierarchy does not collapse.
Thirdly, investigating the possibility of a confluence hierarchy, we
determine the first-order (non-)definability of the notion of confluence and
related properties, using techniques from finite model theory. We find that in
particular Hanf's theorem is fruitful for elegant proofs of undefinability of
properties of abstract rewrite systems. |
| first_indexed | 2024-04-25T01:35:07Z |
| format | Article |
| id | doaj.art-feabf76e8c42455e9629d6bff7032dc7 |
| institution | Directory Open Access Journal |
| issn | 1860-5974 |
| language | English |
| last_indexed | 2024-04-25T01:35:07Z |
| publishDate | 2020-02-01 |
| publisher | Logical Methods in Computer Science e.V. |
| record_format | Article |
| series | Logical Methods in Computer Science |
| spelling | doaj.art-feabf76e8c42455e9629d6bff7032dc72024-03-08T10:29:27ZengLogical Methods in Computer Science e.V.Logical Methods in Computer Science1860-59742020-02-01Volume 16, Issue 110.23638/LMCS-16(1:23)20205145Decreasing Diagrams for Confluence and CommutationJörg EndrullisJan Willem KlopRoy OverbeekLike 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 rewrite 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 rewrite 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. Secondly, we show that this result stands in sharp contrast to the situation for commutation of rewrite relations, where the hierarchy does not collapse. Thirdly, investigating the possibility of a confluence hierarchy, we determine the first-order (non-)definability of the notion of confluence and related properties, using techniques from finite model theory. We find that in particular Hanf's theorem is fruitful for elegant proofs of undefinability of properties of abstract rewrite systems.https://lmcs.episciences.org/5145/pdfcomputer science - logic in computer science |
| spellingShingle | Jörg Endrullis Jan Willem Klop Roy Overbeek Decreasing Diagrams for Confluence and Commutation Logical Methods in Computer Science computer science - logic in computer science |
| title | Decreasing Diagrams for Confluence and Commutation |
| title_full | Decreasing Diagrams for Confluence and Commutation |
| title_fullStr | Decreasing Diagrams for Confluence and Commutation |
| title_full_unstemmed | Decreasing Diagrams for Confluence and Commutation |
| title_short | Decreasing Diagrams for Confluence and Commutation |
| title_sort | decreasing diagrams for confluence and commutation |
| topic | computer science - logic in computer science |
| url | https://lmcs.episciences.org/5145/pdf |
| work_keys_str_mv | AT jorgendrullis decreasingdiagramsforconfluenceandcommutation AT janwillemklop decreasingdiagramsforconfluenceandcommutation AT royoverbeek decreasingdiagramsforconfluenceandcommutation |