一句话：引入高阶球状 Kleene 代数，将合流证明推广为相干合流，并用等式推理证明相干 Church-Rosser 定理与 Newman 引理。
本文关注如何把 Kleene 代数中已有的合流性形式化提升为相干合流证明。作者引入高阶球状 Kleene 代数，这是模态 Kleene 代数与并发 Kleene 代数的高维推广，并在该代数框架中用等式推理计算相干 Church-Rosser 定理和相干 Newman 引理。随后，他们将结果实例化到由 polygraph 建模的高阶重写系统，说明该代数结构可为高阶重写中的相干合流提供统一的代数证明方法。
We extend the formalisation of confluence results in Kleene algebras to a formalisation of coherent confluence proofs. For this, we introduce the structure of higher globular Kleene algebra, a higher-dimensional generalisation of modal and concurrent Kleene algebra. We calculate a coherent Church-Rosser theorem and a coherent Newman's lemma in higher Kleene algebras by equational reasoning. We instantiate these results in the context of higher rewriting systems modelled by polygraphs.
@article{paperbot1640,
title = {Algebraic coherent confluence and higher globular Kleene algebras},
author = {Cameron Calk and Eric Goubault and Philippe Malbos and Georg Struth},
journal = {Logical Methods in Computer Science},
volume = {Volume 18, Issue 4},
year = {2022},
doi = {10.46298/lmcs-18(4:9)2022}
}