ALGEBRAIC COHERENT CONFLUENCE AND HIGHER GLOBULAR KLEENE ALGEBRAS

被引：0

作者：

Calk C. ^{[1
]}

Goubault E. ^{[1
]}

Malbos P. ^{[2
]}

Struth G. ^{[3
,4
]}

机构：

[1] LIX, École Polytechnique, CNRS, IP-Paris, Palaiseau

[2] Université Claude Bernard Lyon 1, CNRS UMR 5208, Institut Camille Jordan, 43 Blvd. du 11 novembre 1918, Villeurbanne cedex

[3] Department of Computer Science, The University of Sheffield, Regent Court, 211 Portobello, Sheffield

[4] Collegium de Lyon, 26 Place Bellecour, Lyon

来源：

Logical Methods in Computer Science | 2022年 / 18卷 / 04期

关键词：

coherence; confluence; higher dimensional rewriting; Modal Kleene algebras;

D O I：

10.46298/lmcs-18(4:9)2022

中图分类号：

O1 [数学];

学科分类号：

0701 ; 070101 ;

摘要：

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. © C. Calk, E. Goubault, P. Malbos, and G. Struth.

引用

页码：9:1 / 9:43

共 50 条

[41] Kleene Algebras, Regular Languages and Substructural Logics
Wurm, Christian
ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2014, (161): : 46 - 59
[42] An Efficient Coq Tactic for Deciding Kleene Algebras
Braibant, Thomas
Pous, Damien
INTERACTIVE THEOREM PROVING, PROCEEDINGS, 2010, 6172 : 163 - 178
[43] EQUATIONAL PROPERTIES OF KLEENE ALGEBRAS OF RELATIONS WITH CONVERSION
ESIK, Z
BERNATSKY, L
THEORETICAL COMPUTER SCIENCE, 1995, 137 (02) : 237 - 251
[44] A FAMILY OF FINITE DE MORGAN AND KLEENE ALGEBRAS
Walker, Carol L.
Walker, Elbert A.
INTERNATIONAL JOURNAL OF UNCERTAINTY FUZZINESS AND KNOWLEDGE-BASED SYSTEMS, 2012, 20 (05) : 631 - 653
[45] INJECTIVE DE-MORGAN AND KLEENE ALGEBRAS
CIGNOLI, R
PROCEEDINGS OF THE AMERICAN MATHEMATICAL SOCIETY, 1975, 47 (02) : 269 - 278
[46] Congruence Permutable Kleene-Stone Algebras
LUO Congwen
Wuhan University Journal of Natural Sciences, 2010, 15 (02) : 99 - 102
[47] The variety of Kleene algebras with conversion is not finitely based
Crvenkovic, S
Dolinka, I
Ésik, Z
THEORETICAL COMPUTER SCIENCE, 2000, 230 (1-2) : 235 - 245
[48] The Cube of Kleene Algebras and the Triangular Prism of Multirelations
Nishizawa, Koki
Tsumagari, Norihiro
Furusawa, Hitoshi
RELATIONS AND KLEENE ALGEBRA IN COMPUTER SCIENCE, PROCEEDINGS, 2009, 5827 : 276 - +
[49] Graded algebras associated to algebraic algebras need not be algebraic
Smoktunowicz, Agata
EUROPEAN CONGRESS OF MATHEMATICS 2008, 2010, : 441 - 449
[50] On Paraconsistent Weak Kleene Logic: Axiomatisation and Algebraic Analysis
Bonzio, Stefano
Gil-Ferez, Jose
Paoli, Francesco
Peruzzi, Luisa
STUDIA LOGICA, 2017, 105 (02) : 253 - 297

← 1 2 3 4 5 →