Decreasing Diagrams are Complete for Confluence
Jörg Endrullis, Ievgen Ivanov, Femke van Raamsdonk
cs.LO
Oct 5, 2026 · v1
TL;DR
The completeness proof of decreasing diagrams for confluence is machine-checked in Lean, alongside an independent Isabelle/HOL formalization.
Abstract
Confluence is a fundamental property of nondeterministic computations, arising from parallelism, concurrency, or freedom in the evaluation order. It guarantees that such a computation always yields the same result, regardless of the order in which steps are taken. 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. Essentially all classical confluence criteria arise as corollaries. 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. A positive answer was known only for countable systems, and recently up to the first uncountable cardinal $\aleph_1$. The general case remained open. We settle this thirty-three-year-old problem in full. 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. It follows that this single criterion can, in principle, certify the confluence of every confluent system, and hence of every confluent program. The entire development is machine-checked in the Isabelle/HOL and Lean proof assistants and relies only on classical logic and the axiom of choice.
Problem
Van Oostrom asked in 1993 whether decreasing diagrams are complete for confluence, that is, whether every confluent abstract rewriting system admits a locally decreasing labeling. This is RTA Open Problem 56. It was previously solved only for countable systems and up to cardinality aleph_1.
Approach
The problem is reduced to connected confluent components. In each component, a cofinal, connected, locally almost deterministic subsystem is built using traps, escapes, trap degree and fans. Systems whose cofinality cardinal is singular are handled with a 'double fan' construction. The almost deterministic subsystem admits a two-label decreasing labeling, which extends to the whole system with one extra label. The development is formalized in both Lean and Isabelle/HOL using classical logic and choice.
Results
Every confluent abstract rewriting system admits a locally decreasing labeling with three labels, which is optimal, so CR = DCR in ZFC. As a consequence, completeness holds independently of the Continuum Hypothesis. Both machine-checked formalizations confirm the result.