<figure><img src="image_1.png" /></figure>

HAL
open science

# Termination of Graph Rewriting using Weighted Type Graphs over Non-well-founded Semirings

Qi Qiu

► To cite this version:

Qi Qiu. Termination of Graph Rewriting using Weighted Type Graphs over Non-well-founded Semirings. 16th International Workshop on Graph Computation Models, Jun 2025, Koblenz, Germany. hal-04954960v3

HAL Id: hal-04954960

https://hal.science/hal-04954960v3

Submitted on 30 Oct 2025

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_2.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# Termination of Graph Rewriting
using Weighted Type Graphs
over Non-Well-Founded Semirings

Qi Qiu*

Universite Claude Bernard Lyon 1, CNRS, INSA Lyon,
LIRIS, UMR5205, 69622 Villeurbanne, France

Univ. Grenoble Alpes, CNRS, Grenoble INP,
LIG, 38000 Grenoble, France

qi.qiu@univ-lyon1.fr

The weighted type graph method is a technique for proving termination of double-pushout (DPO)
graph rewriting systems. Existing approaches use weighted type graphs over well-founded semirings, but these have practical limitations when applied to edge-labeled directed multigraph rewriting.
We investigate the use of non-well-founded semirings to overcome these limitations. We have implemented both our method and a prior approach for edge-labeled graph rewriting within a unified tool.

# 1 Introduction

Modern computing environments increasingly rely on distributed systems to enhance performance, scalability, and efficiency. However, it is challenging to ensure their correctness due to the inherent complexity of these systems [LSP19]. Double pushout (DPO) graph rewriting [CMR+97, HMP01, KNPR18] offers a powerful yet intuitive formal framework for modeling such systems, enabling formal verification of their properties through interactive theorem proving [HUW14]. While interactive theorem proving is a promising approach for formal verification of properties of distributed systems [SP24, PSTU19, CRTU16], it requires proficiency in proof assistants and is often time-consuming. Automated methods aim to mitigate these barriers by synthesizing machine-verifiable proofs, which can be independently validated using established theorem provers [CCF+11]. Such techniques streamline verification workflows while maintaining formal guarantees.

The weighted type graph method is a technique for proving relative termination [Ges90] of DPO
graph rewriting systems. Relative termination of a set of rules $\mathcal{A}$ with respect to another set of rules
$\mathcal{B}$ ensures that in every infinite sequence of rule applications using rules from $\mathcal{A} \cup \mathcal{B}$, rules from
$\mathcal{A}$ are applied only finitely often. The method was first introduced in [ZKB14] for cycle rewriting.
Subsequent work generalized it for DPO rewriting on edge-labeled directed multigraphs with injective
rules and injective matches [BKZ14], later extending it to general DPO rewriting on edge-labeled multigraphs [BKNZ15] and adapting it to broader categories and DPO variants [EO24a]. The method assigns
weights to morphisms targeting a weighted type graph over a well-founded semiring, and the weight of
a graph is defined as the sum of the weights of all morphisms from that graph to the type graph. Relative
termination of $\mathcal{A}$ with respect to $\mathcal{B}$ is proven by ensuring that rewriting steps using rules in $\mathcal{A}$ strictly
decrease the weights of the host graphs, while rewriting steps using rules in $\mathcal{B}$ do not increase them.

<footnote>*This study was partially funded by the project SAPPORO, ANR, 2019-CE25-0005.</footnote>
In the previous work [ZKB14, BKZ14, BKNZ15], three concrete semirings on natural numbers were proposed: the natural tropical semiring $\mathfrak{T}$, the natural arctic semiring $\mathfrak{A}$, and the natural arithmetic semiring $\mathfrak{N}$. However, constructing weighted type graphs over these concrete semirings for DPO rewriting on edge-labeled directed multigraphs is undecidable in general. This is because it requires quantifying over all edge-labeled directed multigraphs with weighted edges over $\mathbb{N}$.

In response to this challenge, the authors in [ZKB14, BKZ14, BKNZ15] proposed reducing the search space by fixing the number of nodes $k \in \mathbb{N}$ and the maximum weight of edges of the weighted type graph, and then constructing a weighted type graph as follows: (1) construct a graph with $k$ nodes, with a directed edge per ordered pair of nodes and label from the finite set of edge labels $\Sigma$ of the rewriting system; (2) for each edge, decide if it exists in the weighted type graph; (3) if an edge exists, assign a weight (a natural number) to it; (4) check if the weighted type graph satisfies the required conditions.

Despite these constraints, searching for weighted type graphs that witness termination of a DPO rewriting system on edge-labeled directed multigraphs remains challenging. Let $n = k^2 \cdot |\Sigma|$. For a weighted type graph over the natural tropical semiring $\mathfrak{T}$ or the natural arctic semiring $\mathfrak{A}$, the problem can be reduced to checking the satisfiability of an existential Presburger arithmetic formula with $n$ binary variables and $n$ integer variables. While modern SMT solvers, such as Z3 [BN24] (which incorporates the dedicated CutSat solver [JM13]), can solve practical instances of this problem, its worst-case complexity remains exponential $O(2^{2n})$. For a weighted type graph over the natural arithmetic semiring $\mathfrak{N}$, the task can be reduced to checking the satisfiability of an existential Peano arithmetic formula with addition and multiplication, involving $n$ binary variables and $n$ integer variables. Though modern solvers like Z3 can tackle practical instances, it is a semi-decidable problem [Mat03].

There are automated tools that implement the weighted type graph method for proving termination of DPO rewriting systems on edge-labeled directed multigraphs: TORPAcyc [Zan24] implements the weighted type graph method for cycle rewriting and uses the SMT solver Yices [Dut14] to solve constraint systems; Grez [Bru24] implements the weighted type graph method for DPO rewriting on edge-labeled directed multigraphs; GraphTT-wtg<fnref n="1" /> [EO24b] implements the weighted type graph method for DPO rewriting on many categories. Grez and GraphTT-wtg use the SMT solver Z3 [MB08] to solve constraint systems.

In spite of the theoretical power of the weighted type graph method, its practical applicability is limited by the high computational complexity of searching for suitable weighted type graphs over well-founded semirings on natural numbers. In fact, to reduce the search space, users of the above-mentioned tools are required to fix the size of the weighted type graph, as well as the maximum weight of edges in the weighted type graph, which are challenging tasks if not impossible to determine a priori even for experts in the field. Furthermore, our experiments with the two publicly available ones TORPAcyc and Grez show that when the number of edge labels is 2, they struggle to search for weighted type graphs with 4 nodes and maximum edge weight of 2, or to search for weighted type graphs with 3 nodes when the maximum edge weight is larger than 3. This article addresses this limitation to make the weighted type graph method more accessible to non-expert users and to enhance its practical applicability.

To reduce the complexity of searching for weighted type graphs that witness termination of a DPO rewriting system on edge-labeled directed multigraphs, we propose extending the weighted type graph method to non-well-founded semirings and introduce three concrete semirings over the real numbers: the real tropical semiring $\mathfrak{T}'$, the real arctic semiring $\mathfrak{A}'$, and the real arithmetic semiring $\mathfrak{N}'$.

Under the same constraints, searching for weighted type graphs over these semirings on real numbers is computationally more tractable. Specifically, for the real tropical semiring $\mathfrak{T}'$ or the real arctic semiring $\mathfrak{A}'$

<footnote n="1">¹To the best of our knowledge, no implementation is publicly available</footnote>
$\mathfrak{A}'$, the problem reduces to checking the satisfiability of an existential linear real arithmetic formula with $n$ binary variables and $n$ real variables for the real tropical semiring $\mathfrak{T}'$ or the real arctic semiring $\mathfrak{A}'$. The SMT solver Z3 can solve practical instances of this problem more easily using CutSat solver, because there are only $n$ integer variables. The worst-case complexity for solving this problem is $O(2^n)$. For a weighted type graph over the real arithmetic semiring $\mathfrak{A}'$, the task reduces to checking the satisfiability of an existential non-linear real arithmetic formula—a task that is decidable [Col74, JM12].

We have implemented both our approach and the approach proposed by Endrullis et al. [EO24a] for DPO rewriting on edge-labeled directed multigraphs in a unified tool$^2$ written in OCaml and employs Z3 [MB08] to solve the constraint systems.

The remainder of this paper is structured as follows. § 2 reviews essential preliminary definitions. § 3 introduces the non-well-founded semirings. § 4 introduces weighted type graphs. § 5 introduces definitions used to estimate pushout-object weights. § 6 presents a termination criterion. § 7 presents the implementation of our tool. § 8 presents the experimental results. § 9 discusses empirical results obtained using the tool. § 10 presents brief remarks and outlines future research directions. The missing proofs can be found in the Appendix.

# 2 Preliminaries

In this section, we recall definitions related to the double-pushout approach to graph rewriting and relative termination, and we introduce strongly monotonic measurable semirings. For further details, we refer the reader to [KNPR18, CMR$^+$97, HMP01] for the DPO graph rewriting, [Pie91, BW95] for category theory concepts, and [Ges90] for relative termination. Basic concepts in the category theory and on edge-labeled graphs needed in this paper are collected in the preliminaries section of [Qiu25b].

## 2.1 DPO rewriting

**Definition 1** (Rewriting rule and match [CMR$^+$97]). A DPO rewriting rule $\rho$ is a span $L \stackrel{l}{\leftarrow} K \stackrel{r}{\rightarrow} R$, where $K$ is the **interface**, $L$ is the **left-hand-side graph**, denoted `lhs($\rho$)`, and $R$ is the **right-hand-side graph**, denoted `rhs($\rho$)`. The rule is **monic** if $l$ and $r$ are both **monic**. A match of the rule in an graph $G$ is a **morphism** $m: L \rightarrow G$.

In this paper, we use examples from the category **Graph** of edge-labeled directed multigraphs (see [KNPR18]) to illustrate the discussed concepts. To facilitate this, we introduce the following notation for visualizing graph homomorphisms.

**Notation 1** ([Qiu25b]). We use the notation from [OE22, Notation 1] to visualize edge-labeled graph homomorphisms. Labeled graphs are enclosed in boxes with their names displayed in the top-left corner. Nodes and edges are assigned subsets of $\mathbb{N}$ as identifiers, and these identifiers are chosen such that: (i) Each node or edge $y$ in the codomain graph is assigned the union of the identifiers of all nodes or edges in the domain graph that are mapped to $y$; (ii) The graph homomorphism is uniquely determined by this assignment. To further improve readability, we represent sets by listing their elements. Additionally, we omit identifiers when doing so does not cause confusion. This is illustrated in the following representation of a homomorphism $h: G \rightarrow H$.

<footnote>$^2$The source code can be accessed at https://github.com/Qi-tchi/LyonParallel/tree/icgt2025</footnote>
<figure><img src="image_3.png" /></figure>

