1 Search Results for "Overbeek, Roy"


Document
Decreasing Diagrams with Two Labels Are Complete for Confluence of Countable Systems

Authors: Jörg Endrullis, Jan Willem Klop, and Roy Overbeek

Published in: LIPIcs, Volume 108, 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)


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.

Cite as

Jörg Endrullis, Jan Willem Klop, and Roy Overbeek. Decreasing Diagrams with Two Labels Are Complete for Confluence of Countable Systems. In 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 108, pp. 14:1-14:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)


Copy BibTex To Clipboard

@InProceedings{endrullis_et_al:LIPIcs.FSCD.2018.14,
  author =	{Endrullis, J\"{o}rg and Klop, Jan Willem and Overbeek, Roy},
  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 =	{Kirchner, H\'{e}l\`{e}ne},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2018.14},
  URN =		{urn:nbn:de:0030-drops-91848},
  doi =		{10.4230/LIPIcs.FSCD.2018.14},
  annote =	{Keywords: confluence, decreasing diagrams, weak diamond property}
}
  • Refine by Author
  • 1 Endrullis, Jörg
  • 1 Klop, Jan Willem
  • 1 Overbeek, Roy

  • Refine by Classification
  • 1 Theory of computation → Equational logic and rewriting

  • Refine by Keyword
  • 1 confluence
  • 1 decreasing diagrams
  • 1 weak diamond property

  • Refine by Type
  • 1 document

  • Refine by Publication Year
  • 1 2018

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail