11institutetext: Vrije Universiteit Amsterdam, Amsterdam, The Netherlands
11email: {r.overbeek, j.endrullis<EMAIL_ADDRESS>
# Graph Rewriting and Relabeling with PBPO+:
A Unifying Theory for Quasitoposes

Roy Overbeek  Jörg Endrullis  Aloïs Rosset

###### Abstract

We extend the powerful Pullback-Pushout (PBPO) approach for graph rewriting
with strong matching. Our approach, called PBPO+, allows more control over the
embedding of the pattern in the host graph, which is important for a large
class of rewrite systems. We argue that PBPO+ can be considered a unifying
theory in the general setting of quasitoposes, by demonstrating that PBPO+ can
define a strict superset of the rewrite relations definable by PBPO, AGREE and
DPO. Additionally, we show that PBPO+ is well suited for rewriting labeled
graphs and some classes of attributed graphs, by introducing a lattice
structure on the label set and requiring graph morphisms to be order-
preserving.

##  1 Introduction

Injectively matching a graph pattern $P$ into a host graph $G$ induces a
classification of $G$ into three parts: (i) a _match graph_ $M$, the image of
$P$; (ii) a _context graph_ $C$, the largest subgraph disjoint from $M$; and
(iii) a _patch_ $J$, the set of edges that are in neither $M$ nor $C$. For
example, if $P$ and $G$ are respectively

$b$$a$$a$and$b$$a$$a$$b$$a$$b$$c$

then $M$, $C$ and $J$ are indicated in green (bold), black and red (dotted),
respectively. We call this kind of classification a _patch decomposition_.

Guided by the notion of patch decomposition, we recently introduced the
expressive Patch Graph Rewriting (PGR) formalism [1]. Like most graph
rewriting formalisms, PGR rules specify a replacement of a left-hand side
(lhs) pattern $L$ by a right-hand side (rhs) $R$. Unlike most rewriting
formalisms, however, PGR rules allow one to (a) constrain the permitted shapes
of patches around a match for $L$, and (b) specify how the permitted patches
should be transformed, where transformations include rearrangement, deletion
and duplication of patch edges.

Whereas PGR is defined set theoretically, in this paper we propose a more
elegant categorical approach, called _PBPO +_, inspired by the same ideas. The
name derives from the fact that the approach is obtained by strengthening the
matching mechanism of the Pullback-Pushout (PBPO) approach by Corradini et al.
[2]. Categorical approaches have at least three important advantages over set
theoretic ones: (i) the classes of structures the method can be applied to is
vastly generalized, (ii) typical meta-properties of interest (such as
parallelism and concurrency) are more easily studied, and (iii) it makes it
easier to compare to existing categorical frameworks.

After discussing the preliminaries in Section 2, we introduce PBPO+ in Section
3, and then provide a detailed comparison with PBPO in Section 4. We argue
that PBPO+ is preferable in situations where matching is not controlled, such
as when specifying generative grammars or modeling execution.

Next, we study PBPO+ in the setting of quasitoposes in Section 5. Quasitoposes
generalize toposes, which can be described as capturing “set-like” categories
[3, Preface]. Quasitoposes include not only the categories of sets, directed
multigraphs [4] and typed graphs [5] (all of which are toposes), but also a
variety of structures such as Heyting algebras (considered as categories) [3],
and the categories of simple graphs (equivalently, binary relations) [6],
fuzzy sets [3], algebraic specifications [6] and safely marked Petri Nets [6].
Most importantly, we show that, using regular monic matching, PBPO+ has enough
expressive power in the quasitopos setting to generate any rewrite relation
generated by the PBPO, AGREE [5, 7], or DPO [8] rewrite formalisms, while the
converse statements are not true. Thus, in this setting, PBPO+ can be viewed
as a unifying theory, additionally enabling the definition of new rewrite
relations.

In Section 6, we adopt a more applied perspective, and show that PBPO+ easily
lends itself for rewriting labeled graphs and certain attributed graphs. To
this end, we define a generalization of the usual category of labeled graphs,
Graph(L,≤), in which the set of labels forms a complete lattice
$(\mathcal{L},\leq)$. Not only does the combination of PBPO+ and Graph(L,≤)
enable constraining and transforming the patch graph in flexible ways, it also
allows naturally modeling notions of relabeling, variables and sorts in
rewrite rules. As we will clarify in the Discussion (Section 7), such
mechanisms have typically been studied in the context of Double Pushout (DPO)
rewriting [8], where the requirement to construct a pushout complement leads
to technical complications and restrictions.

This paper extends the paper presented at ICGT2021 [9]. In the conference
paper, we showed that in the setting of toposes, PBPO+ can define all rewrite
relations definable by PBPO [9, Section 4.3]. For the present extension, we
have generalized this result to quasitoposes (additionally improving the
proof), and integrated it into the wider quasitopos study provided in Section
5, which is completely new material. Additionally, we have improved the proofs
and presentation in Section 3, and we relate category Graph(L,≤) to the
category of fuzzy sets in Section 5.

###### Remark 1

We have recently published a gentle tutorial on PBPO+ [10], targeted
especially to readers unacquainted with category theory.

##  2 Preliminaries

We assume familiarity with various basic categorical notions, notations and
results, including morphisms $X\to Y$, pullbacks, pushouts, monomorphisms
(monos) $X\rightarrowtail Y$, epimorphisms (epis) $X\twoheadrightarrow Y$, and
identities $1_{X}:X\to X$ [11, 12].

The following well-known lemma (also known as the pasting law for pullbacks)
is used frequently throughout the paper.

######  Lemma 1 (Pullback Lemma)

Suppose the right square of

${A}$${B}$${C}$${D}$${E}$${F}$${\mathrm{PB}}$

is a pullback and the left square commutes. Then the outer square is a
pullback iff the left square is a pullback. ∎

###### Corollary 1

If in a commutative cube

${F}$${G}$${E}$${H}$${B}$${C}$${A}$${D}$

all vertical faces except the back face ($FGBC$) are known to be pullbacks,
then the back face is also a pullback. ∎

######  Definition 1 (Graph Notions)

Let a label set $\mathcal{L}$ be fixed. An ($\mathcal{L}$-labeled)
_(multi)graph_ $G$ consists of a set of vertices $V$, a set of edges $E$,
source and target functions $\mathit{s},\mathit{t}:E\to V$, and label
functions $\ell^{V}:V\to\mathcal{L}$ and $\ell^{E}:E\to\mathcal{L}$.

A graph is _unlabeled_ if $\mathcal{L}$ is a singleton.

A _premorphism_ between graphs $G$ and $G^{\prime}$ is a pair of maps

$\phi=(\phi_{V}:V_{G}\to V_{G^{\prime}},\phi_{E}:E_{G}\to E_{G^{\prime}})$

satisfying
$(s_{G^{\prime}},t_{G^{\prime}})\circ\phi_{E}=\phi_{V}\circ(s_{G},t_{G})$.

A _homomorphism_ is a label-preserving premorphism $\phi$, i.e., a premorphism
satisfying $\ell^{V}_{G^{\prime}}\circ\phi_{V}=\ell^{V}_{G}$ and
$\ell^{E}_{G^{\prime}}\circ\phi_{E}=\ell^{E}_{G}$.

######  Definition 2 (Category Graph [13])

The category Graph has graphs as objects, parameterized over some global (and
usually implicit) label set $\mathcal{L}$, and homomorphisms as arrows.

###### Remark 2

Graph can also be obtained as a slice of a presheaf category (see Corradini et
al. [7, Section 2.1-2] for details), by virtue of which one immediately
obtains that it is a topos, and hence a quasitopos.

The definition below formally fixes some graph terminology (see Section 1).

######  Definition 3 (Patch Decomposition [1])

Given a premorphism $x:X\to G$, we call the image $M=\mathit{im}(x)$ of $x$
the _match graph_ in $G$, $G-M$ the _context graph_ $C$ induced by $x$ (i.e.,
$C$ is the largest subgraph disjoint from $M$), and the set of edges
$E_{G}-E_{M}-E_{C}$ the set of _patch edges_ (or simply, _patch_) induced by
$x$.

##  3 PBPO+

We introduce PBPO+, which strengthens the matching mechanism of PBPO [2]. In
Section 4, we compare the two approaches in detail.

######  Definition 4 (PBPO+ Rewrite Rule)

A _PBPO + rewrite rule_ $\rho$ is a diagram

$\rho\ =\ $
${L}$${K}$${R}$${L^{\prime}}$${K^{\prime}}$$\scriptstyle{t_{L}}$${\mathrm{PB}}$$\scriptstyle{t_{K}}$$\scriptstyle{l}$$\scriptstyle{r}$$\scriptstyle{l^{\prime}}$.

$L$ is the _lhs pattern_ of the rule, $L^{\prime}$ its _(context) type_ and
$t_{L}$ the _(context) typing_ of $L$. Similarly for the _interface_ $K$. $R$
is the _rhs pattern_ or _replacement for $L$_.

We often depict the pushout
$K^{\prime}\xrightarrow{r^{\prime}}R^{\prime}\xleftarrow{t_{R}}R$ for span
$K^{\prime}\xleftarrow{t_{K}}K\xrightarrow{r}R$, because it shows the
schematic effect of applying the rewrite rule. We reduce the opacity of
$R^{\prime}$ to emphasize that it is not part of the rule definition.

######  Example 1 (Rewrite Rule in Graph)

A simple example of a rule for unlabeled graphs is the following:

$L$$x_{1}$$x_{2}$$y$$K$$x_{1}$$x_{2}$$y$$R$$x_{1}$$y$$x_{2}$$u$$L^{\prime}$$x_{1}$$x_{2}$$y$$z$$K^{\prime}$$x_{1}$$x_{2}$$y$$z$$R^{\prime}$$x_{1}$$y$$x_{2}$$z$$u$

In this and subsequent examples a vertex is a non-empty set
$\\{x_{1},\ldots,x_{n}\\}$ represented by a box $x_{1}$ $\cdots$ $x_{n}$ ; and
each morphism $\phi=(\phi_{V},\phi_{E}):G\to G^{\prime}$ is the unique
morphism satisfying $S\subseteq\phi(S)$ for all $S\in V_{G}$. For instance,
for $\\{x_{1}\\},\\{x_{2}\\}\in V_{K}$,
$l(\\{x_{1}\\})=l(\\{x_{2}\\})=\\{x_{1},x_{2}\\}\in V_{L}$. For notational
convenience, we will usually use examples that ensure uniqueness of each
$\phi$ (in particular, we ensure that $\phi_{E}$ is uniquely determined).
Colors are purely supplementary, and elements in $L^{\prime}$ and $K^{\prime}$
have reduced opacity if they do not lie in the images of $t_{L}$ and $t_{K}$,
respectively.

######  Definition 5 (Strong Match)

A _match morphism_ $m:L\to G_{L}$ and an _adherence morphism_ $\alpha:G_{L}\to
L^{\prime}$ form a _strong match_ for a context typing $t_{L}:L\to L^{\prime}$
if square $t_{L}\circ\mathrm{1}_{L}=\alpha\circ m$, i.e.,

${L}$${G_{L}}$${L}$${L^{\prime}}$$\scriptstyle{m}$${\mathrm{PB}}$$\scriptstyle{\alpha}$$\scriptstyle{t_{L}}$

is a pullback.

######  Remark 3 (Preimage Interpretation)

In both Set and Graph, and many other categories of structured sets, the
strong match diagram of Definition 5 states that the preimage of $t_{L}(L)$
under $\alpha:G_{L}\to L^{\prime}$ is $L$ itself. So each element of
$t_{L}(L)$ is the $\alpha$-image of exactly one element of $G_{L}$.

###### Proposition 1

Assume C has pullbacks. Let a strong match as in Definition 5 be given. Then
$m$ is monic iff $t_{L}$ is monic.

###### Proof

If $t_{L}$ is monic, monicity of $m$ follows by pullback stability.

For the other direction, assume $m$ is monic. Suppose $t_{L}\circ x=t_{L}\circ
y$ for a parallel pair of morphisms $x,y:X\to L$. Then $\alpha\circ m\circ
x=t_{L}\circ x=t_{L}\circ y=\alpha\circ m\circ y$. Then in diagram

${X}$${X}$${L}$${G_{L}}$${X}$${L}$${L^{\prime}}$$\scriptstyle{m\circ
y}$$\scriptstyle{!z}$$\scriptstyle{x}$${\mathrm{PB}}$$\scriptstyle{m}$${\mathrm{PB}}$$\scriptstyle{\alpha}$$\scriptstyle{x}$$\scriptstyle{t_{L}}$

the two pullback squares compose by the pullback lemma. Hence there exist a
unique $z$ such that $\mathrm{1}_{X}=\mathrm{1}_{X}\circ z=z$ and $m\circ
y=m\circ x\circ z$. Hence $z$ can be canceled and $m\circ y=m\circ x$. By
monicity of $m$, $x=y$. Thus $t_{L}$ is monic. ∎

Because of Proposition 1, if match morphisms $m$ are required to be monic (as
often is the case), rules with non-monic $t_{L}$ will not give rise to strong
matches, and so will not give rise to rewrite steps.

######  Proposition 2 (Unique First Factor)

In any category, if diagrams

${A}$${B}$${A}$${C}$$\scriptstyle{h}$${\mathrm{PB}}$$\scriptstyle{g}$$\scriptstyle{f}$

and
${A}$${B}$${A}$${C}$$\scriptstyle{h^{\prime}}$${=}$$\scriptstyle{g}$$\scriptstyle{f}$

hold then $h=h^{\prime}$.

###### Proof

The universal morphism obtained from the pullback square is $\mathrm{1}_{A}$.
∎

Proposition 2 implies that because of the strong match property, $m$ is
uniquely defined by $\alpha$ and $t_{L}$. However, in practice it is usually
more natural to first fix a match $m$, and to subsequently verify whether it
can be extended into a suitable adherence morphism. For certain choices of
$t_{L}$, $\alpha$ may moreover be uniquely determined by $m$ (if it exists).
See Theorem 5.1 for an example.

In reading the following definition, it may be helpful to refer to Example 2
alongside it.

######  Definition 6 (PBPO+ Rewrite Step)

A PBPO+ rewrite rule $\rho$ (left), a match morphism $m:L\to G_{L}$ and an
adherence morphism $\alpha:G_{L}\to L^{\prime}$ induce a rewrite step
${G_{L}}\Rightarrow_{\mathrm{PBPO}^{+}}^{\rho,(m,\alpha)}{G_{R}}$ on arbitrary
$G_{L}$ and $G_{R}$ if the properties indicated by the commuting diagram
(right)

$\rho\ =\ $
${L}$${K}$${R}$${L^{\prime}}$${K^{\prime}}$$\scriptstyle{t_{L}}$${\mathrm{PB}}$$\scriptstyle{t_{K}}$$\scriptstyle{l}$$\scriptstyle{r}$$\scriptstyle{l^{\prime}}$
${K}$${R}$${L}$${G_{L}}$${G_{K}}$${G_{R}}$${L}$${L^{\prime}}$${K^{\prime}}$$\scriptstyle{!u}$$\scriptstyle{r}$$\scriptstyle{w}$$\scriptstyle{m}$${\mathrm{PB}}$$\scriptstyle{\alpha}$$\scriptstyle{g_{L}}$$\scriptstyle{g_{R}}$$\scriptstyle{u^{\prime}}$${\mathrm{PO}}$$\scriptstyle{t_{L}}$${\mathrm{PB}}$$\scriptstyle{t_{K}}$$\scriptstyle{l^{\prime}}$

hold, where $u:K\to G_{K}$ is the unique morphism satisfying
$t_{K}=u^{\prime}\circ u$ (Lemma 2).

We write $G_{L}\Rightarrow_{\mathrm{PBPO}^{+}}^{\rho,m}G_{R}$ if there exists
an $\alpha$ such that
${G_{L}}\Rightarrow_{\mathrm{PBPO}^{+}}^{\rho,(m,\alpha)}{G_{R}}$, and
${G_{L}}\Rightarrow_{\mathrm{PBPO}^{+}}^{\rho}{G_{R}}$ if there exists an $m$
such that $G_{L}\Rightarrow_{\mathrm{PBPO}^{+}}^{\rho,m}G_{R}$. 111No
assumptions are needed on the underlying category C: if not all (co)limits
exist, this simply restricts the possible rewrite rules and steps.

It can be seen that the rewrite step diagram consists of a match square, a
pullback square for extracting (and possibly duplicating) parts of $G_{L}$,
and finally a pushout square for gluing these parts along pattern $R$.

We must prove that there indeed exists a unique $u$ such that
$t_{K}=u^{\prime}u$ in the rewrite step diagram. The following lemma
establishes this and two other facts.

######  Lemma 2 (On $u$)

In any category, let the pullback of the rewrite rule and the pullbacks of the
rewrite step be given. Then there exists a unique morphism $u:K\to G_{K}$
satisfying $t_{K}={u^{\prime}\circ u}$. Moreover, the following properties
hold:

  1. 1.

squares

${L}$${K}$${K}$${G_{K}}$${G_{L}}$${G_{K}}$${K}$${K^{\prime}}$$\scriptstyle{m}$$\scriptstyle{l}$$\scriptstyle{u}$and$\scriptstyle{u}$$\scriptstyle{u^{\prime}}$$\scriptstyle{g_{L}}$$\scriptstyle{t_{K}}$

are pullbacks; and

  2. 2.

if $m$ or $t_{K}$ is monic, then $u$ is monic.

###### Proof

Consider the commuting diagram

${L}$${K}$${G_{L}}$${G_{K}}$${L^{\prime}}$${K^{\prime}}$$\scriptstyle{m}$$\scriptstyle{t_{L}}$$\scriptstyle{t_{K}}$$\scriptstyle{l}$$\scriptstyle{!u}$$\scriptstyle{\alpha}$PB$\scriptstyle{g_{L}}$$\scriptstyle{u^{\prime}}$$\scriptstyle{l^{\prime}}$

where morphism $u$ satisfying $t_{K}={u^{\prime}\circ u}$ and ${m\circ
l}={g_{L}\circ u}$ is inferred by the universal property of the bottom square.
Because the outer square is the pullback of the rewrite rule, ${m\circ
l}={g_{L}\circ u}$ is a pullback by the pullback lemma. Moreover, this shows
that monicity of $u$ follows from monicity of $t_{K}$ ($g\circ f$ is monic
$\Rightarrow$ $f$ is monic) or monicity of $m$ and pullback stability.

The accumulated squares can be represented as the commutative cube

${K}$${G_{K}}$${L}$${G_{L}}$${K}$${K^{\prime}}$${L}$${L^{\prime}}$$\scriptstyle{u}$$\scriptstyle{l}$$\scriptstyle{u^{\prime}}$$\scriptstyle{g_{L}}$$\scriptstyle{m}$$\scriptstyle{t_{K}}$$\scriptstyle{l}$$\scriptstyle{l^{\prime}}$$\scriptstyle{t_{L}}$$\scriptstyle{\alpha}$

.

which shows that square $t_{K}\circ\mathrm{1}_{K}=t_{K}=u\circ u^{\prime}$ is
a pullback square by Corollary 1. Finally, because it is a pullback square, it
follows from Proposition 2 that for any $v$ with $t_{K}=u^{\prime}\circ v$,
$v=u$. ∎

######  Proposition 3 (Bottom-Right Pushout)

Let cospan $K^{\prime}\xrightarrow{r^{\prime}}R^{\prime}\xleftarrow{t_{R}}R$
be a pushout for span $R\xleftarrow{r}K\xrightarrow{t_{K}}K^{\prime}$ of rule
$\rho$ in Definition 6. Then in the rewrite step diagram, there exists a
morphism $w^{\prime}:G_{R}\to R^{\prime}$ such that $t_{R}=w^{\prime}\circ w$,
and $K^{\prime}\xrightarrow{r^{\prime}}R^{\prime}\xleftarrow{w^{\prime}}G_{R}$
is a pushout for
$K^{\prime}\xleftarrow{u^{\prime}}G_{K}\xrightarrow{g_{R}}G_{R}$.

###### Proof

The argument is similar to the initial part of the proof of Lemma 2, but now
uses the dual statement of the pullback lemma. ∎

Lemma 2 and Proposition 3 show that a PBPO+ step defines a commuting diagram
similar to the PBPO definition (Definition 9):

${\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}{L}}$${K}$${R}$${L}$${G_{L}}$${G_{K}}$${G_{R}}$${L}$${L^{\prime}}$${K^{\prime}}$${\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}{R^{\prime}}}$$\scriptstyle{\definecolor[named]{.}{rgb}{.5,.5,.5}\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}m}$$\scriptstyle{u}$$\scriptstyle{r}$$\scriptstyle{\definecolor[named]{.}{rgb}{.5,.5,.5}\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}l}$${\definecolor[named]{.}{rgb}{.5,.5,.5}\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathrm{PB}}$${\mathrm{PO}}$$\scriptstyle{w}$$\scriptstyle{\definecolor[named]{.}{rgb}{.5,.5,.5}\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}t_{R}}$$\scriptstyle{m}$${\mathrm{PB}}$$\scriptstyle{\alpha}$$\scriptstyle{u^{\prime}}$$\scriptstyle{g_{L}}$$\scriptstyle{g_{R}}$${\mathrm{PB}}$${\definecolor[named]{.}{rgb}{.5,.5,.5}\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathrm{PO}}$$\scriptstyle{\definecolor[named]{.}{rgb}{.5,.5,.5}\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}w^{\prime}}$$\scriptstyle{t_{L}}$$\scriptstyle{\definecolor[named]{.}{rgb}{.5,.5,.5}\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}t_{L}}$$\scriptstyle{l^{\prime}}$$\scriptstyle{\definecolor[named]{.}{rgb}{.5,.5,.5}\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color<EMAIL_ADDRESS>
which will guide our depictions of rewrite steps. We will omit the match
diagram in such depictions.

######  Example 2 (Rewrite Step)

Applying the rule given in Example 1 to $G_{L}$ (as depicted below) has the
following effect:

$L$$x_{1}$$x_{2}$$y$$G_{L}$$x_{1}$$x_{2}$$y$$z_{1}$$z_{2}$$z_{3}$$G_{K}$$x_{2}$$x_{1}$$y$$z_{1}$$z_{2}$$z_{3}$$K$$x_{1}$$x_{2}$$y$$R$$x_{1}$$y$$x_{2}$$u$$G_{R}$$x_{1}$$y$$x_{2}$$z_{1}$$z_{2}$$z_{3}$$u$$L^{\prime}$$x_{1}$$x_{2}$$y$$z_{1}$$z_{2}$$z_{3}$$K^{\prime}$$x_{1}$$x_{2}$$y$$z_{1}$$z_{2}$$z_{3}$$R^{\prime}$$x_{1}$$y$$x_{2}$$z_{1}$$z_{2}$$z_{3}$$u$

This example illustrates (i) how permitted patches can be constrained (e.g.,
$L^{\prime}$ forbids patch edges _targeting_ $y$), (ii) how patch edge
endpoints that lie in the image of $t_{L}$ can be redefined, (iii) how patch
edges can be deleted, and (iv) how patch edges can be duplicated.

In the examples of this section, we have restricted our attention to unlabeled
graphs. In Section 6, we introduce a new category Graph(L,≤), and show that is
more suitable than Graph for rewriting labeled graphs using PBPO+. Section 6
can largely be read independently of Sections 4 and 5, which situate PBPO+ and
are more foundational in character.

##  4 Relating PBPO+ and PBPO

In Section 4.1, we recall and compare the PBPO definitions for rule, match and
step, clarifying why PBPO+ is shorthand for _PBPO with strong matching_. We
then argue why strong matching is usually desirable in Section 4.2.

###  4.1 PBPO: Rule, Match & Step

######  Definition 7 (PBPO Rule [2])

A _PBPO rule_ $\rho$ is a commutative diagram as shown on the right. The
bottom span can be regarded as a typing for the top span. The rule is in
_canonical form_ if the left square is a pullback and the right square is a
pushout.

${L}$${K}$${R}$${L^{\prime}}$${K^{\prime}}$${R^{\prime}}$$\scriptstyle{t_{L}}$$\scriptstyle{l}$$\scriptstyle{r}$$\scriptstyle{t_{K}}$${=}$${=}$$\scriptstyle{t_{R}}$$\scriptstyle{l^{\prime}}$$\scriptstyle{r^{\prime}}$

Every PBPO rule is equivalent to a rule in canonical form [2], and in PBPO+,
rules are limited to those in canonical form.

######  Definition 8 (PBPO Match [2])

A _PBPO match_ for a typing $t_{L}:L\to L^{\prime}$ is a pair of morphisms
$(m:L\to G,\alpha:G\to L^{\prime})$ such that $t_{L}=\alpha\circ m$.

The pullback construction used to establish a match in PBPO+ (Definition 5)
implies $t_{L}=\alpha\circ m$. Thus PBPO matches are more general than the
strong match used in PBPO+ (Definition 5). More specifically for Graph, PBPO
allows mapping elements of the host graph $G_{L}$ not in the image of $m:L\to
G_{L}$ onto the image of $t_{L}$, whereas PBPO+ forbids this. In the next
subsection, we will argue why it is often desirable to forbid such mappings.

######  Definition 9 (PBPO Rewrite Step [2])

A PBPO rule $\rho$ (as in Definition 7) induces a _PBPO step_
${G_{L}}\Rightarrow_{\mathrm{PBPO}}^{\rho,(m,\alpha)}{G_{R}}$ if there exists
a diagram

${L}$${K}$${R}$${G_{L}}$${G_{K}}$${G_{R}}$${L^{\prime}}$${K^{\prime}}$${R^{\prime}}$$\scriptstyle{m}$$\scriptstyle{u}$$\scriptstyle{r}$$\scriptstyle{l}$${\mathrm{=}}$${\mathrm{PO}}$$\scriptstyle{w}$$\scriptstyle{t_{R}}$$\scriptstyle{\alpha}$$\scriptstyle{u^{\prime}}$$\scriptstyle{g_{L}}$$\scriptstyle{g_{R}}$${\mathrm{PB}}$${=}$$\scriptstyle{w^{\prime}}$$\scriptstyle{t_{L}}$$\scriptstyle{l^{\prime}}$$\scriptstyle{r^{\prime}}$$\scriptstyle{t_{K}}$

where (i) $u:K\to G_{K}$ is uniquely determined by the universal property of
pullbacks and makes the top-left square commuting, and (ii)
$w^{\prime}:G_{R}\to R^{\prime}$ is uniquely determined by the universal
property of pushouts and makes the bottom-right square commuting, and (iii)
$t_{L}=\alpha\circ m$.

The strong match square of PBPO+ allows simplifying the characterization of
$u$, as shown in the proof to Lemma 2. This simplification is not possible for
PBPO (see Remark 4). The bottom-right square is omitted in the definition of a
PBPO+ rewrite step, but can be reconstructed through a pushout (modulo
isomorphism). So this difference is not essential.

###### Remark 4

In a PBPO rewrite step, not every morphism $u:K\to G_{K}$ satisfying
$u^{\prime}\circ u=t_{K}$ corresponds to the arrow uniquely determined by the
top-left pullback. This can be seen in the example of a (canonical) PBPO
rewrite rule and step depicted in:

$R$$x_{1}$$x_{2}$$G_{L}$$a$$b$$L$$x$$G_{K}$$a_{1}$$a_{2}$$b_{1}$$b_{2}$$K$$x_{1}$$x_{2}$$G_{R}$$a_{1}$$a_{2}$$b_{1}$$b_{2}$$L^{\prime}$$x$$K^{\prime}$$x_{1}$$x_{2}$$R^{\prime}$$x_{1}$$x_{2}$

Because our previous notational convention breaks for this example, we
indicate two morphisms by dotted arrows. The others can be inferred.

Morphism $u:K\to G_{K}$ (as determined by the top-left pullback) is indicated.
However, it can be seen that three other morphisms $v:K\to G_{K}$ satisfy
$u^{\prime}\circ v=t_{K}$, because every $x\in V_{K^{\prime}}$ has two
elements in its preimage in $G_{K}$.

###  4.2 The Case for Strong Matching

The two following examples serve to illustrate why we find it necessary to
strengthen the matching criterion when matching is not controlled.

###### Example 3

In PBPO+, an application of the rule

$L$$x$$K$$x$$R$$x$$L^{\prime}$$x$$y$$K^{\prime}$$x$$y$$R^{\prime}$$x$$y$

in an unlabeled graph $G_{L}$ removes a loop from an isolated vertex that has
a single loop, and preserves everything else. In PBPO, a match is allowed to
map all of $G_{L}$ into the component determined by vertex $\\{x\\}$, so that
the rule deletes all of $G_{L}$’s edges at once. (Before studying the next
example, the reader is invited to consider what the effect of the PBPO rule is
if $R$ and $R^{\prime}$ are replaced by $L$ and $L^{\prime}$, respectively.)

###### Example 4

Consider the following PBPO rule application

$L$$x$$y$$G_{L}$$x$$y$$x_{1}$$y_{1}$$x_{2}$$G_{K}$$x$$y$$x_{1}$$y_{1}$$x_{2}$$x^{\prime}$$x_{1}^{\prime}$$x_{2}^{\prime}$$K$$x$$y$$x^{\prime}$$R$$x$$y$$x^{\prime}$$G_{R}$$x$$y$$x^{\prime}$$x_{1}$$y_{1}$$x_{2}$$x_{1}^{\prime}$$x_{2}^{\prime}$$L^{\prime}$$x$$y$$K^{\prime}$$x$$y$$x^{\prime}$$R^{\prime}$$x$$y$$x^{\prime}$

to a host graph $G_{L}$ (the morphisms are defined in the obvious way).
Intuitively, host graph $G_{L}$ is spiralled over the pattern of $L^{\prime}$.
The pullback then duplicates all elements mapped onto $x\in V_{L^{\prime}}$
and any incident edges directed at a node mapped into $y\in V_{L^{\prime}}$.
The pushout, by contrast, affects only the image of $u:K\to G_{K}$.

The two examples show how locality of transformations cannot be enforced using
PBPO. They also illustrate how it can be difficult to characterize the class
of host graphs $G_{L}$ and adherences $\alpha$ that establish a match, even
for trivial left-hand sides. Finally, Example 4 in particular highlights an
asymmetry that we find unintuitive: if one duplicates and then merges/extends
pattern elements of $L^{\prime}$, the duplication affects all elements in the
$\alpha$-preimage of $t_{L}(L)$ (which could even consist of multiple
components), whereas the pushout affects only $u(K)\subseteq G_{K}$. In PBPO+,
by contrast, transformations of the pattern affect the pattern only, and the
overall applicability of a rule is easy to understand if the context graph is
relatively simple (e.g., as in Example 2).

######  Remark 5 ($\Gamma$-preservation)

A locality notion has been defined for PBPO called _$\Gamma$ -preservation_
[2]. $\Gamma$ is some subobject of $L^{\prime}$, and a rewrite step
${G_{L}}\Rightarrow_{\mathrm{PBPO}}^{\rho,(m,\alpha)}{G_{R}}$ is said to be
_$\Gamma$ -preserving_ if the $\alpha:G_{L}\to L^{\prime}$ preimage of
$\Gamma\subseteq L^{\prime}$ is preserved from $G_{L}$ to $G_{R}$ (roughly
meaning that this preimage is neither modified nor duplicated). Similarly, a
rule is $\Gamma$-preserving if the rewrite steps it gives rise to are
$\Gamma$-preserving. If one chooses $\Gamma$ to be the context graph (the
right component) of $L^{\prime}$ in Example 3, then the rule, interpreted as a
PBPO rule, is $\Gamma$-preserving. Nonetheless, PBPO does not prevent the
mapping of arbitrarily large parts of the context graph of $G_{L}$ onto the
image of $t_{L}$ (in Example 3, the left component of $L^{\prime}$) which
usually _is_ modified. In this sense, the rule can still give rise to nonlocal
effects.

##  5 PBPO+ as a Unifying Theory for Quasitoposes

For this section, we need the following vocabulary.

###### Definition 10

Let $\mathcal{F}$, $\mathcal{G}$ be rewriting formalisms. We write
$\mathcal{F}\prec_{\textbf{C}}\mathcal{G}$ (or $\mathcal{F}\prec\mathcal{G}$
if C is clear from context) to denote that in category C, for any
$\mathcal{F}$ rule $\rho$, there exists a $\mathcal{G}$ rule $\tau$ such that
${\Rightarrow^{\rho}_{\mathcal{F}}}={\Rightarrow^{\tau}_{\mathcal{G}}}$. If
$\mathcal{F}\prec_{\textbf{C}}\mathcal{G}$ holds, then we say that
_$\mathcal{G}$ models $\mathcal{F}$ in C_. Similarly, we say that an
$\mathcal{F}$ rule $\rho$ can be _modeled by a class_ of $\mathcal{G}$-rules
$S$ if equation

${\Rightarrow_{\mathcal{F}}^{\rho}}\;=\;{\bigcup_{\tau\in
S}\,{\Rightarrow_{\mathcal{G}}^{\tau}}}$

holds.

Some of the most well-known graph rewriting formalisms include DPO [8], SPO
[14], SqPO [15] and AGREE [5, 7]. In the conference version of this paper [9],
we conjectured that in Graph and with monic matching, which implies conflict-
freeness of SPO matches,

PBPO+$\text{SPO}\prec\text{SqPO}\prec\text{AGREE}$DPOPBPO$\prec$$\prec$$\prec$
(1)

holds, and that the other comparisons do not hold. In this diagram, the claims
AGREE $\prec$ PBPO+ and DPO $\prec$ PBPO+ were the two open ones: the claim
PBPO $\prec$ PBPO+ was established in the conference paper for toposes [9,
Lemma 32] (and thus in particular for Graph), and SPO $\prec$ SqPO [15,
Proposition 13] and SqPO $\prec$ AGREE [5, Theorem 2] were known for
categories more general than Graph in the literature.

The main contribution of this section is that we establish Diagram (1) (but
without SPO: see Remark 6 below) much more generally: namely, for C any
quasitopos, and assuming regular monic matching (Theorem 5.4). Of these
claims, only SqPO $\prec$ AGREE follows as a corollary of the previously cited
theorem [5, Theorem 2]. Quasitoposes include not only the categories of sets,
directed multigraphs [4] and typed graphs [5] (all of which are toposes), but
also a variety of structures such as Heyting algebras (considered as
categories) [3], and the categories of simple graphs (equivalently, binary
relations) [6], fuzzy sets [3], algebraic specifications [6] and safely marked
Petri Nets [6]. Behr et al. [16] recently proposed quasitoposes as a natural
setting for non-linear rewriting.

This section is structured as follows. In Section 5.1 we provide all the
required definitions and results pertaining to quasitoposes. We then first
prove a useful sufficient condition for determinism of PBPO+ rules in Section
5.2. This result is independent of the main result of this section. Next, we
work towards the main result, establishing PBPO $\prec$ PBPO+, AGREE $\prec$
PBPO+ and DPO $\prec$ PBPO+ for quasitoposes in Sections 5.3, 5.4 and 5.5,
respectively.

######  Remark 6 (Modeling SPO)

Deciding SPO $\prec$ PBPO+ for quasitoposes (with regular monic matching)
appears relatively involved due to the fact that SPO is defined for partial
morphisms, rather than total ones. For this reason, we consider the question
to be beyond the scope of the present paper. However, we conjecture that for
any SPO rule, which is a partial morphism $\rho:L\rightharpoonup R$, the PBPO+
rule

${\boldsymbol{L}}$${\boldsymbol{K}}$${\boldsymbol{R}}$${T(L)}$${T(K)}$$\scriptstyle{\eta_{L}}$$\scriptstyle{\eta_{K}}$$\scriptstyle{\boldsymbol{l}}$$\scriptstyle{\boldsymbol{r}}$${\mathrm{PB}}$$\scriptstyle{\varphi(\eta_{K},l)}$

models it, where the top span is the span representation of $\rho$ (Definition
12), and the hooked arrows $\hookrightarrow$ are regular monomorphisms. For
the meaning of the given pullback square, see the $\mathcal{M}$-partial map
classifier definition (Definition 13).

######  Remark 7 (Double Pullback Rewriting)

There also exists the double pullback rewriting (DPU) approach by Bauderon
[17] and Bauderon and Jacquet [18]. As a first approximation, a double
pullback rule $\rho$ is of the form $L\stackrel{{\scriptstyle
l}}{{\to}}A\stackrel{{\scriptstyle r}}{{\leftarrow}}R$; a match is a morphism
$m:G\to L$; and a step from $G$ to $H$ is given by a diagram

${G}$${D}$${H}$${L}$${A}$${R}$$\scriptstyle{m}$$\scriptstyle{q}$${\mathrm{PB}}$$\scriptstyle{u}$${\mathrm{PB}}$$\scriptstyle{l}$$\scriptstyle{r}$

where $(q,u)$ is a _pullback complement_. On top of this, constraints on
rules, occurrences and steps are added in order to make the method well-
behaved. The constraints are rather technical and vary slightly between [17]
and [18].

We have provided a detailed comparison between PBPO+ and DPU in a recent PBPO+
tutorial [10]. The most relevant conclusion is that although DPU uses
pullbacks (which are generic), the details are defined for slice categories of
simple graphs [18, Definition 3], and it is not clear to what extent these can
be generalized (let alone be generalized to (quasi)toposes). So it is not
evident how DPU can be fit into the general picture.

###  5.1 Quasitoposes

The following definitions on $\mathcal{M}$-partial map classification derive
from work by Cockett and Lack on restriction categories [19, 20], but we
follow the presentations of Corradini et al. [5] and Behr et al. [16].

######  Definition 11 (Stable System of Monics [19])

A _stable system of monics_ $\mathcal{M}$ in C is a class of monos in C that
includes all isomorphisms, is closed under composition
(${m,m^{\prime}\in\mathcal{M}}\implies{m\circ m^{\prime}\in\mathcal{M}}$) and
is stable under pullback, i.e., if

${A}$${C}$${B}$${D}$$\scriptstyle{m^{\prime}}$$\scriptstyle{f^{\prime}}$$\scriptstyle{f}$$\scriptstyle{m}$

is a pullback and $m\in\mathcal{M}$, then $m^{\prime}\in\mathcal{M}$.

We use $\hookrightarrow$ to denote $\mathcal{M}$-monos.

Examples of stable systems of monics in any category include the class of all
monos and the class of all isomorphisms.

Consider how in set theory, any partial function $g:A\rightharpoonup B$ with
domain $A^{\prime}\subseteq A$ can be represented by a total injective
function $m:X\rightarrowtail A$ (typically an inclusion) and total function
$f:X\to B$ such that $m(X)=A^{\prime}$ and $f(x)=g(m(x))$ for all $x\in X$.
The following definition is the categorical generalization of this idea.

######  Definition 12 ($\mathcal{M}$-Partial Map)

Let $\mathcal{M}$ be a stable system of monics. An _$\mathcal{M}$ -partial
map_ is a span $A\stackrel{{\scriptstyle
m}}{{\hookleftarrow}}X\stackrel{{\scriptstyle f}}{{\to}}B$ where
$m\in\mathcal{M}$.

Alternatively in set theory, one can extend set $B$ to
$B_{\star}=B\uplus\\{\star\\}$, where $\star$ represents undefined elements.
Then any partial map $g:A\rightharpoonup B$ with domain $A^{\prime}\subseteq
A$ is represented by the total function $g_{\star}:A\to B_{\star}$ satisfying
$g_{\star}(x)=g(x)$ for $x\in A^{\prime}$, and $g_{\star}(x)=\star$ for
$x\notin A^{\prime}$. This extension is minimal in the sense that
$g_{\star}:A\to B_{\star}$ is uniquely defined by $g_{\star}(x)=g(x)$ for
$x\in A^{\prime}$, and $g_{\star}(x)\notin B$ for $x\notin A^{\prime}$. The
following definition is the categorical generalization of this idea.

######  Definition 13 ($\mathcal{M}$-Partial Map Classifier [5])

Let $\mathcal{M}$ be a stable system of monics in C. An _$\mathcal{M}$
-partial map classifier_ $(T,\eta)$ in C consists of a functor
$T:{\textbf{C}}\to{\textbf{C}}$ and a natural transformation
$\eta:\mathrm{1}_{{\textbf{C}}}\to T$ such that

  * •

for all objects $X\in\mathrm{Obj}({\textbf{C}})$, $\eta_{X}:X\to T(X)$ is in
$\mathcal{M}$; and

  * •

for each _$\mathcal{M}$ -partial map_, i.e., span $A\stackrel{{\scriptstyle
m}}{{\hookleftarrow}}X\stackrel{{\scriptstyle f}}{{\to}}B$ with
$m\in\mathcal{M}$, there exists a unique morphism $\varphi(m,f):A\to T(B)$
making

${X}$${B}$${A}$${T(B)}$$\scriptstyle{m}$$\scriptstyle{f}$$\scriptstyle{\eta_{B}}$$\scriptstyle{\varphi(m,f)}$

a pullback square.

For $\mathcal{M}$-morphisms $m:X\hookrightarrow A$, we let $\overline{m}$
denote $\varphi(m,\mathrm{1}_{X}):A\to T(X)$.

###### Example 5

As explained in the running text above, in Set there exists a mono-partial map
classifier $(T,\eta)$ with $T(B)=B\uplus\\{\star\\}$ and $\eta_{B}$ the
inclusion.

In the category of unlabeled directed graphs, there exists a mono-partial map
classifier $(T,\eta)$, for graphs $G=(V,E,s,t)$ so that
$T(G)=(V_{\star},E_{\star},s_{\star},t_{\star})$ where
$V_{\star}=V\uplus\\{\star\\}$; $E_{\star}=E\uplus(V_{\star}\times
V_{\star})$; $s_{\star}(e)=s(e)$ if $e\in E$ and $\pi_{1}(e)$ otherwise; and
$t_{\star}(e)=t(e)$ if $e\in E$ and $\pi_{2}(e)$ otherwise ($\pi_{i}$ the
$i$’th projection). An example is given by

$G\;=$ ${v}$${w}$ and $T(G)\;=$ ${v}$${w}$${\star}$,

where the dotted edges represent the edges $e\in V_{\star}\times V_{\star}$.
It can be seen that for any partial homomorphism $\psi:H\to G$ defined on
subgraph $H^{\prime}\subseteq H$, there exists exactly one homomorphism
$\psi_{\star}:H\to T(G)$ such that $\psi_{\star}(x)=\psi(x)$ for $x\in
V_{H^{\prime}}\cup E_{H^{\prime}}$ and $\psi_{\star}(x)\notin V_{G}\cup E_{G}$
for $x\notin V_{H^{\prime}}\cup E_{H^{\prime}}$. Equivalently, $\psi_{\star}$
is the unique morphism $\varphi(m,f):H\to T(G)$ making

${H^{\prime}}$${G}$${H}$${T(G)}$$\scriptstyle{m}$$\scriptstyle{f}$$\scriptstyle{\eta_{G}}$$\scriptstyle{\varphi(m,f)}$

a pullback square, where $H\stackrel{{\scriptstyle
m}}{{\hookleftarrow}}H^{\prime}\stackrel{{\scriptstyle f}}{{\to}}G$ a partial
map span representation of $\psi$, and $\eta_{G}$ and $m$ are inclusions.

The generalization to labeled graphs is straightforward: between any two nodes
$u,v\in V_{\star}$ and $l\in\mathcal{L}$, there is one $l$-labeled edge
representing an undefined $l$-edge between $u$ and $v$.

The following two definitions are standard in algebraic graph rewriting.

######  Definition 14 ($\mathcal{M}$-Van Kampen Square [21, Definition 2.3.2])

Let $\mathcal{M}$ be a class of monomorphisms in a category C. A pushout along
$m\in\mathcal{M}$ is an _$\mathcal{M}$ -Van Kampen_ (_VK_) _square_ if,
whenever it lies at the bottom of a commutative cube

${F}$${G}$${E}$${H}$${B}$${C}$${A}$${D}$$\scriptstyle{m}$

where the vertical back faces are pullbacks and all vertical arrows are in
$\mathcal{M}$, the top face is a pushout iff the vertical front faces are
pullbacks.

######  Definition 15 ($\mathcal{M}$-Adhesive Category [21, Definition 2.4])

Let $\mathcal{M}$ be a class of monomorphisms in a category C. C is
_$\mathcal{M}$ -adhesive_ (also known as _vertical weak adhesive HLR_) if

  * •

C has pushouts along $\mathcal{M}$-morphisms;

  * •

C has pullbacks along $\mathcal{M}$-morphisms;

  * •

pushouts along $\mathcal{M}$-morphisms are $\mathcal{M}$-VK squares; and

  * •

$\mathcal{M}$ contains all isomorphisms and is closed under composition,
pullback and pushout.

######  Lemma 3 ([4, Lemma 13])

If C is $\mathcal{M}$-adhesive for a class of monomorphisms $\mathcal{M}$,
then pushouts along $\mathcal{M}$-morphisms are pullbacks. ∎

Recall that a monomorphism is _regular_ if it is an equalizer for a parallel
pair of morphisms. We write $\mathrm{rm}({\textbf{C}})$ to denote the class of
regular monomorphisms of a category C.

######  Definition 16 (Quasitopos [3, 22, 23])

A category C is a _quasitopos_ if it has all finite limits and colimits, it is
locally cartesian closed, and it has a regular-subobject classifier.

In this paper we rely on various results about quasitoposes: the notions of
local cartesian closure and regular-subobject classifier will not be used
directly, and therefore need not be understood. We could have equivalently
defined quasitoposes in terms of regular-partial map classifiers and
additional properties [22, 3], but because these definitions appear less
standardized, we decided against it.

The following results for quasitoposes will be used throughout the section. We
cite original sources, but stress our indebtedness to the summary provided by
Behr et al. [16, Corollary 1].

######  Proposition 4 (Properties of Quasitoposes)

A quasitopos C

  1. 1.

has a stable system of monics $\mathcal{M}=\mathrm{rm}({\textbf{C}})$ [22,
Corollary 28.6(3) and Proposition 28.3(2)];

  2. 2.

has an $\mathcal{M}$-partial map classifier [3, Definition 19.3];

  3. 3.

satisfies
${gf\in\mathrm{rm}({\textbf{C}})}\implies{f\in\mathrm{rm}({\textbf{C}})}$ for
all morphisms $f$ and $g$ [22, Proposition 7.62(2) and Corollary 28.6(2)];

  4. 4.

is partial map adhesive [24, Lemma 13] and thus $\mathcal{M}$-adhesive [21,
Theorems 3.4 and 3.6];

  5. 5.

is rm-quasiadhesive [25, Definition 1.1], meaning that pushouts along regular
monos exist, and that these pushouts along regular monos are pullbacks and are
stable under pullback;

  6. 6.

has unique epi-$\mathcal{M}$ factorizations for every morphism [22,
Proposition 28.10], i.e., every $f:A\to B$ factors uniquely as
$A\stackrel{{\scriptstyle e}}{{\twoheadrightarrow}}C\stackrel{{\scriptstyle
m}}{{\hookrightarrow}}B$ (up to isomorphism in $C$), where $e$ is epic and $m$
regular monic; and

  7. 7.

is stable under slicing, i.e., every slice category ${\textbf{C}}/X$ (for
$X\in\mathrm{Obj}({\textbf{C}})$) is a quasitopos [3, Theorem 19.4].

∎

We will also need the following basic result, valid in any category.

######  Proposition 5 ([22, Corollary 7.63 and Proposition 7.66]))

An epimorphism that is a regular monomorphism is an isomorphism. ∎

Many categories of interest are toposes. We close this subsection by giving
some relevant examples of non-topos quasitoposes.

######  Example 6 (Simple Graphs)

The category of simple graphs SimpleGraph has pairs of sets $G=(V,E)$ with
$E\subseteq V\times V$ as objects, and the usual graph homomorphisms $\psi$ as
arrows. SimpleGraph is not a topos, but it is a quasitopos (see, e.g., [16,
Section 2.1]). The regular monos of SimpleGraph are injective homomorphisms
that reflect edges (i.e., for regular monos $\psi:G\hookrightarrow H$,
$(\psi(v),\psi(w))\in E_{H}$ implies $(v,w)\in E_{G}$). A modeling example
using simple graphs can be found in [15, Section 3]. The regular-mono partial
map classifier $(T,\eta)$ for SimpleGraph sends simple graphs $G=(V,E)$ to
$T(G)=(V\uplus\\{\star\\},E\cup(V\times\\{\star\\})\cup(\\{\star\\}\times
V)\cup\\{(\star,\star)\\})$, with $\eta_{G}:G\hookrightarrow T(G)$ the
inclusion [22, Exercise 28.2(3)].

######  Definition 17 (Complete Lattice)

A _complete lattice_ $(\mathcal{L},\leq)$ is a poset such that all subsets $S$
of $\mathcal{L}$ have a supremum (join) $\bigvee S$ and an infimum (meet)
$\bigwedge S$. Any complete lattice has a global maximum $\top$ and global
minimum $\bot$, respectively.

A complete lattice $\mathcal{L}$ is _infinitely distributive_ if

$x\wedge(\bigvee_{y\in S}y)\quad=\quad\bigvee_{y\in S}(x\wedge y)$

holds for all $x\in\mathcal{L}$ and $S\subseteq\mathcal{L}$.

Observe that pullbacks and pushouts in a complete lattice, considered as a
category, correspond to meets and joins, respectively.

######  Example 7 (Infinitely Distributive Complete Lattice)

A complete lattice $\mathcal{L}$ considered as a category is a quasitopos iff
$\mathcal{L}$ is infinitely distributive [22, Exercise, 28D.(b)]. Such
complete lattices are exactly the complete Heyting algebras.

The regular monos in a complete Heyting algebra $\mathcal{L}$ are exactly the
identities. So the regular mono-partial map classifier is not very
interesting. However, some toposes can be endowed with a complete Heyting
algebra as in the following definition, which gives rise to more interesting
classifiers.

######  Example 8 ($\mathcal{L}$-Fuzzy Set [3, Chapter 8],[26])

An _$\mathcal{L}$ -fuzzy set_ $(A,\alpha)$ consists of a set $A$ and a
membership function $\alpha:A\to\mathcal{L}$, where $\mathcal{L}$ is a
complete lattice. An $\mathcal{L}$-fuzzy set morphism from $(A,\alpha)$ to
$(B,\beta)$ is a function $\phi:A\to B$ such that
$\alpha(x)\leq\beta\circ\phi(x)$ for all $x\in A$. $\mathcal{L}$-fuzzy sets
have been well studied, in particular in the context of fuzzy logics.

The regular monomorphisms in the category of $\mathcal{L}$-fuzzy sets are the
$\mathcal{L}$-fuzzy set morphisms $\phi$ that preserve membership (i.e.,
$\alpha(x)=\beta\circ\phi(x)$). The category of $\mathcal{L}$-fuzzy sets is
known to be a quasitopos if $\mathcal{L}$ is a complete Heyting algebra (see
Stout [27, Corollary 8] and Goguen [26, Proposition 4]). The regular mono-
partial map classifier $(T,\eta)$ then sends sets $S=(A,\alpha)$ to
$T(S)=(A\uplus\\{\star\\},\alpha\cup\\{(\star\mapsto\top)\\})$, with
$\eta_{S}:S\hookrightarrow T(S)$ the inclusion. An example of how this can be
used to redefine the membership of an element using PBPO+ is given by

${\\{a^{x}\\}}$${\\{a^{\bot}\\}}$${\\{a^{u}\\}}$${{\\{a^{x},b^{y},c^{z}\\}}}$${{\\{a^{\bot},b^{y},c^{z}\\}}}$${{\\{a^{u},b^{y},c^{z}\\}}}$${{\\{a^{x},\star^{\top}\\}}}$${{\\{a^{\bot},\star^{\top}\\}}}$$\scriptstyle{m}$$\scriptstyle{t_{L}=\eta_{\\{x\\}}}$$\scriptstyle{l}$$\scriptstyle{u}$$\scriptstyle{r}$${\mathrm{PB}}$${\mathrm{PO}}$$\scriptstyle{w}$$\scriptstyle{\alpha}$$\scriptstyle{g_{L}}$$\scriptstyle{u^{\prime}}$$\scriptstyle{g_{R}}$${\mathrm{PB}}$$\scriptstyle{l^{\prime}}$

where $a,b,c,\star$ are set elements, and superscripts denote membership
values in $\mathcal{L}$. Morphisms $\alpha$ and $u^{\prime}$ map $b$ and $c$
onto $\star$; all other elements are mapped by way of inclusion. The rule can
be seen to change the fuzziness of an element with fuzziness $x$ to $u$, in
any context. The context is not changed.

Rewriting fuzzy sets is only slightly more interesting than rewriting sets.
But in Section 6, we define the category Graph(L,≤), which is essentially the
category of “fuzzy graphs” (Example 8), and argue that it is a very useful
graph category for modeling and relabeling. We have proven very recently that
this category is a quasitopos if $\mathcal{L}$ is a complete Heyting algebra
[28].

###  5.2 Determinism

For this subsection, we need the following definition.

###### Definition 18

A PBPO+ rule $\rho$ is _deterministic in a category C_ if

${{G_{L}}\Rightarrow_{\mathrm{PBPO}^{+}}^{\rho,(m,\alpha)}{G_{R}}\;\text{ and
}\;{G_{L}}\Rightarrow_{\mathrm{PBPO}^{+}}^{\rho,(m,\beta)}{G_{R}^{\prime}}}\qquad\Longrightarrow\qquad{G_{R}\cong
G_{R}^{\prime}}$

for any $G_{L},G_{R},G_{R}^{\prime}\in\mathrm{Obj}({\textbf{C}})$, match
morphism $m:L\to G_{L}$ and adherence morphisms $\alpha,\beta:G_{L}\to
L^{\prime}$.

By uniqueness of (co)limits, it is easy to see that in any category C, PBPO+
rewriting is deterministic, if, for any match morphism $m:L\to G_{L}$, there
exists at most one adherence morphism $\alpha:G_{L}\to L^{\prime}$ that
establishes a strong match square. In the setting where C is a quasitopos, we
define the following concept, which we can use to prove a more useful
sufficient condition on the type morphism $t_{L}$.

######  Definition 19 (Restricted Classifier)

Let C be a quasitopos. A regular mono $t_{L}:L\hookrightarrow L^{\prime}$ is a
_restricted classifier_ if

${L}$${L^{\prime}}$${T(L)}$$\scriptstyle{\eta_{L}}$$\scriptstyle{t_{L}}$$\scriptstyle{s}$

commutes for some mono $s:L^{\prime}\rightarrowtail T(L)$.

###### Example 9

Recall $G$ and $T(G)$ from Example 5. Let $G^{\prime}$ be a graph resulting
from deleting any number of dotted edges (and possibly $\star$) from $T(G)$,
e.g.,

$G^{\prime}\;=$ ${v}$${w}$${\star}$.

The inclusion $G\hookrightarrow G^{\prime}$ is a restricted classifier. The
$t_{L}$ of Example 1 is also a restricted classifier.

Recall the regular mono-partial map classifier $(T,\eta)$ for
$\mathcal{L}$-fuzzy sets, with $\mathcal{L}$ a complete Heyting algebra
(Example 8), which sends fuzzy sets $S=(A,\alpha)$ to
$T(S)=(A\uplus\\{\star\\},\alpha\cup\\{(\star\mapsto\top)\\})$, with
$\eta_{S}:S\hookrightarrow T(S)$ the inclusion. The inclusion
$(A,\alpha)\hookrightarrow(A\uplus\\{\star\\},\alpha\cup\\{\star\mapsto x\\})$
for $x<\top$ is a restricted classifier, and effectively sets the upper bound
for context elements to $x$ instead of $\top$. Upper bounds for context
elements can similarly be changed for fuzzy graphs (Section 6).

######  Proposition 6 ([7, Lemma 3.2])

Any commuting square of the form

${A}$${A}$${B}$${C}$$\scriptstyle{g}$$\scriptstyle{h}$$\scriptstyle{f}$

is a pullback. ∎

###### Proposition 7

Let C be a quasitopos. For any regular mono $t_{L}$, $t_{L}$ is a restricted
classifier iff $\overline{t_{L}}$ (Definition 13) is monic.

###### Proof

For direction $\Longrightarrow$, use Proposition 6 and the uniqueness property
of partial map classifiers to conclude that the obtained mono $s$ is
$\overline{t_{L}}$. Direction $\Longleftarrow$ is immediate. ∎

###### Lemma 4

Let C be a quasitopos, and let $L\stackrel{{\scriptstyle
t_{L}}}{{\hookrightarrow}}L^{\prime}$ and $L\stackrel{{\scriptstyle
m}}{{\hookrightarrow}}G_{L}$ be given. If $t_{L}$ is a restricted classifier,
then any $\alpha:G_{L}\to L^{\prime}$ making

${L}$${L}$${G_{L}}$${L^{\prime}}$$\scriptstyle{m}$$\scriptstyle{t_{L}}$$\scriptstyle{\alpha}$

a pullback square is unique.

###### Proof

Let $\alpha$ and $\beta$ each make the left square of

${L}$${L}$${L}$${G_{L}}$${L^{\prime}}$${T(L)}$$\scriptstyle{m}$$\scriptstyle{t_{L}}$${\mathrm{PB}}$$\scriptstyle{\eta_{L}}$$\scriptstyle{\alpha}$$\scriptstyle{\beta}$$\scriptstyle{\overline{t_{L}}}$

a pullback square. Because the right square is a pullback square, both
$\overline{t_{L}}\alpha$ and $\overline{t_{L}}\beta$ make the outer square a
pullback square, using the pullback lemma. By the uniqueness property of the
partial map classifier, $\overline{t_{L}}\alpha=\overline{t_{L}}\beta$. By
monicity of $\overline{t_{L}}$, $\alpha=\beta$. ∎

######  Definition 20 (Classifying PBPO+ Rule)

A PBPO+ rule $\rho$ is said to be _classifying_ if $L\stackrel{{\scriptstyle
t_{L}}}{{\hookrightarrow}}L^{\prime}$ is a restricted classifier.

We can now state the following sufficient condition.

######  Theorem 5.1 (Determinism)

Let C be a quasitopos, and let $\rho$ be a classifying PBPO+ rule. If both
${{G_{L}}\Rightarrow_{\mathrm{PBPO}^{+}}^{\rho,(m,\alpha)}{G_{R}}}$ and
${{G_{L}}\Rightarrow_{\mathrm{PBPO}^{+}}^{\rho,(m,\beta)}{G_{R}^{\prime}}}$,
then $\alpha=\beta$ and $G_{R}\cong G_{R}^{\prime}$.

###### Proof

From Lemma 4 and general pullback and pushout properties. ∎

Note that in categories with strict initial objects (such as Set and Graph),
another sufficient condition for determinism is having $K^{\prime}$ initial.
Then the result of any rewrite step is $R$. This observation implies that
necessary conditions for determinism cannot be phrased merely in terms of type
graphs and matching.

###### Remark 8

For some categories, we conjecture that a sufficient condition for determinism
of a rule $\rho$ (with type morphism $t_{L}:L\rightarrowtail L^{\prime}$) is
the case where there exists a commuting diagram

${L}$${L^{\prime\prime}}$${T(L)}$${L^{\prime}}$$\scriptstyle{x}$$\scriptstyle{\eta_{L}}$$\scriptstyle{t_{L}}$$\scriptstyle{\overline{x}}$$\scriptstyle{f}$

for some restricted classifier $x:L\hookrightarrow L^{\prime\prime}$, and
monic and epic morphism $f:L^{\prime\prime}\to L^{\prime}$. For instance, in
category Graph(L,≤) (Section 6), this property corresponds to relaxing the
labels of a restricted classifier $x:L\hookrightarrow L^{\prime\prime}$. We
are interested in knowing in which classes of categories this property holds.

###  5.3 PBPO+ Models PBPO

In the conference version of the present paper, we proved that in any topos,
any PBPO rule can be modeled by a class of PBPO+ rules [9, Corollary 1]. In
this subsection, we generalize this result to the setting of quasitoposes (any
topos is a quasitopos). Additionally, we streamline the original proof
significantly.

In order to prove our result, we first need to establish a technical result
about slice categories ${\textbf{C}}/X$. We let $(A,f:A\to X)$ denote the
objects of ${\textbf{C}}/X$; and $U_{X}$ the forgetful functor
$U_{X}:{\textbf{C}}/X\to{\textbf{C}}$.

######  Proposition 8 ([3, (17.3, Remarks)])

Let $f$ be a morphism in ${\textbf{C}}/X$. We have

  1. 1.

$f$ is monic $\iff$ $U_{X}f$ is monic;

  2. 2.

if C has finite products, then: $f$ is epic $\iff$ $U_{X}f$ is epic; and

  3. 3.

if $f$ is a regular mono, then $U_{X}f$ is a regular mono.

∎

Wyler additionally remarks the following for categories C with finite
products: if a morphism $U_{X}f:A\to X$ is a regular mono in C, then the
morphism $f:(A,f)\to(X,\mathrm{1}_{X})$ is a regular mono in ${\textbf{C}}/X$
[3, (17.3, Remarks)]. We prove that $U_{X}$ in fact _reflects_ all regular
monomorphisms, i.e., that if $U_{X}f$ is a regular mono (with any codomain) in
C, then so is $f$ in ${\textbf{C}}/X$ (Corollary 2 below).

Let $A\stackrel{{\scriptstyle f}}{{\leftarrow}}C\stackrel{{\scriptstyle
g}}{{\to}}B$ be a span in a category with finite products. Recall that the
_product map_ $\langle f,g\rangle:C\to A\times B$ is the unique morphism
induced by the universal property of product $A\times B$.

######  Proposition 9 ([29, (Exercises 2–3, Chapter 3)])

Product maps satisfy

  1. 1.

${\langle f,g\rangle=\langle k,h\rangle}\Longleftrightarrow{f=k\text{ and
}g=h}$; and

  2. 2.

$\langle fh,gh\rangle=\langle f,g\rangle h$.

∎

###### Proposition 10

Assume C has finite products. An equalizer $f:A\to B$ for parallel morphisms
$g,h:B\to C$ is also an equalizer for the product maps $\langle
1_{B},g\rangle,\langle 1_{B},h\rangle:B\to B\times C$.

###### Proof

First, $gf=hf\implies\langle 1_{B}f,gf\rangle=\langle
1_{B}f,hf\rangle\implies\langle 1_{B},g\rangle f=\langle 1_{B},h\rangle f$
using Proposition 9. For universality, suppose $f^{\prime}:A^{\prime}\to B$
also has this equalizing property. Then $\langle 1_{B},g\rangle
f^{\prime}=\langle 1_{B},h\rangle f^{\prime}\implies\langle
1_{B}f^{\prime},gf^{\prime}\rangle=\langle
1_{B}f^{\prime},hf^{\prime}\rangle\implies gf^{\prime}=hf^{\prime}$, again
using Proposition 9. We then obtain the unique $u:A^{\prime}\to A$ such that
$fu=f^{\prime}$ from the fact that $f$ is an equalizer for $g$ and $h$. In a
diagram:

${A^{\prime}}$${C}$${A}$${B}$${B\times
C}$$\scriptstyle{!u}$$\scriptstyle{f^{\prime}}$$\scriptstyle{f}$$\scriptstyle{g}$$\scriptstyle{\langle
1_{B},g\rangle}$$\scriptstyle{\langle 1_{B},h\rangle}$$\scriptstyle{h}$

∎

###### Proposition 11

Let $f:(A,a)\to(B,b)$ and $g,h:(B,b)\to(C,c)$ be morphisms in
${\textbf{C}}/X$. If $U_{X}f$ is an equalizer for $U_{X}g,U_{X}h$ in C, then
$f$ is an equalizer for $g,h$ in ${\textbf{C}}/X$.

###### Proof

First, $gf=hf$ in ${\textbf{C}}/X$ because $U_{X}f$ is an equalizer for
$U_{X}g,U_{X}h$ in C, and composition is lifted from C. For universality,
suppose $gf^{\prime}=hf^{\prime}$ for some
$f^{\prime}:(A^{\prime},a^{\prime})\to(B,b)$ in ${\textbf{C}}/X$. By
definition of the slice category and its forgetful functor, $a^{\prime}=b\circ
U_{X}f^{\prime}$ in C. In addition, because composition is lifted from C,
$U_{X}g\circ U_{X}f^{\prime}=U_{X}h\circ U_{X}f^{\prime}$, and so one obtains
a unique arrow $u:A^{\prime}\to A$ with $U_{X}f\circ u=U_{X}f^{\prime}$ using
that $U_{X}f$ is an equalizer in C. Then $a^{\prime}=b\circ
U_{X}f^{\prime}=b\circ U_{X}f\circ u$ which implies $a^{\prime}=b\circ f\circ
u=a\circ u$. Hence $u:(A^{\prime},a^{\prime})\to(A,a)$ is an arrow in
${\textbf{C}}/X$. Uniqueness in ${\textbf{C}}/X$ follows because any other
arrow would violate the uniqueness property on the level of C.

In a diagram, where solid and dashed arrows represent respectively objects and
morphisms in ${\textbf{C}}/X$:

${A^{\prime}}$${A}$${B}$${C}$${X}$$\scriptstyle{a^{\prime}}$$\scriptstyle{f^{\prime}}$$\scriptstyle{!u}$$\scriptstyle{f}$$\scriptstyle{a}$$\scriptstyle{g}$$\scriptstyle{h}$$\scriptstyle{b}$$\scriptstyle{c}$

∎

###### Proposition 12

If C has finite products and $U_{X}f:A\to B$ is an equalizer for $g,h:B\to C$
in C, then $f$ is an equalizer for $\langle 1_{B},g\rangle,\langle
1_{B},h\rangle:(B,b)\to(B\times C,b\circ\pi_{1})$ in ${\textbf{C}}/X$.

###### Proof

Observe that morphisms $g$ and $h$ may not give rise to morphisms in
${\textbf{C}}/X$. However, by hypothesis, we can construct the product
$B\times C$ in C. From this we can infer the morphism $b\circ\pi_{1}:B\times
C\to X$ and the product maps $\langle 1_{B},g\rangle,\langle
1_{B},h\rangle:B\to B\times C$. Crucially, $b\circ\pi_{1}$ is an object in
${\textbf{C}}/X$ and the product maps are morphisms in ${\textbf{C}}/X$,
because $b\circ\pi_{1}\circ\langle 1_{B},g\rangle=b=b\circ\pi_{1}\circ\langle
1_{B},h\rangle$.

${{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color<EMAIL_ADDRESS>C}$${X}$$\scriptstyle{f}$$\scriptstyle{a}$$\scriptstyle{b}$$\scriptstyle{\langle
1_{B},g\rangle}$$\scriptstyle{\langle
1_{B},h\rangle}$$\scriptstyle{\definecolor[named]{.}{rgb}{.5,.5,.5}\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}g}$$\scriptstyle{\definecolor[named]{.}{rgb}{.5,.5,.5}\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color<EMAIL_ADDRESS>
By Proposition 10, $U_{X}f$ is an equalizer for the product maps in C. By
Proposition 11, $f$ is an equalizer for the product maps in ${\textbf{C}}/X$.
∎

###### Corollary 2

If C has finite products and $X\in\mathrm{Obj}(C)$, then $U_{X}$ reflects
regular monomorphisms.

###### Proof

Let $U_{X}f:A\to B$ be a regular monomorphism in C. By definition this means
$U_{X}f$ is an equalizer for some $g,h:B\to C$ in C. By Proposition 12, $f$ is
an equalizer for $\langle 1_{B},g\rangle,\langle
1_{B},h\rangle:(B,b)\to(B\times C,b\circ\pi_{1})$ in ${\textbf{C}}/X$. So by
definition $f$ is a regular monomorphism. ∎

The definition below generalizes the concept of materialization by Corradini
et al. [30, Definition 7], by replacing the class of all monics by a stable
system of monics $\mathcal{M}$. (For an example of a materialization and how
to construct it, see [30, Corollary 9 and Example 10].)

######  Definition 21 ($\mathcal{M}$-Materialization)

Let $\mathcal{M}$ be a stable system of monics. The _$\mathcal{M}$
-materialization_ of a morphism $f:A\to B$ is a terminal factorization of the
form $A\stackrel{{\scriptstyle f^{\prime}}}{{\hookrightarrow}}{\langle
f\rangle}\stackrel{{\scriptstyle f^{\prime\prime}}}{{\to}}B$ for some object
${\langle f\rangle}$. That is, for any other factorization of the form
$A\stackrel{{\scriptstyle
m}}{{\hookrightarrow}}C\stackrel{{\scriptstyle\alpha}}{{\to}}B$, there exists
a unique morphism $\beta:C\to{\langle f\rangle}$ that makes the square of

${A}$${C}$${B}$${A}$${{\langle
f\rangle}}$$\scriptstyle{f}$$\scriptstyle{m}$$\scriptstyle{\alpha}$$\scriptstyle{!\beta}$$\scriptstyle{f^{\prime}}$${\mathrm{PB}}$$\scriptstyle{f^{\prime\prime}}$

a pullback square, and moreover makes the triangle commute.

For $\mathcal{M}$ the class of all monics, Corradini et al. have shown that
all morphisms have mono-materializations if all slice categories have mono-
partial map classifiers [30, Proposition 8]. This condition holds in any
topos. The following proposition and corollary generalize their result.

###### Proposition 13

If all slice categories ${\textbf{C}}/X$ of a category C have
$\mathcal{M}$-partial map classifiers and the forgetful functor
$U_{X}:{\textbf{C}}/X\to C$ reflects and preserves $\mathcal{M}$-morphisms,
then C has all $\mathcal{M}$-materializations.

###### Proof

The proof is analogous to the proof of Corradini et al. for $\mathcal{M}$ the
class of all monos, available on arXiv [31]. The difference is that we require
reflection and preservation of $\mathcal{M}$-morphisms, rather than relying
implicitly on these properties for monos. ∎

###### Corollary 3

Quasitoposes C admit rm-materializations.

###### Proof

Using Corollary 2 and Proposition 13, the fact that quasitoposes have rm-
partial map classifiers, and the fact that the quasitopos property is stable
under slicing. ∎

######  Definition 22 (Compacted Rule)

Let C be a quasitopos. For any canonical PBPO rule $\rho$ and any
factorization $t_{L}=f\mathop{\circ}e$ where $e$ is epic (note that $f$ is
uniquely determined by $e$, because $e$ is right-cancellative), the _compacted
PBPO + rule_ $\rho_{e}$ is defined as the bold subdiagram of

${L}$${K}$${R}$${\boldsymbol{L_{e}}}$${\boldsymbol{K_{e}}}$${\boldsymbol{R_{e}}}$${\boldsymbol{{\langle
f\rangle}}}$${\boldsymbol{{\langle f\rangle}^{\prime}}}$${{\langle
f\rangle}^{\prime\prime}}$${L^{\prime}}$${K^{\prime}}$${R^{\prime}}$$\scriptstyle{t_{L}}$$\scriptstyle{e}$$\scriptstyle{l}$$\scriptstyle{r}$${\mathrm{PB}}$${\mathrm{PO}}$$\scriptstyle{f}$$\scriptstyle{\boldsymbol{f^{\prime}}}$${\boldsymbol{\mathrm{PB}}}$${\mathrm{PO}}$$\scriptstyle{f^{\prime\prime}}$${\mathrm{PB}}$${\mathrm{PO}}$$\scriptstyle{l^{\prime\prime}}$$\scriptstyle{r^{\prime\prime}}$

where the outer diagram is rule $\rho$, and $L_{e}\stackrel{{\scriptstyle
f^{\prime}}}{{\hookrightarrow}}{\langle f\rangle}\stackrel{{\scriptstyle
f^{\prime\prime}}}{{\to}}L^{\prime}$ the rm-materialization of $f$, and
objects ${\langle f\rangle}^{\prime}$ and ${\langle f\rangle}^{\prime\prime}$
are obtained by respectively pullback and pushout.

We additionally define the class of rules

$\mathrm{compact}(\rho)=\\{\rho_{e}\mid\exists fe.\ t_{L}=f\circ e\text{ and
$e$ is epic}\\}\text{.}$

and its subclass

$\mathrm{compact}^{\cong}(\rho)=\\{\rho_{e}\mid\exists fe.\ t_{L}=f\circ
e\text{ and $e$ is iso}\\}\text{.}$

###### Theorem 5.2

Let C be a quasitopos. For any canonical PPBO rule $\rho$ with type morphism
$t_{L}:L\to L^{\prime}$, the class of PBPO+ rules $\mathrm{compact}(\rho)$
models it, that is,

${\Rightarrow_{\mathrm{PBPO}}^{\rho}}\qquad=\;{\bigcup_{\tau\,\in\,\mathrm{compact}(\rho)}\,{\Rightarrow_{\mathrm{PBPO^{+}}}^{\tau}}}.$

###### Proof

$\subseteq$: Assume a PBPO step
${G_{L}}\Rightarrow_{\mathrm{PBPO}}^{\rho,(m,\alpha)}{G_{R}}$ with
$t_{L}=\alpha m$ for some $m$ and $\alpha$. Because we are in a quasitopos,
$m$ admits a unique (epi, regular mono)-factorization
$L\stackrel{{\scriptstyle
e}}{{\twoheadrightarrow}}L_{e}\stackrel{{\scriptstyle
m^{\prime}}}{{\hookrightarrow}}G_{L}$. Define $f=\alpha m^{\prime}$ and let
$L_{e}\stackrel{{\scriptstyle f^{\prime}}}{{\hookrightarrow}}{\langle
f\rangle}\stackrel{{\scriptstyle f^{\prime\prime}}}{{\to}}L^{\prime}$ be its
materialization. Then by the materialization property, there exists a unique
$\beta:G_{L}\to{\langle f\rangle}$ such that $f^{\prime}=\beta m^{\prime}$ is
a pullback and $\alpha=f^{\prime\prime}\beta$ commutes. The middle two rows of
diagram

${L}$${K}$${R}$${L_{e}}$${K_{e}}$${R_{e}}$${G_{L}}$${G_{K}}$${G_{R}}$${{\langle
f\rangle}}$${{\langle f\rangle}^{\prime}}$${{\langle
f\rangle}^{\prime\prime}}$${L^{\prime}}$${K^{\prime}}$${R^{\prime}}$$\scriptstyle{t_{L}}$$\scriptstyle{m}$$\scriptstyle{e}$$\scriptstyle{l}$$\scriptstyle{r}$${\mathrm{PO}}$${\mathrm{PB}}$$\scriptstyle{m^{\prime}}$${\mathrm{PO}}$${\mathrm{PB}}$$\scriptstyle{\alpha}$$\scriptstyle{!\beta}$${\mathrm{PO}}$${\mathrm{PB}}$$\scriptstyle{f^{\prime}}$$\scriptstyle{f^{\prime\prime}}$${\mathrm{PO}}$${\mathrm{PB}}$$\scriptstyle{f}$$\scriptstyle{l^{\prime}}$$\scriptstyle{r^{\prime}}$

show that the pullback $f^{\prime}=\beta m^{\prime}$ defines a strong match
and therefore a step

${G_{L}}\Rightarrow_{\mathrm{PBPO}^{+}}^{\rho_{e},(m^{\prime},\beta)}{G_{R}}$

for rule $\rho_{e}\in\mathrm{compact}(\rho)$.

$\supseteq$: We start with the middle two rows of the diagram of direction
$\subseteq$, and with $f^{\prime}=\beta m^{\prime}$ a pullback. Observe that
$m^{\prime}$ is necessarily regular by regular monicity of $f^{\prime}$ and
pullback stability of regular monos. Then from the definition of $\rho_{e}$ it
is immediate that the outer diagram defines a PBPO step using rule $\rho$,
match $m$ and adherence morphism $\alpha$. ∎

###### Definition 23

We let PBPO↪ denote the rewriting framework obtained by modifying PBPO to
allow regular monic matches only. That is,

${{G_{L}}\Rightarrow_{\mathrm{PBPO}^{\hookrightarrow}}^{\rho,(m,\alpha)}{G_{R}}}\quad\Longleftrightarrow\quad{{G_{L}}\Rightarrow_{\mathrm{PBPO}}^{\rho,(m,\alpha)}{G_{R}}}\text{
and $m$ is a regular mono.}$

###### Proposition 14

Let C be a quasitopos and $\rho$ a PBPO↪ rule. The class of PBPO+ rules
$\mathrm{compact}^{\cong}(\rho)$ models $\rho$.

###### Proof

For any (epi, regular mono)-factorization $m=m^{\prime}e$ of a regular mono
$m$, $e$ is a regular mono (Proposition 4), and hence an isomorphism
(Proposition 5). Thus one can specialize the claim and proof of Theorem 5.2 to
$\mathrm{compact}^{\cong}(\rho)$ rather than $\mathrm{compact}(\rho)$. ∎

######  Corollary 4 (PBPO+ Models PBPO)

Assume C is a quasitopos and let $\rho$ be a PBPO rule.

  1. 1.

There exists a single PBPO+ rule $\tau$ such that
${\Rightarrow_{\mathrm{PBPO}^{\hookrightarrow}}^{\rho}}={{\Rightarrow_{\mathrm{PBPO}^{+}}^{\tau}}}$.

  2. 2.

If $t_{L}$ of $\rho$ is a regular mono, then there exists a single PBPO+ rule
$\tau$ such that
${{\Rightarrow_{\mathrm{PBPO}}^{\rho}}}={{\Rightarrow_{\mathrm{PBPO}^{+}}^{\tau}}}$.

###### Proof

For the first claim, we are left with only one rule after identifying all
isomorphic objects in the category. For the second claim, if $t_{L}$ of $\rho$
is a regular mono, then for all strong matches $t_{L}=\alpha m$, $m$ is a
regular mono by pullback stability. Thus
$\smash{{{\Rightarrow_{\mathrm{PBPO}}^{\rho}}}={\Rightarrow_{\mathrm{PBPO}^{\hookrightarrow}}^{\rho}}}$,
and the first claim can be applied. ∎

###  5.4 PBPO+ Models AGREE

AGREE is short for “Algebraic Graph REwriting with controlled Embedding” and
is a rewriting framework introduced by Corradini et al. [5, 7]. In categories
where both SqPO and AGREE are applicable, AGREE can roughly be thought of as
adding a filtering mechanism on top of the cloning operations that were
originally introduced by SqPO. Moreover, an interesting technical aspect of
AGREE is that it was the first formalism to utilize partial map classifiers
for the definition of rewrite steps.

######  Definition 24 (AGREE Rewriting [5, 7])

Assume C has $\mathcal{M}$-partial map classifiers for a stable system of
monics $\mathcal{M}$.

An _AGREE rewrite rule_ is of the form

${L}$${K}$${R}$${K^{\prime}}$$\scriptstyle{t_{K}}$$\scriptstyle{l}$$\scriptstyle{r}$

where $t_{K}$ is an $\mathcal{M}$-morphism.

A diagram of the form

${L}$${K}$${R}$${G_{L}}$${G_{K}}$${G_{R}}$${T(L)}$${K^{\prime}}$$\scriptstyle{m}$$\scriptstyle{\eta_{L}}$$\scriptstyle{l}$$\scriptstyle{r}$${\mathrm{PO}}$$\scriptstyle{\overline{m}}$${\mathrm{PB}}$${\mathrm{PB}}$$\scriptstyle{\varphi(t_{K},l)}$$\scriptstyle{t_{K}}$

defines an _AGREE rewrite step_
${G_{L}}\Rightarrow_{\mathrm{AGREE}}^{\rho,m}{G_{R}}$, i.e., it is a step from
object $G_{L}$ to object $G_{R}$ induced by rule $\rho$ and match morphism
$m:L\hookrightarrow G_{L}$.

The proposition below is stated for $\mathcal{M}$ the class of all monos in
[2].

######  Proposition 15 (Relating AGREE and PBPO [2, Proposition 3.1])

Assume C has $\mathcal{M}$-partial map classifiers for a stable system of
monics $\mathcal{M}$. In the diagram

${\boldsymbol{L}}$${\boldsymbol{K}}$${\boldsymbol{R}}$${T(L)}$${\boldsymbol{K^{\prime}}}$${R^{\prime}}$$\scriptstyle{\eta_{L}}$$\scriptstyle{\boldsymbol{t_{K}}}$$\scriptstyle{\boldsymbol{l}}$$\scriptstyle{\boldsymbol{r}}$${\mathrm{PO}}$$\scriptstyle{t_{R}}$${\mathrm{PB}}$$\scriptstyle{\varphi(t_{K},l)}$$\scriptstyle{r^{\prime}}$

let the bold subdiagram depict an AGREE rule $\rho$, and the entire diagram a
PBPO rule ${\llbracket{\rho}\rrbracket}_{\mathrm{PBPO}}$, where the right
square is a pushout. Then for any match $m\in\mathcal{M}$, we have
${\Rightarrow_{\mathrm{AGREE}}^{\rho,m}}={\Rightarrow_{\mathrm{PBPO}}^{{\llbracket{\rho}\rrbracket}_{\mathrm{PBPO}},(m,\overline{m})}}$.
∎

Observe that Proposition 15 relies on a particular choice of adherence
morphism $\alpha=\overline{m}$. Thus it does not establish that PBPO models
AGREE. In fact, we have the following.

###### Proposition 16

In Graph with $\mathcal{M}$ the class of all monos, AGREE $\not\prec$ PBPO.

###### Proof

The AGREE rule $\rho$ given by

$L$$x$$K$$R$$G_{L}$$x$$y$$G_{K}$$y$$G_{R}$$y$$T(L)$$x$$y$$K^{\prime}$$y$

matches and deletes a single node $x$ and any of its incident edges, in any
context. The context itself is preserved. Given the depicted $G_{L}$ and match
$m$, the depicted $\alpha=\overline{m}:G_{L}\to T(L)$ is by definition the
only possible adherence morphism. By contrast, PBPO allows an adherence
morphism that maps $y$ onto $x$, so that $G_{K}$ and $G_{R}$ are both empty.
So
$\Rightarrow_{\mathrm{PBPO}}^{{\llbracket{\rho}\rrbracket}_{\mathrm{PBPO}},m}\not\subseteq{\Rightarrow_{\mathrm{AGREE}}^{\rho,m}}$.
Moreover, it is easy to see that the problem cannot be avoided by redefining
the interpretation, because any redefinition will necessarily have $x$ in
$L^{\prime}$, with $x$ deleted in $K^{\prime}$. ∎

Similar arguments can be constructed for other categories satisfying the
conditions of Proposition 15, including Set. For PBPO+, however, we have the
following result.

######  Proposition 17 (Relating AGREE and PBPO+)

Assume C has $\mathcal{M}$-partial map classifiers for a stable system of
monics $\mathcal{M}$. In the diagram

${\boldsymbol{L}}$${\boldsymbol{K}}$${\boldsymbol{R}}$${T(L)}$${\boldsymbol{K^{\prime}}}$$\scriptstyle{\eta_{L}}$$\scriptstyle{\boldsymbol{t_{K}}}$$\scriptstyle{\boldsymbol{l}}$$\scriptstyle{\boldsymbol{r}}$${\mathrm{PB}}$$\scriptstyle{\varphi(t_{K},l)}$

let the bold subdiagram depict an AGREE rule $\rho$, and the entire diagram a
PBPO+ rule ${\llbracket{\rho}\rrbracket}_{\mathrm{PBPO}^{+}}$. Then for any
match $m\in\mathcal{M}$ and adherence $\alpha$ establishing a PBPO+ step,
${\Rightarrow_{\mathrm{AGREE}}^{\rho,m}}={\Rightarrow_{\mathrm{PBPO}^{+}}^{{\llbracket{\rho}\rrbracket}_{\mathrm{PBPO}^{+}},m}}$.

###### Proof

By virtue of the partial map classifier, $\overline{m}$ is the only adherence
morphism establishing a strong match for PBPO+. ∎

######  Corollary 5 (PBPO+ Models AGREE)

AGREE $\prec$ PBPO+ in any quasitopos. ∎

###  5.5 PBPO+ Models DPO

The Double Pushout (DPO) approach to graph rewriting by Ehrig et al. [8] is
one of the earliest and most well studied algebraic graph rewriting methods.

######  Definition 25 (DPO Rewriting [8])

A _DPO rewrite rule_ $\rho$ is a span $L\stackrel{{\scriptstyle
l}}{{\hookleftarrow}}K\stackrel{{\scriptstyle r}}{{\to}}R$. A diagram

${L}$${K}$${R}$${G_{L}}$${G_{K}}$${G_{R}}$$\scriptstyle{m}$$\scriptstyle{l}$$\scriptstyle{r}$${\mathrm{PO}}$${\mathrm{PO}}$

defines a _DPO rewrite step_
${G_{L}}\Rightarrow_{\mathrm{DPO}}^{\rho,m}{G_{R}}$, i.e., a step from $G_{L}$
to $G_{R}$ using rule $\rho$ and match morphism $m:L\to G_{L}$.

######  Definition 26 (DPO as PBPO+)

Let C be a category with $\mathcal{M}$-partial map classifiers, in which
pushouts along $\mathcal{M}$-morphisms exist, are pullbacks, and where
$\mathcal{M}$-morphisms are stable under pushout.

In the diagram

${\boldsymbol{L}}$${\boldsymbol{K}}$${\boldsymbol{R}}$${L^{\prime}}$${T(K)}$$\scriptstyle{t_{L}}$$\scriptstyle{\boldsymbol{l}}$$\scriptstyle{\boldsymbol{r}}$$\scriptstyle{\eta_{K}}$${\mathrm{PO}}$$\scriptstyle{l^{\prime}}$

let the top span depict a DPO rule $\rho$, and the left square a pushout
(which is a pullback). Then the entire diagram defines a PBPO+ rule
${\llbracket{\rho}\rrbracket}_{\mathrm{PBPO}^{+}}$.

######  Theorem 5.3 (PBPO+ Models DPO)

Let C be a quasitopos. Then for any DPO rule $\rho$,
${\llbracket{\rho}\rrbracket}_{\mathrm{PBPO}^{+}}$ is well-defined, and for
any $\mathcal{M}$-morphism $m:L\hookrightarrow G_{L}$, we have
${\Rightarrow_{\mathrm{DPO}}^{\rho,m}}={\Rightarrow_{\mathrm{PBPO}^{+}}^{{\llbracket{\rho}\rrbracket}_{\mathrm{PBPO}^{+}},m}}$.

###### Proof

Well-definedness of ${\llbracket{\rho}\rrbracket}_{\text{PBPO${}^{+}$}}$
follows from Definition 15, Lemma 3, and the fact that any quasitopos is
$\mathcal{M}$-adhesive for $\mathcal{M}=\mathrm{rm}({\textbf{C}})$.

Direction $\subseteq$: Suppose that

${L}$${K}$${R}$${G_{L}}$${G_{K}}$${G_{R}}$$\scriptstyle{m}$$\scriptstyle{l}$$\scriptstyle{u}$$\scriptstyle{r}$${\mathrm{PO}}$${\mathrm{PO}}$$\scriptstyle{w}$$\scriptstyle{g_{R}}$$\scriptstyle{g_{L}}$

is a DPO step induced by $\rho$. Then by Lemma 3, the left square is a
pullback, and by stability of $\mathcal{M}$-morphisms under pushout and
pullback, $u,g_{L}\in\mathcal{M}$.

Because $u\in\mathcal{M}$, we obtain the classifying arrow
$\overline{u}:G_{K}\to T(K)$ that makes the square $\overline{u}\circ
u=\eta_{K}\circ\mathrm{1}_{K}$ a pullback. Additionally, from the pushout
property of the top left square, we obtain a unique morphism $\alpha:G_{L}\to
L^{\prime}$ satisfying $t_{L}=\alpha\circ m$ and $\alpha\circ
g_{L}=l^{\prime}\circ\overline{u}$:

${L}$${K}$${R}$${G_{L}}$${G_{K}}$${G_{R}}$${L^{\prime}}$${T(K)}$$\scriptstyle{m}$$\scriptstyle{t_{L}}$$\scriptstyle{l}$$\scriptstyle{u}$$\scriptstyle{r}$${\mathrm{PO}}$${\mathrm{PO}}$$\scriptstyle{w}$$\scriptstyle{\alpha}$$\scriptstyle{g_{R}}$$\scriptstyle{g_{L}}$$\scriptstyle{\overline{u}}$$\scriptstyle{l^{\prime}}$$\scriptstyle{\eta_{K}}$
(2)

By the dual of the pullback lemma, it follows that the bottom left commuting
square is a pushout. Because it is a pushout along an $\mathcal{M}$-morphism,
it is also a pullback.

It remains to show that square $t_{L}\circ\mathrm{1}_{L}=\alpha\circ m$ is a
pullback. For this, consider the cubical arrangement

${K}$${K}$${L}$${L}$${G_{K}}$${T(K)}$${G_{L}}$${L^{\prime}}$$\scriptstyle{u}$$\scriptstyle{l}$$\scriptstyle{\eta_{K}}$$\scriptstyle{l}$$\scriptstyle{m}$$\scriptstyle{\overline{u}}$$\scriptstyle{g_{L}}$$\scriptstyle{l^{\prime}}$$\scriptstyle{\alpha}$$\scriptstyle{t_{L}}$

in which the bottom square is a pushout along an $\mathcal{M}$-morphism, the
back faces are pullbacks and the top square is a pushout. By
$\mathcal{M}$-adhesivity, the bottom square is an $\mathcal{M}$-VK square.
From this it follows that the front face is a pullback square. Thus Diagram
(2) defines a PBPO+ step.

Direction $\supseteq$: We are given a PBPO+ step

${L}$${K}$${R}$${L}$${G_{L}}$${G_{K}}$${G_{R}}$${L}$${L^{\prime}}$${T(K)}$$\scriptstyle{m}$$\scriptstyle{l}$$\scriptstyle{u}$$\scriptstyle{r}$${\mathrm{PB}}$${\mathrm{PO}}$$\scriptstyle{w}$$\scriptstyle{m}$${\mathrm{PB}}$$\scriptstyle{\alpha}$$\scriptstyle{g_{R}}$$\scriptstyle{g_{L}}$$\scriptstyle{u^{\prime}}$${\mathrm{PB}}$$\scriptstyle{t_{L}}$$\scriptstyle{l^{\prime}}$$\scriptstyle{\eta_{K}}$
(3)

where the pullback squares can be represented as the commutative cube

${K}$${G_{K}}$${L}$${G_{L}}$${K}$${T(K)}$${L}$${L^{\prime}}$$\scriptstyle{u}$$\scriptstyle{l}$$\scriptstyle{u^{\prime}}$$\scriptstyle{g_{L}}$$\scriptstyle{m}$$\scriptstyle{\eta_{K}}$$\scriptstyle{l}$$\scriptstyle{l^{\prime}}$$\scriptstyle{t_{L}}$$\scriptstyle{\alpha}$

.

By Lemma 2, we know that the back face is a pullback square. Because the floor
is a pushout, and the vertical faces are all pullbacks, it follows that the
top face of the cube is a pushout, using the fact that pushouts are stable
under pullback in rm-quasiadhesive categories. Thus the top row of Diagram (3)
defines a DPO step. ∎

###### Theorem 5.4

Let C be a quasitopos, and let matches $m$ be regular monic. Then:

PBPO+$\text{SqPO}\prec\text{AGREE}$DPOPBPO$\prec$$\prec$$\prec$

###### Proof

By SqPO $\prec$ AGREE [5, Theorem 2], Corollary 4, Corollary 5 and Theorem
5.3. ∎

Moreover, we have the following negative result for the other directions.

###### Proposition 18

In Graph, which is a quasitopos, not every PBPO+ rule can be modeled by a set
of $\mathcal{F}\in\\{\mathrm{AGREE},\mathrm{PBPO},\mathrm{DPO}\\}$ rules.

###### Proof

The PBPO+ rule

$L$$x$$K$$R$$L^{\prime}$$x$$y$$K^{\prime}$$y$$R^{\prime}$$y$

serves to prove all three claims. It specifies the deletion of a single node
in a host graph without edges. AGREE and DPO cannot model this rule even with
an infinite set of rules, because they cannot express that the host graph
cannot have edges. Although PBPO can express this constraint, it cannot
prevent rules from mapping the entire host graph onto $x$, deleting all nodes
at once. ∎

##  6 Category Graph(L,≤)

Unless one employs a meta-notation or restricts to unlabeled graphs, as we did
in Section 3, it is sometimes impractical to use PBPO+ in the category Graph.
The following example illustrates the problem.

###### Example 10

Suppose the set of labels is $\mathcal{L}=\\{0,1\\}$. To be able to
injectively match pattern $L=\leavevmode\hbox to41.45pt{\vbox
to13.86pt{\pgfpicture\makeatletter\hbox{\hskip 20.72427pt\lower-6.98177pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{}{}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{\offinterlineskip{}{}{{{}}{{}}}{{{}}}{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-20.72427pt}{-6.88193pt}\pgfsys@invoke{
}\hbox{\vbox{\halign{\pgf@matrix@init@row\pgf@matrix@step@column{\pgf@matrix@startcell#\pgf@matrix@endcell}&#\pgf@matrix@padding&&\pgf@matrix@step@column{\pgf@matrix@startcell#\pgf@matrix@endcell}&#\pgf@matrix@padding\cr\hfil\hskip
6.80554pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-2.5pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{${0}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}}}&\hskip
6.80554pt\hfil&\hfil\hskip 21.03192pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-2.5pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{${0}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip
6.80554pt\hfil\cr}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}{{{{}}}{{}}{{}}}} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} {}{ {}{}{}}{}{ {}{}{}} {{{{{}}{
{}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{
}{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{-6.9132pt}{-4.38193pt}\pgfsys@lineto{6.51323pt}{-4.38193pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{6.71321pt}{-4.38193pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-1.75pt}{-2.02916pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{$\scriptstyle{1}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{
{}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}$ in any context, one
must inject it into the type graph $L^{\prime}$ shown on the right in which
every dotted loop represents two edges (one for each label), and every dotted
non-loop represents four edges (one for each label, in either direction). For
general $\mathcal{L}$, to allow any context, one needs to include
$|\mathcal{L}|$ additional vertices in $L^{\prime}$, and $|\mathcal{L}|$
complete graphs over $V_{L^{\prime}}$.

${1}$${0}$${0}$${0}$$\scriptstyle{1}$

Beyond this example, and less easily alleviated with meta-notation, in Graph
it is impractical or impossible to express rules that involve (i) arbitrary
labels (or classes of labels) in the application condition; (ii) relabeling;
or (iii) allowing and capturing arbitrary subgraphs (or classes of subgraphs)
around a match graph. As we will discuss in Section 7, these features have
been non-trivial to express in general for algebraic graph rewriting
approaches.

We define a category which allows flexibly addressing all of these issues.
Recall the definition of a complete lattice (Definition 17).

######  Definition 27 (Graph(L,≤))

For a complete lattice $(\mathcal{L},\leq)$, we define the category
Graph(L,≤), where objects are graphs labeled from $\mathcal{L}$, and arrows
are graph premorphisms $\phi:G\to G^{\prime}$ that satisfy
$\ell_{G}(x)\leq\ell_{G^{\prime}}(\phi(x))$ for all $x\in V_{G}\cup E_{G}$.

In terms of graph structure, the pullbacks and pushouts in Graph(L,≤) are the
usual pullbacks and pushouts in Graph. The only difference is that the labels
that are identified by the cospan of the pullback (resp. span of the pushout)
are replaced by their meet (resp. join).

######  Remark 9 (Fuzzy Graph Rewriting)

The idea to label graphs using labels that form a complete lattice, for the
purpose of rewriting, is not new. To the best of our knowledge, Mori and
Kawahara were the first to propose this [32], using a single pushout
construction. There also exists a series of papers by Parasyuk and Yershov, in
which fuzzy graph transformations are studied using single pushouts [33] and
double pushouts [34, 35]. Because PBPO+ rules have both a pattern span and a
type span (unlike in the single and double pushout approaches), both lower and
upper bounds can be specified on fuzzy values. Moreover, that fuzzy graphs
lend themselves well for general relabeling purposes has not yet been
observed.

###### Remark 10

Analogous to the situation for $\mathcal{L}$-fuzzy sets (Example 8), we have
proven very recently that Graph(L,≤) is a quasitopos if $\mathcal{L}$ is a
complete Heyting algebra [28].

One very simple but useful complete lattice is the following.

######  Definition 28 (Flat Lattice)

Let $\mathcal{L}^{\bot,\top}=\mathcal{L}\uplus\\{\bot,\top\\}$. We define the
_flat lattice_ induced by $\mathcal{L}$ as the poset
$(\mathcal{L}^{\bot,\top},{\leq})$, in which $\bot<l<\top$ for all
$l\in\mathcal{L}$ are the only non-trivial relations. Here, we refer to
$\mathcal{L}$ as the _base label set_.

One feature flat lattices provide is a kind of “wildcard element” $\top$.

######  Example 11 (Wildcards)

Using flat lattices, $L^{\prime}$ of Example 10 can be fully expressed for any
base label set $\mathcal{L}\ni 0,1$ as shown on the right (node identities are
omitted). The visual syntax and naming shorthands of PGR [1] (or variants
thereof) could be leveraged to simplify the notation further.

${\top}$${0}$${0}$$\scriptstyle{\top}$$\scriptstyle{\top}$$\scriptstyle{\top}$$\scriptstyle{1}$$\scriptstyle{\top}$$\scriptstyle{\top}$$\scriptstyle{\top}$$\scriptstyle{\top}$$\scriptstyle{\top}$$\scriptstyle{\top}$

As the following example illustrates, the expressive power of a flat lattice
stretches beyond wildcards: it also enables relabeling of graphs. (Henceforth,
we will depict a node $x$ with label $u$ as $x^{u}$.)

######  Example 12 (Relabeling)

As vertex labels we employ the flat lattice induced by the set
$\\{\,a,b,c,\ldots\,\\}$, and assume edges are unlabeled for notational
simplicity. The diagram

$L$$x$$\bot$$K$$x$$\bot$$R$$x$$c$$G_{L}$$x$$a$$z$$b$$G_{K}$$x$$\bot$$z$$b$$G_{R}$$x$$c$$z$$b$$L^{\prime}$$x$$\top$$z$$\top$$K^{\prime}$$x$$\bot$$z$$\top$$R^{\prime}$$x$$c$$z$$\top$

displays a rule ($L,L^{\prime},K,K^{\prime},R$) for overwriting an arbitrary
vertex’s label with $c$, in any context. The middle row is an application to a
host graph $G_{L}$.

Example 12 demonstrates how (i) labels in $L$ serve as lower bounds for
matching, (ii) labels in $L^{\prime}$ serve as upper bounds for matching,
(iii) labels in $K^{\prime}$ can be used to decrease matched labels (in
particular, $\bot$ “instructs” to “erase” the label by overwriting it with
$\bot$, and $\top$ “instructs” to preserve labels), and (iv) labels in $R$ can
be used to increase labels. First erasing a label in $K^{\prime}$ and then
increasing it using another label in $R$ effectively establishes an arbitrary
relabeling from $G_{L}$ to $G_{R}$.

Complete lattices also support modeling sorts.

######  Example 13 (Sorts)

Let $p_{1},p_{2},\ldots\in\mathbb{P}$ be a set of processes and
$d_{1},d_{2},\ldots\in\mathbb{D}$ a set of data elements. Assume a complete
lattice over labels
$\mathbb{P}\cup\mathbb{D}\cup\\{\mathbb{P},\mathbb{D},\rhd,@\\}$, arranged as
in the diagram

$\forall i\in\mathbb{N}:\\\ \leavevmode\hbox to107.42pt{\vbox
to84.96pt{\pgfpicture\makeatletter\hbox{\hskip 53.7087pt\lower-42.47952pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{}{}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{\offinterlineskip{}{}{{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}}{{{}}}{{}{}{{ {}{}}}{
{}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-53.7087pt}{-42.47952pt}\pgfsys@invoke{
}\hbox{\vbox{\halign{\pgf@matrix@init@row\pgf@matrix@step@column{\pgf@matrix@startcell#\pgf@matrix@endcell}&#\pgf@matrix@padding&&\pgf@matrix@step@column{\pgf@matrix@startcell#\pgf@matrix@endcell}&#\pgf@matrix@padding\cr\hfil\hskip
0.0pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}}}&\hskip
0.0pt\hfil&\hfil\hskip 22.42082pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-3.8889pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{${\top}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}}}&\hskip
8.19444pt\hfil&\hfil\hskip 14.22638pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}}}&\hskip
0.0pt\hfil&\hfil\hskip 14.22638pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip
0.0pt\hfil\cr\vskip 8.53583pt\cr\hfil\hskip
7.70833pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-3.40279pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{${\mathbb{P}}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip
7.70833pt\hfil&\hfil\hskip 22.35136pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-3.81944pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{${\mathbb{D}}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip
8.12498pt\hfil&\hfil\hskip 22.42082pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-3.8889pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{${\rhd}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip
8.19444pt\hfil&\hfil\hskip 22.42082pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-3.8889pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{${@}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip
8.19444pt\hfil\cr\vskip 8.53583pt\cr\hfil\hskip
7.7858pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-3.48026pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{${p_{i}}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip
7.7858pt\hfil&\hfil\hskip 22.09898pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-3.56706pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{${d_{i}}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip
7.8726pt\hfil&\hfil\hskip 14.22638pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip
0.0pt\hfil&\hfil\hskip 14.22638pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip
0.0pt\hfil\cr\vskip 8.53583pt\cr\hfil\hskip
0.0pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip
0.0pt\hfil&\hfil\hskip 22.42082pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-3.8889pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{${\bot}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip
8.19444pt\hfil&\hfil\hskip 14.22638pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip
0.0pt\hfil&\hfil\hskip 14.22638pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip
0.0pt\hfil\cr}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}{{{{}}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {}{}{}}{}{ {}{}{}}
{{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{
}{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{-38.01457pt}{13.88464pt}\pgfsys@lineto{-24.42992pt}{24.14046pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.7981}{0.60252}{-0.60252}{0.7981}{-24.27032pt}{24.26094pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{
{}{}{}}{}{ {}{}{}} {{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{
}{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{-15.71628pt}{16.10902pt}\pgfsys@lineto{-15.71628pt}{23.95601pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.0}{1.0}{-1.0}{0.0}{-15.71628pt}{24.15599pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{
{}{}{}}{}{ {}{}{}} {{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{
}{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{6.50455pt}{14.16751pt}\pgfsys@lineto{-7.00108pt}{24.22719pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{-0.80199}{0.59735}{-0.59735}{-0.80199}{-7.16145pt}{24.34665pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{
{}{}{}}{}{ {}{}{}} {{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{
}{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{37.11981pt}{11.04085pt}\pgfsys@lineto{-6.94702pt}{27.45139pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{-0.93713}{0.34898}{-0.34898}{-0.93713}{-7.13441pt}{27.52116pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{
{}{}{}}{}{ {}{}{}} {{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{
}{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{-45.9229pt}{-9.57016pt}\pgfsys@lineto{-45.9229pt}{1.15633pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.0}{1.0}{-1.0}{0.0}{-45.9229pt}{1.35631pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{
{}{}{}}{}{ {}{}{}} {{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{
}{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{-15.71628pt}{-6.93126pt}\pgfsys@lineto{-15.71628pt}{1.15633pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.0}{1.0}{-1.0}{0.0}{-15.71628pt}{1.35631pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope {
{}{}{}}{}{ {}{}{}}{ {}{}{}}{{{{}}{{}}{{}}{{}}}{{{{}}{ {}{}}{}{}{{}{}}}}
}{{{{}}{{}}{{}}{{}}{{}}}{{{{}}{ {}{}}{}{}{{}{}}}} }{{}{}}{{}}
{}{}{}{{{}}{{}}{{}}} {{{}}{{}}{{}}}
{}{{}}{}{{}}{}{{}}{}{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{
}{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{-7.32184pt}{-35.62834pt}\pgfsys@curveto{7.3189pt}{-27.43079pt}{14.37462pt}{-15.57346pt}{14.5905pt}{0.80466pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.01318}{0.99991}{-0.99991}{0.01318}{14.59312pt}{1.00461pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{
{}{}{}}{}{ {}{}{}} {{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{
}{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{-15.71628pt}{-31.67538pt}\pgfsys@lineto{-15.71628pt}{-23.84175pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.0}{1.0}{-1.0}{0.0}{-15.71628pt}{-23.64177pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{
{}{}{}}{}{ {}{}{}} {{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{
}{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{-24.11072pt}{-33.1032pt}\pgfsys@lineto{-37.62773pt}{-22.02864pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{-0.77353}{0.63376}{-0.63376}{-0.77353}{-37.78241pt}{-21.9019pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope {
{}{}{}}{}{ {}{}{}}{ {}{}{}}{{{{}}{{}}{{}}{{}}}{{{{}}{ {}{}}{}{}{{}{}}}}
}{{{{}}{{}}{{}}{{}}{{}}}{{{{}}{ {}{}}{}{}{{}{}}}} }{{}{}}{{}}
{}{}{}{{{}}{{}}{{}}} {{{}}{{}}{{}}}
{}{{}}{}{{}}{}{{}}{}{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{
}{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{-7.32184pt}{-38.79547pt}\pgfsys@curveto{17.5762pt}{-34.96161pt}{33.82031pt}{-21.92296pt}{42.80423pt}{1.18352pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.36238}{0.93204}{-0.93204}{0.36238}{42.8767pt}{1.3699pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys<EMAIL_ADDRESS>
Moreover, assume that the vertices $x,y,\ldots$ in the graphs of interest are
labeled with a $p_{i}$ or $d_{i}$, and that edges are labeled with a $\rhd$ or
$@$. In such a graph,

  * •

an edge $x^{d_{i}}\xrightarrow{@}y^{p_{j}}$ encodes that process $p_{j}$ holds
a local copy of datum $d_{i}$ ($x$ will have no other connections); and

  * •

a chain of edges
$x^{p_{i}}\xrightarrow{\rhd}y^{d_{k}}\xrightarrow{\rhd}z^{d_{l}}\xrightarrow{\rhd}\cdots\xrightarrow{\rhd}u^{p_{j}}$
encodes a directed FIFO channel from process $p_{i}$ to process $p_{j}\neq
p_{i}$, containing a sequence of elements $d_{k},d_{l},\ldots$. An empty
channel is modeled as $x^{p_{i}}\xrightarrow{\rhd}u^{p_{j}}$.

Receiving a datum through an incoming channel (and storing it locally) can be
modeled using the following rule:

$L$$x_{1}$$x_{2}$$\bot$$y$$\bot$$\rhd$$L^{\prime}$$x_{1}$$x_{2}$$\mathbb{D}$$y$$\mathbb{P}$$\rhd$$z$$\top$$\top$$\top$$\top$$\top$$K^{\prime}$$x_{1}$$\bot$$y$$\mathbb{P}$$z$$\top$$\top$$\top$$\top$$\top$$x_{2}$$\mathbb{D}$$K$$x_{1}$$\bot$$y$$\bot$$x_{2}$$\bot$$R$$x_{1}$$y$$\bot$$x_{2}$$\bot$$@$$R^{\prime}$$x_{1}$$y$$\mathbb{P}$$z$$\top$$\top$$\top$$\top$$\top$$x_{2}$$\mathbb{D}$$@$

The rule illustrates how sorts can improve readability and provide type
safety. For instance, the label $\mathbb{D}$ in $L^{\prime}$ prevents empty
channels from being matched. More precisely, always the last element $d$ of a
non-empty channel is matched. $K^{\prime}$ duplicates the node holding $d$:
for duplicate $x_{1}$, the label is forgotten but the connection to the
context retained, allowing it to be fused with $y$; and for $x_{2}$, the
connection is forgotten but the label retained, allowing it to be connected to
$y$ as an otherwise isolated node.

Finally, a very powerful feature provided by the coupling of PBPO+ and
Graph(L,≤) is the ability to model a general notion of variable, used for
matching (possibly disjoint) parts of the context. This is achieved by using
multiple context nodes in $L^{\prime}$ (i.e., nodes not in the image of
$t_{L}$).

######  Example 14 (Variables)

The rule $f(g(x),y)\to h(g(x),g(y),x)$ on ordered trees can be precisely
modeled in PBPO+ by the rule

$L$$v$$f$$w$$g$$y$$\bot$$x_{1}$$x_{2}$$\bot$$1$$1$$2$$K$$v$$\bot$$y$$\bot$$x_{1}$$\bot$$x_{2}$$\bot$$R$$v$$h$$z_{2}$$g$$z_{1}$$g$$x_{2}$$\bot$$y$$\bot$$x_{1}$$\bot$$1$$2$$3$$1$$1$$L^{\prime}$$u$$\top$$v$$f$$w$$g$$y$$\top$$x_{1}$$x_{2}$$\top$$x^{\prime}_{1}$$x^{\prime}_{2}$$\top$$y^{\prime}$$\top$$\top$$\top$$1$$1$$\top$$\top$$2$$\top$$\top$$K^{\prime}$$u$$\top$$v$$\bot$$y$$\top$$y^{\prime}$$\top$$x_{1}$$\top$$x_{2}$$\top$$x^{\prime}_{1}$$\top$$x^{\prime}_{2}$$\top$$\top$$\top$$\top$$\top$$\top$$\top$$\top$$\top$$R^{\prime}$$u$$\top$$v$$h$$z_{2}$$g$$z_{1}$$g$$x_{2}$$\top$$y$$\top$$y^{\prime}$$\top$$x_{1}$$\top$$x^{\prime}_{1}$$\top$$x^{\prime}_{2}$$\top$$\top$$\top$$\top$$\top$$\top$$\top$$\top$$\top$$1$$2$$3$$1$$1$

if one restricts the set of rewritten graphs to straightforward
representations of trees: nodes are labeled by symbols, and edges are labeled
by $n\in\mathbb{N}$, the position of its target (argument of the symbol).

In another paper [36], we developed the idea of Example 14 further, and showed
that any linear term rewriting system $R$ can be faithfully represented by a
PBPO+ graph rewrite system encoding $\mathcal{E}(R)$, with the additional
property that $R$ terminates iff $\mathcal{E}(R)$ terminates on finite graphs
[36, Theorem 62].

##  7 Discussion

We discuss our rewriting (Section 7.1) and relabeling (Section 7.2)
contributions in turn.

###  7.1 Rewriting

Other graph rewriting approaches that bear certain similarities to PBPO+ (see
also the discussion in [2]) include the double-pullout graph rewriting
approach by Kahl [37]; the cospan SqPO approach by Mantz [38, Section 4.5];
and the recent drag rewriting framework by Dershowitz and Jouannaud [39].
Double-pullout graph rewriting also uses pullbacks and pushouts to delete and
duplicate parts of the context (extending DPO), but the approach is defined in
the context of collagories [40], and to us it is not yet clear in what way the
two approaches relate. Cospan SqPO can be understood as being almost dual to
SqPO: rules are cospans, and transformation steps consists of a pushout
followed by a final pullback complement. An interesting question is whether
PBPO+ can also model cospan SqPO. Drag rewriting is a non-categorical approach
to generalizing term rewriting, and like PBPO+, allows relatively fine control
over the interface between pattern and context, thereby avoiding issues
related to dangling pointers and the construction of pushout complements.
Because drag rewriting is non-categorical and drags have inherently more
structure than graphs, it is difficult to relate PBPO+ and drag rewriting
precisely. These could all be topics for future investigation.

Let us note that the combination of PBPO+ and Graph(L,≤) does not provide a
strict generalization of Patch Graph Rewriting (PGR) [1], our conceptual
precursor to PBPO+ (Section 1). This is because patch edge endpoints that lie
in the context graph can be redefined in PGR (e.g., the direction of edges
between context and pattern can be inverted), but not in PBPO+. Beyond that,
PBPO+ is more general and expressive. Therefore, at this point we believe that
the most distinguishing and redeeming feature of PGR is its visual syntax,
which makes rewrite systems much easier to define and communicate. In order to
combine the best of both worlds, our aim is to define a similar syntax for (a
suitable restriction of) PBPO+ in the future.

###  7.2 Relabeling

The coupling of PBPO+ and Graph(L,≤) allows relabeling and modeling sorts and
variables with relative ease, and does not require a modification of the
rewriting framework. Most existing approaches study these topics in the
context of DPO, where the requirement to ensure the unique existence of a
pushout complement requires restricting the method and proving non-trivial
properties:

  * •

Parisi-Presicce et al. [41] limit DPO rules $L\leftarrow K\to R$ to ones where
$K\to R$ is monic (meaning merging is not possible), and where some set-
theoretic consistency condition is satisfied. Moreover, the characterization
of the existence of rewrite step has been shown to be incorrect [42],
supporting the idea that pushout complements are not easy to reason about.

  * •

Habel and Plump [42] study relabeling using the category of partially labeled
graphs. They allow non-monic morphisms $K\to R$, but they nonetheless add two
restrictions to the definition of a DPO rewrite rule. Among others, these
conditions do not allow hard overwriting arbitrary labels as in Example 12.
Moreover, the pushouts of the DPO rewrite step must be restricted to pushouts
that are also pullbacks. Finally, unlike the approach suggested by Parisi-
Presice et al., Habel and Plump’s approach does not support modeling notions
of sorts and variables.

Our result that PBPO+ can model DPO in Graph extends to this relabeling
approach in the following sense: given a DPO rule over graphs partially
labeled from $\mathcal{L}$ that moreover satisfies the criteria of [42], we
conjecture that there exists a PBPO+ rule in
Graph${}^{(\mathcal{L}^{\bot,\top},\leq)}$ that models the same rewrite
relation when restricting to graphs totally labeled over the base label set
$\mathcal{L}$.

Later publications largely appear to build on the approach [42] by Habel and
Plump. For example, Schneider [43] gives a non-trivial categorical
formulation; Hoffman [44] proposes a two-layered (set-theoretic) approach to
support variables; and Habel and Plump [45] generalize their approach to
$\mathcal{M},\mathcal{N}$-adhesive systems (again restricting $K\to R$ to
monic arrows).

Independent of Habel and Plump’s approach, there also exists an approach for
DPO by Kahl, in which attributed graphs are considered as coalgebras [46],
providing support for relabeling operations. Relating Kahl’s approach to ours
is outside the scope of the present paper.

The transformation of attributed structures has been explored in a very
general setting by Corradini et al. [2], which involves an elegant comma
category construction and suitable restrictions of the PBPO notions of rewrite
rule and rewrite step. We leave relating their and our approach to future
work.

#### Acknowledgments

We thank Nicolas Behr for inspiring discussions on quasitoposes and PBPO+, and
for pointing us to some important references; Andrea Corradini for providing
guidance on AGREE and PBPO, and for useful feedback on the conference version
of this paper; Clemens Grabmayer for helpful commentary on the subsumption
result; and Michael Shulman, who identified the sufficient conditions for
materialization for us [47]. We are also grateful to anonymous reviewers for
many useful suggestions and corrections.

The authors received funding from the Netherlands Organization for Scientific
Research (NWO) under the Innovational Research Incentives Scheme Vidi
(project. No. VI.Vidi.192.004).

## References

  * [1] R. Overbeek and J. Endrullis.  Patch graph rewriting.  In Proc. Conf. on Graph Transformation (ICGT), volume 12150 of LNCS, pages 128–145. Springer, 2020.
  * [2] A. Corradini, D. Duval, R. Echahed, F. Prost, and L. Ribeiro.  The PBPO graph transformation approach.  J. Log. Algebraic Methods Program., 103:213–231, 2019.
  * [3] O. Wyler.  Lecture Notes on Topoi and Quasitopoi.  World Scientific Publishing Co., 1991.
  * [4] S. Lack and P. Sobociński.  Adhesive categories.  In Proc. Conf. on Foundations of Software Science and Computation Structures (FOSSACS), volume 2987 of LNCS, pages 273–288. Springer, 2004.
  * [5] A. Corradini, D. Duval, R. Echahed, F. Prost, and L. Ribeiro.  AGREE – algebraic graph rewriting with controlled embedding.  In Proc. Conf. on Graph Transformation (ICGT), volume 9151 of LNCS, pages 35–51. Springer, 2015.
  * [6] P. T. Johnstone, S. Lack, and P. Sobocinski.  Quasitoposes, quasiadhesive categories and Artin glueing.  In Algebra and Coalgebra in Computer Science (CALCO), volume 4624 of LNCS, pages 312–326. Springer, 2007.
  * [7] A. Corradini, D. Duval, R. Echahed, F. Prost, and L. Ribeiro.  Algebraic graph rewriting with controlled embedding.  Theor. Comput. Sci., 802:19–37, 2020.
  * [8] H. Ehrig, M. Pfender, and H. J. Schneider.  Graph-grammars: An algebraic approach.  In Proc. Symp. on on Switching and Automata Theory (SWAT), page 167–180. IEEE Computer Society, 1973.
  * [9] R. Overbeek, J. Endrullis, and A. Rosset.  Graph rewriting and relabeling with PBPO+.  In Proc. Conf. on Graph Transformation (ICGT), volume 12741 of LNCS, pages 60–80. Springer, 2021.
  * [10] R. Overbeek and J. Endrullis.  A PBPO+ graph rewriting tutorial.  In Proc. of Workshop on Computing with Terms and Graphs (TERMGRAPH), volume 377 of EPTCS, pages 45–63. Open Publishing Association, 2023.
  * [11] S. Mac Lane.  Categories for the Working Mathematician, volume 5.  Springer Science & Business Media, 1971.
  * [12] S. Awodey.  Category Theory.  Oxford University Press, 2006.
  * [13] H. Ehrig, K. Ehrig, U. Prange, and G. Taentzer.  Fundamentals of Algebraic Graph Transformation.  Springer, 2006.
  * [14] M. Löwe.  Algebraic approach to single-pushout graph transformation.  Theor. Comput. Sci., 109(1&2):181–224, 1993.
  * [15] A. Corradini, T. Heindel, F. Hermann, and B. König.  Sesqui-pushout rewriting.  In Proc. Conf. on Graph Transformation (ICGT), volume 4178 of LNCS, pages 30–45. Springer, 2006.
  * [16] Nicolas Behr, Russ Harmer, and Jean Krivine.  Concurrency theorems for non-linear rewriting theories.  In Proc. Conf. on Graph Transformation (ICGT), volume 12741 of LNCS, pages 3–21. Springer, 2021.
  * [17] M. Bauderon.  A uniform approach to graph rewriting: The pullback approach.  In Proc. of Graph-Theoretic Concepts in Computer Science, volume 1017 of LNCS, pages 101–115. Springer, 1995.
  * [18] M. Bauderon and H. Jacquet.  Pullback as a generic graph rewriting mechanism.  Appl. Categorical Struct., 9(1):65–82, 2001.
  * [19] J. R. B. Cockett and Stephen Lack.  Restriction categories I: categories of partial maps.  Theor. Comput. Sci., 270(1-2):223–259, 2002.
  * [20] J. R. B. Cockett and S. Lack.  Restriction categories II: partial map classification.  Theor. Comput. Sci., 294(1/2):61–102, 2003.
  * [21] H. Ehrig, U. Golas, and F. Hermann.  Categorical frameworks for graph transformation and HLR systems based on the DPO approach.  Bull. EATCS, 102:111–121, 2010.
  * [22] J. Adámek, H. Herrlich, and G. E. Strecker.  Abstract and Concrete Categories - The Joy of Cats.  Dover Publications, 2009.
  * [23] P. T. Johnstone.  Sketches of an Elephant: A Topos Theory Compendium, Volume 1.  Oxford University Press, 2002.
  * [24] T. Heindel.  Hereditary pushouts reconsidered.  In Proc. Conf. on Graph Transformation (ICGT), volume 6372 of LNCS, pages 250–265. Springer, 2010.
  * [25] R. Garner and S. Lack.  On the axioms for adhesive and quasiadhesive categories.  Theory and Applications of Categories, 27(3):27–46, 2012.
  * [26] J. A. Goguen.  $L$-fuzzy sets.  Journal of Mathematical Analysis and Applications, 18(1):145–174, 1967.
  * [27] L. N. Stout.  The Logic of Unbalanced Subobjects in a Category with Two Closed Structures, pages 73–105.  Springer Netherlands, Dordrecht, 1992.
  * [28] A. Rosset, R. Overbeek, and J. Endrullis.  Fuzzy presheaves are quasitoposes.  CoRR, arXiv:2301.13067, 2023.
  * [29] R. Goldblatt.  Topoi: the categorial analysis of logic.  North-Holland, 1979.
  * [30] A. Corradini, T. Heindel, B. König, D. Nolte, and A. Rensink.  Rewriting abstract structures: Materialization explained categorically.  In Proc. Conf. on Foundations of Software Science and Computation Structures (FOSSACS), volume 11425 of LNCS, pages 169–188. Springer, 2019.
  * [31] A. Corradini, T. Heindel, B. König, D. Nolte, and A. Rensink.  Rewriting abstract structures: Materialization explained categorically.  CoRR, arXiv:1902.04809, 2019.
  * [32] Masao Mori and Yasuo Kawahara.  Fuzzy graph rewritings.  数理解析研究所講究録, 918:65–71, 1995.
  * [33] I. N. Parasyuk and S. V. Yershov.  Categorical approach to the construction of fuzzy graph grammars.  Cybernetics and Systems Analysis, 42:570–581, 2006.
  * [34] I. N. Parasyuk and S. V. Ershov.  Transformations of fuzzy graphs specified by FD-grammars.  Cybernetics and Systems Analysis, 43:266–280, 2007.
  * [35] I. N. Parasyuk and S. V. Yershov.  Transformational approach to the development of software architectures on the basis of fuzzy graph models.  Cybernetics and Systems Analysis, 44:749–759, 2008.
  * [36] R. Overbeek and J. Endrullis.  From linear term rewriting to graph rewriting with preservation of termination.  In Proc. Workshop on Graph Computational Models (GCM), volume 350 of EPTCS, pages 19–34, 2021.
  * [37] W. Kahl.  Amalgamating pushout and pullback graph transformation in collagories.  In Proc. Conf. on Graph Transformation (ICGT), volume 6372 of LNCS, pages 362–378. Springer, 2010.
  * [38] F. Mantz.  Coupled Transformations of Graph Structures applied to Model Migration.  PhD thesis, University of Marburg, 2014.
  * [39] N. Dershowitz and J.-P. Jouannaud.  Drags: A compositional algebraic framework for graph rewriting.  Theor. Comput. Sci., 777:204–231, 2019.
  * [40] W. Kahl.  Collagories: Relation-algebraic reasoning for gluing constructions.  J. Log. Algebraic Methods Program., 80(6):297–338, 2011.
  * [41] F. Parisi-Presicce, H. Ehrig, and U. Montanari.  Graph rewriting with unification and composition.  In Proc. Workshop on Graph-Grammars and Their Application to Computer Science, volume 291 of LNCS, pages 496–514. Springer, 1986.
  * [42] A. Habel and D. Plump.  Relabelling in graph transformation.  In Proc. Conf. on Graph Transformation (ICGT), volume 2505 of LNCS, pages 135–147. Springer, 2002.
  * [43] H. J. Schneider.  Changing labels in the double-pushout approach can be treated categorically.  In Formal Methods in Software and Systems Modeling, volume 3393 of LNCS, pages 134–149. Springer, 2005.
  * [44] B. Hoffmann.  Graph transformation with variables.  In Formal Methods in Software and Systems Modeling, volume 3393 of LNCS, pages 101–115. Springer, 2005.
  * [45] A. Habel and D. Plump.  $\mathcal{M}$, $\mathcal{N}$-adhesive transformation systems.  In Proc. Conf. on Graph Transformation (ICGT), volume 7562 of LNCS, pages 218–233. Springer, 2012.
  * [46] W. Kahl.  Graph transformation with symbolic attributes via monadic coalgebra homomorphisms.  Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 71, 2014.
  * [47] M. Shulman.  Subobject- and factorization-preserving typings.  MathOverflow.  URL:https://mathoverflow.net/q/381933 (version: 2021-01-22).