In this example, the sets {1}, {2}, {3}, {4}, and {3,4} are represented as 1, 2, 3, 4, and 3 4, respectively. Edge identifiers are omitted.

**Example 1.** The injective DPO rule from [BKZ14, Example 6] will be used to illustrate the concepts discussed throughout this paper. The rule can be visualized as follows:

<figure><img src="image_4.png" /></figure>

**Definition 2 (DPO Rewriting step [EO24a]).**

A DPO diagram $\delta$ is a diagram as shown on the right. This diagram $\delta$ is a witness for the **rewriting step** from $G$ to $H$ using the rule $\rho$ and **match** $m$, denoted $G \Rightarrow_{\rho}^{m} H$ or $G \Rightarrow_{\delta}^{\delta} H$. We denote left($\delta$) and right($\delta$) the pushout squares KLGC and KRHC, respectively.

<figure><img src="image_5.png" /></figure>

**Example 2.** The DPO diagram below defines a rewriting step using the rule from Example 1.

<figure><img src="image_6.png" /></figure>

DPO rewriting has several variants, depending on factors such as whether the matching morphism, the left-hand morphism, or the right-hand morphism is monic [HMP01], and whether the left pushout square is restricted [BHK21, BHK23]. Since these restrictions can influence the termination properties of a DPO rewrite system, we use the definition from [EO24a] to encompass different DPO variants.

**Definition 3 (Rewriting framework [EO24a]).** A DPO rewriting framework $\mathfrak{F}$ is a mapping of DPO rewriting rules to classes of DPO diagrams such that, for every rule $\rho$, $\mathfrak{F}(\rho)$ is a class of DPO diagrams with top-span $\rho$.

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

## 2.2 Relative termination

**Definition 5 (Rewriting sequence).** Let $\mathcal{R}$ be a set of rewriting rules. Let $\mathfrak{F}$ be a DPO rewriting framework. A $(\mathcal{R}, \mathfrak{F})$-rewriting sequence is a finite sequence $s_0, s_1, \dots, s_m$ of objects such that $s_n \Rightarrow_{\mathcal{R}, \mathfrak{F}} s_{n+1}$ for each $0 \le n \le m-1$, or an infinite sequence $s_0, s_1, \dots$ of objects such that $s_n \Rightarrow_{\mathcal{R}, \mathfrak{F}} s_{n+1}$ for each $n \in \mathbb{N}$. A $(\mathcal{R}, \mathfrak{F})$-rewriting sequence from $s_0$ will be denoted as: $s_0 \Rightarrow_{\mathcal{R}, \mathfrak{F}} s_1 \Rightarrow_{\mathcal{R}, \mathfrak{F}} s_2 \Rightarrow_{\mathcal{R}, \mathfrak{F}} \dots$
**Definition 6** (Relative termination [Klo87, Ges90]). Let $\mathcal{A}$ and $\mathcal{B}$ be sets of rewriting rules. Let $\mathfrak{F}$ be a DPO rewriting framework. We say that $\Rightarrow_{\mathcal{A}, \mathfrak{F}}$ is **terminating relative to** $\Rightarrow_{\mathcal{B}, \mathfrak{F}}$ if any infinite $(\mathcal{A} \cup \mathcal{B}, \mathfrak{F})$-rewriting sequence has only a finite number of rewriting steps with rules in $\mathcal{A}$.

## 3 Strongly monotonic measurable semiring

A commutative semiring is an algebraic structure (see [BKNZ15][EO24a]). In this work, we adapt the concept of an ordered semiring from [EO24a]. The key difference is that the semiring is required to be equipped with a homomorphism to the extended real numbers instead of being well-founded. Throughout the remainder of this article, $<$ and $\le$ denote the canonical irreflexive and reflexive orders on the set of extended real numbers $\mathbb{R} = \mathbb{R} \cup \{-\infty, +\infty\}$.

**Definition 7** (Strongly monotonic measurable semiring). A strongly monotonic measurable semiring $(S, \oplus, \odot, 0, 1, <, \mu)$ consists of

* A commutative semiring $(S, \oplus, \odot, 0, 1)$,

* A non-empty irreflexive order $\prec$ on $S$,

* A homomorphism $\mu : (S, \prec) \to (\mathbb{R}, \prec)$,

such that $0 \neq 1$ and for all $x, y, z, w \in S$, for all $\delta \in \mathbb{R}_{\ge 0}$, we have

$$1 \preceq x \wedge 1 \preceq y \Rightarrow 1 \preceq x \oplus y \qquad (S0)$$

$$x \preceq x' \wedge y \preceq y' \Rightarrow x \oplus y \preceq x' \oplus y' \qquad (S1)$$

$$x \prec x' \wedge y \prec y' \Rightarrow x \oplus y \prec x' \oplus y' \qquad (S2)$$

$$\delta + \mu(x) < \mu(y) \wedge \delta + \mu(z) < \mu(w) \Rightarrow \delta + \mu(x \oplus z) < \mu(y \oplus w) \qquad (S3)$$

$$x \preceq x' \Rightarrow x \odot y \preceq x' \odot y \qquad (S4)$$

$$x \prec x' \wedge y \neq 0 \Rightarrow x \odot y \prec x' \odot y \qquad (S5)$$

$$\delta + \mu(x) < \mu(y) \wedge 1 \preceq z \neq 0 \Rightarrow \delta + \mu(x \odot z) < \mu(y \odot z) \qquad (S6)$$

$$\delta + \mu(x) < \mu(x') \wedge y \neq 0 \Rightarrow \mu(x \odot y) < \mu(x' \odot y) \qquad (S7)$$

where $\preceq$ denotes the reflexive closure of $\prec$. The semiring is a strictly monotonic measurable semiring if it additionally satisfies

$$x \prec x' \Rightarrow x \oplus y \prec x' \oplus y \qquad (S8)$$

$$\delta + \mu(x) < \mu(x') \Rightarrow \delta + \mu(x \oplus y) < \mu(x' \oplus y) \qquad (S9)$$

**Example 3.** The real tropical semiring $\mathcal{T}' = (\mathbb{R} \cup \{+\infty\}, \min, +, +, +\infty, 0_{\mathbb{R}}, <, \mathrm{id}_{\mathbb{R} \cup \{+\infty\}})$ has domain $\mathbb{R} \cup \{+\infty\}$, the binary function symbol $\oplus$ interpreted by $\min$ and the binary function symbol $\odot$ interpreted by $+$, the constant symbols $0_s$ and $1_s$ interpreted by $+\infty$ and $0_{\mathbb{R}}$, respectively, the binary relation symbol $\prec$ interpreted by the canonical order $<$ on $\mathbb{R} \cup \{+\infty\}$, and the unary function symbol $\mu$ interpreted by the identity function on $\mathbb{R} \cup \{+\infty\}$. The real tropical semiring is a strongly monotonic measurable semiring. It is not strictly monotonic measurable because $2 < 3$ but $2 \oplus 2 = \min(2, 2) = 2 \prec 2 = \min(3, 2) = 3 \oplus 2$.

**Example 4.** The real arctic semiring $\mathcal{A}' = (\mathbb{R} \cup \{-\infty\}, \max, +, -\infty, 0_{\mathbb{R}}, <, \mathrm{id}_{\mathbb{R} \cup \{-\infty\}})$ has domain $\mathbb{R} \cup \{-\infty\}$, the binary function symbol $\oplus$ interpreted by $\max$ and the binary function symbol $\odot$ interpreted by $+$, the constant symbols $0_s$ and $1_s$ interpreted by $-\infty$ and $0_{\mathbb{R}}$, respectively, the binary relation symbol $\prec$ interpreted by the canonical order $<$ on $\mathbb{R} \cup \{-\infty\}$, and the unary function symbol $\mu$ interpreted by the identity function on $\mathbb{R} \cup \{-\infty\}$. The real arctic semiring is a strongly monotonic measurable semiring. It is not strictly monotonic measurable because $2 < 3$ but $2 \oplus 3 = \max(2, 3) = 3 \prec 3 = \max(3, 3) = 3 \oplus 3$.
**Example 5.** The real arithmetic semiring $\mathfrak{N}' = (\mathbb{R}^+, +, *, 0_\mathbb{R}, 1_\mathbb{R}, <, \mathrm{id}_{\mathbb{R}^+})$ has as domain the set $\mathbb{R}^+$ of positive real numbers, the binary function symbol $\oplus$ interpreted by $+$ and the binary function symbol $\odot$ interpreted by $*$, the constant symbols $0_s$ and $1_s$ interpreted by $0_\mathbb{R}$ and $1_\mathbb{R}$, respectively, the binary relation symbol $<$ interpreted by the canonical order $<$ on $\mathbb{R}^+$, and the unary function symbol $\mu$ interpreted by the identity function on $\mathbb{R}^+$. The real arithmetic semiring is a strictly monotonic measurable semiring.

**Example 6.** The natural tropical semiring: $\mathcal{T} = (\mathbb{N} \cup \{+\infty\}, \min, +, +\infty, 0, <, \mathrm{id}_{\mathbb{N} \cup \{+\infty\}})$ and the natural arctic semiring: $\mathfrak{A} = (\mathbb{N} \cup \{-\infty\}, \max, +, -\infty, 0, <, \mathrm{id}_{\mathbb{N} \cup \{-\infty\}})$ are strongly monotonic measurable semirings. The natural arithmetic semiring $\mathfrak{N} = (\mathbb{N}, +, *, 0, 1, <, \mathrm{id}_\mathbb{N})$ is a strictly monotonic measurable semiring.

**Notation 2.** Let $(S, \oplus, \odot, 0_s, 1_s)$ be a semiring. We extend naturally the binary operations $\oplus$ and $\odot$ to finite sets $E \subseteq S$ by letting

* $\odot 0 \stackrel{\mathrm{def}}{=} 1_s$ and $\odot (E \cup \{x\}) \stackrel{\mathrm{def}}{=} (\odot E) \odot x$;

* $\oplus 0 \stackrel{\mathrm{def}}{=} 0_s$ and $\oplus (E \cup \{x\}) \stackrel{\mathrm{def}}{=} (\oplus E) \oplus x$.

# 4 Measuring objects by counting morphisms

Let $\mathcal{C}$ be an arbitrary category. The type graph method is parameterized by a tuple $\mathcal{T} = (T, \mathcal{E}, \mathcal{S}, w)$, called a **weighted type graph** [EO24a], consists of:

* an object $T$ in $\mathcal{C}$, called **type graph**,

* a strongly monotonic, measurable semiring $\mathcal{S} = (S, \oplus, \odot, 0_\mathcal{S}, 1_\mathcal{S}, <, \mu)$,

* a set $\mathcal{E}$ of morphisms with codomain $T$ in $\mathcal{C}$, called **morphism-rulers**,

* a weight function $w: \mathcal{E} \to S \setminus \{0_\mathcal{S}\}$,

