Weighted Rewriting

Martin Avanzini¹ and Akihisa Yamada²

¹ Centre Inria d'Université Côte d'Azur, Sophia Antipolis, France
martin.avanzini@inria.fr

² AIST, Tokyo Waterfront, Japan
akihisa.yamada@aist.go.jp

**Abstract.** We introduce the notion of weighted abstract reduction systems (weighted ARSs), generalising standard and relative ARSs by allowing non-uniform weights on transition steps. Weighted ARSs give rise to a theory of rewriting where quantitative properties—noteworthy complexity related properties—can be more directly studied. Unlike these standard notions, weighted ARSs permit the study of quantitative properties of reduction systems of non-uniform weight, such as the analysis of expectation-based properties of probabilistic systems. We establish ranking functions as a means to analyse (strong) boundedness of weighted ARSs, i.e., the property that weights of reductions are bounded from above. We showcase their applicability by instantiating them to weighted term rewrite systems and probabilistic reduction systems, the latter generalising Lyapunov ranking functions to reason about expected derivation heights.

# 1 Introduction

Rewriting [7] provides a foundational theory of computing, with significant impact on both the theoretical aspects of computer science and the development of programming languages. Traditionally, rewriting primarily focuses on qualitative properties—such as whether a system is terminating or confluent. However, many applications in program analysis require a more fine-grained, *quantitative* perspective. Complexity analysis, cost-sensitive transformations, and resource-aware reasoning all demand a deeper understanding of the quantitative aspects of reduction processes. The study of such quantitative features is crucial for various quality assurance tasks, including guaranteed response time, smart contract deployment costs, resilience against side-channel attacks, security of cryptographic routines, and provable safety guarantees.

Abstract reduction systems (ARSs) provide a general model for a wide class of, possibly nondeterministic or probabilistic, systems. A key strength of ARSs is that they permit studying program properties independently of specific programming paradigms. Yet, they often fail to capture quantitative aspects effectively. A prototypical example is the complexity analysis of high-level, declarative languages, where a single reduction step is not an elementary operation. For instance, in the case of the λ-calculus, it is unrealistic to assume
that a single $\beta$-reduction step incurs a uniform cost. To endow the $\lambda$-calculus with a reasonable cost model—one that relates to Turing machines—Dal Lago and Martini [15] for instance propose to measure the cost of a step in terms of the absolute difference between the size of the reduct and redex. Some approaches to complexity analysis (e.g., [2, 8, 10]) allow the specification of a program’s resource consumption through annotations, the cost of a reduction step thereby becomes dependent on the annotation. A final example, where ARSs fail to model costs effectively, are stochastic, i.e., probabilistic systems.

The key observation of our work is that all these models can be effectively modeled by a *weighted* extension of ARSs, where reduction steps additionally carry *weight* information. Weights are taken from a general (ordered) monoid, whose structure is used to define reflexive and transitive closures, and thereby multi-step reductions. The monoid’s unit serves as the basis for reflexivity, while its binary operation is used for sequential composition. Weights are otherwise left abstract, and can thereby encompass a range of quantitative aspects.

- Using the ordered monoid $\langle \mathbb{N}, 0, +, \le \rangle$, weighted ARSs encompass rewriting under a *unitary cost measure*, where each reduction step is attributed a unit cost 1. The cost measure of Dal Lago and Martini [15] falls also within this setting, attributing cost $\max(1, |M| - |N|)$ to each $\beta$-step $M \to_{\beta} N$.

- Taking the ordered monoid $\langle \mathbb{N}, 0, \max, \le \rangle$, weighted ARSs endow computations with *"watermark"-like cost models*, such as (maximal) space usage.

- Products of monoids, with all operations extended pointwise, can be used to track simultaneously several cost metrics.

- Modelling stochastic reductions as an ARS over (multi)distributions [4], taking weights $\langle \mathbb{R}_{\ge 0}, 0, +, \le \rangle$ facilitates the study of *expected resource usage*.

- The monoid $\langle \mathbb{N}^{\text{Var}} \to \mathbb{N}, 0, + \rangle$, with all operations extended pointwise, can attribute non-ground rewrite steps with a *variable-size cost measure*.

Weighted ARSs provide a natural framework for studying quantitative aspects of computations directly. This encompasses quantitative variations of properties traditionally studied—such as strategies, confluence, and termination—taking for instance the length, or more generally cost, of reductions into account. In this work, we focus on termination-like properties, specifically *boundedness*, demanding that (cumulative) weights remain finite. We establish *ranking functions*, formalized as embeddings from weighted ARSs into a *canonical* weighted ARS over weights themselves, as a methodology for proving (strong) *boundedness*. Specifically, we show that this methodology is sound if the underlying monoid is *positive*, and is complete if the monoid is bounded-complete and continuous. Notably, all of the aforementioned instances fall within this setting.

A natural question then is how these abstract notions relate to concrete settings. First, we show that $\mathbb{N}$-weighted ARSs provide a conservative extension of classical and relative ARSs, serving as a sanity check of the proposed theory. We then introduce *weighted term rewrite systems (TRSs)* and *barycentric ARSs*. The former generalises first-order term rewrite systems, where each rule carries a weight. We show how monotone $\mathcal{F}$-algebras, a sound and complete method for proving termination of TRSs, generalize to a sound and complete method
for proving (strong) boundedness of weighted TRSs. Barycentric ARSs allow us to model probabilistic reductions in a way that weights correspond to expected runtimes or costs. We establish *affine ranking functions* as a mean to reason about boundedness of barycentric ARSs.

*Related Work.* Attaching weights to rules is a natural idea that appears in various contexts throughout the literature. One of the most well-studied examples is the theory of weighted automata (cf. [11]). In the context of term rewriting, a form of weighted (integer) TRSs was employed in [17] in order to keep track of the original runtime cost during simplifying the systems. The idea has also been applied to endow imperative [6], functional probabilistic [1], and quantum programs [5] with *non-uniform* cost models, non-uniform in the sense that computation costs of different primitives are not necessarily equal. Our weighted ARSs extract the common essence and serve as a foundation of these works.

A closely related, but fundamentally different idea to incorporate quantitative information is to *map* reduction steps to weights. For instance, in their study of hyper-normalisation, van Oostrom and Toyama [18] introduce *monoid-measured* ARSs, where steps are assigned weights from a monoid, yielding a derivation measure that abstracts over reduction length. Gavazzo and Florio [14] define *quantitative ARSs*, where steps are mapped to elements of a *quantale*—a monoid endowed with a semilattice structure that satisfies certain distributivity laws. Their construction induces a notion of *distance* between terms in the ARS, conforming to the standard axioms of a metric space. In a similar fashion, weighted transition systems [19] generalize weighted automata with additional structures for metrical analysis. Laird et al. [16] endow a non-deterministic version of Plotkin's PCF with a quantitative semantics, where the denotation of a (non-deterministic) function is turned from a relation between inputs and outputs, to a function assigning weights to input/output pairs.

The fundamental difference of our work lies in the structure of the rewriting relation: rather than augmenting ARSs ($R \subseteq A \times A$) with mappings $A \times A \to W$, we extend ARSs to a ternary relation ($R \subseteq W \times A \times A$). As a result, our framework imposes no intrinsic constraints on the nature of weights—for instance, they need not represent distances or abstract measures of derivation length.

Finally, Faggian [12] introduces another orthogonal formalism, also dubbed *quantitative ARSs* (QARSs), particularly aimed for the study of quantitative behaviors of probabilistically evolving systems. QARSs assign quantities—the *observations*—to states ($A \to W$). This way, fundamental properties of QARSs can be studied through the sequence of observations. QARSs are mainly used to study so called *asymptotic* behaviors of infinite reduction sequences, e.g., uniqueness of “limits” of reductions.

*Outline.* In Section 2, we introduce weighted ARSs and their fundamental properties. In Section 3 we establish ranking functions as a means to reason about bound on the weight an initial state can produce. In Section 4 we present the aforementioned instances of weighted ARSs: standard ARSs, weighted TRSs, and barycentric ARSs, and conclude in Section 5.
## 2 Weighted Abstract Rewriting

In this section we formally introduce weighted ARSs—a generalization of ARSs where transitions between states have (possibly different) weights. To model the concatenation of multiple weighted reduction steps, we will assume that weights have a monoidal structure. This enables us to model reflexivity and transitivity in the weighted setting. We will also demand that weights are (partially) ordered, so that we can argue about bounds on weights.

We quickly recap some basic notions. A partially ordered set (poset) is a set $\mathcal{W}$ equipped with a partial order $\leq$ on $\mathcal{W}$. We say a subset $X \subseteq \mathcal{W}$ of a poset has an (upper) bound $b \in \mathcal{W}$ (written $X \leq b$), if $x \leq b$ for all $x \in X$. We say $\mathcal{W}$ is bounded-complete if every $X \subseteq \mathcal{W}$ that has an upper bound in $\mathcal{W}$ has the least one, sup $X$. A monoid is a set $\mathcal{W}$ equipped with an associative operator $+$ defined on $\mathcal{W}$ and its neutral element $0 \in \mathcal{W}$, i.e., $(x + y) + z = x + (y + z)$ and $0 + x = x + 0 = x$ for all $x, y, z \in \mathcal{W}$. A monoid $\mathcal{W}$ is ordered if it is also a poset where $x \leq y$ implies $x + z \leq y + z$ and $z + x \leq z + y$ for all $x, y, z \in \mathcal{W}$. An ordered monoid $\mathcal{W}$ is positive if $0 \leq w$ for all $w \in \mathcal{W}$. We say $\mathcal{W}$ is continuous if whenever sup $X \in \mathcal{W}$ is defined, sup $\{x + w \mid x \in X\}$ is defined and is sup $X + w$.

**Example 1.** The sets $\mathbb{N}$ and $\mathbb{R}_{\geq 0}$ of natural and non-negative real numbers form bounded-complete positive monoids with $0, +$, and $\leq$ as usual. For any nonempty $X$, the function space $X \to \mathcal{W}$ over a bounded-complete positive monoid $\mathcal{W}$ forms one with respect to the pointwise extensions, i.e., $0(x) := 0$, $(f + g)(x) := f(x) + g(x)$, and $f \leq g \iff \forall x \in X$. $f(x) \leq g(x)$.

**Definition 1 (weighted ARS).** A $\mathcal{W}$-weighted ARS over state space $A$ and positive monoid $\mathcal{W}$ is a ternary relation<fnref n="3" /> $\rightsquigarrow \subseteq \mathcal{W} \times A \times A$. We write $\rightsquigarrow^{[w]}$ for $\{\langle a, b \rangle \mid \langle w, a, b \rangle \in \rightsquigarrow\}$, and hence $a \rightsquigarrow^{[w]} b$ means $\langle w, a, b \rangle \in \rightsquigarrow$. We say $\rightsquigarrow$ is a weighted order if it is

- reflexive: $a \rightsquigarrow^{[0]} a$ for all $a \in A$; and

- transitive: $a \rightsquigarrow^{[w]} b$ and $b \rightsquigarrow^{[v]} c$ implies $a \rightsquigarrow^{[w+v]} c$ for all $a, b, c \in A$.

We denote by $\rightsquigarrow$ the least weighted order containing $\rightsquigarrow$, and write $\rightsquigarrow^w$ for $\rightsquigarrow^{[w]}$. When we know that $\rightsquigarrow$ is transitive, we may write $\rightsquigarrow^w$ instead of $\rightsquigarrow^{[w]}$. Alternatively, the ARS $\rightsquigarrow^w$ can be defined by the following inference rules:

$$ \frac{a \rightsquigarrow^0 a}{a \rightsquigarrow^w a} \qquad \frac{a \rightsquigarrow^{[w]} b}{a \rightsquigarrow^w b} \qquad \frac{a \rightsquigarrow^w b \quad b \rightsquigarrow^v c}{a \rightsquigarrow^{w+v} c} $$

**Definition 2 (closures and normal forms).** Given a weighted ARS $\rightsquigarrow \subseteq \mathcal{W} \times A \times A$, we define transitive weighted ARSs $\rightsquigarrow \geq$ and $\rightsquigarrow >$ as follows:

$$ a \rightsquigarrow^{\geq w} b \iff \exists v \geq w. a \rightsquigarrow^v b \qquad a \rightsquigarrow^{> w} b \iff \exists v > w. a \rightsquigarrow^v b $$

<footnote n="3">³ In the literature a weighted relation is often given as $A \times \mathcal{W} \times A$. In our context, $\mathcal{W} \times A \times A$ turns out notationally more convenient.</footnote>
<figure><img src="image_1.png" /><figcaption>Fig. 1: Hasse diagrams illustrating the impact of non-Zeno and finite branching restrictions on the relationships among the properties from Definition 4. Here TRSs are supposed to be finite.</figcaption></figure>

We call $\rightsquigarrow \ge$ the downward closure as $w \ge v$ implies $\rightsquigarrow \ge w \subseteq \rightsquigarrow \ge v$. By convention, we write $\rightsquigarrow * \subseteq A \times A$ for $\rightsquigarrow \ge 0$ and $\rightsquigarrow +$ for $\rightsquigarrow > 0$. We say $a \in A$ is a normal form (or terminal) with respect to $\rightsquigarrow$ if no such $b \in A$ exists that $a \rightsquigarrow + b$. The set of normal forms with respect to $\rightsquigarrow$ is denoted by $\mathbf{NF}(\rightsquigarrow)$.

**Definition 3 (weighted reduction sequence).** A reduction sequence w.r.t. a weighted ARS $\rightsquigarrow$ is a (possibly infinite) sequence $a_0 \rightsquigarrow [w_1] a_1 \rightsquigarrow [w_2] a_2 \rightsquigarrow [w_3] \dots$. The sequence is called

- terminating, if there exists $n \in \mathbb{N}$ such that $w_n = w_{n+1} = \dots = 0$;

- bounded (by $b \in W$), if $w_1 + \dots + w_n \le b$ for any $n = 1, 2, \dots$;

- Zeno, if it is bounded but not terminating.

**Example 2.** Consider the $\mathbb{R}_{\ge 0}$-weighted ARS $\rightsquigarrow := \{\langle \frac{1}{2^n}, n, n+1 \rangle \mid n \in \mathbb{N}\} \cup \{\langle 0, n, n \rangle \mid n \in \mathbb{N}\}$ over states $\mathbb{N}$. Reduction sequences such as $0 \rightsquigarrow [1] 1 \rightsquigarrow [1/2]$ $2 \rightsquigarrow [0] 2 \rightsquigarrow [0] \dots$ are terminating, as after the third step only weight-0 steps occur. The sequence $0 \rightsquigarrow [1] 1 \rightsquigarrow [1/2] 2 \rightsquigarrow [1/4] 3 \rightsquigarrow [1/8] \dots$ is not terminating as $\frac{1}{2^n} \ne 0$ for any $n \in \mathbb{N}$, but is bounded by $1 + \frac{1}{2} + \frac{1}{4} + \frac{1}{8} + \dots = 2$; i.e., Zeno.

We now define the properties of weighted ARSs that are of interest in this work. The first two properties generalize the corresponding notions of standard ARSs, and the next two generalize the positive and strong almost-sure termination of probabilistic ARSs [4, 9], respectively; the latter was (independently) called "bounded termination" by [13], which inspired the naming below.

**Definition 4 (properties of weighted ARSs).** A weighted ARS $\rightsquigarrow$ over $A$ is

1. $\text{WN}_{\rightsquigarrow}(S)$: (weakly) normalizing on $S \subseteq A$ if every $a \in S$ has $b \in \mathbf{NF}(\rightsquigarrow)$ such that $a \rightsquigarrow * b$;

2. $\text{SN}_{\rightsquigarrow}(S)$: terminating on $S \subseteq A$ if any reduction sequence from any $a \in S$ is terminating;
<figure><img src="image_2.png" /><figcaption>Fig. 2: Examples demonstrating the strictness of the implications in Proposition 1.</figcaption></figure>

3. $\text{WB}_{\sim}(S)$: weakly bounded on $S \subseteq A$ if any reduction sequence from any $a \in S$ is bounded;

4. $\text{SB}_{\sim}(S)$: strongly bounded on $S \subseteq A$ if every $a \in S$ has $p \in W$ such that any reduction sequence from $a$ is bounded by $p$;

5. strongly finitely branching if for every $a \in A$, both $\{\langle w, b \rangle \mid a \rightsquigarrow^{[w]} b\}$ and $\{b \mid a \rightsquigarrow^0 b\}$ are finite;

6. non-Zeno if it admits no Zeno sequence.

Fig. 1 depicts the relationships between these properties, formally proven in Proposition 1 below. The various Hasse diagrams illustrate the following cases: (a) without restrictions; (b) non-Zeno systems; (c) strongly finitely branching systems; and (d) systems that are both strongly finitely branching and non-Zeno. These subclasses are of particular interest, as each corresponds to a distinct class of reduction systems, studied within this work.

**Proposition 1.** Let $\rightsquigarrow \subseteq W \times A \times A$ be a weighted ARS and let $S \subseteq A$. Then

1. $\text{SN}_{\sim}(S) \Rightarrow \text{WN}_{\sim}(S)$;

2. $\text{SB}_{\sim}(S) \Rightarrow \text{WB}_{\sim}(S)$;

3. $\text{SN}_{\sim}(S) \Rightarrow \text{WB}_{\sim}(S)$;

4. $\text{SN}_{\sim}(S) \Longleftrightarrow \text{WB}_{\sim}(S)$ if $\rightsquigarrow$ is non-Zeno;

5. $\text{SN}_{\sim}(S) \Rightarrow \text{SB}_{\sim}(S)$ if $\rightsquigarrow$ is strongly finitely branching;

*Proof.* We only present interesting ones: 3 and 5. For 3, consider $a_0 \rightsquigarrow^{[w_1]} a_1 \rightsquigarrow^{[w_2]} a_2 \rightsquigarrow^{[w_3]} \dots$. By assumption $w_n = w_{n+1} = \dots = 0$ for some $n \in \mathbb{N}$. Defining $p := w_1 + \dots + w_{n-1}$ proves that the considered sequence is bounded.

For 5, suppose that $\text{SN}_{\sim}(S)$ and $\rightsquigarrow$ is strongly finitely branching. For an arbitrary $a \in S$, we prove the set $X := \{w \mid \exists b. a \rightsquigarrow^w b\}$ is bounded. Note that there is a surjection onto $X$ from the paths of the graph over $A$ where for each $w > 0$ with $a \rightsquigarrow^{[w]} \cdot \rightsquigarrow^0 b$ there is a corresponding arc from $a$ to $b$. As this graph is finitely branching, König's Lemma tells that if there are infinitely many paths, then there exists an infinite path $a \rightsquigarrow^0 \cdot \rightsquigarrow^{[w_1]} a_1 \rightsquigarrow^0 \cdot \rightsquigarrow^{[w_2]} \dots$ with $w_i > 0$. Such reduction does not exist, due to the termination condition. Therefore $X$ is finite, and thus $\sum_{w \in X} w$ is an upper bound of $X$ due to positiveness. $\square$

