Algebraic coherent confluence and higher globular Kleene algebras
Logic in Computer Science
2023-06-22 v5 Category Theory
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.
Keywords
Cite
@article{arxiv.2006.16129,
title = {Algebraic coherent confluence and higher globular Kleene algebras},
author = {Cameron Calk and Eric Goubault and Philippe Malbos and Georg Struth},
journal= {arXiv preprint arXiv:2006.16129},
year = {2023}
}