* for every $(e: X \to T) \in \mathcal{E}$ and every object $G$, the sets $\mathrm{Hom}(X, G)$ and $\mathrm{Hom}(G, T)$ are finite.

**Example 7.** In Graph, a weighted type graph can be visualized as a graph with weighted labels and weights given as superscripts as proposed in [BKNZ15] if $\mathrm{dom}(\mathcal{E})$ consists of graphs with two vertices and one labeled edge between them. For example, the weighted type graph $\mathcal{T} = (T, \mathcal{E}, \mathcal{S}, w)$ with $\mathcal{S}$ as the real arithmetic semiring $(\mathbb{R}^+, +, *, 0_\mathbb{R}, 1_\mathbb{R}, <, \mathrm{id}_{\mathbb{R}^+})$, $T$ as the graph illustrated below (without superscripts), $\mathcal{E} = \{e_{11a}, e_{12a}, e_{21a}, e_{11b}\}$ as the set of morphism-rulers where $e_{uvl}$ has domain $\bullet \xrightarrow{l} \bullet$ and image $\mathrm{u} \xrightarrow{l} \mathrm{v}$ in the graph $T$, and $w(e) = 1.0$ for all $e \in \mathcal{E}$, can be visualized as follows:

<figure><img src="image_7.png" /></figure>

Analogous to the measurement of a physical object, a morphism-ruler measures a morphism, and provides a measurement, which is the number of $l$ that make the commutative triangle shown on the right (Definition 8).

<figure><img src="image_8.png" /></figure>

Combining the measurements of a morphism provided by all morphism-rulers with the help of the weight function $w$ gives the weight of the morphism (Definition 9), and the weight of an object is defined as the semiring sum of the weights of all morphisms from the object to the type graph $T$ (Definition 10).
**Notation 3** ([EO24a]). For morphisms $\alpha: A \to B$, $\beta: B \to C$, $\gamma: A \to C$ and $E \subseteq \text{Hom}(A, B)$, define:

$$ \{\alpha \star - = \gamma\} \stackrel{\text{def}}{=} \{\beta \in \text{Hom}(B, C) \mid \alpha \star \beta = \gamma\}. $$

$$ \{-\star\beta = \gamma\} \stackrel{\text{def}}{=} \{\alpha \in \text{Hom}(A, B) \mid \alpha \star \beta = \gamma\}. $$

$$ E \star \beta \stackrel{\text{def}}{=} \{\alpha \star \beta \mid \alpha \in E\}. $$

**Definition 8.** The measurement of a morphism $h: G \to T$ relative to a morphism-ruler $e: X \to T$, denoted $m_e(h)$, is defined as: $m_e(h) \stackrel{\text{def}}{=} |\{-\star h = e\}|$

Measurements of a morphism $h: G \to T$ provided by different morphism-rulers can be combined to obtain the weight of the morphism with the help of the weight function.

**Definition 9.** The weight of a morphism $h: G \to T$ relative to a type graph $\mathcal{T}$ is defined as the semiring product of $w(e)^{m_e(h)}$ for all $e \in \mathbb{E}$:

$$ w_{\mathcal{T}}(h) \stackrel{\text{def}}{=} \bigotimes_{e \in \mathbb{E}} w(e)^{m_e(h)} $$

**Definition 10.** The weight of an object $G$ is defined as the semiring sum of $w_{\mathcal{T}}(h)$, for all $h \in \text{Hom}(G, T)$:

$$ w_{\mathcal{T}}(G) \stackrel{\text{def}}{=} \bigoplus_{h \in \text{Hom}(G, T)} w_{\mathcal{T}}(h) $$

**Example 8.** Consider the following morphisms and the weighted type graph $\mathcal{T}$ from Example 7:

<figure><img src="image_9.png" /></figure>

We have $w_{\mathcal{T}}(h_{11}^1) = w(e_{13a})^{m_{e_{13a}}(h_{11}^1)} \odot w(e_{31a})^{m_{e_{31a}}(h_{11}^1)} = 1.0^1 * 1.0^1 = 1.0$ and $w_{\mathcal{T}}(h_{11}^2) = 1.0$

In certain scenarios, when measuring a morphism $h: G \to T$ relative to a morphism-ruler $e: X \to T$, it is necessary to exclude specific morphisms $\iota: X \to G$. For this reason, for any set $\Gamma \subseteq \text{Hom}(A, G)$, we define $\Gamma'$ as the set consisting of all morphisms $\iota: X \to G$ admitting morphisms $\zeta: X \to A$ and $\alpha \in \Gamma$ such that the diagram illustrated on the right is commutative. Formally,

<figure><img src="image_10.png" /></figure>

$$ \Gamma' \stackrel{\text{def}}{=} \{\iota \in \text{Hom}(X, G) \mid \exists \alpha \in \Gamma, \exists \zeta: X \to A, \zeta \star \alpha = \iota\}. $$

**Definition 11.** Let $\Gamma \subseteq \text{Hom}(A, G)$. The measurement of a morphism $h: G \to T$ relative to a morphism-ruler $e: X \to T$, excluding morphisms in $\Gamma'$, denoted $m_e(h - \Gamma)$, is defined as:

$$ m_e(h - \Gamma) \stackrel{\text{def}}{=} |\{-\star h = e\} \setminus \Gamma'| $$

**Definition 12.** The weight of a morphism $h: G \to T$ relative to a set $\mathbb{E}$ of morphism-rulers excluding morphisms in $\Gamma'$ is defined as the semiring product of $w(e)^{w_e(h - \Gamma)}$ for $e \in \mathbb{E}$:

$$ w_{\mathcal{T}}(h - \Gamma) \stackrel{\text{def}}{=} \bigotimes_{e \in \mathbb{E}} w(e)^{m_e(h - \Gamma)} $$
## 5 Estimating weights of pushout objects

Let $\mathcal{R} = \mathcal{A} \cup \mathcal{B}$ be a set of DPO rewriting rules and let $\mathcal{T} = (T, \mathbb{E}, \mathcal{S}, w)$ be a weighted type graph over the strongly monotonic measurable semiring $\mathcal{S}$. A proof of the following proposition can be found in [Qiu25a, Proposition 36].

**Proposition 1.** For all $x, y$ in $\mathcal{S}$:

$$0_{\mathcal{T}} \neq x \wedge 0_{\mathcal{T}} \neq y \Rightarrow 0_{\mathcal{T}} \neq x \odot y$$

$$1_{\mathcal{T}} \preceq x \wedge 1_{\mathcal{T}} \preceq y \wedge 0_{\mathcal{T}} \neq x \wedge 0_{\mathcal{T}} \neq y \Rightarrow 1_{\mathcal{T}} \preceq x \odot y$$

$$0_{\mathcal{T}} \neq x \wedge 0_{\mathcal{T}} \neq y \Rightarrow 0_{\mathcal{T}} \neq x \oplus y$$

Suppose that (1) $w(e) \succeq 1_{\mathcal{T}}$ for all $e \in \mathbb{E}$, and (2) for all $x \in \mathcal{S}$, if $1_{\mathcal{T}} \preceq x \neq 0_{\mathcal{T}}$ then $\mu(x) \geq \mu(1_{\mathcal{T}})$ and $\mu(x) \in \mathbb{R}$. By definition of a weighted type graph, $w(e) \neq 0_{\mathcal{T}}$ for all $e \in \mathbb{E}$. Therefore, by the proposition above, Hypothesis (1) and the definition of the weight of a morphism (Definition 9), for all morphisms $h$ from a finite graph $G$ to $\mathcal{T}$, we have $0_{\mathcal{T}} \neq w_{\mathcal{T}}(h) \succeq 1_{\mathcal{T}}$. By the above proposition, Axiom (S0) and the definition of the weight of an object (Definition 10), we conclude that for all objects $G$ with $\mathrm{Hom}(G, T) \neq \emptyset$, $0_{\mathcal{T}} \neq w_{\mathcal{T}}(G) \succeq 1_{\mathcal{T}}$. By Hypothesis (2), we have that for all objects $G$ with $\mathrm{Hom}(G, T) \neq \emptyset$, $\mu(w_{\mathcal{T}}(G)) \geq \mu(1_{\mathcal{T}}) = 0$ if $\mathcal{S}$ is the real tropical or arctic semiring, and $\mu(w_{\mathcal{T}}(G)) \geq 1$ if $\mathcal{S}$ is the arithmetic semiring.

Suppose additionally that for every graph $G$ subject to rewriting, we have $\mathrm{Hom}(G, T) \neq \emptyset$. The rewriting relation $\Rightarrow_{\mathcal{A}, \mathcal{T}}$ is terminating relative to $\Rightarrow_{\mathcal{B}, \mathcal{T}}$ if there exists a constant $\delta > 0$ such that: (i) for all $G \Rightarrow_{\mathcal{A}, \mathcal{T}} H$, $\mu(w_{\mathcal{T}}(G)) > \mu(w_{\mathcal{T}}(H)) + \delta$, and (ii) for all $G \Rightarrow_{\mathcal{B}, \mathcal{T}} H$, $\mu(w_{\mathcal{T}}(G)) \geq \mu(w_{\mathcal{T}}(H))$. However, directly verifying all rewriting steps is infeasible due to the potentially infinite number of rewriting steps.

In this section, we recall the concepts of traceability of objects (Definition 13) and relative monicity of morphisms (Definition 14), which are used to define the notion of weighable pushout squares (Definition 15). Using the notion of a weighable pushout square, we can bound the weight of the pushout object as explained below.

Consider a DPO diagram (illustrated on the right) that defines a rewriting step $G \Rightarrow_{\rho, \mathcal{T}} H$. If the left pushout square is weighable with $\mathcal{T}$ and the right pushout square is bounded above by $\mathcal{T}$ (concepts defined in Definition 15), then, by [EO24a, Lemma 4.13], we obtain:

<figure><img src="image_11.png" /></figure>

$$w_{\mathcal{T}}(G) = \bigoplus_{t_K:K \to T} \left( \bigoplus_{t_C:C \to T} w_{\mathcal{T}}(t_C - u) \right) \odot \left( \bigoplus_{t_{L:L \to T} \atop t_K=l*t_L} w_{\mathcal{T}}(t_L) \right)$$

$$w_{\mathcal{T}}(H) \preceq \bigoplus_{t_K:K \to T} \left( \bigoplus_{t_C:C \to T \atop t_K=u*t_C} w_{\mathcal{T}}(t_C - u) \right) \odot \left( \bigoplus_{t_R:R \to T \atop t_K=r*t_R} w_{\mathcal{T}}(t_R) \right)$$

According to these results, a termination criterion will be established in § 6 by comparing the weights $\bigoplus_{t_{L:L \to T}} w_{\mathcal{T}}(t_L)$ and $\bigoplus_{t_K=r*t_R} w_{\mathcal{T}}(t_R)$ for every $t_K: K \to T$.
**Definition 13** (Traceability [EO24a]).

An object $X \in \mathcal{C}$ is called **traceable** along a class of pushout squares $\Delta$ if for every diagram $\delta \in \Delta$ (shown on the right), the following hold

<figure><img src="image_12.png" /></figure>

(a) there exists a morphism $f : X \to B$ such that $h = f \star \beta'$, or

(b) there exists a morphism $g : X \to C$ such that $h = g \star \alpha'$.

If additionally, whenever (a) and (b) hold,

(c) there exists a morphism $k : X \to A$ such that $h = k \star \alpha \star \beta'$,

then we say that $X$ is **$\beta$-strongly traceable** along $\Delta$.

Consider the category **Graph**. Intuitively, a graph $X$ is $\beta$-strongly traceable along a pushout square as illustrated above, if whenever $X$ occurs in $D$, it occurs either in $B$ or in $C$, and if it occurs in both, then it occurs in $A$ as well.

**Remark 1** ([EO24a]). In **Graph**, the objects $\bullet$ and $\bullet \xrightarrow{x} \bullet$ (for edge labels $x$) are the only (non-initial) objects that are (strongly) traceable along all pushout squares. Other objects, such as loops $\bullet \looparrowright x$, are strongly traceable if all morphisms in the square are monomorphisms.

**Example 9.** For the DPO diagram in Example 2. The graph $\bullet \xrightarrow{a} \bullet \xrightarrow{a}$ is not traceable in both pushout squares. The graph $\bullet \xrightarrow{a}$ is traceable (and $u$-strongly traceable) along both pushout squares.

**Example 10.** The graph $\circ \xrightarrow{c} \circ$ is traceable along both pushout squares. It is $u$-strongly traceable along the left pushout square, but not $u$-strongly traceable along the right pushout square. The graph $\circ \xrightarrow{c} \circ \xrightarrow{c}$ is not traceable along both pushout squares.

<figure><img src="image_13.png" /></figure>

The following concepts are restricted versions of the concept of monicity.

**Definition 14** (Relative Monicity [EO24a]). Let $A, B, C$ and $X$ be objects, $\Gamma$ a set of objects, $S$ a set of morphisms to $A$ and $u : C \to A$ a morphism. A morphism $f : A \to B$ is called
(i) **monic for S** if $g \star f = h \star f$ implies $g = h$ for all $g, h \in S$;

(ii) **X-monic** if $f$ is monic for $\operatorname{Hom}(X, A)$.

(iii) **X-monic outside of u**, if $f$ is monic for $\operatorname{Hom}(X, A) \setminus (\operatorname{Hom}(X, C) \star u)$.

(iv) **Γ-monic** if $f$ is X-monic for every $X \in \Gamma$.

**Example 11** (Edge-Monicity [EO24a]). In **Graph**, let $\Gamma = \{ \xrightarrow{\bullet} \xleftarrow{\alpha} | 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.

**Definition 15** (Weighable Pushout Square [EO24a, § 4.9]).

Let $\mathcal{T} = (T, \mathbb{E}, S, w)$ be a finitary weighted type graph. Consider the pushout square $\delta$ shown on the right. We say that $\delta$ is

(a) **weighable** with $\mathcal{T}$ if the following hold:

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

(ii) $\beta'$ is $\mathrm{dom}(\mathbb{E})$-monic,

(iii) $\alpha'$ is $\mathrm{dom}(\mathbb{E})$-monic outside of $\beta$.

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

<figure><img src="image_14.png" /></figure>

# 6 A Termination Criterion

It is crucial to ensure that the weight of any object subject to rewriting is not $0_S$, because $0_S$ behaves unpredictably in strongly monotonic measurable semirings. For instance, in the natural and real tropical semirings $(\mathbb{N} \cup \{+\infty\}, \min, +)$, $0_S$ is the greatest element $+\infty$, while in the natural and real arctic semirings $(\mathbb{N} \cup \{-\infty\}, \max, +)$, $0_S$ is the smallest element $-\infty$. This issue is addressed by the existence of a context closure.

## 6.1 Context Closure

**Definition 16** (Context Closure [EO24a]).

Let $\mathcal{T} = (T, \mathbb{E}, S, w)$ be a type graph, $\rho = (L \stackrel{l}{\leftarrow} K \stackrel{r}{\rightarrow} R)$ a DPO rewriting rule and $\mathfrak{F}$ a rewriting framework. A **context closure** for $\rho$ and $\mathcal{T}$ in $\mathfrak{F}$ is a morphism $c: L \to T$ such that for every DPO diagram in $\mathfrak{F}(\rho)$ (shown on the right) there exists $\alpha: G \to T$ such that $m \star \alpha = c$.

<figure><img src="image_15.png" /></figure>

**Example 12.** Let the set of edge labels be $\Sigma = \{a, b\}$. Consider the DPO rule in Example 1, the weighted type graph in Example 7, and the morphism $c$ illustrated below. Since for every match $m: L \to G$, there exists a morphism $\alpha: G \to T$ such that $m \star \alpha = c$, the morphism $c$ is a context closure for the DPO rule in the type graph.

<figure><img src="image_16.png" /></figure>
## 6.2 Decreasing rules

The definition below adapts the concept of decreasing rules from [EO24a]. The difference lies in the treatment of weight comparisons for uniformly decreasing and closure decreasing rules: instead of directly comparing weights, we evaluate the difference between weights relative to the homomorphism $\mu$ of the strongly monotonic measurable semirings.

**Definition 17 (Decreasing Rules).** Let $\mathcal{T} = (T, \mathbb{E}, (S, \oplus, \odot, 0_S, 1_S, \prec, \mu), w)$ be a finitary weighted type graph, $\mathfrak{F}$ a DPO rewriting framework, $\rho = (L \stackrel{L}{\leftarrow} K \stackrel{R}{\rightarrow} R)$ a DPO rewriting rule, and $\delta \in \mathbb{R}_{>0}$.

The rule $\rho$ is **weakly decreasing** w.r.t. $\mathcal{T}$ in $\mathfrak{F}$ if for every $t_K: K \rightarrow T$,

$$w_{\mathcal{T}}(\{l^* = t_K\}) \geq w_{\mathcal{T}}(\{r^* = t_K\})$$

The rule $\rho$ is $\delta$-uniformly decreasing w.r.t. $\mathcal{T}$ in $\mathfrak{F}$ if the following hold:

- there exists a context closure $c_\rho$ for $\rho$ and $\mathcal{T}$ in $\mathfrak{F}$,

- for every $t_K: K \rightarrow T$,

• $\{l^* = t_K\} = \emptyset = \{r^* = t_K\}$, or

• $\mu(w_{\mathcal{T}}(\{l^* = t_K\})) > \mu(w_{\mathcal{T}}(\{r^* = t_K\})) + \delta$.

The rule $\rho$ is $\delta$-closure decreasing w.r.t. $\mathcal{T}$ in $\mathfrak{F}$ if the following hold:

- $S$ is strictly monotonic measurable semiring,

- $\rho$ is weakly decreasing,

- there exists a context closure $c_\rho$ for $\rho$ and $\mathcal{T}$ in $\mathfrak{F}$,

- $\mu(w_{\mathcal{T}}(\{l^* = t_K\})) > \mu(w_{\mathcal{T}}(\{r^* = t_K\})) + \delta$ for $t_K = l^*c_\rho$.

**Example 13.** Consider the DPO rule in Example 1 and the weighted type graph in Example 7 over the real arithmetic semiring $\mathfrak{N} = (\mathbb{R}^+, +, *, 0_{\mathbb{R}}, 1_{\mathbb{R}}, <, \mathrm{id}_{\mathbb{R}^+})$. There are $t_K^{11}, t_K^{12}, t_K^{21}, t_K^{22}: K \rightarrow T$ as depicted below:

<figure><img src="image_17.png" /></figure>

<figure><img src="image_18.png" /></figure>

The set $\{l^* = t_K^{11}\}$ has two morphisms $h_{11}^1$ and $h_{11}^2$ as illustrated below:

<figure><img src="image_19.png" /></figure>
Therefore, we have

$$
\begin{align*}
w_{\mathcal{F}}(\{l^* = -t_K^{11}\}) &= w_{\mathcal{F}}(\{h_{11}^1, h_{11}^2\}) \\
&\stackrel{\text{def}}{=} w_{\mathcal{F}}(h_{11}^1) + w_{\mathcal{F}}(h_{11}^2) \\
&= (1.0^1 * 1.0^1) + (1.0^1 * 1.0^1) \\
&= 2.0
\end{align*}
$$

The set {$r^* = -t_K^{11}$} has one morphism $h_{11}^3$ as illustrated below:

<figure><img src="image_20.png" /></figure>

Therefore, we have: $w_{\mathcal{F}}(\{r^* = -t_K^{11}\}) = w_{\mathcal{F}}(h_{11}^3) = 1.0^1 * 1.0^1 * 1.0^1 = 1.0$. Thus, we have $w_{\mathcal{F}}(\{l^* = -t_K^{11}\}) = 2.0 \ge 1.0 = w_{\mathcal{F}}(\{r^* = -t_K^{11}\})$.

Similarly, we can check that $w_{\mathcal{F}}(\{l^* = -t_K^{12}\}) = 1.0 \ge 1.0 = w_{\mathcal{F}}(\{r^* = -t_K^{12}\})$, $w_{\mathcal{F}}(\{l^* = -t_K^{21}\}) = 1.0 \ge 1.0 = w_{\mathcal{F}}(\{r^* = -t_K^{21}\})$, and $w_{\mathcal{F}}(\{l^* = -t_K^{22}\}) = 1.0 \ge 1.0 = w_{\mathcal{F}}(\{r^* = -t_K^{22}\})$. The rule is therefore weakly decreasing.

There exists a context closure c for the DPO rule in the weighted type graph, as shown in Example 12.
Since we have additionally $t_K^{11} = l^*c$ and $w_{\mathcal{F}}(\{l^* = -t_K^{11}\}) = 2.0 > 1.0 + \delta = w_{\mathcal{F}}(\{r^* = -t_K^{11}\}) + \delta$
for $0 < \delta < 1.0$, the rule is $\delta$-closure decreasing with $0 < \delta < 1.0$ since the semiring is strictly monotonic
measurable.

Adapted from [EO24a, Theorem C.3], the lemma below relates decreasing rules to weight reduction
under specific constraints. For its proof, we refer to [Qiu25a, Theorem 36].

**Lemma 1 (Decreasing steps).**

Let $\mathcal{T} = (T, \mathbb{E}, (S, \oplus, \odot, 0_S, 1_S, \prec, \mu), w)$ be a finitely weighted type graph, $\rho$ a rewriting rule and $\Delta \in \mathcal{F}(\rho)$ a DPO diagram (shown on the right) such that the following conditions hold:

<figure><img src="image_21.png" /></figure>

• left(Δ) is weighable with $\mathcal{T}$, and

• right(Δ) is bounded above by $\mathcal{T}$, and

• $w(e) \succeq 1_S$ for all $e \in \mathbb{E}$.

We have:

• $\mu(w_{\mathcal{F}}(G)) \geq \mu(w_{\mathcal{F}}(H))$ if $\rho$ is weakly decreasing,

• $\mu(w_{\mathcal{F}}(G)) > \mu(w_{\mathcal{F}}(H)) + \delta$ if $\rho$ is $\delta$-uniformly or $\delta$-closure decreasing for some $\delta > 0$ and $w(e) \succeq 1_S$ for all $e \in \mathbb{E}$.
## 6.3 Termination Criterion

Finally, we formulate a termination criterion leveraging type graphs weighted over non-well-founded semirings. For its proof, we refer to [Qiu25a, Theorem 37].

**Theorem 1 (Termination of DPO rewriting system).** Let $\mathcal{A}$ and $\mathcal{B}$ be sets of DPO rewriting rules, $\mathcal{T} = (T, \mathcal{E}, (S, \oplus, \odot, 0_S, 1_S, \prec, \mu), w)$ a finitary weighted type graph and $\mathfrak{F}$ a DPO rewriting framework such that

i) $w(e) \succeq 1_S$ for all $e \in \mathcal{E}$, and

