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 条

[1] ALGEBRAIC COHERENT CONFLUENCE AND HIGHER GLOBULAR KLEENE ALGEBRAS
Calk, Cameron
Goubault, Eric
Malbos, Philippe
Struth, Georg
LOGICAL METHODS IN COMPUTER SCIENCE, 2020, 18 (04)
[2] ON KLEENE ALGEBRAS
CRVENKOVIC, S
MADARASZ, RS
THEORETICAL COMPUTER SCIENCE, 1993, 108 (01) : 17 - 24
[3] Kleene algebras with implication
José Luis Castiglioni
Sergio Arturo Celani
Hernán Javier San Martín
Algebra universalis, 2017, 77 : 375 - 393
[4] Kleene algebras with implication
Luis Castiglioni, Jose
Arturo Celani, Sergio
Javier San Martin, Hernan
ALGEBRA UNIVERSALIS, 2017, 77 (04) : 375 - 393
[5] Continuous Kleene ω-Algebras
Esik, Zoltan
Fahrenberg, Uli
Legay, Axel
DEVELOPMENTS IN LANGUAGE THEORY (DLT 2015), 2015, 9168 : 240 - 251
[6] Residuated Kleene algebras
Alfréd Rényi Institute of Mathematics, Hungarian Academy of Sciences, 13-15 Reáltanoda u., 1053 Budapest, Hungary
不详
Lect. Notes Comput. Sci., 2012, (1-11):
[7] DECIDING KLEENE ALGEBRAS IN COQ
Braibant, Thomas
Pous, Damien
LOGICAL METHODS IN COMPUTER SCIENCE, 2012, 8 (01)
[8] Characterizing determinacy in Kleene algebras
Desharnais, J
Möller, B
INFORMATION SCIENCES, 2001, 139 (3-4) : 253 - 273
[9] INJECTIVE DEMORGAN AND KLEENE ALGEBRAS
CIGNOLI, RLO
NOTICES OF THE AMERICAN MATHEMATICAL SOCIETY, 1974, 21 (02): : A293 - A294
[10] Free Kleene algebras with domain
McLean, Brett
JOURNAL OF LOGICAL AND ALGEBRAIC METHODS IN PROGRAMMING, 2020, 117

← 1 2 3 4 5 →