代数相干合流与高阶球形克莱尼代数
Algebraic coherent confluence and higher globular Kleene algebras
AI总结：
本文提出高阶球形克莱尼代数，将合流形式化扩展至相干合流证明，通过等式推理得到相干Church-Rosser定理与Newman引理，并应用于多面图建模的高阶重写系统。
摘要：
我们将克莱尼代数中合流结果的形式化扩展到相干合流证明的形式化。为此，我们引入了高阶球形克莱尼代数的结构，这是模态与并发克莱尼代数的高维推广。我们通过等式推理在高阶克莱尼代数中计算了相干的Church-Rosser定理和相干的Newman引理。我们将这些结果实例化到由多面图建模的高阶重写系统的上下文中。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
