2026

  1. Decreasing Diagrams Are Complete for Confluence
    Jörg Endrullis, Ievgen Ivanov, and Femke van Raamsdonk
    https://arxiv.org/abs/2610.06368, (2026)
    paper

    Summary

    The decreasing diagrams technique of van Oostrom is one of the most versatile methods for establishing confluence of transition systems (abstract rewriting systems). It reduces global confluence to local confluence: a system is confluent whenever its transitions admit a locally decreasing labeling.

    A central question, posed by van Oostrom in 1993, asks whether the decreasing diagrams technique is complete: does every confluent transition system admit a locally decreasing labeling? This is Problem 56 of the RTA List of Open Problems. We prove that every confluent transition system admits a locally decreasing labeling using only three labels. This bound is optimal, as two labels do not suffice even at the first uncountable cardinality. The entire development is machine-checked in the Isabelle/HOL and Lean proof assistants (Zenodo).

    See research for an overview of my research on confluence.

    Bibtex

    @misc{confluence:decreasing:diagrams:2026,
  author = {Endrullis, J{\"{o}}rg and Ivanov, Ievgen and van Raamsdonk, Femke},
  title = {Decreasing Diagrams are Complete for Confluence},
  howpublished = {arXiv preprint 2610.06368},
  year = {2026},
  url = {https://arxiv.org/abs/2610.06368},
  doi = {10.48550/arXiv.2610.06368},
  keywords = {rewriting, confluence},
  type = {miscellaneous}
}

    Digital Object Identifier

    10.48550/arXiv.2610.06368