Confluence is a central property of rewrite systems, and it plays an important role for:

• program correctness as it guarantees uniqueness of results (normal forms), and
• model checking where it is employed for state space reduction.

Confluence

A binary relation \( \to \) on a set \( A \) is confluent if \( \forall a,b,c \in A. \) \[ b \leftarrow^* a \to^* c \implies \exists d.\; b \to^* d \leftarrow^* c \]

In other words, \( \to \) is confluent if \( {\leftarrow^* \cdot \to^*} \subseteq {\to^* \cdot \leftarrow^*} \). This can be illustrated as follows:

Here we write \( \twoheadrightarrow \) for \( \to^* \), the reflexive, transitive closure of \( \to \). The solid lines stand for universal quantification, and the dotted lines for existential quantification.

Decreasing Diagrams & Weak Diamond Property

The decreasing diagrams technique is one of the strongest and most versatile methods for proving confluence. It is complete for proving confluence of all systems [1], and it has many well-known confluence criteria as corollaries, for instance:

• Newman’s lemma,
• Huet’s strong confluence.
• the lemma of Hindley–Rosen, and
• Rosen’s request lemma.

The way to decreasing diagrams was paved by De Bruijn in 1978 in a note describing the weak diamond property, with a proof based on an intricate induction. The search for an elegant proof led van Oostrom in 1994 to the decreasing diagrams technique.

The weak diamond property and decreasing diagrams have many similarities. The basic idea of both techniques is to employ a labeling of the steps in order to conclude confluence from local confluence. Local confluence (\( {\leftarrow \cdot \to} \subseteq {\to^* \cdot \leftarrow^*} \)) itself is not sufficient for confluence. To this end, both methods exploit the labeling of the steps to impose additional requirements on the joining reductions, as displayed in the following figure:

The red and green lines inside the diagrams are just a visual aid. The red lines indicate a strict decrease of the label, the green lines a weak decrease.

Weak Diamond Property - De Bruijn (1978)

A relation \( \to \) is confluent if the steps can be labeled with labels from a well-founded total order \( < \) such that every peak \[ c \stackrel{\beta}{\leftarrow} a \stackrel{\alpha}{\to} b \] with \( \boldsymbol{\beta \le \alpha} \) can be joined by reductions of the form of the weak diamond property (above).

Decreasing Diagrams - Van Oostrom (1994)

A relation \( \to \) is confluent if the steps can be labeled with labels from a well-founded partial order \( < \) such that every peak \[ c \stackrel{\beta}{\leftarrow} a \stackrel{\alpha}{\to} b \] can be joined by reductions of the form of the decreasing diagram (above).

So the differences between the weak diamond property and decreasing diagrams concern the use of total vs. partial orders, and the symmetry in the decreasing diagram.

Our contribution

De Bruijn’s note on the weak diamond property is a seminal work as it pioneers the key ingredients (the labeling and the shape of the diagrams) that make decreasing diagrams so strong. Nevertheless, the weak diamond property has almost been forgotten over time.

