Algebraic coherent confluence and higher globular Kleene algebras

TL;DR

This paper introduces higher globular Kleene algebras to formalize coherent confluence proofs, extending existing algebraic frameworks to higher dimensions and applying them to higher rewriting systems.

Contribution

It develops the structure of higher globular Kleene algebras and proves coherent Church-Rosser and Newman's lemmas within this framework, advancing algebraic formalization of confluence.

Findings

Coherent Church-Rosser theorem established in higher Kleene algebras

Coherent Newman's lemma proved for higher rewriting systems

Application to polygraphs demonstrates practical relevance

Abstract

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.