ii) for all $x \in S$, if $1_S \preceq x \neq 0_S$ then $\mu(x) \geq \mu(1_S)$ and $\mu(x) \in \mathbb{R}$, and

iii) for every rule $\rho \in (\mathcal{A} \cup \mathcal{B})$ and every double pushout diagram $\Delta \in \mathfrak{F}(\rho)$

* left($\Delta$) is weighable with $\mathcal{T}$,

* right($\Delta$) is bounded above by $\mathcal{T}$.

If the following conditions hold:

1. there exists $\delta > 0$ such that either every $\rho \in \mathcal{A}$ is $\delta$-uniformly decreasing, or every $\rho \in \mathcal{A}$ is $\delta$-closure decreasing, and

2. every rule $\rho \in \mathcal{B}$ is weakly decreasing,

then $\Rightarrow_{\mathcal{A}, \mathfrak{F}}$ is terminating relative to $\Rightarrow_{\mathcal{B}, \mathfrak{F}}$.

**Example 14.** Termination of the DPO rule in Example 1 can be established using Theorem 1 together with the weighted type graph in Example 7 over the real arithmetic semiring $\mathfrak{N}' = (\mathbb{R}^+, +, *, 0_{\mathbb{R}}, 1_{\mathbb{R}}, <, \mathrm{id}_{\mathbb{R}^+})$. It is $\delta$-closure decreasing with $\delta = 0.5$ by Example 13.

# 7 Implementation

We have implemented both our approach and the one proposed by Endrullis and Overbeek [EO24a] for edge-labeled DPO rewriting systems into a unified tool. These two approaches can be launched in parallel and collaborate to establish termination of a DPO rewriting system.

**Searching Strategy.** Consider a DPO rewriting system $\mathcal{R}$. Given a fixed semiring $S$, a processor is spawned to iteratively search for a suitable weighted type graph over $S$. The search starts with a weighted type graph containing 1 node, incrementally increasing the node count by 1 until a maximum of 4 nodes is reached. For a fixed number of nodes, if $S$ is a semiring over the natural numbers, the maximum edge weight is initialized to 1 and incremented by 1 (up to a limit of 3) if no suitable weighted type graph is found; if $S$ is a semiring over the real numbers, the search is performed over all real numbers. Processors targeting different semirings can run in parallel to analyze the same DPO rewriting system. When a processor discovers a weighted type graph that witnesses relative termination of a subset of rules $\mathcal{A}$ with respect to another subset of rules $\mathcal{B}$ such that $\mathcal{R} = \mathcal{A} \cup \mathcal{B}$, it broadcasts this result to all processors and waits for them to terminate. If $\mathcal{B} = \emptyset$, the system's termination is proven. Otherwise, we initiate a new search for the rules in $\mathcal{B}$ unless a timeout is reached.

For a fixed number of nodes $k$, we adopt the approach proposed in [BKNZ15, BKZ14, ZKB14] to reduce the search space. Specifically, we construct a weighted type graph with $k$ nodes and no parallel edges of the same label. The search proceeds as follows: (1) decide if $s \xrightarrow{1} t$ exists for every pair of nodes $s, t$ and label $l$; (2) assign a weight to every existing edge (3) verify the existence of a constant
$\delta > 0$ and a partition of the rule set $\mathcal{R}$ into a non-empty subset $\mathcal{A}$ and a subset $\mathcal{B}$ such that: (i) either all rules in $\mathcal{A}$ are $\delta$-uniformly decreasing or all rules in $\mathcal{A}$ are $\delta$-closure decreasing, and all rules in $\mathcal{B}$ are weakly decreasing. This procedure can be reduced to checking the satisfiability of an existential Presburger arithmetic, Peano arithmetic, linear real arithmetic, or non-linear real arithmetic formula depending on the semiring $\mathcal{S}$ considered.

**Z3 Modeling.** The type graph $T$ is modeled in Z3 by defining a Boolean variable $x_{u,v,l} \in \mathbb{B}$ for every directed labeled edge $u \stackrel{l}{\to} v$ in the type graph, where $u, v \in \{1, ..., k\}$ are nodes and $l \in \Sigma$ is an edge label. The variable $x_{u,v,l}$ has the value “true” if the directed edge $u \stackrel{l}{\to} v$ exists in the result type graph, “false” otherwise.

The weight function $w$ and the set $\mathbb{E}$ of morphism-rulers are modeled in Z3 by defining a variable $y_{u,v,l}$ in $\mathbb{N}$ or $\mathbb{R}_{\ge 0}$, depending on the semiring $\mathcal{S}$ considered, for every pair $u, v \in \{1, ..., k\}$ of nodes and edge label $l \in \Sigma$. The variable $y_{u,v,l}$ represents the weight of the directed labeled edge $u \stackrel{l}{\to} v$ in the resulting weighted type graph, but only if edge $u \stackrel{l}{\to} v$ exists (i.e. $x_{u,v,l}$ has the value “true”).

A variable $\delta \in \mathbb{R}_{>0}$ is defined to ensure that there is a partition of the rule set $\mathcal{R}$ into a non-empty subset $\mathcal{A}$ and a subset $\mathcal{B}$ such that all rules in $\mathcal{A}$ are either $\delta$-uniformly decreasing or $\delta$-closure decreasing, and all rules in $\mathcal{B}$ are weakly decreasing.

