11institutetext: Vrije Universiteit Amsterdam, Amsterdam, The Netherlands
11email: {j.endrullis<EMAIL_ADDRESS>
# Generalized Weighted Type Graphs for
Termination of Graph Transformation Systems

Jörg Endrullis  0000-0002-2554-8270 Roy Overbeek  0000-0003-0569-0947

###### Abstract

We refine the weighted type graph technique for proving termination of double
pushout (DPO) graph transformation systems. We increase the power of the
approach for graphs, we generalize the technique to other categories, and we
allow for variations of DPO that occur in the literature.

###### Keywords:

Graph rewriting, Termination, Weighted Type Graphs, DPO

##  1 Introduction

Termination is a central aspect of program correctness. There has been
extensive research on termination [5, 29, 12, 13, 2, 23] of imperative,
functional, and logic programs. Moreover, there exists a wealth of powerful
termination techniques for term rewriting systems [42]. Term rewriting has
proven useful as an intermediary formalism to reason about C, Java, Haskell
and Prolog programs [24, 22].

There are limitations to the adequacy of terms, however. Terms are usually
crude representations of program states, and termination might be lost in
translation. This holds especially for programs that operate with graph
structures, and for programs that make use of non-trivial pointer or reference
structures.

Nonetheless, such programs can be elegantly represented by graphs. This
motivates the use of graph transformation systems as a unifying formalism for
reasoning about programs. Correspondingly, there is a need for automatable
techniques for reasoning about graph transformation systems, in particular for
(dis)proving properties such as termination and confluence.

Unfortunately, there are not many techniques for proving termination of graph
transformation systems. A major obstacle is the large variety of graph-like
structures. Indeed, the termination techniques that do exist are usually
defined for rather specific notions of graphs. This is in stark contrast to
the general philosophy of algebraic graph transformation [19], the predominant
approach to graph transformation, which uses the language of category theory
to define and study graph transformations in a graph-agnostic manner.

In this paper, we propose a powerful graph-agnostic technique for proving
termination of graph transformation systems based on weighted type graphs. We
base ourselves on work by Bruggink et al. [9]. Their method was developed
specifically for edge-labelled multigraphs, using double pushout (DPO) graph
transformation, and the graph rewrite rules were required to have a discrete
interface, i.e., an interface without edges. We generalize and improve their
approach in several ways:

  1. (a)

We strengthen the weighted type graphs technique for graph rewriting with
monic matching. In the DPO literature, matches are usually required to be
monic since this increases expressivity [26]. The method of Bruggink et al.
[9] is not sensitive to such constraints. It always proves the stronger
property of termination with respect to unrestricted matching. Consequently,
it is bound to fail whenever termination depends on monic matching. Our
method, by contrast, is sensitive to such constraints.

  2. (b)

We generalize weighted type graphs to arbitrary categories, and we propose the
notion of ‘traceable (sub)objects’ as a generalization of nodes and edges to
arbitrary categories.

  3. (c)

We formulate our technique on an abstract level, by describing minimal
assumptions on the behaviour of pushouts involved in the rewrite steps. This
makes our technique applicable to the many variations of DPO (see Remark 1),
for instance, restrictions to specific pushout complements.

### Outline

$K$$L$$R$$G$$C$$H$$l$$r$$m$POPO

The general idea behind our technique, and outline of the paper, is as
follows. DPO rewrite systems induce rewrite steps $G\Rightarrow H$ on objects
if there exists a diagram as shown on the right (the top span of the diagram
is a rule of the rewrite system). We define a decreasing measure $\mathbf{w}$
on objects, and show that $\mathbf{w}(G)>\mathbf{w}(H)$ for any such step
generated by the system. We want to do this in a general categorical setting.
This means that we cannot make assumptions about what the objects and
morphisms represent. For simplicity, assume for now that the system contains a
single rule $\rho:L\leftarrow K\to R$.

A first approximation of our measure $\mathbf{w}$ is
$\mathbf{w}=\\#\mathrm{Hom}(\,\cdot\,,T)$ for some distinguished object $T$,
where a termination proof consists of an analysis that shows that for any step
$G\Rightarrow H$ generated by $\rho$,
$\\#\mathrm{Hom}(G,T)>\\#\mathrm{Hom}(H,T)$. The technical challenge in this
case consists in establishing a lower bound on $\\#\mathrm{Hom}(G,T)$ and an
upper bound for $\\#\mathrm{Hom}(H,T)$, using only $\rho$ and generic facts
(and possibly assumptions) about pushout squares. The fact that the two
pushout squares of a DPO step share the vertical morphism $u:K\to C$ is
useful, because naively, $G={L\cup_{K}C}$ and $H={R\cup_{K}C}$, meaning that
$K$ and $C$ are factors common to $G$ and $H$.

Whatever the precise details of the approximation, it would not be very
powerful, because it simply counts morphisms into $T$, effectively assigning
each a weight of $1$. Instead, we would like to be able to differentiate
between morphisms into $T$. We therefore add more structure to $T$ by
equipping it with a set of weighted $T$-valued elements $\mathbb{E}$, which
are morphisms of the form $e:\mathit{dom}(e)\to T$, together with some weight
$\mathbf{w}(e)$ associated to them. Then morphisms $\phi:G\to T$ are assigned
a weight depending on how they relate to these weighted elements.

$=$$G$$T$$\mathit{dom}(e)$$\phi$$\alpha$$e$ (1)

A priori there are different ways of doing this, but we will count for each
$e\in\mathbb{E}$ the number $n(e)$ of commuting triangles of the form shown on
the right and compute
$\mathbf{w}(\phi)=\prod_{e\in\mathbb{E}}\mathbf{w}(e)^{n(e)}$. Next, the
weight function $\mathbf{w}$ on objects $X$ sums the weights of the individual
morphisms in $\mathrm{Hom}(G,T)$. These combinations are done formally and
more generally using a semiring structure. We define this notion of a weighted
type graph in Section 3.

The technical challenge described for the simple measure
$\mathbf{w}=\\#\mathrm{Hom}(\,\cdot\,,T)$ above returns, but takes a different
form. To measure $\mathbf{w}(G)$, we need to measure every $\phi:G\to T$, for
which in turn, we need to count, for every $e\in\mathbb{E}$, the number of
commuting triangles of the form shown in Diagram (1). In Section 4 we will
identify some assumptions that allow us to do precisely this. Intuitively, we
rely on pushouts not creating certain structure out of thin air. For general
pushouts in Graph, for instance, any node or edge in the pushout object $G$
traces back to a node or edge in $L$ or $C$ – the same is not true for loops
in $G$, which can be created by the pushout. For pushouts along monomorphisms
in Graph, however, these “traceable elements” do include loops. What we
require, then, is that $\mathbb{E}$ is traceable in this sense w.r.t. the
class of pushouts under consideration. We show that this requirement, combined
with some additional assumptions, is sufficient to precisely determine
$\mathbf{w}(G)$ and to determine an upper bound on $\mathbf{w}(H)$ for any
induced rewrite step.

In Section 5, we show how to analyze systems for termination, using weighted
type graphs that satisfy the right traceability conditions. In Section 6 we
demonstrate our technique on a number of examples. We conclude by comparing to
related work in Section 7, followed by a discussion of some directions for
future research in Section 8. All proofs may be found in Appendix 0.C. In
Appendix 0.E we provide some benchmarks from a Scala implementation.

##  2 Preliminaries

We assume an understanding of basic category theory, in particular of
pushouts, pullbacks and monomorphisms $\rightarrowtail$. Throughout this
paper, we work in a fixed category C. For an introduction to DPO graph
transformation, see [27, 21, 17].

We write Graph for the category of finite multigraphs, and SGraph for the
category of finite simple graphs (i.e., without parallel edges). The graphs
can be edge-labelled and/or node-labelled over a fixed label set.

######  Definition 1 (DPO Rewriting [21]).

A DPO rewrite rule $\rho$ is a span $K$$L$$R$$l$$r$. A diagram, as shown on
the right, defines a DPO rewrite step
${G}\Rightarrow_{\mathrm{DPO}}^{\rho,m}{H}$, i.e., a step from $G$ to $H$
using rule $\rho$ and match morphism $m:L\to G$.

$K$$L$$R$$G$$C$$H$$l$$r$$m$POPO

######  Remark 1.

Usually Definition 1 is accompanied with constraints. Most commonly, $l$ and
$m$ are required to be (regular) monic. Sometimes also the left pushout square
is restricted, e.g., it may be required that the pushout complement is minimal
or initial [7, 4, 3]. Because such restrictions affect whether a DPO rewrite
system is terminating, we will define our approach in a way that is parametric
in the variation of DPO under consideration (see Definition 13).

######  Definition 2 (Termination).

Let $R,S$ be binary relations on $\mathit{Ob}({\textbf{C}})$. Relation $R$ is
terminating relative to $S$, denoted $\mathrm{SN}(R/S)$, if every (finite or
infinite) sequence $o_{1}\mathrel{(R\cup S)}o_{2}\mathrel{(R\cup
S)}o_{3}\mathrel{(R\cup S)}o_{4}\ldots,\text{where
$o_{1},o_{2},\ldots\in\mathit{Ob}({\textbf{C}})$},$ contains only a finite
number of $R$ steps. The relation $R$ is terminating, denoted
$\mathrm{SN}(R)$, if $R$ terminates relative to the empty relation
$\varnothing$.

These concepts carry over to sets of rules via the induced rewrite relations.

We will interpret weights into a well-founded semiring as defined below.

######  Definition 3.

A monoid $\langle\,S,\cdot,e\,\rangle$ is a set $S$ with an operation
$\cdot:S\times S\to S$ and an identity element $e$ such that for all $a,b,c\in
S$: $(a\cdot b)\cdot c=a\cdot(b\cdot c)$ and $a\cdot e=a=e\cdot a$. The monoid
is commutative if for all $a,b\in S$: $a\cdot b=b\cdot a$.

######  Definition 4.

A semiring is a tuple
$\mathcal{S}=\langle\,S,\oplus,\odot,\mathbf{0},\mathbf{1}\,\rangle$ where $S$
is a set,

  1. (i)

$\langle\,S,\oplus,\mathbf{0}\,\rangle$ is a commutative monoid,

  2. (ii)

$\langle\,S,\odot,\mathbf{1}\,\rangle$ is a monoid,

  3. (iii)

$\mathbf{0}$ is an annihilator for $\odot$: for all $a\in S$ we have
$\mathbf{0}\odot a=\mathbf{0}=a\odot\mathbf{0}$, and

  4. (iv)

$\odot$ distributes over $\oplus$: for all $a,b,x\in S$ we have $(a\oplus
b)\odot x=(a\odot x)\oplus(b\odot x)$ and $x\odot(a\oplus b)=(x\odot
a)\oplus(x\odot b)$.

The semiring $\mathcal{S}$ is commutative if
$\langle\,S,\odot,\mathbf{1}\,\rangle$ is commutative. We will often denote a
semiring by its carrier set, writing $S$ for $\mathcal{S}$.

######  Definition 5.

A well-founded semiring
$\langle\,S,\oplus,\odot,\mathbf{0},\mathbf{1},\prec,\leq\,\rangle$ consists
of

  1. (i)

a semiring $\langle\,S,\oplus,\odot,\mathbf{0},\mathbf{1}\,\rangle$; and

  2. (ii)

non-empty orders ${\prec},\,{\leq}\subseteq S\times S$ for which
${\prec}\subseteq{\leq}$ and $\leq$ is reflexive;

such that $\mathrm{SN}({\succ}/{\geq})$, $\mathbf{0}\neq\mathbf{1}$, and for
all $x,x^{\prime},y,y^{\prime}\in S$ we have

$\displaystyle x\leq x^{\prime}\ \wedge\ y\leq y^{\prime}$
$\displaystyle\quad\implies\quad x\oplus y\ \leq\ x^{\prime}\oplus y^{\prime}$
(S1) $\displaystyle x\prec x^{\prime}\ \wedge\ y\prec y^{\prime}$
$\displaystyle\quad\implies\quad x\oplus y\ \prec\ x^{\prime}\oplus
y^{\prime}$ (S2) $\displaystyle x\leq x^{\prime}\ \wedge\ \mathbf{1}\leq y$
$\displaystyle\quad\implies\quad x\odot y\ \leq\ x^{\prime}\odot y$ (S3)
$\displaystyle x\prec x^{\prime}\ \wedge\ \mathbf{1}\leq y\neq\mathbf{0}$
$\displaystyle\quad\implies\quad x\odot y\ \prec\ x^{\prime}\odot y$ (S4)

The semiring is strictly monotonic if additionally

$\displaystyle x\prec x^{\prime}\ \wedge\ y\leq y^{\prime}$
$\displaystyle\quad\implies\quad x\oplus y\ \prec\ x^{\prime}\oplus
y^{\prime}$ (S5)

######  Example 1.

The arithmetic semiring $\langle\,\mathbb{N},+,\cdot,0,1,<,\leq\,\rangle$ is a
strictly monotonic, well-founded semiring. The tropical semiring
$\langle\,\mathbb{N}\cup\\{\infty\\},\min,+,\infty,0,<,\leq\,\rangle$ and
arctic semiring
$\langle\,\mathbb{N}\cup\\{-\infty\\},\max,+,-\infty,0,<,\leq\,\rangle$ are
well-founded semirings, but not strictly monotone. (For details see Examples
9, 10, 11.)

##  3 Weighted Type Graphs

In this section, we introduce a notion of weighted type graphs for arbitrary
categories, and we employ them to weigh morphisms (into the type graph) and
objects in the category.

######  Definition 6.

A weighted type graph $\mathcal{T}=(T,\mathbb{E},S,\mathbf{w})$ consists of:

  1. (i)

an object $T\in\mathit{Ob}({\textbf{C}})$, called a type graph,

  2. (ii)

a set $\mathbb{E}$ of $T$-valued elements $e:\mathit{dom}(e)\to T$,

  3. (iii)

a commutative semiring
$\langle\,S,\oplus,\odot,\mathbf{0},\mathbf{1}\,\rangle$, and

  4. (iv)

a weight function $\mathbf{w}:\mathbb{E}\to S$ such that, for all
$e\in\mathbb{E}$, $\mathbf{0}\neq\mathbf{w}(e)\geq\mathbf{1}$.

The weighted type graph $\mathcal{T}$ is finitary if, for every
$e\in\mathbb{E}$ and every $G\in\mathit{Ob}({\textbf{C}})$,
$\mathrm{Hom}(\mathit{dom}(e),G)$ and $\mathrm{Hom}(G,T)$ are finite sets.

######  Remark 2.

Bruggink et al. [9] introduce weighted type graphs for the category Graph of
edge-labelled multigraphs. We generalize this concept to arbitrary categories.
Important technical issues aside (discussed below), their notion is obtained
by instantiating our notion of weighted type graphs for Graph with
$\smash{\mathbb{E}=\bigcup\;\\{\,\mathrm{Hom}(\,\leavevmode\hbox
to21.91pt{\vbox to13.77pt{\pgfpicture\makeatletter\hbox{\hskip
0.99583pt\lower-2.59998pt\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{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}\pgfsys@moveto{0.99583pt}{0.0pt}\pgfsys@curveto{0.99583pt}{0.54999pt}{0.54999pt}{0.99583pt}{0.0pt}{0.99583pt}\pgfsys@curveto{-0.54999pt}{0.99583pt}{-0.99583pt}{0.54999pt}{-0.99583pt}{0.0pt}\pgfsys@curveto{-0.99583pt}{-0.54999pt}{-0.54999pt}{-0.99583pt}{0.0pt}{-0.99583pt}\pgfsys@curveto{0.54999pt}{-0.99583pt}{0.99583pt}{-0.54999pt}{0.99583pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{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}}}
{{{{}}}}{{}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}\pgfsys@moveto{20.91277pt}{0.0pt}\pgfsys@curveto{20.91277pt}{0.54999pt}{20.46692pt}{0.99583pt}{19.91693pt}{0.99583pt}\pgfsys@curveto{19.36694pt}{0.99583pt}{18.9211pt}{0.54999pt}{18.9211pt}{0.0pt}\pgfsys@curveto{18.9211pt}{-0.54999pt}{19.36694pt}{-0.99583pt}{19.91693pt}{-0.99583pt}\pgfsys@curveto{20.46692pt}{-0.99583pt}{20.91277pt}{-0.54999pt}{20.91277pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{19.91693pt}{0.0pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{19.91693pt}{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@moveto{3.84111pt}{0.0pt}\pgfsys@lineto{15.67583pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{15.87582pt}{0.0pt}\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}{7.10083pt}{3.533pt}\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{{$x$}}
}}\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}}\,,T)\mid x\text{ an
edge label}\,\\}}$.

The technical differences are as follows. We require
$\mathbf{w}(e)\geq\mathbf{1}$ and $\mathbf{w}(e)\neq\mathbf{0}$ for every
$e\in\mathbb{E}$. The work [9] requires

  * •

$\mathbf{w}(e)>\mathbf{0}$ only for loops $e\in\mathbb{E}$ on a distinguished
‘flower node’.

It turns out that this condition is insufficient, causing [9, Theorem 2] to
fail as illustrated by Example 8. The authors of [9] have confirmed and solved
this problem in their latest arXiv version [10].

Moreover, observe that $\mathbf{w}(e)\geq\mathbf{1}$ is often a weaker
condition than $\mathbf{w}(e)>\mathbf{0}$. For instance, in the tropical
semiring (see Example 10), $\mathbf{0}<\mathbf{1}$ does not hold since there
$\mathbf{0}=+\infty$ and $\mathbf{1}=0$. The tropical semiring is one of the
prime examples in [9], but, in fact, the condition $\mathbf{w}(e)>\mathbf{0}$
rules out the use of the tropical semiring.

######  Notation 3.1.

We use the following notation:

  1. (a)

For $\alpha:A\to B$, $x:A\to C$, let
$\\{\,{-}\circ\alpha=x\,\\}\;=\;\\{\,\phi:B\to C\mid\phi\circ\alpha=x\,\\}$;

  2. (b)

For $\alpha:B\to C$, $x:A\to C$, let
$\\{\,\alpha\circ{-}=x\,\\}\;=\;\\{\,\phi:A\to B\mid\alpha\circ\phi=x\,\\}$;

  3. (c)

For $\alpha:B\to C$ and a set $S$ of morphisms $\phi:A\to B$, we define
$\alpha\circ S\;=\;\\{\,\alpha\circ\phi\mid\phi\in S\,\\}$.

######  Definition 7 (Weighing morphisms and objects).

Let $\mathcal{T}=(T,\mathbb{E},S,\mathbf{w})$ be a finitary weighted type
graph and let $G,A\in\mathit{Ob}({\textbf{C}})$.

  1. (i)

The weight of a morphism $\phi:G\to T$ is
$\displaystyle\mathbf{w}_{\mathcal{T}}(\phi)=\bigodot_{e\in\mathbb{E}}\mathbf{w}(e)^{\\#\\{\,\phi\circ{-}=e\,\\}}$.
This is equivalent to
$\displaystyle\mathbf{w}_{\mathcal{T}}(\phi)\;=\bigodot_{{\scriptsize\begin{array}[]{@{}c@{}}e\in\mathbb{E}\\\
\alpha\in\\{\,{\phi\circ{-}}=e\,\\}\end{array}}}\mathbf{w}(e)$; visually
$=$$G$$T$$\mathit{dom}(e)$$\phi$$\alpha$$e$.

  2. (ii)

The weight of finite $\Psi\subseteq\\{\,\phi\mid\phi:G\to T\,\\}$ is
$\mathbf{w}_{\mathcal{T}}(\Psi)=\bigoplus_{\phi\in\Psi}\mathbf{w}_{\mathcal{T}}(\phi)$.

  3. (iii)

The weight of an object $G\in\mathit{Ob}({\textbf{C}})$ is
$\mathbf{w}_{\mathcal{T}}(G)=\mathbf{w}_{\mathcal{T}}(\mathrm{Hom}(G,T))$.

  4. (iv)

The weight of $\phi:G\to T$ excluding $(\alpha\circ{-})$, for $\alpha:A\to G$,
is

$\displaystyle\mathbf{w}_{\mathcal{T}}(\phi-(\alpha\circ{-}))$
$\displaystyle\;=\;\bigodot_{e\in\mathbb{E}}\mathbf{w}(e)^{\\#\\{\,\tau\in\\{\,\phi\circ{-}=e\,\\}\mid\not\exists\zeta.\
\tau={\alpha\circ\zeta}\,\\}}$

In other words, we count all $\tau$ such that

for all $\zeta:\mathit{dom}(e)\to A$, we have the following:

$G$$T$$\mathit{dom}(e)$$A$$\neq$$=$$\phi$$\alpha$$e$$\tau$$\zeta$

Observe the analogy to weighted automata where the weight of a word is the sum
of the weights of all runs, and the weight of a run is the product of the edge
weights.

##  4 Weighing Pushouts

In this section, we introduce techniques for determining exact and upper
bounds on the weights of pushout objects in terms of the corresponding pushout
span. For these techniques to work, we need certain assumptions on the pushout
squares. This concerns, in particular, traceability of elements (Section 4.1)
and relative monicity conditions (Section 4.2), which are used to define the
notion of weighable pushout squares (Section 4.3). Using the notion of a
weighable pushout square, we can bound weights of morphisms out of the pushout
object (Section 4.4), and consequently bound the weight of the pushout object
itself (Section 4.5).

###  4.1 Traceability

We introduce the concept of traceability of elements
$X\in\mathit{Ob}({\textbf{C}})$ along pushout squares. Roughly speaking,
traceability guarantees that the pushout cannot create occurrences of $X$ out
of thin air.

######  Definition 8 (Traceability).

Let $\Delta$ be a class of pushout squares. An object
$X\in\mathit{Ob}({\textbf{C}})$ is called traceable along $\Delta$ if:
whenever we have a configuration as displayed on the right, such that the
displayed square is from $\Delta$, then (a) there exists a $g:X\to B$ such
that $f=\beta^{\prime}g$, or (b) there exists an $h:X\to C$ such that
$f=\alpha^{\prime}h$. If additionally, whenever (a) and (b) hold together,
then also (c) there exists an $i:X\to A$ such that $f=\beta^{\prime}\alpha i$,
then we say that $X$ is strongly traceable along $\Delta$.
$A$$B$$C$$D$$X$$\alpha$$\beta$$\beta^{\prime}$$\alpha^{\prime}$$f$$\Delta$

In $\mathcal{M}$-adhesive categories (for $\mathcal{M}$ a stable class of
monos) [20, Definition 2.4], pushouts along $\mathcal{M}$-morphisms are also
pullbacks [28, Lemma 13]. This is a common setting for graph transformation.
In this case, the notions of traceability and strong traceability coincide for
pushouts along $\mathcal{M}$-morphisms, as the proposition below shows.

######  Proposition 1.

If $\Delta$ is a class of pushouts that are also pullbacks, then traceability
along $\Delta$ implies strong traceability along $\Delta$ (for
$X\in\mathit{Ob}({\textbf{C}})$).

######  Remark 3 (Traceability in Graph).

In Graph, the objects  and $x$ (for edge labels $x$) are the only (non-
initial) objects that are (strongly) traceable along all pushout squares.
Other objects, such as loops  , are strongly traceable if all morphisms in the
square are monomorphisms.

######  Remark 4 (Traceability in SGraph).

In the category of simple graphs SGraph, object  is strongly traceable along
all pushout squares. An object $X=\,\leavevmode\hbox to21.91pt{\vbox
to13.77pt{\pgfpicture\makeatletter\hbox{\hskip 0.99583pt\lower-2.59998pt\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{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}\pgfsys@moveto{0.99583pt}{0.0pt}\pgfsys@curveto{0.99583pt}{0.54999pt}{0.54999pt}{0.99583pt}{0.0pt}{0.99583pt}\pgfsys@curveto{-0.54999pt}{0.99583pt}{-0.99583pt}{0.54999pt}{-0.99583pt}{0.0pt}\pgfsys@curveto{-0.99583pt}{-0.54999pt}{-0.54999pt}{-0.99583pt}{0.0pt}{-0.99583pt}\pgfsys@curveto{0.54999pt}{-0.99583pt}{0.99583pt}{-0.54999pt}{0.99583pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{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}}}
{{{{}}}}{{}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}\pgfsys@moveto{20.91277pt}{0.0pt}\pgfsys@curveto{20.91277pt}{0.54999pt}{20.46692pt}{0.99583pt}{19.91693pt}{0.99583pt}\pgfsys@curveto{19.36694pt}{0.99583pt}{18.9211pt}{0.54999pt}{18.9211pt}{0.0pt}\pgfsys@curveto{18.9211pt}{-0.54999pt}{19.36694pt}{-0.99583pt}{19.91693pt}{-0.99583pt}\pgfsys@curveto{20.46692pt}{-0.99583pt}{20.91277pt}{-0.54999pt}{20.91277pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{19.91693pt}{0.0pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{19.91693pt}{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@moveto{3.84111pt}{0.0pt}\pgfsys@lineto{15.67583pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{15.87582pt}{0.0pt}\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}{7.10083pt}{3.533pt}\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{{$x$}}
}}\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}}\,$ (for an edge label
$x$) is traceable along all pushout squares, but not necessarily strongly
traceable.

The pushout on the right is a counterexample. However, using Proposition 1, we
have that $X$ is strongly traceable along pushout squares in which one of the
span morphisms $\alpha$ or $\beta$ is a regular monomorphism, because such
pushouts are pullbacks in SGraph (and more generally in quasitoposes).

$x$$x$$x$PO

######  Remark 5.

As is well known, the category of unlabeled graphs is equivalent to the
functor category $[\leavevmode\hbox to29.8pt{\vbox
to10.16pt{\pgfpicture\makeatletter\hbox{\hskip 4.80566pt\lower-5.07935pt\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{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{ }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-3.40279pt}{-3.41666pt}\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{{E}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\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}{16.16693pt}{-3.41666pt}\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{{V}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{}}{{{}}{{}}}{}{{}}{}{{}}{{{}}{{}}}{}
{}{}{}{}{}{}{{}}\pgfsys@moveto{7.65094pt}{1.99168pt}\pgfsys@lineto{11.59232pt}{1.99168pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{11.79231pt}{1.99168pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} {{}}{{{}}{{}}}{}{{}}{}{{}}{{{}}{{}}}{}
{}{}{}{}{}{}{{}}\pgfsys@moveto{7.65094pt}{-1.99168pt}\pgfsys@lineto{11.59232pt}{-1.99168pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{11.79231pt}{-1.99168pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\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}}\,,{\textbf{Set}}]$,
where index category EV is the category consisting of two objects $E$ and $V$
and two non-identity arrows that are parallel. This makes the category of
unlabeled graphs a presheaf category, and the two representable functors for
this category are precisely the one node graph $\cdot$ and the one edge graph
$\cdot\to\cdot$ (see [41, Section 3] for more detail). We identified these two
graphs as non-initial objects that are strongly traceable along any pushout
(Remark 3). Our conjecture is that for any presheaf category for which the
index category is small and acyclic, the non-initial strongly traceable
objects for any pushout are precisely the representable functors. For many
examples of such presheaf categories, see the overview provided by Löwe [31,
Section 3.1] (there called graph structures).

###  4.2 Relative Monicity

Traceability suffices to derive an upper bound on the weight of a pushout.
However, we need additional monicity assumptions for lower or exact bounds.

######  Definition 9 (Relative monicity).

A morphism $f:A\to B$ is called

  1. (i)

monic for $S\subseteq\mathrm{Hom}(-,A)$ if $fg=fh\implies g=h$ for all $g,h\in
S$,

  2. (ii)

$X$-monic, where $X\in\mathit{Ob}({\textbf{C}})$, if $f$ is monic for
$\mathrm{Hom}(X,A)$, and

  3. (iii)

$X$-monic outside of $u$, where $X\in\mathit{Ob}({\textbf{C}})$ and $u:C\to
A$, if $f$ is monic for $\mathrm{Hom}(X,A)-u\circ\mathrm{Hom}(X,C)$.

For $\Gamma\subseteq\mathit{Ob}({\textbf{C}})$, $f$ is called $\Gamma$-monic
if $f$ is $X$-monic for every $X\in\Gamma$. When $\Gamma$ is clear from the
context, $A$$B$denotes a $\Gamma$-monic morphism from $A$ to $B$.

######  Example 2 (Edge-Monicity).

In Graph, let $\Gamma=\\{\,\leavevmode\hbox to21.91pt{\vbox
to13.77pt{\pgfpicture\makeatletter\hbox{\hskip 0.99583pt\lower-2.59998pt\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{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}\pgfsys@moveto{0.99583pt}{0.0pt}\pgfsys@curveto{0.99583pt}{0.54999pt}{0.54999pt}{0.99583pt}{0.0pt}{0.99583pt}\pgfsys@curveto{-0.54999pt}{0.99583pt}{-0.99583pt}{0.54999pt}{-0.99583pt}{0.0pt}\pgfsys@curveto{-0.99583pt}{-0.54999pt}{-0.54999pt}{-0.99583pt}{0.0pt}{-0.99583pt}\pgfsys@curveto{0.54999pt}{-0.99583pt}{0.99583pt}{-0.54999pt}{0.99583pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{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}}}
{{{{}}}}{{}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}\pgfsys@moveto{20.91277pt}{0.0pt}\pgfsys@curveto{20.91277pt}{0.54999pt}{20.46692pt}{0.99583pt}{19.91693pt}{0.99583pt}\pgfsys@curveto{19.36694pt}{0.99583pt}{18.9211pt}{0.54999pt}{18.9211pt}{0.0pt}\pgfsys@curveto{18.9211pt}{-0.54999pt}{19.36694pt}{-0.99583pt}{19.91693pt}{-0.99583pt}\pgfsys@curveto{20.46692pt}{-0.99583pt}{20.91277pt}{-0.54999pt}{20.91277pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{19.91693pt}{0.0pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{19.91693pt}{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@moveto{3.84111pt}{0.0pt}\pgfsys@lineto{15.67583pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{15.87582pt}{0.0pt}\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}{7.10083pt}{3.533pt}\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{{$x$}}
}}\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}}\,\mid x\text{ is an
edge label}\\}$. A morphism $f:G\to H$ that does not identify edges (but may
identify nodes) is not necessarily monic, but it is $\Gamma$-monic. In this
particular case for Graph, we will say that $f$ is edge-monic.

###  4.3 Weighable Pushout Squares

The following definition introduces an orientation for pushout squares,
distinguishing between horizontal and vertical morphisms. A double pushout
rewrite step with respect to a rule consists of two oriented pushout squares.
For both squares, $\beta$ is the shared morphism, and $\alpha$ will be $l$ or
$r$ of the rule span, respectively. For the left square, $\beta^{\prime}$ is
the match morphism. The distinction between horizontal and vertical morphisms
will be used in Definition 11 below to impose different conditions on these
morphisms.

######  Definition 10 (Oriented pushout squares).

An oriented pushout square

$\tau$ is a pushout square (as shown on the right) with a fixed orientation.
We distinguish the morphisms into horizontal and vertical. Morphisms $\beta$
and $\beta^{\prime}$ are vertical and $\alpha$ and $\alpha^{\prime}$ are
horizontal.

We denote the pushout square by
$\langle\,C\stackrel{{\scriptstyle\beta}}{{\leftarrow}}A\stackrel{{\scriptstyle\alpha}}{{\to}}B;\;C\stackrel{{\scriptstyle\alpha^{\prime}}}{{\to}}D\stackrel{{\scriptstyle\beta^{\prime}}}{{\leftarrow}}B\,\rangle$
where the order of the morphisms in the span is vertical before horizontal,
and the order of the morphisms in the cospan is horizontal before vertical.

$A$$B$$C$$D$$\alpha$$\beta$$\beta^{\prime}$$\alpha^{\prime}$PO

The following definition summarizes the conditions required to derive an upper
or exact bound on the weight of a pushout object.

######  Definition 11 (Weighable pushout square).

Let $\mathcal{T}=(T,\mathbb{E},S,\mathbf{w})$ be a finitary weighted type
graph. Let $\delta$ be the oriented pushout square from Definition 10. We say
that $\delta$ is

  1. (a)

weighable with $\mathcal{T}$ if:

    1. (i)

$\mathit{dom}(\mathbb{E})$ is strongly traceable along $\delta$,

    2. (ii)

$\beta^{\prime}$ is $\mathit{dom}(\mathbb{E})$-monic, and

    3. (iii)

$\alpha^{\prime}$ is $\mathit{dom}(\mathbb{E})$-monic outside of $\beta$.

  2. (b)

bounded above by $\mathcal{T}$ if $\mathit{dom}(\mathbb{E})$ is traceable
along $\delta$.

###  4.4 Weighing Morphisms Rooted in Pushout Objects

Consider the pushout diagram in Lemma 1, below. The lemma decomposes the
weight $\mathbf{w}(\phi)$ of the morphism $\phi$, rooted in the pushout
object, into the product of the weights $\mathbf{w}(\phi\circ\beta^{\prime})$
and $\mathbf{w}(\phi\circ\alpha^{\prime}-(\beta\circ{-}))$. Intuitively, the
reasoning is as follows. Let $e\in\mathbb{E}$ be a weighted element. Assume
that $e:\mathit{dom}(e)\to T$ occurs in $\phi$, that is, there exists
$d:\mathit{dom}(e)\to D$ with $e=\phi\circ d$. Then traceability guarantees
that this occurrence $d$ can be traced back to $\phi\circ\beta^{\prime}$ or
$\phi\circ\alpha^{\prime}$. In case the occurrence $d$ traces back all the way
to $A$ (to
$\phi\circ\beta^{\prime}\circ\alpha=\phi\circ\alpha^{\prime}\circ\beta$), then
it occurs in both $\phi\circ\beta^{\prime}$ and $\phi\circ\alpha^{\prime}$. To
avoid unnecessary double counting, we exclude those elements from
$\phi\circ\alpha^{\prime}$, giving rise to
$\mathbf{w}(\phi\circ\alpha^{\prime}-(\beta\circ{-}))$. In this way, we obtain
the following upper bound on the weight of $\phi$:

$\displaystyle\mathbf{w}(\phi)\ \leq\
\mathbf{w}(\phi\circ\beta^{\prime})\odot\mathbf{w}(\phi\circ\alpha^{\prime}-(\beta\circ{-}))$

To obtain the precise weight we need to avoid double counting. First, we need
strong traceability to exclude all double counting between
$\phi\circ\beta^{\prime}$ and $\phi\circ\alpha^{\prime}-(\beta\circ{-})$.
Second, we need $\mathit{dom}(\mathbb{E})$-monicity of $\alpha^{\prime}$
outside of $\beta$ and $\mathit{dom}(\mathbb{E})$-monicity of $\beta^{\prime}$
to avoid double counting along these morphisms.

######  Lemma 1 (Weighing morphisms rooted in pushout objects).

Let a finitary weighted type graph $\mathcal{T}=(T,\mathbb{E},S,\mathbf{w})$
be given. Consider an oriented pushout square $\delta$:

$A$$B$$C$$D$$T$$\alpha$$\beta$$\beta^{\prime}$$\alpha^{\prime}$$\phi$$\delta$

We define
$k=\mathbf{w}_{\mathcal{T}}(\phi\circ\beta^{\prime})\odot\mathbf{w}_{\mathcal{T}}(\phi\circ\alpha^{\prime}-(\beta\circ{-}))$.
Then the following holds:

  1. (A)

We have $\mathbf{w}_{\mathcal{T}}(\phi)=k$ if $\delta$ is weighable with
$\mathcal{T}$.

  2. (B)

We have $\mathbf{w}_{\mathcal{T}}(\phi)\leq k$ if $\delta$ is bounded above by
$\mathcal{T}$.

######  Remark 6 (Related work).

Lemma 1 is closely related to Lemma 2 of [9] which establishes
$\mathbf{w}(\phi)=\mathbf{w}(\phi\circ\beta^{\prime})\odot\mathbf{w}(\phi\circ\alpha^{\prime})$
for directed, edge-labelled multigraphs under the following assumptions:

  1. (i)

the interface $A$ must be discrete (contains no edges),

  2. (ii)

the weighted type graph has only edge weights (no node weights).

As a consequence of the discrete interface $A$, all arrows involved in the
pushout are edge-monic (Example 2).

Lemma 1 generalizes Lemma 2 of [9] in multiple directions:

  1. (a)

it works for arbitrary categories with some (strongly) traceable
$\mathit{dom}(\mathbb{E})$,

  2. (b)

it does not require discreteness ($\mathit{dom}(\mathbb{E})$-freeness) of the
interface, and

  3. (c)

it allows for $\alpha$ and $\alpha^{\prime}$ that are not
$\mathit{dom}(\mathbb{E})$-monic.

Both (a) and (b) are crucial to make the termination techique applicable in
general categories, and (c) is important to allow for rewrite rules whose
right morphism merges elements that we are weighing.

###  4.5 Weighing Pushout Objects

The following lemma (cf. [9, Lemma 1]) is a direct consequence of the
universal property of pushouts. We will use this property for weighing pushout
objects:

$A$$B$$C$$D$$\delta$$\alpha$$\beta$$\beta^{\prime}$$\alpha^{\prime}$ (2)

######  Lemma 2 (Pushout morphisms).

Let $T\in\mathit{Ob}({\textbf{C}})$ and consider a pushout square as in (2).
For every morphism $t_{A}:A\to T$, there is a bijection $\theta$ from

  1. (a)

the class $U$ of morphisms $t_{D}:D\to T$ for which
$t_{A}=t_{D}\circ\beta^{\prime}\circ\alpha$, to

  2. (b)

the class $P$ of pairs $(t_{B}:B\to T,\;t_{C}:C\to T)$ of morphisms for which
$t_{A}=t_{B}\circ\alpha=t_{C}\circ\beta$,

such that for all $t_{D}\in U$ and pairs $(t_{B},t_{C})\in P$,
$\theta(t_{D})=(t_{B},t_{C})\;\iff\;t_{B}=t_{D}\circ\beta^{\prime}\text{ and
}t_{C}=t_{D}\circ\alpha^{\prime}$.

######  Lemma 3 (Weighing pushout objects).

Let $\mathcal{T}=(T,\mathbb{E},S,\mathbf{w})$ be a finitary weighted type
graph. Consider an oriented pushout square $\delta$ as in (2). Define

$\displaystyle k$ $\displaystyle=\bigoplus_{t_{A}:A\to
T}\;\Big{(}\bigoplus_{\begin{subarray}{c}t_{C}:C\to T\\\
t_{A}=t_{C}\circ\beta\end{subarray}}\mathbf{w}(t_{C}-\beta)\Big{)}\odot\underbrace{\Big{(}\bigoplus_{\begin{subarray}{c}t_{B}:B\to
T\\\
t_{A}=t_{B}\circ\alpha\end{subarray}}\mathbf{w}(t_{B})\Big{)}}_{=\mathbf{w}(\\{\,{-}\circ\alpha=t_{A}\,\\})}$

Then the following holds:

  1. (A)

We have $\mathbf{w}_{\mathcal{T}}(D)=k$ if $\delta$ is weighable with
$\mathcal{T}$.

  2. (B)

We have $\mathbf{w}_{\mathcal{T}}(D)\leq k$ if $\delta$ is bounded above by
$\mathcal{T}$.

##  5 Termination via Weighted Type Graphs

In the previous section, we have developed techniques for weighing pushout
objects. Our next goal is to apply these techniques to the pushout squares of
double pushout diagrams in order to prove that rewrite steps reduce the
weight.

As we have already noted in Remark 1, there exist many variations of the
general concept of double pushout graph transformation. To keep our treatment
as general as possible, we introduce in Section 5.1 an abstract concept of a
double pushout framework $\mathfrak{F}$ which maps rules $\rho:L\leftarrow
K\to R$ to classes $\mathfrak{F}(\rho)$ of double pushout diagrams with top
span $\rho$.

In order to prove that rewrite steps decrease the weight, we need to ensure
that every object that can be rewritten admits some morphism into the weighted
type graph. To this end, we introduce the concept of context closures of rules
in Section 5.2. In Section 5.3, we prove that rewrite steps are decreasing
(Theorem 0.C.1) if the rules satisfy certain criteria (Definition 16).
Finally, we state our main theorem (Theorem 5.1) for proving (relative)
termination.

###  5.1 Double Pushout Frameworks

######  Definition 12.

A double pushout diagram $\delta$ is a diagram of the form

$K$$L$$R$$G$$C$$H$$l$$r$$m$$u$$w$$l^{\prime}$$r^{\prime}$POPO

This diagram $\delta$ is a witness for the rewrite step
$G\Rightarrow^{\delta}H$. We use the following notation for the left and the
right square of the diagram, respectively:

$\displaystyle\textit{left}(\delta)$
$\displaystyle=\langle\,C\stackrel{{\scriptstyle
u}}{{\leftarrow}}K\stackrel{{\scriptstyle
l}}{{\to}}L;\;C\stackrel{{\scriptstyle
l^{\prime}}}{{\to}}G\stackrel{{\scriptstyle m}}{{\leftarrow}}L\,\rangle$
$\displaystyle\textit{right}(\delta)$
$\displaystyle=\langle\,C\stackrel{{\scriptstyle
u}}{{\leftarrow}}K\stackrel{{\scriptstyle
r}}{{\to}}R;\;C\stackrel{{\scriptstyle
r^{\prime}}}{{\to}}H\stackrel{{\scriptstyle w}}{{\leftarrow}}R\,\rangle$

Both $\textit{left}(\delta)$ and $\textit{right}(\delta)$ are oriented pushout
squares (where $u$ is vertical). For a class $\Delta$ of double pushout
diagrams, we define
$\textit{left}(\Delta)=\\{\,\textit{left}(\delta)\mid\delta\in\Delta\,\\}$ and
$\textit{right}(\Delta)=\\{\,\textit{right}(\delta)\mid\delta\in\Delta\,\\}$.

######  Definition 13 (Double pushout framework).

A double pushout framework $\mathfrak{F}$ is a mapping of DPO rules to classes
of DPO diagrams such that, for every DPO rule $\rho$, $\mathfrak{F}(\rho)$ is
a class of DPO diagrams with top-span $\rho$.

The rewrite relation $\Rightarrow_{\rho,\mathfrak{F}}$ induced by a DPO rule
$\rho$ in $\mathfrak{F}$ is defined as follows:
$G\Rightarrow_{\rho,\mathfrak{F}}H$ iff $G\Rightarrow^{\delta}H$ for some
$\delta\in\mathfrak{F}(\rho)$. The rewrite relation
$\Rightarrow_{\mathfrak{S},\mathfrak{F}}$ induced by a set $\mathfrak{S}$ of
DPO rules is given by: $G\Rightarrow_{\mathfrak{S},\mathfrak{F}}H$ iff
$G\Rightarrow_{\rho,\mathfrak{F}}H$ for some $\rho\in\mathfrak{S}$. When
$\mathfrak{F}$ is clear from the context, we suppress $\mathfrak{F}$ and write
$\Rightarrow_{\rho}$ and $\Rightarrow_{\mathfrak{S}}$.

###  5.2 Context Closures

For proving termination, we need to establish that every rewrite step causes a
decrease in the weight of the host graph. In particular, we need to ensure
that every host graph admits some morphism into the weighted type graph. For
this purpose, we introduce the concept of a context closure. Intuitively, a
context closure for a rule $L\leftarrow K\to R$ is a morphism $c:L\to T$ into
the type graph $T$ in such a way that every match $L\to G$ can be mapped
‘around $c$’.

######  Definition 14 (Context closure).

Let $\mathcal{A}$ be a class of morphisms. A context closure of an object
$L\in\mathit{Ob}({\textbf{C}})$ for class $\mathcal{A}$ is an arrow $c:L\to T$
such that, for every arrow $\alpha:L\to G$ in $\mathcal{A}$, there exists a
morphism $\beta:G\to T$ with $c=\beta\circ\alpha$. This can be depicted as

$=$$G$$T$$L$$\beta$$\alpha$$c$

######  Remark 7 (Partial map classifiers as context closures).

The notion of a context closure is strictly weaker than a partial map
classifier. If category C has an $\mathcal{M}$-partial map classifier
$(T,\eta)$ (see [1, Definition 28.1] and [15, Definition 5]) for a stable
class of monics $\mathcal{M}$, then the $\mathcal{M}$-partial map classifier
arrow $\eta_{X}:X\hookrightarrow T(X)$ for an object $X$ is a context closure
of $X$ for $\mathcal{M}$, because for any $\alpha:X\hookrightarrow Z$ in
$\mathcal{M}$ there exists a unique $\beta:Z\to T(X)$ making the following
square a pullback:

$X$$T(X)$$X$$Z$$\eta_{X}$$\beta$$\alpha$PB

######  Definition 15 (Context closure for a rule).

Let $\mathfrak{F}$ be a DPO framework and $\rho$ a DPO rule
$L\stackrel{{\scriptstyle}}{{\leftarrow}}K\stackrel{{\scriptstyle}}{{\to}}R$.
A context closure for $\rho$ and $T$ (in $\mathfrak{F}$) is a context closure
$c:L\to T$ for the class of match morphisms occurring in $\mathfrak{F}(\rho)$.

######  Remark 8 (Context closures for unrestricted matching).

Consider a DPO rule $\rho\;=\;{L\leftarrow K\to R}$ in an arbitrary DPO
framework $\mathfrak{F}$ (in particular, matching can be unrestricted). Every
morphism $c:L\to 1\to T$, that factors through the terminal object $1$, is a
context closure for $\rho$ and $T$ in $\mathfrak{F}$.

This particular choice of a context closure generalizes the flower nodes from
[9] which are defined specifically for the category of edge-labelled
multigraphs. A flower node [9] in a graph $T$ is just a morphism $1\to T$.

When employing such context closures, we establish termination with respect to
unrestricted matching. This is bound to fail if termination depends on the
matching restrictions.

######  Remark 9 (Increasing the power for monic matching).

For rules $L\stackrel{{\scriptstyle l}}{{\leftarrow}}K\stackrel{{\scriptstyle
r}}{{\to}}R$ with monic matching, it is typically fruitful to choose a type
graph $T$ and context closure $c:L\to T$ in such a way that $c$ avoids
collapsing $l(K)$ in $L$. In other words, the context closure $c$ should be
monic for $\\{\,l\circ h\mid h\in\mathrm{Hom}(-,K)\,\\}$. In the case that $l$
is monic, this is equivalent to $c\circ l$ being monic.

For Graph, the intuition is as follows. When collapsing nodes of $l(K)$ along
$c$, we actually prove a stronger termination property than intended. We then
prove termination even if matches $m:L\to G$ are allowed to collapse those
nodes.

######  Example 3 (Context closure for monic matching).

Let $\rho$ be the DPO rule

$L$$x$$y$$z$$K$$x$$y$$R$$x$$y$$w$$l$$r$

from [34, Example 55] in Graph with a framework $\mathfrak{F}$ with monic
matching.

Following Remark 9, we construct a context closure $c:L\to T$ for $\rho$ that
avoids collapsing $l(K)$ of $L$. Since $l(K)\cong K$, this means that the
complete graph around the nodes of $K$ must be a subobject of $T$. We pick

$L$$x$$y$$z$$T$$x$$y$$z$$u$$c$

Indeed, for every monic match $m:L\rightarrowtail G$ there exists a morphism
$\alpha:G\to T$ such that $c=\alpha\circ m$. Thus $c$ is a context closure for
$\rho$ and $T$ in $\mathfrak{F}$.

###  5.3 Proving Termination

In this section we prove our main theorem (Theorem 5.1) for using weighted
type graphs to prove termination of graph transformation systems.

First, we introduce different notions of decreasing rules (Defintion 16). Then
we prove that rewrite steps arising from these rules cause a decrease in the
weight of the host graphs (Theorem 0.C.1). Finally, we summarize our technique
for proving (relative) termination (Theorem 5.1).

The following definition introduces the notions of weakly, uniformly and
closure decreasing rules. Weakly decreasing rules never increase the weight of
the host graph. Uniformly decreasing rules reduce the weight of the host graph
for every mapping of the host graph onto the type graph. If the underlying
semiring is strictly monotonic, then closure decreasingness suffices: the
weight of the host graph decreases for those mappings that correspond to the
context closure of the rule (and is non-increasing for the other mappings).

######  Definition 16 (Decreasing rules).

Let $\mathfrak{F}$ be a DPO framework. Moreover, let
$\mathcal{T}=(T,\mathbb{E},S,\mathbf{w})$ be a finitary weighted type graph
over a well-founded commutative semiring
$\langle\,S,\oplus,\odot,\mathbf{0},\mathbf{1},\prec,\leq\,\rangle$. A DPO
rule $\rho:L\stackrel{{\scriptstyle l}}{{\leftarrow}}K\stackrel{{\scriptstyle
r}}{{\to}}R$ is called

  1. (i)

weakly decreasing (w.r.t. $\mathcal{T}$ in $\mathfrak{F}$) if

     * •

$\mathbf{w}(\\{\,{-}\circ l=t_{K}\,\\})\geq\mathbf{w}(\\{\,{-}\circ
r=t_{K}\,\\})$ for every $t_{K}:K\to T$;

  2. (ii)

uniformly decreasing (w.r.t. $\mathcal{T}$ in $\mathfrak{F}$) if

     * •

for every $t_{K}:K\to T$:
$\mathbf{w}(\\{\,{-}\circ l=t_{K}\,\\})\succ\mathbf{w}(\\{\,{-}\circ
r=t_{K}\,\\})$ or
$\\{\,{-}\circ l=t_{K}\,\\}=\varnothing=\\{\,{-}\circ r=t_{K}\,\\}$, and

     * •

there exists a context closure $\mathfrak{c}_{\rho}$ for $\rho$ and $T$ in
$\mathfrak{F}$;

If semiring $S$ is moreover strictly monotonic, we say that $\rho$ is

  1. (iii)

closure decreasing (w.r.t. $\mathcal{T}$ in $\mathfrak{F}$) if

     * •

$\rho$ is weakly decreasing,

     * •

there exists a context closure $\mathfrak{c}_{\rho}$ for $\rho$ and $T$ in
$\mathfrak{F}$, and

     * •

$\mathbf{w}(\\{\,{-}\circ l=t_{K}\,\\})\succ\mathbf{w}(\\{\,{-}\circ
r=t_{K}\,\\})$ for $t_{K}=\mathfrak{c}_{\rho}\circ l$.

By saying that a rule is closure decreasing, we tacitly assume that the
semiring is strictly monotonic (for otherwise the concept is not defined).
Note that if $S$ is strictly monotonic, uniformly decreasing implies closure
decreasing.

######  Remark 10.

Our notions of uniformly and closure decreasing rules generalize the
corresponding concepts (strongly and strictly decreasing rules) in [11, 9].
The techniques in [9] fail to generalize [11] as explained in Remark 11.

We now state our main theorem.

######  Theorem 5.1 (Proving termination).

Let $\mathfrak{F}$ be a DPO framework and let $\mathfrak{S}_{1}$ and
$\mathfrak{S}_{2}$ be sets of double pushout rules. Let
$\langle\,S,\oplus,\odot,\mathbf{0},\mathbf{1},\prec,\leq\,\rangle$ be a well-
founded commutative semiring, and let
$\mathcal{T}=(T,\mathbb{E},S,\mathbf{w})$ be a finitary weighted type graph
such that

  * •

$\textit{left}(\delta)$ is weighable with $\mathcal{T}$, and

  * •

$\textit{right}(\delta)$ is bounded above by $\mathcal{T}$

for every rule $\rho\in(\mathfrak{S}_{1}\cup\mathfrak{S}_{2})$ and double
pushout diagram $\delta\in\mathfrak{F}(\rho)$. If

  1. 1.

$\rho$ is weakly decreasing for every $\rho\in\mathfrak{S}_{2}$, and

  2. 2.

$\rho$ is uniformly or closure decreasing for every $\rho\in\mathfrak{S}_{1}$,

then $\mathfrak{S}_{1}$ is terminating relative to $\mathfrak{S}_{2}$.

##  6 Examples

######  Notation 6.1 (Visual Notation).

We use the visual notation as in [34]. The vertices of graphs are non-empty
sets $\\{x_{1},\ldots,x_{n}\\}$ depicted by boxes $x_{1}$$\cdots$ $x_{n}$. We
will choose the vertices of the graphs in such a way that the homomorphisms
$h:G\to H$ are fully determined by $S\subseteq h(S)$ for all $S\in V_{G}$. For
instance, in Example 5 below, the morphism $\mathfrak{c}_{\rho}:L\to T$ maps
nodes $\\{x\\},\\{y\\},\\{z\\}\in L$ as follows:
$\mathfrak{c}_{\rho}(\\{x\\})=\\{x\\}$ and
$\mathfrak{c}_{\rho}(\\{y\\})=\mathfrak{c}_{\rho}(\\{z\\})=\\{y,z\\}\in T$.

We start with two examples (Examples 4 and 5) for which the approaches from
[11, 9] fail, as the systems are not terminating with unrestricted matching.

######  Example 4 (Loop unfolding with monic matching).

Let $\rho$ be the DPO rule

$L$$x$$y$$K$$x$$y$$R$$x$$y$$l$$r$

in Graph, and let matches $m$ restrict to monic matches. We prove termination
using the weighted type graph $\mathcal{T}$$x$$y$$2$$2$ over the (strictly
monotonic) arithmetic semiring. The type graph $T$ is unlabelled. The numbers
along the edges indicate the weighted elements $\mathbb{E}$. Here $\mathbb{E}$
consists of $2$ morphisms with domain  (see further Remark 3) and their weight
is the number along the edge they target. So
$\mathbb{E}=\\{\,e_{x},e_{y}\,\\}$ where $e_{x}$ and $e_{y}$ map  onto the
loop on $\\{x\\}$ and the loop on $\\{y\\}$ in $T$, respectively. The weights
of $e_{x}$ and $e_{y}$ are $\mathbf{w}(e_{x})=\mathbf{w}(e_{y})=2$.

As the context closure $\mathfrak{c}_{\rho}$ for $\rho$ and $T$ we use the
inclusion $\mathfrak{c}_{\rho}:L\rightarrowtail T$. Clearly, for any monic
match $L\rightarrowtail G$, there exists a map $\alpha:G\to T$ such that
$\mathfrak{c}_{\rho}=\alpha\circ m$. For $t_{K}=\mathfrak{c}_{\rho}\circ l$ we
have $\mathbf{w}(\\{\,{-}\circ
l=t_{K}\,\\})={2}\succ{1}=\mathbf{w}(\\{\,{-}\circ r=t_{K}\,\\})$ since the
empty product is $1$. Moreover, $\mathbf{w}(\\{\,{-}\circ
l=t_{K}\,\\})\geq\mathbf{w}(\\{\,{-}\circ r=t_{K}\,\\})$ for all other
$t_{K}:K\to T$. Thus $\rho$ is closure decreasing, and consequently
terminating by Theorem 5.1.

######  Example 5 (Reconfiguration).

Continuing Example 3, we prove termination  of $\rho$ with matches $m$
restrict to monic matches. We use the weighted type graph shown on the right,
over the (strictly monotonic) arithmetic semiring. This is the type graph
constructed in Example 3, enriched with weighted elements.
$\mathcal{T}$$x$$y$$z$$u$$2$
$\mathbb{E}$ consists of a single morphism with weight $2$, mapping  onto the
edge from $\\{y,z\\}$ to $\\{u\\}$ in $T$.

As the context closure $\mathfrak{c}_{\rho}$ for $\rho$ and $T$ we use
$\mathfrak{c}_{\rho}:L\to T$ as indicated by the node names ($\\{y\\}$ and
$\\{z\\}$ are mapped onto $\\{y,z\\}$). For $t_{K}=\mathfrak{c}_{\rho}\circ l$
we then obtain $\mathbf{w}(\\{\,{-}\circ
l=t_{K}\,\\})={1+1+2}\succ{1+1}=\mathbf{w}(\\{\,{-}\circ r=t_{K}\,\\})$ since
the empty product is $1$, and $\\{z\\}$ in $L$ can be mapped onto $\\{x\\}$,
$\\{y,z\\}$ and $\\{u\\}$, while $\\{w\\}$ in $R$ can only be mapped onto
$\\{x\\}$ and $\\{y,z\\}$ in $T$. Furthermore, $\mathbf{w}(\\{\,{-}\circ
l=t_{K}\,\\})\geq\mathbf{w}(\\{\,{-}\circ r=t_{K}\,\\})$ for all other
$t_{K}:K\to T$. Thus $\rho$ is closure decreasing, and hence terminating by
Theorem 5.1.

We continue with an example (Example 6) of rewriting simple graphs. Here the
techniques from [11, 9] are not applicable, because they are defined only for
multigraphs. Even when considering the rule as a rewrite rule on multigraphs,
the technique from [11] is not applicable due to non-monic $r$, and the
technique from [9] fails because the rule is not terminating with respect to
unrestricted matching.

######  Example 6 (Simple graphs and monic matching).

Let $\rho$ be the DPO rule

$L$$x$$y$$K$$x$$y$$R$$x$$y$$z$$w$$l$$r$

in the category of simple graphs SGraph, and let matches $m$ restrict to monic
matches. This rule folds an edge into a loop, similar to [34, Example 49], but
extended with the addition of two fresh nodes in the right-hand side. We prove
termination using the weighted type graph
$\mathcal{T}=(T,\mathbb{E},S,\mathbf{w})$ given by

$\mathcal{T}$$x$$y$$1$$z$

over the tropical semiring. So $\mathbb{E}$ consists of a single morphism $e$
mapping  onto $x$ in $T$, and $\mathbf{w}(e)=1$. (See Remark 4 on strong
traceability in SGraph.) As the context closure $\mathfrak{c}_{\rho}$ for
$\rho$ and $T$ we use the morphism $\mathfrak{c}_{\rho}:L\to T$ as indicated
by the node names ($\\{x\\}$ and $\\{y\\}$ are mapped onto $\\{x,y\\}$).

Then $\mathbf{w}(\\{\,{-}\circ l=t_{K}\,\\})=2\succ 1=3\oplus 2\oplus 2\oplus
1=\mathbf{w}(\\{\,{-}\circ r=t_{K}\,\\})$ for $t_{K}=\mathfrak{c}_{\rho}\circ
l$. For every other morphism $t_{K}:K\to T$ it holds that $\\{\,{-}\circ
l=t_{K}\,\\}=\varnothing=\\{\,{-}\circ r=t_{K}\,\\}$. Thus $\rho$ is uniformly
decreasing, and Theorem 5.1 yields termination of $\rho$.

######  Example 7 (Reconfiguration on simple graphs).

Example 5 can also be considered on SGraph with monic matching. Assume that we
add in $K$ an edge from $\\{x\\}$ to $\\{y\\}$ (this does not change the
rewrite relation). Then $l$ is regular monic, and we have strong traceability
for the edges along the left pushout squares of rewrite steps. Hence all left
squares are weighable, and all right squares are bounded above by the type
graph in Example 5; so the same type graph proves also termination on SGraph.

Additional examples with unrestricted matching may be found in Appendix 0.D:

  * •

Example 12 treats [40, Example 3] and [37, Example 3.8] by Plump;

  * •

Example 13 treats [9, Example 6] by Bruggink et al.;

  * •

Example 14 shows that the technique also can be fruitfully applied for rules
$\rho:L\leftarrow K\to R$ for which $L$ is a subgraph of $R$, that is,
$L\rightarrowtail R$.

Finally, Example 15 illustrates a limitation of our technique:

######  Open Question 6.2.

We conjecture that our technique cannot be applied for rules
$\rho:L\stackrel{{\scriptstyle l}}{{\leftarrow}}K\stackrel{{\scriptstyle
r}}{{\to}}R$ for which there exists an epimorphism $e:R\twoheadrightarrow L$
with $l=e\circ r$. Can the technique be enhanced to deal with such rules?

In Appendix 0.E we provide some benchmarks from a Scala implementation.

##  7 Related Work

The approaches [11, 9] by Bruggink et al. are the most relevant to our paper.
Both employ weighted type graphs for multigraphs to prove termination of graph
transformation. We significantly strengthen the weighted type graphs technique
for rewriting with monic matching and we generalize the techniques to
arbitrary categories and different variants of DPO.

Plump has proposed two systematic termination criteria [37, 40] for hypergraph
rewriting with DPO. The approach in [37] is based on the concept of forward
closures. The paper [40] introduces a technique for modular termination proofs
based on sequential critical pairs. The modular approach can often simplify
the termination arguments significantly. However, the smaller decomposed
systems still require termination arguments. Therefore, our techniques and the
approach from [40] complement each other perfectly. Our technique can handle
all examples from the papers [37, 40], except for one (see Example 15 for
discussion of this system).

In [34], we have proposed a termination approach based on weighted element
counting. Like the method presented in this paper, the method [34] is defined
for general categories (more specifically, rm-adhesive quasitoposes), but for
PBPO+ [35, 36] instead of DPO. PBPO+ subsumes DPO in the quasitopos setting
[35, Theorem 72] if both the left-hand morphism $l$ of DPO rules and matches
$m$ are required to be regular monic. The weighted element counting approach
defines the weight of an object $G$ by means of counting weighted elements of
the form $t:T\to G$, meaning it is roughly dual to the approach presented in
this paper.

An example that the weighted type graph approach can prove, but the weighted
element counting approach cannot prove, is Example 13 [9, Example 6], which
requires measuring a global property rather than a local one. Conversely,
Example 15 [40, Example 6] is an example that seems unprovable using weighted
type graphs, while the element counting approach can prove it rather
straightforwardly [34, Example 39]. So it appears the two methods may be
complementary even in settings where they are both defined.

The paper [30] proposes a criterion for termination of DPO rules with respect
to injective matching. Roughly speaking, they show that a system is
terminating if the size of repeated sequential compositions of rules tends to
infinity. It remains to be seen if this criterion can be fruitfully automated.

The paper [6] introduces a framework for proving termination of high-level
replacement units (these are systems with with external control expressions).
They show that their framework can be used for node and edge counting
arguments which are subsumed by weighted type graphs (see further [9]).

There are also various techniques that generalize TRS methods to term graphs
[39, 38, 32] and drags [18].

##  8 Future Work

There are several interesting directions for future research:

  1. 1.

Can the weighted type graphs technique be extended to other algebraic graph
transformation frameworks, such as SPO [31], SqPO [16], PBPO [14], AGREE [15]
and PBPO+ [35]?

  2. 2.

Can the technique be enhanced to deal with examples like Example 15? (See also
Open Question 6.2.)

  3. 3.

Can the technique be extended to deal with negative application conditions
[25]?

  4. 4.

Are there semirings other than arctic, tropical and arithmetic that can be
fruitfully employed for termination proofs with the weighted type graph
technique?

Concerning (1), an extension to PBPO+ would be particularly interesting. In
[35], it has been shown that, in the setting of quasitoposes, every rule of
the other formalisms can be straightforwardly encoded as a PBPO+ rule that
generates the same rewrite relation111The subsumption of SPO by PBPO+ in
quasitoposes remains a conjecture [35, Remark 23], but has been established
for Graph.. However, our proofs (Lemma 3) crucially depend on a property
specific to pushouts (Lemma 2). It will therefore be challenging to lift the
reasoning to the pullbacks in PBPO+ without (heavily) restricting the
framework (to those pullbacks that are pushouts).

## References

  * [1] Adámek, J., Herrlich, H., Strecker, G.E.: Abstract and concrete categories: The joy of cats 17, 1–507 (2006), http://www.tac.mta.ca/tac/reprints/articles/17/tr17.pdf
  * [2] Apt, K.R., Pedreschi, D.: Reasoning about termination of pure prolog programs. Inf. Comput. 106(1), 109–157 (1993). doi:10.1006/inco.1993.1051
  * [3] Behr, N., Harmer, R., Krivine, J.: Concurrency theorems for non-linear rewriting theories. In: Proc. Conf. on Graph Transformation (ICGT). LNCS, vol. 12741, pp. 3–21. Springer (2021). doi:10.1007/978-3-030-78946-6_1
  * [4] Behr, N., Harmer, R., Krivine, J.: Fundamentals of compositional rewriting theory. CoRR abs/2204.07175 (2022). doi:10.48550/arXiv.2204.07175
  * [5] Beyer, D.: Progress on software verification: SV-COMP 2022. In: Proc. TACAS (2). pp. 375–402. LNCS 13244, Springer (2022). doi:10.1007/978-3-030-99527-0_20
  * [6] Bottoni, P., Hoffmann, K., Parisi-Presicce, F., Taentzer, G.: High-level replacement units and their termination properties. J. Vis. Lang. Comput. 16(6), 485–507 (2005). doi:10.1016/j.jvlc.2005.07.001
  * [7] Braatz, B., Golas, U., Soboll, T.: How to delete categorically - two pushout complement constructions. J. Symb. Comput. 46(3), 246–271 (2011). doi:10.1016/j.jsc.2010.09.007
  * [8] Brown, K., Patterson, E., Hanks, T., Fairbanks, J.P.: Computational category-theoretic rewriting. In: Proc. Conf. on Graph Transformation (ICGT). LNCS, vol. 13349, pp. 155–172. Springer (2022). doi:10.1007/978-3-031-09843-7_9
  * [9] Bruggink, H.J.S., König, B., Nolte, D., Zantema, H.: Proving termination of graph transformation systems using weighted type graphs over semirings. In: Proc. Conf. on Graph Transformation (ICGT). LNCS, vol. 9151, pp. 52–68. Springer (2015). doi:10.1007/978-3-319-21145-9_4
  * [10] Bruggink, H.J.S., König, B., Nolte, D., Zantema, H.: Proving termination of graph transformation systems using weighted type graphs over semirings (2023), arXiv:1505.01695v3
  * [11] Bruggink, H.J.S., König, B., Zantema, H.: Termination analysis for graph transformation systems. In: Proc. Conf. on Theoretical Computer Science (TCS). LNCS, vol. 8705, pp. 179–194. Springer (2014). doi:10.1007/978-3-662-44602-7_15
  * [12] Cook, B., Podelski, A., Rybalchenko, A.: Termination proofs for systems code. In: Proc. Conf. on Programming Language Design and Implementation. pp. 415–426. ACM (2006). doi:10.1145/1133981.1134029
  * [13] Cook, B., Podelski, A., Rybalchenko, A.: Proving program termination. Commun. ACM 54(5), 88–98 (2011). doi:10.1145/1941487.1941509
  * [14] Corradini, A., Duval, D., Echahed, R., Prost, F., Ribeiro, L.: The PBPO graph transformation approach. J. Log. Algebraic Methods Program. 103, 213–231 (2019)
  * [15] Corradini, A., Duval, D., Echahed, R., Prost, F., Ribeiro, L.: Algebraic graph rewriting with controlled embedding. Theor. Comput. Sci. 802, 19–37 (2020). doi:10.1016/j.tcs.2019.06.004
  * [16] Corradini, A., Heindel, T., Hermann, F., König, B.: Sesqui-Pushout Rewriting. In: Proc. Conf. on Graph Transformation (ICGT). LNCS, vol. 4178, pp. 30–45. Springer (2006). doi:10.1007/11841883_4
  * [17] Corradini, A., Montanari, U., Rossi, F., Ehrig, H., Heckel, R., Löwe, M.: Algebraic approaches to graph transformation - part I: basic concepts and double pushout approach. In: Handbook of Graph Grammars and Computing by Graph Transformations, Volume 1: Foundations, pp. 163–246. World Scientific (1997)
  * [18] Dershowitz, N., Jouannaud, J.: Graph path orderings. In: Proc. Conf. on Logic for Programming, Artificial Intelligence and Reasoning (LPAR). EPiC Series in Computing, vol. 57, pp. 307–325. EasyChair (2018). doi:10.29007/6hkk
  * [19] Ehrig, H., Ehrig, K., Prange, U., Taentzer, G.: Fundamentals of Algebraic Graph Transformation. Monographs in Theoretical Computer Science. An EATCS Series, Springer (2006). doi:10.1007/3-540-31188-2
  * [20] Ehrig, H., Golas, U., Hermann, F.: Categorical frameworks for graph transformation and HLR systems based on the DPO approach. Bull. EATCS 102, 111–121 (2010)
  * [21] Ehrig, H., Pfender, M., Schneider, H.J.: Graph-Grammars: An Algebraic Approach. In: Proc. Symp. on on Switching and Automata Theory (SWAT). p. 167–180. IEEE Computer Society (1973). doi:10.1109/SWAT.1973.11
  * [22] Giesl, J., Brockschmidt, M., Emmes, F., Frohn, F., Fuhs, C., Otto, C., Plücker, M., Schneider-Kamp, P., Ströder, T., Swiderski, S., Thiemann, R.: Proving termination of programs automatically with AProVE. In: Proc. Conf. on Automated Reasoning (IJCAR). LNCS, vol. 8562, pp. 184–191. Springer (2014). doi:10.1007/978-3-319-08587-6_13
  * [23] Giesl, J., Raffelsieper, M., Schneider-Kamp, P., Swiderski, S., Thiemann, R.: Automated termination proofs for haskell by term rewriting. ACM Trans. Program. Lang. Syst. 33(2), 7:1–7:39 (2011). doi:10.1145/1890028.1890030
  * [24] Giesl, J., Rubio, A., Sternagel, C., Waldmann, J., Yamada, A.: The termination and complexity competition. In: Proc. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol. 11429, pp. 156–166. Springer (2019). doi:10.1007/978-3-030-17502-3_10
  * [25] Habel, A., Heckel, R., Taentzer, G.: Graph grammars with negative application conditions. Fundam. Informaticae 26(3/4), 287–313 (1996). doi:10.3233/FI-1996-263404
  * [26] Habel, A., Müller, J., Plump, D.: Double-pushout graph transformation revisited. Math. Struct. Comput. Sci. 11(5), 637–688 (2001). doi:10.1017/S0960129501003425
  * [27] König, B., Nolte, D., Padberg, J., Rensink, A.: A tutorial on graph transformation. In: Graph Transformation, Specifications, and Nets - In Memory of Hartmut Ehrig. LNCS, vol. 10800, pp. 83–104. Springer (2018). doi:10.1007/978-3-319-75396-6_5
  * [28] Lack, S., Sobociński, P.: Adhesive categories. In: Proc. Conf. on Foundations of Software Science and Computation Structures (FOSSACS). LNCS, vol. 2987, pp. 273–288. Springer (2004). doi:10.1007/978-3-540-24727-2_20
  * [29] Lee, C.S., Jones, N.D., Ben-Amram, A.M.: The size-change principle for program termination. In: Proc. Symp. on Principles of Programming Languages (POPL). pp. 81–92. ACM (2001). doi:10.1145/360204.360210
  * [30] Levendovszky, T., Prange, U., Ehrig, H.: Termination criteria for DPO transformations with injective matches. In: Proc. Workshop on Graph Transformation for Concurrency and Verification. ENTCS, vol. 175, pp. 87–100. Elsevier (2006). doi:10.1016/J.ENTCS.2007.04.019
  * [31] Löwe, M.: Algebraic approach to single-pushout graph transformation. Theor. Comput. Sci. 109(1&2), 181–224 (1993). doi:10.1016/0304-3975(93)90068-5
  * [32] Moser, G., Schett, M.A.: Kruskal’s tree theorem for acyclic term graphs. In: Proc. Workshop on Computing with Terms and Graphs, TERMGRAPH. EPTCS, vol. 225, pp. 25–34 (2016). doi:10.4204/EPTCS.225.5
  * [33] de Moura, L.M., Bjørner, N.S.: Z3: an efficient SMT solver. In: Proc. Conf. on on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol. 4963, pp. 337–340. Springer (2008). doi:10.1007/978-3-540-78800-3_24
  * [34] Overbeek, R., Endrullis, J.: Termination of graph transformation systems using weighted subgraph counting. CoRR abs/2303.07812 (2023). doi:10.48550/arXiv.2303.07812, https://doi.org/10.48550/arXiv.2303.07812
  * [35] Overbeek, R., Endrullis, J., Rosset, A.: Graph rewriting and relabeling with PBPO+: A unifying theory for quasitoposes. Journal of Logical and Algebraic Methods in Programming (2023). doi:https://doi.org/10.1016/j.jlamp.2023.100873
  * [36] Overbeek, R.: A Unifying Theory for Graph Transformation. Ph.D. thesis, Vrije Universiteit Amsterdam (2024). doi:10.5463/thesis.524
  * [37] Plump, D.: On termination of graph rewriting. In: Proc. Workshop on Graph-Theoretic Concepts in Computer Science (WG). LNCS, vol. 1017, pp. 88–100. Springer (1995). doi:10.1007/3-540-60618-1_68
  * [38] Plump, D.: Simplification orders for term graph rewriting. In: Proc. Symp. on Mathematical Foundations of Computer Science (MFCS). LNCS, vol. 1295, pp. 458–467. Springer (1997). doi:10.1007/BFb0029989
  * [39] Plump, D.: Term graph rewriting. Handbook Of Graph Grammars And Computing By Graph Transformation: Volume 2: Applications, Languages and Tools pp. 3–61 (1999), https://www-users.york.ac.uk/~djp10/Papers/tgr_survey.pdf
  * [40] Plump, D.: Modular termination of graph transformation. In: Graph Transformation, Specifications, and Nets. LNCS, vol. 10800, pp. 231–244. Springer (2018). doi:10.1007/978-3-319-75396-6_13
  * [41] Vigna, S.: A guided tour in the topos of graphs (2003). doi:10.48550/arxiv.math/0306394
  * [42] Zantema, H.: Termination. In: Term Rewriting Systems, Cambridge Tracts in Theoretical Computer Science, vol. 55, pp. 181–259. Cambridge University Press (2003)

## Appendix

##  Appendix 0.A Weighted Type Graphs by Bruggink et al.

######  Example 8 (Missing conditions in [9]).

The problem discussed here concerns the published conference proceedings [9];
the authors have confirmed and solved the problem in their latest arXiv
version [10].

Consider the following rule

$L$$x$$a$$K$$x$$R$$x$$y$$a$$b$$l$$r$

with unrestricted matching. This rule is obviously not terminating.

However, according to [9, Theorem 2] it should be. The problem is caused by
negative weights in the type graph (these are allowed, except for the flower
node). To understand the problem, take the following weighted type graph

$\mathcal{T}$$x$$y$$a^{1}$$b^{1}$$b^{\bot}$$b^{\bot}$$a^{1}$$b^{1}$

with weights from the ordered semiring
$\langle\mathbb{N}_{\bot},+,\cdot,0,1,\leq\rangle$ where

  1. 1.

$\mathbb{N}_{\bot}=\mathbb{N}\cup\\{\,\bot\,\\}$;

  2. 2.

$\leq$ is the usual order on $\mathbb{N}$ extended with $\bot\leq n$ for every
$n\in\mathbb{N}$;

  3. 3.

$+$ is defined as usual on $\mathbb{N}$ and $\bot+n=n+\bot=\bot$ for all
$n\in\mathbb{N}_{\bot}$;

  4. 4.

$\cdot$ is defined as usual on $\mathbb{N}$ and

    1. (a)

$\bot\cdot n=n\cdot\bot=\bot$ for all
$n\in\mathbb{N}_{\bot}\mathbin{\mathchoice{\hbox{ \leavevmode\hbox
to3.6pt{\vbox to6.6pt{\pgfpicture\makeatletter\hbox{\hskip
0.3pt\lower-0.3pt\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{
}{{{}{}}{{}}{} {{}{}}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.6pt}\pgfsys@invoke{ }\pgfsys@roundcap\pgfsys@invoke{
}{}\pgfsys@moveto{3.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{6.0pt}\pgfsys@stroke\pgfsys@invoke{
} \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}}}}{\hbox{
\leavevmode\hbox to3.6pt{\vbox to6.6pt{\pgfpicture\makeatletter\hbox{\hskip
0.3pt\lower-0.3pt\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{
}{{{}{}}{{}}{} {{}{}}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.6pt}\pgfsys@invoke{ }\pgfsys@roundcap\pgfsys@invoke{
}{}\pgfsys@moveto{3.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{6.0pt}\pgfsys@stroke\pgfsys@invoke{
} \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}}}}{\hbox{
\leavevmode\hbox to2.45pt{\vbox to4.45pt{\pgfpicture\makeatletter\hbox{\hskip
0.22499pt\lower-0.22499pt\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{
}{{{}{}}{{}}{} {{}{}}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.45pt}\pgfsys@invoke{ }\pgfsys@roundcap\pgfsys@invoke{
}{}\pgfsys@moveto{2.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{4.0pt}\pgfsys@stroke\pgfsys@invoke{
} \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}}}}{\hbox{
\leavevmode\hbox to1.9pt{\vbox to3.4pt{\pgfpicture\makeatletter\hbox{\hskip
0.2pt\lower-0.2pt\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{
}{{{}{}}{{}}{} {{}{}}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\pgfsys@roundcap\pgfsys@invoke{
}{}\pgfsys@moveto{1.5pt}{0.0pt}\pgfsys@lineto{0.0pt}{3.0pt}\pgfsys@stroke\pgfsys@invoke{
} \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}}}}}\\{\,0\,\\}$, and

    2. (b)

$\bot\cdot 0=0\cdot\bot=0$.

It is easily checked that this semiring is commutative and strongly ordered in
the sense of [9]).

The nodes $x$ and $y$ of the type graph are flower nodes. Let $t_{K}:K\to T$
be the morphism that maps $x$ in $K$ onto $x$ in $T$. Then, we have

$\displaystyle\mathbf{w}(\\{\,{-}\circ l=t_{K}\,\\})=1\quad>\quad\bot=1\cdot
1+1\cdot\bot=\mathbf{w}(\\{\,{-}\circ r=t_{K}\,\\})$

For this mapping $t_{K}$ of the interface, the weight of the left-hand side is
bigger than that of the right-hand side. By the symmetry of the type graph $T$
we have the same weight decrease for the morphism $t_{K}$ that maps $x$ in $K$
onto $y$ in $T$. Thus the rule is strongly decreasing in the sense of [9]
(that is, decreasing for every mapping $t_{K}:K\to T$).

All conditions of [9, Theorem 2] are fulfilled. However, contrary to the claim
of the theorem, the rule is not terminating. The problem goes back to the
proofs of Lemma 3 and Lemma 4 in [9]. Also the proof of [9, Theorem 1] is
invalidated since it is based on Lemma 3. The root cause in Lemma 4 is
concluding

$\displaystyle\mathbf{w}(t_{K})\cdot\mathbf{w}(\\{\,{-}\circ
l=t_{K}\,\\})>\mathbf{w}(t_{K})\cdot\mathbf{w}(\\{\,{-}\circ r=t_{K}\,\\})$

from

$\displaystyle\mathbf{w}(\\{\,{-}\circ l=t_{K}\,\\})>\mathbf{w}(\\{\,{-}\circ
r=t_{K}\,\\})$

Similarly in Lemma 3 (and Theorem 1), but with $>$ replaced by $\geq$.

######  Remark 11.

Our notion of uniformly decreasing is a relaxation of ‘strongly decreasing’ in
[9] where it is required that $\mathbf{w}(\\{\,{-}\circ
l=t_{K}\,\\})\succ\mathbf{w}(\\{\,{-}\circ r=t_{K}\,\\})$ for every
$t_{K}:K\to T$. Bruggink et al. [9] mistakenly claim that their notion
generalizes the termination techniques from their earlier work [11] focused on
the tropical and arctic semirings. However, this is not the case since there
typically exist morphisms $t_{K}:K\to T$ for which $\\{\,{-}\circ
l=t_{K}\,\\}=\varnothing$ and thus $\mathbf{w}(\\{\,{-}\circ
l=t_{K}\,\\})=\mathbf{0}$:

  1. 1.

In the arctic semiring $\mathbf{0}=-\infty$ and
$-\infty\succ\mathbf{w}(\\{\,{-}\circ r=t_{K}\,\\})$ is impossible. In
contrast, the paper [11] allows for $\mathbf{w}(\\{\,{-}\circ
r=t_{K}\,\\})=-\infty$ in this case.

  2. 2.

In the tropical semiring $\mathbf{0}=\infty$ and
$\infty\succ\mathbf{w}(\\{\,{-}\circ r=t_{K}\,\\})$ enforces that
$\\{\,{-}\circ r=t_{K}\,\\}\neq\varnothing$ while [11] allows for
$\mathbf{w}(\\{\,{-}\circ r=t_{K}\,\\})=\infty$ in this case.

Our notion of uniform decreasingness properly generalizes the techniques in
[11] and works for any well-founded commutative semiring.

##  Appendix 0.B The Arithmetic, Tropical and Arctic Semirings

######  Example 9 (Arithmetic semiring).

The arithmetic semiring
$\langle\,\mathbb{N},\oplus,\odot,\mathbf{0},\mathbf{1},\prec,\leq\,\rangle$,
over the natural numbers $\mathbb{N}$, is a strictly monotonic, well-founded
semiring where $\oplus=+$, $\odot=\cdot$, $\mathbf{0}=0$, $\mathbf{1}=1$, and
${\prec}={<}$ and $\leq$ are the usual orders on $\mathbb{N}$.

######  Example 10 (Tropical semiring).

The tropical semiring $\langle\,S,\oplus,\odot,\mathbf{0},\mathbf{1}\,\rangle$
has carrier set $S=\mathbb{N}\cup\\{\infty\\}$. The usual order $\leq$ on
$\mathbb{N}$ is extended to $S$ by letting $a\leq\infty$ for all $a\in S$. The
operation $+$ on $\mathbb{N}$ is extended to $S$ by $a+\infty=\infty$ for all
$a\in S$. Then the operations and unit elements of the tropical semiring are
given by:

$\displaystyle\oplus(a,b)$ $\displaystyle=\min\\{\,a,b\,\\}$
$\displaystyle\odot(a,b)$ $\displaystyle=a+b$ $\displaystyle\mathbf{0}$
$\displaystyle=\infty$ $\displaystyle\mathbf{1}$ $\displaystyle=0$

The tropical semiring is a well-founded semiring
$\langle\,S,\oplus,\odot,\mathbf{0},\mathbf{1},\prec,\leq\,\rangle$, where
$\prec$ is the strict part of $\leq$. It is not strictly monotonic because
$2\oplus 2\not\prec 3\oplus 2$.

######  Example 11 (Arctic semiring).

The arctic semiring $\langle\,S,\oplus,\odot,\mathbf{0},\mathbf{1}\,\rangle$
has carrier set $S=\mathbb{N}\cup\\{-\infty\\}$. The usual order $\leq$ on
$\mathbb{N}$ is extended to $S$ by $-\infty\leq a$ for all $a\in S$. The
operation $+$ on $\mathbb{N}$ is extended to $S$ by $a+(-\infty)=-\infty$ for
all $a\in S$. The operations and unit elements of the arctic semiring are:

$\displaystyle\oplus(a,b)$ $\displaystyle=\max\\{\,a,b\,\\}$
$\displaystyle\odot(a,b)$ $\displaystyle=a+b$ $\displaystyle\mathbf{0}$
$\displaystyle=-\infty$ $\displaystyle\mathbf{1}$ $\displaystyle=0$

The arctic semiring is a well-founded semiring
$\langle\,S,\oplus,\odot,\mathbf{0},\mathbf{1},\prec,\leq\,\rangle$ where
$\prec$ is the strict part of $\leq$. It is not strictly monotonic because
$2\oplus 3\not\prec 3\oplus 3$.

##  Appendix 0.C Proofs

Due to space limitations we were not able to include proofs in the main body
of the paper. All proofs along with auxiliary lemmas, propositions and
theorems may be found in this appendix.

######  Proposition 2.

Let $\langle\,S,\oplus,\odot,\mathbf{0},\mathbf{1},\prec,\leq\,\rangle$ be a
well-founded semiring, then

$\displaystyle\mathbf{1}\leq x,y\ \wedge\ x,y\neq\mathbf{0}$
$\displaystyle\quad\implies\quad\mathbf{1}\ \leq\ (x\odot y)\ \neq\
\mathbf{0}$ (S6) $\displaystyle\mathbf{1}\leq a,b\ \wedge\ x\leq y$
$\displaystyle\quad\implies\quad(a\oplus b)\odot x\ \leq\ (a\oplus b)\odot y$
(S7) $\displaystyle\mathbf{1}\leq a,b\ \wedge\ a,b\neq\mathbf{0}\ \wedge\
x\prec y$ $\displaystyle\quad\implies\quad(a\oplus b)\odot x\ \prec\ (a\oplus
b)\odot y$ (S8)

for all $x,y,a,b\in S$.

###### Proof of Proposition 2.

For (S6), assume that $\mathbf{1}\leq x,y$ and $x,y\neq\mathbf{0}$. We get
$\mathbf{1}\leq y=\mathbf{1}\odot y\leq x\odot y$ from (S3). By definition,
there exist $c,d\in S$ with $c\prec d$, and hence $x\odot y=\mathbf{0}$ would
contradict $c\odot x\odot y\prec d\odot x\odot y$ by (S4).

For (S7), let $\mathbf{1}\leq a,b$ and $x\leq y$. We have

$\displaystyle(a\oplus b)\odot x=(a\odot x)\oplus(b\odot x)\leq(a\odot
y)\oplus(b\odot y)=(a\oplus b)\odot y$

using distributivity and (S2) since $a\odot x\leq a\odot y$ and $b\odot x\leq
b\odot y$ by (S3).

For (S8), let $\mathbf{1}\leq a,b$, $a,b\neq\mathbf{0}$ and $x\prec y$. We
have

$\displaystyle(a\oplus b)\odot x=(a\odot x)\oplus(b\odot x)\prec(a\odot
y)\oplus(b\odot y)=(a\oplus b)\odot y$

using distributivity and (S2) since $a\odot x\prec a\odot y$ and $b\odot
x\prec b\odot y$ by (S4). ∎

######  Lemma 4.

Let $\mathcal{T}=(T,\mathbb{E},S,\mathbf{w})$ be a finitary weighted type
graph. Then

  1. 1.

for every $\phi:G\to T$:
$\mathbf{1}\leq\mathbf{w}_{\mathcal{T}}(\phi)\neq\mathbf{0}$;

  2. 2.

for every $\phi:G\to T$ and $\alpha:A\to G$:
$\mathbf{1}\leq\mathbf{w}_{\mathcal{T}}(\phi-(\alpha\circ{-}))\neq\mathbf{0}$;

###### Proof of Lemma 4.

Follows from $\mathbf{1}\leq\mathbf{w}(e)\neq\mathbf{0}$ for every
$e\in\mathbb{E}$ and Proposition 2. ∎

###### Proof of Proposition 1.

If conditions (a) and (b) of Definition 8 hold, the outer diagram of

${X}$${A}$${B}$${C}$${D}$$\scriptstyle{g}$$\scriptstyle{x}$$\scriptstyle{i}$$\scriptstyle{\alpha}$$\scriptstyle{\beta}$${\delta}$$\scriptstyle{\beta^{\prime}}$$\scriptstyle{\alpha^{\prime}}$

commutes, so that $i$ is obtained (uniquely) by the pullback property of
$\delta\in\Delta$. ∎

###### Proof of Lemma 1.

Recall the relevant definitions:

$\displaystyle\mathbf{w}_{\mathcal{T}}(\phi)$
$\displaystyle=\bigodot_{e\in\mathbb{E}}\mathbf{w}(e)^{\\#\\{\,\phi\circ{-}=e\,\\}}$
$\displaystyle\mathbf{w}(\phi\circ\beta^{\prime})$
$\displaystyle=\bigodot_{e\in\mathbb{E}}\mathbf{w}(e)^{\\#\\{\,\phi\circ\beta^{\prime}\circ{-}=e\,\\}}$
$\displaystyle\mathbf{w}(\phi\circ\alpha^{\prime}-(\beta\circ{-}))$
$\displaystyle=\bigodot_{e\in\mathbb{E}}\mathbf{w}(e)^{\\#\\{\,\tau\in\\{\,\phi\circ\alpha^{\prime}\circ{-}=e\,\\}\mid\not\exists\zeta.\
\tau={\beta\circ\zeta}\,\\}}$

For part (A) of the lemma, it suffices to prove that

$\displaystyle\begin{aligned} \\#\\{\,\phi\circ{-}=e\,\\}=&\
\\#\\{\,\phi\circ\beta^{\prime}\circ{-}=e\,\\}+{}\\\ &\
\\#\\{\,\tau\in\\{\,\phi\circ\alpha^{\prime}\circ{-}=e\,\\}\mid\not\exists\zeta.\
\tau={\beta\circ\zeta}\,\\}\end{aligned}$ (3)

for every $e\in\mathbb{E}$. Moreover, for part (B) of the lemma, it suffices
to prove Equation (3) with $\leq$ instead of $=$ (because by definition
$\mathbf{1}\leq\mathbf{w}(e)$ for every $e\in\mathbb{E}$, any additional terms
on the right do not decrease the product by (S3)).

Let $e\in\mathbb{E}$ be arbitrary. We define morphism sets

$\displaystyle\Psi_{A}$
$\displaystyle=\\{\,\phi\circ\beta^{\prime}\circ\alpha\circ{-}=e\,\\}$
$\displaystyle\Psi_{B}$
$\displaystyle=\\{\,\phi\circ\beta^{\prime}\circ{-}=e\,\\}$
$\displaystyle\Psi_{D}$ $\displaystyle=\\{\,\phi\circ{-}=e\,\\}$
$\displaystyle\Psi_{C}$
$\displaystyle=\\{\,\phi\circ\alpha^{\prime}\circ{-}=e\,\\}$

Observe that by $\alpha^{\prime}\circ\beta=\beta^{\prime}\circ\alpha$, we have

$\displaystyle\Psi_{A}=\\{\,\phi\circ\beta^{\prime}\circ\alpha\circ{-}=e\,\\}=\\{\,\phi\circ\alpha^{\prime}\circ\beta\circ{-}=e\,\\}$

and so $\beta\circ\Psi_{A}=\\{\,\tau\in\Psi_{C}\mid\exists\zeta.\
\tau=\beta\circ\zeta\,\\}$. Equation (3) thus becomes

$\displaystyle\\#\Psi_{D}$
$\displaystyle=\\#\Psi_{B}+\\#\Psi_{C}-\\#(\beta\circ\Psi_{A})$ (4)

Because $\mathit{dom}(\mathbb{E})$ is traceable along $\delta$ and the square
$\delta$ commutes, we have

$\displaystyle\Psi_{D}=$ $\displaystyle\
\beta^{\prime}\circ\Psi_{B}\cup\alpha^{\prime}\circ\Psi_{C}$ (5)
$\displaystyle\
\beta^{\prime}\circ\Psi_{B}\cap\alpha^{\prime}\circ\Psi_{C}\supseteq\alpha^{\prime}\circ\beta\circ\Psi_{A}$
(6)

For part (B) of the lemma, we use the general laws

$\displaystyle\\#(A\cup B)$ $\displaystyle\leq\\#A+\\#B$ (7)
$\displaystyle\\#(f\circ A)$ $\displaystyle\leq\\#A$ (8) $\displaystyle(f\circ
A-f\circ B)$ $\displaystyle\subseteq f\circ(A-B)$ (9)

and proceed as follows:

$\displaystyle\Psi_{D}$
$\displaystyle=\beta^{\prime}\circ\Psi_{B}\cup(\alpha^{\prime}\circ\Psi_{C}-\alpha^{\prime}\circ\beta\circ\Psi_{A})$
by (5) and (6) (10) $\displaystyle\\#\Psi_{D}$
$\displaystyle\leq\\#(\beta^{\prime}\circ\Psi_{B})+\\#(\alpha^{\prime}\circ\Psi_{C}-\alpha^{\prime}\circ\beta\circ\Psi_{A})$
by (10) and (7) (11)
$\displaystyle\leq\\#\Psi_{B}+\\#(\alpha^{\prime}\circ\Psi_{C}-\alpha^{\prime}\circ\beta\circ\Psi_{A})$
by (8) (12)
$\displaystyle\leq\\#\Psi_{B}+\\#(\alpha^{\prime}\circ(\Psi_{C}-\beta\circ\Psi_{A}))$
by (9) (13) $\displaystyle\leq\\#\Psi_{B}+\\#(\Psi_{C}-\beta\circ\Psi_{A})$ by
(8) (14) $\displaystyle=\\#\Psi_{B}+\\#\Psi_{C}-\\#(\beta\circ\Psi_{A})$ since
$\beta\circ\Psi_{A}\subseteq\Psi_{C}$ (15)

Equation (15) establishes Equation (4) for $\leq$, and hence proves part (B).

We now prove part (A) of the lemma. Because $\mathit{dom}(\mathbb{E})$ is
strongly traceable along $\delta$, we have
$\beta^{\prime}\circ\Psi_{B}\cap\alpha^{\prime}\circ\Psi_{C}=\alpha^{\prime}\circ\beta\circ\Psi_{A}$.
Hence from (5) we obtain

$\displaystyle\Psi_{D}$
$\displaystyle=\beta^{\prime}\circ\Psi_{B}\uplus(\alpha^{\prime}\circ\Psi_{C}-\alpha^{\prime}\circ\beta\circ\Psi_{A})$
(16) $\displaystyle\\#\Psi_{D}$
$\displaystyle=\\#(\beta^{\prime}\circ\Psi_{B})+\\#(\alpha^{\prime}\circ\Psi_{C}-\alpha^{\prime}\circ\beta\circ\Psi_{A})$
(17)
$\displaystyle=\\#\Psi_{B}+\\#(\alpha^{\prime}\circ\Psi_{C}-\alpha^{\prime}\circ\beta\circ\Psi_{A})$
(18)

where the last equality is justified by $\mathit{dom}(\mathbb{E})$-monicity of
$\beta^{\prime}$.

Because $\alpha^{\prime}$ is $\mathit{dom}(\mathbb{E})$-monic outside of
$\beta$, we have

  * ($\star$)

For any $f,g\in\Psi_{C}$ with $f\neq g$ and $g\not\in\beta\circ\Psi_{A}$, we
have $\alpha^{\prime}\circ f\neq\alpha^{\prime}\circ g$.

From ($\star$) it follows that

$\displaystyle\\#(\alpha^{\prime}\circ\Psi_{C}-\alpha^{\prime}\circ\beta\circ\Psi_{A})$
$\displaystyle=\\#(\alpha^{\prime}\circ(\Psi_{C}-\beta\circ\Psi_{A}))$ (19)
$\displaystyle=\\#\Psi_{C}-\\#(\beta\circ\Psi_{A})$ (20)

Then using Equation (18), we get

$\displaystyle\\#\Psi_{D}$
$\displaystyle=\\#\Psi_{B}+\\#(\alpha^{\prime}\circ\Psi_{C}-\alpha^{\prime}\circ\beta\circ\Psi_{A})$
(21) $\displaystyle=\\#\Psi_{B}+\\#\Psi_{C}-\\#(\beta\circ\Psi_{A})$ (22)

This establishes Equation (4), and hence proves part (A). ∎

###### Proof of Lemma 2.

Let $t_{A}:A\to T$ be given. For $p=(t_{B},t_{C})\in P$, define
$\zeta(p)=t_{D}$ where $t_{D}:D\to T$ is the unique morphism satisfying
$t_{B}={t_{D}\circ\beta^{\prime}}$ and $t_{C}={t_{D}\circ\alpha^{\prime}}$.
Then $t_{A}=t_{B}\circ\alpha=t_{D}\circ\beta^{\prime}\circ\alpha$ and so
$\zeta(p)\in U$. Map $\zeta$ is injective, because if
$\zeta(t_{B},t_{C})=t_{D}=\zeta(t_{B}^{\prime},t_{C}^{\prime})$, then
$t_{B}=t_{D}\circ\beta^{\prime}=t_{B}^{\prime}$ and
$t_{C}=t_{D}\circ\alpha^{\prime}=t_{C}^{\prime}$. It is surjective, because
for any $t_{D}\in U$, $(t_{D}\circ\beta^{\prime},t_{D}\circ\alpha^{\prime})\in
P$ and $t_{D}$ must be the universal morphism for this pair. Thus $\zeta$ and
$\theta=\zeta^{-1}$ are bijections. Direction $\implies$ now trivially follows
from the commutative property of universal morphisms, and direction
$\impliedby$ by using uniqueness of universal morphisms. ∎

###### Proof of Lemma 3.

For part (A) of the lemma we have:

$\displaystyle\mathbf{w}(D)$ $\displaystyle=\bigoplus_{t_{D}:D\to
T}\mathbf{w}(t_{D})$ $\displaystyle=\bigoplus_{t_{A}:A\to
T}\;\bigoplus_{\begin{subarray}{c}t_{D}:D\to T\\\
t_{A}=t_{D}\circ\beta^{\prime}\circ\alpha\end{subarray}}\mathbf{w}(t_{D})$
$\displaystyle=\bigoplus_{t_{A}:A\to
T}\;\bigoplus_{\begin{subarray}{c}t_{D}:D\to T\\\
t_{A}=t_{D}\circ\beta^{\prime}\circ\alpha\end{subarray}}\mathbf{w}(t_{D}\circ\beta^{\prime})\odot\mathbf{w}(t_{D}\circ\alpha^{\prime}-\beta)$
by Lemma 1 $\displaystyle=\bigoplus_{t_{A}:A\to
T}\;\bigoplus_{\begin{subarray}{c}t_{C}:C\to T\\\
t_{A}=t_{C}\circ\beta\end{subarray}}\;\bigoplus_{\begin{subarray}{c}t_{B}:B\to
T\\\
t_{A}=t_{B}\circ\alpha\end{subarray}}\mathbf{w}(t_{B})\odot\mathbf{w}(t_{C}-\beta)$
by Lemma 2
$\displaystyle\stackrel{{\scriptstyle(\dagger)}}{{=}}\bigoplus_{t_{A}:A\to
T}\;\bigoplus_{\begin{subarray}{c}t_{C}:C\to T\\\
t_{A}=t_{C}\circ\beta\end{subarray}}\Big{(}\mathbf{w}(t_{C}-\beta)\odot\bigoplus_{\begin{subarray}{c}t_{B}:B\to
T\\\ t_{A}=t_{B}\circ\alpha\end{subarray}}\mathbf{w}(t_{B})\Big{)}$
$\displaystyle\stackrel{{\scriptstyle(\dagger)}}{{=}}\bigoplus_{t_{A}:A\to
T}\;\Big{(}\bigoplus_{\begin{subarray}{c}t_{C}:C\to T\\\
t_{A}=t_{C}\circ\beta\end{subarray}}\mathbf{w}(t_{C}-\beta)\Big{)}\odot\Big{(}\bigoplus_{\begin{subarray}{c}t_{B}:B\to
T\\\ t_{A}=t_{B}\circ\alpha\end{subarray}}\mathbf{w}(t_{B})\Big{)}$

The equalities marked with $(\dagger)$ are justified since
$\mathbf{w}(t_{C}-\beta)$ and $\bigoplus_{\begin{subarray}{c}t_{B}:B\to T\\\
t_{A}=t_{B}\circ\alpha\end{subarray}}\mathbf{w}(t_{B})$ are constant.

For part (B) we get almost the same derivation. The only difference concerns
the step with the application of Lemma 1 which yields $\leq$ instead of $=$
under the assumptions for (B). ∎

######  Theorem 0.C.1 (Decreasing steps).

Let $\mathfrak{F}$ be a DPO framework. Moreover, let
$\mathcal{T}=(T,\mathbb{E},S,\mathbf{w})$ be a finitary weighted type graph
over a well-founded commutative semiring
$\langle\,S,\oplus,\odot,\mathbf{0},\mathbf{1},\prec,\leq\,\rangle$. Let
$\rho$ be a DPO rule and $\delta\in\mathfrak{F}(\rho)$ such that

  * •

$\textit{left}(\delta)$ is weighable with $\mathcal{T}$, and

  * •

$\textit{right}(\delta)$ is bounded above by $\mathcal{T}$.

Then, for the induced rewrite step $G\Rightarrow^{\delta}H$, we have

  1. 1.

$\mathbf{w}_{\mathcal{T}}(G)\geq\mathbf{w}_{\mathcal{T}}(H)$ if $\rho$ is
weakly decreasing;

  2. 2.

$\mathbf{w}_{\mathcal{T}}(G)\succ\mathbf{w}_{\mathcal{T}}(H)$ if $\rho$ is
uniformly or closure decreasing.

###### Proof of Theorem 0.C.1.

Let $\delta$ be the following double pushout diagram:

$K$$L$$R$$G$$C$$H$$l$$r$$m$$u$$w$$l^{\prime}$$r^{\prime}$POPO

For $t_{K}:K\to T$, define

$\displaystyle w_{C,t_{K}}{}=\bigoplus_{\begin{subarray}{c}t_{C}:C\to T\\\
t_{K}=t_{C}\circ u\end{subarray}}\mathbf{w}(t_{C}-(u\circ-))$

By Lemma 4, $\mathbf{1}\leq\mathbf{w}(t_{C}-(u\circ-))\neq\mathbf{0}$. By
Proposition 2, for all $x,y\in S$:

  1. (a)

$x\leq y\implies w_{C,t_{K}}{}\odot x\leq w_{C,t_{K}}{}\odot y$;

  2. (b)

$x\prec y\implies w_{C,t_{K}}{}\odot x\prec w_{C,t_{K}}{}\odot y$ if there
exists $t_{C}$ with $t_{K}=t_{C}\circ u$;

  3. (c)

$w_{C,t_{K}}{}\odot x=\mathbf{0}=w_{C,t_{K}}{}\odot y$ if there does not exist
$t_{C}$ with $t_{K}=t_{C}\circ u$;

  4. (d)

If there is a context closure $\mathfrak{c}_{\rho}$ for $\rho$ and $T$ in
$\mathfrak{F}$, then

$\displaystyle x\prec y\implies w_{C,t_{K}}{}\odot x\prec w_{C,t_{K}}{}\odot
y$

for $t_{K}=\mathfrak{c}_{\rho}\circ l$. This can be argued as follows. By the
definition of context closure, there exists $\alpha:G\to T$ such that
$\mathfrak{c}_{\rho}=\alpha\circ m$. Define $t_{C}=\alpha\circ l^{\prime}$.
Then $t_{K}=\alpha\circ m\circ l=\alpha\circ l^{\prime}\circ u=t_{C}\circ u$
and the claim follows from (b).

Since $\textit{left}(\delta)$ is weighable with $\mathcal{T}$, by Lemma 3 we
obtain

$\displaystyle\mathbf{w}_{\mathcal{T}}(G)$
$\displaystyle=\bigoplus_{t_{K}:K\to
T}\;w_{C,t_{K}}{}\odot\mathbf{w}(\\{\,{-}\circ l=t_{K}\,\\})$

Since $\textit{right}(\delta)$ is bounded above by $\mathcal{T}$, by Lemma 3
we obtain

$\displaystyle\mathbf{w}_{\mathcal{T}}(H)$
$\displaystyle\leq\bigoplus_{t_{K}:K\to
T}\;w_{C,t_{K}}{}\odot\mathbf{w}(\\{\,{-}\circ r=t_{K}\,\\})$

We distinguish cases:

  1. 1.

If $\rho$ is weakly decreasing, then $\mathbf{w}(\\{\,{-}\circ
l=t_{K}\,\\})\geq\mathbf{w}(\\{\,{-}\circ r=t_{K}\,\\})$ for every $t_{K}:K\to
T$. By (a) we have:

$\displaystyle w_{C,t_{K}}\odot\mathbf{w}(\\{\,{-}\circ l=t_{K}\,\\})\geq
w_{C,t_{K}}\odot\mathbf{w}(\\{\,{-}\circ r=t_{K}\,\\})$ (23)

for every $t_{K}:K\to T$. Hence
$\mathbf{w}_{\mathcal{T}}(G)\geq\mathbf{w}_{\mathcal{T}}(H)$ by (S1).

  2. 2.

If $\rho$ is uniformly decreasing, then from (b) and (c) we obtain

    1. (i)

$w_{C,t_{K}}\odot\mathbf{w}(\\{\,{-}\circ l=t_{K}\,\\})\succ
w_{C,t_{K}}\odot\mathbf{w}(\\{\,{-}\circ r=t_{K}\,\\})$, or

    2. (ii)

$w_{C,t_{K}}\odot\mathbf{w}(\\{\,{-}\circ
l=t_{K}\,\\})=\mathbf{0}=w_{C,t_{K}}\odot\mathbf{w}(\\{\,{-}\circ
r=t_{K}\,\\})$.

for every $t_{K}:K\to T$. To establish
$\mathbf{w}_{\mathcal{T}}(G)\succ\mathbf{w}_{\mathcal{T}}(H)$, using (S2), it
suffices to show that we have case 2(i) for some $t_{K}:K\to T$. This follows
from (d) since we have a context closure $\mathfrak{c}_{\rho}$ for $\rho$ and
$T$ by assumption.

  3. 3.

If $\rho$ is closure decreasing, then it is also weakly decreasing and we
obtain (23) for every $t_{K}:K\to T$. Since the semiring is strictly
monotonic, by (S5), it suffices to show that there exists some $t_{K}:K\to T$
such that

$\displaystyle w_{C,t_{K}}\odot\mathbf{w}(\\{\,{-}\circ l=t_{K}\,\\})\succ
w_{C,t_{K}}\odot\mathbf{w}(\\{\,{-}\circ r=t_{K}\,\\})$ (24)

in order to conclude
$\mathbf{w}_{\mathcal{T}}(G)\succ\mathbf{w}_{\mathcal{T}}(H)$. There is a
context closure $\mathfrak{c}_{\rho}$ for $\rho$ and $T$. By assumption
$\mathbf{w}(\\{\,{-}\circ l=t_{K}\,\\})\succ\mathbf{w}(\\{\,{-}\circ
r=t_{K}\,\\})$ for $t_{K}=\mathfrak{c}_{\rho}\circ l$, and we obtain (24) by
(d).

∎

###### Proof of Theorem 5.1.

Follows immediately from Theorem 0.C.1. ∎

##  Appendix 0.D Additional Examples

We now consider some examples in Graph using unrestricted matching.

######  Example 12 (Unrestricted matching).

Consider the following double pushout rewrite system

$\rho=$ $L$$x$$y$$z$$a$$b$$K$$x$$z$$R$$x$$y$$z$$a$$c$$l$$r$

$\tau=$ $L$$x$$y$$z$$c$$d$$K$$x$$z$$R$$x$$y$$z$$d$$b$$l$$r$

from [40, Example 3] and [37, Example 3.8] in Graph with unrestricted
matching. These are graph transformation versions of the string rewrite rules
$ab\to ac$ and $cd\to db$, respectively. We prove termination in two steps
using the type graphs

$\mathcal{T}_{1}$$u$$x$$y$$z$$b$$a^{2}$$a,b,c,d$

$\mathcal{T}_{2}$$u$$x$$y$$z$$d$$c^{2}$$a,b,c,d$

over the arithmetic semiring. Here the weights of the weighted elements are
indicated as superscripts (both type graphs have one weighted element with
domain  and weight $2$).

First, we take the weighted type graph $\mathcal{T}_{1}$. Consider the rule
$\rho$ together with the context closure $\mathfrak{c}_{\rho}:L\to T_{1}$
mapping all nodes onto $\\{x,y,z\\}$ in $T_{1}$. For
$t_{K}=\mathfrak{c}_{\rho}\circ l$ we have

$\displaystyle\mathbf{w}(\\{\,{-}\circ l=t_{K}\,\\})=1+2\succ
1=\mathbf{w}(\\{\,{-}\circ r=t_{K}\,\\}).$

Here weight $1$ arises from those morphisms mapping all nodes onto
$\\{x,y,z\\}$ in $T_{1}$; then there are no weighted elements in the image of
the morphism and the empty product is $1$. For all other $t_{K}:K\to T$ we
have $\mathbf{w}(\\{\,{-}\circ l=t_{K}\,\\})=0\geq 0=\mathbf{w}(\\{\,{-}\circ
r=t_{K}\,\\})$. Thus $\rho$ is closure decreasing.

For the rule $\tau$, $L$ and $R$ admit only one morphism with codomain
$T_{1}$. So it is easy to see that $\mathbf{w}(\\{\,{-}\circ
l=t_{K}\,\\})\geq\mathbf{w}(\\{\,{-}\circ r=t_{K}\,\\})$ for all $t_{K}:K\to
T$, and thus $\tau$ is weakly decreasing.

As a consequence, by Theorem 5.1, $\rho$ is terminating relative to $\tau$.
Hence it suffices to prove termination of $\tau$ which follows analogously
using $\mathcal{T}_{2}$.

######  Example 13 (Tree counter).

Consider the system

$\rho_{1}\,{=}$$x$$y$$0$$x$$x$$y$$1$

$\rho_{3}\,{=}$$x$$y$$z$$c$$0$$0$$x$$y$$z$$x$$y$$z$$0$$1$$0$

$\rho_{5}\,{=}$$x$$y$$z$$c$$1$$0$$x$$y$$z$$x$$y$$z$$0$$c$$0$

$\rho_{2}\,{=}$$x$$y$$1$$x$$x$$y$$c$

$\rho_{3}\,{=}$$x$$y$$z$$c$$0$$1$$x$$y$$z$$x$$y$$z$$0$$1$$1$

$\rho_{6}\,{=}$$x$$y$$z$$c$$1$$1$$x$$y$$z$$x$$y$$z$$0$$c$$1$

from [9, Example 6] in Graph with unrestricted matching. This system
implements a counter on trees. We prove termination in two steps using the
type graphs

$\mathcal{T}_{1}$$x$$y$$u$$0$$0^{2}$$0^{2}$$1$$1$$1^{2}$$c$$c^{2}$

$\mathcal{T}_{2}$$u$$0$$1^{2}$$c^{3}$

over the arithmetic semiring. The superscripts indicate the weights of the
weighted elements (all weighted elements have domain  ).

First, we take the weighted type graph $\mathcal{T}_{1}$. Consider the rule
$\rho_{1}$ together with the context closure $\mathfrak{c}_{\rho}:L\to T_{1}$
mapping all nodes onto $\\{x,y\\}$ in $T_{1}$. For
$t_{K}=\mathfrak{c}_{\rho}\circ l$ we have

$\displaystyle\mathbf{w}(\\{\,{-}\circ l=t_{K}\,\\})=1+2\succ
1+1=\mathbf{w}(\\{\,{-}\circ r=t_{K}\,\\}).$

For $t_{K}$ mapping $\\{x\\}$ to $\\{u\\}$, we get $\mathbf{w}(\\{\,{-}\circ
l=t_{K}\,\\})=2\geq 2=\mathbf{w}(\\{\,{-}\circ r=t_{K}\,\\})$. Thus $\rho_{1}$
is closure decreasing. Likewise, $\rho_{2}$ is also closure decreasing and all
other rules are weakly decreasing. By Theorem 5.1 it suffices to prove
termination without the rules $\rho_{1}$ and $\rho_{2}$.

Termination of the remaining rules is established by the weighted type graph
$\mathcal{T}_{2}$. The rules $\rho_{3}$, $\rho_{4}$, $\rho_{5}$ and $\rho_{6}$
are all closure decreasing with respect to $\mathcal{T}_{2}$. As a
consequence, the system is terminating by Theorem 5.1.

######  Example 14 (Morphism counting).

Let $\rho$ be the double pushout rule

$L$$x$$y$$K$$x$$R$$x$$y$$l$$r$

in the category of graphs Graph with unrestricted matching. Intuitively, this
rule connects an isolated node with an edge. We prove termination using the
weighted type graph $\mathcal{T}=(T,\mathbb{E},S,\mathbf{w})$ given by

$\mathcal{T}$$x$$y$

over the arithmetic semiring. Here $\mathbb{E}=\varnothing$. This means that
every morphism into $T$ has weight $1$ (the empty product) and thus the weight
of an object $X\in\mathit{Ob}({\textbf{C}})$ is $\\#\mathrm{Hom}(X,T)$, the
number of morphisms from $X$ to $T$. As the context closure
$\mathfrak{c}_{\rho}$ for $\rho$ and $T$ we use the inclusion
$\mathfrak{c}_{\rho}:L\rightarrowtail T$ as indicated by the node names.

For every morphism $t_{K}:K\to T$ we have

$\displaystyle\mathbf{w}(\\{\,{-}\circ l=t_{K}\,\\})=1+1=2\succ
1=\mathbf{w}(\\{\,{-}\circ r=t_{K}\,\\})$

Thus $\rho$ is closure decreasing, and Theorem 5.1 yields termination of
$\rho$.

Finally, we consider a hypergraph example with unrestricted matching. Our
method can prove relative termination of the first rule, but termination of
the second rule does not seem to be provable with our method.

######  Example 15 (Limitations).

Consider the following hypergraph rewriting system

$\rho=$ $L$$x$$y$$z$$+$$0$$K$$x$$y$$z$$0$$R$$x$$y$$z$$0$$l$$r$

$\tau=$ $L$$x$$y$$z$$s$$s$$0$$K$$x$$y$$z$$s$$0$$R$$x$$y$$z$$s$$0$$s$$0$$l$$r$

from [40, Example 6] with unrestricted matching.

Termination of $\rho$ relative to $\tau$ follows using the following weighted
type graph

$\mathcal{T}$$w$$+$$2$$0$$s$

over the arithmetic semiring by Theorem 5.1. Here the ‘$+$’ hyperedge has
weight $2$.

However, $\tau$ is an interesting rule for which we could not find a
termination proof using weighted type graphs over the arctic, tropical or
arithmetic semiring. First, note that there exists an epimorphism
$e:R\twoheadrightarrow L$ with $l=e\circ r$. In such situations, no weighted
type graph over the arithmetic semiring can make the rule strictly decreasing.
Second, it seems that the arctic and tropical semiring are also not applicable
here. Intuitively, one might try to use the tropical semiring since the
additional freedom in mapping $R$ could lead to a lower weight. However, for
this rule, there are morphisms $h_{1},h_{2}:L\to R$ where $h_{1}$ maps $L$
onto the left component of $R$, and $h_{2}$ maps $L$ onto the right component
of $R$. So, for any mapping $t:R\to T$, either $t\circ h_{1}$ or $t\circ
h_{2}$ will be at least as ‘light’.

In [40], it is argued that this rule is terminating since the sum of the
squares of in-degrees is decreasing in each step. This argument can be
automated, for instance, using the technique proposed in [34]: see Section 7
for a related discussion.

##  Appendix 0.E Implementation and Benchmarks

We have implemented our techniques in GraphTT (short for Graph Termination
Tool) for automatically proving termination of graph transformation. The tool
is written in Scala and employs Z3 [33] to solve the constraint systems.

The tool allows to specify the underlying category using copresheaves, i.e.,
functors $F:{\textbf{I}}\to{\textbf{Set}}$222We restrict to acyclic
copresheaves, i.e., copresheaves that are acyclic if one ignores the identity
morphisms., which are equivalent to unary algebras [31] and $\mathcal{C}$-sets
[8]. The grammar for specifying the index category I is

$\displaystyle\textit{IndexCategory}=\;$
$\displaystyle\textit{Object}\;\ldots\;\textit{Object}$
$\displaystyle\textit{Object}=\;$
$\displaystyle\textit{Name}[\boldsymbol{[}\underbrace{\textit{Label},\ldots,\textit{Label}}_{\text{labels}}\boldsymbol{]}](\underbrace{\textit{Name},\ldots,\textit{Name}}_{\text{arguments}})[!]$

where Name is the name of an object in I, and the ‘arguments’ are the targets
of outgoing arrows. Optionally, an object can be equipped with a set of labels
which corresponds to a slice category construction. Our tool GraphTT can
thereby be applied to the multigraph examples [11, 9], and the hypergraph
examples [40].

Moreover, the tool supports what could be called ‘partially simple’ presheaves
in which some of the element sets are simple (the elements are uniquely
determined by their ‘argument values’). To this end, an object declaration can
be followed by ‘!’. For instance

$\displaystyle V$ $\displaystyle\text{edge}(V,V)$
$\displaystyle\text{plus}(V,V,V)!$ $\displaystyle\text{flag}[a,b](V)$

describes presheaves having a set of nodes $V$, binary edges, ternary
hyperedges ‘plus’ between nodes of $V$, and unary hyperedges ‘flag’ labelled
with labels from $\\{a,b\\}$. The binary edges allow for multiple parallel
edges. The ternary ‘plus’ is declared as simple, meaning that there cannot be
two ‘plus’ edges between the same tuple of nodes (the order matters).

|  A |  T |  N |  A,T |  A,N |  T,N |  A,T,N
---|---|---|---|---|---|---|---
Example 4 |  |  | 0.08 |  | 0.06 | 0.06 | 0.09
Example 5 |  |  | 0.12 |  | 0.11 | 0.11 | 0.12
Example 6 |  | 0.03 |  | 0.03 |  | 0.03 | 0.04
Example 14 | 0.3 |  | 0.06 | 0.04 | 0.04 | 0.05 | 0.04
[37, Example 3.8] | 0.17 | 0.19 | 0.54 | 0.20 | 0.20 | 0.21 | 0.21
[40, Figure 10] | 0.43 | 0.42 | 0.49 | 0.46 | 0.51 | 0.48 | 0.52
[40, Example 3] | 0.11 | 0.09 | 0.26 | 0.1 | 0.12 | 0.11 | 0.12
[40, Example 6] |  |  |  |  |  |  |
[9, Example 4] | 0.30 | 0.35 | 0.56 | 0.24 | 0.26 | 0.31 | 0.27
[9, Example 5] |  |  | 1.11 |  | 0.89 | 0.82 | 0.83
[9, Example 6] |  |  | 2.44 |  | 1.20 | 1.25 | 1.34
[11, Example 1] | 0.10 |  | 0.18 | 0.09 | 0.11 | 0.19 | 0.11
[11, Example 4] | 0.07 | 0.08 | 0.26 | 0.09 | 0.08 | 0.10 | 0.10
[11, Example 5] | 0.61 | 0.50 | 2.39 | 0.49 | 0.68 | 0.57 | 0.52
[11, Example 6] |  |  |  | 0.23 |  | 0.47 | 0.39
Table 1: Benchmark for the examples from [11, 9, 37, 40, 34] and the examples
from Section 6. The columns display different semiring configurations: A, T
and N stand for arctic, tropical and arithmetic semiring, respectively.
Runtimes are indicated in seconds (s). Observe that [11, Example 6] requires
either a combination of both arctic with tropical, or tropical with arithmetic
semiring, for different iterations of the relative termination proof.

GraphTT supports a simple strategy language of the form

$\displaystyle\textit{Strategy}=$
$\displaystyle\textit{Strategy}\mathop{\textbf{;}}\textit{Strategy}$
sequential composition $\displaystyle\mid\;$
$\displaystyle\textit{Strategy}\mathop{\boldsymbol{|}}\textit{Strategy}$
parallel composition $\displaystyle\mid\;$
$\displaystyle\text{repeat}(\textit{Strategy})$ repeat while successful
$\displaystyle\mid\;$
$\displaystyle\text{arctic}(\text{size}=\mathbb{N},\text{bits}=\mathbb{N},\text{timeout}=\mathbb{N})$
arctic type graphs $\displaystyle\mid\;$
$\displaystyle\text{tropical}(\text{size}=\mathbb{N},\text{bits}=\mathbb{N},\text{timeout}=\mathbb{N})$
tropical type graphs $\displaystyle\mid\;$
$\displaystyle\text{arithmetic}(\text{size}=\mathbb{N},\text{bits}=\mathbb{N},\text{timeout}=\mathbb{N})$
arithmetic type graphs

This enables the user to specify what technique is applied in what order and
for how long. Each strategy can transform the system by removing rules. A
strategy is considered successful if at least one rule has been removed. For
the basis strategies, that is, arctic, tropical or arithmetic weighted type
graphs, ‘size’ specifies the size of the type graph, ‘bits’ the number of bits
for encoding the semiring elements, and ‘timeout’ is the the maximum number of
seconds to try this technique.

Table 1 shows benchmarks for running GraphTT on the examples from [11, 9, 37,
40]333We have included all uniform termination examples from [11, 9, 37, 40].
We did not include [11, Example 3] as this concerns local termination on a
particular starting language. We have also not included [37, Example 4.1]
since this concerns a category of term graphs (which our tool does not
support). The paper [34] contains examples of terminating PBPO+ systems. We
have included those examples that have DPO equivalents; see Example 5 and
Example 6. under different combinations of the arctic, tropical and arithmetic
semiring.444The benchmarks were obtained on a laptop with an i7-8550U cpu
having 4 cores, a base clock of 1.8GHz and boost of 4GHz. The techniques
proposed in the current paper successfully establish termination of all
examples, with the exception of [40, Example 6]. See Example 15 for a
discussion about this system.