In [2], we show that the weak diamond property and decreasing diagrams have equal strengths. Given a confluence proof using decreasing diagrams, we obtain a proof using the weak diamond property by transforming the partial order on the labels into a total order. We demonstrate that this does not require the Axiom of Choice as we can identify elements of equal `ordinal height’. Previously, it has been known that the decreasing diagrams technique subsumes the weak diamond property, but the reverse has not been known.

In [2], we moreover give a new proof of confluence by decreasing diagrams. Our proof is just about one page long, and is one of the shortest proofs of confluence by decreasing diagrams.

Finally, we prove in [2] that decreasing diagrams are not complete for proving commutation of countable (even finite) systems (while they are complete for confluence of countable systems).

In [3], we investigate how the size of the label set influences the strength of decreasing diagrams. Surprisingly, we find that two labels suffice for proving confluence of every countable confluent system. This stands in sharp contrast to the situation for commutation, where two labels do not suffice. We construct, for every \( n \in \mathbb{N} \), a rewrite system that can be proven commutating using \( n \) labels but not with less labels.

Ievgen Ivanov subsequently showed that two labels do not suffice for uncountable systems: there is a confluent system of cardinality \( \aleph_1 \) that cannot be proven confluent by decreasing diagrams with two labels (Ievgen Ivanov, On Non-triviality of the Hierarchy of Decreasing Church-Rosser Abstract Rewriting Systems, IWC 2024; see also Completeness of the Decreasing Diagrams Method for Proving Confluence of Rewriting Systems of the Least Uncountable Cardinality, FSCD 2025). This answers one of the questions raised by our work (see the open problems below). He then showed that decreasing diagrams are complete for confluence of all systems of cardinality up to \( \aleph_1 \), the first completeness result beyond countable systems (Ievgen Ivanov, FSCD 2025).

In [1], together with Ievgen Ivanov and Femke van Raamsdonk, we have recently extended this result: decreasing diagrams are unconditionally complete for confluence, for systems of arbitrary cardinality, and three labels suffice. This solves Problem #56 of the RTA List of Open Problems, posed by van Oostrom in 1993 (see below). By Ivanov’s result, three labels are optimal. Since the weak diamond property and decreasing diagrams have equal strengths [2], the weak diamond property is complete for confluence as well. The proof is machine-checked in the proof assistants Isabelle/HOL and Lean, using only classical logic and the axiom of choice; the formalizations are available on Zenodo.

Open problems (now solved)

Considering the importance and wide use of decreasing diagrams, it is surprising that it remained open from 1993 until 2026 whether decreasing diagrams are complete for uncountable systems:

Open Problem (#56 on the RTA List of Open Problems) (Solved)

Is decreasing diagrams complete for proving confluence of uncountable systems?

Posed by Vincent van Oostrom in 1993.

Solution

Yes. Every confluent system can be proven confluent by decreasing diagrams with three labels [1]. This extends the result of Ievgen Ivanov (FSCD 2025), who proved completeness for systems of cardinality up to \( \aleph_1 \). The proof is formalized in Isabelle/HOL and Lean; see Zenodo.

Our results in [3] suggest that it may be fruitful to first answer the following question:

Open Problem (Solved)

Is there an uncountable confluent system that cannot be proven confluent by decreasing diagrams with two labels?

Solution

Yes. Ievgen Ivanov showed that there is a confluent system of cardinality \( \aleph_1 \) that cannot be proven confluent by decreasing diagrams with two labels (IWC 2024; see also FSCD 2025). On the other hand, three labels always suffice [1].

References

1. Decreasing Diagrams Are Complete for Confluence

   Jörg Endrullis, Ievgen Ivanov, and Femke van Raamsdonk

   https://arxiv.org/abs/2610.06368, (2026)

   summary paper bib doi

   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

2. De Bruijn’s Weak Diamond Property Revisited

   Jörg Endrullis, and Jan Willem Klop

   Indagationes Mathematicae , 24 (4) , pp. 1050–1072 (2013)

   summary paper bib doi

   Summary

   In this paper we revisit an unpublished but influential technical report from 1978 by N.G. de Bruijn, written in the framework of the Automath project. This report describes a technique for proving confluence of abstract reduction systems, called the weak diamond property. It paved the way for the powerful technique developed by Van Oostrom to prove confluence of abstract reduction systems, called decreasing diagrams.

   We first revisit in detail De Bruijn’s old proof, providing a few corrections and hints for understanding. We find that this original criterion and proof technique are still worthwhile. Next, we establish that De Bruijn’s confluence criterion can be used to derive the decreasing diagrams theorem (the reverse was already known). We also provide a short proof of decreasing diagrams in the spirit of De Bruijn. We finally address the issue of completeness of this method.

   See research for an overview of my research on confluence.

   Bibtex

   @article{confluence:weak:diamond:2013,
     author = {Endrullis, J\"{o}rg and Klop, Jan Willem},
     title = {{De Bruijn’s Weak Diamond Property Revisited}},
     journal = {Indagationes Mathematicae},
     volume = {24},
     number = {4},
     pages = {1050 -- 1072},
     year = {2013},
     doi = {10.1016/j.indag.2013.08.005},
     note = {In memory of N.G. (Dick) de Bruijn (1918–2012)},
     keywords = {rewriting, confluence},
     type = {journal}
   }
   

   Digital Object Identifier

   10.1016/j.indag.2013.08.005

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

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

   In: Proc. Conf. on Formal Structures for Computation and Deduction (FSCD 2018) , pp. 14:1–14:15 , Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2018)

   summary paper bib doi

   Summary

   The decreasing diagrams technique is one of the strongest and most versatile methods for proving confluence of abstract reduction systems. So what makes decreasing diagrams so powerful? In contrast to other confluence techniques, decreasing diagrams employ a labelling of the steps.

   In this paper we investigate how the size of the label set influences the strength of the technique. Surprisingly, we find that two labels suffice for proving confluence of every confluent, countable system. In contrast, for proving commutation of rewrite relations, it turns out that the strength of the technique increases with more labels.

   While decreasing diagrams is complete for proving confluence of countable systems, the technique is not complete for commutation. In our paper De Bruijn's Weak Diamond Property Revisited we give a counterexample to the completeness of decreasing diagrams for commutation.

   See research for an overview of my research on confluence.

   Bibtex

   @inproceedings{confluence:decreasing:diagrams:2018,
     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 = {Proc.\ Conf.\ on Formal Structures for Computation and Deduction (FSCD~2018)},
     volume = {108},
     pages = {14:1--14:15},
     publisher = {Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik},
     series = {LIPIcs},
     year = {2018},
     doi = {10.4230/LIPIcs.FSCD.2018.14},
     keywords = {rewriting, confluence},
     type = {conference}
   }
   

   Digital Object Identifier

   10.4230/LIPIcs.FSCD.2018.14