论文标题
代数相干汇合和较高的球状Kleene代数
Algebraic coherent confluence and higher globular Kleene algebras
论文作者
论文摘要
我们将汇合的形式化扩展到Kleene代数的形式上，以形式化连贯的汇合证明。为此，我们介绍了较高的球状Kleene代数的结构，这是对模态和并发kleene代数的高维概括。我们通过方程推理计算了一个连贯的教会定理和一个连贯的纽曼省的引理。我们将这些结果实例化在由测谎仪建模的较高重写系统的背景下。
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.
