Compositionality of Rewriting Rules with Conditions
Nicolas Behr, Jean Krivine
TL;DR
This paper extends the framework of compositional rewriting rules to include conditions, using category theory to analyze rule composition in DPO and SqPO rewriting systems with application conditions.
Contribution
It introduces a category-theoretical approach to rule composition with conditions, demonstrating associativity and compatibility in complex rewriting systems.
Findings
Established a formal framework for rule composition with conditions
Proved associativity of rule composition in the extended setting
Analyzed the interplay between conditions and categorical constructions
Abstract
We extend the notion of compositional associative rewriting as recently studied in the rule algebra framework literature to the setting of rewriting rules with conditions. Our methodology is category-theoretical in nature, where the definition of rule composition operations encodes the non-deterministic sequential concurrent application of rules in Double-Pushout (DPO) and Sesqui-Pushout (SqPO) rewriting with application conditions based upon -adhesive categories. We uncover an intricate interplay between the category-theoretical concepts of conditions on rules and morphisms, the compositionality and compatibility of certain shift and transport constructions for conditions, and thirdly the property of associativity of the composition of rules.
Click any figure to enlarge with its caption.
Figure 1
Figure 2
Figure 3
Figure 4
Figure 5
Figure 6
Figure 7
Figure 8
Figure 9
Figure 10
Figure 11
Figure 12
Figure 13
Figure 0
Figure 1
Figure 10
Figure 11
Figure 12
Figure 13
Figure 14
Figure 15
Figure 16
Figure 17
Figure 18
Figure 19
Figure 2
Figure 20
Figure 21
Figure 22
Figure 23
Figure 24
Figure 25
Figure 26
Figure 27
Figure 28
Figure 29
Figure 3
Figure 30
Figure 31
Figure 32Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
\homepage
http://nicolasbehr.com \orcid0000-0002-8738-5040 ††thanks: corresponding author; the work of N.B. was supported by a Marie Skłodowska-Curie Individual fellowship (Grant Agreement No. 753750 – RaSiR)
\homepage
https://www.irif.fr/~jkrivine/homepage/Home.html \orcid0000-0001-7261-7462
Compositionality of Rewriting Rules with Conditions
Nicolas Behr
Jean Krivine
Université de Paris, CNRS, IRIF, F-75205, Paris, France
Abstract
We extend the notion of compositional associative rewriting as recently studied in the rule algebra framework literature to the setting of rewriting rules with conditions. Our methodology is category-theoretical in nature, where the definition of rule composition operations encodes the non-deterministic sequential concurrent application of rules in Double-Pushout (DPO) and Sesqui-Pushout (SqPO) rewriting with application conditions based upon -adhesive categories. We uncover an intricate interplay between the category-theoretical concepts of conditions on rules and morphisms, the compositionality and compatibility of certain shift and transport constructions for conditions, and thirdly the property of associativity of the composition of rules.
1 Introduction and relation to previous work
Graph rewriting has emerged as a powerful formalism to represent complex systems whose dynamics can be captured by a finite set of rules. The rule-based modeling approach, originally introduced by V. Danos and C. Laneve in the early 2000s Danos and Laneve (2003b, 2004, a), has developed into one of the main frameworks for the study of biochemical reaction systems (in the form of the two main frameworks Kappa Danos et al. (2007); Boutillier et al. (2018) and BioNetGenBlinov et al. (2004); Harris et al. (2016)). The approach proposes to model protein-protein interaction networks using graph rewriting models, in which proteins are the vertices of a graph whose connected components denote molecular complexes. A paradigmatic application scenario for rule-based methods in the systems biology community is the study of signaling pathways Danos et al. (2007, 2012), which are highly intricate biochemical reaction networks ubiquitous in living cells.
While the algorithmic aspects of graph rewriting are well-studied, programming language approaches to modeling with graphs are to date still a comparatively underdeveloped topic. Contrary to classical term rewriting, the notion of a match of a graph rewriting rule and its effects on a term (a graph) is subject to various definitions, allowing more or less control over possible rewrites. In addition, the mere nature of the graphs that are being rewritten impacts both the algorithmic design and expressiveness of graph rewriting. Category theory is a practical toolkit for equipping graphs with well-defined operational semantics. Double-Pushout (DPO) rewriting Corradini et al. (1997) is a widespread technique, partly because it does not yield side effects when rules are applied (which makes it amenable to static analysis for instance). However, when a graph rewriting rule entails node deletion, DPO semantics will not allow a match of such a rule to trigger if the node that is deleted is connected outside the domain of the match (which would yield side-effects). This has limited the practicality of DPO semantics in the context of biological modeling, where more permissive techniques have been employed. Sesqui-Pushout (SqPO) rewriting Corradini et al. (2006) in particular is the technique that is used to rewrite Kappa graphs Danos et al. (2007).
Quite orthogonal to the issue of defining rule matches and effects, having access to a fine-grained control over rule triggering is a key issue when graph rewriting is used as a modeling language. To this aim, graph rewriting rules have been equipped with application conditions Habel and Pennemann (2009); Ehrig et al. (2014), which can be seen as constraints that need to be checked “on the fly” when a rewrite rule is applied.
This paper presents a compositional variant of DPO and SqPO-type rewriting for rules with conditions in a general category-theoretical setting. From a mathematical perspective, while the framework of both types of rewriting developed here relies upon the original definitions of DPO-rewriting (see e.g. Ehrig et al. (2014)) and of SqPO-rewriting Corradini et al. (2006), new developments are necessary in order to obtain the desired compositionality properties. For rules without conditions, one of the core technical obstacles has proved to be establishing a compositional associativity property for sequential compositions of rewriting rules, which for the DPO-type case has been achieved in Behr and Sobocinski (2018, 2020); Behr et al. (2016a), and for the SqPO-type case in Behr (2019). The latter work also established a novel compositional concurrency property for SqPO-type rewriting theories. Lifting these results to the settings of rules with application conditions is the core contribution of this work.
The main motivation for our search for compositional rewriting theories is two-fold: in the setting of rewriting without conditions, the notion of rule algebras Behr et al. (2016a, b); Behr and Sobocinski (2018); Behr (2019) has been developed as a new mathematical framework to encode the concurrent and combinatorial interactions of rewriting rules, which in particular allows one to develop principled and novel analysis techniques for stochastic rewriting systems Behr et al. (2016a); Behr and Sobocinski (2018); Behr et al. (2020a). Especially the recent results of Behr et al. (2020a) hint at the intimate interplay of design choices in constructing rewriting systems with regards to their dynamical properties, and with the potential of greatly improving the tractability of the analysis of such systems via judiciously chosen constraints on objects and rewriting rules (such as implemented in the form of rigidity constraints in the Kappa formalism Danos et al. (2008)).
Our second main motivation originates in the desire to analyze rewriting systems statically, rather than via simulation-based techniques. While the traditional rewriting theory generally approaches this problem from the viewpoint of derivation traces (i.e. sequences of rule applications to a given input graph), we posit that a viable alternative approach may consist in focusing instead on sequential rule compositions, which in particular when combined with application conditions is anticipated to yield a powerful framework to study the causality of rewriting systems. For certain specialized applications of DPO-type graph rewriting, namely those in the well-established field of chemical graph rewriting Benkö et al. (2003); Banzhaf et al. (2015); Andersen et al. (2016), such types of analyses have already proven very fruitful Andersen et al. (2018b, a); Fagerberg et al. (2018); Andersen et al. (2019). Therefore, we believe that our compositional refinements described in the present paper can provide a significant contribution to future algorithm developments in this field.
1.1 Related work
1.1.1 Traditional rewriting literature
First and foremost, the work presented in this paper relies heavily upon the rich literature on categorical rewriting theories with its almost 50 year long history. The introduction of the seminal concept of adhesive categories by Lack and Sobociński in the early 2000s Lack and Sobociński (2004, 2005) and its refinement to -adhesive categories in the work of Ehrig et al. Ehrig et al. (2006b, 2010); Habel and Plump (2012a); Braatz et al. (2014); Ehrig et al. (2014) resulted in a powerful mathematical framework for Double-Pushout (DPO) rewriting, and in particular permitted to unify numerous concepts from the earlier graph rewriting literature Rozenberg (1997). While -adhesive categories have been demonstrated to be capable of describing a broad range of data structures of relevance in applications of rewriting theories (see e.g. Ehrig et al. (2006a) and Behr and Sobocinski (2020) for curated lists of examples), it is only via a second key refinement of the rewriting theory that more elaborate data structures such as e.g. chemical molecules may be encoded: the theory of constraints and application conditions. This theory had been a well-established component of some of the earliest categorical formulations of graph rewriting theories since the 1980s by Habel et al. Ehrig and Habel (1986); Habel et al. (1996), and was later generalized to the -adhesive setting as utilized in the present paper in Habel and Pennemann (2009); Pennemann (2008); Ehrig et al. (2014).
Building upon this extensive body of work, and motivated by applications to modeling in the life sciences (cf. Behr and Krivine (2020) and comments below), we demonstrate in the present paper that by requiring the underlying -adhesive category to satisfy certain additional technical assumptions, one obtains a refined variant of DPO-semantics that is well suited for developing novel static analysis techniques for rewriting systems. Referring to Remarks 3.9 and 4.32 in the main text for the precise technical details of the relationship between our “refined” and the “traditional” DPO semantics, our work moreover extends the traditional DPO-theory by providing an associativity theorem which had not been previously known in the literature (cf. Theorem 4.39).
The second type of categorical rewriting semantics considered in this paper is the Sesqui-Pushout (SqPO) rewriting theory introduced in Corradini et al. (2006). Despite the importance of this type of semantics especially in the modeling of biochemical reaction systems (cf. Section 1.1.2), the approach had been considerably less well-developed than the DPO-variant, lacking in particular a theory of constraints and application conditions as well as notions of concurrency and associativity theorems. While in Danos et al. (2014) an attempt had been made to identify a special sub-class of SqPO-type rewriting systems over -adhesive categories in which the rewriting semantics coincides with that of the DPO-setting, and thus allowing to reuse the theory of application condition from this setting, this special case of “reversible” SqPO-rules constitutes too strong a restriction in order to study the rewriting systems of relevance e.g. in biochemistry (Section 1.1.2). Building upon our earlier work on SqPO-rewriting in the setting of rules without conditions Behr (2019), and taking advantages of the close analogies with our refined DPO-type framework as presented in comprehensive technical detail in the present paper, we develop these missing elements of SqPO-rewriting theory (cf. Section 5). Referring to Corradini et al. (2006) for an extended discussion, it might finally be worthwhile to note that SqPO-semantics in the setting of (-) linear rules and (-) monic matches (as is the case in the present paper) is well known to coincide with single-pushout (SPO) semantics Löwe (1993).
1.1.2 Bio- and organo-chemistry
An intriguing trend in modern rewriting theory over the past 15 years has been the development of rule-based modeling approaches in biochemistry (Kappa Boutillier et al. (2018), BioNetGen Harris et al. (2016)) and in organic chemistry (MØD Andersen et al. (2016)), which are based upon SqPO- and DPO-type semantics, respectively. While an detailed discussion of the numerous sophisticated theoretical and algorithmic techniques (including in particular various notions of static analysis techniques, cf. e.g. Danos et al. (2007, 2008, 2012); Murphy et al. (2010); Petrov et al. (2012); Abou-Jaoudé et al. (2016); Camporesi et al. (2017); Feret et al. (2012) and Benkö et al. (2003); Banzhaf et al. (2015); Fagerberg et al. (2018); Andersen et al. (2018b, 2019)) is beyond the scope of the present paper, suffice it here to comment on a salient technical point: notably, many of the developments in the aforementioned frameworks were not explicitly rooted in categorical rewriting theory itself, despite the foundations of the two fields upon this type of theory. We recently demonstrated in Behr and Krivine (2020) that based upon the results of the present paper, one may not only reformulate equivalently the current implementations of chemical rewriting theories, but one may also take advantage of our novel compositionality and associativity results in order to formulate rule algebra and tracelet theories (see below) to develop new approaches to the static analysis of complex reaction systems and their dynamics. The encodings of chemical molecules and their reactions as reported in Behr and Krivine (2020) in both the bio- and the organo-chemical settings are based upon typed variants of undirected simple graphs that satisfy suitable sets of constraints, which is why we will take undirected simple graphs and rewriting rules thereof as a running example throughout this paper.
1.1.3 Rule algebra and tracelet theory
Rule-based modeling approaches for chemical reaction systems are part of a larger class of theories known as stochastic rewriting theories. Over the past five years, we have demonstrated that one may express such systems based upon the general theory of continuous-time Markov chains (CTMCs) Norris (1998), leading to the so-called stochastic mechanics framework Behr et al. (2016a); Behr and Sobocinski (2018, 2020); Behr (2019); Behr et al. (2020a); Behr and Krivine (2020). At the core of this framework is the notion of rule algebras, which encode the non-determinism in the choices of admissible matches in sequential compositions of rules via the construction of a certain binary operation (on a vector space whose basis is indexed by equivalence classes of linear rules). As explained in detail in Behr and Sobocinski (2020); Behr et al. (2020a), since the “blueprint” of this type of construction in the general mathematics and in particular combinatorics literature is provided by the operations of derivative and multiplication by formal variables acting upon the space of formal power series, the aforementioned binary operation must satisfy two fundamental technical properties: it must be associative (in the standard sense of associativity of binary operations), and it must possess a neutral element. Referring to loc. cit. for the precise technical details, the former property requires an associativity theorem for sequential rule compositions, while the latter property requires the underlying category to possess a (strict) -initial object. Finally, in order to formulate the stochastic rewriting theories themselves, it is necessary to endow the rule algebras with canonical representations, the construction of which in turn hinges on the concurrency theorems for the respective sort of rewriting. The technical results presented in the present paper have been recently applied in Behr and Krivine (2020) to establish precisely the rule algebra theories for linear rules with conditions both in DPO- and in SqPO-semantics.
A second recent line of developments has been the introduction of the theory of tracelets in Behr (2020), which also relies heavily on the technical results of the present paper. Intuitively, while the aforementioned rule algebraic constructions aim to reason based upon rule algebra products of linear rules (which, in a sense, encode “sums over all possible ways to compose rules”), the concept of tracelets is more directly related to the classical rewriting-theoretical notion of derivation traces Rozenberg (1997); Ehrig et al. (2006a); Corradini et al. (2006). We refer the interested readers to Behr (2020) for an in-depth review of the relationship of tracelet theory with the traditional concepts of concurrency and related static analysis techniques, mentioning here only the fact that yet again this new theory relies upon the notion of associative compositional rewriting theories.
1.2 A motivating example: rewriting simple graphs
Since our main constructions will be somewhat technical, let us start with a simple example in order to provide the readers with an intuitive picture of the main concepts. To this end, consider the task of defining a sound notion of rewriting for undirected simple graphs, the type of graphs where at most one undirected edge may exist between any two given vertices of the graph, as opposed to undirected multigraphs. While there exist various attempts in the literature to encode simple graphs directly via a suitable category-theoretical construction (cf. e.g. Adámek et al. (1990); Corradini et al. (2006); Braatz and Brandt (2008); Danos et al. (2014); Braatz et al. (2014)), the disadvantage of such an approach consists of the fact that these categories are not -adhesive, and thus do not permit to profit from the constructions for -adhesive categories available in the general DPO-rewriting framework. In fact, constructions of simple graph categories such as RDFGraph of Braatz and Brandt (2008) (for a notion of directed typed simple graphs called RDF graphs) or SGraph of Adámek et al. (1990); Corradini et al. (2006) (of undirected simple graphs) are well known to lack uniqueness of pushout complements (POCs), quintessential in defining DPO-semantics (Section 4) as well as (compositional) SqPO-semantics (Section 5) in the first place. Albeit several elaborate workarounds to this problem have been considered in the literature (such as e.g. the minimal-POC-PO semantics for RDF-graph rewriting in Braatz and Brandt (2008)), these workarounds introduce alterations to the rewriting semantics that do not necessarily reflect the intuitions one might have for simple graph rewriting from a mathematics or general applied sciences background.
To circumvent these issues, we will instead start our construction from a “host category” of undirected multigraphs111Interestingly, the category constitutes one of the simplest non-trivial examples of a category that is -adhesive, but not adhesive, unlike the prototypical example of an adhesive category Lack and Sobociński (2004). Padberg (2017); Behr and Sobocinski (2020); Behr and Krivine (2020) that is itself -adhesive and satisfies all requirements to admit compositional rewriting theories of both DPO- and SqPO-type. Imposing the aforementioned structural constraint prohibiting parallel edges via the framework of conditions, we obtain an algorithmically versatile implementation of simple graphs. Following the rewriting theory paradigms, one may envision manipulating graphs via application of graph rewriting rules. Intuitively, specifying a rewriting rule amounts to providing the following data:
- •
An Input pattern ,
- •
an Output pattern , and
- •
a Kontext pattern together with embedding morphisms and .
Then in order to apply a rule to a graph , one has to
specify an embedding of the input pattern into (i.e. one has to select a particular occurrence of the pattern in ), referred to as a match, 2. 2.
in , replace with , and 3. 3.
“glue” a copy of onto (according to the embedding morphism ).
For example, one may consider the rewriting rules
[TABLE]
which implement the manipulations of adding a new edge between two vertices () and deleting an edge between two vertices (). However, in the setting of rewriting of simple graphs, the above tentative definition for the rewriting of graphs is as of yet incomplete. For example, given the graph below,
[TABLE]
if we were to apply our edge creation rule at a match comprising the vertices marked and , we would produce the non-simple graph depicted below (with the newly produced edge):
[TABLE]
Therefore, in order to ensure that our transformations via application of rules keep intact the constraint of graphs to be simple, we need to endow the rules with application conditions. While this approach is well known in the rewriting literature, it turns out that, via a careful re-implementation of the traditional framework, some interesting mathematical structures may be uncovered: rules with conditions are endowed with a structure of composition operation that allows one to synthesize sequences of causally sound rewriting steps without reference to a host object. Crucially, this operation can be shown to be associative. Contact with the traditional techniques of rewriting is then made in the form of a suitable adaption of the concurrency theorem, whereby a sequence of rule applications to a given object can always be equivalently described by a “one-shot” application of a sequential composite of the rules to that object (i.e. in a sense characterizing the effect of the sequential rule applications by the application of a single composite rule). The most subtle part of our results then consists in a certain compositional associativity property present in triple sequential compositions of rules.
To relate to the example at hand, in addition to using the standard application condition technique to express constraints on rules (such as the constraint that the edge creation rule should only be applied to a graph if its input is matched to two vertices that are not already linked), we will also be able to compute causal information, such as e.g. that applying the edge creation rule followed by applying the edge deletion rule (in a fashion such as to delete the previously created edge) will lead to a rule with no effect, which can only be applied at two vertices that cannot be already linked (transforming the graph identically). Finally, we will present examples of the property of associativity in Examples 4.41 and 5.53 in the setting of DPO- and SqPO-type rewriting theories, respectively.
1.3 Overview of main results and structure of the paper
The main results of this paper are summarized as follows (cf. Figure 1):
- •
We provide a self-contained account of all category-theoretical prerequisites and specialized definitions extracted from the rich literature on categorical rewriting theories (Sections 2 and 3; Appendix 6), intended not least as an entry-point for the general applied category theory audience.
- •
For Double-Pushout (DPO) rewriting (Section 4), we identify a set of sufficient assumptions on the underlying categories such that the resulting rewriting theories have suitable compositionality properties (in the sense of a certain form of concurrency and associativity properties of sequential rule compositions). This part of our theory is thus to a large extent a careful “fine-tuning” of results from the traditional DPO-rewriting literature, combined with a number of original results.
- •
For Sesqui-Pushout (SqPO) rewriting (Section 5), we present the first-of-its-kind category-theoretical compositional SqPO-type rewriting theory for rules with conditions, profiting from fruitful analogies to results in the DPO-type theory as presented in the first part of the paper.
2 Category-theoretical preliminaries
Rewriting in its modern formulations is a concept that heavily relies on specific types of categorical structures. In this section, we collect all the necessary prerequisites that allow one to formulate consistent frameworks of associative rewriting theories with conditions on objects and morphisms, in both the Double-Pushout (DPO) and the Sesqui-Pushout (SqPO) approaches. While many of the mathematical details of these setups are by now standard in the literature, we will emphasize the specific additional conditions that are required in order to guarantee associativity (in the sense of Behr and Sobocinski (2018)) and compositionality, where both of these properties concern concurrent compositions of rules with conditions.
2.1 -adhesive categories
We begin by quoting a number of essential definitions and standard results from the literature, where our main references will be Braatz et al. (2014); Habel and Pennemann (2009); Ehrig et al. (2014) (see also Radke (2016); Schneider et al. (2017) for some more recent works). Let us first recall the notion of -adhesive categories, which is the most general mathematical setting currently known that allows one to define DPO- and SqPO-type rewriting theories, and which generalizes adhesive categories Lack and Sobociński (2005).
Definition 1** (Braatz et al. (2014), Def. 2.1)**
Let be a category, and let be a class of monomorphisms. Then the data defines an -adhesive category if the following requirements are satisfied:
- (i)
The class contains all isomorphisms and is closed under
- (a)
composition*,*
[TABLE] 2. (b)
decomposition*,*
[TABLE] 2. (ii)
* has pushouts and pullbacks along morphisms, i.e. pushouts of spans and pullbacks of cospans where at least one of the two morphisms of the (co-) span is in exist.* 3. (iii)
morphisms are closed under pushouts and pullbacks:* if in the diagram below is a pushout, then implies , while if is a pullback, then implies :*
[TABLE] 4. (iv)
Pushouts along -morphisms are -van Kampen (-VK) squares (also referred to as vertical weak VK squares in the literature):* given a commutative cube in as shown below, where the bottom square is a pushout along an -morphism , the back faces are both pullbacks, and if , then the top face is a pushout if and only if the two front faces are pullbacks.*
[TABLE]
For certain applications, it is also of interest to consider a variant of the definition called weak -adhesive categories, which are categories in which all of the above axioms hold except for the -VK property; the latter is modified to the weak -VK property:
- (iv)’
Pushouts along -morphisms are weak -van Kampen (-VK) squares:* given a commutative cube in as shown in (5), where the bottom square is a pushout along an -morphism , the back faces are both pullbacks, and if*
[TABLE]
then the top face is a pushout if and only if the two front faces are pullbacks.
Strictly speaking, several points in the above definition are redundant, since the closure under isomorphisms and the decomposition property are known to follow directly from closure under compositions and stability of -morphisms under pullbacks (see Appendix B for the former property). It is moreover worthwhile to note that in some of the earlier literature (cf. Ehrig et al. (2010) for a review), several authors referred to categories satisfying properties as vertical weak -adhesive categories, and by analogy to categories satisfying and only the second alternative of (i.e. that the “horizontal” morphisms and should be in ) as horizontal weak -adhesive categories. In practice (cf. e.g. Behr and Sobocinski (2020) for a review and a list of examples), most categories considered in the rewriting literature in fact qualify as both horizontal and vertical weak -adhesive categories, yet since a few exceptions only satisfy the vertical variant, and since moreover in the relevant proofs only this variant is required, the standard convention has become to refer to the vertical variant simply as -adhesive categories Braatz et al. (2014). -adhesive categories enjoy a number of special properties (some of which referred to in the literature as high-level replacement (HLR) properties) that will be important to our main constructions. We collect these properties in Appendix A.
As advocated in particular in the work of Ehrig Braatz et al. (2014), one of the optimal compromises for a general setting in which DPO (and, as we shall see, also SqPO) rewriting theories involving constraints on objects and morphisms can be formulated efficiently is provided by -adhesive categories with certain additional special properties. A central role in this setup is played by the following concepts:
Definition 2** (-initial object; Braatz et al. (2014), Def. 2.5)**
An object of an -adhesive category is defined to be an -initial object if for each object there exists a unique monomorphism , which is moreover required to be in . An -initial object is said to be strict if for each object , every morphism must be an isomorphism.
Lemma 1** (Braatz et al. (2014), Fact 2.6)**
If an -adhesive category possesses an -initial object , then the category has finite coproducts, and moreover the coproduct injections are in . In particular, the coproduct of two objects is then given as the pushout of the span .
For later convenience, we present a number of consequences of an -adhesive category possessing a (strict) -initial object in Appendix D.
Definition 3** (Finite objects, finitary categories, finitary restrictions; Braatz et al. (2014), Def. 2.8 and Def. 4.1)**
Let be an -adhesive category. An object is said to be finite, if there exist only finitely many isoclasses of -morphisms into (i.e. if “ has finitely many -subobjects”). is finitary if all its objects are finite. Let denote the full subcatgory of spanned by finite objects, and let denote the class of -morphisms between finite objects. Then we refer to as the finitary restriction of .
Theorem 1** (Braatz et al. (2014), Thm. 3.14)**
The finitary restriction of an -adhesive category is a finitary -adhesive category.
Definition 4** (Epi--factorizations; cf. e.g. Habel and Pennemann (2009), Def. 3)**
An -adhesive category is said to possess an epi--factorization if every morphism of can be factorized into an epimorphism and a monomorphism such that , and such that this factorization is unique up to isomorphism.
It is worthwhile to note that a large class of -adhesive categories of practical importance (see e.g. the examples listed below) indeed possess an epi--factorization.
Example 1
Referring to (Braatz et al., 2014, Ex. 2.3ff) and (Ehrig et al., 2006a, Section 4.2) for further details, well-known examples of -adhesive categories with -initial objects include:
- •
, the category of sets and (total) set functions, with the class of all injective set morphisms, and with the -initial object the empty set .
- •
, the category of undirected multigraphs Behr and Sobocinski (2020)** and graph homomorphisms, with the class of all injective homomorphisms of , and with -initial object the empty graph .
- •
, the category of directed multigraphs, with the class of all injective graph homomorphisms, and with -initial object the empty graph .
- •
, the category of typed graphs and morphisms thereof (constructed as the slice category for some fixed type graph ), with the class of all injective typed graph homomorphisms.
- •
The categories of Petri nets and of elementary Petri nets (Braatz et al., 2014, Ex. 2.3ff) are -adhesive and -initial for certain classes of .
All categories in the above list possess an epi--factorization, as do their finitary restrictions. For example, in , every graph homomorphism can be factored into the a surjective composed with an injective graph homomorphism. Interestingly, the well-known non-examples, which are certain categories of (typed or untyped) attributed graphs, fail to possess an -initial object and an epi--factorization. There exist a number of functorial constructions that allow one to construct finitary -adhesive categories with the desired properties from known such categories. We refer the reader to (Braatz et al., 2014, Sec. 5) for the details.
One of the most important additional properties required in view of compositionality of rewriting rules is the following one:
Definition 5** (-effective unions)**
Let be an -adhesive category, for a class of monomorphisms. Then is said to possess -effective unions if for every commutative diagram as below where all morphisms except are in , where is a pushout and where the exterior square is a pullback,
[TABLE]
the morphism is in .
While adhesive categories (which constitute a special case of -adhesive categories where ) are well known to posses (-) effective unions Lack and Sobociński (2005), we are not aware of a set of sufficient conditions to ensure the property of -effective unions in the general -adhesive case. Referring to Behr and Sobocinski (2020) for an extended discussion, for some of these more general cases such as for the category Behr and Krivine (2020) the following technical result allows one to verify the property:
Theorem 2** (Behr and Sobocinski (2020), Thm. 1.15)**
Let be a horizontal weak -adhesive category. Then in a diagram of the form (6), the morphism is a monomorphism (however not necessarily in the class ).
Finally, the property of balancedness defined below will be an essential ingredient for our rewriting framework (cf. Theorem 3).
Definition 6** (compare Lack and Sobociński (2005), Lem. 4.9)**
A category is said to be balanced if every morphism that is both a mono- and an epimorphism is an isomorphism.
2.2 Additional prerequisites for the Sesqui-Pushout (SqPO) framework
Referring to Behr (2019) for a more extensive presentation, we focus here on quoting some necessary background materials, and on discussing the general -adhesive setting.
Definition 7** (Final Pullback Complement (FPC); Corradini et al. (2006); Löwe (2015))**
Given a commutative diagram of the form
[TABLE]
a pair of morphisms is a final pullback complement (FPC) of a pair if
- (i)
* is a pullback of , and* 2. (ii)
for each collection of morphisms as in (7), where is pullback of and where , there exists a morphism with and that is unique (up to isomorphisms).
Lemma 2** (cf Löwe (2015), Fact 2, and Corradini et al. (2006), Lemma 2ff)**
For an arbitrary morphism , is an FPC of and vice versa. Moreover, every pushout square is also an FPC square. FPCs are unique up to isomorphism and preserve monomorphisms.
If we are working over an adhesive category (i.e. an -adhesive category where coincides with the class of all monomorphisms Braatz et al. (2014)), the stability of monomorphisms under FPCs as guaranteed by Lemma 2 will be sufficient for our purposes. However, in the more general -adhesive setting, we will have to require the following stronger property:
Definition 8** (Stability of -morphisms under FPCs)**
Let be an -adhesive category (for a class of monomorphisms). Then -morphisms in are said to be stable under FPCs if whenever for a pair of morphisms with in and arbitrary, if such that is the FPC of , then .
2.3 Summary: full set of assumptions for DPO and SqPO rewriting
Combining all findings of the previous two sections (together with some insights from the constructions presented in the following sections), we present here sets of requirements for associative Double-Pushout (DPO) and Sesqui-Pushout (SqPO) rewriting that admit conditions on both objects and morphisms. As we were primarily motivated by deriving a sufficient set of assumptions in order to study rewriting theories in the life-sciences (as in Behr and Krivine (2020)), we have not attempted to prove that the assumptions provided are strictly necessary, albeit the latter point might in itself provide an interesting direction for future work.
Assumption 1** (Associative DPO rewriting with conditions)**
We assume that is an -adhesive category with epi--factorization. We also assume that is balanced, possesses a strict -initial object and -effective unions.
Note that according to (Lack and Sobociński, 2005, Lem. 4.9), all adhesive categories are balanced, while for the general case the requirement is more non-trivial to demonstrate. An example of the former class which also satisfies all additional assumptions stated above is given by the category of directed multigraphs Lack and Sobociński (2005), while a more general example of an -adhesive category satisfying Assumption 1 is given by the category Behr and Sobocinski (2020); Behr and Krivine (2020) of undirected multigraphs.
Assumption 2** (Associative SqPO rewriting with conditions)**
We assume that is an -adhesive category satisfying Assumption 1, and we assume in addition that for all pairs of composable -morphisms , the final pullback complement exists, and moreover that -morphisms are stable under FPCs.
According to Corradini et al. (2015), examples of -adhesive categories for which the existence of FPCs as required in Assumption 2 is guaranteed are those categories that possess an -partial map classifier (cf. (Corradini et al., 2015, Thm. 1 and Sec. 2–5); compare Cockett and Lack (2003)). While we refer the interested readers to these references for the full technical details, we mention here that examples of categories possessing an -partial map classifier include the -adhesive categories and , all presheaf categories, numerous variants of typed or polarized graphs, and more generally all slice categories with a topos and . To the best of our knowledge there are no known sufficient conditions to guarantee this stability property, other than a result by J.R.B. Cockett and S. Lack (Cockett and Lack, 2003, Prop. 4.16 and Example 4.17), which however in effect only reaffirms the case of being an adhesive category. In the general -adhesive setting, -stability under FPCs will have to be verified at a case-by-case level. Note that the guaranteed existence of final pullback complements in the configurations encountered in SqPO rewriting will drastically simplify the framework, and is in fact necessary to guarantee associativity as discussed in Behr (2019).
3 Conditions on objects and morphisms
The central concepts of the framework of conditions are the following notions of constraints (i.e. conditions over objects), application conditions (i.e. conditions over morphisms) and the associated notions of satisfiability. We quote the precise definitions from Ehrig et al. (2014), and also from Habel and Pennemann (2009), where some important clarifying details are given (on the notion of satisfiability on objects and morphisms).
3.1 Core definitions
Definition 9** (Conditions;
cf. Ehrig et al. (2014), Def. 3.3, and Habel and Pennemann (2009), Def. 4)**
(Nested) conditions are recursively defined as follows:
- (i)
Trivial condition:* for every object , is a condition over .* 2. (ii)
“Transported” conditions:* for every object , for every222It is here that our restriction to -morphisms in the formulation of conditions reflects our choice of framework, i.e. that of -satisfiability (for -morphisms). We refer the interested readers to Habel and Pennemann (2009) for the proof that this is in fact the most general framework available when working with -morphisms in matches and rewriting rules only, i.e. generalizing morphisms in conditions of arbitrary morphisms in this setting does not lead to more expressivity. -morphism and for every condition over , is a condition over .* 3. (iii)
Negation:* for every condition over , is a condition over .* 4. (iv)
Conjunction:* given a family of conditions (for some index set ) over an object , is a condition over .*
The following two shorthand notations are customary:
[TABLE]
The precise meaning of the above definitions is specified via the associated notions of satisfiability, which are also defined inductively:
- S1
Every -morphism satisfies the trivial condition .
- S2
Given -morphisms and as well as a condition over , the morphism is defined to satisfy the condition if and only if there exists an -morphism such that and such that satisfies the condition ,
[TABLE]
- S3
Given an -morphism and a condition over , satisfies if it does not satisfy . If (for some indexing set ) is a family of conditions over , satisfies if it satisfies each of the application conditions .
For an -morphism , we write
[TABLE]
to denote that satisfies the condition . Two application conditions over some object are equivalent, denoted , if and only if for all -morphisms , i.e. for arbitrary with as an -subobject, we find that
[TABLE]
Finally, a (nested) condition or constraint on an object is defined as a (nested) condition over the -initial object , and the associated notion of satisfiability of constraints as satisfaction of the condition over by the -initial morphism Habel and Pennemann (2009):
- C1
Every object satisfies .
- C2
An object satisfies the condition if there exists an -morphism such that and .
- C3
Given an object and a condition over the -initial object , satisfies if it does not satisfy .
- C4
If (for some indexing set ) is a family of conditions over , satisfies if it satisfies each of the conditions .
It may be instructive to the readers to explicitly parse the potentially somewhat counter-intuitive definition of conditions on objects in a concrete example:
Example 2
Given an object , a condition of the form “ contains an -subobject ” is expressed in the present framework as , since by virtue of the definition of satisfiability of conditions on objects, iff there exists an -morphism such that :
[TABLE]
Next, consider the following example for illustration of the concept of nested conditions. We will, in practice, be interested exclusively in finite nested conditions, i.e. in sequences (or in general directed acyclic graphs) of conditions that ultimately end in an instance of a condition of the form . In this sense, the example below is sufficiently generic.
Example 3
The condition below (on undirected multigraphs)
[TABLE]
parses more explicitly into the diagram
[TABLE]
*expressing the condition that a morphism p:\vbox{\hbox{\includegraphics{diagrams/nacExB1.pdf}}}\hookrightarrow G satisfies the condition if contains at least one other vertex
(which is the information encoded in the first part of the condition), and such that
and
are linked by an edge. Moreover, the -morphism in the above diagram automatically exists if the entire condition is satisfied. This is in fact a typical example of refinement (or -coverability Habel and Pennemann (2009)), whereby the condition is refined by the condition .*
3.2 A refined notion of shift construction
One of the key concepts in the theory of rewriting with conditions is the notion of shift construction, which is, in essence, a category-theoretical characterization of the interplay between conditions and extensions of their domains. We introduce here an optimized version of the classical shift construction presented in Ehrig et al. (2014)) (which is itself a variant of an earlier construction as reviewed in Habel and Pennemann (2009)). Our optimization hinges on the assumed properties of the underlying -adhesive categories according to Assumption 1. We believe this optimization will be of key importance in future developments of algorithms and software implementations of our framework. The following theorem is at the basis of our novel construction:
Theorem 3
Given an -adhesive category satisfying Assumption 1, consider a commutative diagram of the form below,
[TABLE]
where the square marked is a pushout, where (and thus by stability of -morphisms under pushout also ), {\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}e_{1}},{\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}e_{2}}\in\mathcal{M} and {\color[rgb]{0,0,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.4}X}=\mathsf{PB}(B_{1}{\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}\xrightarrow{e_{1}}E\xleftarrow{e_{2}}}B_{2}) (and thus by stability of -morphisms under pullbacks also {\color[rgb]{0,0,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.4}b_{1}},{\color[rgb]{0,0,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.4}b_{2}}\in\mathcal{M}, plus due to the decomposition property of morphisms, also {\color[rgb]{0,0,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.4}x}\in\mathcal{M}). Then the following holds: the morphism {\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}e} is an epimorphism if and only if the exterior square is a pushout.
Proof 3.4**.**
“” direction: Suppose that the exterior square in (14) is a pushout. Let e={\color[rgb]{0,0,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.4}m}\circ{\color[rgb]{0,0,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.4}f} be the epi--factorization of (with {\color[rgb]{0,0,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.4}(f:D\rightarrow F)}\in\mathsf{epi}(\mathbf{C}) and {\color[rgb]{0,0,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.4}(m:F\rightarrow E)}\in\mathcal{M}). Then construct the commutative diagram presented in the left part of (15) as follows: form the two pullbacks {\color[rgb]{0,0,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.4}B_{i}^{\prime}}=\mathsf{PB}({\color[rgb]{0,0,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.4}F\rightarrow}E\leftarrow B_{i}), which by the universal property of pullbacks also induces morphisms {\color[rgb]{0,0,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.4}B_{i}\rightarrow B_{i}^{\prime}} (for ); according to Lemma C.56 of Appendix C, we conclude that {\color[rgb]{0,0,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.4}B_{1}^{\prime}}\cong B_{1} and {\color[rgb]{0,0,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.4}B_{2}^{\prime}}\cong B_{2}. Next, let {\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}X^{\prime}}=\mathsf{PB}({\color[rgb]{0,0,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.4}B_{1}^{\prime}\rightarrow F\leftarrow B_{2}^{\prime}}); by the universal property of pullbacks, this implies the existence of morphisms A{\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}\rightarrow X^{\prime}} and {\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}X^{\prime}\rightarrow}X (and by decomposition of -morphisms, the latter is in ). Since the square just constructed is a pullback, the bottom square a pushout along -morphisms (and thus a pullback), and since, due to {\color[rgb]{0,0,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.4}B_{i}^{\prime}}\cong B_{i} (for ) and {\color[rgb]{0,0,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.4}m}\in\mathcal{M}, Lemma A.54(i)c entails that the bottom left and bottom front vertical squares are pullbacks, we conclude via invoking pullback-pullback decomposition (Lemma A.54(iii)a) that also the bottom back and bottom right vertical squares are pullbacks. Thus by virtue of stability of isomorphisms under pullbacks (Lemma A.54(i)d), {\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}X^{\prime}}\cong X. Moreover, the -van Kampen property entails that the middle horizontal square is a pushout, whence by uniqueness of pushouts up to isomorphism, we have that {\color[rgb]{0,0,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.4}F}\cong E, which proves the claim that e={\color[rgb]{0,0,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.4}m}\circ{\color[rgb]{0,0,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.4}f}\in\mathsf{epi}(\mathbf{C}).
“” direction:
Suppose that and that the exterior square in (14) is a pullback. Construct the commutative diagram depicted in the right part of (15) as follows: start by forming the pushout {\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}F^{\prime}}=\mathsf{PO}(B_{1}\leftarrow X\rightarrow B_{2}), which by the universal property of pushouts (recalling that the top square is by assumption also a pushout) furnishes morphisms {\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}f^{\prime}}:D{\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}\rightarrow F^{\prime}} and {\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}m^{\prime}}:{\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}F^{\prime}\rightarrow}E such that e={\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}m^{\prime}}\circ{\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}f^{\prime}}. By stability of -morphisms under pushouts, the morphisms {\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}B_{1}\rightarrow F^{\prime}} and {\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}B_{2}\rightarrow F^{\prime}} are in . The top commutative cube thus precisely satisfies the properties necessary to invoke the theorem in the “*” direction, in order to conclude that {\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}f^{\prime}}\in\mathsf{epi}(\mathbf{C}). Since by assumption , and since e={\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}m^{\prime}}\circ{\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}f^{\prime}}, invoking decomposition of epimorphisms yields that {\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}m^{\prime}}\in\mathsf{epi}(\mathbf{C}). On the other hand, since by assumption the bottom square is a pullback, invoking the property of -effective unions permits us to conclude that {\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}m^{\prime}}\in\mathcal{M}. As the underlying category is assumed to be balanced, and since , we conclude that {\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}m^{\prime}}\in\mathsf{iso}(\mathbf{C}), i.e. {\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}F^{\prime}}\cong E, which proves that the bottom square is a pushout (by uniqueness of pushouts, and since pushouts along -morphisms are also pullbacks). *
An interesting consequence of the above theorem is the following result, which allows one to compare our technical framework more directly with the traditional literature:
Corollary 3.5**.**
In an -adhesive category satisfying Assumption 1, given two -morphisms , let the -morphisms
[TABLE]
be defined (uniquely up to isomorphisms) as follows: denoting by {\color[rgb]{0,0,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.4}(C_{1}\hookleftarrow X\hookrightarrow C_{2})} the pullback of the cospan , define {\color[rgb]{0,0,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.4}(c_{1}^{\prime},c_{2}^{\prime})} as the pushout of this span, and let {\color[rgb]{0,0,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.4}d} be defined as the induced morphism from {\color[rgb]{0,0,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.4}\bar{D}} into . Then the cospan {\color[rgb]{0,0,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.4}(c_{1}^{\prime},c_{2}^{\prime})} is jointly epimorphic.
Proof 3.6**.**
Given that (which follows from stability of -morphisms under pullback and pushout, and from the property of -effective unions, respectively), construct the following commutative diagram:
[TABLE]
Here, given the unique -morphisms {\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}(\mathop{\varnothing}\hookrightarrow C_{1})}, {\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}(\mathop{\varnothing}\hookrightarrow C_{2})} and {\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}(\mathop{\varnothing}\hookrightarrow X)} from the -initial object , and with {\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}(C_{1}\hookrightarrow C_{1}+C_{2}\hookleftarrow C_{2})} the pushout of {\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}(C_{1}\hookleftarrow\mathop{\varnothing}\hookrightarrow C_{2})}, the existence of the morphism {\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}(e:C_{1}+C_{2}\rightarrow\bar{D})} follows by the universal property of pushouts. Then it follows via invoking Theorem 3 that {\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}e} is an epimorphism.
We will take advantage of this corollary when discussing the results of Theorem 3.7 below as well as the notion of DPO-type rule compositions in its various forms in Section 4.1. Theorem 3.7 below constitutes another interesting consequence of Theorem 3, deriving an algorithmic refinement of the so-called construction, which allows one to extend application conditions to larger contexts:
Theorem 3.7** (Shift construction; compare Habel and Pennemann (2009), Thm. 5 and Lem. 3, Ehrig et al. (2014) Lem. 3.11).**
Given an -adhesive category satisfying Assumption 1, there exists a shift construction, denoted , such that for every condition over an object and for every -morphism , an -morphism {\color[rgb]{0.6,0.6,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.6,1}n}\circ p:P{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}\rightarrow H} (with {\color[rgb]{0.6,0.6,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.6,1}n}\in\mathcal{M}) satisfies the condition iff ({\color[rgb]{0.6,0.6,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.6,1}n}:Q{\color[rgb]{0.6,0.6,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.6,1}\rightarrow}{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}H}) satisfies , referred to as the shift of along :
[TABLE]
Here, the application condition is constructed inductively as follows:
- (i)
Case :**
[TABLE] 2. (ii)
Case \mathsf{c}_{P}=\exists({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}a},{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{c}_{A}}) (for some {\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}(a:P\rightarrow A)}\in\mathcal{M} and {\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{c}_{A}} an application condition over {\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}A}\in\mathsf{obj}(\mathbf{C})):* construct the commutative diagram below, where the square marked is a pushout333Besides a more concrete characterization of , we also profit from restricting all morphisms involved in this construction (except for the epimorphisms ) to be -morphisms, which in particular guarantees due to the assumed -adhesivity of the underlying category that the pushout to form the object always exists.:*
[TABLE]
Here, each -morphism {\color[rgb]{0,0,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.4}x:P\rightarrow X} such that there exist -morphisms {\color[rgb]{0,0,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.4}p^{\prime\prime}:X\rightarrow Q} and {\color[rgb]{0,0,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.4}a^{\prime\prime}:X\rightarrow{A}}, and with {\color[rgb]{0,0,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.4}p^{\prime\prime}}\circ{\color[rgb]{0,0,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.4}x}=p and {\color[rgb]{0,0,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.4}a^{\prime\prime}}\circ{\color[rgb]{0,0,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.4}x}={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}a}, induces an object {\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}E} and -morphisms {\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}r:Q\rightarrow E} and {\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}s:A\rightarrow{E}} via taking the pushout of the span (Q{\color[rgb]{0,0,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.4}\xleftarrow{p^{\prime\prime}}X\xrightarrow{a^{\prime\prime}}}A). Since objects in are assumed to be finite, which entails in particular that there are only finitely many -subobjects of and {\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}A}, up to isomorphisms of spans (induced by isomorphisms of {\color[rgb]{0,0,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.4}X}) there are only finitely many isomorphism classes of spans (Q{\color[rgb]{0,0,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.4}\xleftarrow{p^{\prime\prime}}X\xrightarrow{a^{\prime\prime}}}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}A}). Denoting the set of all isomorphism classes of -morphism pairs {\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}(r,s)} thus obtained by , we define
[TABLE] 3. (iii)
Case :**
[TABLE] 4. (iv)
Case :**
[TABLE]
Proof 3.8**.**
We will closely follow the proof strategy of (Ehrig et al., 2014, Lem. 3.11), adapted to our variant of the construction (and proving en passent the equivalence of our construction to the ones of (Habel and Pennemann, 2009, Thm. 5 and Lem. 3) and (Ehrig et al., 2014, Lem. 3.11), see Remark 3.9 below). The statement is trivially true for the case . For the case \mathsf{c}_{P}=\exists({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}a:P\hookrightarrow A},{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{c}_{A}}) of a nested application condition, we will prove the claim by induction over the levels of nesting.
[TABLE]
“” direction:
Suppose that {\color[rgb]{0.6,0.6,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.6,1}n}\circ p\vDash\exists({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}a:P\hookrightarrow A},{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{c}_{A}}), and take (20) as the induction hypothesis in case that {\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{c}_{A}} is itself a nested condition. By definition of satisfiability, this entails that there exists {\color[rgb]{0.8,0.8,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.8,0}\pgfsys@color@cmyk@stroke{0}{0}{0.8}{0.2}\pgfsys@color@cmyk@fill{0}{0}{0.8}{0.2}(m:A\hookrightarrow H)}\in\mathcal{M} such that {\color[rgb]{0.8,0.8,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.8,0}\pgfsys@color@cmyk@stroke{0}{0}{0.8}{0.2}\pgfsys@color@cmyk@fill{0}{0}{0.8}{0.2}m}\circ{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}a}={\color[rgb]{0.6,0.6,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.6,1}n}\circ p. Construct the span {\color[rgb]{0,0,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.4}(p^{\prime\prime},a^{\prime\prime})} by taking the pullback of the cospan ({\color[rgb]{0.6,0.6,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.6,1}n},{\color[rgb]{0.8,0.8,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.8,0}\pgfsys@color@cmyk@stroke{0}{0}{0.8}{0.2}\pgfsys@color@cmyk@fill{0}{0}{0.8}{0.2}m}), which by universal property of pullbacks furnishes a morphism {\color[rgb]{0,0,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.4}x:P\rightarrow X}. By stability of -morphisms under pullbacks, we find that {\color[rgb]{0,0,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.4}p^{\prime\prime}},{\color[rgb]{0,0,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.4}a^{\prime\prime}}\in\mathcal{M}, and thus by the decomposition property of -morphisms also that {\color[rgb]{0,0,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.4}x}\in\mathcal{M}. Next, construct the cospan {\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}(r,s)} via taking the pushout of the span {\color[rgb]{0,0,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.4}(p^{\prime\prime},a^{\prime\prime})}, which by stability of -morphisms under pushout entails that {\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}r},{\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}s}\in\mathcal{M}. By the universal property of pushouts, there exist morphisms {\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}e:S\rightarrow E} and (see (23)), with {\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}e}\in\mathsf{epi}(\mathbf{C}) (via Theorem 3) and (via -effective unions). By definition of satisfiability, {\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}m}\vDash{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{c}_{A}} and {\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}m}=h\circ{\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}s} together with the induction hypothesis for entail that h\vDash\mathsf{Shift}({\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}s},\mathsf{c}_{A}). Again invoking the definition of satisfiability, since h\circ{\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}r}={\color[rgb]{0.6,0.6,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.6,1}n} and h\vDash\mathsf{Shift}({\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}s},{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{c}_{A}}), we have thus verified that indeed {\color[rgb]{0.6,0.6,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.6,1}n}\vDash\exists({\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}r},\mathsf{Shift}({\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}s},{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{c}_{A}}).
“” direction:
Let us assume that {\color[rgb]{0.6,0.6,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.6,1}n}\vDash\mathsf{Shift}(p,\exists({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}a},{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{c}_{A}})), with the shifted condition constructed according to (20). We have to verify that this entails n\circ p\vDash\exists({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}a},{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{c}_{A}}). Combining the assumption with the definition of satisfiability of conditions, there must exist {\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}r},{\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}s},h\in\mathcal{M} such that h\circ{\color[rgb]{0,0,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.4}r}={\color[rgb]{0.6,0.6,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.6,1}n} and h\vDash\mathsf{Shift}({\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}s},{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{c}_{A}}). By the induction assumption, h\vDash\mathsf{Shift}({\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}s},{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{c}_{A}}) entails that the morphism {\color[rgb]{0.8,0.8,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.8,0}\pgfsys@color@cmyk@stroke{0}{0}{0.8}{0.2}\pgfsys@color@cmyk@fill{0}{0}{0.8}{0.2}m}\in\mathcal{M} given by {\color[rgb]{0.8,0.8,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.8,0}\pgfsys@color@cmyk@stroke{0}{0}{0.8}{0.2}\pgfsys@color@cmyk@fill{0}{0}{0.8}{0.2}m}:=h\circ{\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}s} (see (23)) satisfies {\color[rgb]{0.6,0.6,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.6,1}m}\vDash\mathsf{c}_{A}. Since by construction {\color[rgb]{0.8,0.8,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.8,0}\pgfsys@color@cmyk@stroke{0}{0}{0.8}{0.2}\pgfsys@color@cmyk@fill{0}{0}{0.8}{0.2}m}\circ a={\color[rgb]{0.6,0.6,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.6,1}n}\circ p, by definition of satisfiability we have thus demonstrated that indeed {\color[rgb]{0.6,0.6,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.6,1}n}\circ p\vDash\exists({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}a},{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{c}_{A}}).
*Finally, the proof of statements and is obtained in an analogous fashion. *
Remark 3.9**.**
Since an algorithmically tractable construction is quintessential for developing a calculus of compositional rewriting, let us briefly discuss the precise relationship of our refined construction to the pre-existing constructions in the literature, highlighting in particular the nature of the refinement:
- •
In the variant of the construction and corresponding proof strategy presented in (Ehrig et al., 2014, Lem. 3.11), the authors base their construction upon assuming a priori that a set of cospans
[TABLE]
is provided, where no additional properties for the commutative squares \Box(P,Q,{\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}E},{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}A}) are required. As for the class of cospans , the origin of this class in Ehrig et al. (2014)* is an --pair factorization property that is assumed to hold for the category , whereby any cospan of arbitrary morphisms () factors uniquely up to isomorphisms as*
[TABLE]
On the one hand, this construction permits to consider the seemingly more general case of conditions formulated in terms of non--morphisms, which however according to highly technical results presented in Habel and Pennemann (2009)** in fact does not increase the expressivity of the calculus of conditions. On the other hand, the construction of Ehrig et al. is strictly more general than ours in that it permits to consider non-monic matches for applications of linear rules. Yet for an -adhesive category satisfying Assumption 1 and for the case of -morphisms as admissible matches, Corollary 3.5 entails that our construction is mathematically equivalent to the one of (Ehrig et al., 2014, Lem. 3.11), since in this case the relevant --pair-factorizations of cospans of -morphisms are precisely of the form presented in the corollary. From an algorithmic standpoint, the class is typically non-trivial to construct, whereas our construction based upon the results of Theorem 3 only requires algorithmically rather concrete notions of “forming all larger overlaps” (Q{\color[rgb]{0,0,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.4}\hookleftarrow X\hookrightarrow}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}A}) starting from a given “overlap” (Q\hookleftarrow\!P\,{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\hookrightarrow A}). In summary, for categories satisfying Assumption 1, our construction thus constitutes a certain algorithmic refinement of the “traditional” Ehrig et al. construction.
- •
The construction of (Habel and Pennemann, 2009, Thm. 5 and Lem. 3) was developed for the setting of -morphisms as admissible matches as in our case. This variant of a construction is based upon a shape of commutative diagram as in (23) without the subdiagrams involving the object {\color[rgb]{0,0,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.4}X} and morphisms incident to it. Instead, the authors devise an algorithm whereby one iterates over the triples of morphisms ({\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}r},{\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}s},{\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}e}) such that {\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}r},{\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}s}\in\mathcal{M}, {\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}e}\in\mathsf{epi}(\mathbf{C}) and such that the diagram commutes. Inspecting the proof of Theorem 3.7, our refined construction precisely mirrors this algorithmic idea, yet it provides by virtue of Theorem 3 also a concrete construction principle for such triples of morphisms (which was not available in Habel and Pennemann (2009)**).
- •
Finally, it is worthwhile noting that the complexity of the construction may be significantly reduced444We would like to thank one of the anonymous reviewers for drawing our attention to this result.* in an alternative setting within which conditions as well as satisfiability are defined not in terms of -morphisms, but in terms of arbitrary morphisms (Navarro Gomez et al., 2016, Lem .1). However, this generalized setting is unfortunately not the setting relevant to the type of compositional rewriting theories considered in the present paper (i.e. those that satisfy both concurrency and associativity properties), which is why we indeed must necessarily rely upon the -morphism variant of the construction as presented in Theorem 3.7.*
As a first application of our refined construction, let us consider a special situation for shifts that plays a role later on in the theory of compositions of rewriting rules:
Lemma 3.10** ( along coproduct injections).**
Let be an -adhesive category satisfying Assumption 1. Let be objects, and let \exists({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}a:P\rightarrow A},{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{c}_{A}}) be a condition over . Then \mathsf{Shift}(P\rightarrow P+Q,\exists({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}a:P\rightarrow A},{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{c}_{A}})) is computed via the following type of diagram:
[TABLE]
Proof 3.11**.**
Consider the following specialization of Lemma D.62: starting from the diagram depicted in (14), any -morphism decomposes into the form (where and ), and analogously the morphism decomposes into the pair of -morphisms (with ). But since by commutativity of the diagram in (24) , it follows that and , which upon invoking Theorem 3.7 proves the claim.
Example 3.12**.**
As an illustrative application of Lemma 3.10, consider the following explicit computation in the category of undirected multigraphs (which satisfies Assumption 1, with the empty graph):
[TABLE]
The image demonstrates how the shift along the embedding of the two-vertex graph with an edge (highlighted in orange) into a disjoint union with a “square” graph yields a condition over this disjoint union of graphs that tests for a disjoint pattern, but also (via the only other possible non-trivial overlap up to isomorphisms, along an additional disjoint vertex marked in blue) an alternative condition that tests for a non-disjoint pattern:
[TABLE]
Finally, we will require two additional technical lemmas of key importance to our framework of compositional rewriting. Both results rely on the notion of equivalences of conditions (see Definition 9 and equation (10)).
Lemma 3.13** (Units for Shift).**
For every object and for every condition over , we have that
[TABLE]
Proof 3.14**.**
This follows directly from the definition of according to Theorem 3.7, by specializing (17) in the form
[TABLE]
Lemma 3.15** (Compositionality of Shift; compare Golas et al. (2014), Fact 3.14).**
Let be an object, an application condition over , and let and be two morphisms of . Then the following equivalence of conditions holds:
[TABLE]
Proof 3.16**.**
The proof follows by a repeated application of Theorem 3.7. The equivalence holds if for all morphisms , we find that
[TABLE]
Starting from the diagram below,
[TABLE]
we may calculate:
[TABLE]
4 Compositional associative Double-Pushout rewriting with conditions
In this section, we will develop a variant of Double Pushout (DPO) rewriting for linear rules, which may be obtained from the well-known “traditional” DPO-rewriting framework of Ehrig et al. Ehrig et al. (1973) with its nearly 50 years of developments Ehrig et al. (1991); Corradini et al. (1997); Rozenberg (1997); Lack and Sobociński (2005); Ehrig et al. (2006a, b, 2010); Habel and Plump (2012a); Braatz et al. (2014); Ehrig et al. (2014) via requiring the underlying -adhesive categories to satisfy Assumption 1. As we will demonstrate, this particular specialization of the original theory yields a semantics for rewriting with certain additional properties, which we refer to as compositionality and associativity. The former property is a statement on the existence of a certain form of sequential rule composition (cf. Definition 4.31), which via a variant of the classical concurrency theorem (cf. Theorem 4.37) opens the possibility to develop algorithms for the static analysis of rule application sequences. The associativity phenomenon for sequential compositions of linear rules with conditions (cf. Theorem 4.39) is an original result of the present paper, adding to the aforementioned tool-set of static analysis the possibility to analyze sequences of more than two rule applications (ultimately leading to the notions of tracelet analysis Behr (2020) and rule algebras Behr et al. (2016a); Behr and Sobocinski (2018, 2020); Behr (2019); Behr and Krivine (2020)).
Notational convention 1
Since many of the constructions and results presented in the following constitute variants of well-known results from the rich DPO-rewriting literature, by convention a mention of “compare” or “cf.” without additional comments indicates that the results coincide with those in the literature (modulo possibly some notational adjustments and minor modifications). On several occasions, we nevertheless provide full proofs of some of the essential statements, since these will provide the “blueprint” for the corresponding constructions in the SqPO-setting presented in Section 5. Our choices of notations follows mostly those taken in Behr and Sobocinski (2018).
4.1 DPO-rewriting in -adhesive categories
Contrary to the traditional graph rewriting literature, we prefer to interpret spans as encoding a partial injective map going from the right leg to the left leg, rather than the other way around. This notational convention as well as the focus on linear rules (i.e. rules based upon spans of -morphisms as opposed to non-linear rules based upon generic morphisms) was motivated by our work on the rule algebra and related tracelet constructions Behr et al. (2016a); Behr and Sobocinski (2018, 2020); Behr (2019, 2020); Behr and Krivine (2020). Furthermore, all constructions presented in the following are naturally defined only up to isomorphisms, whence the choice to consider isomorphism classes of linear rules.
Definition 4.17** (Linear rules).**
Let be an -adhesive category. We denote by the set of linear rules, defined as the set of isomorphism classes
[TABLE]
Here, we define and as isomorphic when there exist isomorphisms , and that make the evident diagram commute. Thus a (representative of a) linear rule is a span of -morphisms with Output object , Kontext object and Input object .
The precise interpretation of the concept of linear rules is provided in the form of the following main definition of DPO rewriting:
Definition 4.18** (DPO rewriting).**
Let be a linear rule, let be an object, and let be an -morphism555For our construction of a DPO-type rule algebra framework, we will only be interested in admissible matches that are in the class , even though DPO rewriting in its most general form as e.g. discussed in Ehrig et al. (2014) would permit also non-monic matches.. Then is defined to be an admissible match for the application of to , if and only if the diagram below is constructible:
[TABLE]
Here, the square marked must be constructible as a pushout complement, while if this square exists the square marked is always constructible as a pushout (cf. Assumption 1), whence the moniker Double-Pushout (DPO) rewriting is derived. In this case, we refer to as the rewrite of via the rule along the (admissible) match . We introduce the notation for the set of admissible matches for the application of the rule to the object :
[TABLE]
For compatibility with the standard DPO rewriting literature, we will sometimes use the notation
[TABLE]
in order to explicitly reference the information contained in (34). Moreover, the morphism is referred to as the comatch of (under the application of linear rule to the object ).
In order to provide a quick intuitive illustration of the DPO rewriting concept, consider the edge creation rule described in the introduction:
[TABLE]
Here, as customary in the graph rewriting literature, the structure of the linear rule (in this case a span of undirected multigraphs) is indicated via the labeling indices, i.e. in the present case reflecting that the vertices marked and are preserved in applications of this rule, and that the edge marked is created. An example for an admissible match and the respective rule application to the example graph
[TABLE]
along the example match (which sends the vertices and of to the vertices and of , respectively) is depicted below:
[TABLE]
4.2 From conditions to application conditions for rewriting rules
Conditions formulated for objects and for morphisms interact in a straightforward manner with the concept of rewriting rules, which requires two key constructions: the shift construction, as introduced in Theorem 3.7, and the so-called transport construction. We will follow the standard literature on -adhesive categories (cf. e.g. Ehrig et al. (2014)) in defining the latter construction666In this definition, there is, a priori, a choice to be made about the “direction” of the transport; our chosen convention agrees with the one in the literature and will prove convenient in our later applications to notions of compositionality of rules with application conditions..
Definition 4.19** (Transport of conditions over rules; cf. Ehrig et al. (2014), Construction 3.15).**
Let
[TABLE]
be a linear rule, and let be an application condition over . Then we define a transport construction such that is an application condition over , and which is constructed inductively as follows:
- (i)
Case :
[TABLE] 2. (ii)
Case with : if the diagram below
[TABLE]
is constructible, i.e. if the pushout complement marked exists, we define
[TABLE]
with . Otherwise, we define
[TABLE] 3. (iii)
Case :
[TABLE] 4. (iv)
Case :
[TABLE]
It is straightforward to verify that the transport construction is invariant under the various possible isomorphisms involved in the relevant constructions of pushouts and pushout complements, for precisely the same reasons as those ensuring the invariance of the shift construction under isomorphisms as detailed in the proof of Theorem 3.7.
Lemma 4.20** (Property of transport along DPO-type rules; cf. Ehrig et al. (2014), Lemma 3.14).**
In an -adhesive category satisfying Assumption 1, let be a linear rule, and let be an application condition over . Then for any DPO-admissible match of the rule into an object , and if denotes the comatch of , one finds that
[TABLE]
The transport construction allows us to choose, without loss of generality, a “standard position” for the application conditions in a linear rule, where we fix the following conventions:
Definition 4.21** (Standard form for DPO-type rules with conditions and admissible matches).**
Let denote the set of linear rules with application conditions in standard form, whose elements are defined to be of the form
[TABLE]
Consequently, we introduce the notion of admissible matches for applications of rules with application conditions to objects as follows; let be an object, as above a rule with application conditions, and an element of . Then we refer to as an admissible match if and only if satisfies the application condition,
[TABLE]
and if the diagram below is constructible:
[TABLE]
Equivalently, admissibility of thus amounts to admissibility with respect to the linear rule without application conditions (i.e. in the sense of (35)) combined with satisfaction of the application condition, resulting in the following compact formula for the set of admissible matches :
[TABLE]
For later convenience, we will employ the shorthand notation to signify “equivalence under the constraint of admissibility” 777Following the standard notational convention in the rewriting literature, we choose to not make the linear rule with respect to which admissibility is required explicit in our notation , since we will only utilize this form of equivalence in situations where the nature of this rule will be clear from the given context.:
Definition 4.22**.**
Let be a linear rule and conditions over . Then we define
[TABLE]
As a further refinement, the construction enables a certain form of compression of application conditions for linear rules.
Definition 4.23** (Compressed standard form for conditions).**
Let be a linear rule with application conditions. Then we define the compressed standard form for as
[TABLE]
where .
The intuition behind the above definition of “equivalence up to non-transportable subconditions” is that while it is perfectly possible to define arbitrary conditions of the form over the input of a linear rule, only those conditions will contribute in applications of the linear rule via matches that are transportable via , since by definition of the operation in effect tests whether or not the relevant pushout complement exists such that an admissible match of the rule could satisfy . This also implies that
[TABLE]
thus motivating the notation . A further illustration of this phenomenon is provided in Example 4.41.
We conclude this subsection by stating a number of technical lemmas that are necessary in order to derive our novel associative compositional DPO rewriting framework as presented in the following subsection, which concern certain important properties of the construction and of the compatibility of the and constructions:
Lemma 4.24** (Units for Trans).**
Let be an arbitrary object and a condition over . Then with the “identity rule on ”, we find that
[TABLE]
Proof 4.25**.**
The proof follows directly from the property of the construction stated in Lemma 4.20, whereby one finds for arbitrary admissible matches that
[TABLE]
Here, the pushout complement in the squares marked always exists by virtue of Lemma A.54(i)a, and as well as follow due to stability of isomorphisms under pushouts.
Lemma 4.26** (Compositionality of Trans).**
Given two composable spans of -morphisms
[TABLE]
define their composition via pullback as
[TABLE]
which is again a span of -morphisms (by stability of -morphisms under pullbacks and compositions), and thus . Let be a condition over . Then we find that
[TABLE]
Proof 4.27**.**
The proof relies upon the property of the transport construction stated in Lemma 4.20 as well as on the -adhesivity of the underlying category . We proceed by constructing the following commutative diagram in two different ways for the two directions of the proof:
[TABLE]
“” direction:
Suppose that and that the comatch of satisfies (with ). Then according to Lemma 4.20, this implies that
[TABLE]
We have to demonstrate that as well as
[TABLE]
Admissibility of and entails that the squares formed in the back row of (54) (the ones drawn in black and blue) are constructible as pushouts and pushout complements, respectively. Construct the objects and as pullbacks,
[TABLE]
which by the universal property of pullbacks induces a unique arrow . By stability of -morphisms under pullbacks and by the -morphism decomposition property, respectively, all morphisms thus constructed are found to be in . Invoking pullback-pullback decomposition (Lemma A.54(iii)a*) and the -van Kampen property twice (cf. Definition 1), we conclude that the induced squares and are in fact pushouts. Thus by pushout composition, the front left and right “curvy” faces (in orange) are pushouts. This entails that , and thus by definition of that indeed*
[TABLE]
“” direction:
Suppose that , which by Lemma 4.20 implies that if is the comatch of under the application of the rule , then
[TABLE]
Admissibility of for the rule applied to the object entails that the “curvy” front right and front left squares of the diagram (54) drawn in black and orange are constructible as pushout complement and pushout, respectively. We may then construct the remaining parts of the diagram via forming the pushouts
[TABLE]
which uniquely induces the remaining arrows drawn in blue (and where we could have equivalently defined as ). By virtue of three applications of pushout-pushout decomposition (Lemma A.54(iii)b*), we conclude that all squares in the back of diagram (54) thus constructed are pushouts. Furthermore, stability of -morphisms under pushouts implies that all newly constructed morphisms are in . Since thus the back part of the diagram encodes two DPO rewrite steps with , the comatch of under application of the rule , , and since is also the comatch of under application of , we find by Lemma 4.20 that*
[TABLE]
*which concludes the proof. *
The compositionality of the construction in particular permits an efficient encoding of the reduced standard form of application conditions:
Corollary 4.28**.**
Let be a linear rule with application conditions. Then the compressed standard form for according to Definition 4.23 evaluates to
[TABLE]
Lemma 4.29** (Compatibility of Shift and Trans; compare Golas et al. (2014), Fact 3.14).**
Given the data as in the commutative diagram below,
[TABLE]
letting and , we have that for all objects and for all admissible matches of into ,
[TABLE]
which we can write more compactly as
[TABLE]
Proof 4.30**.**
Let us fix an object and some admissible match .
“” direction:
Suppose that satisfies (which by definition of satisfaction of conditions entails in particular that ). Since is by assumption an admissible match of , we can rewrite by applying along , resulting in the diagram below (where the top part is inserted from the assumption of the lemma):
[TABLE]
By composition of pushout squares, we conclude that the -morphism is an admissible match for , which entails that . By definition of , implies that satisfies , and moreover that . Since we found that , by definition of we have that the comatch of (which is by construction of DPO rule applications in ) has the property . The latter implies that . Since by assumption , and since is the comatch of , we finally conclude that indeed .
“” direction:
*The proof is entirely analogous to the previous case (starting from the observation that together with the data provided in (57) entails that ). *
4.3 A refined notion of sequential compositions of DPO-type rules with conditions
In this subsection, we will present a refinement of the notion of sequential rule compositions known from the traditional rewriting literature Ehrig et al. (2014) obtained via requiring the underlying -adhesive category to satisfy Assumption 1, which as we will demonstrate guarantees a number of additional technical properties of this type of composition. Referring to Remark 4.32 for the precise technical disambiguation, the motivation for our construction consisted in the idea that the operation of sequential composition of two linear rules should lift to an operation permitting to compose arbitrary numbers of linear rules, in the sense that the composition operation should satisfy a certain abstract associativity property (cf. Section 4.5). From a technical standpoint, ensuring this notion of compositionality permits to develop novel static analysis techniques for rule-based systems, such as the DPO-type rule algebra framework Behr et al. (2016a); Behr and Sobocinski (2018, 2020) for the study of stochastic rewriting systems, which has recently been extended to the setting of linear rules with conditions based upon the present article in Behr and Krivine (2020). The second main application of compositional rewriting has been the development of the theory of tracelets Behr (2020).
Definition 4.31**.**
Let be a category satisfying Assumption 1. Let {\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}R_{j}\equiv(r_{j},\mathsf{c}_{I_{j}})}\in\overline{\mathsf{Lin}}(\mathbf{C}) be two linear rules with application conditions (), and let
[TABLE]
be a span of monomorphisms (i.e. ). If the diagram below is constructible,
[TABLE]
where
[TABLE]
and if , then we call an admissible match for the rules with conditions and , denoted
[TABLE]
In this case, we introduce the notation to denote the composite,
[TABLE]
Remark 4.32**.**
The variant of rule composition provided in Definition 4.31 (i.e. starting from an “overlap” of two rules encoded as an -monic span, followed by taking a pushout of this span) follows the philosophy put forward in Boehm et al. (1987); Lack and Sobociński (2005) (sometimes referred to as D-concurrent composition). However, for the setting of DPO-rewriting over -adhesive categories for rules with conditions, an alternative construction, referred to as E-concurrent composition, had been the de facto standard in the rewriting literature, developed by Ehrig et al. (cf. e.g. Ehrig et al. (2014), Definition 4.13). More precisely, based upon the assumption that the underlying -adhesive category possesses an --pair-factorization (cf. Remark 3.9), the starting point of constructing an E-concurrent rule composition according to Ehrig et al. (2014) consists in picking a cospan {\color[rgb]{0,0,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.4}(m_{2}^{\prime},m_{1}^{\prime})}\in\mathcal{E}^{\prime}, as opposed to picking a span of -morphisms {\color[rgb]{0,0,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.4}(m_{2},m_{1})} and taking the pushout to obtain the cospan {\color[rgb]{0,0,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.4}(m_{2}^{\prime},m_{1}^{\prime})} as in (61) for the D-concurrent approach. While the E-concurrent approach possesses the technical advantage that it does not require the category to possess -effective unions, nor that rules must be linear nor matches necessarily in (and thus applying to a broader class of rewriting systems), the reliance upon the --factorizations is also responsible for certain algorithmic disadvantages. In close analogy to the discussion provided in Remark 3.9, exhaustively enumerating all possible cospans in suitable for the composition of two rewriting rules is algorithmically quite non-trivial in the general case, while enumerating the (isomorphism classes of -) monic spans (i.e. the “overlaps”) of two linear rules is comparatively straightforward (c.f. e.g. Behr et al. (2020b) for a recent implementation via the Microsoft Z3 SMT-solver). On the other hand, utilizing yet again the results of Corollary 3.5, our refinement of D-concurrent compositions as well as the respective variant of the concurrency theorem (see Theorem 4.37) can be demonstrated to constitute a special case of the E-concurrent constructions of Ehrig et al. Ehrig et al. (2014): for an -adhesive category satisfying Assumption 1, a cospan {\color[rgb]{0,0,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.4}(m_{2}^{\prime},m_{1}^{\prime})} of -morphisms constructed via taking the pushout of a span of -morphisms {\color[rgb]{0,0,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.4}(m_{2},m_{1})} is in particular jointly epimorphic, and thus constitutes a special case of a cospan in (cf. (Braatz et al., 2014, Fact 3.7), applied under the assumption of -effective unions).
The definition of the composition operation entails a number of highly non-trivial effects in practical computations, which originate from the interplay of admissibility of matches for rules without application conditions and the requirements on the induced composite application conditions. One of the most striking such results, well known also from the traditional graph rewriting literature Ehrig et al. (2014), is the following:
Lemma 4.33** (Trivial matches).**
By definition of the notion of admissible matches, for any two linear rules with application conditions (), the trivial match
[TABLE]
is an admissible match if and only if the composite condition does not evaluate to .
Proof 4.34**.**
The proof follows directly from the definition of the composition operation , namely by construction of the following diagram:
[TABLE]
By virtue of Lemma 1 and Lemma D.58, the pushout complements marked in the diagram above always exist. To determine whether the trivial match is an admissible match, it then remains to evaluate the composite condition , which according to (62) of Definition 4.31 reads
[TABLE]
Thus the claim follows, since the above condition may evaluate to in general, such as in the case where .
Nevertheless, it is possible to exhibit one special rule for which is always an admissible match:
Lemma 4.35** (Neutral element for ).**
By definition of , the trivial rule
[TABLE]
is the (left- and right-) neutral element for .
Proof 4.36**.**
The proof follows from a specialization of (64) in the proof of Lemma 4.33, by specializing either of the two linear rules involved to the trivial rule. Note first that on the level of rules without application conditions, the only admissible match between the trivial rule and another linear rule is the trivial match . Let us then compute the condition of the composite for the case and for generic , which reads according to (62) of Definition 4.31 reads
[TABLE]
Thus for every linear rule with application condition , we have . For the remaining case, consider that is an arbitrary linear rule with application condition . Again, admissibility of as a match of the rules without conditions follows by a specialization of (64), so it remains to compute the composite condition :
[TABLE]
4.4 Concurrency theorem for DPO-type rules with conditions
We will need the following concurrency theorem, which is a variant of a result of Habel and Plump (2012a) adapted to our refined notion of rule compositions, and which for the case of rules without conditions was introduced in Behr and Sobocinski (2020):
Theorem 4.37** (Concurrency theorem, compare Thm. 4 of Habel and Plump (2012b) and Thm. 2.7 of Behr and Sobocinski (2020)).**
Let be an -adhesive category satisfying Assumption 1, an object, and {\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}R_{j}\equiv(r_{j},\mathsf{c}_{I_{j}})} be two linear rules with application conditions (). Then there exists the following bijection:
- (i)
“Synthesis”:* For every sequence of rule applications*
[TABLE]
along admissible matches and with , there exist admissible matches of the linear rule into and , with , , and an application condition computed as
[TABLE]
where the morphisms and objects in this formula depend (uniquely up to isomorphism) on the input data, such that . 2. (ii)
“Analysis”:* For every admissible match and for every rule application*
[TABLE]
with and , there exists a pair of admissible matches such as in (68) which transform via into the same (up to isomorphism) object .
Proof 4.38**.**
Referring the interested readers to Behr and Sobocinski (2020) for the precise details, note first that at the level of linear rules without application conditions, the concurrency theorem of Behr and Sobocinski (2020) entails the parts of the above statements pertaining to the existence of the admissible matches of “plain” rules. The concrete technical construction of the proof provided in Behr and Sobocinski (2020) is summarized by the diagram below, where all vertical squares are pushouts (and where we have marked the relevant conditions for later convenience). The aforementioned proof consisted in verifying that the parts of the diagram marked in blue can be uniquely constructed from the parts of the diagram colored in orange and vice versa:
[TABLE]
It thus remains to verify the part of the claim pertaining to the relevant conditions of the rules.
“Analysis” part of the proof:
Suppose that we are given admissible matches {\color[rgb]{0,0,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.4}(m_{1}:I_{1}\rightarrow X_{0})}\in M_{R_{1}}(X) and {\color[rgb]{0,0,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.4}(m_{2}:I_{2}\rightarrow X_{1})}\in M_{R_{2}}(X_{1}) with X_{1}=r_{1_{{\color[rgb]{0,0,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.4}m_{1}}}}(X_{0}). Admissibility entails in particular that {\color[rgb]{0,0,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.4}m_{1}}\vDash\mathsf{c}_{I_{1}} and {\color[rgb]{0,0,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.4}m_{2}}\vDash\mathsf{c}_{I_{2}}. By construction of the diagram in (71), we have that {\color[rgb]{0,0,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.4}m_{1}} and {\color[rgb]{0,0,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.4}m_{2}} factor as
[TABLE]
which entails by definition of the construction that {\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}m_{21}}:=({\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}I_{21}\rightarrow}X_{0}) and {\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}\bar{m}_{21}}=({\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}N_{21}\rightarrow}X_{1}) satisfy {\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}m_{21}}\vDash\mathsf{Shift}(I_{1}{\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}\rightarrow I_{21}},\mathsf{c}_{I_{1}}) and {\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}\bar{m}_{21}}\vDash\mathsf{Shift}(I_{2}{\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}\rightarrow N_{21}},\mathsf{c}_{I_{2}}), respectively. Noting that the rightmost two bottom squares in the back of (71) are pushouts, we find in addition that
[TABLE]
Since according to Definition 4.31, {\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}R_{21}}:=R_{2}\stackrel{{\scriptstyle\mu_{21}}}{{\blacktriangleleft}}R_{1}={\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}(r_{21},\mathsf{c}_{I_{21}})}, with {\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}\mathsf{c}_{I_{21}}} as defined in (69), we confirm that {\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}m_{21}}\vDash{\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}\mathsf{c}_{I_{21}}}, which concludes the proof of the “analysis” part of the theorem.
“Synthesis” part of the proof:
*Supposing that we are given an admissible match {\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}m_{21}} of the composite {\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}R_{21}} of the rules with application conditions with along the admissible match {\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}\mu_{21}}\in\mathsf{M}_{R_{1}}(R_{2}), the construction of the diagram in (71) provides two admissible matches {\color[rgb]{0,0,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.4}(m_{1}:I_{1}\rightarrow X_{0})}\in\mathsf{M}_{r_{1}}(X_{0}) and {\color[rgb]{0,0,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.4}(m_{2}:I_{2}\rightarrow X_{1})}\in\mathsf{M}_{r_{2}}({\color[rgb]{0,0,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.4}X_{1}}) with {\color[rgb]{0,0,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.4}X_{1}}=r_{1_{{\color[rgb]{0,0,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.4}m_{1}}}}(X_{0}). It thus remains to verify the claim that these matches satisfy the conditions and , respectively, which is demonstrated by running the corresponding arguments of the “analysis” part of the proof “in reverse”. *
4.5 Associativity of DPO-type composition of rules with conditions
We will now state one of the main results of this paper, in the form of an associativity property afforded by the DPO-type composition operation on rules with conditions. The case of DPO-type compositions of rules without conditions was studied in Behr et al. (2016a); Behr and Sobocinski (2018, 2020), and the following result is an extension to the setting of rules with conditions afforded by our refined framework for conditions as introduced in Section 3 and the current section. In contrast to the DPO-type concurrency theorem (which, in a slightly different formulation, had been previously known in the literature), the associativity result presented below is, to the best of our knowledge, the first of its kind.
Theorem 4.39** (DPO-type Associativity Theorem).**
Let () be three linear rules with application conditions. Then there exists a bijection between the pairs of admissible matches and defined as
[TABLE]
with (and defined as in (62)) such that
[TABLE]
and vice versa. In this particular sense, the operation is associative.
Proof 4.40**.**
Considering first the case of compositions of “plain” rules , i.e. of rules without application conditions, we quote from Behr and Sobocinski (2020) (Theorem 2.9) an isomorphism of pairs of admissible matches of the form
[TABLE]
The isomorphism entails that for each corresponding pair, equation (73a) is verified. Consider then two such isomorphic pairs
[TABLE]
of admissible matches of “plain” rules. The isomorphism entails in particular that the following commutative diagram is uniquely constructible (where we also draw the positions of the various application conditions at play for later convenience):
[TABLE]
In order to verify the validity of (73b), it is sufficient to utilize our various technical lemmas pertaining to the and constructions, and to follow the “paths” in the diagram depicted in (75) along which the three conditions for have to be shifted and transported in order to form the conditions and , respectively.
- (i)
contribution of :
[TABLE] 2. (ii)
contribution of :
[TABLE]
Here, in the last step, we have made use of the commutativity of the diagram (75), whereby
[TABLE] 3. (iii)
contribution of :
[TABLE]
It is then easy to verify (using the definition of concurrent compositions of rules with application conditions with rules according to Definition 4.31 and eq. (62)) that since
[TABLE]
where by “rhs” we mean the very last equality in each set of equations, we find indeed that
[TABLE]
Example 4.41**.**
In order to illustrate the notion of associativity more intuitively, we provide a concrete example of a triple rule composition as depicted in Figure 2, with the application conditions of the three rules given as
[TABLE]
Note that the application conditions as specified guarantee that applying the rules to simple undirected graphs preserves the constraint of no two vertices being linked by more than one edge. Rather than depicting the relevant data for this computation in the form of a “commutative tube” as in (75), we opt here to “unfold” the two pair-wise sequential rule composition steps for each branch of the equivalence
[TABLE]
with the two sides of the equivalences depicted on the top and bottom parts of Figure 2, respectively. The example allows us to highlight a number of interesting phenomena:
- •
Upon closer inspection, one may verify that the application condition of the rule is not specified in “compressed standard form” in the sense of Definition 4.23, since in fact . Intuitively, under DPO-semantics the application condition does not constrain the admissible matches, since in cases where the two vertices in would be matched against two vertices in a host graph linked by an edge, the rule would not be applicable (since edges cannot be deleted implicitly in DPO-rewriting).
- •
Utilizing the and constructions, followed by applying the “compression” according to Definition 4.23, the application condition of the composite rule can be computed as follows:
[TABLE]
This is a typical illustration of the way associativity in sequential compositions gives rise to causal relationships: while the rule can only be applied to vertices not linked by an edge, the fact that in the triple composition depicted the rule is in a sense “providing” the two vertices on its output that are later acted upon by , and since by the application of as shown the edge between the two vertices on the output of is removed, it is indeed the case that we find a graph pattern that can be applied to.
- •
Finally, associativity also entails that one may equivalently lead the preceding causality argument from the viewpoint depicted in the bottom part of Figure 2: composing rule with rule as demonstrated, the composite rule has an application condition {\color[rgb]{0,0,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.4}\mathsf{c}_{I_{32}}} that demands that the two vertices on the input of the composite rule are not linked to each other by two edges. But then if the input pattern of the composite rule (two vertices linked by an edge) is “provided” by the output of as depicted (i.e. via computing the composition {\color[rgb]{0,0,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.4}r_{3}\stackrel{{\scriptstyle\mu_{32}}}{{\blacktriangleleft}}r_{2}} and the composite rule’s application condition {\color[rgb]{0,0,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.4}\mathsf{c}_{I_{32}}}), and since can only be applied at two vertices not linked to each other, one finds again that the overall triple composite possesses an application condition that is equivalent to a trivial condition .
We refer the interested readers to Behr (2020) for further examples of such types of sequential rule compositions and associativity properties, which play a quintessential role in the theory of tracelets, where the latter are a form of invariant encoding of length sequences of rule compositions for general . Associativity is moreover at the core of the construction of rule algebra theories Behr et al. (2016a); Behr and Sobocinski (2018, 2020); Behr (2019), and with the case of rule algebras for linear rules with conditions recently covered in Behr and Krivine (2020), yet a full discussion of this novel mathematical concept is out of the scope of the present paper.
5 Compositional associative Sesqui-Pushout rewriting with conditions
While the previously discussed notion of compositional DPO-type rewriting may be seen as a refinement of pre-existing notions of DPO-rewriting from the literature (apart from the associativity theorem), the corresponding construction for a framework of SqPO-rewriting is almost entirely new. The first framework for a compositional SqPO-rewriting framework for rules without conditions was introduced in Behr (2019). The essential technical step in order to extend our framework from DPO- to SqPO-type semantics consists in analyzing the interplay of final pullback complements with application conditions and transformations thereof. We will first provide a brief introduction to this type of rewriting, and then develop our new framework.
5.1 Definition of SqPO rule applications and rule compositions
Definition 5.42** (compare Corradini et al. (2006), Def. 4).**
Given an object and a linear rule , we denote the set of SqPO-admissible matches as
[TABLE]
Let . Then the diagram below is constructed by taking the final pullback complement marked followed by taking the pushout marked :
[TABLE]
We write for the object “produced” by the above diagram. The process is called (SqPO)-derivation of along rule and admissible match , and denoted .
Notably, SqPO-type rewriting thus differs from DPO-type rewriting in the important aspect that final pullback complements as well as pushouts are guaranteed to exist in our base category (cf. Assumption 2), whereas pushout complements may fail to exist in general. A typical example already mentioned in the introduction concerns the application of a vertex-deletion rule to a graph that consists of two vertices linked by an edge:
[TABLE]
In DPO-type rewriting, the deletion rule is not applicable along the match presented, since the square is not constructible as a pushout complement. In SqPO-type rewriting however, since the square is constructible as a final pullback complement as presented, the deletion rule is applicable, resulting in a graph with just a single vertex. This example demonstrates the distinguishing feature of SqPO-type rewriting over DPO-rewriting, in that the former admits “deletion in unknown context” (here the implicit deletion of the edge via application of the vertex deletion rule).
It should be noted that one of the additional distinctive features of SqPO-rewriting (see Corradini et al. (2006)) consists in the possibility to faithfully model cloning of structures via considering non-linear rules (i.e. rules based upon non-monic spans). While an interesting topic in its own right, we found that our proofs for key properties such as the concurrency and associativity theorems in the forms presented here would not easily carry over to this more general setting, which is why we did not consider the case of non-linear rules in any further detail.
5.2 The transport construction in the SqPO-type setting
The following theorem demonstrates that the construction as introduced in Definition 4.19 is precisely the construction needed in order to implement “transporting” conditions over linear rules also in the SqPO-rewriting setting. This quintessential result appears to be new.
Theorem 5.43** (Transport construction in SqPO rewriting).**
Let be an -adhesive category satisfying Assumption 2. Then the transport construction satisfies the following property: for every linear rule , for every SqPO-admissible match of into an object and for every application condition over , in the commutative diagram below
[TABLE]
it holds that
[TABLE]
Proof 5.44**.**
Due to the recursive nature of the definition of (Definition 4.19), it suffices to verify the claim on conditions of the form \mathsf{c}_{O}=\exists({\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}b^{*}:O\hookrightarrow B},{\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}\mathsf{c}_{B}}) (for {\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}b^{*}}\in\mathcal{M}).
“” direction:
Suppose that we are given an SqPO-type rewriting step and a condition of the form \mathsf{c}_{O}=\exists({\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}b^{*}:O\hookrightarrow B},{\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}\mathsf{c}_{B}}), which by definition of satisfiability of conditions according to Definition 9 furnishes a morphism {\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}(n^{*}:B\hookrightarrow r_{m}(X))}\in\mathcal{M} such that {\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}n^{*}}\circ{\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}b^{*}}={\color[rgb]{0,0,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.4}m^{*}}:
[TABLE]
We then construct the commutative diagram below,
[TABLE]
with the following individual steps taken:
- (i)
The square {\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}(1)} is formed by taking pullback, which by the universal property of pullbacks furnishes a morphism K{\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}\rightarrow K^{\prime}}. By stability of -morphisms under pullback, the morphisms of the induced span are in . Since thus in particular {\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}K^{\prime}\rightarrow}\overline{K} is in , and since by stability of -morphisms under pullback (and thus under FPC) also , we conclude by -morphism decomposition that K{\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}\rightarrow K^{\prime}} is in . Moreover, by virtue of pushout-pullback decomposition (Lemma A.54(iii)c*), the squares {\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}(1)} and {\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}(2)} are both pushouts.* 2. (ii)
The square {\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}(3)} is formed by taking pushout. The universal property of pushouts provides a morphism {\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}n:C\rightarrow}X such that {\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}n}\circ{\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}b}={\color[rgb]{0,0,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.4}m}. Then invoking vertical FPC-pushout decomposition (Lemma A.54(iii)h*), the resulting square is an FPC and {\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}n}\in\mathcal{M}.*
If {\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}\mathsf{c}_{B}}\equiv{\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}\mathsf{true}}, we have thus demonstrated by virtue of the definition of satisfiability of conditions that the -morphism {\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}n} satisfies the condition \exists({\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}b:I\hookrightarrow C},{\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}\mathsf{Trans}(r^{\prime},\mathsf{true})}), since by definition of we have that {\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}\mathsf{Trans}(r^{\prime},\mathsf{true})}\equiv{\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}\mathsf{true}}. If {\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}\mathsf{c}_{B}} is itself nested, we proceed by induction in the evident fashion, i.e. repeat the preceding argument for {\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}\mathsf{c}_{B}} and {\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}r^{\prime}}:={\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}(B\leftarrow K^{\prime}\rightarrow C)}, thus the claim of the “” part of the theorem statement follows.
“” direction
Suppose that we are given the following part of data presented in diagram (87):
- (i)
The squares {\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}(1)+(2)} (a pushout), {\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}(2)} (a pushout), {\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}(3)+(4)} (an FPC) and {\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}(3)} (a pushout). 2. (ii)
An arrow {\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}n}\in\mathcal{M} that satisfies the condition \mathsf{Trans}({\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}r^{\prime}},{\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}\mathsf{c}_{B}}), and with {\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}n}\circ{\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}b}={\color[rgb]{0,0,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.4}m}.
What is somewhat hidden in this set of data is the fact that the square \Box(K,{\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}K^{\prime}},X,I) is a pullback (where the -morphism {\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}K^{\prime}}\rightarrow X is provided as the composition of the -morphisms {\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}K^{\prime}\rightarrow C} and {\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}n:C\rightarrow}X, which are by assumption part of the above data). This statement can be verified by constructing the commutative cube below left:
[TABLE]
By virtue of Lemma A.54(i)c*, the right square is a pullback. Since the top square is a pushout and thus also a pullback, by pullback composition the square \Box(K,{\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}K^{\prime}},X,I) (i.e. the composite of the top and right squares) is indeed a pullback.*
We then invoke the universal property of FPCs (compare Definition 7) in the form presented in the right part of (88), which entails that there exists a morphism {\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}K^{\prime}\rightarrow}\overline{K}. Then by -morphism decomposition, as {\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}K^{\prime}\rightarrow}X and are in , so is the morphism {\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}K^{\prime}\rightarrow}\overline{K}. Consequently, vertical FPC-pushout decomposition (Lemma A.54(iii)h*) implies that the square {\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}(4)} in (87) is an FPC, while due to pushout-pushout decomposition (Lemma A.54(iii)b**) the square {\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}(1)} is verified to be a pushout. The latter result entails in particular, by virtue of stability of -morphisms under pushout, that the induced morphism {\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}n^{*}} is in .*
*In summary, if {\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}\mathsf{c}_{B}}\equiv\mathsf{true}, we have verified that {\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}n^{*}}\vDash{\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}\mathsf{c}_{B}}, and thus that {\color[rgb]{0,0,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.4}m^{*}}\vDash\exists({\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}b^{*}:O\rightarrow B},{\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}\mathsf{c}_{B}}). If {\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}\mathsf{c}_{B}} is itself nested, we can prove the statement inductively in the evident fashion. *
The detailed structure of the above proof allows us to clarify that, while the construction from the DPO rewriting setting carries over to the SqPO setting seemingly verbatim, the precise reasons for why it indeed furnishes an operation of transport of conditions in the desired sense in the two settings are dependent on the semantics (i.e. in particular why satisfaction of conditions is “transported” against the direction of SqPO linear rules as detailed above). Moreover, since there does not exist a construction that would permit to transport conditions “with” the direction of the linear rules (i.e. in the direction of rule applications) in SqPO rewriting888Consider for example the case of a rule with “plain” rule and application condition . Applying the “plain” rule to a graph with two vertices linked by an arbitrary number of edges would result in a single-vertex graph under SqPO-semantics regardless of the number of edges (which are all implicitly deleted), yet only the case without edges permits admissible matches of , which provides a counter-example to the hypothesis that one could formulate a post-condition “transport-equivalent” to ., the only degree of freedom in describing linear rules with application conditions in SqPO semantics is to transport any conditions a rule might carry on its output to its input, motivating the following definition:
Definition 5.45** (Standard form for SqPO-type linear rules with application conditions and for admissble matches).**
. Let be an -adhesive category satisfying Assumption 2. Let denote the set of linear rules with application conditions in standard form as introduced in Definition 4.21, whence elements of are of the form
[TABLE]
We then introduce the notion of SqPO-admissible matches for applications of rules with application conditions to objects under SqPO-type semantics as follows: let be an object, as above a rule with application conditions, and an element of . Since according to Assumption 2 FPCs of arbitrary pairs of composable -morphisms exist, the diagram below is always constructible,
[TABLE]
the SqPO-admissibility of hinges solely on whether the match satisfies the condition of the rule . We thus define the set of SqPO-admissible matches for the application of the rule to the object as
[TABLE]
A beneficial side-effect of the former observation is the following result, most statements of which carry over from the DPO-rewriting setting for the construction:
Theorem 5.46** (Properties of in SqPO-rewriting).**
Given an -adhesive category satisfying Assumption 2, the transport construction has the following properties:
- (i)
Units for :* Let be an arbitrary object and a condition over . Then with the “identity rule on ”, we find that*
[TABLE] 2. (ii)
Compositionality of :* Given two composable spans of -morphisms*
[TABLE]
we find that
[TABLE] 3. (iii)
Compatibility of and :**
[TABLE]
letting and , we have that for all objects and for all admissible matches of into ,
[TABLE]
which we write more compactly as999Note that unlike in the DPO rewriting case, since by Assumption 2 FPCs of arbitrary composable pairs of -morphisms exist, it is indeed the case that any -morphism is an admissible match for the linear rule without application conditions ; consequently, the equivalence takes precisely the form of standard equivalence of application conditions without a constraint of admissibility.**
[TABLE]
Proof 5.47**.**
The proofs of the first two statements take precisely the same shape as the corresponding proofs of Lemma 4.24 (units for ) and Lemma 4.26 (compositionality of ) for the DPO-rewriting setting, as they are independent of the underlying type of rewriting. It remains to prove the third statement, which follows by suitably adapting the proof strategy of Lemma 4.29 (compatibility of and in DPO-rewriting). More precisely, construct the commutative diagram below, where the top part is inserted from the assumption of the lemma, and where the bottom part constitutes an SqPO-type rewrite step of applying the rule to along the match :
[TABLE]
From hereon, the proof structure is fully analogous to the DPO rewriting case: since
[TABLE]
we find that . Since the top and bottom left squares compose into a pushout and the top and bottom right squares into an FPC, implies that {\color[rgb]{0,0,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.4}m^{*}}={\color[rgb]{0,0,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.4}n^{*}}\circ p^{*}\vDash\mathsf{c}_{O}. Since {\color[rgb]{0,0,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.4}m^{*}}={\color[rgb]{0,0,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.4}n^{*}}\circ p^{*}, {\color[rgb]{0,0,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.4}m^{*}}\vDash\mathsf{c}_{O} implies that {\color[rgb]{0,0,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.4}n^{*}}\vDash\mathsf{Shift}(p^{*},\mathsf{c}_{O}), and since the bottom left and right squares are of the form of an SqPO-type rewriting step, we find that indeed . The proof of the converse direction follows by reversing the order of the preceding steps of the proof.
5.3 SqPO-type concurrent composition of rules with conditions
The second central definition for our rewriting framework is the following notion of concurrent composition, which is an extension of a construction first introduced in Behr (2019) to the setting of rules with conditions.
Definition 5.48** (SqPO-type concurrent composition).**
Let be an -adhesive category satisfying Assumption 2. Let {\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}R_{j}\equiv(r_{j},\mathsf{c}_{I_{j}})}\in\overline{\mathsf{Lin}}(\mathbf{C}) be two linear rules with application conditions (), and let
[TABLE]
be a span of -morphisms (i.e. ). If the diagram below is constructible (if the pushout complement marked exists),
[TABLE]
where (in close analogy to the DPO-type rewriting setting)
[TABLE]
and if , then we call an SqPO-admissible match for the rules with conditions into , denoted
[TABLE]
In this case, we introduce the notation to denote the composite,
[TABLE]
As already noted in Behr (2019) for the case of SqPO-type rewriting for rules without conditions, it might appear surprising at first sight that there is an asymmetry in the above definition (in that the left part of the diagram consists of an FPC and a pushout, while the right part is formed by a pushout complement and a pushout, respectively), but the precise reason for this definition will become apparent when considering the concurrency theorem for SqPO-type rules with conditions in the following subsection.
5.4 SqPO-type concurrency theorem for rules with conditions
To the best of our knowledge, the following key result is the first of its kind in the SqPO-rewriting setting:
Theorem 5.49** (SqPO-type Concurrency Theorem, extended from Behr (2019), Thm. 2.9).**
Let be an -adhesive category satisfying Assumption 2, let () be two linear rules with application conditions, and let be an object.
- •
Synthesis:* Given a two-step sequence of SqPO derivations*
[TABLE]
with and , there exists a SqPO-composite rule for a unique as well as an SqPO-admissible match (that is unique up to isomorphisms) such that
[TABLE]
- •
Analysis:* Given an SqPO-admissible match of into and an SqPO-admissible match of the SqPO-composite into , there exists a pair of SqPO-admissible matches and (with , and unique up to isomorphisms) such that*
[TABLE]
Proof 5.50**.**
For the part of the proof pertaining to the concurrency of SqPO-type rules without application conditions, we will follow the strategy presented in Behr (2019) (where slightly stronger conditions than the ones required according to Assumption 2 were made, i.e. in Behr (2019) was assumed to be adhesive, whence the re-derivation here in the -adhesive setting).
“Synthesis” part of the proof:
Suppose we are given rules with application conditions and SqPO-admissible matches {\color[rgb]{0,0,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.4}m_{1}}\in\mathsf{M}^{sq}_{R_{1}}(X_{0}) and {\color[rgb]{0,0,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.4}m_{2}}\in\mathsf{M}^{sq}_{R_{2}}(X_{1}), with X_{1}=R_{1_{{\color[rgb]{0,0,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.4}m_{1}}}}(X_{0}). This data is encoded in the blue part of the diagram in (71). Let us begin by constructing the orange parts of (71) as follows: take the pullback {\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}M_{21}}=\mathsf{PB}(I_{2}{\color[rgb]{0,0,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.4}\rightarrow X_{1}\leftarrow}O_{1}), and then the pushout {\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}N_{21}}=\mathsf{PO}(I_{2}{\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}\leftarrow M_{21}\rightarrow}O_{1}); by the universal property of pushouts, there exists a morphism {\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}N_{21}}\rightarrow{\color[rgb]{0,0,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.4}X_{1}}, which is in since is assumed to possess -effective unions according to Assumption 2. Next, form the pullbacks {\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}K_{i}^{\prime}}=\mathsf{PB}({\color[rgb]{0,0,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.4}\overline{K}_{i}\rightarrow X_{1}}\leftarrow{\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}N_{21}}) (for ), which furnishes morphisms K_{i}{\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}\rightarrow K_{i}^{\prime}} (for ) that are in due to the decomposition property of -morphism. By virtue of vertical FPC-pullback decomposition (Lemma A.54(iii)g*), the second from the left bottom and top squares in the back of (71) are FPCs, while via pushout-pullback decomposition (Lemma A.54(iii)c**) the second from the right top and bottom squares in the back of (71) are pushouts. Let {\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}O_{21}}=\mathsf{PO}(O_{2}\leftarrow K_{2}{\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}\rightarrow K_{2}^{\prime}}), which by the universal property of pushouts furnishes a morphism {\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}O_{21}\rightarrow}X_{2}; by pushout-pushout decomposition (Lemma A.54(iii)b**), the leftmost bottom square in the back of (71) is a pushout, which also entails by stability of -morphisms under pushouts that ({\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}O_{21}\rightarrow}X_{2})\in\mathcal{M}. Analogously, let {\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}I_{21}}=\mathsf{PO}({\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}K_{1}^{\prime}\leftarrow}K_{1}\rightarrow I_{1}), which furnishes a morphism {\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}I_{21}\rightarrow}X_{0}, and via vertical FPC-pushout decomposition (Lemma A.54(iii)h**) that the rightmost bottom back square in (71) is an FPC and that ({\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}I_{21}\rightarrow}X_{0})\in\mathcal{M}.*
At this point, note that the bottom row of squares in the back of (71) has the shape of two consecutive SqPO rewriting steps. Since {\color[rgb]{0,0,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.4}(m_{1}:I_{1}\rightarrow X_{0})\vDash\mathsf{c}_{I_{1}}} and {\color[rgb]{0,0,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.4}(m_{2}:I_{2}\rightarrow X_{1})\vDash\mathsf{c}_{I_{2}}} by assumption, we conclude that {\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}m_{21}=(I_{21}\rightarrow X_{0})} satisfies {\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}m_{21}\vDash\mathsf{c}_{21}}, with
[TABLE]
To complete this part of the proof, take the pullbacks
[TABLE]
which also induces a morphism {\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}K_{21}\rightarrow\overline{K}_{21}}. By pullback-pullback decomposition (Lemma A.54(iii)a*), the induced square \Box({\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}K_{21}},{\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}\overline{K}_{21}},{\color[rgb]{0,0,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.4}\overline{K}_{1}},{\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}K_{1}^{\prime}}) (i.e. the inner right “curvy” square) is a pullback, which entails by stability of -morphisms under pullbacks that {\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}K_{21}\rightarrow\overline{K}_{21}} is in . Then by the -van Kampen property, the square \Box({\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}K_{21}},{\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}\overline{K}_{21}},{\color[rgb]{0,0,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.4}\overline{K}_{2}},{\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}K_{2}^{\prime}}) (i.e. the inner left “curvy” square) is a pushout. The composition of the latter pushout (and thus an FPC) square and of the second bottom square from the left in the back of (71) (an FPC) yields an FPC square, while the third from the left bottom back square is a pushout (and thus an FPC), whence, by horizontal FPC decomposition (Lemma A.5410**), we derive that the inner right “curvy” square is an FPC. Consequently, forming the front left “curvy” square as a composition of pushout squares and the front right “curvy” square as a composition of FPCs, we have in summary exhibited an SqPO rewriting step of along the rule {\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}(O_{21}\leftarrow K_{21}\rightarrow I_{21})} and admissible match {\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}m_{21}}.*
“Analysis” part of the proof:
Suppose that we are given an SqPO-composite of linear rules with application conditions with along the SqPO-admissible match {\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}\mu_{21}}=(I_{2}{\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}\leftarrow M_{21}\rightarrow}O_{1}), and that moreover {\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}m_{21}}=({\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}I_{21}\rightarrow}X_{0}) is an SqPO-admissible match of into . Forming a SqPO-rewrite step by applying along {\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}m_{21}} to yields the orange parts of the diagram in (71). In order to prove the claim, we have to construct two SqPO-admissible matches {\color[rgb]{0,0,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.4}m_{1}}\in\mathsf{M}^{sq}_{R_{1}}(X_{0}) and {\color[rgb]{0,0,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.4}m_{2}}\in\mathsf{M}^{sq}_{R_{1}}({\color[rgb]{0,0,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.4}X_{1}}), with {\color[rgb]{0,0,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.4}X_{1}}=R_{1_{{\color[rgb]{0,0,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.4}m_{1}}}}(X_{0}), and that X_{2}\cong R_{2_{{\color[rgb]{0,0,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.4}m_{2}}}}({\color[rgb]{0,0,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.4}X_{1}}) under these assumptions.
We begin by forming the FPC {\color[rgb]{0,0,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.4}\overline{K}_{1}}=\mathsf{FPC}({\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}K_{1}^{\prime}\rightarrow I_{21}\rightarrow}X_{0}), which according to Assumption 2 is guaranteed to exist and to yield two -morphisms {\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}K_{1}^{\prime}}\rightarrow{\color[rgb]{0,0,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.4}\overline{K}_{1}} and {\color[rgb]{0,0,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.4}\overline{K}_{1}}\rightarrow X_{0}. By the universal property of FPCs, there exists a morphism {\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}\overline{K}_{21}}\rightarrow{\color[rgb]{0,0,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.4}\overline{K}_{1}}, which by the -morphism decomposition property is in . Horizontal FPC decomposition (Lemma A.5410*) entails that the square \Box({\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}K_{21}},{\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}\overline{K}_{21}},{\color[rgb]{0,0,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.4}\overline{K}_{1}},{\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}K_{1}^{\prime}}) (inner right “curvy” square) is an FPC. Next, we take the pushout {\color[rgb]{0,0,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.4}X_{1}}=\mathsf{PO}({\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}M_{21}\leftarrow K_{1}^{\prime}\rightarrow}{\color[rgb]{0,0,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.4}\overline{K}_{1}}), followed by forming the FPC*
[TABLE]
Since the inner right “curvy” square \Box({\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}K_{21}},{\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}\overline{K}_{21}},{\color[rgb]{0,0,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.4}\overline{K}_{1}},{\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}K_{1}^{\prime}}) is an FPC and the second from the right bottom back square in (71) a pushout, the composition of these two squares is an FPC and thus a pullback. Then by the universal property of FPCs, there exists a morphism {\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}\overline{K}_{21}}\rightarrow{\color[rgb]{0,0,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.4}\overline{K}_{2}}, which is by the -morphism decomposition property in , and by the horizontal FPC decomposition property, the left inner “curvy” square is an FPC. Noting that the square \Box({\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}K_{21}},{\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}K_{2}^{\prime}},{\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}N_{21}},{\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}K_{1}^{\prime}}) is by assumption a pullback, by pullback-pullback decomposition so is \Box({\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}\overline{K}_{21}},{\color[rgb]{0,0,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.4}\overline{K}_{2}},{\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}X_{1}},{\color[rgb]{0,0,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.4}\overline{K}_{1}}); thus by the -van Kampen property, the left inner “curvy” square is an FPC, noting that the square is in fact a pushout. The latter entails by the universal property of pushouts the existence of a morphism {\color[rgb]{0,0,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.4}\overline{K}_{2}}\rightarrow X_{2}, and then by pushout-pushout decomposition that the leftmost bottom back square in (71) is a pushout (and thus by stability of -morphisms under pushouts that ({\color[rgb]{0,0,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.4}\overline{K}_{2}}\rightarrow X_{2})\in\mathcal{M}).
To complete the proof, note that the rightmost and second from right bottom back squares in (71) are an FPC and a pushout, respectively, thus {\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}m_{21}\vDash\mathsf{c}_{I_{21}}} (with {\color[rgb]{0.9,0.45,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.45,0}\mathsf{c}_{I_{21}}} defined as in (101)) implies that the -morphisms
[TABLE]
*satisfy and according to the properties of the and constructions. It then remains to compose pushout squares and FPC squares in the top and bottom back of the diagram (71) in order to form the two SqPO rewriting steps claimed to exist by the statement of the theorem, which concludes the proof. *
5.5 Associativity of SqPO rewriting with conditions
Based upon the developments presented thus far and on the central result of Behr (2019) (the associativity theorem for SqPO rewriting without rules), we may now state another original contribution of this paper. Due to the structural similarities between the strategies of the associativity proof in the DPO- and SqPO-type cases for rules without application conditions, the following statement is almost verbatim equivalent to the corresponding DPO-type statement. More precisely, in both cases, the part of the proof needed on top of the case without conditions consists of a “diagram chase” involving the and constructions and their properties.
Theorem 5.51** (SqPO-type Associativity Theorem).**
Let be an -adhesive category satisfying Assumption 2. Let () be three linear rules with application conditions. Then there exists a bijection between the sets of pairs of admissible matches and defined as
[TABLE]
with (and defined as in (62)) such that
[TABLE]
and vice versa. In this particular sense, the operation is associative.
Proof 5.52**.**
Referring the interested readers to Behr (2019) for the precise details of the proof for the part of the above statement pertaining to rules without application conditions, and to Behr and Sobocinski (2020) for the generalization of the requisite technical lemmas from the adhesive to the -adhesive setting, suffice it here to quote the following result: the diagram (where we have also indicated the relevant conditions on rules for later convenience) is constructible starting from either of the sets of pairs of SqPO-admissible matches in (102), and thereby proves the bijection for the sets of matches of rules without conditions:
[TABLE]
In contrast to the analogous diagram (75) of the proof of the DPO-type associativity theorem, the nature of the various squares in (104) differs at several positions. For the purpose of proving the part of the SqPO-type associativity theorem pertaining to the conditions on rules, we thus quote from Behr (2019) that
- •
the third and fourth squares in the front (counting from the left) are a pushout and an FPC, respectively
- •
the second to right and rightmost bottom squares are pushouts.
Consequently, it suffices to replace the various applications of the DPO-type compatibility of and (Lemma 4.29) in the proof of Theorem 4.39 with its SqPO-type variant (Theorem 5.46) in order to obtain a proof of the statements of the present Theorem 5.51 pertaining to the conditions on rules.
Example 5.53** (Ex. 4.41 continued).**
It is instructive to compare the associativity property in the SqPO-type variant directly with its counterpart in the DPO-type setting by considering once more the triple rule composition depicted in Figure 2. Note first that since pushout complements along -morphisms are also FPCs, the triple composition at the level of “plain” rules is a valid composition both in DPO- and in SqPO-semantics. However, the two semantics differ at the level of the application conditions. More precisely, since the SqPO-type construction is in a sense “asymmetric” (in that conditions can be transported from the output to the input of a rule, but not vice versa), the “compression” as described in Definition 4.23 for the DPO-setting is not available in the SqPO-setting. Indeed, the application condition
[TABLE]
yields a non-trivial test on candidate matches of rule in the SqPO-rewriting, since an application of at two vertices linked by an arbitrary number of vertices is possible for the “plain” rule in SqPO-rewriting (leading to the implicit deletion of all edges incident to the deleted vertex). Applying the SqPO-type construction as well as , one may compute that the application conditions and are again equivalent to each other, and are found to evaluate to .
Having scratched but the very surface of the intricate matter of causality in SqPO-type rewriting, and referring to Behr (2020); Behr and Krivine (2020) for a more in-depth discussion, suffice it here to mention that it is precisely this type of causality that is of key importance to the analysis of biochemical reaction systems in the Kappa framework Danos et al. (2012); Murphy et al. (2010); Boutillier et al. (2018).
6 Conclusion and Outlook
This paper provides a self-contained account of a class of rewriting theories that possess the special property of compositionality. Based upon the rich theory of “traditional” Double-Pushout (DPO) Ehrig et al. (1973, 1991); Corradini et al. (1997); Rozenberg (1997); Ehrig et al. (2006a, 2008, 2010); Habel and Plump (2012a); Ehrig et al. (2014) and Sesqui-Pushout (SqPO) Corradini et al. (2006); Löwe (2015) rewriting in the setting of -adhesive categories Lack and Sobociński (2005); Ehrig et al. (2006b); Braatz et al. (2014), we lift our earlier results on compositional concurrency and compositional associativity as developed in Behr et al. (2016a); Behr and Sobocinski (2018); Behr (2019); Behr and Sobocinski (2020) to the realm of rewriting systems with conditions on objects and morphisms.
A key original contribution of the present paper is a derivation of the precise technical conditions under which compositionality in the aforementioned sense is attainable for a given rewriting theory. Concretely (cf. Section 2), it has proved essential to suitably adapt the requirements on the host categories for both DPO- and SqPO-type rewriting with application conditions on objects and morphisms Pennemann (2008); Habel and Pennemann (2009); Ehrig et al. (2014); Hermann et al. (2014); Golas et al. (2014), concluding that these categories should be -adhesive and possess certain additional properties such as the existence of epi--factorizations and -effective unions as described in Assumptions 1 (DPO-case) and 2 (SqPO-case).
Our second original contribution consists of a refinement of the theory of conditions in -adhesive categories as presented in Section 3. For categories satisfying either of the assumptions mentioned earlier, it is possible to refine a central construction of the theory of conditions, the so-called shift construction, into a form that leads to new results on the interplay of rewriting rules and conditions. In particular, the transport construction is shown to possess a compatibility property in interaction with the shift construction, which is required to ensure compositionality of rewriting with conditions.
The main results of this paper are the compositional concurrency and associativity of rewriting with conditions in both the DPO (Section 4) and SqPO (Section 5) cases, demonstrated to hold under the aforementioned assumptions. Our proof strategy and techniques rely heavily on earlier developments in the setting of rewriting without conditions Behr and Sobocinski (2018); Behr (2019) in conjunction with the aforementioned results on the properties of the refined shift and transport constructions. While admittedly a rather technical work, we believe that our results can serve as a starting point for a new generation of developments in the field of rewriting, in particular in view of static analysis tasks. Indeed, in most applications of practical interest, idealized data structures such as multigraphs must be restricted to more rigid structures (such as e.g. site graphs in the Kappa framework Danos and Laneve (2004); Boutillier et al. (2018)) in order to obtain tractable algorithms of sufficient predictive power. First results in the fields of stochastic mechanics of continuous-time Markov chains based upon stochastic rewriting systems Behr et al. (2016a); Behr and Sobocinski (2018); Behr (2019); Behr et al. (2020a) hint at a great potential of the framework of compositional rewriting with conditions as presented here. We recently demonstrated that based upon the results of the present paper, it is possible to develop a faithful encoding of both bio- and organo-chemical reaction systems via typed undirected simple graphs with suitable sets of additional structure constraints Behr and Krivine (2020). Together with the respective SqPO- and DPO-type stochastic mechanics frameworks introduced in Behr and Krivine (2020), a direct and in-detail comparison of the sophisticated rule-based modeling frameworks Kappa Boutillier et al. (2018) and BioNetGen Harris et al. (2016) (SqPO/biochemistry) as well as MØD Andersen et al. (2016) (DPO/organic chemistry) with the general theory of categorical rewriting over -adhesive categories has become possible. As a first hint at the potential of such an approach in view of the development of algorithmic implementations of rewriting-theoretical concepts, we have recently presented a first prototype of an implementation of SqPO-type compositional rewriting systems for rules with conditions based upon the present theory as well as on the Microsoft Z3 SMT-solver in Behr et al. (2020b). Work in progress further includes the theory of tracelets as introduced in Behr (2020), whereby the classical concept of derivation traces (i.e. of sequences of applications of rewriting rules) is analyzed via exploiting the associativity theorems in order to characterize a derivation trace of length in terms of a minimal derivation trace of the same length (a so-called tracelet of length ). As briefly touched upon in the discussion of Examples 4.41 and 5.53 (which consider the case of a “triple” composite of rules, i.e. the case ), compositional associativity of the operations of DPO- and SqPO-type rule compositions (Theorems 4.39 and 5.51) opens the possibility to statically generate such minimal derivation traces without the need to first obtain generic derivation traces (either from simulations or from unfoldings), posing thus considerable potential in terms of analyzing pathways and their dynamics in chemical reaction systems.
Appendix A Collection of technical lemmata for -adhesive categories
In many practical computations in the framework of -adhesive categories, one may take advantage of a number of technical results, some of which elementary, some of which rather specialized (such as in particular the lemmata pertaining to final pullback complements (FPCs)). For the readers’ convenience, we provide here the full list of results used in the framework of this paper. The list is an adaptation of the list provided in Behr (2019) from the setting of adhesive to -adhesive categories. Note also that while the category-theoretical constructions of objects and morphisms via pullbacks, pushouts, pushout complements and FPCs are by definition unique only up to universal isomorphisms, we follow standard practice in simplifying our notations by employing a convention whereby e.g. the pushout of an isomorphism as in (105)(A) is denoted by “equality arrows” (rather than keeping a notation with generic labels and decorations on arrows).
Lemma A.54**.**
Let be a category.
- (i)
“Single-square” lemmas (see e.g. Behr and Sobocinski (2020), Lem. 1.7):* In any category, given commutative diagrams of the form*
[TABLE]
- (a)
* is a pushout for arbitrary morphisms ,* 2. (b)
* is a pullback if and only if the morphism is a monomorphism,* 3. (c)
* is a pullback for arbitrary morphisms if is a monomorphism,* 4. (d)
If and is a pullback, then . 2. (ii)
special -adhesivity corollaries* (cf. e.g. Ehrig et al. (2014)**, Lemma 2.6): in any adhesive category,*
- (a)
pushouts along -morphisms are also pullbacks, 2. (b)
(uniqueness of pushout complements) given an -morphism and a generic morphism , the respective pushout complement (if it exists) is unique up to isomorphism, and with (due to stability of -morphisms under pushouts). 3. (iii)
“Double-square lemmas”**: given commutative diagrams of the shapes
[TABLE]
then in any category (cf. e.g. Lack and Sobociński (2005)**):
- (a)
Pullback-pullback (de-)composition*: If is a pullback, then is a pullback if and only if is a pullback.* 2. (b)
Pushout-pushout (de-)composition*: If is a pushout, then is a pushout if and only if is a pushout.*
If the category is -adhesive:
- (c)
pushout-pullback decomposition* (Ehrig et al. (2014)**, Lemma 2.6): If is a pushout, is a pullback, and if and ( or ), then and are both pushouts (and thus also pullbacks).* 2. (d)
pullback-pushout decomposition* (Golas et al. (2014)**, Lem. B.2): if is a pullback, a pushout, commutes and , then is a pullback.* 3. (e)
Horizontal FPC (de-)composition* (cf. Corradini et al. (2006), Lem. 2 and Lem. 3, compare Löwe (2015), Prop. 36):101010It is worthwhile emphasizing that in these FPC-related lemmas, the “orientation” of the diagrams plays an important role. Moreover, the precise identity of the pair of morphisms that plays the role of the final pullback complement in a given square can be inferred from the “orientation” specified in the condition part of each statement. If is an FPC (i.e. if is FPC of ), then is an FPC if and only if is an FPC.* 4. (f)
Vertical FPC (de-)composition* (ibid): if is an FPC (i.e. if is FPC of ), then*
- i.
if is an FPC (i.e. if is FPC of ), then is an FPC (i.e. is FPC of ); 2. ii.
if is an FPC (i.e. if is FPC of ), and if is a pullback, then is an FPC (i.e. is FPC of ). 5. (g)
Vertical FPC-pullback decomposition* (compare Löwe (2015)**, Lem. 38): If , if is a pullback and if is an FPC (i.e. if is FPC of ), then and are FPCs.*
If the category is -adhesive and in addition possesses an epi--factorization and -effective unions:
- (h)
Vertical FPC-pushout decomposition*: If all morphisms of the squares and except are in , if , if is a pushout and if is an FPC (i.e. if is FPC of ), then is an FPC and .*
Proof A.55**.**
Proofs of all but the very last statement are found in the references quoted in each statement. It thus remains to prove our novel vertical FPC-pushout decomposition result (in the setting of -adhesive categories). To this end, we first invoke pullback-pushout decomposition (Lemma A.54((iii)d)): since is an FPC and thus in particular a pullback, since is a pushout, commutes, and finally since , we find that is a pullback.
In order to demonstrate that , construct the commutative cube below left:
[TABLE]
Since the bottom square is the FPC (and thus pullback) , and since the right square is a pullback via Lemma A.54((i)c) (because ), by pullback composition the square (the right plus the bottom square) is a pullback. Thus assembling the commutative diagram as shown above right, since by assumption is a pushout and all arrows except are in , invoking the property of -effective unions (Definition 5) allows us to prove that also . Finally, by applying vertical FPC-pullback decomposition, we conclude that is an FPC.
Appendix B Closure of under isomorphisms
As mentioned in the main text, the definition of -adhesive categories as given in Definition 1 is well known to be overcomplete. With the -decomposition property derivable directly via stability of -morphisms under pullbacks, we present below a derivation of the fact that contains all isomorphisms.
- (i)
Given an arbitrary -morphism , since , by the decomposition property of -morphisms (Definition 1), we find that , for every . 2. (ii)
Let be an isomorphism, and take the pullback of the cospan , resulting in a span . Then by stability of -morphisms under pullback (Definition 1), we conclude that (i.e. by -decomposition also ).
Appendix C Some useful consequences of epi--factorizations
Lemma C.56**.**
Let be an -adhesive category satisfying Assumption 1. Then given a commutative diagram as below left where and is an arbitrary morphism,
[TABLE]
then if the epi--factorization of the morphism reads , with and , and if we form the pullback (thus inducing by the universal property a morphism ), then .
Proof C.57**.**
Note first that by virtue of stability of -morphisms under pullbacks and by the decomposition property of -morphisms, respectively, one may conclude that and (since ). Next, form the commutative cube diagram as depicted in the right part of (108). The left square is a pullback (Lemma A.54(i)c), and so is the top square (Lemma A.54(i)a). Since by construction also the bottom square is a pullback, by virtue of pullback-pullback decomposition (Lemma A.54(iii)a), the right square is a pullback. Thus by stability of isomorphisms under pullbacks (Lemma A.54(i)d), we obtain that .
Appendix D Some useful consequences of (strict) -initiality
In the case that an -adhesive category possesses a (strict) -initial object, the following useful properties can be derived.
Lemma D.58**.**
Let be an -adhesive category with -initial object . Then the commutative diagram of -morphisms below is both a pushout and a pullback:
[TABLE]
Proof D.59**.**
Consider the following commutative diagram:
[TABLE]
Since the outer square and the left square are pushouts, according to the pushout-pushout decomposition property stated in Lemma A.54(iii)b, the right inner square is also a pushout (and thus a pullback).
Lemma D.60**.**
Let be an -adhesive category with a strict -initial object , and consider the commutative diagrams of -morphisms below,
[TABLE]
If is a pullback, then , and if is a pullback, then .
Proof D.61**.**
Consider the following auxiliary commutative diagrams:
[TABLE]
The left diagram is formed by taking a pullback to obtain the bottom square, followed by taking the appropriate pullbacks to form the left and right squares (which induces the dotted arrow by the universal property of pullbacks). Since the left, back and right squares are pullbacks, by pullback-pullback decomposition (see Lemma A.54(iii)a) so is the front square. Then by stability of isomorphisms under pullbacks (see Lemma A.54(i)d), . The right diagram is constructed in precisely the same fashion, thus proving that .
The notion of strict -initiality also plays an interesting role in our framework of conditions on objects and rewriting rules studied in the main part of this paper due to the following result:
Lemma D.62** (-morphisms into binary coproducts).**
Let be an -adhesive category (for a class of monomorphisms) that possesses a strict -initial object . Then for all objects , if there exists an -morphism , then with
[TABLE]
and consequently (by the universal property of binary coproducts) (with and both in ).
Proof D.63**.**
Construct the following commutative cube, with the bottom square a pushout, and where the front and left faces are formed by taking pullbacks as described in (113) in order to obtain and , followed by forming , which provides an arrow by the universal property of pushouts (since the bottom square is a PO):
[TABLE]
By virtue of strict -initiality of , the existence of the arrow entails that . Since the bottom square is a pushout, all vertical squares are pullbacks and all vertical morphisms are in , by the -van Kampen property the top square is a pushout. Thus by uniqueness of pushouts up to isomorphisms, and the claim follows.
Acknowledgments.
The work of NB was supported by a Marie Skłodowska-Curie Individual fellowship (Grant Agreement No. 753750 – RaSiR). We would like to thank P.A.M. Melliès, P. Sobociński and N. Zeilberger for fruitful discussions.
The reference list from the paper itself. Each links out to its DOI / PubMed record.
- 1Abou-Jaoudé et al. (2016) Wassim Abou-Jaoudé, Denis Thieffry, and Jérôme Feret. Formal derivation of qualitative dynamical models from biochemical networks. Biosystems , 149:70–112, 2016. https://doi.org/10.1016/j.biosystems.2016.09.001 . · doi ↗
- 2Adámek et al. (1990) Jiř\́@nil Adámek, Horst Herrlich, and George Strecker. Abstract and concrete categories, 1990.
- 3Andersen et al. (2016) Jakob L. Andersen, Christoph Flamm, Daniel Merkle, and Peter F. Stadler. A Software Package for Chemically Inspired Graph Transformation. In R. Echahed and M. Minas, editors, Graph Transformation (ICGT 2016) , volume 9761 of Lecture Notes in Computer Science, , pages 73–88, Cham, 2016. Springer International Publishing. https://doi.org/10.1007/978-3-319-40530-8_5 . · doi ↗
- 4Andersen et al. (2019) Jakob L. Andersen, Christoph Flamm, Daniel Merkle, and Peter F. Stadler. Chemical Transformation Motifs — Modelling Pathways as Integer Hyperflows. IEEE/ACM Transactions on Computational Biology and Bioinformatics , 16(2):510–523, 2019. https://doi.org/10.1109/tcbb.2017.2781724 . · doi ↗
- 5Andersen et al. (2018 a) Jakob Lykke Andersen, Rolf Fagerberg, Christoph Flamm, Rojin Kianian, Daniel Merkle, and Peter F Stadler. Towards mechanistic prediction of mass spectra using graph transformation. MATCH Commun. Math. Comput. Chem. , 80:705–731, 2018 a.
- 6Andersen et al. (2018 b) Jakob Lykke Andersen, Christoph Flamm, Daniel Merkle, and Peter F Stadler. Rule composition in graph transformation models of chemical reactions. MATCH Commun. Math. Comput. Chem. , 80(661-704):45, 2018 b.
- 7Banzhaf et al. (2015) Wolfgang Banzhaf, Christoph Flamm, Daniel Merkle, and Peter F. Stadler. Algorithmic Cheminformatics (Dagstuhl Seminar 14452). Dagstuhl Reports , 4(11):22–39, 2015. https://doi.org/10.4230/Dag Rep.4.11.22 . · doi ↗
- 8Behr (2019) Nicolas Behr. Sesqui-Pushout Rewriting: Concurrency, Associativity and Rule Algebra Framework. In Rachid Echahed and Detlef Plump, editors, Proceedings of the Tenth International Workshop on Graph Computation Models (GCM 2019) in Eindhoven, The Netherlands , volume 309 of Electronic Proceedings in Theoretical Computer Science , pages 23–52. Open Publishing Association, 2019. https://doi.org/10.4204/eptcs.309.2 . · doi ↗