Document Open Access Logo

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

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

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2018.14.pdf
  • Filesize: 450 kB
  • 15 pages

Document Identifiers

Author Details

Jörg Endrullis
  • Vrije Universiteit Amsterdam, Department of Computer Science, Amsterdam, the Netherlands
Jan Willem Klop
  • Vrije Universiteit Amsterdam, Department of Computer Science, Amsterdam, the Netherlands, and, Centrum Wiskunde & Informatica (CWI), Amsterdam, the Netherlands
Roy Overbeek
  • Vrije Universiteit Amsterdam, Department of Computer Science, Amsterdam, the Netherlands

Cite AsGet BibTex

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)
https://doi.org/10.4230/LIPIcs.FSCD.2018.14

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.

Subject Classification

ACM Subject Classification
  • Theory of computation → Equational logic and rewriting
Keywords
  • confluence
  • decreasing diagrams
  • weak diamond property

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. N.G. de Bruijn. A Note on Weak Diamond Properties. Memorandum 78-08, Eindhoven Uninversity of Technology, 1978. Google Scholar
  2. J. Endrullis, H. Geuvers, J.G. Simonsen, and H. Zantema. Levels of Undecidability in Rewriting. Information and Computation, 209(2):227-245, 2011. Google Scholar
  3. J. Endrullis, J. Karhumäki, J.W. Klop, and A. Saarela. Degrees of infinite words, polynomials and atoms. In Proc. Conf. Developments in Language Theory (DLT 2016), LNCS, pages 164-176. Springer, 2016. Google Scholar
  4. J. Endrullis and J.W. Klop. De Bruijn’s weak diamond property revisited. Indagationes Mathematicae, 24(4):1050-1072, 2013. In memory of N.G. (Dick) de Bruijn (1918–2012). Google Scholar
  5. J. Endrullis, J.W. Klop, A. Saarela, and M. Whiteland. Degrees of transducibility. In Proc. Conf. on Combinatorics on Words (WORDS 2015), volume 9304 of LNCS, pages 1-13. Springer, 2015. Google Scholar
  6. J.R. Hindley. The Church-Rosser Property and a Result in Combinatory Logic. PhD thesis, University of Newcastle-upon-Tyne, 1964. Google Scholar
  7. G.P. Huet. Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems. Journal of the ACM, 27(4):797-821, 1980. Google Scholar
  8. J. Ketema and J.G. Simonsen. Least upper bounds on the size of confluence and church-rosser diagrams in term rewriting and λ-calculus. ACM Trans. Comput. Log., 14(4):31:1-31:28, 2013. Google Scholar
  9. J.W. Klop. Combinatory Reduction Systems, volume 127 of Mathematical centre tracts. Mathematisch Centrum, 1980. Google Scholar
  10. J.W. Klop. Term Rewriting Systems. In Handbook of Logic in Computer Science, volume II, pages 1-116. Oxford University Press, 1992. Google Scholar
  11. M. Li and P.M.B. Vitányi. An Introduction to Kolmogorov Complexity and Its Applications. Springer, 2nd edition, 2008. Google Scholar
  12. M.H.A. Newman. On Theories with a Combinatorial Definition of "Equivalence". Annals of Mathematics, 42(2):223-243, 1942. Google Scholar
  13. B.K. Rosen. Tree-manipulating systems and Church-Rosser theorems. Journal of the ACM, 20:160-187, 1973. Google Scholar
  14. J.R. Shoenfield. Degrees of Unsolvability. North-Holland, Elsevier, 1971. Google Scholar
  15. Terese. Term Rewriting Systems, volume 55 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2003. Google Scholar
  16. R. Treinen. The first-order theory of one-step rewriting is undecidable. In Proc. Conf. on Rewriting Techniques and Applications (RTA), volume 1103 of LNCS, pages 276-286. Springer, 1996. Google Scholar
  17. V. van Oostrom. Confluence by Decreasing Diagrams. Theoretical Computer Science, 126(2):259-280, 1994. Google Scholar
  18. V. van Oostrom. Confluence for Abstract and Higher-Order Rewriting. PhD thesis, Vrije Universiteit Amsterdam, 1994. Google Scholar
  19. V. van Oostrom. Confluence by Decreasing Diagrams, Converted. In Proc. Conf. on Rewriting Techniques and Applications (RTA 2008), volume 5117 of LNCS, pages 306-320. Springer, 2008. Google Scholar
  20. H. Zantema. The Termination Hierarchy for Term Rewriting. Applicable Algebra in Engineering, Communication and Computing, 12(1):3-19, 2001. Google Scholar
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
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact