Single Pushout Rewriting in Comprehensive Systems
 61 Downloads
Abstract
The elegance of the singlepushout (SPO) approach to graph transformations arises from substituting total morphisms by partial ones in the underlying category. Thus, SPO’s applicability depends on the durability of pushouts after this transition. There is a wide range of work on the question when pushouts exist in categories with partial morphisms starting with the pioneering work of Löwe and Kennaway and ending with an essential characterisation in terms of an exactness property (for the interplay between pullbacks and pushouts) and an adjointness condition (w.r.t. inverse image functions) by Hayman and Heindel.
Triple graphs and graph diagrams are frameworks to synchronize two or more updatable data sources by means of internal mappings, which identify common substructures. Comprehensive systems generalise these frameworks, treating the network of data sources and their structural interrelations as a homogeneous comprehensive artifact, in which partial maps identify commonalities. Although this inherent partiality produces amplified complexity, Heindel’s characterisation still yields cocompleteness of the category of comprehensive systems equipped with closed partial morphisms and thus enables computing by SPO graph transformation.
Keywords
Single Pushout Rewriting Partial morphism Category theory Hereditary pushout Upper adjoint Comprehensive system1 Introduction and Motivation
We want to dedicate this paper to Michael Löwe, the founder of the singlepushout approach [12] and simultaneously a pioneer in the investigation of categories of partial algebras with partial morphisms between them [13].
Comprehensive Systems have been introduced in [21] (see also [22]) as a means for global consistency management, representing a collection of interrelated systems. To provide an intuition of a comprehensive system (Definition 3 in Sect. 3), take a look at Fig. 1. There are three conceptual models \(A_1, A_2, A_3\), which depict persons Open image in new window with certain features: In \(A_1\) a phone number Open image in new window is assigned to the person, in \(A_2\) and \(A_3\) the person possesses a home address Open image in new window , and in \(A_3\) persons additionally may have a business address Open image in new window . You may think of \(A_{1/2/3}\) representing (excerpts of) the contents of three databases possibly in three distributed ITsystems, the first stores records of persons and phone numbers while the second and third store records of persons and addresses.
 IMC
Every person with a business address must either provide a phone number or a home address or both.
Note that \(A_{1/2/3}\) formally represent directed graphs. But the junctions of each commonality ( Open image in new window ) – called commonality representatives – form another graph \(A_0\) in Fig. 1. Elements of \(A_0\) witness common elements among \(A_{1/2/3}\) and these commonalities must obviously respect nodeedgeincidences (see the person to home address assignment), such that their respective outgoing grey lines are in fact graph morphisms \(a_i:A_0\rightarrow A_i\), \(i\in I = \{1,2,3\}\).
For \({}{I}{}=2\) the underlying starshape of comprehensive systems (finite collections of arrows \((a_i)_{i\in \{1,\ldots , n\}}\) with common source) reduces to the span shape \(\bullet \leftarrow \bullet \rightarrow \bullet \), which is the underlying setting for triple graphs [18], the common source in the middle specifying the commonality graph. An extension of triple graphs are graph diagrams [23], a framework for multiary model synchronisation. Since multiary commonality relations such as the ternary tentacles of identical person records in Fig. 1 can not be encoded with several binary relations [19], one must distinguish relations of different arity in the underlying shape for graph diagrams: E.g. in Fig. 1, a shape with two nodes is required: One node specifies the existence of a graph containing binary home address commonalities and one node is used for ternary commonalities of person records. In larger system landscapes (\(n>3\)), there may be many more commonality relations of arbitrary arity \(k \le n\), which would cause a considerable amount of heterogeneity of commonality nodes in the underlying shape for graph diagrams. Moreover, this schema and hence the basic setting for implementations must be altered, whenever new commonality relations are added.
We showed in [21, 22] that comprehensive systems are a homogeneous generalisation of graph diagrams. They are homogeneous, because we need only one node to cope with commonality relations of arbitrary arity (the center of the starshape specifying commonality graph \(A_0\)) and must not alter the base setting, if new relations are added. It is a generalisation, because we can implement each graph diagram as a comprehensive system, i.e. we can jointly collect different commonalities into one graph \(A_0\).
We expect the reader to have basic knowledge in category theory. For categorical artefacts, we employ the following notations: Categories like \(\mathbb {C}\) will be denoted in a doublestruck font. When distinguishing between members of \(\mathbb {C}\), we write \({}{\mathbb {C}}{}\) (or just \(\mathbb {C}\)) for its objects and \(Arr(\mathbb {C})\) for its morphisms. Moreover, there are identities \({id_A}: {A} \rightarrow {A}\) and composition, e.g. \(g\circ f\), for \({f}: {A} \rightarrow {B}\) and \({g}: {B} \rightarrow {C}\). \(\mathbb {S}\mathbb {E}\mathbb {T}\) is the category of sets and total mappings and we will use the letter \(\mathbb {G}\) for categories that are based on a signature with unary operation symbols only, see Sect. 3 for more details. Monomorphisms (\(\rightarrowtail \)), epimorphisms (\(\twoheadrightarrow \)) and – if applicable – inclusions (\(\hookrightarrow \)) have special notations. We furthermore expect the reader to be familiar with basic universal constructions like pullbacks, coproducts, and pushouts. When describing a pullback as in Fig. 2, we either say that the span \((g',f')\) is the pullback of cospan (f, g) or we call \(g'\) the pullback of g along f. Moreover, the pullback object D in this construction is highlighted with a small adjacent right angle.
2 SPO Rewriting
2.1 GraphLike Structures
A category \(\mathbb {G}\) is called based on a signature with unary operation symbols only, if it is isomorphic to a category of total algebras w.r.t. a signature, which only contains sorts and unary operation symbols. The simplest example in our context – and the rationale behind using letter \(\mathbb {G}\) – are directed graphs, which are based on a signature with sorts E and V and two unary operation symbols \(s,t:E\rightarrow V\). We do not endorse directed graphs in particular and could likewise choose \(\mathbb {G}\) to be given by EGraphs [4] or bipartite artefacts like conditioneventnets. It is wellknown that all these categories are topoi and thus possess all limits (e.g. pullbacks) and colimits (coproducts, pushouts) [6].
Objects of such categories \(\mathbb {G}\) are sometimes called “graphlike structures”, as e.g. in [14], and thus we will simply call \(\mathbb {G}\)objects and morphisms “graphs” and “graph morphisms” bearing in mind the above mentioned more general setting.
Remark: \(\mathbb {G}\) will serve as the base category (or base structure) for assembling comprehensive systems, cf. Fig. 1. Actually, we could have traded \(\mathbb {G}\) for more general (weak) adhesive (HLR) categories w.r.t. an admissible subclass \(\mathcal {M}\) of all monomorphisms.^{1} Adhesive HLR categories have mainly been introduced to model attributes, which poses some challenges regarding adhesiveness, in turn requiring to work with special subclasses of morphisms, which are isomorphic on the “data part”. However, we restrict ourselves to graphlike structures because we are not focusing on attributes here and we want to stay in the tradition of Michael Löwe, who originally investigated graphlike structures only. Since graphlike structures are sufficiently concrete, we can actually refer to an element \(x\in A\) for some \(A\in \mathbb {G}\), i.e. an element of some carrier set of graph A. Likewise, “\(\forall x\in A\)” means “for all x of any sort s in the carrier set of A”.
2.2 Partial Map Categories
Consider an arbitrary category \(\mathbb {C}\) with pullbacks. Michael had the courage to leave the comfortable world of total \(\mathbb {C}\)morphisms and utilised partial morphisms [17] for the SPO approach. While other researchers adhered to total morphisms, he forcefully followed through with partiality and proved that it is worthwhile [12]. He used the following definitions: A \(\mathbb {C}\)span Open image in new window, is equivalent to a second span Open image in new window, if and only if there is an isomorphism \(i:dom(f)\rightarrow dom(f')\) such that \(m'\circ i = m\) and \(f'\circ i = f\). A partial morphism is an equivalence class w.r.t. this relation, denoted by Open image in new window, i.e. the pair (m, f) is a representative of its equivalence class. \(\langle m,f\rangle \) is called total, if m is an isomorphism, and we use the usual arrow tip in this case: \(\langle m,f\rangle :X\rightarrow Y\).
It is then easy to see that the objects of \(\mathbb {C}\) together with partial morphisms constitute a new category \(\texttt {Par}(\mathbb {C})\): An identity is the equivalence class of the identity span and composition of Open image in new window and \({\langle m_2,f_2\rangle }: {G_2} \rightharpoonup {G_3}\) is given by constructing the pullback span \((m_2',f_1')\) of cospan \((f_1,m_2)\) yielding the composed partial morphism \(\langle m_1\circ m_2',f_2\circ f_1'\rangle \). This is in fact independent of the choice of pullbacks and independent of the choice of representatives.
Definition 1 (Hereditary Pushout)
[8] Any pushout in \(\mathbb {C}\) is called hereditary, if its \(\varGamma \)image is a pushout in \(\texttt {Par}(\mathbb {C})\). If all pushouts exist in \(\mathbb {C}\) and they are all hereditary, we say that \(\mathbb {C}\) is a hereditary pushout category.
The following result can be found in [10]:
Proposition 1
If the \(\varGamma \)image of a \(\mathbb {C}\)span has a pushout in \(\texttt {Par}(\mathbb {C})\), then this cocone consists of two total morphisms, which are the \(\varGamma \)image of the pushout of this span in \(\mathbb {C}\). \(\square \)
For \(\mathbb {C}:=\mathbb {G}\), we can refer to elements inside objects of \(\mathbb {G}\), such that we will work with representatives Open image in new window of a partial morphism, in which the left leg m is chosen as the effective inclusion of dom(f), the domain of definition of the partial morphism, into G. Since the name m is of minor importance, we may as well write Open image in new window. In this setting, we will call f “total”, if the inclusion m is the identity. For the remainder of this paper we will use \(\mathbb {G}\)inclusions when there is a choice for monomorphisms (replacing \(\rightarrowtail \) with \(\hookrightarrow \)).
The following result was stated in [7] but fully worked out already in [12]:
Proposition 2
\(\mathbb {G}\) is a hereditary pushout category. \(\square \)
Finally, hereditariness can equivalently be characterised as follows:
Proposition 3
(Equivalent Characterisation of Hereditariness). [9] A pushout like the top face in the cube in Fig. 3 is hereditary, if and only if in any commutative cube as in Fig. 3 with rear faces being pullbacks and vertical front left and back right arrows (c and b in Fig. 3) being monomorphisms, the following equivalence holds: The bottom face is a pushout if and only if (1) the two front faces are pullbacks and (2) the vertical front right arrow (the dashed arrow in Fig. 3) is a monomorphism. \(\square \)
2.3 Rewriting Rule and Derivation
While the doublepushout approach (DPO) [4] requires the construction of a pushout complement and another pushout in the underlying category \(\mathbb {C}\), the introduction of partial morphisms enables graph transformations to be expressed by a single pushout in \(\texttt {Par}(\mathbb {C})\). This elegant alternative to DPO was initiated by Raoult [16] and then fully worked out in Michael’s PhD Thesis [12].
Definition 2 (Rule, Match, Derivation, ConflictFreeness)
An SPO rule is a morphism Open image in new window of \(\texttt {Par}(\mathbb {C})\). A match for \(\rho \) at (host) \(G\in \mathbb {C}\) is a total morphism \({\mu }: {L} \rightarrow {G}\). A pushout of \(\rho \) and \(\mu \) in \(\texttt {Par}(\mathbb {C})\) generates the (SPO) derivation \(G\,{\mathop {\Rightarrow }\limits ^{\rho ,\mu }}\, H\) with trace \(\rho '\) and comatch \(\mu '\), see Fig. 4. The match \(\mu \) is called conflictfree, if \(\mu '\) is a total morphism.
Computing by SPO graph transformation requires the existence of pushouts in \(\texttt {Par}(\mathbb {C})\) and it requires conflict freeness of matches, cf. Definition 2, if one wants to avoid partial matches. We can prove existence of pushouts for \(\texttt {Par}(\mathbb {CS})\) in Sect. 4, but  in contrast to a simple criterion for conflict freeness in terms of injectivity of \(\mu \) on deletepreserve pairs [12]  we have to leave the question of a criterion for conflict freeness in \(\texttt {Par}(\mathbb {CS})\) for future research.
3 Comprehensive Systems
For now and the rest of the paper, we fix a sufficiently large number \(n\in \mathbb {N}\).^{2}
3.1 Definitions and Background
Definition 3 (Comprehensive System)
\((A_j)_{1\le j \le n}\) the Components and
\(A_0\) the Commonality Representatives
In order to make reading easier, we always use letter i, if indexing comprises graphs \(A_0, A_1, \ldots , A_n\) and we use letter j, if indexing is only over the components \(A_1, \ldots , A_n\). Moreover, we denote comprehensive systems with bold face letters.
Comprehensive systems admit an allembracing view on a system of possibly heterogeneously typed components, in which all necessary informational overlaps are coded, cf. Fig. 1. They have been treated on the level of graphs in [20] and – on a more abstract level – in [3].
Definition 4 (Morphism of Comprehensive Systems)
Whenever we mention morphisms \(\mathbf {{f}: {A} \rightarrow {A'}}\) between comprehensive systems, we implicitly assume the components of \(\mathbf {A}\) and \(\mathbf {A'}\) be denoted as in Definition 3 and we assume the constituents of \(\mathbf {f}\) be denoted as in Definition 4.
There is the obvious identical morphism \(\mathbf {id_{A}}\) for each comprehensive system \(\mathbf {A}\) and composition can be defined componentwise. Hence we obtain
Proposition 4
(Category \(\mathbb {C}\mathbb {S}\) and Component Functors). Let \(\mathbb {G}\) be a category as described above.

Comprehensive Systems and morphisms between them constitute a category, denoted \(\mathbb {C}\mathbb {S}_{\mathbb {G}}\) or often just \(\mathbb {C}\mathbb {S}\), if the base category is clear from the context.

For each \(i\in \{0,\ldots ,n\}\) there is the component functor \(\mathcal {C}_i:\mathbb {C}\mathbb {S}\rightarrow \mathbb {G}\) defined by \(\mathcal {C}_i(\mathbf {{f}: {A} \rightarrow {A'}}) = {A_i} \xrightarrow {f_i} {A_i'}\) for any \(\mathbf {f}\) defined as in Definition 4. \(\square \)
It is important to note that we claim (1) to hold in \(\texttt {Par}(\mathbb {G})\) and not in \(\mathbb {G}\)! Let’s investigate the consequences: Recall that the definition of composition of partial morphisms involves pullbacks. In the situation in Fig. 5 this enforces that a pullback of \(\subseteq _j'\) along \(f_0\) (to express the composition of \(\langle \subseteq _j',a_j'\rangle \) and \(\langle id_{A_0},f_0\rangle \)) can be chosen to be equal to \(\subseteq _j\), the inclusion of the domain of definition of \(f_j\circ a_j\) into \(A_0\), see the upper square in Fig. 5, and it enforces that the lower square commutes. If \(x\in A_0\), this observation is equivalent to the statement \(x\in dom(a_j)\iff f_0(x)\in dom(a_j')\), because “\(\Rightarrow \)” corresponds to commutatitivity of the upper square and “\(\Leftarrow \)” corresponds to the pullback property (in \(\mathbb {S}\mathbb {E}\mathbb {T}\) and hence in \(\mathbb {G}\), in which pullbacks are constructed sortwise). This yields a more handy admissibility characterisation for \(\mathbb {C}\mathbb {S}\)morphisms:
Proposition 5
Usually a morphism between two partial algebras A and B requires only preservation of definedness, i.e. “\(\Rightarrow \)” in (2). In the next section, we justify why we additionally need reflection of definedness.
3.2 Why Must Definedness Be Reflected?
Since our goal is to show that SPO rewriting is applicable for comprehensive systems, we must show that \(\texttt {Par}(\mathbb {CS})\) possesses all pushouts. Assume we would not have claimed reflection of definedness for \(\mathbb {C}\mathbb {S}\)morphisms, but only commutativity of the two squares in Fig. 5, which is equivalent to claiming the properties of Proposition 5 except for the implication direction “\(\Leftarrow \)” in (2). In this case let’s consider for \(n=1\) two simple comprehensive systems. Let \(\mathbb {G}=\mathbb {S}\mathbb {E}\mathbb {T}\) and \(A_0=\{*\}\) and \(A_1=\{\bullet \}\) be two oneelement sets and let Open image in new window with \(a_1\) the totally undefined map depicted with \((*\quad \bullet )\) and \(\mathbf {A'} = ({a'_1}: {A_0} \rightarrow {A_1})\) with \(a_1'\) the unique total map from \(A_0\) to \(A_1\) depicted \((*\mapsto \bullet )\). If we only work with preservation of definedness, then morphism \(\langle id_A,f\rangle \mathbf {{}: {A} \rightarrow {A'}}\), in which \(f_0\) maps \(*\) to \(*\) and \(f_1\) maps \(\bullet \) to \(\bullet \), is an admissible morphism. We claim that the span \({\mathbf {A'}} \xleftarrow {\langle id_A,f\rangle } {\mathbf {A}} \xrightarrow {\langle id_A,f\rangle } {\mathbf {A'}}\) does not possess a pushout in \(\texttt {Par}(\mathbb {CS})\).
This example shows that we cannot expect to have all pushouts in \(\texttt {Par}(\mathbb {CS})\), if we would not require reflection of definedness. And this is true, even if the two morphisms, for which the pushout shall be constructed, are total monomorphisms.
3.3 Important Properties
Let’s now assume all \(\mathbb {C}\mathbb {S}\)morphisms to reflect definedness.
In the sequel, we will use formulations like “a property is valid componentwise” in \(\mathbb {C}\mathbb {S}\) or some construction “is carried out componentwise”. Since many of the following considerations are based on this methodology, we give a formalisation: “Pushout”, “Pullback”, “Monomorphism”, “Commutativity” impose truth of a predicate (a certain property) on a diagram in a category \(\mathbb {C}\). For pushouts and pullbacks the underlying diagram is a square, for the predicate “Monomorphism” it is a single arrow, for “Commutativity” it is an appropriate triangle of arrows. E.g. \(\mathbb {C}\mathbb {S}\)morphism \(\mathbf {{f}: {A} \rightarrow {B}}\) is a componentwise monomorphism means that each \(f_i\) is a \(\mathbb {G}\)monomorphism. More precisely: Given a diagram \(\mathcal {D}\) of any of the above mentioned shapes in \(\mathbb {C}\mathbb {S}\), let \(\mathcal {D}_i:=\mathcal {C}_i(\mathcal {D})\) with component functor \(\mathcal {C}_i\) from Proposition 4, then the predicate p is true componentwise if and only if it is true for \(\mathcal {D}_i\) in \(\mathbb {G}\) for all \(i\in \{0,\ldots ,n\}\).
Another formulation is “componentwise construction of predicate p”, where p is based on a certain universal property. If e.g. p is the predicate for pushouts, componentwise construction of a \(\mathbb {C}\mathbb {S}\)cospan \(\mathbf {{C} \xrightarrow {f'} {D} \xleftarrow {g'} {B}}\) from a \(\mathbb {C}\mathbb {S}\)span \(\mathbf {{C} \xleftarrow {g} {A} \xrightarrow {f} {B}}\) consists of two steps: In a first step one constructs pushout cospans \({C_i} \xrightarrow {f_i'} {D_i} \xleftarrow {g_i'} {B_i}\) of spans \(\mathcal {C}_i(\mathbf {{C} \xleftarrow {g} {A} \xrightarrow {f} {B}})\) for each \(i\in \{0,\ldots ,n\}\). In a second step one tries to define the projections \(d_j\) in Open image in new window, cf. Definition 3, with the help of the pushouts’ unique mediators. The cospan morphisms \(\mathbf {f'}\) and \(\mathbf {g'}\) consist of the respective components \((f_i')_{0\le i\le n}\) and \((g_i')_{0\le i\le n}\). The phrase “p can be constructed componentwise” then means that the newly constructed object \(\mathbf {D}\) is an admissible object according to Definition 3, that the newly created morphisms \(\mathbf {f'}\) and \(\mathbf {g'}\) are admissible according to Definition 4, and that predicate p holds on the resulting diagram in \(\mathbb {C}\mathbb {S}\), i.e. the square that arises from enhancing the above \(\mathbb {C}\mathbb {S}\)span by the \(\mathbb {C}\mathbb {S}\)cospan yields a pushout in \(\mathbb {C}\mathbb {S}\). Of course, this procedure applies to other universal constructions in a similar way and after such a construction, we know that property p is valid componentwise.
“Commutatitivity” is valid componentwise by definition, but we also obtain.
Proposition 6
(Componentwise Properties of \(\mathbb {C}\mathbb {S}\)). Morphism \(\mathbf {{f}: {A} \rightarrow {B}}\) is a monomorphism if and only if it is such componentwise.
 1.
all pullbacks
 2.
all pushouts
 3.
all coproducts
The equivalent characterization of hereditaryness in Proposition 3 uses the predicates pushout, pullback, monomorphism, and commutativity, of which we have shown that validity in \(\mathbb {C}\mathbb {S}\) is equivalent to componentwise validity. By jumping back and forth from a comprehensive system to its components, this yields
Corollary 1
\(\mathbb {C}\mathbb {S}\) is a hereditary pushout category. \(\square \)
Although it is not the focus of this paper, we mention another important consequence for the application of graph transformations in \(\mathbb {C}\mathbb {S}\):
Corollary 2
\(\mathbb {C}\mathbb {S}\) is a weak adhesive HLR category [4] w.r.t. the class of all monomorphisms.
Proof
Heindel proves in [8], Prop. 8.1 that this conclusion can be drawn from Corollary 1, if pushouts are always stable under pullbacks, i.e. the implication “top face pushout, all side faces pullbacks \(\Rightarrow \) bottom face pushout” holds for all choices of vertical morphisms in Fig. 3. But this implication is true in \(\mathbb {C}\mathbb {S}\) by Proposition 6 and because this holds in \(\mathbb {G}\) [6]. \(\square \)
This corollary guarantees validity of the classical theorems for DPO rewriting such as Local Church Rosser, Parallelism, or Local Confluence Theorem to hold in \(\mathbb {C}\mathbb {S}\), as well.^{5}
4 The Partial Map Category of Comprehensive Systems Admits All Pushouts
The goal of this section is to prove that SPO rewriting is well possible for comprehensive systems \(\mathbb {C}\mathbb {S}\) by showing that the category \(\texttt {Par}(\mathbb {CS})\) possesses all pushouts. This will follow mainly from a result of Hayman and Heindel:
Proposition 7
(Existence of Pushouts of Partial Maps, [7]). Let \(\mathbb {C}\) be a category with pullbacks in which for each span \({C} \xleftarrow {g} {A} \xrightarrow {f} {B}\) of morphisms there is a cospan \({C} \xrightarrow {f'} {D} \xleftarrow {g'} {B}\) making the resulting square commutative. \(\texttt {Par}(\mathbb {C})\) has all pushouts if and only if \(\mathbb {C}\) is a hereditary pushout category and inverse image functions have upper adjoints. \(\square \)
Section 4.1 is devoted to define inverse image functions and upper adjoints and Sect. 4.2 will show that they exist in \(\mathbb {C}\mathbb {S}\).
4.1 Upper Adjoints in General ...
Let in a category \(\mathbb {C}\) with pullbacks an object A be given. There is the semilattice \(Sub(A)\) of subobjects of A, which consists of all monomorphisms \({m}: {M} \rightarrowtail {A}\) modulo the equivalence relation \(m\equiv ({m'}: {M'} \rightarrowtail {A})\), where \(m\equiv m'\), if and only if there is an isomorphism \(i:M\rightarrow M'\) such that \(m'\circ i = m\). In the sequel, subobjects will be denoted by small letters \(m,n,\ldots \) and we implicitly assume their domain to be the corresponding upper case letter \(M, N,\ldots \).
Definition 5 (Inverse Images and Upper Adjoints)
Note that \(\mathcal {U}\) is unique, if it exists [7], and that \(f^{1}\) is monotone, since pulling back (between comma categories) is functorial and preserves monomorphisms.
4.2 ...and in \(\mathbb {C}\mathbb {S}\)
Proposition 8
\(\mathbb {C}\mathbb {S}\) has images and the pullback functors preserve them.
In \(\mathbb {G}\) pullbacks preserve epimorphisms, i.e. u is an epimorphism and the square in Fig. 9b has a unique diagonal [6] \(\hat{a}_j:I\rightarrow Im(f_j)\), such that everything commutes. Adding this diagonal in Fig. 9a yields Open image in new window and the inclusion Open image in new window. Moreover, \(\mathbf {Im(f)}\) can be shown to be the image of \(\mathbf {{f}: {A} \rightarrow {A'}}\) in \(\mathbb {C}\mathbb {S}\), because it was set up by componentwise epimonofactorization (in \(\mathbb {G}\)), in which the monopart is componentwise the least subobject of the respective codomains of \(f_0\) and \(f_j\).
Pullback functors preserve images in \(\mathbb {C}\mathbb {S}\) because of the essential uniqueness of epimonofactorisations, of preservation of monomorphisms and epimorphisms [6] under pullbacks in \(\mathbb {G}\), and componentwise pullback construction (cf. Proposition 6). \(\square \)
Proposition 9
(Upper Adjoints in \(\mathbb {C}\mathbb {S}\)). Let \(\mathbf {{f}: {A} \rightarrow {B}}\) and \(\mathbf {n} \in Sub(\mathbf {A})\), then \(\mathcal {U}(\mathbf {n}):=\bigcup \{\mathbf {m}\in Sub(\mathbf {B})\mid f^{1}(\mathbf {m})\sqsubseteq \mathbf {n}\}\) is the upper adjoint of \(f^{1}\).
Proof
To prove that \(\mathcal {U}\) is monotone, assume \(\mathbf {n},\mathbf {n}' \in Sub(\mathbf {A})\) with \(\mathbf {n}\sqsubseteq \mathbf {n'}\). Hence \(X:=\{\mathbf {m}\in Sub(\mathbf {B})\,\, f^{1}(\mathbf {m})\sqsubseteq \mathbf {n}\}\) \(\subseteq \{\mathbf {m}\in Sub(\mathbf {B})\mid f^{1}(\mathbf {m})\sqsubseteq \mathbf {n'}\}=:X'\) and thus there is the mediator \(\mathbf {u}:\coprod _{\mathbf {m}\in X}dom(\mathbf {m}) \rightarrow \coprod _{\mathbf {m}\in X'}dom(\mathbf {m})\), such that \(\mathcal {U}(\mathbf {n'})\) becomes a factor in a decomposition of \(\coprod _{\mathbf {m}\in X}dom(\mathbf {m}) \rightarrow A\). Since \(\mathcal {U}(\mathbf {n})\) is the least of these factors, we obtain \(\mathcal {U}(\mathbf {n}) \sqsubseteq \mathcal {U}(\mathbf {n'})\).
4.3 The Main Theorem
Theorem 1
\(\texttt {Par}(\mathbb {CS})\) has all pushouts.
Proof
Because \(\mathbb {C}\mathbb {S}\) has all pushouts by Proposition 6 and thus spancompletions, this follows from Proposition 7, Corollary 1 and Proposition 9. \(\square \)
Due to space limitations we can not provide an example in which the full power of SPO rewriting compared to the DPO approach can be demonstrated. Instead we provide a simple example, which reveals one additional helpful aspect of our definition of \(\mathbb {C}\mathbb {S}\)morphisms. The proper construction of arbitrary pushouts in \(\texttt {Par}(\mathbb {CS})\) (with noninjective rules and/or partial matches) is elaborated in [7].
Assume that a comprehensive system is in state \(\mathbf {G}\) (the bottom left system in Fig. 10) which is apparently inconsistent w.r.t IMC in Sect. 1, because the person in \(G_{2/3}\) possesses no phone. If it turns out that this person is the same as the one in \(G_1\), we can restore global consistency by applying rule Open image in new window, which deletes a binary commonality (dashed) among two person records and adds a new ternary commonality which comprises these two records. The application of the rule yields a comprehensive system \(\mathbf {H}\) (bottom right), which satisfies IMC. Despite being relatively simple, this example demonstrates an advantage of our approach: We do not need Negative Application Conditions to prevent repeated application of the rule, because there is no longer a corresponding match of \(\mathbf {L}\) into \(\mathbf {H}\). This is the case, because \(l_1\) (the projection of \(L_0\) into \(L_1\), cf. Definition 3) is undefined on the only element in \(L_0\), but the respective projection \(h_1\) in \(\mathbf {H}\) is defined on the hypothetically matched element (in \(H_0\)), i.e. the required reflection of definedness is violated, cf. Definition 4.
5 Related and Future Work
The best reference for Single Pushout Rewriting is [12], see also [2]. Comprehensive systems are basically a functor category invented in [20] and generalized in [11], its basic ideas originating from the theory of triple graphs [18]. Pushouts in partial map categories and especially hereditariness of colimits have been thoroughly investigated in [7, 8].
Our approach still lacks the proof that it is practically applicable, but we hope that SPO rules can serve as a basis for repair rules [15] in order to maintain consistency of informationally overlapping multimodels. We must also find an appropriate way of SPO rule typing, which can not rely on pure slice categories, because a typing morphism should not be forced to reflect definedness. And there should be a thorough characterisation of conflictfreeness in \(\mathbb {C}\mathbb {S}\), which is difficult, because upper adjoints in \(\mathbb {C}\mathbb {S}\) are not constructed componentwise. The situation is as in the following quotation: “The contents of this [paper] should rather be considered a starting point ... than the final document of this research issue”^{8}.
Footnotes
 1.
It seems that the subsequent proofs can still be carried out, if \(\mathbb {G}\) is such a more general structure. We will provide respective facts from time to time.
 2.
Usually the number of distributed systems under consideration.
 3.
One might consider elements of \(A_0\) to be vectors (of arbitrary arity), in which common elements are listed, hence the term “projection” for the \(a_j\).
 4.
A more general proof has been given in [11], if \(\mathbb {G}\) is a (variant of an) adhesive category, such that the result carries over to these base structures, as well.
 5.
Whereas we obtain this result as a corollary from hereditariness, it is proved directly for underlying adhesive categories in [11].
 6.
Since we are working with equivalence classes, is easy to see that \(f^{1}\) is independent of the choice of representative of m and independent of the choice of pullback.
 7.
A function \(U:(X,\le _X)\rightarrow (Y,\le _Y)\) between two partially ordered sets is called monotone, if it preserves the order, i.e. \(\forall x,x'\in X: x\le _X x'\Rightarrow U(x)\le _Y U(x')\).
 8.
This is an almost identical citation of the last statement in Michael’s PhD Thesis!
Notes
Acknowledgment
We want to thank Tobias Heindel for pointing to the basic theoretical results needed to produce the results in this paper. Moreover, we would like to thank the referees for their constructive criticism.
References
 1.Adámek, J., Herrlich, H., Strecker, G.E.: Abstract and Concrete Categories. KATMAT: University Bremen (2004). http://katmat.math.unibremen.de/acc/acc.pdf
 2.Burmeister, P., Monserrat, M., Rosselló, F., Valiente, G.: Algebraic transformation of unary partial algebras II: singlepushout approach. Theor. Comput. Sci. 216(1–2), 311–362 (1999)MathSciNetCrossRefGoogle Scholar
 3.Diskin, Z., König, H., Lawford, M.: Multiple model synchronization with multiary delta lenses with amendment and KPutput. Formal Aspects Comput. 31(5), 611–640 (2019). https://doi.org/10.1007/s00165019004930MathSciNetCrossRefzbMATHGoogle Scholar
 4.Ehrig, H., Ehrig, K., Prange, U., Taentzer, G.: Fundamentals of Algebraic Graph Transformation. MTCSAES. Springer, Heidelberg (2006). https://doi.org/10.1007/3540311882CrossRefzbMATHGoogle Scholar
 5.Feldmann, S., Kernschmidt, K., Wimmer, M., VogelHeuser, B.: Managing intermodel inconsistencies in modelbased systems engineering: application in automated production systems engineering. J. Syst. Softw. 153, 105–134 (2019). https://doi.org/10.1016/j.jss.2019.03.060. http://www.sciencedirect.com/science/article/pii/S0164121219300639CrossRefGoogle Scholar
 6.Goldblatt, R.: Topoi: The Categorial Analysis of Logic. Dover Publications, New York (1984)zbMATHGoogle Scholar
 7.Hayman, J., Heindel, T.: On pushouts of partial maps. In: Giese, H., König, B. (eds.) ICGT 2014. LNCS, vol. 8571, pp. 177–191. Springer, Cham (2014). https://doi.org/10.1007/9783319091082_12CrossRefGoogle Scholar
 8.Heindel, T.: A category theoretical approach to the concurrent semantics of rewriting: adhesive categories and related concepts. Ph.D. thesis, University of DuisburgEssen (2009). http://duepublico.uniduisburgessen.de/servlets/DerivateServlet/Derivate24329/diss.pdf
 9.Heindel, T.: Hereditary pushouts reconsidered. In: Ehrig, H., Rensink, A., Rozenberg, G., Schürr, A. (eds.) ICGT 2010. LNCS, vol. 6372, pp. 250–265. Springer, Heidelberg (2010). https://doi.org/10.1007/9783642159282_17CrossRefGoogle Scholar
 10.Kennaway, R.: Graph rewriting in some categories of partial morphisms. In: Ehrig, H., Kreowski, H.J., Rozenberg, G. (eds.) Graph Grammars 1990. LNCS, vol. 532, pp. 490–504. Springer, Heidelberg (1991). https://doi.org/10.1007/BFb0017408CrossRefzbMATHGoogle Scholar
 11.Kosiol, J., Fritsche, L., Schürr, A., Taentzer, G.: Adhesive subcategories of functor categories with instantiation to partial triple graphs. In: Guerra, E., Orejas, F. (eds.) ICGT 2019. LNCS, vol. 11629, pp. 38–54. Springer, Cham (2019). https://doi.org/10.1007/9783030236113_3CrossRefGoogle Scholar
 12.Löwe, M.: Extended algebraic graph transformation. Ph.D. thesis, Technical University of Berlin, Germany (1991). http://dnb.info/910935696
 13.Löwe, M., Tempelmeier, M.: Singlepushout rewriting of partial algebras. In: Plump, D. (ed.) Proceedings of GCM Colocated with ICGT/STAF, L’Aquila, Italy. CEUR Workshop Proceedings, vol. 1403, pp. 82–96 (2015). http://ceurws.org/Vol1403/paper7.pdf
 14.Löwe, M.: Algebraic approach to singlepushout graph transformation. Theoret. Comput. Sci. 109(1), 181–224 (1993)MathSciNetCrossRefGoogle Scholar
 15.Rabbi, F., Lamo, Y., Yu, I.C., Kristensen, L.M.: A diagrammatic approach to model completion. In: Dingel, J., Kokaly, S., Lucio, L., Salay, R., Vangheluwe, H. (eds.) Proceedings of the 4th Workshop on the Analysis of Model Transformations Colocated with MODELS 2015, Ottawa, Canada. CEUR Workshop Proceedings, vol. 1500, pp. 56–65. CEURWS.org (2015). http://ceurws.org/Vol1500/paper7.pdf
 16.Raoult, J.: On graph rewritings. Theor. Comput. Sci. 32, 1–24 (1984). https://doi.org/10.1016/03043975(84)900215MathSciNetCrossRefzbMATHGoogle Scholar
 17.Robinson, E., Rosolini, G.: Categories of partial maps. Inf. Comput. 79(2), 95–130 (1988)MathSciNetCrossRefGoogle Scholar
 18.Schürr, A.: Specification of graph translators with triple graph grammars. In: Mayr, E.W., Schmidt, G., Tinhofer, G. (eds.) WG 1994. LNCS, vol. 903, pp. 151–163. Springer, Heidelberg (1995). https://doi.org/10.1007/3540590714_45CrossRefGoogle Scholar
 19.Stevens, P.: Bidirectional transformations in the large. In: MODELS 2017, pp. 1–11 (2017)Google Scholar
 20.Stünkel, P., König, H., Lamo, Y., Rutle, A.: Multimodel correspondence through intermodel constraints. In: Conference Companion of the 2nd International Conference on Art, Science, and Engineering of Programming, Nice, France, 09–12 April 2018, pp. 9–17 (2018). http://doi.acm.org/10.1145/3191697.3191715
 21.Stünkel, P., König, H., Lamo, Y., Rutle, A.: Towards multiple model synchronization with comprehensive systems. In: Wehrheim, H., Cabot, J. (eds.) FASE 2020. LNCS, vol. 12076, pp. 335–356. Springer, Cham (2020). https://doi.org/10.1007/9783030452346_17CrossRefGoogle Scholar
 22.Stünkel, P., König, H., Lamo, Y., Rutle, A.: Towards multiple model synchronization with comprehensive systems: extended version. Technical report, University of Applied Sciences, FHDW Hannover (2020). https://fhdwdev.ha.bib.de/public/papers/0202001.pdf
 23.Trollmann, F., Albayrak, S.: Extending model synchronization results from triple graph grammars to multiple models. In: Van Van Gorp, P., Engels, G. (eds.) ICMT 2016. LNCS, vol. 9765, pp. 91–106. Springer, Cham (2016). https://doi.org/10.1007/9783319420646_7CrossRefGoogle Scholar