The implications in Proposition 1 are strict, as illustrated by examples in Fig. 2. As for classical ARSs, weak normalisation does not imply strong normalisation
(Fig. 2(a)). The Zeno weighted ARS from Fig. 2(b) shows that in general boundedness does not imply normalisation. The non-Zeno, infinitely branching weighted ARS from Fig. 2(c) shows that weak boundedness and normalisation does not imply strong boundedness. Fig. 2(d) is another counterexample of the claim, which is finitely branching as a graph but fails the finiteness of zero-weighted reductions required in Definition 4(5).

## 3 Bound Analysis via Ranking Functions

Ranking functions are the prototypical way to prove termination, and also play a fundamental role in complexity analysis. For discrete programs over a state space A with transition relation $\mapsto \subseteq A \times A$, a ranking function is a function $\eta: A \to \mathbb{N} \cup \{\infty\}$ which is finite on initial states and decreases along state transitions: $a \mapsto b$ implies $\eta(a) > \eta(b)$ (i.e., $\eta$ embeds $\mapsto$ into $>$). In this section, we adapt ranking functions to weighted ARSs, formalised as embeddings between weighted ARSs.

**Definition 5 (embedding).** Let $\rightsquigarrow \subseteq W \times A \times A$ and $> \subseteq W \times X \times X$ be weighted ARSs. We say a mapping $\eta: A \to X$ is an embedding of $\rightsquigarrow$ into $>$ if $a \rightsquigarrow^{[w]} b$ implies $\eta(a) >^{[w]} \eta(b)$.

An embedding is required to strictly preserve the weight of reduction steps. It is possible to relax the condition so that a step of weight $w$ is embedded into a step of weight at least $w$; however, the same effect is achievable by embedding into the downward-closed weighted ARS $> \geq w$.

An embedding witnesses that every $\rightsquigarrow$-reduction sequence can be associated with a corresponding $>$-reduction sequence of identical weight. Indeed, for any state $a \in A$, the maximal weight of $\rightsquigarrow$-reduction sequences is controlled in terms of $\eta(a)$ and $>$. To state the relationship precisely, we introduce the notion of potential: a function in the state space capturing possible reduction weights.

**Definition 6 (potential).** Let $\rightsquigarrow \subseteq W \times A \times A$ be a weighted ARS. We define the potential of $a \in A$ as the set $\text{Pot}_{\rightsquigarrow}(a) := \{w \mid \exists b. a \rightsquigarrow^w b\} \subseteq W$. We write $\text{pot}_{\rightsquigarrow}(a)$ for $\sup \text{Pot}_{\rightsquigarrow}(a)$.

Note that $a$ is a normal form of $\rightsquigarrow$ if its (only) potential is 0. Proving strong boundedness is equivalent to proving boundedness on potentials, by definition.

**Proposition 2.** $\text{SB}_{\rightsquigarrow}(S)$ iff for every $a \in S$, $\text{Pot}_{\rightsquigarrow}(a)$ has a bound $b \in W$.

**Theorem 1 (embedding, soundness).** Let $\eta: A \to X$ be an embedding of $\rightsquigarrow \subseteq W \times A \times A$ into $> \subseteq W \times X \times X$. Then $\text{Pot}_{\rightsquigarrow}(a) \subseteq \text{Pot}_{>}^>(\eta(a))$ for every $a \in A$. In particular, for $S \subseteq A$, $\text{SB}_{>}^>(\eta(S))$ implies $\text{SB}_{\rightsquigarrow}(S)$.

*Proof.* Fix $a \in A$ and $w \in \text{Pot}_{\rightsquigarrow}(a)$, i.e., $a \rightsquigarrow^w b$ for some $b \in A$. Thus, there is a sequence

$$a = a_0 \rightsquigarrow^{[w_1]} a_1 \rightsquigarrow^{[w_2]} \dots \rightsquigarrow^{[w_n]} a_n = b$$
such that $w = w_1 + \cdots + w_n$. By Definition 5,

$$ \eta(a) = \eta(a_0) \succ^{[w_1]} \eta(a_1) \succ^{[w_2]} \cdots \succ^{[w_n]} \eta(a_n) = \eta(b) $$

i.e., $\eta(a) \succ_w \eta(b)$ and hence $w \in \mathrm{Pot}_\succ(\eta(a))$. This concludes $\mathrm{Pot}_\succ(a) \subseteq \mathrm{Pot}_\succ(\eta(a))$. Moreover, if $\mathrm{Pot}_\succ(\eta(a))$ has a bound $b \in W$ then so does $\mathrm{Pot}_\succ(a)$, trivially. Hence, $\mathrm{SB}_\succ(\eta(S))$ implies $\mathrm{SB}_\succ(S)$ by Proposition 2. $\square$

Ranking functions can now be seen as embeddings into a canonical order $\succ_W$ defined as follows. Note that $\succ_W$ is downward-closed by construction.

**Definition 7 (ranking function).** Let $\infty \notin W$ be a fresh top element. We denote by $W^\infty$ the ordered monoid extending $W$, where $w < \infty$ and $w + \infty := \infty$ for all $w \in W$. We define the weighted order $\succ_W \subseteq W \times W^\infty \times W^\infty$ by $x \succ_W^+[w] y \iff x \ge w + y$. We call an embedding $\eta: A \to W^\infty$ of a weighted ARS $\rightsquigarrow \subseteq W \times A \times A$ into $\succ_W a$ (W-valued) ranking function for $\rightsquigarrow$.

**Lemma 1.** For a positive monoid $W$, $\mathrm{SB}_{\succ_W}(W)$ and $\mathrm{pot}_{\succ_W}(x) = x$.

*Proof.* Fix $x \in W$. Note that $\mathrm{Pot}_{\succ_W}(x) = \{w \in W \mid \exists y \in W^\infty, x \ge w + y\}$. Because of positiveness, $x \ge w + y$ implies $w \le x$ and thus $x$ is a bound of $\mathrm{Pot}_{\succ_W}(x)$. Since $x = x+0 \in \mathrm{Pot}_{\succ_W}(x)$, $x$ is the maximum and thus supremum of $\mathrm{Pot}_{\succ_W}(x)$, i.e., $\mathrm{pot}_{\succ_W}(x) = \sup \mathrm{Pot}_{\succ_W}(x) = x$. $\square$

The following is an immediate consequence of Theorem 1 and Lemma 1:

**Corollary 1 (ranking functions, soundness).** If a weighted ARS $\rightsquigarrow \subseteq W \times A \times A$ admits a ranking function $\eta: A \to W^\infty$ with $\eta(S) \subseteq W$ for $S \subseteq A$, then $\mathrm{SB}_\succ(S)$. In particular, $\mathrm{pot}_\succ(a) \le \eta(a)$ for every $a \in S$.

Completeness also holds, at least if the weights constitute a bounded-complete continuous monoid. Since $\mathbb{N}$ and $\mathbb{R}_{\ge 0}$ with usual 0, $+$ and $\le$ are such instances, $\mathbb{N}$-valued ($\mathbb{R}_{\ge 0}$-valued) ranking functions yield both a sound and complete methodology for proving strong boundedness. We leave it for a future work to find a milder condition preserving completeness.

**Theorem 2 (ranking functions, completeness).** If $W$ is a bounded-complete continuous monoid and a weighted ARS $\rightsquigarrow \subseteq W \times A \times A$ is strongly bounded on $S$, then $\rightsquigarrow$ admits a ranking function $\eta: A \to W^\infty$ with $\eta(S) \subseteq W$.

*Proof.* Observe that $\sup X \in W^\infty$ is defined for any $X \subseteq W$: if $X$ has a bound in $W$ then $\sup X \in W$ due to bounded-completeness, and $\sup X = \infty$ otherwise. Therefore, $\mathrm{pot}_\succ: A \to W^\infty$ is defined.

Now we show that $\mathrm{pot}$ is an embedding of $\rightsquigarrow$ into $\succ_W$. So we prove that $a \rightsquigarrow [w] b$ implies $\mathrm{pot}_\succ(a) \succ_W^+[w] \mathrm{pot}_\succ(b)$. If $\mathrm{pot}_\succ(a) = \infty$ the claim is trivial. Otherwise, using $a \rightsquigarrow [w] b$, observe that

$$ \mathrm{Pot}_\succ(a) = \{v \mid \exists c. a \rightsquigarrow^v c\} \supseteq \{w + u \mid \exists c. b \rightsquigarrow^u c\} =: X. $$
Since $\mathbf{pot}_{\rightsquigarrow}(a) \in \mathcal{W}$ is a bound of $\mathbf{Pot}(a)$, it is also a bound of $X$; thus, $\sup X \in \mathcal{W}$ is defined due to bounded-completeness. Now due to continuity

$$ \mathbf{pot}_{\rightsquigarrow}(a) \geq \sup X = w + \sup \{u \mid b \rightsquigarrow^u c\} = w + \mathbf{pot}_{\rightsquigarrow}(b), $$

i.e., indeed $\mathbf{pot}_{\rightsquigarrow}(a) >_{W}^{[w]} \mathbf{pot}_{\rightsquigarrow}(b)$ holds. Finally, since $\mathbf{SB}_{\rightsquigarrow}(S)$ means that $\mathbf{Pot}_{\rightsquigarrow}(a)$ has a bound in $\mathcal{W}$ for every $a \in S$, bounded-completeness gives $\mathbf{pot}_{\rightsquigarrow}(a) \in \mathcal{W}$. This concludes $\mathbf{pot}_{\rightsquigarrow}(S) \subseteq \mathcal{W}$. $\square$

# 4 Instances

Having defined weighted ARSs and a method to prove strong boundedness, the aim of this section is to demonstrate their versatility. We begin by formally stating the connection between (unitary) weighted ARSs and ARSs, ensuring that the notions we introduced align with standard concepts in abstract rewriting. Next, we generalize term rewrite systems (TRSs) to weighted TRSs, where rules carry weights, and show how the interpretation method can be used to prove strong boundedness. Finally, we introduce barycentric ARSs. One particular class of barycentric ARSs is given by probabilistic ARSs, with weights modelling expected runtime. Through ranking functions, we obtain a methodology for proving probabilistic termination properties.

## 4.1 Abstract Reduction System

We may identify an ARS $\mapsto \subseteq A \times A$ as the $\mathbb{N}$-weighted ARS $\{1\} \times \mapsto = \{\langle 1, a, b \rangle \mid a \mapsto b\}$. This is justified by the following correspondences. As usual, $\mapsto^n$, $\mapsto^+$, $\mapsto^*$, and $\mathbf{NF}(\mapsto)$ denote the standard $n$-th fold, transitive closure, reflexive-transitive closure, and the set normal forms of $\mapsto$, respectively. The *derivation height* $\mathbf{dh}_{\mapsto}(a) \in \mathbb{N}^{\infty}$ of $a \in A$ with respect to $\mapsto$ is defined by $\mathbf{dh}_{\mapsto}(a) := \sup\{n \in \mathbb{N} \mid \exists b. a \mapsto^n b\}$.

**Proposition 3.** For any (unweighted) ARS $\mapsto \subseteq A \times A$:

$$ - (\{1\} \times \mapsto)^\alpha = \mapsto^\alpha \text{ where } \alpha \in \mathbb{N} \cup \{*, +\}, $$

$$ - \mathbf{NF}(\{1\} \times \mapsto) = \mathbf{NF}(\mapsto), \text{ and } \mathbf{pot}_{\{1\} \times \mapsto}(s) = \mathbf{dh}_{\mapsto}(s). $$

Clearly the $\mathbb{N}$-weighted ARS $\{1\} \times \mapsto$ is non-Zeno, so termination coincides with weak boundedness due to Proposition 1 (see also Fig. 1 (b)). If $\mapsto$ is finitely branching, then $\{1\} \times \mapsto$ is strongly finitely branching, and termination coincides with weak and strong boundedness (see Fig. 1 (d)).

The correspondence extends to relative reduction. The reduction of an ARS $\mapsto$ relative to another ARS $\sim$ is modeled by the ARS $\mapsto/\sim := \sim^* \circ \mapsto \circ \sim^*$. Attributing $\mapsto$ weight one and $\sim$ weight zero allows us to model relative reduction through $\mathbb{N}$-weighted ARS $\mapsto//\sim := (\{1\} \times \mapsto) \cup (\{0\} \times \sim)$.

**Proposition 4.** For any ARSs $\mapsto$, $\sim \subseteq A \times A$:

