发表机构
Vrije Universiteit Amsterdam; Taras Shevchenko National University of Kyiv（阿姆斯特丹自由大学; 基辅塔拉斯舍甫琴科国立大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本文证明了 van Oostrom 的递减图技术对合流性是完备的：每个合流转移系统都存在一个仅用三个标记的局部递减标记，且该界最优，从而解决了 RTA 开放问题第 56 题。
AI 中文摘要
合流性是非确定性计算的一个基本性质，它源于并行性、并发性或求值顺序的自由性。它保证此类计算无论以何种顺序执行步骤，总能产生相同的结果。van Oostrom 的递减图技术是建立转移系统（抽象重写系统）合流性最通用的方法之一。它将全局合流性归结为局部合流性：一个系统是合流的，当且仅当其转移允许一个局部递减的标记。本质上，所有经典合流性判据都是其推论。van Oostrom 于 1993 年提出的一个核心问题询问递减图技术是否完备：是否每个合流的转移系统都允许一个局部递减的标记？这是 RTA 开放问题列表中的第 56 个问题。此前已知对于可数系统答案为肯定，并且最近已推进到第一个不可数基数 $\aleph_1$。一般情况仍然开放。我们完整解决了这个存在了三十三年之久的问题。我们证明了每个合流的转移系统都允许一个仅使用三个标记的局部递减标记。这个界是最优的，因为即使在第一个不可数基数下，两个标记也不够。由此可知，这一单一判据原则上可以证明每个合流系统的合流性，从而证明每个合流程序的合流性。整个开发过程在 Isabelle/HOL 和 Lean 证明助手中进行了机器校验，并且仅依赖于经典逻辑和选择公理。
英文摘要
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.
