Document Open Access Logo

Completeness of the Decreasing Diagrams Method for Proving Confluence of Rewriting Systems of the Least Uncountable Cardinality

Author Ievgen Ivanov

PDF HTML 5

Files

Thumbnail PDF
PDF
LIPIcs.FSCD.2025.25.pdf
  • Filesize: 0.98 MB
  • 20 pages
HTML5 Logo HTML (experimental)
LIPIcs.FSCD.2025.25.html

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Equational logic and rewriting
  • Theory of computation → Logic and verification
Keywords
  • confluence
  • decreasing diagrams method
  • rewriting systems
  • reduction
  • formal methods
  • formal proofs
  • formal verification
  • non-discrete models
  • nondeterministic models
  • interval models

Metrics

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

Abstract

We show that every confluent abstract rewriting system (ARS) of the cardinality that does not exceed the first uncountable cardinal belongs to the class DCR₃, i.e. the class of confluent ARS for which confluence can be proved with the the help of the decreasing diagrams method using the set of labels {0,1,2} ordered in such a way that 0<1<2 (in the general case, the decreasing diagrams method with two labels is not sufficient for proving confluence of such ARS). Under the Continuum Hypothesis this result implies that the decreasing diagrams method is sufficient for establishing confluence of ARS on many structures of interest to applied mathematics and various interdisciplinary fields (confluence of ARS on real numbers, continuous real functions, etc.). 
We provide a machine-checked formal proof of a formalized version of the main result in Isabelle proof assistant using HOL logic and the HOL-Cardinals theory. An extended version of this formalization is available in the Archive of Formal Proofs.

Cite As Get BibTex

Ievgen Ivanov. Completeness of the Decreasing Diagrams Method for Proving Confluence of Rewriting Systems of the Least Uncountable Cardinality. In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 25:1-25:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.FSCD.2025.25

Author Details

Ievgen Ivanov
  • Taras Shevchenko National University of Kyiv, Ukraine

Supplementary Materials