$$ - (\mapsto//\sim)^0 = \sim^* \text{ and } (\mapsto//\sim)^n = (\mapsto/\sim)^n \text{ where } n = 1, 2, \dots, $$
$$- (\mapsto/\sim)^* = (\mapsto \cup \sim)^* = \sim^* \cup (\mapsto/\sim)^*,$$

$$- (\mapsto/\sim)^+ = (\mapsto/\sim)^+,$$

$$- \mathrm{NF}(\mapsto/\sim) = \mathrm{NF}(\mapsto/\sim), \text{ and } \mathrm{pot}_{\mapsto/\sim}(s) = \mathrm{dh}_{\mapsto/\sim}(s).$$

## 4.2 Term Rewrite Systems

We now introduce weighted versions of term rewrite systems (TRSs), i.e., TRSs where each rule carries a weight. Usual TRSs correspond to $\{1\} \times \mathcal{R}$. The reduction relation attributed to a weighted TRS will be given as a weighted ARS over terms. We define monotone algebras (i.e., the interpretation method) as a sound and complete methodology for proving strong boundedness.

We quickly recap notations. For a signature $\mathcal{F}$ and variables $\mathcal{V}$, let us denote by $\mathcal{T}(\mathcal{F}, \mathcal{V})$ the set of terms. Terms are denoted by $s, t, l, r$ below. For a substitution $\sigma$, we write $t\sigma$ for its application to a term $t$. For a context $C$, i.e., term with one special symbol $\square$, we denote by $C[t]$ the term obtained by replacing $\square$ in $C$ by $t$. With $\mathrm{Var}(t)$ we denote the set of variables in $t$.

**Definition 8 (weighted TRS).** A $\mathcal{W}$-weighted rule is a triple $(w, l, r) \in \mathcal{W} \times \mathcal{T}(\mathcal{F}, \mathcal{V}) \times \mathcal{T}(\mathcal{F}, \mathcal{V})$, where variable conditions $l \notin \mathcal{V}$ and $\mathrm{Var}(r) \subseteq \mathrm{Var}(l)$ hold. A $\mathcal{W}$-weighted TRS is a set $\mathcal{R}$ of weighted rules.

**Definition 9 (weighted rewrite relation).** A $\mathcal{W}$-weighted rewrite relation is a $\mathcal{W}$-weighted ARS $\rightsquigarrow$ that is closed under substitutions and contexts; i.e., $C[l\sigma] \rightsquigarrow^{[w]} C[r\sigma]$ for every context $C$ and substitution $\sigma$ whenever $l \rightsquigarrow^{[w]} r$.

We define the weighted ARS $\rightsquigarrow_{\mathcal{R}}$ over $\mathcal{T}(\mathcal{F}, \mathcal{V})$ as the least weighted rewrite relation containing $\mathcal{R}$; more concretely $C[l\sigma] \rightsquigarrow_{\mathcal{R}}^{[w]} C[r\sigma]$ for every weighted rule $(w, l, r) \in \mathcal{R}$, context $C$ and substitution $\sigma$. It is well known that a TRS is terminating if and only if it is included in a well-founded rewrite relation. A similar correspondence holds for weighted TRSs:

**Theorem 3.** Let $\mathcal{R}$ be a $\mathcal{W}$-weighted TRS. The rewrite relation $\rightsquigarrow_{\mathcal{R}}$ is strongly bounded if and only if $\mathcal{R} \subseteq \succ$ for a strongly bounded weighted rewrite relation $\succ$.

*Proof.* For the “if” direction, suppose $\succ$ is a strongly bounded rewrite relation containing $\mathcal{R}$. Suppose $C[l\sigma] \rightsquigarrow_{\mathcal{R}}^{[w]} C[r\sigma]$ with $(w, l, r) \in \mathcal{R}$. Since $\mathcal{R} \subseteq \succ$, we have $l \succ^{[w]} r$, as $\succ$ is a rewrite relation it follows that $C[l\sigma] \succ^{[w]} C[r\sigma]$. Consequently, the identity function embeds $\rightsquigarrow_{\mathcal{R}}$ into $\succ$. From this, it follows that $\rightsquigarrow_{\mathcal{R}}$ is strongly bounded by Theorem 1. The “only if” direction follows by taking $\rightsquigarrow_{\mathcal{R}}$ for $\succ$. $\square$

The interpretation method, which interprets terms through an algebra into a well-founded order $\succ$, is among the most fundamental methods for proving termination of standard TRSs. This method naturally adapts to weighted TRSs for proving strong boundedness: An $\mathcal{F}$-algebra is a set $\mathcal{A}$ equipped with the interpretation $f_{\mathcal{A}}: \mathcal{A}^n \to \mathcal{A}$ of every $n$-ary symbol $f \in \mathcal{F}$. The interpretation $[s]_{\mathcal{A}}^{\alpha}$ of terms $s \in \mathcal{T}(\mathcal{F}, \mathcal{V})$ under assignment $\alpha: \mathcal{V} \to \mathcal{A}$ is defined as usual.
**Definition 10 (weighted monotone $\mathcal{F}$-algebra).** A ($\mathcal{W}$-weighted) monotone $\mathcal{F}$-algebra $\langle \mathcal{A}, \succcurlyeq \rangle$ consists of an $\mathcal{F}$-algebra $\mathcal{A}$ and a weighted ARS $\succcurlyeq \subseteq \mathcal{W} \times \mathcal{A} \times \mathcal{A}$, such that every interpretation is monotone with respect to $\succcurlyeq$, that is, $x \succcurlyeq^{[w]} y$ implies $f_{\mathcal{A}}(\dots, x, \dots) \succcurlyeq^{[w]} f_{\mathcal{A}}(\dots, y, \dots)$ for every $f \in \mathcal{F}$.

Given a monotone $\mathcal{F}$-algebra $\langle \mathcal{A}, \succcurlyeq \rangle$ we define the weighted ARS $\succcurlyeq_{\mathcal{A}}$ over terms by $s \succcurlyeq_{\mathcal{A}}^{[w]} t$ iff $[[s]]_{\mathcal{A}}^{\alpha} \succcurlyeq^{[w]} [[t]]_{\mathcal{A}}^{\alpha}$ holds for every assignment $\alpha : \mathcal{V} \to X$.

**Lemma 2.** For a monotone $\mathcal{F}$-algebra $\langle \mathcal{A}, \succcurlyeq \rangle$, $\succcurlyeq_{\mathcal{A}}$ is a weighted rewrite relation.

*Proof.* Reasoning inductively, $[[s\theta]]_{\mathcal{A}}^{\alpha} = [[s]]_{\mathcal{A}}^{[\theta]}{}^{\alpha}$, where $[[\cdot]]_{\mathcal{A}}^{\alpha}$ is extended homomorphically to the substitution $\theta$. Closure under substitutions now follows from definition of $\succcurlyeq_{\mathcal{A}}$, closure under contexts by monotonicity. $\square$

Let us call an $\mathcal{F}$-algebra $\langle \mathcal{A}, \succcurlyeq \rangle$ strongly bounded if $\succcurlyeq$ is.

**Theorem 4.** A weighted TRS $\mathcal{R}$ is strongly bounded if and only if $\mathcal{R} \subseteq \succcurlyeq_{\mathcal{A}}$ for a strongly bounded monotone $\mathcal{F}$-algebra $\langle \mathcal{A}, \succcurlyeq \rangle$.

*Proof.* The “if”-direction follows by Theorem 3 and Lemma 2. The “only if” direction holds taking for $\langle \mathcal{A}, \succcurlyeq \rangle$ the $\mathcal{W}$-weighted $\mathcal{F}$-algebra $\langle \mathcal{T}, \rightsquigarrow_{\mathcal{R}} \rangle$, where $\mathcal{T}$ is the term algebra. Trivially, $\mathcal{R} \subseteq \rightsquigarrow_{\mathcal{R}} = (\rightsquigarrow_{\mathcal{R}})^{\mathcal{T}}$ and $\rightsquigarrow_{\mathcal{R}}$ is monotone. $\square$

One prototypical instance for the order $\succcurlyeq$ is the canonical weighted ARS $\succcurlyeq_{\mathbb{N}}$; this way, interpretations over naturals can be seen as a way to inductively define ranking functions on TRSs. Another noticeable instance is $\succcurlyeq_{\mathbb{R}_{\ge 0}}$; using such real-valued interpretations one can prove strong boundeness, which is equivalent to termination as long as the set of rewrite rules is finite (compare Fig. 1 (d)).

## 4.3 Barycentric ARSs

Probabilistic ARSs were introduced by Bournez and Garnier [9] as a means to study reduction systems with probabilistic behavior. In essence, probabilistic ARS (over objects $\mathcal{A}$) allow sampling of reducts from a (probability) distribution, a function $d : \mathcal{A} \to [0, 1]$ with $\sum_{a \in \mathcal{A}} d(a) = 1$, assigning to each $a \in \mathcal{A}$ a probability $d(a)$. Rules in probabilistic ARSs take the form $a \to d$; the intended meaning of such a rule is that $a$ reduces to $b$ with probability $d(b)$. When a policy that resolves non-deterministic choices is fixed, reduction sequences can be defined in terms of stochastic processes. Equivalently, reduction can be defined directly through an ARS over multidistributions [3,4], a structure that generalises probability distributions and multisets, encapsulating the probabilistic and non-deterministic effects, respectively. We will generalize probabilistic ARSs into a class of weighted ARSs called barycentric ARSs. Before, we recap notions, following the presentation of [4].

We denote the set of distributions on $\mathcal{A}$ by $\mathcal{D}(\mathcal{A})$. The convex combinations of distributions are defined by $(\sum_{i \in \mathcal{I}} p_i \cdot d_i)(a) := \sum_{i \in \mathcal{I}} p_i \cdot d_i(a)$ for $\sum_{i \in \mathcal{I}} p_i = 1$. We may view distributions as sets of pairs of $a \in \mathcal{A}$ and $p > 0$ written $p : a$, i.e., $d = \{d(a) : a \mid a \in \mathcal{A}, d(a) > 0\}$. A (sub-)multidistribution on $\mathcal{A}$ is a multiset $\mu$
of such pairs $p : a$, satisfying $|\mu| := \sum_{(p:a) \in \mu} p = 1$ ($\le 1$). We denote the set of (sub-)multidistributions on $A$ by $\mathcal{M}(A)$ ($\mathcal{M}^{\le 1}(A)$). The (sub-)convex combination of multidistributions $\langle \mu_i \rangle_{i \in I}$ along probabilities $p_i > 0$ with $\sum_{i \in I} p_i \le 1$ is the (sub-)multidistribution defined by:

$$ \biguplus_{i \in I} p_i \cdot \mu_i := \{ \{p_i \cdot q_j : a_j\} \mid i \in I, \mu_i = \{\{q_j : a_j\}\}_{j \in J}, j \in J \} $$

A probabilistic ARS over $A$ is a set $\mathcal{P} \subseteq A \times \mathcal{M}(A)$. The probabilistic one-step reduction is given in [4] by an ARS $\hookrightarrow_P \mathcal{M}^{\le 1}(A) \times \mathcal{M}^{\le 1}(A)$. Informally, $\mu \hookrightarrow_P \nu$ if $\nu$ is obtained from $\mu$ by (i) removing terminal objects ($\not\in\mu$, $a \in \mathcal{P} \mu$), and by (ii) replacing every occurrence of a reducible object $a$ by a corresponding reduct scaled by the associated probability. Formally, the ARS $\hookrightarrow_P$ can be defined inductively, as follows:

$$ \frac{\not\in\mu. a \mathcal{P} \mu}{\{\{1 : a\}\} \hookrightarrow_P \emptyset} \qquad \frac{a \mathcal{P} \mu}{\{\{1 : a\}\} \hookrightarrow_P \mu} \qquad \frac{\sum_{i \in I} p_i \le 1 \quad \forall i \in I. \mu_i \hookrightarrow_P \nu_i}{\biguplus_{i \in I} p_i \cdot \mu_i \hookrightarrow_P \biguplus_{i \in I} p_i \cdot \nu_i} $$

A probabilistic reduction sequence is a sequence $\vec{\mu} = \langle \mu_0, \mu_1, \mu_2, \dots \rangle$ such that

$$ \mu_0 \hookrightarrow_P \mu_1 \hookrightarrow_P \mu_2 \hookrightarrow_P \dots \qquad (1) $$

where $\mu_n$ represents the state distribution after $n$-step transitions from the initial state distribution $\mu_0$. As terminal objects are removed along the way, $|\mu_n|$ quantifies the possibility of having state transitions of length at least $n$, following the reduction strategy implicit in (1).

Let $\text{red}_P(\mu)$ denote the set of all probabilistic reduction sequences starting from $\mu$. A probabilistic ARS $\mathcal{P}$ is said to be almost surely terminating (AST) if the probability of having infinite transitions is zero: $\lim_{n \to \infty} |\mu_n| = 0$ for any $\vec{\mu} \in \text{red}_P(\{\{1 : a\}\})$ of any $a \in A$; $\mathcal{P}$ is said to be positively AST if the expected derivation length $\text{edl}(\vec{\mu}) := \sum_{n \ge 1} |\mu_n| \in \mathbb{R}_{\ge 0}^\infty$ is finite for any $\vec{\mu} \in \text{red}_P(\{\{1 : a\}\})$ of any $a \in A$; and $\mathcal{P}$ is strongly AST if the expected derivation height

$$ \text{edh}_{\mathcal{P}}(\mu) := \sup\{\text{edl}(\vec{\nu}) \mid \vec{\nu} \in \text{red}_{\mathcal{P}}(\mu)\} $$

is finite for any $\mu = \{\{1 : a\}\}$ with $a \in A$.

**Example 3.** Let $\mathbb{N} := \{\underline{n} \mid n \in \mathbb{N}\}$ be a fresh copy of $\mathbb{N}$, and consider the probabilistic ARS $\mathcal{G}$ over $\mathbb{N} \uplus \mathbb{N}$, defined as

$$ \mathcal{G} := \{ \langle \underline{n}, \{\{1/2 : n, 1/2 : \underline{n} + 1\}\} \mid n \in \mathbb{N} \}. $$

Then, for instance, there is an infinite reduction sequence

$$ \{\{1 : \underline{0}\}\} \hookrightarrow_{\mathcal{G}} \{\{1/2 : 0, 1/2 : \underline{1}\}\} \hookrightarrow_{\mathcal{G}} \{\{1/4 : 1, 1/4 : \underline{2}\}\} \hookrightarrow_{\mathcal{G}} \{\{1/8 : 2, 1/8 : \underline{3}\}\} \hookrightarrow_{\mathcal{G}} \dots $$

whose expected derivation length is $1 + \frac{1}{2} + \frac{1}{4} + \dots = 2$.
Now we capture probabilistic ARS as a class of weighted ARSs, where the states and weights constitute *barycentric algebras*. A *barycentric algebra* (also called a *convex space*) is typically given as a set $X$ equipped with a binary operation $+_p : X \times X \to X$ with $x +_p y$ giving the mean of $x$ and $y$ weighted by $p \in [0, 1]$, satisfying certain laws. The binary operator extends to finite sums $\sum_{i=0}^n p_i \cdot x_i$ for $\sum_{i=0}^n p_i = 1$, and partially to infinite sums $\sum_i p_i \cdot x_i$, which can then be used to define a partial expectation operator $\mathbb{E} : \mathcal{M}(X) \to X$. In this paper, we just assume the presence of such partial operator $\mathbb{E}$.

**Definition 11 (multidistribution-algebra).** A partial $\mathcal{M}$-algebra is a set $X$ equipped with a partial barycenter operator $\mathbb{E}: \mathcal{M}(X) \to X$. We say $X$ is an $\mathcal{M}$-algebra if $\mathbb{E}(\mu) \in X$ for all $\mu \in \mathcal{M}(X)$. An $\mathcal{M}$-algebraic monoid is a monoid which is also an $\mathcal{M}$-algebra.

The monoid $\mathbb{R}_{\ge 0}$ is a partial $\mathcal{M}$-algebra by defining $\mathbb{E}(\{\{p_i : x_i\}\}_{i \in I}) := \sum_{i \in I} p_i \cdot x_i$, and $\mathbb{R}_{\ge 0}^\infty$ is an $\mathcal{M}$-algebra. The sets $\mathcal{D}(X)$ and $\mathcal{M}(X)$ of distributions and multidistributions are $\mathcal{M}$-algebras with $\mathbb{E}(\{\{p_i : d_i\}\}_{i \in I}) := \sum_{i \in I} p_i \cdot d_i$ and $\mathbb{E}(\{\{p_i : \mu_i\}\}_{i \in I}) := \bigcup_{i \in I} p_i \cdot \mu_i$, respectively. This, in turn, allows us to model ARSs with probabilistic behaviour as *barycentric ARSs*.

**Definition 12 (barycentric ARS).** A barycentric ARS is a weighted ARS $\rightsquigarrow \subseteq W \times A \times A$ where $W$ is a partial $\mathcal{M}$-algebra and $A$ is an $\mathcal{M}$-algebra, such that if $\mathbb{E}(\{p_i : w_i\})_{i \in I} \in W$ and $\forall i \in I$. $a_i \rightsquigarrow [w_i] b_i$, then

$$ \mathbb{E}\{p_i : a_i\}_{i \in I} \rightsquigarrow [\mathbb{E}\{p_i : w_i\}_{i \in I}] \mathbb{E}\{p_i : b_i\}_{i \in I}. $$

Given a weighted ARS $\rightsquigarrow \subseteq W \times A \times A$, we denote the least barycentric weighted order extending $\rightsquigarrow$ by $\tilde{\rightsquigarrow}$.

**Example 4.** The $\mathbb{R}_{\ge 0}$-weighted ARS $\rightsquigarrow_{\mathbb{R}}$ over distributions of molecules, defined by the single rule

$$ \{\frac{1}{2} : \text{HCl}, \frac{1}{2} : \text{NaOH}\} \rightsquigarrow_{\mathbb{R}}^{[56.5]} \{\frac{1}{2} : \text{NaCl}, \frac{1}{2} : \text{H}_2\text{O}\}, $$

models the classical neutralization reaction, turning hydrogen chloride and sodium hydroxide into salt and water, at a unit weight of 56.5 (kJ/mol). Then, for instance, there is a derivation leading to a normal form:

$$ \begin{align*} & \{\frac{1}{5} : \text{HCl}, \frac{4}{5} : \text{NaOH}\} \\ &= \frac{1}{5}\{\frac{1}{2} : \text{HCl}, \frac{1}{2} : \text{NaOH}\} + \frac{1}{5}\{\frac{1}{2} : \text{HCl}, \frac{1}{2} : \text{NaOH}\} + \frac{3}{5}\{1 : \text{NaOH}\} \\ &\rightsquigarrow_{\mathbb{R}}^{11.3} \frac{1}{5}\{\frac{1}{2} : \text{NaCl}, \frac{1}{2} : \text{H}_2\text{O}\} + \frac{1}{5}\{\frac{1}{2} : \text{HCl}, \frac{1}{2} : \text{NaOH}\} + \frac{3}{5}\{1 : \text{NaOH}\} \\ &\rightsquigarrow_{\mathbb{R}}^{11.3} \frac{1}{5}\{\frac{1}{2} : \text{NaCl}, \frac{1}{2} : \text{H}_2\text{O}\} + \frac{1}{5}\{\frac{1}{2} : \text{NaCl}, \frac{1}{2} : \text{H}_2\text{O}\} + \frac{3}{5}\{1 : \text{NaOH}\} \\ &= \{\frac{1}{5} : \text{NaCl}, \frac{1}{5} : \text{H}_2\text{O}, \frac{3}{5} : \text{NaOH}\}. \end{align*} $$

<footnote n="4">⁴ This instantiation is possible because we do not impose the usual idempotency law $x +_p x = x$, i.e., we do not require $\mathbb{E}(\{p_i : \mu_i\}_{i \in I}) = \mu$ for $\sum_i p_i = 1$ to hold.</footnote>
*Example 5.* The $\mathbb{R}_{\ge 0}$-weighted ARS $\mathcal{G}$ from Example 3 is modeled as weighted ARS over multidistributions $\mathcal{M}(\mathbb{N} \cup \mathbb{N})$ defined through the rules

$$ \{\{1:n\}\} \rightsquigarrow_G^{[1]} \{^{1/2}:n, 1/2:\underline{n+1}\} \quad \text{for all } n \in \mathbb{N}. $$

Then, for instance, the following infinite reduction, whose weight is bounded precisely by 2, corresponds to the reduction from Example 3:

$$ \{\{1:\underline{0}\}\} \rightsquigarrow_G^1 \{\{1/2:0, 1/2:\underline{1}\}\} \rightsquigarrow_G^{1/2} \{\{1/2:0, 1/4:1, 1/4:\underline{2}\}\} \rightsquigarrow_G^{1/4} \dots $$

The above construction generalises to arbitrary probabilistic ARSs: Given a probabilistic ARS $\mathcal{P}$ over $A$, we define the $\mathbb{R}_{\ge 0}$-weighted ARS over the state space $\mathcal{M}(A)$ by $\{\{1:a\}\} \rightsquigarrow_P^{[1]} \mu \iff a \mathcal{P} \mu$. The induced barycentric weighted order $\rightsquigarrow_P$ can also be defined inductively:

$$ \mu \rightsquigarrow_P^0 \mu \quad \frac{\mu \rightsquigarrow_P^w \nu \quad \nu \rightsquigarrow_P^v \xi}{\mu \rightsquigarrow_P^{w+v} \xi} \quad \frac{a \mathcal{P} \mu}{\{\{1:a\}\} \rightsquigarrow_P^1 \mu} \quad \frac{\forall i \in I. \mu_i \rightsquigarrow_P^{w_i} \nu_i}{\biguplus_{i \in I} p_i \cdot \mu_i \rightsquigarrow_P^{\sum_{i \in I} p_i \cdot w_i} \biguplus_{i \in I} p_i \cdot \nu_i} $$

where the last rule assumes $\sum_{i \in I} p_i \cdot w_i < \infty$. Unlike the one-step $\hookrightarrow_P$, the weighted order $\rightsquigarrow_P$ already covers multi-step reductions. As illustrated in Example 5, terminals remain persistent through reductions. The weight $w$ in a step $\mu \rightsquigarrow_P^w \nu$ gives the expected number of reduction steps carried out in the reduction from $\mu$ to $\nu$. Precisely, the potentials reflect expected derivation heights:

**Lemma 3.** Let $\mathcal{P} \subseteq A \times \mathcal{M}(A)$ be a probabilistic ARS over $A$. Then $\mathrm{edh}_P(\mu) = \mathrm{pot}_{\rightsquigarrow_P}(\mu)$ for every proper multidistribution $\mu \in \mathcal{M}(A)$.

*Proof.* Observe that, for $\mu, \nu, \rho \in \mathcal{M}^{\le 1}(A)$, if $\mu \hookrightarrow_P \nu$, then $\mu \uplus \rho \rightsquigarrow_P^{|\nu|} \nu \uplus \xi \uplus \rho$, where $\xi \subseteq \mu$ gives the sub-multidistribution of terminals in $\mu$. We first show

$$ \mathrm{edh}_P(\mu) = \sup \left\{ \sum_{i=1}^{\infty} |\mu_i| \mid \mu \hookrightarrow_P \mu_1 \hookrightarrow_P \mu_2 \hookrightarrow_P \dots \right\} \le \mathrm{pot}_{\rightsquigarrow_P}(\mu) $$

for every proper multidistribution $\mu$. To this end, consider an infinite reduction of the form $\mu \hookrightarrow_P \mu_1 \hookrightarrow_P \mu_2 \hookrightarrow_P \dots$. The above observation inductively yields

$$ \mu \rightsquigarrow_P^{|\mu_1|} \mu_1 \uplus \xi_1 \rightsquigarrow_P^{|\mu_2|} \mu_2 \uplus \xi_1 \uplus \xi_2 \rightsquigarrow_P^{|\mu_3|} \dots \rightsquigarrow_P^{|\mu_n|} \mu_n \uplus \xi_1 \uplus \dots \uplus \xi_n, $$

and thus $\mu \rightsquigarrow_P^{|\mu_1|+\dots+|\mu_n|} \mu_n \uplus \xi_1 \uplus \dots \uplus \xi_n$ for every $n \in \mathbb{N}$. By the definition of potentials, we have $|\mu_1| + \dots + |\mu_n| \le \mathrm{pot}_{\rightsquigarrow_P}(\mu)$ for every $n \in \mathbb{N}$, and thus $\sum_{i=1}^{\infty} |\mu_i| \le \mathrm{pot}_{\rightsquigarrow_P}(\mu)$. We conclude by showing

$$ \mathrm{edh}_P(\mu) \ge \sup \{w \mid \mu \rightsquigarrow_P^w \nu\} = \mathrm{pot}_{\rightsquigarrow_P}(\mu), $$

that is, $w \le \mathrm{edh}_P(\mu)$ whenever $\mu \rightsquigarrow_P^w \nu$. More precisely we prove $\mathrm{edh}_P(\mu) \ge w + \mathrm{edh}_P(\nu)$ by induction on the derivation of $\mu \rightsquigarrow_P^w \nu$. The claim is trivial if $\mu = \nu$ and $w = 0$. If $\mu \rightsquigarrow_P^u \xi \rightsquigarrow_P^v \nu$ and $w = u + v$, then

$$ \mathrm{edh}_P(\mu) \ge u + \mathrm{edh}_P(\xi) \ge u + v + \mathrm{edh}_P(\nu) = w + \mathrm{edh}_P(\nu) $$
by the induction hypotheses. If $\mu = \{\{1 : a\}\}, a \in \mathcal{P} \nu$, and $w = 1$, then we conclude as $\mathrm{edh}_{\mathcal{P}}(\{\{1 : a\}\}) \ge 1 + \mathrm{edh}_{\mathcal{P}}(\nu)$ by definition of $\mathrm{edh}_{\mathcal{P}}$. Finally, consider $\mu = \biguplus_{i \in I} p_i \cdot \mu_i$, $\nu = \biguplus_{i \in I} w_i \cdot \nu_i$, $w = \sum_{i \in I} p_i \cdot w_i$, and $\mu_i \rightsquigarrow_{\mathcal{P}}^{w_i} \nu_i$ for all $i \in I$. It is not difficult to show that $\mathrm{edh}_{\mathcal{P}}(\mu) = \sum_{i \in I} p_i \cdot \mathrm{edh}_{\mathcal{P}}(\mu_i)$ (cf. [4, Lemma 4]). By induction hypothesis, $\mathrm{edh}_{\mathcal{P}}(\mu_i) \ge w_i + \mathrm{edh}_{\mathcal{P}}(\nu_i)$, and consequently,

$$ \mathrm{edh}_{\mathcal{P}}(\mu) = \sum_{i \in I} p_i \cdot \mathrm{edh}_{\mathcal{P}}(\mu_i) \ge \sum_{i \in I} p_i \cdot (w_i + \mathrm{edh}_{\mathcal{P}}(\nu_i)) = w + \mathrm{edh}_{\mathcal{P}}(\nu). \quad \square $$

**Proposition 5.** A probabilistic ARS $\mathcal{P} \subseteq A \times \mathcal{M}(A)$ is strongly AST iff $\rightsquigarrow_{\mathcal{P}}$ is strongly bounded on singleton multidistributions.

As we have seen in Corollary 1 and Theorem 2, embeddings of $\rightsquigarrow$ into the canonical $W$-weighted ARS $\succ_W$ are also sound and complete for proving strong boundedness of barycentric ARSs. For soundness, one can use embeddings of $\rightsquigarrow$ instead of the barycentric extension $\rightsquigarrow$, if the embeddings are affine.

**Definition 13 (affinity).** Let $A$ and $X$ be $\mathcal{M}$-algebras, with barycenter operators $\mathbb{E}_A$ and $\mathbb{E}_X$, respectively. We say a mapping $\eta : A \to X$ is affine if $\eta(\mathbb{E}_A\{\{p_i : a_i\}\}_{i \in I}) = \mathbb{E}_X\{\{p_i : \eta(a_i)\}\}_{i \in I}$.

**Theorem 5 (affine embedding, soundness).** Let $W$ be a partial $\mathcal{M}$-algebra, $A$ and $X$ be $\mathcal{M}$-algebras, and $\eta : A \to X$ an affine embedding of $\rightsquigarrow \subseteq W \times A \times A$ into a barycentric weighted order $\succ \subseteq W \times X \times X$. Then $\mathrm{Pot}_{\rightsquigarrow}(a) \subseteq \mathrm{Pot}_{\succ}(\eta(a))$. In particular, $\mathrm{SB}_{\succ}(\eta(S))$ implies $\mathrm{SB}_{\rightsquigarrow}(S)$.

*Proof.* We prove by induction on the derivation that $a \rightsquigarrow^{w} b$ implies $\eta(a) \succ^{w} \eta(b)$. Hence $\eta$ is an embedding from $\rightsquigarrow$ to $\succ$, and we conclude the claim by Theorem 1. The interesting case is when $a = \mathbb{E}\{\{p_i : a_i\}\}_{i \in I} \rightsquigarrow^{w} \mathbb{E}\{\{p_i : b_i\}\}_{i \in I} = b$, $w = \mathbb{E}\{\{p_i : w_i\}\}_{i \in I} \in W$, and $a_i \rightsquigarrow^{w_i} b_i$ for all $i \in I$. Then induction hypothesis gives $\eta(a_i) \succ^{w_i} \eta(b_i)$, and since $\eta$ is affine and $\succ$ is barycentric, we conclude

$$ \eta(a) = \eta(\mathbb{E}\{\{p_i : a_i\}\}_{i \in I}) = \mathbb{E}\{\{p_i : \eta(a_i)\}\}_{i \in I} \\ \succ^{w} \mathbb{E}\{\{p_i : \eta(b_i)\}\}_{i \in I} = \eta(\mathbb{E}\{\{p_i : b_i\}\}_{i \in I}) = \eta(b). \quad \square $$

For any $\mathbb{R}_{\ge 0}$-valued function $h : A \to \mathbb{R}_{\ge 0}$, the expectation $\mathbb{E}h(\{p_i : a_i\}_{i \in I}) := \sum_{i \in I} p_i \cdot h(a_i)$ is affine on $\mathcal{D}(A)$ or $\mathcal{M}(A)$. Moreover, $\succ_{\mathbb{R}_{\ge 0}} \subseteq \mathbb{R}_{\ge 0} \times \mathbb{R}_{\ge 0}^{\infty} \times \mathbb{R}_{\ge 0}^{\infty}$ is a barycentric weighted order, as $\forall i \in I$. $x_i \ge w_i + y_i$ implies

$$ \sum_{i \in I} p_i \cdot x_i \ge \sum_{i \in I} p_i \cdot (w_i + y_i) = \sum_{i \in I} p_i \cdot w_i + \sum_{i \in I} p_i \cdot y_i, $$

i.e., $\mathbb{E}\{\{p_i : x_i\}\}_{i \in I} \succ_{\mathbb{R}_{\ge 0}} \mathbb{E}\{\{p_i : w_i\}\}_{i \in I} \mathbb{E}\{\{p_i : y_i\}\}_{i \in I}$. Therefore, $\mathbb{R}_{\ge 0}$-valued ranking functions are sound for proving strong boundedness of barycentric $\mathbb{R}_{\ge 0}$-weighted ARSs. This generalises to arbitrary partial $\mathcal{M}$-algebras $W$, provided $W^{\infty}$ forms an $\mathcal{M}$-algebra which is

$$ \text{-- monotone: if } \forall i \in I. x_i \ge y_i, \text{ then } \mathbb{E}\{\{p_i : x_i\}\}_{i \in I} \ge \mathbb{E}\{\{p_i : y_i\}\}_{i \in I}; \text{ and} $$
superadditive: $\mathbb{E}\{\{p_i : x_i + y_i\}\}_{i \in I} \ge \mathbb{E}\{\{p_i : x_i\}\}_{i \in I} + \mathbb{E}\{\{p_i : y_i\}\}_{i \in I}$.

**Theorem 6 (ranking functions, soundness).** Let $\mathcal{W}$ be an $\mathcal{M}$-algebraic positive monoid such that $\mathcal{W}^\infty$ is monotone and superadditive. If a weighted ARS $\rightsquigarrow \subseteq \mathcal{W} \times A \times A$ admits an affine ranking function $\eta : A \to \mathcal{W}^\infty$ with $\eta(S) \subseteq \mathcal{W}$, then $\text{SB}_{\rightsquigarrow}(S)$. In particular, $\text{pot}_{\rightsquigarrow}(a) \le \eta(a)$ for every $a \in S$.

*Proof.* To use Theorem 5 we show that the weighted order $\succ_{\mathcal{W}} \subseteq \mathcal{W} \times \mathcal{W}^\infty \times \mathcal{W}^\infty$ is barycentric. So consider $x_i, y_i \in \mathcal{W}^\infty$ such that $x_i \succ_{\mathcal{W}}^{w_i} y_i$, i.e., $x_i \ge w_i + y_i$ for all $i \in I$, and $\mathbb{E}(\{\{p_i : w_i\}\}_{i \in I}) \in \mathcal{W}$. We have, indeed,

$$ \mathbb{E}\{\{p_i : x_i\}\}_{i \in I} \ge \mathbb{E}\{\{p_i : w_i + y_i\}\}_{i \in I} \ge \mathbb{E}\{\{p_i : w_i\}\}_{i \in I} + \mathbb{E}\{\{p_i : y_i\}\}_{i \in I}, $$

by monotonicity and superadditivity. Now $\text{Pot}_{\rightsquigarrow}(a) \subseteq \text{Pot}_{\succ_{\mathcal{W}}}(\eta(a))$ by Theorem 5, so with Lemma 1 we conclude

$$ \text{pot}_{\rightsquigarrow}(a) = \sup \text{Pot}_{\rightsquigarrow}(a) \le \sup \text{Pot}_{\succ_{\mathcal{W}}}(\eta(a)) = \text{pot}_{\succ_{\mathcal{W}}}(\eta(a)) = \eta(a) \in \mathcal{W}. \quad \square $$

*Example 6.* Theorem 6 proves that $\tilde{\eta}_{\mathcal{R}}$ from Example 4 is strongly bounded on all distributions using the affine ranking function $\mathbb{E}h$, where $h(\text{HCl}) = h(\text{NaOH}) = 56.5$, and $h(\text{NaCl}) = h(\text{H}_2\text{O}) = 0$; being a ranking function is exemplified by:

$$ \begin{aligned} \mathbb{E}h(\{1/2 : \text{HCl}, 1/2 : \text{NaOH}\}) &= 1/2 \cdot h(\text{HCl}) + 1/2 \cdot h(\text{NaOH}) = 56.5 \\ &= 56.5 + 1/2 \cdot h(\text{NaCl}) + 1/2 \cdot h(\text{H}_2\text{O}) = 56.5 + \mathbb{E}h(\{1/2 : \text{HCl}, 1/2 : \text{NaOH}\}). \end{aligned} $$

*Example 7.* We can prove that $\tilde{\eta}_{\mathcal{G}}$ from Example 4 is strongly bounded, by defining $h(\underline{n}) = 2$ and $h(n) = 0$. Then, for any $n \in \mathbb{N}$,

$$ \mathbb{E}h(\{1 : \underline{n}\}) = 2 \ge 1 + 1/2 \cdot h(n) + 1/2 \cdot h(n+1) = 1 + \mathbb{E}h(\{1/2 : n, 1/2 : \underline{n+1}\}). $$

Theorem 6 encompasses the soundness of probabilistic ranking functions [4]. As illustrated in the above example, if there exists $h : A \to \mathbb{R}_{\ge 0}$ such that $h(a) \ge 1 + \mathbb{E}h(\mu)$ for all $a \in \mathcal{P} \mu$, then Theorem 6 ensures that $\rightsquigarrow_{\mathcal{P}}$ over $\mathcal{M}(A)$ is strongly bounded, i.e., $\mathcal{P}$ is strongly AST. They are also complete for proving strong AST of probabilistic ARSs [4], since pot serves as a ranking function. We conjecture that affine ranking functions are complete for a reasonably wide class of barycentric ARSs; however, pot is not necessarily affine in general: note that $\text{pot}_{\rightsquigarrow_{\mathcal{R}}} (\{1 : \text{HCl}\}) = \text{pot}_{\rightsquigarrow_{\mathcal{R}}} (\{1 : \text{NaOH}\}) = 0$ in Example 4.

# 5 Conclusion

In this work, we introduced weighted ARSs, providing a framework for studying rewriting systems with quantitative properties, particularly those related to complexity. By assigning uniform weights, weighted ARSs generalize standard and relative rewriting while enabling the analysis of reduction systems with non-uniform weights, such as expectation-based properties in probabilistic systems. To study (strong) boundedness in this setting, we established ranking functions as a central tool, and have seen how these adapt to weighted term rewrite systems and barycentric ARSs, encompassing probabilistic reduction systems.

As future work, it would for instance be interesting to enrich the theory with a study of confluence and related properties.
References

1. Avanzini, M., Barthe, G., Lago, U.D.: On continuation-passing transformations and expected cost analysis. Proc. ACM Program. Lang. **5**(ICFP), 1–30 (2021). https://doi.org/10.1145/3473592

2. Avanzini, M., Lago, U.D.: Automating sized-type inference for complexity analysis. Proc. ACM Program. Lang. **1**(ICFP), 43:1–43:29 (2017). https://doi.org/10.1145/3110287

3. Avanzini, M., Lago, U.D., Yamada, A.: On probabilistic term rewriting. In: Gallagher, J.P., Sulzmann, M. (eds.) Functional and Logic Programming - 14th International Symposium, FLOPS 2018, Nagoya, Japan, May 9-11, 2018, Proceedings. Lecture Notes in Computer Science, vol. 10818, pp. 132–148. Springer (2018). https://doi.org/10.1007/978-3-319-90686-7_9

4. Avanzini, M., Lago, U.D., Yamada, A.: On probabilistic term rewriting. Sci. Comput. Program. **185** (2020). https://doi.org/10.1016/J.SCICO.2019.102338

5. Avanzini, M., Moser, G., Péchoux, R., Perdrix, S., Zamdzhiev, V.: Quantum expectation transformers for cost analysis. In: Baier, C., Fisman, D. (eds.) LICS '22: 37th Annual ACM/IEEE Symposium on Logic in Computer Science, Haifa, Israel, August 2–5, 2022. pp. 10:1–10:13. ACM (2022). https://doi.org/10.1145/3531130.3533332

6. Avanzini, M., Moser, G., Schaper, M.: A modular cost analysis for probabilistic programs. Proc. ACM Program. Lang. **4**(OOPSLA), 172:1–172:30 (2020). https://doi.org/10.1145/3428240

7. Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press (1998)

8. Baillot, P., Ghyselen, A., Kobayashi, N.: Sized types with usages for parallel complexity of pi-calculus processes. In: Haddad, S., Varacca, D. (eds.) 32nd International Conference on Concurrency Theory, CONCUR 2021, August 24-27, 2021, Virtual Conference. LIPIcs, vol. 203, pp. 34:1–34:22. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2021). https://doi.org/10.4230/LIPICS.CONCUR.2021.34

9. Bournez, O., Garnier, F.: Proving positive almost-sure termination. In: Giesl, J. (ed.) Term Rewriting and Applications, 16th International Conference, RTA 2005, Nara, Japan, April 19-21, 2005, Proceedings. Lecture Notes in Computer Science, vol. 3467, pp. 323–337. Springer (2005). https://doi.org/10.1007/978-3-540-32033-3_24

10. Danielsson, N.A.: Lightweight semiformal time complexity analysis for purely functional data structures. In: Necula, G.C., Wadler, P. (eds.) Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2008, San Francisco, California, USA, January 7-12, 2008. pp. 133–144. ACM (2008). https://doi.org/10.1145/1328438.1328457

11. Droste, M., Kuske, D.: Weighted automata. In: Pin, J. (ed.) Handbook of Automata Theory, pp. 113–150. European Mathematical Society Publishing House, Zürich, Switzerland (2021). https://doi.org/10.4171/AUTOMATA-1/4

12. Faggian, C.: Probabilistic rewriting and asymptotic behaviour: on termination and unique normal forms. Log. Methods Comput. Sci. **18**(2) (2022). https://doi.org/10.46298/LMCS-18(2:5)2022

13. Fu, H., Chatterjee, K.: Termination of nondeterministic probabilistic programs. In: Enea, C., Piskac, R. (eds.) Verification, Model Checking, and Abstract Interpretation - 20th International Conference, VMCAI 2019, Cascais, Portugal, January 13-15, 2019, Proceedings. Lecture Notes in Computer Science, vol. 11388, pp. 468–490. Springer (2019). https://doi.org/10.1007/978-3-030-11245-5_22
14. Gavazzo, F., Florio, C.D.: Elements of quantitative rewriting. Proc. ACM Program. Lang. 7(POPL), 1832–1863 (2023). https://doi.org/10.1145/3571256

