We gratefully acknowledge support from
the Simons Foundation and member institutions.
Full-text links:


Current browse context:


Change to browse by:


References & Citations

DBLP - CS Bibliography


(what is this?)
CiteULike logo BibSonomy logo Mendeley logo del.icio.us logo Digg logo Reddit logo ScienceWISE logo

Computer Science > Logic in Computer Science

Title: Concurrency Theorems for Non-linear Rewriting Theories

Authors: Nicolas Behr (Université de Paris, CNRS, IRIF), Russ Harmer (Univ. Lyon, EnsL, UCBL, CNRS, LIP, France), Jean Krivine (Université de Paris, CNRS, IRIF)
Abstract: Sesqui-pushout (SqPO) rewriting along non-linear rules and for monic matches is well-known to permit the modeling of fusing and cloning of vertices and edges, yet to date, no construction of a suitable concurrency theorem was available. The lack of such a theorem, in turn, rendered compositional reasoning for such rewriting systems largely infeasible. We develop in this paper a suitable concurrency theorem for non-linear SqPO-rewriting in categories that are quasi-topoi (subsuming the example of adhesive categories) and with matches required to be regular monomorphisms of the given category. Our construction reveals an interesting "backpropagation effect" in computing rule compositions. We derive in addition a concurrency theorem for non-linear double pushout (DPO) rewriting in rm-adhesive categories. Our results open non-linear SqPO and DPO semantics to the rich static analysis techniques available from concurrency, rule algebra and tracelet theory.
Comments: 19+14 pages, LNCS style; ICGT 2021 conference paper extended version
Subjects: Logic in Computer Science (cs.LO)
MSC classes: 16B50, 60J27, 68Q42 (Primary) 60J28, 16B50, 05E99 (Secondary)
ACM classes: F.4.2; G.3; G.2.2
Cite as: arXiv:2105.02842 [cs.LO]
  (or arXiv:2105.02842v1 [cs.LO] for this version)

Submission history

From: Nicolas Behr [view email]
[v1] Thu, 6 May 2021 17:34:23 GMT (2442kb,D)

Link back to: arXiv, form interface, contact.