For convenience, the following auxiliary variables are also defined: a Boolean variable $v_h \in \mathbb{B}$ for every morphism $h$ from $L$ or $R$ to $T$; a real-valued variable $v_{h'} \in \mathbb{R}_{\ge 0}$ for every morphism $h$ from $L$ or $R$ to $T$; a Boolean variable $v_c \in \mathbb{B}$ for every morphism $c$ from $L$ to $T$.

The value of $v_h$ has the value “true” if the morphism $h$ exists in the result type graph (i.e. all edges in its image exist), and “false” otherwise. The variable $v_{h'}$ holds the weight of the morphism $h$, provided the morphism $h$ exists (i.e., $v_h$ is true). The variable $v_c$ has the value “true” if the morphism $c$ exists in the result type graph and can serve as a context closure for the rule, and “false” otherwise.

If there exists an assignment of values to $(x_{u,v,l})_{u,v \in \{1, ..., k\}}, l \in \Sigma$, $(y_{u,v,l})_{u,v \in \{1, ..., k\}}, l \in \Sigma$ and $\delta$ such that all conditions of Theorem 1 are satisfied, then a suitable weighted type graph that witnesses termination of the DPO rewriting system can be constructed: the values of $(x_{u,v,l})_{u,v \in \{1, ..., k\}}, l \in \Sigma$ define the type graph $T$; the values of $(y_{u,v,l})_{u,v \in \{1, ..., k\}}, l \in \Sigma$ define the weight function $w$ and the set $\mathbb{E}$ of morphism-rulers.

# 8 Empirical Results

We evaluated our OCaml implementation using 13 examples from [EO24a, Table 1], excluding [EO24a, Example 6.4] which is a DPO rewriting system in an unsupported category, and [BKNZ14, Example 6] because it duplicates [BKNZ15, Example 4]. Our approach with semirings over the real numbers proves termination for 8 out of 13 systems tested. Table 1 summarizes runtime performance across benchmark examples under different semiring configurations $^3$.

# 9 Discussion

**Acceleration with the real tropical/arctic semiring.** Consider the examples in Table 1 whose termination is provable using the tropical or arctic semirings. For all such examples except [Plu18, Example 5] and [BKNZ15, Example 4], the real-number semiring approach achieves better runtime performance than

<footnote>$^3$Experiments were conducted on a laptop equipped with an i5-1038NG7 CPU, which features 4 cores, a base clock speed of 2 GHz, and a boost speed of 3.8 GHz.</footnote>
<table><caption>Table 1: Runtime performance in seconds (200s timeout). Columns denote semirings: “A”, “T”, “N” denote the arctic, tropical, and arithmetic semirings over the (extended) natural numbers; “a”, “t”, “n” denote the arctic, tropical, and arithmetic semirings over the (extended) real numbers. Empty cells indicate termination not proven.</caption><thead><tr><th></th><th>A</th><th>a</th><th>T</th><th>t</th><th>N</th><th>n</th></tr></thead><tbody><tr><td>[EO24a, Example 6.2]</td><td></td><td></td><td></td><td></td><td>2.68</td><td>1.15</td></tr><tr><td>[EO24a, Example 6.3]</td><td></td><td></td><td></td><td></td><td>2.74</td><td>1.16</td></tr><tr><td>[EO24a, Example D.3]</td><td>2.25</td><td>1.18</td><td></td><td></td><td>2.24</td><td>1.18</td></tr><tr><td>[Plu95, Example 3.8]</td><td>2.95</td><td>1.90</td><td>2.94</td><td>1.87</td><td>3.49</td><td>1.87</td></tr><tr><td>[Plu18, Example 4]</td><td>4.26</td><td>3.19</td><td>4.24</td><td>3.13</td><td>5.82</td><td>timeout</td></tr><tr><td>[Plu18, Example 5]</td><td>5.54</td><td>5.55</td><td>5.53</td><td>5.50</td><td>9.11</td><td>5.62</td></tr><tr><td>[Plu18, Example 6]</td><td></td><td></td><td></td><td></td><td></td><td></td></tr><tr><td>[BKNZ15, Example 4]</td><td>2.44</td><td>2.46</td><td>2.47</td><td>2.54</td><td>4.58</td><td>2.46</td></tr><tr><td>[BKNZ15, Example 5]</td><td></td><td></td><td></td><td></td><td>7.80</td><td>timeout</td></tr><tr><td>[BKNZ15, Example 6]</td><td></td><td></td><td></td><td></td><td>9.75</td><td>timeout</td></tr><tr><td>[BKZ14, Example 1]</td><td>2.26</td><td>1.18</td><td></td><td></td><td>2.24</td><td>1.18</td></tr><tr><td>[BKZ14, Example 4]</td><td>2.25</td><td>1.22</td><td>2.24</td><td>1.18</td><td>2.25</td><td>1.19</td></tr><tr><td>[BKZ14, Example 5]</td><td>4.23</td><td>3.23</td><td>4.25</td><td>3.28</td><td>5.82</td><td>timeout</td></tr></tbody></table>

the natural-number semiring approach. The acceleration rate varies across examples due to Z3’s internal heuristics. This result is notable because termination proofs for these systems only require weighted type graphs with small edge weights (e.g., values less than 2 for most examples and at most 3 for all), which theoretically favors the implementation of the natural-number semiring approach.

**Timeout with the real arithmetic semiring.** The systems whose termination is not proven by our tool are [Plu18, Example 6], [BKNZ15, Examples 5 and 6], [Plu18, Example 4], and [BKZ14, Example 5]. The first case ([Plu18, Example 6]) is due to a limitation of the type graph method in general, as the system has a rule whose right-hand side graph can be embedded into its left-hand side graph, which is problematic for the type graph method as pointed out in [EO24a, Example D.4]. For the remaining cases, the failure stems from the double-exponential time complexity [Col74, JM12] in the number of variables $(x_{u,v,l})_{u,v \in \{1, \dots, k\}, l \in \Sigma}$ and $(y_{u,v,l})_{u,v \in \{1, \dots, k\}, l \in \Sigma}$, which is also influenced by the length of the conditions of Theorem 1 encoded in Z3.

**Acceleration with the real arithmetic semiring.** For some examples, the approach with semirings on real numbers can achieve a better runtime performance than the approach with semirings on natural numbers. These are (1) examples which need weighted type graphs with 1 or 2 nodes, and the constraints can be expressed in Z3 with a short formula, or (2) examples which can first be simplified by eliminating some rules using weighted type graphs with 1 node, and then the remaining rules can be easily shown to terminate as the first case.
**Interest of the approach with semiring on natural numbers.** In the cases where the termination cannot be proven with the semiring on real numbers, using the semiring on natural numbers is more efficient, as it allows one to restrict the search space to an extremely small size by bounding the maximum weight of edges, which is not possible for the semiring on real numbers. However, this advantage can be achieved only if the termination can be proven with a weighted type graph with small edge weights, as is the case for all examples from the previous work in the type graph method.

**Limitations of our experiments.** While our search strategy is very close to the real-world scenario that a non-expert user would use to prove termination of DPO rewriting systems, it makes it difficult to estimate the runtime performance gain of our approach over the one proposed by Endrullis and Overbeek [EO24a]. This is because the reported runtimes include (1) translation of constraints into Z3's input format, (2) the time spent in Z3 to solve the constraint system, and (3) the parallelism overhead. Another problem is that the examples in our experiments are limited to those whose termination can be proven with a weighted type graph whose edge weights are small (at most 3). These examples favor the approach with semirings on natural numbers, as the search space is extremely small when the maximum edge weight is bounded by 3.

**Comparison with GraphTT-wtg.** A comparison of our implementation of the approach with semirings on real numbers with the one proposed in GraphTT-wtg by Endrullis and Overbeek [EO24b] is desired, but this tool is not publicly available and we do not think their article provides enough information of the implementation to allow us to do so.

# 10 Conclusion

The type graph method is a technique for proving termination of DPO rewriting systems. To apply this method, one needs to construct a weighted type graph over a semiring that witnesses termination of the rewriting system, and three concrete well-founded semirings over the natural numbers have been proposed in prior work: the tropical semiring, the arctic semiring, and the arithmetic semiring. However, constructing suitable weighted type graphs over these concrete semirings for DPO rewriting systems on edge-labeled directed multigraphs is difficult. To address this challenge, we investigate weighted type graphs over non-well-founded semirings, and propose three corresponding concrete semirings over the real numbers: the tropical semiring, the arctic semiring, and the arithmetic semiring. Construction of weighted type graphs over these concrete semirings is computationally easier.

We implemented both our approach and the one proposed by Endrullis et al. [EO24a] for DPO rewriting systems on edge-labeled directed multigraphs into a unified tool. Experiments show that for the tropical and arctic semirings, the weighted type graphs over the real semiring can be constructed more easily, but for the arithmetic semiring, the weighted type graphs over the real semiring are more difficult to construct than those over the natural semiring.

A promising direction involves generalizing the type graph method to other algebraic graph rewriting formalisms, broadening its applicability in automated verification.

# Acknowledgments

I thank the anonymous reviewers for their valuable feedback; my supervisor, Xavier Urbain, for his guidance; and my mother and wife for their unwavering support.
References

[BHK21] N. Behr, R. Harmer & J. Krivine (2021): *Concurrency Theorems for Non-linear Rewriting Theories*. CoRR abs/2105.02842. arXiv:2105.02842.

[BHK23] N. Behr, R. Harmer & J. Krivine (2023): *Fundamentals of compositional rewriting theory*. *J. Log. Algebraic Methods Program.* 135, p. 100893, doi:10.1016/J.JLAMP.2023.100893. Available at https://doi.org/10.1016/j.jlamp.2023.100893.

[BKNZ15] H.J.S. Bruggink, B. König, D. Nolte & H. Zantema (2015): *Proving Termination of Graph Transformation Systems using Weighted Type Graphs over Semirings*. CoRR abs/1505.01695. arXiv:1505.01695.

[BKZ14] H.J.S. Bruggink, B. König & H. Zantema (2014): *Termination Analysis for Graph Transformation Systems*. In J. Díaz, I. Lanese & D. Sangiorgi, editors: *Theoretical Computer Science - 8th IFIP TC 1/WG 2.2 International Conference, TCS 2014, Rome, Italy, September 1-3, 2014. Proceedings, Lecture Notes in Computer Science* 8705, Springer, pp. 179-194, doi:10.1007/978-3-662-44602-7_15.

[BN24] N. Bjørner & L. Nachmanson (2024): *Arithmetic Solving in Z3*. In A. Gurfinkel & V. Ganesh, editors: *Computer Aided Verification*, Springer Nature Switzerland, Cham, pp. 26-41.

[Bru24] H.S. Bruggink (2024): *Grez*. https://www.ti.inf.uni-due.de/research/tools/grez/. Accessed: 2024-11-07.

[BW95] M. Barr & C. Wells (1995): *Category theory for computing science (2. ed.).* Prentice Hall international series in computer science, Prentice Hall.

[CCF+11] E. Contejean, P. Courtieu, J. Forest, O. Pons & X. Urbain (2011): *Automated Certified Proofs with CiME3*. In M. Schmidt-Schauß, editor: *Proceedings of the 22nd International Conference on Rewriting Techniques and Applications, RTA 2011, May 30 - June 1, 2011, Novi Sad, Serbia, LIPIcs* 10, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, pp. 21-30, doi:10.4230/LIPICS.RTA.2011.21.

[CMR+97] A. Corradini, U. Montanari, F. Rossi, H. Ehrig, R. Heckel & M. Löwe (1997): *Algebraic Approaches to Graph Transformation - Part I: Basic Concepts and Double Pushout Approach*. In G. Rozenberg, editor: *Handbook of Graph Grammars and Computing by Graph Transformations, Volume 1: Foundations*, World Scientific, pp. 163-246.

[Col74] G.E. Collins (1974): *Quantifier elimination for real closed fields by cylindrical algebraic decomposition-preliminary report*. SIGSAM Bull. 8(3), pp. 80-90, doi:10.1145/1086837.1086852. Available at https://doi.org/10.1145/1086837.1086852.

[CRTU16] P. Courtieu, L. Rieg, S. Tixeuil & X. Urbain (2016): *Certified Universal Gathering in $\mathbb{R}^2$ for Oblivious Mobile Robots*. In C. Gavoille & D. Ilcinkas, editors: *Distributed Computing - 30th International Symposium, DISC 2016, Paris, France, September 27-29, 2016. Proceedings, Lecture Notes in Computer Science* 9888, Springer, pp. 187-200, doi:10.1007/978-3-662-53426-7_14.

[Dut14] B. Dutertre (2014): *Yices 2.2*. In A. Biere & R. Bloem, editors: *Computer Aided Verification - 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18-22, 2014. Proceedings, Lecture Notes in Computer Science* 8559, Springer, pp. 737-744, doi:10.1007/978-3-319-08867-9_49. Available at https://doi.org/10.1007/978-3-319-08867-9_49.

[EO24a] J. Endrullis & R. Overbeek (2024): *Generalized Weighted Type Graphs for Termination of Graph Transformation Systems*. arXiv:2307.07601v2.

[EO24b] J. Endrullis & R. Overbeek (2024): *Termination of Graph Transformation Systems via Generalized Weighted Type Graphs*. arXiv:2307.07601v3.

[Ges90] A. Geser (1990): *Relative Termination*. Ph.D. thesis, University of Passau, Germany. Available at http://vts.uni-ulm.de/docs/2012/8146/vts_8146_11884.pdf.

[HMP01] A. Habel, J. Müller & D. Plump (2001): *Double-pushout graph transformation revisited*. *Math. Struct. Comput. Sci.* 11(5), pp. 637-688, doi:10.1017/S0960129501003425.
[HUW14] J. Harrison, J. Urban & F. Wiedijk (2014): **History of Interactive Theorem Proving**. In J.H. Siekmann, editor: *Computational Logic, Handbook of the History of Logic* 9, Elsevier, pp. 135–214, doi:10.1016/B978-0-444-51624-4.50004-6.

[JM12] D. Jovanovic & L.M. de Moura (2012): **Solving Non-linear Arithmetic**. In B. Gramlich, D. Miller & U. Sattler, editors: *Automated Reasoning - 6th International Joint Conference, IJCAR 2012, Manchester, UK, June 26-29, 2012. Proceedings, Lecture Notes in Computer Science* 7364, Springer, pp. 339–354, doi:10.1007/978-3-642-31365-3_27. Available at https://doi.org/10.1007/978-3-642-31365-3_27.

[JM13] D. Jovanovic & L.M. de Moura (2013): **Cutting to the Chase - Solving Linear Integer Arithmetic**. *J. Autom. Reason.* 51(1), pp. 79–108, doi:10.1007/S10817-013-9281-X. Available at https://doi.org/10.1007/s10817-013-9281-x.

[Klo87] J.W. Klop (1987): **Term Rewriting Systems: A Tutorial**. *Bulletin of the European Association for Theoretical Computer Science*.

[KNPR18] B. König, D. Nolte, J. Padberg & A. Rensink (2018): **A Tutorial on Graph Transformation**. In R. Heckel & G. Taentzer, editors: *Graph Transformation, Specifications, and Nets - In Memory of Hartmut Ehrig, Lecture Notes in Computer Science* 10800, Springer, pp. 83–104, doi:10.1007/978-3-319-75396-6_5.

[LSP19] L. Lamport, R.E. Shostak & M.C. Pease (2019): **The Byzantine generals problem**. In D. Malkhi, editor: *Concurrency: the Works of Leslie Lamport*, ACM, pp. 203–226, doi:10.1145/3335772.3335936.

[Mat03] Y. Matiyasevich (2003): **Enumerable sets are diophantine**. *Mathematical logic in the 20th century*, pp. 269–273.

[MB08] L.M. de Moura & N.S. Bjørner (2008): **Z3: An Efficient SMT Solver**. In C.R. Ramakrishnan & J. Rehof, editors: *Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings, Lecture Notes in Computer Science* 4963, Springer, pp. 337–340, doi:10.1007/978-3-540-78800-3_24. Available at https://doi.org/10.1007/978-3-540-78800-3_24.

[OE22] R. Overbeek & J. Endrullis (2022): **A PBPO+ Graph Rewriting Tutorial**. In C. Grabmayer, editor: *Proceedings Twelfth International Workshop on Computing with Terms and Graphs, TERMGRAPH@FSCD 2022, Technion, Haifa, Israel, 1st August 2022, EPTCS* 377, pp. 45–63, doi:10.4204/EPTCS.377.3.

[Pie91] B.C. Pierce (1991): **Basic category theory for computer scientists**. *Foundations of computing*, MIT Press.

[Plu95] D. Plump (1995): **On Termination of Graph Rewriting**. In M. Nagl, editor: *Graph-Theoretic Concepts in Computer Science, 21st International Workshop, WG '95, Aachen, Germany, June 20-22, 1995, Proceedings, Lecture Notes in Computer Science* 1017, Springer, pp. 88–100, doi:10.1007/3-540-60618-1_68.

[Plu18] D. Plump (2018): **Modular Termination of Graph Transformation**. In R. Heckel & G. Taentzer, editors: *Graph Transformation, Specifications, and Nets - In Memory of Hartmut Ehrig, Lecture Notes in Computer Science* 10800, Springer, pp. 231–244, doi:10.1007/978-3-319-75396-6_13.

[PSTU19] M. Potop-Butucaru, N. Sznajder, S. Tixeuil & X. Urbain (2019): **Formal Methods for Mobile Robots**. In P. Flocchini, G. Prencipe & N. Santoro, editors: *Distributed Computing by Mobile Entities, Current Research in Moving and Computing, Lecture Notes in Computer Science* 11340, Springer, pp. 278–313, doi:10.1007/978-3-030-11072-7_12.

[Qiu25a] Q. Qiu (2025): **Termination of Graph Rewriting using Weighted Type Graphs over Non-well-founded Semirings**. Technical Report, Universite Claude Bernard Lyon 1 (UCBL), Lyon, FRA. Available at https://hal.science/hal-04954960v2.
[Qiu25b] Q. Qiu (2025): Termination of Injective DPO Graph Rewriting Systems using Subgraph Counting. Technical Report, Universite Claude Bernard Lyon 1. Available at https://hal.science/ hal-04955684.

[SP24] R. Söldner & D. Plump (2024): Formalising the Double-Pushout Approach to Graph Transformation. Log. Methods Comput. Sci. 20(4), doi:10.46298/LMCS-20(4:3)2024.

[Zan24] H. Zantema (2024): TORPAcyc. https://hzantema.win.tue.nl/torpa.html. Accessed: 2024-11-07.

[ZKB14] H. Zantema, B. König & H.J.S. Bruggink (2014): Termination of Cycle Rewriting. In G. Dowek, editor: Rewriting and Typed Lambda Calculi - Joint International Conference, RTA-TLCA 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings, Lecture Notes in Computer Science 8560, Springer, pp. 476–490, doi:10.1007/978-3-319-08918-8_33.
# 11 Appendix

The following proposition ensures that every morphism to a type graph $(T, S, \mathbb{E}, w)$ has a weight different from $0_S$. Additionally, if every T-valued element has a weight greater than $1_S$, then the weight of a morphism to a type graph is greater than $1_S$ too. This lemma will be used in Lemma 2.

**Proposition 2.** Let $(S, \oplus, \odot, 0_S, 1_S, \prec, \mu)$ be a strongly monotonic measurable semiring. We have for all $x, y \in S$:

$$0_S \neq x \wedge 0_S \neq y \Rightarrow 0_S \neq x \odot y \qquad (S10)$$

$$1_S \preceq x \wedge 1_S \preceq y \wedge 0_S \neq x \wedge 0_S \neq y \Rightarrow 1_S \preceq x \odot y \qquad (S11)$$

$$0_S \neq x \wedge 0_S \neq y \Rightarrow 0_S \neq x \oplus y \qquad (S12)$$

*Proof.* Let $x, y \in S$ such that $x, y \neq 0_S$. By definition, $\prec$ is not empty, therefore there exist $a, b \in S$ such that $a \prec b$.

* $\prec$ is irreflexive, because $\mu : (S, \prec) \to (\bar{\mathbb{R}}, \prec)$ is a homomorphism.

* S10: Suppose $(x \odot y) = 0_S$. We have

$$
\begin{align*}
0_S &= a \odot 0_S && 0_S \text{ is annihilator for } \odot \\
    &= a \odot (x \odot y) && \text{by assumption on } x \odot y \\
    &= a \odot x \odot y && \text{by associativity} \\
    &\prec b \odot x \odot y && \text{by (S5) and } x, y \neq 0_S \\
    &= b \odot (x \odot y) && \text{by associativity} \\
    &= b \odot 0_S && \text{by assumption on } x \odot y \\
    &= 0_S
\end{align*}
$$

which contradicts the irreflexivity of $\prec$.

* S11: Suppose $1_S \preceq x$ and $1_S \preceq y$. We have either $1_S = x$ or $1_S \prec x$. If $1_S = x$ then

$$
\begin{align*}
x \odot y &= 1_S \odot y \\
&= y \\
&\preceq 1_S && \text{by assumption}
\end{align*}
$$

If $1_S \prec x$ then $1_S \odot y \prec x \odot y$ by (S5) since $y \neq 0$ by assumption.

* S12: By (S5), we have $a \odot x \prec b \odot x$ and $a \odot y \prec b \odot y$.

$$
\begin{align*}
a \odot (x \oplus y) &= (a \odot x) \oplus (a \odot y) && \text{by distributivity} \\
\prec (b \odot x) \oplus (b \odot y) && \text{by (S2)} \\
&= b \odot (x \oplus y) && \text{by distributivity}
\end{align*}
$$

if $x \oplus y = 0_S$ then we have $0_S = a \odot 0_S = a \odot (x \oplus y) \prec b \odot (x \oplus y) = b \odot 0_S = 0_S$ which contradicts the irreflexivity of $\prec$.

☐

☐
The following lemma guaranteeing that, under certain constraints: exact weights of host graphs can be computed, and upper bounds for result-graph weights can be derived.

**Lemma 2 ([EO24a])**.

Let $\mathcal{T} = (T, \mathbb{E}, (S, \oplus, \odot, 0_S, 1_S, \prec, \mu), w)$ be a finitary weighted type graph. Consider the pushout square $\delta$ illustrated on the right. We define
$$ \begin{array}{ccc} A & \xrightarrow{\alpha} & B \\ \beta & \searrow & \delta \\ C & \xrightarrow{\alpha'} & D \end{array} $$

$$ k = \bigoplus_{t_A:A \to T} \left( \bigoplus_{\substack{t_C:C \to T \\ t_A = \beta \star t_C}} w_{\mathcal{T}}(t_C - \beta) \right) \odot w_{\mathcal{T}}(\{\alpha \star - = t_A\}) $$

The following conditions hold

(A) $w_{\mathcal{T}}(D) = k$ if $\delta$ is weighable with $\mathcal{T}$.

(B) $w_{\mathcal{T}}(D) \leq k$ if $\delta$ is bounded above by $\mathcal{T}$ and $w(e) \geq 1_S$ for all $e \in \mathbb{E}$.

The proof of the following lemma follows the structure of the proof of [EO24a, Theorem C.3] to make the comparison with the original proof easier.

**Lemma 1**

Let $\mathcal{T} = (T, \mathbb{E}, (S, \oplus, \odot, 0_S, 1_S, \prec, \mu), w)$ be a finitary weighted type graph, $\rho$ a rewriting rule and $\Delta \in \mathfrak{F}(\rho)$ a DPO diagram (shown on the right) such that the following conditions hold:
$$ \begin{array}{cccc} L & \leftarrow & L & R \\ \downarrow & & \downarrow & \\ G & \leftarrow & C & \rightarrow H \end{array} $$

• left($\Delta$) is weighable with $\mathcal{T}$,

• right($\Delta$) is bounded above by $\mathcal{T}$,

• $w(e) \geq 1_S$ for all $e \in \mathbb{E}$.

We have:

• $\mu(w_{\mathcal{T}}(G)) \geq \mu(w_{\mathcal{T}}(H))$ if $\rho$ is weakly decreasing,

• $\mu(w_{\mathcal{T}}(G)) > \mu(w_{\mathcal{T}}(H)) + \delta$ if $\rho$ is $\delta$-uniformly or $\delta$-closure decreasing for some $\delta > 0$ and $w(e) \geq 1_S$ for all $e \in \mathbb{E}$.

*Proof.* For every $t_K: K \to T$, we define $S_{t_K} \stackrel{\text{def}}{=} \bigoplus_{\substack{t_C:C \to T \\ t_K=h_{KC}*t_C}} w_{\mathcal{T}}(t_C - h_{KC})$.

For all $t_K: K \to T$ and $X, Y \in S$, the following claims hold:

(a) $S_{t_K} \neq 0_S$ if there is $t_C$ with $t_K = h_{KC} \star t_C$.

*Proof.* By definition of weighted type graph, for all $e \in \mathbb{E}$, we have

$$ w(e) \neq 0_S \qquad (1) $$
For every $t_C : C \to T$, we have

$$ w_{\mathcal{F}}(t_C - h_{KC}) = \bigoplus_{e \in \mathbb{E}} w_e(t_C - h_{KC}) \qquad \text{by Definition 12} $$

$$ = \bigoplus_{e \in \mathbb{E}} \bigoplus_{\substack{\alpha \in \{-*t_C=e\} \\ \alpha \notin \{1 \in \operatorname{Hom}(X,C) \mid \exists \zeta: X \to K, \zeta \star h_{KC}=1\}}} w(e) \qquad \text{by Definition 11} $$

$$ \neq 0_S \qquad \text{by (1), (S10) and Notation 2} $$

Therefore, $S_{t_K} \stackrel{\text{def}}{=} \bigoplus_{\substack{t_C:C \to T \\ t_K=h_{KC}*t_C}} w_{\mathcal{F}}(t_C - h_{KC}) \neq 0_S$ if there exists a morphism such that $t_K = h_{KC} \star t_C$ by (S12). $\square$

(b) $S_{t_K} \succeq 1_S$ if there is $t_C$ with $t_K = h_{KC} \star t_C$ and $w_{\mathcal{F}}(e) \succeq 1_S$ for all $e \in \mathbb{E}$,

*Proof.* By the definition of weighted type graph, for all $e \in \mathbb{E}$, we have $w(e) \neq 0_S$. By assumption, we have $w_{\mathcal{F}}(e) \succeq 1_S$ for all $e \in \mathbb{E}$. Thus, we have

$$ 1_S \preceq w(e) \neq 0_S \qquad (2) $$

By (S11), we have

$$ 1_S \preceq w_{\mathcal{F}}(t_C - h_{KC}) \qquad (3) $$

Therefore, $S_{t_K} \stackrel{\text{def}}{=} \bigoplus_{\substack{t_C:C \to T \\ t_K=h_{KC}*t_C}} w_{\mathcal{F}}(t_C - h_{KC}) \succeq 1_S$ if there exists a morphism such that $t_K = h_{KC} \star t_C$ by (S1). $\square$

(c) if there exists $t_C$ with $t_K = h_{KC} \star t_C$ then

$$ \mu(Y) > \mu(X) + \delta \implies \mu(Y \odot S_{t_K}) > \mu(X \odot S_{t_K}) $$

*Proof.* Suppose that there is $t_C$ with $t_K = h_{KC} \star t_C$. We have $S_{t_K} \neq 0_S$ by (a), and we conclude by (S7). $\square$

(d) if there exists $t_C$ with $t_K = h_{KC} \star t_C$, and $w_{\mathcal{F}}(e) \succeq 1_S$ for all $e \in \mathbb{E}$ then

$$ \mu(Y) > \mu(X) + \delta \implies \mu(Y \odot S_{t_K}) > \mu(X \odot S_{t_K}) + \delta $$

*Proof.* Suppose that there is $t_C$ with $t_K = h_{KC} \star t_C$. We have $1_S \preceq S_{t_K} \neq 0_S$ by (a) and (b), and we conclude by (S6). $\square$

(e) if there is no $t_C$ with $t_K = h_{KC} \star t_C$ then $S_{t_K} = 0_S$, thus

$$ Y \odot S_{t_K} = 0_S = X \odot S_{t_K} $$

(f) If there is a context closure $t_L$ for $\rho$ and $T$ in $\mathcal{F}$, then, let $t_K = l \star t_L$, we have

$$ \mu(Y) > \mu(X) + \delta \implies \mu(Y \odot S_{t_K}) > \mu(X \odot S_{t_K}) $$
*Proof.* By Definition 16 of context closure, there exists $t_G : G \to T$ such that

$$t_L = h_{LG} \star t_G \qquad (1)$$

i.e. we have the following commutative diagram

<figure><img src="image_22.png" /></figure>

Let $t_C \stackrel{\text{def}}{=} h_{CG} \star t_G$ and $t_K \stackrel{\text{def}}{=} l \star t_L$. We have

$t_K = l \star t_L$ by definition of $t_K$

$= l \star (h_{LG} \star t_G)$ by Equation 1

$= (l \star h_{LG}) \star t_G$ by associativity

$= (h_{KC} \star h_{CG}) \star t_G$ by commutative of $\square KLGC$

$= h_{KC} \star (h_{CG} \star t_G)$ by associativity

$= h_{KC} \star t_C$ by definition of $t_C$

and the claim follows from (c), since $t_C$ is a morphism such that $t_K = h_{KC} \star t_C$. $\square$

(g) If there is a context closure $t_L$ for $\rho$ and $T$ in $\mathcal{F}$, and $w_{\mathcal{F}}(e) \succeq 1_S$ for all $e \in \mathbb{E}$ then, let $t_K = l \star t_L$, we have

$$Y \succ X + \delta \implies Y \odot S_{t_K} \succ X \odot S_{t_K} + \delta$$

*Proof.* The proof is analogous to the proof of (f) but with (d) instead of (c) in the end. $\square$

For every $t_K : K \to T$, let

$$\Lambda_{t_K} \stackrel{\text{def}}{=} w_{\mathcal{F}}(\{l \star - = t_K\})$$

$$\Omega_{t_K} \stackrel{\text{def}}{=} w_{\mathcal{F}}(\{r \star - = t_K\})$$

By Lemma 2, we have

$$w_{\mathcal{F}}(G) = \bigoplus_{t_K:K \to T} (S_{t_K} \odot \Lambda_{t_K})$$

$$w_{\mathcal{F}}(H) \preceq \bigoplus_{t_K:K \to T} (S_{t_K} \odot \Omega_{t_K})$$

We complete the proof with a analysis by cases:

1. If $\rho$ is weakly decreasing, then, by Definition 17 of weakly decreasing rule, we have $\Lambda_{t_K} \ge \Omega_{t_K}$ for every $t_K : K \to T$. By (S4), for every $t_K : K \to T$, we have

$$S_{t_K} \odot \Lambda_{t_K} \succeq S_{t_K} \odot \Omega_{t_K} \qquad (\text{NE})$$

Thus, we have $w_{\mathcal{F}}(G) \succeq w_{\mathcal{F}}(H)$, from (S1).
2. Suppose that $\rho$ is $\delta$-uniformly decreasing for $\delta \in \mathbb{R}_{>0}$, and $w_{\mathcal{T}}(e) \ge 1$ for all $e \in \mathbb{E}$. By Definition 17 of $\delta$-uniformly decreasing rule, for all $t_K : K \to T$, we have

* $\mu(\Lambda_{t_K}) > \mu(\Omega_{t_K}) + \delta$, or

* $\{l^* - t_K\} = \emptyset = \{r^* - t_K\}$

From (d) and (e), for every $t_K : K \to T$, we obtain

(i) $S_{t_K} \odot \Lambda_{t_K} = 0_S = S_{t_K} \odot \Omega_{t_K}$, or

(ii) $\mu(\Lambda_{t_K} \odot S_{t_K}) > \mu(\Omega_{t_K} \odot S_{t_K}) + \delta$

To establish $\mu(w_{\mathcal{T}}(G)) > \mu(w_{\mathcal{T}}(H)) + \delta$, using (S3), it suffices to show that we have case (ii) for some $t_K : K \to T$. This follows from (g) since we have a context closure for $\rho$ and $\mathcal{T}$ by assumption.

3. If $\rho$ is $\delta$-closure decreasing, and $w_{\mathcal{T}}(e) \ge 1$ for all $e \in \mathbb{E}$ then it is also weakly decreasing and we obtain (NE) for every $t_K : K \to T$. Since the semiring is a strictly monotonic museurable semiring, by Equation S3 and (S9), it suffices to show that there exists some $t_K : K \to T$ such that

$$ \mu(S_{t_K} \odot \Lambda_{t_K}) > \mu(S_{t_K} \odot \Omega_{t_K}) + \delta \quad (\star\star) $$

in order to conclude $\mu(w_{\mathcal{T}}(G)) > \mu(w_{\mathcal{T}}(H)) + \delta$. There is a context closure $t_L$ for $\rho$ and $T$, and $\mu(\Lambda_{t_K}) > \mu(\Omega_{t_K}) + \delta$ for $t_K = l^*t_L$. Thus, we obtain (\star\star) by (g). $\square$

**Theorem 1** Let $\mathcal{A}$ and $\mathcal{B}$ be sets of DPO rewriting rules, $\mathcal{T} = (T, \mathbb{E}, (S, \oplus, \odot, 0_S, 1_S, \prec, \mu), w)$ a finitary weighted type graph and $\mathcal{F}$ a DPO rewriting framework such that

i) $w(e) \ge 1_S$ for all $e \in \mathbb{E}$,

ii) for all $x \in S$, if $1_S \preceq x \neq 0_S$ then $\mu(x) \ge \mu(1_S)$ and $\mu(x) \in \mathbb{R}$,

iii) for every rule $\rho \in (\mathcal{A} \cup \mathcal{B})$ and every double pushout diagram $\Delta \in \mathcal{F}(\rho)$