References

  1. Radhakisan Baheti and Helen Gill. Cyber-physical systems. The impact of control technology, 12(1):161-166, 2011. Google Scholar
  2. Nicolas Behr and Jean Krivine. Rewriting theory for the life sciences. In International Conference on Graph Transformation, pages 185-202, 2020. Google Scholar
  3. Jasmin Christian Blanchette, Andrei Popescu, and Dmitriy Traytel. Cardinals in Isabelle/HOL. In Lecture Notes in Computer Science, volume 8558, pages 111-127, 2014. URL: https://doi.org/10.1007/978-3-319-08970-6_8.
  4. Mirna Bognar. A point version of decreasing diagrams. In Proceedings Accolade 1996. Dutch Graduate School in Logic, pages 1-14, 1997. Google Scholar
  5. F. Bonchi, F. Gadducci, A. Kissinger, P. Sobociński, and F. Zanasi. String diagram rewrite theory I: Rewriting with Frobenius structure. Journal of the ACM, 69(2):14:1-14:58, 2022. URL: https://doi.org/10.1145/3502719.
  6. N.G. de Bruijn. A note on weak diamond properties. Memorandum 78-08, Eindhoven Uninversity of Technology, 1978. Google Scholar
  7. R. Diestel and O. Pikhurko. On the cofinality of infinite partially ordered sets: Factoring a poset into lean essential subsets. Order, 20:53-66, 2003. URL: https://doi.org/10.1023/A:1024449306316.
  8. Jörg Endrullis and Jan Willem Klop. De Bruijn’s weak diamond property revisited. Indagationes Mathematicae, 24:1050-1072, 2013. Google Scholar
  9. 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), pages 14:1-14:15. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018. URL: https://doi.org/10.4230/LIPICS.FSCD.2018.14.
  10. Jörg Endrullis, Jan Willem Klop, and Roy Overbeek. Decreasing diagrams for confluence and commutation. Logical Methods in Computer Science, 16:23:1-23:25, 2020. URL: https://doi.org/10.23638/LMCS-16(1:23)2020.
  11. A.A. Fraenkel, Y. Bar-Hillel, and A. Levy. Foundations of Set Theory. Elsevier, 1973. Google Scholar
  12. Jean Goubault-Larrecq. Non-Hausdorff topology and domain theory: Selected topics in point-set topology. Cambridge University Press, 2013. Google Scholar
  13. N. Hirokawa, A. Middeldorp, C. Sternagel, and S. Winkler. Abstract completion, formalized. Logical Methods in Computer Science, 15(3):19:1-19:42, 2019. URL: https://doi.org/10.23638/LMCS-15(3:19)2019.
  14. Isabelle proof assistant. http://isabelle.in.tum.de. [Online].
  15. J.R. Isbell. The category of cofinal types. II. Trans. Amer. Math. Soc., 116:394-416, 1965. Google Scholar
  16. Ievgen Ivanov. Generalized Newman’s lemma for discrete and continuous systems. In Leibniz International Proceedings in Informatics, volume 260, pages 9:1-9:17, 2023. URL: https://doi.org/10.4230/LIPICS.FSCD.2023.9.
  17. Ievgen Ivanov. Formal proof of completeness of the decreasing diagrams method for proving confluence of relations of the least uncountable cardinality (supplementary material for this paper). https://doi.org/10.5281/zenodo.14254256, 2024. [Online].
  18. Ievgen Ivanov. On Newman’s lemma and non-termination. In CEUR-WS.org, volume 3624, pages 14-24, 2024. URL: https://ceur-ws.org/Vol-3624/Paper_2.pdf.
  19. Ievgen Ivanov. On non-triviality of the hierarchy of decreasing Church-Rosser abstract rewriting systems. In Proceedings of the 13th International Workshop on Confluence, pages 30-35, 2024. Google Scholar
  20. Ievgen Ivanov. On the cofinality property in the context of the hierarchy of decreasing Church-Rosser abstract rewriting systems. In Information Technology and Implementation, November 20-21, 2024, Kyiv, Ukraine, 2024. Google Scholar
  21. Ievgen Ivanov. Completeness of decreasing diagrams for the least uncountable cardinality. Archive of Formal Proofs, April 2025. https://isa-afp.org/entries/Completeness_Decreasing_Diagrams_for_N1.html, Formal proof development.
  22. Ievgen Ivanov. Formalization of a confluent abstract rewriting system of the least uncountable cardinality outside of the class DCR2. https://doi.org/10.5281/zenodo.14740062, 2025. [Online].
  23. John L. Kelley. General topology. Van Nostrand, 1955. Google Scholar
  24. Jan Willem Klop. Combinatory Reduction Systems. PhD thesis, Rijks-universiteit Utrecht, 1980. Google Scholar
  25. Alexander Krauss and Andreas Schropp. A mechanized translation from Higher-Order Logic to set theory. In Lecture Notes in Computer Science, volume 6172, pages 323-338. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-14052-5_23.
  26. Ondřej Kunčar and Andrei Popescu. Comprehending Isabelle/HOL’s consistency. In Lecture Notes in Computer Science, volume 10201, pages 724-749. Springer, 2017. URL: https://doi.org/10.1007/978-3-662-54434-1_27.
  27. Ondřej Kunčar and Andrei Popescu. A consistent foundation for Isabelle/HOL. Journal of Automated Reasoning, 62:531-555, 2019. URL: https://doi.org/10.1007/S10817-018-9454-8.
  28. Edward A. Lee. Fundamental limits of cyber-physical systems modeling. ACM Transactions on Cyber-Physical Systems, 1(1):1-26, 2016. URL: https://doi.org/10.1145/2912149.
  29. George Markowsky. Chain-complete posets and directed sets with applications. Algebra universalis, 6(1):53-68, 1976. Google Scholar
  30. Elliott Mendelson. Introduction to Mathematical Logic. CRC Press, 2015. Google Scholar
  31. Eric C. Milner and Maurice Pouzet. On the cofinality of partially ordered sets. Ordered sets, pages 279-298, 1982. Google Scholar
  32. Eric C. Milner and Karel Prikry. The cofinality of a partially ordered set. Proc. London Math. Soc., 46:454-470, 1983. Google Scholar
  33. Chuangjie Xu Nicolai Kraus, Fredrik Nordvall Forsberg. Type-theoretic approaches to ordinals. Theoretical computer science, 957, 2023. URL: https://doi.org/10.1016/J.TCS.2023.113843.
  34. Tobias Nipkow, Markus Wenzel, and Lawrence C Paulson. Isabelle/HOL: a proof assistant for higher-order logic. Springer, 2002. URL: https://doi.org/10.1007/3-540-45949-9.
  35. Andrew Pitts. The HOL logic. In Introduction to HOL: A Theorem Proving Environment for Higher Order Logic, pages 191-232. Cambridge University Press, 1993. Google Scholar
  36. Raymond Smullyan. Set theory and the continuum problem. Clarendon Press, 1996. Google Scholar
  37. Christian Sternagel and Rene Thiemann. Abstract rewriting. Archive of Formal Proofs, June 2010. Google Scholar
  38. Stevo Todorcevic. Directed sets and cofinal types. Trans. Amer. Math. Soc., 290:711-723, 1985. Google Scholar
  39. John W. Tukey. Convergence and uniformity in topology. Princeton University Press, 1940. Google Scholar
  40. Vincent Van Oostrom. Confluence by decreasing diagrams. Theoretical computer science, 126(2):259-280, 1994. URL: https://doi.org/10.1016/0304-3975(92)00023-K.
  41. Vincent Van Oostrom. Confluence for Abstract and Higher-Order Rewriting. PhD thesis, Vrije Universiteit Amsterdam, 1994. Google Scholar
  42. Vincent Van Oostrom. Confluence by decreasing diagrams - converted. In Lecture Notes in Computer Science, volume 5117, pages 306-320, 2008. Google Scholar
  43. Shang-Zhi Wang and Bo Yu Li. On the minimal cofinal subsets of a directed quasi-ordered set. Discrete Mathematics, 48:289-306, 1984. URL: https://doi.org/10.1016/0012-365X(84)90189-4.
  44. Freek Wiedijk. The seventeen provers of the world: Foreword by Dana S. Scott, volume 3600. Springer, 2006. URL: https://doi.org/10.1007/11542384.
  45. Harald Zankl. Confluence by decreasing diagrams - formalized. In 24th International Conference on Rewriting Techniques and Applications, pages 352-367. Leibniz International Proceedings in Informatics, 2013. URL: https://doi.org/10.4230/LIPICS.RTA.2013.352.
  46. Harald Zankl. Decreasing diagrams. Archive of Formal Proofs, 2013. Google Scholar
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact