Concurrency theorems for non-linear rewriting theories
From MaRDI portal
Publication:2117255
DOI10.1007/978-3-030-78946-6_1zbMATH Open1489.68115arXiv2105.02842OpenAlexW3173342440MaRDI QIDQ2117255FDOQ2117255
Authors: Nicolas Behr, Russ Harmer, Jean Krivine 
Publication date: 21 March 2022
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.
Full work available at URL: https://arxiv.org/abs/2105.02842
Recommendations
Grammars and rewriting systems (68Q42) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)
Cites Work
- Abstract and concrete categories: the joy of cats
- Title not available (Why is that?)
- Restriction categories. I: Categories of partial maps
- Exponentiable morphisms, partial products and pullback complements
- Counting planar maps, coloured or uncoloured
- Graph Transformations
- Foundations of Software Science and Computation Structures
- Sesqui-Pushout Rewriting
- Fundamentals of algebraic graph transformation
- On the axioms for adhesive and quasiadhesive categories
- Adhesive and quasiadhesive categories
- Quasitopoi, logic and Heyting-valued models
- Restriction categories II: Partial map classification
- Rule algebras for adhesive categories
- Quasitoposes, Quasiadhesive Categories and Artin Glueing
- Finitary \(\mathcal{M}\)-adhesive categories
- How to delete categorically -- two pushout complement constructions
- -adhesive transformation systems with nested application conditions. Part 1: parallelism, concurrency and amalgamation
- Categorical frameworks for graph transformation and HLR systems based on the DPO approach
- AGREE -- algebraic graph rewriting with controlled embedding
- Title not available (Why is that?)
- Stochastic mechanics of graph rewriting
- Hereditary pushouts reconsidered
- Title not available (Why is that?)
- Title not available (Why is that?)
- Compositionality of rewriting rules with conditions
- Rewriting theory for the life sciences: a unifying theory of CTMC semantics
- Reversible sesqui-pushout rewriting
- Polymorphic sesqui-pushout graph rewriting
- Title not available (Why is that?)
- Knowledge representation and update in hierarchies of graphs
Cited In (17)
- Theoretical Aspects of Computing – ICTAC 2005
- Fundamentals of compositional rewriting theory
- Double-pushout rewriting in context: rule composition and parallel independence
- A theory for nondeterminism, parallelism, communication, and concurrency
- Graph rewriting and relabeling with PBPO\(^+\): a unifying theory for quasitoposes
- Compositionality of rewriting rules with conditions
- Sesqui-Pushout Rewriting
- Reversible sesqui-pushout rewriting
- Computational category-theoretic rewriting
- Computational Category-Theoretic Rewriting
- Algebraic laws for nondeterminism and concurrency
- A living monograph for graph transformation
- Fuzzy presheaves are quasitoposes
- Termination of graph transformation systems using weighted subgraph counting
- Adhesive DPO parallelism for monic matches
- A generalized concurrent rule construction for double-pushout rewriting: generalized concurrency theorem and language-preserving rule applications
- A generalized concurrent rule construction for double-pushout rewriting
Uses Software
This page was built for publication: Concurrency theorems for non-linear rewriting theories
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2117255)