15. Lago, U.D., Martini, S.: An invariant cost model for the lambda calculus. In: Beckmann, A., Berger, U., Löwe, B., Tucker, J.V. (eds.) Logical Approaches to Computational Barriers, Second Conference on Computability in Europe, CiE 2006, Swansea, UK, June 30-July 5, 2006, Proceedings. Lecture Notes in Computer Science, vol. 3988, pp. 105–114. Springer (2006). https://doi.org/10.1007/11780342_11

16. Laird, J., Manzonetto, G., McCusker, G., Pagani, M.: Weighted relational models of typed lambda-calculi. In: 28th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2013, New Orleans, LA, USA, June 25-28, 2013. pp. 301–310. IEEE Computer Society (2013). https://doi.org/10.1109/LICS.2013.36

17. Naaf, M., Frohn, F., Brockschmidt, M., Fuhs, C., Giesl, J.: Complexity analysis for term rewriting by integer transition systems. In: Dixon, C., Finger, M. (eds.) Frontiers of Combining Systems - 11th International Symposium, FroCoS 2017, Brasília, Brazil, September 27-29, 2017, Proceedings. Lecture Notes in Computer Science, vol. 10483, pp. 132–150. Springer (2017). https://doi.org/10.1007/978-3-319-66167-4_8

18. van Oostrom, V., Toyama, Y.: Normalisation by random descent. In: Kesner, D., Pientka, B. (eds.) 1st International Conference on Formal Structures for Computation and Deduction, FSCD 2016, June 22-26, 2016, Porto, Portugal. LIPIcs, vol. 52, pp. 32:1–32:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2016). https://doi.org/10.4230/LIPICS.FSCD.2016.32

19. Thrane, C., Fahrenheit, U., Larsen, K.G.: Quantitative analysis of weighted transition systems. The Journal of Logic and Algebraic Programming 79(7), 689 – 703 (2010). https://doi.org/10.1016/j.jlap.2010.07.010