Algebraic coherent confluence and higher globular Kleene algebras

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-Ro...

Full description

Saved in:
Bibliographic Details
Published in:Logical methods in computer science 2022-11, Vol.18, Issue 4 (4)
Main Authors: Calk, Cameron, Goubault, Eric, Malbos, Philippe, Struth, Georg
Format: Article
Language:English
Subjects:
Category Theory
Computer Science
computer science - logic in computer science
Data Structures and Algorithms
Mathematics
mathematics - category theory
Citations: Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.
ISSN:1860-5974
1860-5974
DOI:10.46298/lmcs-18(4:9)2022