| Title: |
Algebraic coherent confluence and higher globular Kleene algebras |
| Authors: |
Calk, Cameron; Goubault, Eric; Malbos, Philippe; Struth, Georg |
| Source: |
Logical Methods in Computer Science, Volume 18, Issue 4 (November 28, 2022) lmcs:6743 |
| Publication Year: |
2020 |
| Collection: |
Computer Science; Mathematics |
| Subject Terms: |
Computer Science - Logic in Computer Science; Mathematics - Category Theory |
| Description: |
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. |
| Document Type: |
Working Paper |
| DOI: |
10.46298/lmcs-18(4:9)2022 |
| Access URL: |
http://arxiv.org/abs/2006.16129 |
| Accession Number: |
edsarx.2006.16129 |
| Database: |
arXiv |