| Title: |
Algebraic coherent confluence and higher-dimensional globular Kleene algebras |
| Authors: |
Calk, Cameron; Malbos, Philippe; Goubault, Eric; Struth, Georg |
| Contributors: |
Institut Camille Jordan Villeurbanne (ICJ); École Centrale de Lyon (ECL); Université de Lyon-Université de Lyon-Université Claude Bernard Lyon 1 (UCBL); Université de Lyon-Université Jean Monnet Saint-Étienne (UJM)-Institut National des Sciences Appliquées de Lyon (INSA Lyon); Université de Lyon-Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Centre National de la Recherche Scientifique (CNRS) |
| Source: |
https://hal.archives-ouvertes.fr/hal-03161580 ; 2020. |
| Publisher Information: |
HAL CCSD |
| Publication Year: |
2020 |
| Collection: |
Archive ouverte HAL (Hyper Article en Ligne, CCSD - Centre pour la Communication Scientifique Directe) |
| Subject Terms: |
Modal Kleene algebras; confluence; coherence; higher-dimensional rewriting; M.S.C. 2010 -68Q65; 03B35; 18D05; [MATH.MATH-CT]Mathematics [math]/Category Theory [math.CT]; [INFO.INFO-DS]Computer Science [cs]/Data Structures and Algorithms [cs.DS] |
| Description: |
We extend the formalisation of confluence results in Kleene algebras to a formalisation of coherent proofs by confluence. To this end, we introduce the structure of modal higher-dimensional globular Kleene algebra, a higher-dimensional generalisation of modal and concurrent Kleene algebra. We give a calculation of a coherent Church-Rosser theorem and Newman's lemma in higher-dimensional Kleene algebras. We interpret these results in the context of higher-dimensional rewriting systems described by polygraphs. |
| Document Type: |
report |
| Language: |
English |
| Relation: |
info:eu-repo/semantics/altIdentifier/arxiv/2006.16129; hal-03161580; https://hal.archives-ouvertes.fr/hal-03161580; https://hal.archives-ouvertes.fr/hal-03161580/document; https://hal.archives-ouvertes.fr/hal-03161580/file/algebraicCoherence.pdf; ARXIV: 2006.16129 |
| Availability: |
https://hal.archives-ouvertes.fr/hal-03161580; https://hal.archives-ouvertes.fr/hal-03161580/document; https://hal.archives-ouvertes.fr/hal-03161580/file/algebraicCoherence.pdf |
| Rights: |
info:eu-repo/semantics/OpenAccess |
| Accession Number: |
edsbas.7DD37E8A |
| Database: |
BASE |