Sesqui-Pushout Rewriting: Concurrency, Associativity and Rule Algebra Framework
Nicolas Behr (Universit\'e de Paris, IRIF, CNRS)
TL;DR
This paper introduces a concurrency theorem and associativity property for sesqui-pushout (SqPO) graph rewriting, enabling the development of rule algebras and stochastic models for complex transformations.
Contribution
It provides the first concurrency theorem and associativity framework for SqPO rewriting, facilitating algebraic and probabilistic analysis of graph transformations.
Findings
Established a concurrency theorem for SqPO rewriting
Proved associativity property for SqPO rule compositions
Constructed rule algebras for stochastic rewriting systems
Abstract
Sesqui-pushout (SqPO) rewriting is a variant of transformations of graph-like and other types of structures that fit into the framework of adhesive categories where deletion in unknown context may be implemented. We provide the first account of a concurrency theorem for this important type of rewriting, and we demonstrate the additional mathematical property of a form of associativity for these theories. Associativity may then be exploited to construct so-called rule algebras (of SqPO type), based upon which in particular a universal framework of continuous-time Markov chains for stochastic SqPO rewriting systems may be realized.
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 14
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 31Peer 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.
\NewEnviron
mycd[1][]{tikzpicture}[baseline=(current bounding box.west), transform shape, scale=1] \node[inner sep=0, outer sep=0] {tikzcd}[#1] \BODY;
Sesqui-Pushout Rewriting:
Concurrency, Associativity and Rule Algebra Framework††thanks: This project has received funding from the European Union’s Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie grant agreement No 753750.
Nicolas Behr Université de Paris, IRIF, CNRS
F-75013 Paris, France [email protected]
Abstract
Sesqui-pushout (SqPO) rewriting is a variant of transformations of graph-like and other types of structures that fit into the framework of adhesive categories where deletion in unknown context may be implemented. We provide the first account of a concurrency theorem for this important type of rewriting, and we demonstrate the additional mathematical property of a form of associativity for these theories. Associativity may then be exploited to construct so-called rule algebras (of SqPO type), based upon which in particular a universal framework of continuous-time Markov chains for stochastic SqPO rewriting systems may be realized.
1 Motivation and relation to previous work
The framework of Sesqui-Pushout (SqPO) rewriting has been introduced relatively recently in [17] as a novel alternative to the pre-existing algebraic graph transformation frameworks known as Double-Pushout (DPO) [27, 25, 18, 35] and Single-Pushout (SPO) rewriting [33, 36, 39]. In the setting of the rewriting of graph-like structures, the distinguishing feature of the aforementioned DPO-type rewriting is that the deletion of vertices with incident edges is only possible if the incident edges are explicitly deleted via the application of the rewriting rule. In contrast, in both the SqPO and the SPO rewriting setups, “deletion in unknown context” is implementable. Thus for practical applications of rewriting, in particular in view of the modeling of stochastic rewriting systems, the S(q)PO rewriting semantics provide an important additional option for the practitioners, and will thus in particular complement the existing DPO-type associative rewriting and rule algebra framework as introduced in [4, 8]. Referring the interested readers to [37] for a recent review and further conceptual details of the three approaches, suffice it here to quote that SqPO and SPO rewriting via linear rules111While non-linear rules in SqPO rewriting have interesting applications in their own right (permitting e.g. the cloning and fusing of vertices in graphs), this most general case is left for future work. (defined as monic spans) and along monomorphic matches effectively encode the same semantics of rewriting. We chose (by the preceding argument without loss of expressivity) to develop the theory of associative rewriting within the SqPO rather than the SPO setting, since the SqPO framework bears certain close technical similarities to the DPO rewriting framework, which proved crucial in finding a strategy for the highly intricate proofs of the concurrency and associativity theorems presented in this paper. While it is well-known (see e.g. Section 5.1 of [17]) that DPO- and SqPO-type semantics coincide for certain special classes of linear rules (essentially rules that do not delete vertices), and while these cases might provide some valuable cross-checks of technical results to the experts, SqPO-type semantics is in its full generality a considerably more intricate variant of semantics due to its inherent “mixing” of pushouts with final pullback complements. It should further be noted that we must impose a set of additional assumptions on the underlying adhesive categories (see Assumption 1) in order to ensure certain technical properties necessary for our concurrency and associativity theorems to hold. To the best of our knowledge, apart from some partial results in the direction of developing a concurrency theorem for SqPO-type rewriting in [17, 37, 16], prior to this work neither of the aforementioned theorems had been available in the SqPO framework.
Associativity of SqPO rewriting theories plays a pivotal role in our development of a novel form of concurrent semantics for these theories, the so-called SqPO-type rule algebras. Previous work on associative DPO-type rewriting theories [4, 6, 8] (see also [9]) has led to a category-theoretical understanding of associativity that may be suitably extended to the SqPO setting. In contrast to the traditional and well-established formalisms of concurrency theory for rewriting systems (see e.g. [43, 26, 24, 16] for DPO-type semantics and [17, 16] for a notion of parallel independence and a Local Church-Rosser theorem for SqPO-rewriting of graphs), wherein the focus of the analysis is mostly on derivation traces and their sequential independence and parallelism properties, the focus of our rule-algebraic approach differs significantly: we propose instead to put sequential compositions of linear rules at the center of the analysis (rather than the derivation traces), and moreover to employ a vector-space based semantics in order to encode the non-determinism of such rule compositions. It is for this reason that the concurrency theorem plays a quintessential role in our rule algebra framework, in that it encodes the relationship between sequential compositions of linear rules and derivation traces, which in turn gives rise to the so-called canonical representations of the rule algebras (see Section 4). This approach in particular permits to uncover certain combinatorial properties of rewriting systems that would otherwise not be accessible. While undoubtedly not a standard technique in the realm of theoretical computer science, certain special examples of rule algebras are ubiquitous in many areas of applied mathematics and theoretical physics. The most famous such example concerns the so-called Heisenberg-Weyl algebra (see e.g. [10, 11, 12]), which is well-known to possess a representation in terms of the formal multiplication operator and the differentiation operator on formal power series in the formal variable , with and acting as the derivative. Referring the interested readers to Example 2 (see also [8, 5]) for the precise details, it transpires that the monomials (for a non-negative integer) are found to be in one-to-one correspondence with graph states associated to -vertex discrete graphs, while and may be understood as the canonical representations of the discrete graph rewriting rules of creation and deletion of vertices. It will thus come as no surprise that considering more general rewriting rules than those of discrete graphs will lead to a very substantial generalization of these traditional results and techniques.
From the very beginning of the development of the rule algebra framework [4], one of our main motivations has been the study of stochastic rewriting systems, whence of continuous-time Markov chains (CTMCs) based upon DPO- or SqPO-type rewriting rules. While previously in particular applications of stochastic SqPO-type rewriting systems have played a role predominantly in highly specialized settings such as e.g. the formulation of the biochemical reaction system framework known as Kappa [21, 22, 20, 19], our novel approach of formulating such systems in terms of associative unital rule algebras may very well open this versatile modeling technique to many other areas of applied research. In conjunction with our previously developed DPO-type framework in [8], one could argue that our stochastic mechanics frameworks are in a certain sense a universal construction, in that once a semantics for associative unital rewriting is provided, the steps necessary to obtain the associated CTMCs are clearly formalized. It is interesting to compare the traditional approaches to stochastic rewriting systems with CTMC semantics such as [32, 31] in the DPO- and [30] in the SPO-settings to our present reformulation in terms of rule algebras. The former approaches yet again tend to focus on derivation traces of stochastic rewriting systems, while our rule-algebraic approach aims to extract dynamical information from stochastic rewriting systems via analysis of certain combinatorial relationships (so-called nested commutators) of the infinitesimal generator of the CTMC with the (pattern-counting) observables of the system. It is via these relations that one may in certain cases obtain exact closed-form solutions for such dynamical data (see e.g. Section 6). It would nevertheless be an intriguing avenue for future research to understand better the finer points of the “traditional” stochastic rewriting frameworks (which also feature sophisticated developments in terms of probabilistic model-checking and various types of stochastic logics), and furthermore whether or not rule-algebraic techniques might be of interest also in more general stochastic rewriting semantics such as probabilistic (timed) graph transformations [34, 41].
Structure of the paper: In Section 2, some category-theoretical background material is provided. The key results of associativity and concurrency of SqPO rewriting are presented in Section 3, followed by the construction of SqPO-type rule algebras in Section 4. The second part of the paper contains the stochastic mechanics framework (Section 5) as well as a practical application example (Section 6). Technical proofs are situated in the Appendix.
2 Background: adhesive categories and final pullback complements
We recall some of the elementary definitions and properties related to the notions of adhesive categories, upon which our framework will rely.
Definition 1** ([35]).**
A category is said to be adhesive if
- (i)
has pushouts along monomorphisms, 2. (ii)
has pullbacks, 3. (iii)
pushouts along monomorphisms are van Kampen (VK) squares.
The last property entails that in a commutative cube as in (1) on the left where the bottom square is a pushout, this square is a VK square if and only if whenever the back and right vertical faces are pullbacks, then the top square is a pushout if and only if the front and left vertical squares are pullbacks.
[TABLE]
We will be exclusively interested in categories that satisfy certain finiteness properties (in order to ensure finiteness of the sets of matches for rule applications and compositions, see Section 3):
Definition 2** (Finitary categories [13]).**
A category is said to be finitary if every object has only finitely many subobjects (i.e. if there only exist finitely many monomorphisms up to isomorphism for every ). For every adhesive category , the restriction to finite objects of defines a full subcategory called the finitary restriction of .
Theorem 1** (Finitary restrictions; [13], Thm. 4.6).**
The finitary restriction of any adhesive category is a finitary adhesive category.
Adhesive categories have been introduced and advocated in [35] as a framework for rewriting due to their numerous useful properties, some of which are listed in Appendix A for the reader’s convenience. One of the central concepts in the theory of SqPO rewriting is the following:
Definition 3** (Final Pullback Complement (FPC); [17, 37]).**
Let be a category. Given a commutative diagram as in (1) on the right, a pair of morphisms is a final pullback complement (FPC) of a pair if (i) is a pullback of (i.e. if the square marked is a pullback square), and (ii) for each collection of morphisms as in (1) on the right, where is pullback of and where , there exists a unique morphism with and .
For our associative rewriting framework, it will be crucial to work with a category in which (i) FPCs are guaranteed to exist when constructing them for composable pairs of monomorphisms, and (ii) monomorphisms are stable under FPCs, i.e. FPCs of pairs of monomorphisms are given by pairs of monomorphisms. This property is satisfied by adhesive categories (cf. Lemma 3 of Appendix A), yet to the best of our knowledge the question of which more general types of categories possess this property has not yet been investigated to quite the level of generality as analogous classification problems in the case of DPO rewriting, even though there does exist a large body of work on classes of categories that admit SqPO constructions [17, 40, 37, 15, 38]. Within these classes, according to [14, 15] guarantees for the existence of FPCs may be provided for categories that possess a so-called -partial map classifier. However, it appears to be an open question of whether the statement of Lemma 3 on stability of monomorphisms under FPCs may be generalized to the setting of -adhesive categories, where is a class of monomorphisms. Relaying such questions to future work, we refer to Lemma 4 of Appendix A for a well-known instantiation of a suitable categorical setting from the SqPO literature in the form of the category of finite directed multigraphs, which also serves to illustrate the FPC construction.
Assumption 1**.**
* is an adhesive category in which all FPCs along monomorphisms exist, and in which monomorphisms are stable under FPCs.*
3 Sesqui-Pushout rewriting
We will now develop a framework for Sesqui-Pushout (SqPO) rewriting in the setting of a category satisfying Assumption 1, in close analogy to the framework of associative Double-Pushout (DPO) rewriting as introduced in [8, 9]. Unlike in the general setting of SqPO rewriting, we will thus be able to not only prove a concurrency theorem (Section 3.1), but also an associativity property of the SqPO-type rule composition (Section 3.2).
3.1 Concurrent composition and concurrency theorem
For reasons that will become more transparent when introducing the SqPO-type rule algebra framework starting from Section 4, we opt for a non-standard convention of reading spans of monomorphisms “from right to left” (rather than the traditional “left to right”), which is why we will speak of “input” and “output” of rules rather than “left-” and “right hand sides” to avoid confusion.
Definition 4** (SqPO-type rewriting; compare [17], Def. 4).**
Let be an adhesive category satisfying Assumption 1. Denote by the set of (isomorphism classes222Two productions and are defined to be isomorphic if there exist isomorphisms , and that make the obvious diagram commute; we will not distinguish between isomorphic productions. As natural in this category-theoretical setting, the constructions presented in the following are understood as defined up to such isomorphisms. of) so-called linear productions, defined as the set of spans of monomorphisms,
[TABLE]
Given an object and a linear production , we denote the set of SqPO-admissible matches as the set of monomorphisms . 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 production and admissible match , and denoted .
Next, a notion of sequential composition of productions is introduced:
Definition 5** (SqPO-type concurrent composition).**
Let be two linear productions. Then an overlap of the output object of with the input object of , encoded as a span
[TABLE]
with , is called an SqPO-admissible match of into , denoted , if the square marked in (4) is constructible as a pushout complement (with the cospan obtained by taking the pushout marked {\color[rgb]{0,0,0.4}\mathsf{PO}}). In this case, the remaining parts of the diagram are formed by taking the final pullback complement marked and the pushouts marked :
[TABLE]
If , we write for the composite of with along the admissible match , defined as
[TABLE]
Due to stability of monomorphisms under pushouts, pullbacks and FPCs in the setting of a category satisfying Assumption 1, all morphisms in Definitions 4 and 5 are guaranteed to be monomorphisms, whence in particular the span is a span of monomorphisms and thus indeed an element of .
At first sight, it might appear irritating that in the definition of the SqPO-type rule composition, the right hand part of (4) involves a pushout complement (marked ), while the left hand part of the diagram in (4) features a final pullback complement (marked ). Intuitively, considering the case of graph rewriting for concreteness, in a given sequential application of two productions, while the application of the first production may lead to implicit edge deletions, the second production is incapable of having any causal interaction with edges deleted by the first production. In contrast, the second production may in a given sequential application very well implicitly delete edges present in the output object of the first production, which explains the presence of the FPC in the defining equation (4). We refer the interested readers to [6] for further intuitions attainable in terms of so-called rule diagrams for presenting rule compositions. The justification for Definition 5 in the general case is provided via the following concurrency theorem. Even though at least in certain specialized settings the “synthesis” part of this theorem has been foreseen already in [37] (where it is also commented that a full concurrency theorem for SqPO rewriting might be attainable), the following result appears to be new.
Theorem 2** (SqPO-type Concurrency Theorem).**
Let be an adhesive category satisfying Assumption 1. Let be two linear rules and an object.
- •
Synthesis:* Given a two-step sequence of SqPO derivations*
[TABLE]
with and , there exists a SqPO-composite rule for a unique , and a unique SqPO-admissible match , such that
[TABLE]
- •
Analysis:* Given an SqPO-admissible match of into and an SqPO-admissible match of the SqPO-composite into , there exists a unique pair of SqPO-admissible matches and with such that*
[TABLE]
Proof.
See Appendix B.1. ∎
3.2 Composition and associativity
The following theorem establishes that in analogy to the DPO rewriting setting of [8], also the sesqui-pushout variant of rule compositions possesses a form of associativity property.
Theorem 3** (SqPO-type associativity theorem).**
Let be an adhesive category satisfying Assumption 1. Then the SqPO-composition operation on linear productions of is associative in the following sense: given linear productions , there exists a bijective correspondence between pairs of SqPO-admissible matches and such that
[TABLE]
Proof.
Intuitively, the associativity property in the SqPO case manifests itself in a form entirely analogous to the DPO case [8], whereby the data provided along the path highlighted in orange below permits to uniquely compute the data provided along the path highlighted in blue and vice versa (with both sets of overlaps computing the same “triple composite” production that is encoded as the composition of the three spans in the bottom front row):
[TABLE]
See Appendix B.2 for the precise technical details of the proof. ∎
We invite the interested readers to compare the SqPO-type constructions presented here against those contained in the extended journal version [9] of [8] for the DPO framework, since this might lend some intuitions on the otherwise very abstract nature of the proofs to the experts.
4 From associativity to SqPO-type rule algebras
For the rule algebra constructions, we will require an additional structure:
Definition 6** (Initial objects).**
An object of some category is said to be a strict initial object if for every object , there exists a unique morphism , and if any morphism must be an isomorphism.
For example, the category and its finitary restriction possess a strict initial object (the empty graph). For the experts, it appears worthwhile noting the following result:
Lemma 1** (Extensive categories; [35], Lem. 4.1).**
An adhesive category is an extensive category333For the purposes of this paper, it suffices to consider the “if” direction as a definition of extensivity, since the relevant structure to our constructions is that of having a strict initial object (see e.g. [35] for the precise definition of extensivity). if and only if it possesses a strict initial object.
Assumption 2** (Prerequisites for SqPO-type rule algebras).**
We assume that is an adhesive category satisfying Assumption 1, and which is in addition finitary and possesses a strict initial object .
Definition 7** (SqPO-type rule algebras).**
Let be defined as an isomorphism from to the basis of a free -vector space , such that444Recall that for a set , the notation entails to “take the -span over basis vectors indexed by elements of ”, i.e. elements of the resulting -vector space are (finite) linear combinations of the basis vectors with real coefficients .
[TABLE]
In order to clearly distinguish between elements of and basis vectors of , we introduce the notation
[TABLE]
Define the SqPO rule algebra product on a category that satisfies Assumption 2 as the binary operation
[TABLE]
where for two basis vectors encoding the linear rules (),
[TABLE]
The definition is extended to arbitrary (finite) linear combinations of basis vectors by bilinearity, whence for and ,
[TABLE]
We call the SqPO-type rule algebra over the finitary adhesive and extensive category .
The rule algebra product for () thus encodes the non-determinism in the SqPO-type sequential composition of the linear rule with in terms of the “sum over all possible compositions”. As the following example illustrates, since is defined to map from isomorphism classes of linear rules to basis vectors of , and since two distinct matches may lead to isomorphic composite rules, typically evaluates to a linear combination of basis vectors with integer coefficients:
Example 1**.**
Let be the category of finite directed multigraphs, with the empty graph. Then with , we find for example
[TABLE]
The result of the composition thus captures the combinatorial insight that there are two contributions that evaluate to an isomorphic rule algebra element. More generally, one finds the following structure of compositions of rule algebra elements based upon “discrete” graph rewriting rules: letting denote the -vertex graph without edges (for ), one finds (for )
[TABLE]
This result is further interpreted in Example 2.
Theorem 4** (Properties of ).**
For every category satisfying Assumption 2, the associated SqPO-type rule algebra is an associative unital algebra, with unit element . (Proof: Appendix B.3)
For the unital and associative SqPO-type rule algebras, one may provide a notion of representations in analogy to the DPO-type case (compare [4, 8]):
Definition 8** (Canonical representation of ).**
Let be a category satisfying Assumption 2, with a strict initial object , and let be its associated rule algebra of SqPO type. Denote by the free -vector space spanned by basis vectors indexed by isomorphism classes of objects,
[TABLE]
Then the canonical representation of is defined as a morphism from the SqPO-type rule algebra to endomorphisms of , with
[TABLE]
and extended to arbitrary elements of and of by linearity.
Example 2**.**
Extending Example 1, letting , note first that by definition for all (isomorphism classes of) finite multigraphs , . With
[TABLE]
as a consequence of (14) of Example 1 one may verify that
[TABLE]
In other words, the data of (17) and (18) furnishes a representation of the famous Heisenberg-Weyl algebra that is of fundamental importance in combinatorics and physics (see e.g. [10, 11, 12]). An alternative such representation is given by the linear operators (multiplication by ) and (derivation by ) acting on the -vector space spanned by monomials , which reproduces equations isomorphic to (17) and (18), with and . However, the action of and is of course defined on all states with , so that we may e.g. compute the following “derivative of a graph”:
[TABLE]
The following theorem states that as given in Definition 8 is indeed a homomorphism (and thus qualifies as a representation of ).
Theorem 5** (SqPO-type canonical representation).**
For a category satisfying Assumption 2, of Definition 8 is a homomorphism of unital associative algebras. (Proof: Appendix B.4)
5 Applications of SqPO-type rule algebras to stochastic mechanics
In practical applications of stochastic rewriting systems, the type of rewriting semantics presents one of the key design choices. For example, if in a given situation a stochastic graph rewriting system should be implemented, choosing DPO- vs. SqPO-type rewriting entails two entirely different semantics in terms of the behavior of vertex deletion rules: in the former case, vertices may only be deleted if also all its incident edges are explicitly deleted as well, while in the latter case no such restriction applies (i.e. an application of a vertex deletion rule “automatically” leads to the deletion of all incident edges). Evidently, such fundamentally different behavior at the level of rewriting rules will also have strong influence on the dynamical behavior of the associated stochastic rewriting systems, whence it is of considerable practical interest to have a universal implementation of such systems available in both formalisms. We begin by specializing the general definition of continuous-time Markov chains (see e.g. [42, 2]) to the setting of SqPO-type rewriting systems in close analogy to [4, 7, 8].
Definition 9** (Continuous-time Markov Chains (CTMCs); compare [8], Def. 7.1).**
Let be a category satisfying Assumption 2, and which in addition possesses a countable set of isomorphism classes of objects . Let denote the free -vector space introduced in Definition 8. We define the space as the space of sub-probability distributions in the following sense:
[TABLE]
Let be the space of endomorphisms of , with elements referred to as sub-stochastic operators. Then a continuous-time Markov chain (CTMC) is specified in terms of a tuple of data , where is the initial state, and where is the infinitesimal generator or Hamiltonian of the CTMC (with the space of real-valued sequences indexed by elements of and with finite coefficients). is required to be an infinitesimal (sub-) stochastic operator, which entails that for and for all ,
[TABLE]
Then this data encodes the evolution semi-group as the (point-wise minimal non-negative) solution of the Kolmogorov backwards or master equation:
[TABLE]
Consequently, the time-dependent state of the system is given by
[TABLE]
An important technical aspect of the above definition of CTMCs is the definition of the relevant space of (sub-)probability distributions in interaction with the definition of the infinitesimal generator and of the space . Some remarks on this interaction and a short explanation of the relevant mathematical concepts are provided in Appendix B.5.
Our main approach in studying CTMCs based on rewriting systems will consist in analyzing the dynamical statistical behavior of so-called observables:
Definition 10** (Observables; [8], Def. 7.1).**
Let denote the space of observables, defined as the space of diagonal operators555Depending on the concrete case, the eigenvalue in may e.g. coincide with the number of occurrences of a pattern in the object (see also Appendix B.5).,
[TABLE]
We furthermore define the so-called projection operation via extending by linearity the definition of acting on basis vectors of ,
[TABLE]
These definitions induce a notion of correlators of observables (also referred to as (mixed) moments), defined for and as
[TABLE]
The precise relationship between the notions of CTMCs and SqPO-type rewriting rules as encoded in the corresponding SqPO-type rule algebra formalism is established in the form of the following theorem, where in particular the notion of observables is quite different in nature to the DPO-type analogon (compare Thm. 7.12 of [8]). This result is the first-of-its-kind universal definition of SqPO-type stochastic rewriting systems with “mass-action semantics” (where activities of productions are proportional to their number of admissible matches in a given system state).
Theorem 6** (SqPO-type stochastic mechanics framework).**
Let be a category satisfying Assumption 2. Let be a (finite) set of rule algebra elements, and a collection of non-zero parameters (called base rates). Then one may construct the Hamiltonian of the associated CTMC from this data according to
[TABLE]
Here, the notation for arbitrary objects denotes the observables (sometimes referred to as motif counting observables) for the resulting CTMC of SqPO-type, with
[TABLE]
We furthermore have the SqPO-type jump-closure property, whereby for all
[TABLE]
Proof.
See Appendix B.5. ∎
6 Application example: a dynamical random graph model
In order to illustrate our novel SqPO-type stochastic mechanics framework, let us consider a dynamical system evolving on the space of finite directed multigraphs.
Example 3**.**
Let be the finitary restriction of the category (see also Lemma 4), and denote by the strict initial object (the empty graph). We define a stochastic SqPO rewriting system based upon rules encoding vertex creation/deletion () and edge creation/deletion ():
[TABLE]
Together with a choice of base rates and an initial state , this data defines a stochastic rewriting system with Hamiltonian ,
[TABLE]
where and .
Despite the apparent simplicity of this model (which might be seen as a paradigmatic example of a random graph model), the explicit analysis via the stochastic mechanics framework will uncover a highly non-trivial interaction of the dynamics of the vertex- and of the edge-counting observables. Intuitively, since in SqPO-rewriting no conditions are posed upon vertices that are to be deleted, the model is expected to possess a vertex dynamics that is the one of a so-called birth-death process. If it were not for the vertex deletions, one would find a similar dynamics for the edge-counting observables (compare e.g. the DPO-type rewriting model considered in [8]). However, since deletion of vertices deletes all incident edges, the dynamics of the edge-counting observable is rendered considerably more complicated, and in particular much less evident to foresee by heuristic arguments.
In order to compute the dynamics of the vertex counting observable O_{\_}V:=\mathbb{O}_{\_}{\vbox{\hbox{\leavevmode\hbox{\includegraphics{tikz/NB-GCM2019-proceedings-final-figure38}}}}}, we follow the approach of exponential moment-generating functions put forward in [4, 7, 5] and define
[TABLE]
with a formal variable. encodes the moments of the observable , in that taking the -th derivative of w.r.t. followed by setting yields the -th moment of . Note that we must assume the finiteness of all statistical moments as standard in the probability theory literature in order for to be well-posed, a property that we will in the case at hand indeed derive explicitly. Referring the interested readers to [9] for further details, suffice it here to recall the following variant of the BCH formula (see e.g. [29], Prop. 3.35), for a formal variable and two composable linear operators,
[TABLE]
with the convention that . The operation is typically referred to as the commutator. We may then derive the formal evolution equation for :
[TABLE]
Since by definition , it remains to compute the adjoint action of on :
[TABLE]
Here, the result that has a very simple intuitive meaning: in applications of the linear rules , the number of vertices remains unchanged, whence the vanishing of the commutator. Combining these results with the SqPO-type jump-closure property (cf. Theorem 6), we finally arrive at the following formal evolution equation for :
[TABLE]
Supposing for simplicity an initial state (for some graph with vertices and edges), we find that . The resulting initial value problem may be solved in closed-form via semi-linear normal-ordering techniques known from the combinatorics literature [23, 10, 12, 7] (see also [9, 5]), and we obtain (for )
[TABLE]
In the limit , the moment-generating function becomes that of a Poisson-distribution (of parameter ), thus confirming the aforementioned intuition that the vertex-counting observable has the dynamical behavior of a so-called birth-death process (see e.g. [7]).
Let us consider next the dynamics of the edge-counting observable O_{\_}E:=\mathbb{O}_{\_}{\vbox{\hbox{\leavevmode\hbox{\includegraphics{tikz/NB-GCM2019-proceedings-final-figure39}}}}}, where for brevity we will only consider the evolution of the mean edge count. The calculation of the evolution equation for the expectation value of simplifies to the analogue of the so-called Ehrenfest equation,
[TABLE]
Recalling that , it remains to compute the commutator :
[TABLE]
This calculation is a representative example of various effects that may occur in rule-algebraic commutation relations: we find a zero commutator , indicating the fact that application of the vertex creation rule does not influence the edge count. The commutators encode that application of the edge creation/deletion rules leads to positive/negative contributions to the edge count. Finally, the contribution of the commutator is given by the representations of two rule algebra elements not originally present in the Hamiltonian , with the structure of the underlying linear rules indicated by the labels and on the vertices (as customary in the rewriting literature). It then remains to apply the jump-closure property (Theorem 6) together with the identity \mathbb{O}_{\_}{\vbox{\hbox{\leavevmode\hbox{\lower 2.86658pt\hbox{\includegraphics{tikz/NB-GCM2019-proceedings-final-figure46}}}}}\;\vbox{\hbox{\leavevmode\hbox{\lower 3.13329pt\hbox{\includegraphics{tikz/NB-GCM2019-proceedings-final-figure47}}}}}}=O_{\_}V(O_{\_}V-1) in order to obtain the evolution equation
[TABLE]
Together with an initial condition such as e.g. for some (finite) directed graph with vertices and edges, and computing the closed-form expression for the first contribution in (40) from our previous solution (37) (as followed by setting ), the initial value problem for the mean edge count evolution may be easily solved in closed form via the use of a computer algebra software such as Maple, Mathematica or Sage. It is also straightforward to verify that for an arbitrary initial state , the limit value of the mean edge count for reads
[TABLE]
Since the rates and are free parameters, the above result entails that in this model one may freely adjust the limit value of the average vertex count as encoded in (36) (whence ) as well as the limit value of the average edge count via suitable choices of the parameters . For illustration, we present some plots of the mean edge count evolution for the case and various choices of parameters in Figure 1.
7 Conclusion and Outlook
Extending our previous work on Double-Pushout (DPO) rewriting theories as presented in [4, 8, 5] to the important alternative setting of Sesqui-Pushout (SqPO) rewriting, we provide a number of original results in the form of concurrency and associativity theorems for SqPO rewriting theories on adhesive categories. These fundamental results in turn permit us to formulate so-called SqPO-type rule algebras, which play a central role in our novel universal stochastic mechanics framework. We strongly believe that these contributions will provide fruitful grounds for further developments both in theory and practice of rewriting beyond the specialists’ communities, especially in view of static analysis techniques [3].
Appendix A A collection of useful technical results on adhesive categories and final pullback complements
Notational convention: Here and as throughout this paper, while evidently category-theoretical constructions such as pushouts are only unique up to isomorphisms, we will typically nevertheless pick convenient representatives of the respective isomorphism classes to simplify our notations. As standard practice in the literature, we will thus e.g. fix the convention as in (42) to choose representatives appropriately to label the pushout along an isomorphism with “equality arrows” (rather than keeping object labels generic and decorating the relevant arrow with a “” symbol).
Lemma 2**.**
Let be a category.
- (i)
“Single-square” lemmata (see e.g. [9], 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, and* 3. (c)
* is a pullback for arbitrary morphisms if is a monomorphism.* 2. (ii)
special adhesivity corollaries* (cf. e.g. [24], Lemma 2.6): in any adhesive category,*
- (a)
pushouts along monomorphisms are also pullbacks, and 2. (b)
(uniqueness of pushout complements) given a monomorphism and a generic morphism , the respective pushout complement (if it exists) is unique up to isomorphism, and with (due to stability of monomorphisms under pushouts). 3. (iii)
“Double-square lemmata”**: given commutative diagrams of the shapes
[TABLE]
then in any category (cf. e.g. **[35]**):
- (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* ([24], 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* ([28], Lem. B.2): if is a pullback, a pushout, commutes and , then is a pullback.* 3. (e)
Horizontal FPC (de-)composition* (cf. [17], Lem. 2 and Lem. 3, compare [37], Prop. 36):666It is worthwhile emphasizing that in these FPC-related lemmata, 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 may 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 [37], Lem. 38): If , if is a pullback and if is an FPC (i.e. if is FPC of ), then and are FPCs.* 6. (h)
Vertical FPC-pushout decomposition777We invite the interested readers to compare the precise formulation of the vertical FPC-pushout decomposition result to its concrete applications in the setting of the proof of the concurrency theorem, for which it has been specifically developed.: 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.
Referring to the references above for the proofs of the (well-known) statements (where necessary by specializing the more general case of -adhesive categories to the case of adhesive categories via setting to the class of all monomorphisms), it remains to prove our novel vertical FPC-pushout decomposition result. To this end, we first invoke pullback-pushout decomposition (Lemma 2(3d)) in order to demonstrate that since is an FPC and thus also a pullback, and since is a pushout and since , is a pullback. By applying vertical FPC-pullback decomposition, we may conclude that is an FPC. 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 2(1c) (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 monomorphisms, invoking Theorem 7 below permits to prove that also . ∎
The last part of the preceding proof relied upon one of the quintessential properties of adhesive categories in view of associative rewriting theories:
Theorem 7** (Effective unions; [35], Thm. 5.1).**
In an adhesive category , given a commutative diagram such as in the middle of (1), if all morphisms except the morphism are monomorphisms, if the square marked is a pushout and if the exterior square is a pullback, then is also a monomorphism.
The following result provides several important facts on FPCs.
Lemma 3** (cf. [37], Fact 2, and [17], Lemma 2 and Proposition 2).**
Let be adhesive. For an arbitrary morphism , is an FPC of and vice versa. Moreover, every pushout square along monomorphisms is also an FPC square. FPCs are unique up to isomorphism and preserve monomorphisms. The latter property entails that if is the FPC of and if , then also and vice versa (while entails that by stability of monomorphisms under pullbacks in an adhesive category ).
For concreteness, we quote the following explicit construction of FPCs in the category of directed multigraphs:
Lemma 4** (FPCs for graphs; [17], Sec. 4.1 and Construction 5).**
Let denote the adhesive category of directed multigraphs, with
- •
: (multi-)graphs, i.e. tuples , with the set of vertices, the set of edges (with ), the source and the target maps
- •
: graph homomorphisms , specified in terms of pairs of morphisms such that and .
Let denote the class of all injective graph morphisms. Then for every composable pair of monomorphisms , the FPC exists and is constructed explicitly as888The quoted Construction 5 of [17] is slightly more general, in that the morphism may be permitted to not be a monomorphism; we will however have no application for such a generalization in our framework. , where denotes an inclusion morphism, and where the graph reads
[TABLE]
Appendix B Proofs
B.1 Proof of the SqPO concurrency theorem
Proof.
Throughout this proof, in each individual constructive step it may be verified that due to the stability of monomorphisms under pullbacks and pushouts, due to the various decomposition lemmata provided in the form of Lemma 2, and on occasion due to Theorem 7 on effective unions in adhesive categories, all morphisms induced in the “Synthesis” and “Analysis” steps are in fact monomorphisms. For better readability, we will not explicitly mention the individual reasoning steps on this point except for a few intricate sub-steps, since they may be recovered in a straightforward manner.
— Synthesis: Consider the setting presented in (46a). Here, we have obtained the candidate match {\color[rgb]{0,0,0.4}\mathbf{n}}=(I_{\_}2{\color[rgb]{0,0,0.4}\leftarrow M_{\_}{21}\rightarrow}O_{\_}1) via pulling back the cospan (I_{\_}2{\color[rgb]{0,0,0.4}\rightarrow}X_{\_}1{\color[rgb]{0,0,0.4}\leftarrow}O_{\_}1). Next, we construct {\color[rgb]{0,0,0.4}N_{\_}{21}} via taking the pushout of {\color[rgb]{0,0,0.4}\mathbf{n}}, which induces a unique arrow {\color[rgb]{0,0,0.4}N_{\_}{21}\rightarrow}X_{\_}1 that is according to Theorem 7 a monomorphism. The diagram in (46b) is obtained by taking the pullbacks of the spans \overline{K}_{\_}i\rightarrow X_{\_}1{\color[rgb]{0,0,0.4}\leftarrow N_{\_}{21}} (obtaining the objects , for ). By virtue of pushout-pullback decomposition (Lemma 2(3c)), the squares \Box(K_{\_}1^{\prime},\overline{K}_{\_}1,X_{\_}1,{\color[rgb]{0,0,0.4}N_{\_}{21}}) and \Box(K_{\_}1,K_{\_}1^{\prime},{\color[rgb]{0,0,0.4}N_{\_}{21}},O_{\_}1) are pushouts. Invoking vertical FPC-pullback decomposition (Lemma 2(3g)), the squares \Box(K_{\_}2^{\prime},{\color[rgb]{0,0,0.4}N_{\_}{21}},X_{\_}1,\overline{K}_{\_}2) and \Box(K_{\_}2,I_{\_}2,{\color[rgb]{0,0,0.4}N_{\_}{21}},K_{\_}2^{\prime}) are FPCs. Next, letting {\color[rgb]{0.9,0.45,0}O_{\_}{21}}:=\mathsf{PO}(O_{\_}2\leftarrow K_{\_}2\rightarrow K_{\_}2^{\prime}) and {\color[rgb]{0.9,0.45,0}I_{\_}{21}}:=\mathsf{PO}(O_{\_}1\leftarrow K_{\_}1\rightarrow K_{\_}1^{\prime}), we have via vertical FPC-pushout decomposition (Lemma 2(7)) that the resulting two squares on the very right (the ones involving {\color[rgb]{0.9,0.45,0}I_{\_}{21}}) are FPCs and that the arrow {\color[rgb]{0.9,0.45,0}I_{\_}{21}\rightarrow}X_{\_}0 is a monomorphism, while pushout-pushout decomposition (Lemma 2(3b)) entails that the two newly formed squares on the very left (the ones involving {\color[rgb]{0.9,0.45,0}O_{\_}{21}}) are pushouts.
The final step as depicted in (46c) consists in constructing {\color[rgb]{0.9,0.45,0}K_{\_}{21}}=\mathsf{PB}(K_{\_}2^{\prime}\rightarrow{\color[rgb]{0,0,0.4}N_{\_}{21}}\leftarrow K_{\_}1^{\prime}) and {\color[rgb]{0.9,0.45,0}\overline{K}_{\_}{21}}=\mathsf{PB}(\overline{K_{\_}2}\rightarrow X_{\_}1\leftarrow\overline{K_{\_}1}), which by universality of pullbacks induces a unique arrow {\color[rgb]{0.9,0.45,0}K_{\_}{21}\rightarrow\overline{K}_{\_}{21}}. By invoking pullback-pullback decomposition (Lemma 2(3a)), one may show that the squares \Box({\color[rgb]{0.9,0.45,0}K_{\_}{21}},{\color[rgb]{0.9,0.45,0}\overline{K}_{\_}{21}},\overline{K}_{\_}i,K_{\_}i^{\prime}) (for ) are pullbacks. Since the square \Box(K_{\_}1^{\prime},\overline{K}_{\_}1,X_{\_}1,{\color[rgb]{0,0,0.4}N_{\_}{21}}) is a pushout, via the van Kampen property (cf. Def. 1) the square \Box({\color[rgb]{0.9,0.45,0}K_{\_}{21}},{\color[rgb]{0.9,0.45,0}\overline{K}_{\_}{21}},\overline{K}_{\_}2,K_{\_}2^{\prime}) is a pushout. Since according to Lemma 3 pushouts are also FPCs, it follows via horizontal composition of FPCs (Lemma 2(6)) that the square \Box({\color[rgb]{0.9,0.45,0}K_{\_}{21}},{\color[rgb]{0.9,0.45,0}\overline{K}_{\_}{21}},X_{\_}1,{\color[rgb]{0,0,0.4}N_{\_}{21}}) is an FPC. Noting that the pushout square \Box(K_{\_}1^{\prime},\overline{K}_{\_}1,X_{\_}1,{\color[rgb]{0,0,0.4}N_{\_}{21}}) is an FPC as well, it follows via horizontal decomposition of FPCs (Lemma 2(6)) that \Box({\color[rgb]{0.9,0.45,0}K_{\_}{21}},{\color[rgb]{0.9,0.45,0}\overline{K}_{\_}{21}},\overline{K}_{\_}1,K_{\_}1^{\prime}) is an FPC. Thus the claim follows by invoking pushout composition (Lemma 2(3b)) and horizontal FPC composition (Lemma 2(6)) in order to obtain the pushout square \Box({\color[rgb]{0,0,0.4}K_{\_}{21}},{\color[rgb]{0,0,0.4}\overline{K}_{\_}{21}},X_{\_}2,{\color[rgb]{0,0,0.4}O_{\_}{21}}) and the FPC square \Box({\color[rgb]{0,0,0.4}K_{\_}{21}},{\color[rgb]{0,0,0.4}\overline{K}_{\_}{21}},X_{\_}0,{\color[rgb]{0,0,0.4}I_{\_}{21}}).
— Analysis: Given the setting as depicted in (47a) of Figure 3, where the top row has the structure of an SqPO-composition (compare (4)), where the square \Box({\color[rgb]{0.9,0.45,0}K_{\_}{21}},K_{\_}1^{\prime},{\color[rgb]{0,0,0.4}N_{\_}{21}},K_{\_}2^{\prime}) is a pullback, the left “curvy” bottom square a pushout and the right “curvy” bottom square an FPC, we may obtain the configuration of (47c) as follows: construct999Note that it is precisely in this step and the following step that we require the existence of FPCs for arbitrary pairs of monomorphisms as per Assumption 1. via taking the final pullback complement of (which implies the existence of an arrow {\color[rgb]{0.9,0.45,0}\overline{K}_{\_}{21}}\rightarrow\overline{K}_{\_}1 via the FPC property). Note in particular that according to Lemma 3, both arrows constructed via forming the aforementioned FPC are monomorphisms, and thus by stability of monomorphisms in an adhesive category (compare Definition 1 and Lemma 2(1c)), the arrow {\color[rgb]{0.9,0.45,0}\overline{K}_{\_}{21}}\rightarrow\overline{K}_{\_}1 is a monomorphism as well. Next, take the pushout X_{\_}1=\mathsf{PO}(\overline{K}_{\_}1\leftarrow K_{\_}1^{\prime}\rightarrow{\color[rgb]{0,0,0.4}N_{\_}{21}}), followed by constructing as the final pullback complement of K_{\_}2^{\prime}\rightarrow{\color[rgb]{0,0,0.4}N_{\_}{21}}\rightarrow X_{\_}1 (which implies due to the FPC property of the resulting square \Box(K_{\_}2^{\prime},\overline{K}_{\_}2,X_{\_}1,{\color[rgb]{0,0,0.4}N_{\_}{21}}) the existence of an arrow {\color[rgb]{0.9,0.45,0}\overline{K}_{\_}{21}}\rightarrow\overline{K}_{\_}2). Invoking pullback-pullback decomposition (Lemma 2(3a)) twice, followed by the van Kampen property (Def. 1), we may conclude that the square \Box({\color[rgb]{0.9,0.45,0}K_{\_}{21}},{\color[rgb]{0.9,0.45,0}\overline{K}_{\_}{21}},\overline{K}_{\_}2,K_{\_}2^{\prime}) is a pushout. Thus invoking pushout-pushout decomposition (Lemma 2(3b)), we find that also is a pushout. We finally arrive at the configuration in (47d) via composition of pushout and FPC squares, respectively, thus concluding the proof. ∎
B.2 Proof of the SqPO associativity theorem
Our proof strategy will be closely related to the one presented in [8] (with full technical details provided in [9]) for the analogous associativity theorem in the DPO-rewriting case. However, the SqPO-type case poses considerable additional challenges, since this rewriting semantics yields diagrams of a rather heterogeneous nature (including pullbacks, pushouts, pushout complements and FPCs) as compared to the DPO case, and in addition unlike DPO-type rule compositions, SqPO-type compositions are not reversible in general, which necessitates an independent proof of both directions of the bijective correspondence.
Proof.
We first prove the claim in the “” direction, i.e. starting from the set of data
[TABLE]
we have to demonstrate that one may uniquely (up to isomorphisms) construct from this information a pair of admissible matches
[TABLE]
and such that the property described in (6) holds. We begin by forming the SqPO-composite rule , which results in the diagram
[TABLE]
by virtue of invoking SqPO-composition twice. For the remainder of the proof, it is very important to precisely determine the nature of each of the squares in this diagram:
- •
To clarify the structure of the rightmost four squares at the bottom, consider the setting presented in (47a): since in the definition of the SqPO-composition as presented in (4) the nature of the squares to the right is that of pushout complement and pushout, respectively, it may be verified that applying the analysis procedure to the diagram in (47a) with thus the “curvy” front and right bottom faces both pushouts, one eventually arrives (by virtue of pushout-pushout and pushout-pullback decomposition) at the setting depicted in (47c) with all squares in the bottom row being pushouts. Thus the rightmost four squares at the bottom of (50) are all pushouts.
- •
By virtue of the definition of SqPO-composition, all vertical squares in the back of (47c) are pushouts, except for the square \Box(K_{\_}2,K_{\_}2^{\prime},{\color[rgb]{0,0,0.4}N_{\_}{21}},I_{\_}2), which is an FPC. Analogously, the bottom leftmost three squares are (in order from left to right) a pushout, an FPC and a pushout.
Constructing the pullback {\color[rgb]{0,0,0.4}M_{\_}{32}}=\mathsf{PB}({\color[rgb]{0,0,0.4}M_{\_}{3(21)}\rightarrow}O_{\_}{21}\leftarrow O_{\_}2) (which by composition of pullbacks also leads to an arrow {\color[rgb]{0,0,0.4}M_{\_}{32}\rightarrow}I_{\_}3) and forming the three additional vertical squares on the far left in the evident fashion in the diagram below
[TABLE]
allows us to construct {\color[rgb]{0,0,0.4}N_{\_}{32}}=\mathsf{PO}(I_{\_}3{\color[rgb]{0,0,0.4}\leftarrow M_{\_}{32}\rightarrow}O_{\_}2), which in turn via universality of pushouts uniquely induces an arrow {\color[rgb]{0,0,0.4}N_{\_}{32}\rightarrow N_{\_}{3(21)}}:
[TABLE]
Here, the rightmost three squares on the top are formed in the evident fashion (and they are pushouts by virtue of Lemma 2(1a)), while the other arrows of the above diagram are constructed as follows:
[TABLE]
Invoking pushout-pullback, pushout-pushout and vertical FPC-pullback decompositions, it may be verified that (describing positions of front and top square pairs by the position of the respective front square, from left to right)
- •
the leftmost front and top squares are pushouts,
- •
the second from the left front and top squares are FPCs,
- •
the third from the left front and top squares are pushouts,
- •
in the next adjacent pair, the front square is an FPC and the top square a pushout,
- •
the second from the right front and top squares are pushouts, and
- •
the rightmost front and top squares are pushouts.
Defining the pullback object {\color[rgb]{0,0,0.4}M_{\_}{(32)1}}=\mathsf{PB}(I_{\_}{32}{\color[rgb]{0,0,0.4}\rightarrow N_{\_}{3(21)}\leftarrow}O_{\_}1), thus inducing an arrow {\color[rgb]{0,0,0.4}M_{\_}{21}\rightarrow M_{\_}{3(21)}},
[TABLE]
it remains to verify that the square \Box({\color[rgb]{0,0,0.4}M_{\_}{3(21)}},I_{\_}{32},{\color[rgb]{0,0,0.4}N_{\_}{3(21)}},O_{\_}1) is not only a pullback, but also a pushout square. This part of the proof requires a somewhat intricate diagram chase; since the required arguments are identical101010More precisely, the only difference in the structure of the relevant sub-diagram compared to the DPO case resides in the two FPC squares in the front and back in fourth position from the left (which happen to be pushout squares in the corresponding DPO-type proof), but the structure of this part of the diagram is not explicitly used in the proof in the DPO variant of the theorem, whence the claim follows. to the “” part of proof of DPO-type associativity as presented in [9], we omit this part of the proof here in the interest of brevity.
It thus remains to prove the claim in the “” direction, i.e. starting from the set of data
[TABLE]
we need to demonstrate that one may uniquely (up to isomorphisms) construct from this information a pair of admissible matches
[TABLE]
and such that the property described in (6) holds. We begin by forming the SqPO-composite rule , which results in the diagram
[TABLE]
by virtue of invoking SqPO-composition twice. A careful inspection of the definition of the SqPO-composition and of the analysis part of the SqPO concurrency theorem permit to verify that the nature of all squares thus constructed coincides precisely with the nature of the corresponding squares in the “” part of the proof.
Constructing the pullback {\color[rgb]{0,0,0.4}M_{\_}{21}}=\mathsf{PB}(I_{\_}2\rightarrow I_{\_}{32}\leftarrow\color[rgb]{0,0,0.4}M_{\_}{(32)1}) (which by composition of pullbacks also leads to an arrow {\color[rgb]{0,0,0.4}M_{\_}{21}\rightarrow}O_{\_}1) and forming the three additional vertical squares on the far right in the evident fashion in the diagram below
[TABLE]
allows us to construct {\color[rgb]{0,0,0.4}N_{\_}{21}}=\mathsf{PO}(I_{\_}2{\color[rgb]{0,0,0.4}\leftarrow M_{\_}{21}\rightarrow}O_{\_}1), which in turn via the universal property of pushouts induces an arrow {\color[rgb]{0,0,0.4}N_{\_}{21}\rightarrow N_{\_}{(32)1}}:
[TABLE]
The remaining new squares of the above diagram are constructed as follows:
[TABLE]
Moreover, by virtue of vertical FPC composition, the square \Box(K_{\_}3,\overline{K}_{\_}3,{\color[rgb]{0,0,0.4}N_{\_}{3(21)}},I_{\_}3) is an FPC, while via pushout composition the square is a pushout.
Again, the nature of all squares constructed thus far coincides precisely with the structure as presented in the “” part of the proof, with one notable exception: by virtue of vertical FPC-pullback decomposition, we may only conclude that the square \Box(K_{\_}2^{\prime},\overline{K}_{\_}2,{\color[rgb]{0,0,0.4}N_{\_}{(32)1}},{\color[rgb]{0,0,0.4}N_{\_}{21}}) is an FPC (but at this point we do not know whether it is also a pushout as in the analogous part of the diagram in the “” part of the proof). However, an auxiliary calculation demonstrates that this square is in fact a pushout in disguise — consider the following “splitting” of the relevant sub-part of the diagram as shown below:
[TABLE]
The precise steps are as follows: the front left square in the diagram above left is an FPC; thus if one takes the pushout {\color[rgb]{0,0,0.4}N_{\_}{(32)1}^{\prime}}=\mathsf{PO}(\overline{K}_{\_}2\leftarrow K_{\_}2^{\prime}\rightarrow{\color[rgb]{0,0,0.4}N_{\_}{21}}) as well as in the bottom back the pushout along the isomorphism of as displayed (yielding the arrows in the middle), followed by taking the pullback O_{\_}1^{\prime}=\mathsf{PB}({\color[rgb]{0,0,0.4}N_{\_}{(32)1}^{\prime}},{\color[rgb]{0,0,0.4}N_{\_}{(32)1}},O_{\_}1) (which entails that the arrow {\color[rgb]{0,0,0.4}M_{\_}{3(21)}}\rightarrow O_{\_}1^{\prime} exists), it is straightforward to verify that . Invoking the van Kampen property (recalling that by definition the right square on the bottom is a pushout), we find that \Box({\color[rgb]{0,0,0.4}M_{\_}{3(21)}},O_{\_}1^{\prime},{\color[rgb]{0,0,0.4}N_{\_}{(32)1}^{\prime}},I_{\_}{32}) is a pushout. Thus by pushout-pushout decomposition, the square \Box(O_{\_}1^{\prime},O_{\_}1,{\color[rgb]{0,0,0.4}N_{\_}{(32)1}},{\color[rgb]{0,0,0.4}N_{\_}{(32)1}^{\prime}}) is a pushout, whence {\color[rgb]{0,0,0.4}N_{\_}{(32)1}^{\prime}}\cong{\color[rgb]{0,0,0.4}N_{\_}{(32)1}}. This in summary entails111111Coincidentally, at this point we are back into full structural analogy to the “” part of the proof, a necessary prerequisite for completing this part of the proof as it will turn out. that the square \Box(K_{\_}2^{\prime},\overline{K}_{\_}2,{\color[rgb]{0,0,0.4}N_{\_}{(32)1}},{\color[rgb]{0,0,0.4}N_{\_}{21}}) is not only an FPC, but in fact also a pushout.
Back to the main proof, defining the pullback object
[TABLE]
thus inducing an arrow {\color[rgb]{0,0,0.4}M_{\_}{32}\rightarrow M_{\_}{3(21)}},
[TABLE]
it remains to verify that the square \Box({\color[rgb]{0,0,0.4}M_{\_}{3(21)}},O_{\_}{21},{\color[rgb]{0,0,0.4}N_{\_}{3(21)}},I_{\_}3) is not only a pullback, but also a pushout square. Let us construct the auxiliary diagram as depicted in Figure LABEL:fig:SqPOrevAuxDiag, with objects obtained via taking suitable pullbacks as indicated. The four cubes that are drawn separately are the top, back, bottom and front cubes induced via the newly constructed arrows, and are oriented such that one may easily apply the van Kampen property in the next step of the proof (which in most cases requires a suitable 3d-rotation).
Invoking pullback-pullback decomposition and the van Kampen property repeatedly, it may be verified that in the relevant sub-diagram as presented below
[TABLE]
we find the following structure of the squares:
- •
All squares on the top are pushouts, except the second one from the right (which is a pullback).
- •
The second and third square from the left in the back of the diagram are pushouts, the other two back squares are pullbacks, with the same structure for the front squares.
- •
Counting from left to right, the second and fourth square on the bottom are pushouts, the other two are pullbacks.
In particular, as indicated this entails that . We proceed by performing the following “splitting” of the diagram:
[TABLE]
Start the “splitting” via taking the pushouts {\color[rgb]{0,0,0.4}N_{\_}{32}^{\prime}}=\mathsf{PO}(I_{\_}3\leftarrow I_{\_}3\rightarrow{\color[rgb]{0,0,0.4}N_{\_}{32}}) (which entails that {\color[rgb]{0,0,0.4}N_{\_}{32}^{\prime}}\cong{\color[rgb]{0,0,0.4}N_{\_}{32}}) and O_{\_}2^{\prime}=\mathsf{PO}({\color[rgb]{0,0,0.4}M_{\_}{3(21)}}\leftarrow{\color[rgb]{0,0,0.4}M_{\_}{32}}\rightarrow O_{\_}2). By pullback-pullback decomposition followed by pushout-pullback decomposition, we may conclude that the resulting square \Box(O_{\_}2^{\prime},{\color[rgb]{0,0,0.4}N_{\_}{32}^{\prime}},I_{\_}3,{\color[rgb]{0,0,0.4}M_{\_}{3(21)}}) is a pushout. Note also that all vertical squares in the bottom left part of the diagram thus constructed are pullbacks (by virtue of suitable pullback decompositions).
Next, construct the pullbacks \overline{K}_{\_}2^{\prime}=\mathsf{PB}({\color[rgb]{0,0,0.4}N_{\_}{32}^{\prime}\rightarrow N_{\_}{3(21)}}\leftarrow\overline{K}_{\_}2) and . By pushout-pullback decomposition, in the diagram on the right the top and bottom front squares and back squares in the second column are pushouts, while the square is a pullback. Performing the precise same steps in the next column, i.e. via taking the pullbacks and , we obtain via pushout-pullback decomposition that the top and bottom front and top and bottom back squares in the third column are pushouts, while the square is a pullback. But since and since isomorphisms are stable under pullback, we conclude that , and thus that the square is in fact a pushout.
By pushout composition, we may thus conclude that is a pushout, whence the square \Box(O_{\_}2^{\prime},O_{\_}{21},{\color[rgb]{0,0,0.4}N_{\_}{3(21)}},{\color[rgb]{0,0,0.4}N_{\_}{32}^{\prime}}) is a pushout, which finally allows us to verify that \Box({\color[rgb]{0,0,0.4}M_{\_}{3(21)}},O_{\_}{21},{\color[rgb]{0,0,0.4}N_{\_}{3(21)}},I_{\_}3) is a pushout. This concludes the proof of the SqPO-type associativity theorem. ∎
B.3 Proof of the theorem on SqPO rule algebra properties
Proof.
Associativity of follows from the associativity of the operation proved in Theorem 3. The claim that is the unit element of the rule algebra follows directly from the definition of the rule algebra product for and for . More concretely, we present below the category-theoretic composition calculation that underlies the equation :
[TABLE]
Here, it is important to note that the pushout complement used to construct the square marked always exists (see Lemma 2(1a)), whence the claim follows. ∎
B.4 Proof of the SqPO canonical representation theorem
Proof.
In order for to qualify as an algebra homomorphism (of unital associative algebras and ), we must have (with , )
[TABLE]
Due to linearity, it suffices to prove the two properties on basis elements of (for ) and on basis elements of . Property follows directly from the definition,
[TABLE]
Property follows from Theorem 2 (the SqPO-type concurrency theorem): for all basis elements (with ) and for all ,
[TABLE]
∎
B.5 Proof of the SqPO stochastic mechanics framework theorem
Proof.
By definition, the SqPO-type canonical representation of a generic rule algebra element is a row-finite linear operator, since by virtue of the finitarity of objects according to Assumption 2, for every object the set of SqPO-admissible matches of the associated linear rule is finite. We may thus verify that the linear operator possesses all the required properties of a so-called -matrix (or infinitesimal generator) of a CTMC [42, 2], i.e. its non-diagonal entries are non-negative, its diagonal entries are finite, and furthermore the row sums of are zero (whence constitutes a conservative and stable -matrix; compare (21) of Definition 9). It is crucial to note that while originally as a linear combination of representations of rule algebra elements is only defined to act on finite linear combinations of basis vectors of , an important mathematical result from the theory of CTMCs entails that if a row-finite linear operator such as is a stable and conservative -matrix, it extends to a linear operator on infinitely supported distributions (here over basis vectors of ) with finite real coefficients (see e.g. [2], Chapters 1 and 2). Moreover, the property follows directly from the defining equations (21) of Definition 9.
Let us prove next the claim on the precise structure of observables. Recall that according to Definition 10, an observable must be a linear operator in that acts diagonally on basis states (for ), whence that satisfies for all
[TABLE]
Comparing this equation to the definition of the SqPO-type canonical representation (Definition 8) of a generic rule algebra basis element (for ),
[TABLE]
we find that in order for to be diagonal we must have
[TABLE]
But by definition of SqPO-type derivations of objects along admissible matches (Definition 4), the only linear rules that have this special property are precisely the rules of the form
[TABLE]
In particular, defining , we find that the eigenvalue coincides with the cardinality of the set of SqPO-admissible matches,
[TABLE]
This proves that the operators form a basis of diagonal operators on (and thus on ) that can arise as linear combinations of representations of rule algebra elements.
To prove the jump-closure property, note that it follows from Definition 4 that for an arbitrary linear rule , a generic object and a monomorphism , is according to Definition 4 both a match of the rule as well as of the rule . Evidently, the application of the rule to along the match produces an object that is in general different from the object produced by application of the rule to along the match . But by definition of the projection operator (Definition 10),
[TABLE]
we find that
[TABLE]
whence we may prove the claim of the SqPO-type jump-closure property via verifying it on arbitrary basis elements (with notations as above):
[TABLE]
Since was chosen arbitrarily, we thus have indeed that
[TABLE]
This concludes the proof that our definition of continuous-time Markov chains based upon SqPO-type rewriting rules is well-posed and yields all the requisite properties. ∎
The reference list from the paper itself. Each links out to its DOI / PubMed record.
- 1[1]
- 2[2] W.J. Anderson (1991): Continuous-Time Markov Chains . Springer New York, 10.1007/978-1-4612-3038-0 . · doi ↗
- 3[3] N. Behr (2019): Tracelets and Tracelet Analysis Of Compositional Rewriting Systems . ar Xiv preprint ar Xiv:1904.12829 .
- 4[4] N. Behr, V. Danos & I. Garnier (2016): Stochastic mechanics of graph rewriting . In: Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science - LICS ’16 , ACM Press, 10.1145/2933575.2934537 . · doi ↗
- 5[5] N. Behr, V. Danos & I. Garnier (2019): Combinatorial Conversion and Moment Bisimulation for Stochastic Rewriting Systems . ar Xiv preprint 1904.07313 .
- 6[6] N. Behr, V. Danos, I. Garnier & T. Heindel (2016): The algebras of graph rewriting . ar Xiv:1612.06240 .
- 7[7] N. Behr, G.H.E. Duchamp & K.A. Penson (2017): Combinatorics of Chemical Reaction Systems . ar Xiv:1712.06575 .
- 8[8] N. Behr & P. Sobocinski (2018): Rule Algebras for Adhesive Categories . In Dan Ghica & Achim Jung, editors: 27th EACSL Annual Conference on Computer Science Logic (CSL 2018) , Leibniz International Proceedings in Informatics (LIP Ics) 119, Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, pp. 11:1–11:21, 10.4230/LIP Ics.CSL.2018.11 . · doi ↗