ALGEBRAIC COHERENT CONFLUENCE AND HIGHER GLOBULAR KLEENE ALGEBRAS

被引：0

作者：

Calk, Cameron ^{[1
]}

Goubault, Eric ^{[1
]}

Malbos, Philippe ^{[2
]}

Struth, Georg ^{[3
,4
]}

机构：

[1] Ecole Polytech, LIX, CNRS, IP Paris, Palaiseau, France

[2] Univ Claude Bernard Lyon 1, Inst Camille Jordan, CNRS UMR 5208, 43 Blvd 11 Novembre 1918, F-69622 Villeurbanne, France

[3] Univ Sheffield, Dept Comp Sci, 211 Portobello, Sheffield S1 4DP, England

[4] Coll Lyon, 26 Pl Bellecour, F-69002 Lyon, France

来源：

LOGICAL METHODS IN COMPUTER SCIENCE | 2020年 / 18卷 / 04期

关键词：

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

D O I：

10.46298/LMCS-18(4:9)2022

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

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.

引用

页数：43

共 50 条

[1] ALGEBRAIC COHERENT CONFLUENCE AND HIGHER GLOBULAR KLEENE ALGEBRAS
Calk C.
Goubault E.
Malbos P.
Struth G.
Logical Methods in Computer Science, 2022, 18 (04): : 9:1 - 9:43
[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 →