* left($\Delta$) is weighable with $\mathcal{T}$,

* right($\Delta$) is bounded above by $\mathcal{T}$.

If the following conditions hold:

1. there exists $\delta > 0$ such that either every $\rho \in \mathcal{A}$ is $\delta$-uniformly, or every $\rho \in \mathcal{A}$ is $\delta$-closure decreasing,

2. every rule $\rho \in \mathcal{B}$ is weakly decreasing,

then $\Rightarrow_{\mathcal{A}, \mathcal{F}}$ is **terminating** relative to $\Rightarrow_{\mathcal{B}, \mathcal{F}}$.

*Proof.* From the definition of weighted type graph, we have

for all $e \in \mathbb{E}, w(e) \neq 0_S$

From assumption (i)), we have

for all $e \in \mathbb{E}, 1_S \preceq w(e)$

Therefore, we have

$$ \text{for all } e \in \mathbb{E}, 1_S \preceq w(e) \neq 0_S \quad (4) $$
Let $G$ be a graph admitting a match of a DPO rewriting rule. We have

$$ w_{\mathcal{F}}(G) \stackrel{\text{def}}{=} \bigoplus_{h \in \text{Hom}(G,T)} w_{\mathcal{F}}(h) \\ \stackrel{\text{def}}{=} \bigoplus_{h \in \text{Hom}(G,T)} \left( \bigodot_{e \in \mathbb{E}} \left( \bigodot_{\alpha \in \{-\star h=e\}} w(e) \right) \right) $$

By Equation 4, Proposition 2, def:bigodot and $1_S \neq 0_S$, for every $h \in \text{Hom}(G, T)$, we have

$$ 1_S \preceq \bigodot_{e \in \mathbb{E}} \left( \bigodot_{\alpha \in \{-\star h=e\}} w(e) \right) \neq 0_S \qquad (5) $$

Since $G$ be a graph admitting a match of a DPO rewriting rule, by Proposition 2 and (S0), we have

$$ 1_S \preceq w_{\mathcal{F}}(G) \neq 0_S $$

By Assumption (ii)), we have

$$ \mu(w_{\mathcal{F}}(G)) \geq \mu(1_S) $$

By Lemma 1, every rewriting step with rules in $\mathcal{A}$ strictly decreases the weight by at least $\delta$ and no rewriting step with rules in $\mathcal{B}$ increases the weight. Consequently, there is no infinite rewriting sequence with an infinite rewriting steps with rules in $\mathcal{A}$ from $G$. $\square$ $\square$