Algebraic coherent confluence and higher globular Kleene algebras

Cameron Calk; Eric Goubault; Philippe Malbos; Georg Struth

doi:10.46298/lmcs-18(4:9)2022

Cameron Calk ; Eric Goubault ; Philippe Malbos ; Georg Struth - Algebraic coherent confluence and higher globular Kleene algebras

lmcs:6743 - Logical Methods in Computer Science, November 28, 2022, Volume 18, Issue 4 - https://doi.org/10.46298/lmcs-18(4:9)2022

Algebraic coherent confluence and higher globular Kleene algebrasArticle

Authors: Cameron Calk ; Eric Goubault ; Philippe Malbos ; Georg Struth

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.

https://doi.org/10.46298/lmcs-18(4:9)2022

Source: arXiv.org:2006.16129

Volume: Volume 18, Issue 4

Published on: November 28, 2022

Imported on: August 29, 2020

Keywords: Computer Science - Logic in Computer Science, Mathematics - Category Theory

Licence: arXiv.org - Non-exclusive license to distribute