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...
| Main Authors: | , , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Logical Methods in Computer Science e.V.
2022-11-01
|
| Series: | Logical Methods in Computer Science |
| Subjects: | |
| Online Access: | https://lmcs.episciences.org/6743/pdf |
| _version_ | 1797268470034857984 |
|---|---|
| author | Cameron Calk Eric Goubault Philippe Malbos Georg Struth |
| author_facet | Cameron Calk Eric Goubault Philippe Malbos Georg Struth |
| author_sort | Cameron Calk |
| collection | DOAJ |
| 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. |
| first_indexed | 2024-04-25T01:32:59Z |
| format | Article |
| id | doaj.art-0a53cf6d1ce14baa98c252946e41df48 |
| institution | Directory Open Access Journal |
| issn | 1860-5974 |
| language | English |
| last_indexed | 2024-04-25T01:32:59Z |
| publishDate | 2022-11-01 |
| publisher | Logical Methods in Computer Science e.V. |
| record_format | Article |
| series | Logical Methods in Computer Science |
| spelling | doaj.art-0a53cf6d1ce14baa98c252946e41df482024-03-08T10:40:29ZengLogical Methods in Computer Science e.V.Logical Methods in Computer Science1860-59742022-11-01Volume 18, Issue 410.46298/lmcs-18(4:9)20226743Algebraic coherent confluence and higher globular Kleene algebrasCameron CalkEric GoubaultPhilippe MalbosGeorg StruthWe 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://lmcs.episciences.org/6743/pdfcomputer science - logic in computer sciencemathematics - category theory |
| spellingShingle | Cameron Calk Eric Goubault Philippe Malbos Georg Struth Algebraic coherent confluence and higher globular Kleene algebras Logical Methods in Computer Science computer science - logic in computer science mathematics - category theory |
| title | Algebraic coherent confluence and higher globular Kleene algebras |
| title_full | Algebraic coherent confluence and higher globular Kleene algebras |
| title_fullStr | Algebraic coherent confluence and higher globular Kleene algebras |
| title_full_unstemmed | Algebraic coherent confluence and higher globular Kleene algebras |
| title_short | Algebraic coherent confluence and higher globular Kleene algebras |
| title_sort | algebraic coherent confluence and higher globular kleene algebras |
| topic | computer science - logic in computer science mathematics - category theory |
| url | https://lmcs.episciences.org/6743/pdf |
| work_keys_str_mv | AT cameroncalk algebraiccoherentconfluenceandhigherglobularkleenealgebras AT ericgoubault algebraiccoherentconfluenceandhigherglobularkleenealgebras AT philippemalbos algebraiccoherentconfluenceandhigherglobularkleenealgebras AT georgstruth algebraiccoherentconfluenceandhigherglobularkleenealgebras |