**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 \text{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;

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

4. $\text{SB}_{\rightsquigarrow}(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.

Figure 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}_{\rightsquigarrow}(S) \implies \text{WN}_{\rightsquigarrow}(S)$;

2. $\text{SB}_{\rightsquigarrow}(S) \implies \text{WB}_{\rightsquigarrow}(S)$;

3. $\text{SN}_{\rightsquigarrow}(S) \implies \text{WB}_{\rightsquigarrow}(S)$;

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

5. $\text{SN}_{\rightsquigarrow}(S) \implies \text{SB}_{\rightsquigarrow}(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}_{\rightsquigarrow}(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. Figure 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).
<figure><img src="image_40.png" /><figcaption>Fig. 2. Examples demonstrating the strictness of the implications in Proposition 1.</figcaption></figure>

## 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}_{>}^>(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 + \dots + w_n$. By Definition 5,

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

i.e., $\eta(a) \succ_w \eta(b)$ and hence $w \in \text{Pot}_{\succ}(\eta(a))$. This concludes $\text{Pot}_{\succ}(a) \subseteq \text{Pot}_{\succ}(\eta(a))$. Moreover, if $\text{Pot}_{\succ}(\eta(a))$ has a bound $b \in W$ then so does $\text{Pot}_{\succ}(a)$, trivially. Hence, $\text{SB}_{\succ}(\eta(S))$ implies $\text{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$, $\text{SB}_{\succ_W}(W)$ and $\text{pot}_{\succ_W}(x) = x$.

*Proof.* Fix $x \in W$. Note that $\text{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 $\text{Pot}_{\succ_W}(x)$. Since $x = x + 0 \in \text{Pot}_{\succ_W}(x)$, $x$ is the maximum and thus supremum of $\text{Pot}_{\succ_W}(x)$, i.e., $\text{pot}_{\succ_W}(x) = \sup \text{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 $\text{SB}_{\succ_W}(S)$. In particular, $\text{pot}_{\succ_W}(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, $\text{pot}_{\succ_W}: A \to W^\infty$ is defined.

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

$$\text{Pot}_{\succ_W}(a) = \{v \mid \exists c. a \rightsquigarrow^v c\} \supseteq \{w + u \mid \exists c. b \rightsquigarrow^u c\} =: X.$$
Since $\text{pot}_{\rightsquigarrow}(a) \in \mathcal{W}$ is a bound of $\text{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

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

i.e., indeed $\text{pot}_{\rightsquigarrow}(a) \succ_{\mathcal{W}}^{[w]} \text{pot}_{\rightsquigarrow}(b)$ holds. Finally, since $\text{SB}_{\rightsquigarrow}(S)$ means that $\text{Pot}_{\rightsquigarrow}(a)$ has a bound in $\mathcal{W}$ for every $a \in S$, bounded-completeness gives $\text{pot}_{\rightsquigarrow}(a) \in \mathcal{W}$. This concludes $\text{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 $\text{NF}(\mapsto)$ denote the standard $n$-th fold, transitive closure, reflexive-transitive closure, and the set normal forms of $\mapsto$, respectively. The *derivation height* $\text{dh}_{\mapsto}(a) \in \mathbb{N}^{\infty}$ of $a \in A$ with respect to $\mapsto$ is defined by $\text{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$ where $\alpha \in \mathbb{N} \cup \{*+, +\}$,

- $\text{NF}(\{1\} \times \mapsto) = \text{NF}(\mapsto)$, and $\text{pot}_{\{1\} \times \mapsto}(s) = \text{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^*$ 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)^+$,

- $\mathbf{NF}(\mapsto//\sim) = \mathbf{NF}(\mapsto/\sim)$, and $\mathbf{pot}_{\mapsto//\sim}(s) = \mathbf{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_R$ 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_R$ over $\mathcal{T}(\mathcal{F}, \mathcal{V})$ as the least weighted rewrite relation containing $\mathcal{R}$; more concretely $C[l\sigma] \rightsquigarrow_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_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_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_R$ into $\succ$. From this, it follows that $\rightsquigarrow_R$ is strongly bounded by Theorem 1. The “only if” direction follows by taking $\rightsquigarrow_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 A, \succ \rangle$ consists of an $\mathcal{F}$-algebra $A$ and a weighted ARS $\succ \subseteq \mathcal{W} \times A \times A$, such that every interpretation is monotone with respect to $\succ$, that is, $x \succ^{[w]} y$ implies $f_A(\dots, x, \dots) \succ^{[w]} f_A(\dots, y, \dots)$ for every $f \in \mathcal{F}$.

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

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

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

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

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

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

One prototypical instance for the order $\succ$ is the canonical weighted ARS $\succ_N$; this way, interpretations over naturals can be seen as a way to inductively define ranking functions on TRSs. Another noticeable instance is $\succ_{\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 $A$) allow sampling of reducts from a (probability) distribution, a function $d: A \to [0, 1]$ with $\sum_{a \in A} d(a) = 1$, assigning to each $a \in 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 $A$ by $\mathcal{D}(A)$. The *convex combinations* of distributions are defined by $(\sum_{i \in I} p_i \cdot d_i)(a) := \sum_{i \in I} p_i \cdot d_i(a)$ for $\sum_{i \in I} p_i = 1$. We may view distributions as sets of pairs of $a \in A$ and $p > 0$ written $p: a$, i.e., $d = \{d(a): a \mid a \in A, d(a) > 0\}$. A (*sub*)*multidistribution* on $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_{\mathcal{P}} \subseteq \mathcal{M}^{\le 1}(A) \times \mathcal{M}^{\le 1}(A)$. Informally, $\mu \hookrightarrow_{\mathcal{P}} \nu$ if $\nu$ is obtained from $\mu$ by (i) removing terminal objects ($\nexists \mu. a \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_{\mathcal{P}}$ can be defined inductively, as follows:

$$ \frac{\nexists \mu. a \mathcal{P} \mu}{\{\{1 : a\}\} \hookrightarrow_{\mathcal{P}} \emptyset} \qquad \frac{a \mathcal{P} \mu}{\{\{1 : a\}\} \hookrightarrow_{\mathcal{P}} \mu} \qquad \frac{\sum_{i \in I} p_i \le 1 \quad \forall i \in I. \mu_i \hookrightarrow_{\mathcal{P}} \nu_i}{\biguplus_{i \in I} p_i \cdot \mu_i \hookrightarrow_{\mathcal{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_{\mathcal{P}} \mu_1 \hookrightarrow_{\mathcal{P}} \mu_2 \hookrightarrow_{\mathcal{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 (eq:red).

Let $\text{red}_{\mathcal{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}_{\mathcal{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}_{\mathcal{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{aligned} & \{\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} \{\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} \{\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} \{\text{NaOH}\} \\ &= \{\frac{1}{5} : \text{NaCl}, \frac{1}{5} : \text{H}_2\text{O}, \frac{3}{5} : \text{NaOH}\}. \end{aligned} $$

<footnote n="2">² 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 : \underline{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 := \Leftrightarrow a \mathcal{P} \mu$. The induced barycentric weighted order $\rightsquigarrow_P$ can also be defined inductively:

$$ \frac{\mu \rightsquigarrow_P^0 \mu}{\mu \rightsquigarrow_P^0} \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}_{\mathcal{P}}(\mu) = \mathrm{pot}_{\rightsquigarrow_{\mathcal{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}_{\mathcal{P}}(\mu) = \sup \{ \sum_{i=1}^{\infty} |\mu_i| \mid \mu \hookrightarrow_P \mu_1 \hookrightarrow_P \mu_2 \hookrightarrow_P \dots \} \le \mathrm{pot}_{\rightsquigarrow_{\mathcal{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}_{\mathcal{P}}(\mu) \ge \sup \{w \mid \mu \rightsquigarrow_P^w \nu\} = \mathrm{pot}_{\rightsquigarrow_{\mathcal{P}}}(\mu), $$

that is, $w \le \mathrm{edh}_{\mathcal{P}}(\mu)$ whenever $\mu \rightsquigarrow_P^w \nu$. More precisely we prove $\mathrm{edh}_{\mathcal{P}}(\mu) \ge w + \mathrm{edh}_{\mathcal{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}_{\mathcal{P}}(\mu) \ge u + \mathrm{edh}_{\mathcal{P}}(\xi) \ge u + v + \mathrm{edh}_{\mathcal{P}}(\nu) = w + \mathrm{edh}_{\mathcal{P}}(\mu) $$
by the induction hypotheses. If $\mu = \{\{1 : a\}\}, a \in \mathcal{P} \nu, \text{ and } w = 1, \text{ then we conclude as } \mathrm{edh}_{\mathcal{P}}(\{\{1 : a\}\}) \ge 1 + \mathrm{edh}_{\mathcal{P}}(\nu) \text{ by definition of } \mathrm{edh}_{\mathcal{P}}$. Finally, consider $\mu = \bigcup_{i \in I} p_i \cdot \mu_i, \nu = \bigcup_{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 $\mathcal{W}$-weighted ARS $\succ_{\mathcal{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 $\mathcal{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 \mathcal{W} \times A \times A$ into a barycentric weighted order $\succ \subseteq \mathcal{W} \times X \times X$. Then $\mathrm{Pot}_{\rightsquigarrow}(a) \subseteq \mathrm{Pot}_{\succ}(\eta(a))$. In particular, $\mathrm{SB}_{\rightsquigarrow}(\eta(S))$ implies $\mathrm{SB}_{\succ}(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 \mathcal{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 $\mathcal{W}$, provided $\mathcal{W}^{\infty}$ forms an $\mathcal{M}$-algebra which is
- monotone: if $\forall i \in I$. $x_i \ge y_i$, then $\mathbb{E}\{p_i : x_i\}_{i \in I} \ge \mathbb{E}\{p_i : y_i\}_{i \in I}$; 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 \mathcal{A} \times \mathcal{A}$ admits an affine ranking function $\eta: \mathcal{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_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_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_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_W}(\eta(a)) = \text{pot}_{\succ_W}(\eta(a)) = \eta(a) \in \mathcal{W}. \quad \square $$

*Example 6.* Theorem 6 proves that $\rightsquigarrow_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 $\rightsquigarrow_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(\underline{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_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_R}(\{1 : \text{HCl}\}) = \text{pot}_{\rightsquigarrow_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., Dal Lago, U.: 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., Dal Lago, U.: 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., Dal Lago, U., Yamada, A.: On probabilistic term rewriting. In: Gallagher, J.P., Sulzmann, M. (eds.) FLOPS 2018. LNCS, vol. 10818, pp. 132–148. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-90686-7_9

4. Avanzini, M., Dal Lago, U., 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 2022: 37th Annual ACM/IEEE Symposium on Logic in Computer Science, Haifa, Israel, 2–5 August 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, Cambridge (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, 24–27 August 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.) RTA 2005. LNCS, vol. 3467, pp. 323–337. Springer, Heidelberg (2005). https://doi.org/10.1007/978-3-540-32033-3_24

10. Dal Lago, U., Martini, S.: An invariant cost model for the lambda calculus. In: Beckmann, A., Berger, U., Löwe, B., Tucker, J.V. (eds.) CiE 2006. LNCS, vol. 3988, pp. 105–114. Springer, Heidelberg (2006). https://doi.org/10.1007/11780342_11
11. Danielsson, N.A.: Lightweight semiformal time complexity analysis for purely func-
tional 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, 7–12 January 2008, pp. 133–144. ACM
(2008). https://doi.org/10.1145/1328438.1328457

12. 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

13. 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

14. Fu, H., Chatterjee, K.: Termination of nondeterministic probabilistic programs. In: Enea, C., Piskac, R. (eds.) VMCAI 2019. LNCS, vol. 11388, pp. 468–490. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-11245-5_22

15. Gavazzo, F., Florio, C.D.: Elements of quantitative rewriting. Proc. ACM Program. Lang. 7(POPL), 1832–1863 (2023). https://doi.org/10.1145/3571256

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, 25–28 June 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.) Fro-CoS 2017. LNCS (LNAI), vol. 10483, pp. 132–150. Springer, Cham (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., Fahrenberg, U., Larsen, K.G.: Quantitative analysis of weighted transition systems. J. Logic Algebraic Program. 79(7), 689–703 (2010). https://doi.org/10.1016/j.jlap.2010.07.010

**Open Access** This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.

The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
# Graph-Embedded Rewrite Systems: Combination and Undecidability Results

Serdar Erbatur¹, Andrew M. Marshall², Paliath Narendran³, and Christophe Ringeissen⁴

¹ University of Texas at Dallas, Richardson, TX, USA
serdar.erbatur@utdallas.edu

² University of Mary Washington, Fredericksburg, VA, USA
marshall@umw.edu

³ University at Albany, SUNY, Albany, NY, USA
pnarendran@albany.edu

⁴ Université de Lorraine, CNRS, Inria, LORIA, 54000 Nancy, France
christophe.ringeissen@loria.fr

**Abstract.** In this paper, we consider the knowledge problems of *deduction* and *static equivalence* in the formal analysis of security protocols. We extend a recent result that developed a decision procedure for these problems in the non-disjoint combination $R \cup E$, where $R$ is a subterm $E$-convergent term rewrite system (TRS) and $E$ is a restricted form of permutative theory. Here, we consider the same combination problem but replace the subterm $E$-convergent TRS with a superclass of subterm $E$-convergent, called *contracting $E$-convergent*. We show that the previous decision procedure can be extended to obtain a new algorithm for this larger class of combined theories.

We also explore the gap between the contracting TRSs, for which deduction and static-equivalence are decidable, and a larger superclass called *graph-embedded* for which these problems are undecidable. This gap is of interest since one would like to get closer to graph-embedded and still maintain decidability of the above “knowledge problems.” We show that at least one way of weakening the restrictions of the contracting definition will not work, as it leads to undecidability results for deduction and static equivalence. We also show that a subset of the graph-embedded rules is still sufficient to obtain undecidability.

**Keywords:** Permutative Equational Theories · Term Rewriting · Combination

## 1 Introduction

In the formal analysis of security protocols, a number of tools have been developed that use constraint solving in term algebras [3, 8, 10, 11, 15, 20, 25, 29, 30]. These tools implement algorithms and procedures to reason about the knowledge an adversary could gain by observing a protocol in execution. Two key
measures of this knowledge are (intruder) deduction [24,28] and *static equivalence* [1], and there has been substantial work on developing decision procedures for these problems (e.g., [1,4,7,11,13,18]). These procedures typically model protocols symbolically, using rewrite systems or equational theories, and are often proven sound and complete for specific classes of theories.

One of the most common such classes is that of subterm convergent term rewrite systems. These are systems where the right-hand side of each rule is a strict subterm of the left-hand side or a constant (see, e.g., [1,11]). In recent work [9,16], an extension of this class, called *graph-embedded*, was introduced. This class leverages the graph minor relation in term graphs to define a super-class of subterm convergent systems. However, deduction and static equivalence problems are undecidable for graph-embedded systems. To address this, a sub-class called *contracting* was identified in [9,16], for which both problems remain decidable.

In this paper, we begin to explore the gap between the contracting and graph-embedded classes. This is of interest because narrowing this gap could allow for broader classes of theories to be analyzed while preserving decidability. We show that at least one natural weakening of the contracting definition leads to undecidability for both deduction and static equivalence. Furthermore, we examine restrictions of the graph-embedded definition, demonstrating that even a single rule from this definition can lead to undecidability. While it is plausible that the gap between contracting and graph-embedded systems can be reduced without sacrificing decidability, the best approach to achieving this remains an open question.

Another important aspect of many decision procedures is the ability to handle combinations of theories, particularly when some components cannot be oriented into a term rewrite system—for example, theories involving Associativity and Commutativity (AC). In recent work [19], decision procedures were developed for deduction and static equivalence in combined theories of the form $R \cup E$, where $R$ and $E$ are non-disjoint. In [19] $R$ is a subterm convergent term rewrite system, and $E$ several types of permutative theories.

In this paper, we again consider the same combination scenario $R \cup E$ but go beyond the restriction that $R$ is a subterm rewrite system. Rather, we investigate the case where $R$ is a contracting rewrite system and $R$ is convergent modulo a permutative theory $E$. We show that the procedure developed in [19] can be adapted to the larger class of theories where $R$ is contracting. Thus, we obtain decision procedures for deductions and static equivalence in this larger class of theories.

*Paper Outline:* Section 2 contains the preliminaries and background information. Section 3 presents several new combination results. In particular, it introduces the main result presented in Theorem 5. Section 4 presents several new undecidable results. First, for a contracting systems without depth restrictions, Theorem 6. Then, showing two subsets of the graph-embedded systems still have undecidable knowledge problems, Theorem 7 and Theorem 8. Finally, Sect. 5 contains the conclusions and future work.
# 2 Preliminaries

We use the standard notation of equational unification [6] and term rewriting systems [5]. Given a first-order signature $\Sigma$ and a (countable) set of variables $V$, the $\Sigma$-terms over variables $V$ are built in the usual way by taking into account the arity of each function symbol in $\Sigma$. Each $\Sigma$-term is well-formed: if it is rooted by an $n$-ary function symbol in $\Sigma$, then it has necessarily $n$ direct subterms. The set of $\Sigma$-terms over variables $V$ is denoted by $T(\Sigma, V)$. The set of variables from $V$ occurring in a term $t \in T(\Sigma, V)$ is denoted by $Var(t)$. A term $t$ is *ground* if $Var(t) = \emptyset$. A term $t$ is *linear* if each variable in $Var(t)$ occurs only once in $t$. For any position $p$ in a term $t$ (including the root position $\varepsilon$), $t(p)$ is the symbol at position $p$, $t|_p$ is the subterm of $t$ at position $p$, and $t[u]_p$ is the term $t$ in which $t|_p$ is replaced by $u$. A substitution is an endomorphism of $T(\Sigma, V)$ with only finitely many variables not mapped to themselves. A substitution is denoted by $\sigma = \{x_1 \mapsto t_1, \dots, x_m \mapsto t_m\}$, where the domain of $\sigma$ is $Dom(\sigma) = \{x_1, \dots, x_m\}$ and the range of $\sigma$ is $Ran(\sigma) = \{t_1, \dots, t_m\}$. Application of a substitution $\sigma$ to $t$ is written $t\sigma$. A $\Sigma$-equation is a pair of $\Sigma$-terms denoted by $s =^? t$ or simply $s = t$ when it is clear from the context that we do not refer to an axiom. The size of a term $t$, denoted by $|t|$, is defined inductively as follows: $|f(t_1, \dots, t_n)| = 1 + \sum_{i=1}^n |t_i|$ if $f$ is an $n$-ary function symbol with $n \ge 1$, $|c| = 1$ if $c$ is a constant, and $|x| = 1$ if $x$ is a variable. The depth of a term $t$, denoted by $depth(t)$, is defined inductively as follows: $depth(f(t_1, \dots, t_n)) = 1 + \max_{i=1, \dots, n} depth(t_i)$ if $f$ is an $n$-ary function symbol with $n \ge 1$, $depth(c) = 1$ if $c$ is a constant, and $depth(x) = 0$ if $x$ is a variable.

## 2.1 Equational Theories

Given a set $E$ of $\Sigma$-axioms (i.e., pairs of terms in $T(\Sigma, V)$, denoted by $l = r$), the *equational theory* $=_{E}$ is the congruence closure of $E$ under the law of substitutivity (by a slight abuse of terminology, $E$ is often called an equational theory). Equivalently, $=_{E}$ can be defined as the reflexive transitive closure $\leftrightarrow_E^*$ of an equational step $\leftrightarrow_E$ defined as follows: $s \leftrightarrow_E t$ if there exist a position $p$ of $s$, $l = r$ (or $r = l$) in $E$, and substitution $\sigma$ such that $s|_p = l\sigma$ and $t = s[r\sigma]_p$. An equational theory $E$ is said to be *permutative* if for any $l = r$ in $E$, the number of occurrences of any (function or variable) symbol in $l$ is equal to the number of occurrences of that symbol in $r$. Well-known theories such as *Associativity* ($A = \{(x+y)+z = x+(y+z)\}$), *Commutativity* ($C = \{x+y=y+x\}$), and *Associativity-Commutativity* ($AC = A \cup C$) are *permutative theories*. A theory $E$ is *syntactic* if it has finite *resolvent presentation S*, defined as a finite set of axioms $S$ such that each equality $t =_E u$ has an equational proof $t \leftrightarrow_S^* u$ with at most one equational step $t \leftrightarrow_S u$ applied at the root position. The theories $C$ and $AC$ are *syntactic* [22].

## 2.2 Rewrite Relations

Given a signature $\Sigma$, an oriented $\Sigma$-axiom is called a rewrite rule of the form $l \to r$ such that $l, r \in T(\Sigma, V)$, $l$ is not a variable and $Var(r) \subseteq Var(l)$. A finite
set of rewrite rules is called a *term rewriting system* (TRS, for short). Let $R$ be any TRS. For any $\Sigma$-terms $s$ and $t$, $s$ *R-rewrites* to $t$, denoted by $s \to_R t$, if there exist a position $p$ of $s$, $l \to r \in R$, and substitution $\sigma$ such that $s|_p = l\sigma$ and $t = s[r\sigma]_p$. The term $s$ is said to be *R-reducible*, $s|_p$ is called a *redex*, and in the particular case where $s|_p = l\sigma$, $s$ *R-rewrites* to $t$, denoted by $s \to_R t$. A term is an *innermost redex* if none of its proper subterms is a redex. The symmetric relation $\leftarrow_R \cup \to_R$ is denoted by $\leftarrow_R^*$. The rewrite relation $\to_R$ is confluent if $\leftarrow_R^*$ is included in $\to_R^* \circ \leftarrow_R^*$. The rewrite relation $\to_R$ is *convergent* if $\to_R$ is both terminating and confluent. When $\to_R$ is convergent, we have that for any terms $t, t', t \leftarrow_R^* t'$ iff $t \downarrow_R = t' \downarrow_R$, where $t \downarrow_R$ (resp., $t' \downarrow_R$) denotes the unique normal form of $t$ (resp., $t'$) w.r.t. $\to_R$. A convergent TRS $R$ is said to be *subterm convergent* if for any $l \to r \in R$, $r$ is either a strict subterm of $l$ or a constant. We refer to [5] for the classical notions of overlap and critical pair. Hence, a trivial critical pair is obtained by an overlap at the root position of a rule with a renaming of the same rule. A TRS with no non-trivial critical pairs is *non-overlapping*.

Let us now introduce the notion of equational rewriting, also called class
rewriting [21]. Given a TRS $R$ and an equational theory $E$, the rewrite relation
of $R$ modulo $E$ is defined as follows: $s \to_{R,E} t$ if there exist some position $p$ in $s$,
some rule $l \to r \in R$ and a substitution $\mu$ such that $s|_p =_E l\mu$ and $t = s[r\mu]|_p$. The
TRS $R$ is said to be $E$-convergent if the relation $=_E \circ \to_R \circ =_E$ is terminating
and $\leftarrow_{R,E}^* \subseteq \to_{R,E}^* \circ =_E \circ \leftarrow_{R,E}^*$. In an $E$-convergent TRS $R$, any term $t$
admits a unique $R$-normal form modulo $E$ denoted by $t \downarrow_{R,E}$, and for any terms
$s$ and $t$, we have $s \leftarrow_{R,E}^* t$ iff $(s \downarrow_{R,E}) =_E (t \downarrow_{R,E})$.

2.3 Knowledge Problems

The applied pi calculus and frames are used to model attacker knowledge [2]. In
this model, the set of messages or terms which the attacker knows, and which
could have been obtained from observing one or more protocol sessions, are
the set of terms in Ran(σ) of the frame φ = νñ.σ, where σ is a substitution
ranging over ground terms. We also need to model cryptographic concepts such
as nonces, keys, and publicly known values. We do this by using names, which
are essentially free constants. Here also, we need to track the names which the
attacker knows, such as public values, and the names which the attacker does
not know a priori, such as freshly generated nonces. ñ consists of a finite set of
restricted names; these names represent freshly generated names which remain
secret from the attacker. The set of names occurring in a term t is denoted
by fn(t). For any frame φ = νñ.σ, let fn(φ) be the set of names fn(σ) \ ñ where
fn(σ) = ⋃ t∈Ran(σ) fn(t); and for any term t, let tφ denote—by a slight abuse of
notation—the term tσ. For any term t, we say that t satisfies the name restriction
of φ if fn(t) ∩ ñ = ∅.

**Definition 1 (Deduction).** Let $\phi = \nu\tilde{n}.\sigma$ be a frame, and $t$ a ground term. We say that $t$ is deduced from $\phi$ modulo $E$, denoted by $\phi \vdash_E t$, if there exists a term $\zeta$ such that $\zeta\sigma =_E t$ and $fn(\zeta) \cap \tilde{n} = \emptyset$. The term $\zeta$ is called a *recipe* of $t$ in $\phi$ modulo $E$.
Another form of knowledge is the ability to tell if two frames are statically equivalent modulo E.

**Definition 2 (Static Equivalence).** Two terms s and t are equal in a frame $\phi = \nu\tilde{n}.\sigma$ modulo an equational theory E, denoted ($s =_E t$)$\phi$, if $s\sigma =_E t\sigma$, and $\tilde{n} \cap (fn(s) \cup fn(t)) = \emptyset$. The set of all equalities $s = t$ such that ($s =_E t$)$\phi$ is denoted by Eq($\phi$). Given a set of equalities Eq, the fact that ($s =_E t$)$\phi$ for all $s = t \in Eq$ is denoted by $\phi \models Eq$. Two frames $\phi = \nu\tilde{n}.\sigma$ and $\psi = \nu\tilde{n}.\tau$ are statically equivalent modulo E, denoted as $\phi \cong_E \psi$, if $Dom(\sigma) = Dom(\tau)$, $\phi \models Eq(\psi)$ and $\psi \models Eq(\phi)$.

Deduction and static equivalence are known to be decidable for subterm convergent rewrite systems [1].

## 2.4 Graph-Embedded Rewrite Systems

Let us now introduce the graph-embedded and contracting systems. These systems were introduced in [16] and then simplified in [9], where they are used to expand on the class of subterm convergent term rewrite systems. The idea behind the definitions was to capture the “near subterm” properties of many systems that model the properties of cryptographic protocols. Many systems were close but not fully subterm. That is, the right-hand side of some rules contain terms formed from the symbols and variable on the left but which are not strict subterms.

*Example 1 (Blind Signatures).* For example, the theory of blind signatures [11] is such a theory that is beyond subterm:

$$ 
\begin{align*}
\check{\text{sign}}(\text{sign}(x, y), pk(y)) &\rightarrow x \\
\text{unblind}(\text{blind}(x, y), y) &\rightarrow x \\
\text{unblind}(\text{sign}(\text{blind}(x, y), z), y) &\rightarrow \text{sign}(x, z)
\end{align*}
$$

Consider the rule $\text{unblind}(\text{sign}(\text{blind}(x, y), z), y) \rightarrow \text{sign}(x, z)$. Notice that while $\text{sign}(x, z)$ is not a strict subterm of $\text{unblind}(\text{sign}(\text{blind}(x, y), z), y)$ it can be formed from the function symbols and variables contained in this term.

The expanded definitions allowed these systems to be captured under one single definition. To begin, we need to define the components that will be used in the two definitions, this includes a type of restricted permutation.

**Definition 3 (Leaf and Subterm Permutations).** We define two types of permutations, $\approx_s$ and $\approx_I$:

1. For terms $t$ and $t'$, we say $t$ is subterm permutatively equal to $t'$, denoted $t \approx_s t'$, if one of the following is true:

(a) $t = t'$, where $t$ and $t'$ are constants or variables, or

(b) $t = f(u_1, \dots, u_n)$ and $t' = f(u_{\sigma(1)}, \dots, u_{\sigma(n)})$ where $f$ is an $n$-ary function symbol, $n \ge 1$, and $\sigma$ is a permutation of the indexes $(1, \dots, n)$.
2. For terms $t$ and $t'$, we say $t$ is leaf permutatively equal to $t'$, denoted $t \approx_l t'$, if $t'$ is obtained from $t$ by applying a permutation on the set of leaves (variables and constants) occurring in $t$.

The first type of permutation, $\approx_s$, allows for permutation inside the term but preserves the layer like structure of the function symbols in the term graph. The second type of permutation in the classical leaf permutability and is restricted to the leaf nodes, i.e., just the variables and constants of the term graph. Notice that the two types of permutations, $\approx_s$ and $\approx_l$, do not encompass all permutative theories since $\approx_s$ permutes subterms just below the root while $\approx_l$ permutes just the leaves. We will use a combination of the above two permutations in the definition employed for graph-embedded TRS.

**Definition 4 (Permutatively Equal).** For terms $t$ and $t'$, we say $t$ is permutatively equal to $t'$, denoted $t \approx t'$, if $t \approx_s t'' \approx_l t'$, for some term $t''$.

The class of contracting TRS first starts by modeling the graph minor relation in the TRS setting. This is done by a set of rewrite schemas. This set of rewrite schemata then induces a graph-embedded term rewrite system. Notice that this is very similar to what is often done when considering the homeomorphic embedding relation in TRSs.

**Definition 5 (Graph-Embedding).** Consider the following reduction relation, $\rightarrow_{R_{gemb}}^*$, where $R_{gemb}$ is the set of rules given by the instantiation of the following rule schema:

$$ \left\{ \begin{array}{l} \text{for any } f \in \Sigma \\ \text{(1) } f(x_1, \dots, x_n) \rightarrow x_i \\ \text{(2) } f(x_1, \dots, x_{i-1}, x_i, x_{i+1} \dots, x_n) \rightarrow f(x_1, \dots, x_{i-1}, x_{i+1}, \dots, x_n) \\ \text{and for any } f, g \in \Sigma \\ \text{(3) } f(x_1, \dots, x_{i-1}, g(\tilde{z}), x_{i+1}, \dots, x_m) \rightarrow g(x_1, \dots, x_{i-1}, \tilde{z}, x_{i+1}, \dots, x_m) \\ \text{(4) } f(x_1, \dots, x_{i-1}, g(\tilde{z}), x_{i+1}, \dots, x_m) \rightarrow f(x_1, \dots, x_{i-1}, \tilde{z}, x_{i+1}, \dots, x_m) \end{array} \right\} $$

We say a term $t'$ is graph-embedded in a term $t$, denoted $t \succcurlyeq_{gemb} t'$, if $t'$ is a well formed term such that $t \rightarrow_{R_{gemb}}^* t'$.

A TRS $R$ is graph-embedded if for any $l \rightarrow r \in R$, $l \succcurlyeq_{gemb} r$ or $r$ is a constant.

The graph-embedded class is not sufficient to obtain decidability of static equivalence, so we next need to introduce a type of projection rule that ensure access to subterms and thus decidability of deduction and static equivalence.

**Definition 6 (Projecting Rule).** Let $R$ be a TRS, $x$ a variable and $t$ a term with a single occurrence of $x$. A projecting rule in $R$ over $t$ leading to $x$ is a rule in $R$ which is a variant of $t' \rightarrow x$ where $t'$ is a superterm of $t$ with no additional occurrences of $x$.

Another way to view the projection rules of the above definition is that $t'$ is a context, $t'[ ]$, and there is a rule of the form $t'[t] \rightarrow x$. The way these projecting rules relate to the entire term rewrite system can now be defined.
**Definition 7 (Projection-Closed Derivation).** Let $R$ be a TRS. A non-empty $R_{gemb}$-derivation is said to be projection-closed with respect to $R$ if it has the form

$$s \to_{R_{gemb}}^{l \to r, \gamma} s' \to_{R_{gemb}}^{*} t$$

where

- $s$ is a linear term and $t$ is a well formed term,

- $l \to r$ is a $R_{gemb}$ rule among (1), (2) and (4),

- $\gamma$ is a variable renaming s.t.:

- if $l \to r$ is rule (1), $f(x_1, \dots, x_n) \to x_i$, then for any $x_i\gamma$ occurring in $t$ there exists a projecting rule in $R$ over $f(x_1, \dots, x_n)\gamma$ leading to $x_i\gamma$,

- if $l \to r$ is rule (4),

$$f(x_1, \dots, x_{i-1}, g(\bar{z}), x_{i+1}, \dots, x_m) \to f(x_1, \dots, x_{i-1}, \bar{z}, x_{i+1}, \dots, x_m)$$

then for any $z_i\gamma$ occurring in $t$ there exists a projecting rule in $R$ over $g(\bar{z})\gamma$ leading to $z_i\gamma$,

- $s' \to_{R_{gemb}}^{*} t$ is either projection-closed with respect to $R$ or empty.

**Definition 8 (Projection-Closed Permutative Equality).** Let $R$ be a TRS and $l = r$ a permutative equality obtained by one or zero applications of $\approx_s$ followed by one or zero applications of $\approx_l$. The equality $l = r$ is said to be projection-closed with respect to $R$ if the following holds: for any variable $x$ occurring in a strict subterm $l' \neq x$ of $l$ and in a strict subterm $r'$ of $r$ such that $l' \neq r'$, there exists a projecting rule in $R$ over $l'$ leading to $x$.

Based on Definitions 7 and 8, we can now introduce the subset of graph-embedded rules for which we can obtain decidability of the knowledge problems.

**Definition 9 (Contracting TRS).** A TRS $R$ is said to be contracting if for any non-subterm rule $l \to r$ in $R$ one of the following holds:

- there exist a position $p$ of $l$, a substitution $\sigma$ ranging over variables, a projection-closed derivation $g \to_{R_{gemb}}^+ d$ with respect to $R$ such that $l|_p = g\sigma$ and $r = d\sigma$ is of depth 1,

- $l = r$ is a permutative equality of depth 2 which is projection-closed with respect to $R$.

A contracting TRS, $R$, is strictly contracting if for any $l \to r \in R$, depth($l$) > depth($r$).

**Example 2.** Consider the theory of blind signatures from Example 1. This theory is contracting. Let's look at the rule: unblind(sign(blind($x, y$), $z$), $y$) $\to$ sign($x, z$). Let $l = \text{unblind}(\text{sign}(\text{blind}(x, y), z), y)$.

Then, $l = \text{unblind}(\text{sign}(\text{blind}(x, y), z), y) \to_{R_{gemb}}^{e, \text{rule 1}} \text{sign}(\text{blind}(x, y), z)$. We can start the projection-closed derivation at $l|_1 = \text{sign}(\text{blind}(x, y), z)$. This leads to $\text{sign}(\text{blind}(x, y), z) \to_{R_{gemb}}^{\text{rule 4}} \text{sign}(x, y, z) \to_{R_{gemb}}^{\text{rule 2}} \text{sign}(x, z)$. We also need the required projecting rule, given the above projection-closed derivation.

The step, $\text{sign}(\text{blind}(x, y), z) \to_{R_{gemb}}^{\text{rule 4}} \text{sign}(x, y, z)$, applied rule 4 below the root, to remove the blind() function symbol. Thus, there must be a projecting rule, which is the rule $\text{unblind}(\text{blind}(x, y), y) \to x$.
## 2.5 Restricted Classes of Permutative Theories

Leaf permutative theories are a further restriction on permutative theories where for each axiom, $l = r$, $r$ is a leaf permutation of $l$, i.e., $r = l\sigma$, where $\sigma$ is a permutation of the leaf nodes of $l$. It has already been shown in [9] that deduction is decidable in permutative theories but static equivalence is not [17].

**Definition 10 (Variable-Permuting Theory).** An axiom $l = r$ is said to be variable-permuting [26] if all the following conditions are satisfied:

1. the set of occurrences of $l$ is identical to the set of occurrences of $r$,

2. for any non-variable occurrence $p$ of $l$, $l(p) = r(p)$,

3. for any $x \in \text{Var}(l) \cup \text{Var}(r)$, the number of occurrences of $x$ in $l$ is identical to the number of occurrences of $x$ in $r$.

An equational theory $E$ is said to be separate variable-permuting (SVP, for short) if for any $l = r \in E$ we have:

- $l = r$ is a variable-permuting axiom,

- $l$ and $r$ are rooted by the same function symbol that does not occur elsewhere in $E$.

An inner constructor symbol of $E$ is a function symbol from $E$ that never occurs at the root of any equality in $E$.

**Example 3 (Intruder Theory with a Permutative Axiom).** Let us consider a theory used in practice to model a group messaging protocol [12]. For this protocol, the theory modeling the intruder can be defined [27] as a combination $R \cup K$ where $K = \{\text{keyexch}(x, pk(x'), y, pk(y')) = \text{keyexch}(x', pk(x), y', pk(y))\}$ and

$$R = \left\{ \begin{array}{l} \text{adec}(\text{aenc}(m, pk(sk)), sk) \rightarrow m \ \text{getmsg}(\text{sign}(m, sk)) \rightarrow m \\ \text{checksign}(\text{sign}(m, sk), m, pk(sk)) \rightarrow \text{ok} \ \text{sdec}(\text{senc}(m, k), k) \rightarrow m \end{array} \right\}.$$

$R$ is a subterm convergent TRS and $K$ is a SVP theory such that the shared symbol $pk$ is an inner constructor of $K$ and a constructor of $R$.

An equational theory $E$ is closed by paramodulation if $E$ is a finite set of equalities saturated with respect to the classical paramodulation rule [23]. Thus, an equational theory is saturated by paramodulation when, after exhaustive applications of the paramodulation rule, no further non-redundant equalities.

**Lemma 1.** Any SVP theory is closed by paramodulation.

Critical for the results in this paper is the following from [17].

**Theorem 1 ([17]).** Static equivalence is undecidable in general for variable permuting theories.

**Theorem 2 ([17]).** Both deduction and static equivalence are decidable in any SVP theory.
It has already been shown in [9] that it is possible to combine ≈-free contracting convergent TRS with permutative theories to obtain decidability results for deduction. However, since static equivalence is undecidable in general for even variable permuting theories [17], there was no equivalent result for static equivalence.

**Theorem 3.** Let $R$ be any contracting convergent TRS and $E$ any SVP theory such that the function symbols shared by $R$ and $E$ are constructors for $R$ and inner constructors for $E$. Then, both deduction and static equivalence are decidable in $R \cup E$.

*Proof.* The combination result from [18] can be applied due to Theorem 2. □

Next, we consider going beyond the restriction of only sharing constructors.

## 3 Equational Rewriting Modulo Permutative Theories

In this section we start investigating the possibility to consider $E$ is syntactic permutative, e.g., $E$ is a permutative theory closed by paramodulation, and $R$ is $E$-convergent. In this case, an additional finiteness assumption is required, as shown below. The investigated approach relies on the possibility of computing a finite representation of all the terms that are matched modulo $E$ by the left-hand sides of the TRS $R$.

**Definition 11.** An $E$-variant of a term $l$ is a pair $(t, \sigma)$ such that $t =_E l \sigma$ and $\text{Dom}(\sigma)$ is included in $fv(l)$. Given two $E$-variants $(u, \theta)$ and $(v, \gamma)$ of a term $l$, $(u, \theta)$ is more general than $(v, \gamma)$, denoted by $(u, \theta) \leq_E (v, \gamma)$ if there exists a substitution $\tau$ such that $u\tau =_E v$ and $\theta\tau =_E \gamma$. A complete set of $E$-variants of $l$, denoted by $CV_E(l)$, is a set of $E$-variants of $l$ such that for any $E$-variant $(v, \gamma)$ of $l$, there exists $(u, \theta) \in CV_E(l)$ such that $(u, \theta) \leq_E (v, \gamma)$. The equational theory $E$ is said to have the Finite Equational Variant Property (FEVP, for short) if any term admits a finite complete set of $E$-variants.

Given a syntactic permutative theory $E$, we have developed in [19] a general procedure that, when terminating, computes a finite set of terms $E$-matched by $l$, denoted by $CMT_E(l)$ and such that $\{(t, \sigma) \mid t \in CMT_E(l), l\sigma =_E t\}$ is a finite $CV_E(l)$. This procedure, called MTG is defined as a rule-based system consisting of a matching procedure for syntactic permutative theories plus some additional rules to guide the instantiation of terms to be $E$-matched by $l$, in case the matching procedure fails when the terms are too small. The MTG procedure is not guaranteed to terminate for an arbitrary syntactic permutative theory $E$. However, the MTG procedure is guaranteed to terminate for permutative theories closed under paramodulation which are known to be syntactic [23], and so we have:

**Theorem 4.** Any permutative theory closed by paramodulation has the FEVP.
**Definition 12.** Assume $R$ is TRS such that for any $l \to r \in R$, $CMT_E(l)$ is finite. Under this assumption, the size of $R$ modulo $E$, denoted by $|R|$, is defined as follows: $|R| = \max\{|t| \mid t \in CMT_E(l), l \to r \in R\}$.

From now on, we assume that $E$ is a syntactic permutative theory and $R$ is a contracting $E$-convergent TRS such that $|R|$ is defined. We introduce below some notions defined with respect to $|R|$, such as the completion of a frame and a set of equalities generated by terms bounded by $|R|$.

**Definition 13.** Given a term $t$, $gst_E(t)$ denotes the set of terms $E$-equal to some term in $\bigcup_{\{t' \mid t'=Et\}}$ $gst(t')$, where $gst(t')$ is the set of (well-typed) terms reachable by $R_{gemb}$ from $t'$. For any normalized frame $\phi = \nu\tilde{n.}\sigma$, let $gst_E(\sigma)$ be the set of terms $\bigcup_{x \in Dom(\sigma)}$ $gst_E(x\sigma)$. The set of terms $D_*(\phi)$ is the smallest set $D$ such that:

(1) $Ran(\sigma) \subseteq D$,

(2) if $t_1, \dots, t_n \in D$ and $f(t_1, \dots, t_n) \in gst_E(\sigma)$ then $f(t_1, \dots, t_n) \in D$,

(3) if $t \in D$, $t' \in gst_E(\sigma)$, $t=E$ $t'$, then $t' \in D$,

(4) if there is a root reduction $s[\bar{d}] \to^{\epsilon}_{R,E} t$ where $|s| \le |R|$, $fn(s) \cap \tilde{n} = \emptyset$, $\bar{d} \in D$ and $t \in gst_E(\sigma)$, then $t \in D$.

Let $\sigma_* = \sigma\{\chi_u \mapsto u \mid u \in D_*(\phi)\setminus Ran(\sigma)\}$ where $\chi_u$ is a fresh variable. The frame $\phi_* = \nu\tilde{n.}\sigma_*$ is called the completion of $\phi$ with respect to contexts bounded by $|R|$. Given a recipe $\zeta_u$ for each $u \in D_*(\phi)\setminus Ran(\sigma)$, the substitution $\{\chi_u \mapsto \zeta_u \mid u \in D_*(\phi)\setminus Ran(\sigma)\}$ is called a recipe substitution of $\phi$ and is denoted by $\zeta_\phi$. The set $Eq_\zeta^B(\phi)$ is the set of equalities $t\zeta_\phi = t'\zeta_\phi$ such that $(t\zeta_\phi =_{RE} t'\zeta_\phi)\phi$ and $t, t'$ are terms such that $|t| \le |R|$, $|t'| \le |R|$ and $(fn(t) \cup fn(t')) \cap \tilde{n} = \emptyset$.

In the following, we present reduction methods from $RE = R \cup E$ to the combined theory $\emptyset \cup E$ where $\emptyset$ is the empty theory over the function symbols occurring in $R$ but not in $E$. In the next subsections, this combined theory is simply denoted by $E$.

## 3.1 Deduction

The decision procedure for the deduction problem in $RE$ is based on the following reduction lemma.

**Lemma 2 (Deduction).** Let $RE = R \cup E$ where $E$ is any syntactic permutative theory and $R$ is any contracting $E$-convergent TRS such that $|R|$ is defined. For any normalized frame $\phi$ and any normalized term $t$, we have that $\phi \vdash_{RE} t$ if and only if $\phi_* \vdash_E t$.

## 3.2 Static Equivalence

In a way similar to what is done for disjoint combinations [14], we extend the input frames with the instantiation of recipes of all deducible terms occurring in the completions.
**Definition 14.** Let $\phi = \nu\tilde{n} \cdot \sigma$ be a frame. Let $\Pi$ be a set of terms $t$ such that $t\sigma$ is ground and $t$ satisfies the name restriction of $\phi$. The $\Pi$-extension of $\phi$ is the frame $\Pi\phi = \nu\tilde{n} \cdot \{\chi_t \mapsto t \mid t \in \Pi\}\sigma$.

Given any normalized frames $\phi = \nu\tilde{n} \cdot \sigma$ and $\psi = \nu\tilde{n} \cdot \tau$ such that $\text{Dom}(\sigma) = \text{Dom}(\tau)$, let $\bar{\phi} = (\Pi\phi)_{\downarrow R,E}$, and $\bar{\psi} = (\Pi\psi)_{\downarrow R,E}$ where $\Pi$ is the set of subterms in $\text{Ran}(\zeta_\phi) \cup \text{Ran}(\zeta_\psi)$.

**Lemma 3.** We have $(\bar{\phi})_* = \bar{\phi}$, $(\bar{\psi})_* = \bar{\psi}$ and $\phi \approx_{RE} \psi$ if and only if $\bar{\phi} \approx_{RE} \bar{\psi}$.

The decision procedure for static equivalence in RE is based on the following reduction lemma:

**Lemma 4 (Static Equivalence).** Let $RE = R \cup E$ where $E$ is any syntactic permutative theory and $R$ is any contracting $E$-convergent TRS such that $|R|$ is defined. For any normalized frames $\bar{\phi}$ and $\bar{\psi}$, we have $\bar{\phi} \approx_{RE} \bar{\psi}$ iff $\bar{\psi} \models \text{Eq}^B(\bar{\phi})$ and $\bar{\phi} \models \text{Eq}^B(\bar{\psi})$ and $\bar{\phi} \approx_E \bar{\psi}$.

## 3.3 Decidability Results and Correctness Proofs

According to the above reduction lemmas, we get the following result.

**Theorem 5.** Let $RE = R \cup E$ where $E$ is any syntactic permutative theory and $R$ is any contracting $E$-convergent TRS such that $|R|$ is defined. If both deduction and static equivalence are decidable in $E$, then both deduction and static equivalence are decidable in $RE$.

**Corollary 1.** Let $RE = R \cup E$ where $E$ is any SVP theory and $R$ is any contracting $E$-convergent TRS. Then, both deduction and static equivalence are decidable in $RE$.

The proofs of the reduction lemmas rely on the following technical lemma:

**Lemma 5.** Let $RE = R \cup E$ where $E$ is any syntactic permutative theory and $R$ is any contracting $E$-convergent TRS such that $|R|$ is defined. Assume $\bar{\phi} \approx_E \bar{\psi}$ and $\bar{\psi} \models \text{Eq}^B(\bar{\phi})$. For any term $s$ satisfying the name restriction and for any term $t$ such that $s\bar{\phi} \to_{R,E} t$, there exists a term $u$ satisfying the name restriction such that $t =_E u\bar{\phi}$ and $s\bar{\psi} =_{RE} u\bar{\psi}$.

*Proof.* There are two possibilities.

(i) Let us first assume that the rewrite step occurs at the root position. Suppose $s\bar{\phi} =_E l\mu$ with $l \to r \in R$. For any $x \in fv(l)$, $x\mu$ is possibly a term of the form $t\bar{\phi}$ where $t$ is a subterm of $s$. Consider a constant-abstraction mapping $\pi$ defined as follows: for any maximal subterm $s|_p\bar{\phi}$ occurring in $x\mu$ where $x \in fv(l)$, let $\pi(s|_p\bar{\phi}) = c_p$ where $c_p$ is a fresh free constant. For the term $s'\bar{\phi}$ obtained from $s\bar{\phi}$ by replacing each maximal subterm $s|_p\bar{\phi}$ by the constant $\pi(s|_p\bar{\phi})$, we have that $s'$ is a small context such that $|s'| \le |R|$ and $s'\bar{\phi} \to_{R,E} r\mu$ for $l \to r \in R$. By assumption, $R$ is contracting and so we have $r\mu =_E u'\bar{\phi}$ for some term $u'$. By replacing back the constants introduced by the constant
abstraction, we have $(s'\bar{\phi})\pi^{-1} \to_{R,E} \circ =_E (u'\bar{\phi})\pi^{-1}$, where $(s'\bar{\phi})\pi^{-1} = s\bar{\phi}$ and $(u'\bar{\phi})\pi^{-1} = u\bar{\phi}$ for some term $u$. Consequently, $s\bar{\phi} \to_{R,E} \circ =_E u\bar{\phi}$. By definition of $Eq^B$ and by assumption on $\bar{\psi}$, we have that $s'\bar{\psi} =_{RE} u'\bar{\psi}$. By replacing each constant $\pi(s|_p\bar{\phi})$ with $s|_p\bar{\psi}$, we get $s\bar{\psi} =_{RE} u\bar{\psi}$.

(ii) Let us now assume that the rewrite step occurs below the root position. There exists a position $p \neq \epsilon$ such that $s'\bar{\phi} = (s'\bar{\phi})[s\bar{\phi}]_p$ with $s\bar{\phi} \to_{R,E} \epsilon t$. By the case (i) above, there exists a term $u$ such that $t =_E u\bar{\phi}$ and $s\bar{\psi} =_{RE} u\bar{\psi}$. Then, we have

$$s'\bar{\phi} \to_{R,E} (s'\bar{\phi})[t]_p =_E (s'\bar{\phi})[u\bar{\phi}]_p = (s'[u]_p)\bar{\phi}$$

and

$$s'\bar{\psi} = (s'\bar{\psi})[s\bar{\psi}]_p =_{RE} (s'\bar{\psi})[u\bar{\psi}]_p = (s'[u]_p)\bar{\psi}$$

□

# 4 Undecidability Results

One approach that could be investigated to expand the above results would be to try to weaken the definition of projection-closed equality (Definition 8) so that more permutative theories could be considered in the framework of contracting TRS. However, we show that if we weaken the definition of contracting, Definition 9, by relaxing the type of permutations allowed, we quickly run into undecidability results.

It turns out that while the above restrictions detailed in Definition 9 may be able to be weakened slightly, one still requires restrictions on both the rule applications and the permutations allowed or undecidability results follow. Indeed, we next show that we can consider subsets of the rules from the graph-embedded definition and these subsets still lead to the undecidability of the knowledge problems.

## 4.1 A Weaker Contracting Definition

Let us first consider removing the depth restriction from the definition of contracting TRS (Definition 8). We show that by removing this restriction we run into undecidability. To prove this result we start with a construction developed in [17] showing that a Linear Bounded Automaton's (LBA) transition function can be simulated by a leaf permuting TRS. This in turn is used to show that static equivalence is undecidable in leaf permuting theories. However, the resulting TRS, simulating the LBA, from [17] is permutative but not contracting. The TRS is missing the required projection rules of Definition 8. These rule cannot just be added since they will have overlaps with the existing rules and thus interfere with the LBA simulation. We can however, modify slightly the construction from [17] to prevent these overlaps when adding the required projection rules.
To detail the modification, we first give a brief overview of the construction. Given a LBA $M = (Q, \Sigma, \Gamma, q_0, q_a, q_r, \delta)$, assume $\Sigma = \{a_1, a_2, \dots, a_n\}$ and $\Gamma = \{<, >, \sqcup\} \cup \Sigma$, where `<, >` are the left and right end caps respectively, and `\sqcup` is the blank symbol. Terms can be constructed that simulate the state of the LBA by introducing three function symbols, $f, g, h$ and three constants, $a, b$, and $P$. $h$ is used to represent the state of the LBA. To represent state $q_i$, a constant $b$ is placed at the $i^{th}$ position with the remaining positions containing $a$ constants. There is an extra position in $h$, one more than $|Q|$ and it is used to represent a dummy or default state. $g$ has arity $|\Gamma|$ and is used to encode the alphabet characters. A constant $b$ at position $i$ in $g$ with $a$ constants placed at all other positions to encode $a_i$. $f$ is used to form terms which consist of an encoding of a state, an encoding of a single character, and an $f$-rooted subterm or the constant $P$. The subterm is used to encode the rest of the string. The constant $P$ is used to stop the encoding. For example, suppose you have a state $<q_0, 0>$ of the LBA, $|Q| = 2$, and $\Gamma = \{<, >, 0, \sqcup\}$. Then the term representation of this would be:

$$f(h(b, a, a), g(b, a, a, a), f(h(a, a, b), g(a, a, b, a), f(h(a, a, b), g(a, b, a, a), P)))$$

Then, the left and right moves of the LBA can be simulated by a permutative TRS. For example, if the LBA has a move $\delta(q_0, <) = (q_1, <, R)$ one of the rules for this transition would then be:

$$f(h(b, a, a), g(b, a, a, a), f(h(a, a, b), g(a, a, b, a), x)) \rightarrow \\ f(h(a, a, b), g(b, a, a, a), f(h(a, b, a), g(a, a, b, a), x))$$

Notice that there would be several versions of this rule, since this is the version with the 0 symbol encoded as the next symbol to read, right of $<$. Likewise for a LBA transition $\delta(q_0, >) = (q_1, >, L)$, one of the rules would be:

$$f(h(a, a, b), g(a, a, b, a), f(h(b, a, a), g(a, b, a, a), x)) \rightarrow \\ f(h(a, b, a), g(a, a, b, a), f(h(a, a, b), g(a, a, b, a), x))$$

Now, notice we can't just add projection rules to this TRS. The required projection rule for the above right-move example transition would be:

$$f(h(a, a, b), g(a, a, b, a), x) \rightarrow x$$

However, notice that this overlaps with the above left-move transition.

**Theorem 6.** *Static equivalence is undecidable in general for contracting TRSs without a depth restriction.*

*Proof.* We can fix the above issue with overlapping projection rules by introducing two dummy states instead of one, a left-dummy state, $q_{ld}$, and a right-dummy state, $q_{rd}$. This can be done by increasing the arity of $h$ by one. The second to last position being the left-dummy state and the final position the right dummy-state. Thus if $|Q| = n$, $h$ has arity of $n + 2$. For example, in the above case with $|Q| = 2$, the left-dummy state $q_{ld} = h(a, a, b, a)$ and the right $q_{rd} = h(a, a, a, b)$.
The initial state of the LBA tape has just right-dummy states with the LBA tape head to the left of all the dummy states. Right moves by the LBA change the dummy states, that are now left of the LBA tape head, to left-dummy states. Likewise, left rule moves of the LBA change left-dummy states back to right-dummy states.

We illustrate these modifications with the two rule examples from above. The right moves are now modified as follows:

$$f(h(a, a, a), g(a, a, a), f(h(a, a, a), g(a, a, b), x)) \rightarrow \\ f(h(a, a, b), g(a, a, a), f(h(a, b, a), g(a, a, b), x))$$

The left moves are modified as follows:

$$f(h(a, a, b), g(a, a, b), f(h(b, a, a), g(a, b, a), x)) \rightarrow \\ f(h(a, b, a), g(a, a, b), f(h(a, a, b), g(a, a, b), x))$$

Now when we add the projection rules for right LBA moves we have rules of the form:

$$f(h(a, a, b), g(a, a, b), x) \rightarrow x$$

However, this now doesn't overlap the left move rules of the LBA since they include the subterm for the right-dummy state $h(a, a, a, b)$ instead of the left-dummy that is now included in the projection rules, $h(a, a, b, a)$. The same occurs for the left LBA moves. □

## 4.2 Subset of Graph-Embedded

Next, let us consider subsets of the rules from the graph-embedded definition.

**Definition 15.** A rule-4 graph-embedded term rewrite system is any TRS, R, such that for all $l \rightarrow r \in R$, $l \rightarrow_{R_{gemb}}^+$ r, using only rules (4) and (2) of Definition 5. Denote this set of graph-embedded rules as $R_4$.

Likewise, a rule-3 graph-embedded term rewrite system is any TRS, R, such that for all $l \rightarrow r \in R$, $l \rightarrow_{R_{gemb}}^+$ r, using only rules (3) and (2) of Definition 5.

**Rule-4 Graph-Embedded:** First, we can consider the restricted rule-4 graph-embedded TRSs and use a result previously developed for homeomorphic embedded TRSs.

**Theorem 7.** *Deduction is undecidable in general for rule-4 graph-embedded TRS.*

*Proof.* Assume for each $l \rightarrow r \in R$, for some TRS R, that $l \rightarrow_{R_{emb}}^*$ r, r is homeomorphically embedded in l, and the root symbol of l remains the root symbol for r, $l(\epsilon) = r(\epsilon)$. Then, $l \rightarrow_{R_4}^*$ r. Notice that any homeomorphic rewrite
step below the root can be emulated by several applications of rule (4) and (2). If $t = f(\bar{t}_1, g(x_1, \dots, x_i, \dots, x_n), \bar{t}_2) \to_{R_{qemb}} f(\bar{t}_1, x_i, \bar{t}_2)$ then,

$$ 
\begin{aligned}
t &= f(\bar{t}_1, g(x_1, \dots, x_i, \dots, x_n), \bar{t}_2) \to_{(4)} \\
  & f(\bar{t}_1, x_1, \dots, x_i, \dots, x_n, \bar{t}_2) \to_{(4)}^{n-1} f(\bar{t}_1, x_i, \bar{t}_2).
\end{aligned}
$$

In [9] it is shown that deduction is undecidable in general for homeomorphic embedded TRS. The proof uses a reduction from the Modified Post Correspondence Problem (MPCP). The TRS developed in that reduction was the following:

$$ B = \bigcup_{i=1}^{n} \{ f(\tilde{\alpha}_i(x), g_i(y), \tilde{\beta}_i(z), \text{unlocked}(z)) \to f(x, y, z, \text{unlocked}(z)) \}, $$

$$ U = \{ f(x, y, x, \text{locked}(\text{unlocked}(z))) \to f(x, y, x, \text{unlocked}(z)) \}. $$

Notice that each of these rules is both homeomorphic embedded and root symbol preserving. Thus, each of these rules is also rule-4 graph-embedded. □

**Rule-3 Graph-Embedded:** Next, consider the rule-3 graph-embedded TRSs. For this reduction we will use the Modified Post Correspondence Problem (MPCP) an undecidable version of the well known undecidable Post Correspondence Problem (PCP). Let $\Gamma = \{a, b\}$ be the alphabet of the MPCP problem. Then, an instance of the problem is a finite set of string pairs, $S = \{(\alpha_i, \beta_i) | i \in [1, n]\} \subseteq \Gamma^+ \times \Gamma^+$, and an input string $\alpha_0 \in \Gamma^*$. A solution is a sequence of indexes $i_1, \dots, i_k \in [1, n]$ such that $\alpha_{i_1} \alpha_{i_2} \dots \alpha_{i_k} = \beta_{i_1} \beta_{i_2} \dots \beta_{i_k}$, $\alpha_0$ is a suffix of $\alpha_{i_1} \alpha_{i_2} \dots \alpha_{i_k}$, and $\alpha_0$ is a suffix of $\beta_{i_1} \beta_{i_2} \dots \beta_{i_k}$. That is, there is a string $\alpha' \in \Gamma^*$ s.t. $\alpha_{i_1} \alpha_{i_2} \dots \alpha_{i_k} = \alpha' \cdot \alpha_0 = \beta_{i_1} \beta_{i_2} \dots \beta_{i_k}$. Notice that the standard MPCP is easily reducible to this MPCP by setting $\alpha_0$ to the empty string.

**Theorem 8.** *Deduction is undecidable in general for rule-3 graph-embedded TRS.*

*Proof.* Let $P = \{(\alpha_i, \beta_i) | i \in [1, n]\}$ be an instance of MPCP over the alphabet $\Gamma = \{a, b\}$ with the input string $\alpha_0 \in \Gamma^*$. We can convert this MPCP problem into the TRS setting. First, let $f$ be a binary function symbol and let $a$ and $b$ be constants, and let $d_1, \dots, d_n$, be public constants, one for each string pair of the MPCP. We can convert a string over $\Gamma$ into a term using $f$, $a$ and $b$ in a recursive fashion. For $\gamma \in \Gamma^+$ and $x \in V$, let $\gamma(\widetilde{x})$ denote the term version defines as follows: If $\gamma = a$ (or $b$) then $\gamma(\widetilde{x}) = f(a, x)$ (likewise $\gamma(\widetilde{y}) = f(b, y)$). If $\gamma = a \cdot \gamma'$ then $\gamma(\widetilde{x}) = f(a, \gamma'(\widetilde{x}))$. Let $lck$ (for locked), $ulck$ (for unlocked), and $d$, $d_i$ ($0 \le i \le n$) be public constants. Now, construct a TRS, $R$, as follows: for each pair $\{(\alpha_i, \beta_i) | i \in [1, n]\}$ we create the rule

$$ f(f(f(ulck, v), f(d_i, x)), f(\widetilde{\alpha_i}(y), \widetilde{\beta_i}(z))) \to f(f(f(ulck, v), x), f(y, z)) $$

Add one final “locking” rule to $R$:

$$ f(f(f(ulck, f(lck, v)), f(d_0, x)), f(y, y)) \to f(f(f(ulck, v), x), f(y, y)). $$
The $d_i$ ensure there are no critical pairs between rules and thus we have a convergent TRS. In addition, note that each rule in $R$ can be obtained by using just rule-3 (and rule-2 to remove extra terms). That is, $\forall l \to r \in R, l \to^{+(3),(2)} r$.

Now for the *MPCP* instance, construct the frame $\phi = \nu\tilde{n} \cdot \sigma$ with $\tilde{n} = \{c, e\}$ and $\sigma = \{v \mapsto f(ulck, f(lck, e)), x \mapsto \tilde{\alpha}_0(c)\}$. Likewise, construct a deduction problem with the target term $M = f(f(ulck, e), d), f(c, c)$.

First, suppose there exists a recipe term, $t$, such that $t\sigma \downarrow_R = M$. Then the first rule that must be applied is the unlocking rule, since it is required before any of the other rules can be applied. The unlocking rule also ensures that the two strings are equal. Next, each remaining rewrite step corresponds to a single string pair from the *MPCP*, ensuring the recipe corresponds to a solution. The solution can be extracted from the indexes of each of the $d_i$ constants occurring in the rewrite derivation.

Second, it also easy to see that if there is a solution to the *MPCP* we can from that solution construct a recipe to deduce $M$. For example, if the solution is $i_1, \dots, i_k \in [1, n]$. Then, a recipe would be:

$$t = f(f(v, f(d_0, f(d_{i_1}, f(\dots, f(d_{i_k}, d))))), f(\tilde{\alpha}'(x), \tilde{\beta}'(x)))$$

where $\alpha_{i_1} \alpha_{i_2} \dots \alpha_{i_k} = \alpha' \cdot \alpha_0 = \beta' \cdot \alpha_0 = \beta_{i_1} \beta_{i_2} \dots \beta_{i_k}$

# 5 Conclusions

In this paper, we have extended the combination result from [19], providing decision procedures for the problems of deduction and static equivalence in the combination $R \cup E$, where $R$ is contracting and $E$-convergent. This improves upon the previous result, which required $R$ to be subterm $E$-convergent.

We also examined the gap between two extensions of subterm TRSs, contracting and graph-embedded, with respect to the decidability of knowledge problems. We showed that several natural attempts to narrow this gap while preserving decidability fail, leading to TRSs with undecidable knowledge problems. Nevertheless, it remains plausible that a class of systems closer to graph-embedded than contracting could be defined in a way that maintains decidability. Identifying the best approach to achieve this remains an open question.

Regarding the undecidability proof for deduction in rule-3 TRSs, we note that since the terms involve a single non-constant function symbol, rule-3 behaves similarly to rule-4. It would be interesting to investigate whether this proof could be adapted to avoid relying on the presence of a single function symbol.

# References

1. Abadi, M., Cortier, V.: Deciding knowledge in security protocols under equational theories. Theor. Comput. Sci. 367(1-2), 2-32 (2006)
2. Abadi, M., Fournet, C.: Mobile values, new names, and secure communication. In: Hankin, C., Schmidt, D. (eds.) Conference Record of POPL 2001: The 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, London, UK, 17–19 January 2001, pp. 104–115. ACM (2001)

3. Armando, A., et al.: The AVISPA tool for the automated validation of internet security protocols and applications. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 281–285. Springer, Heidelberg (2005). https://doi.org/10.1007/1151398827

4. Ayala-Rincón, M., Fernández, M., Nantes-Sobrinho, D.: Intruder deduction problem for locally stable theories with normal forms and inverses. Theor. Comput. Sci. 672, 64–100 (2017)

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

6. Baader, F., Snyder, W.: Unification theory. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning, pp. 445–532. Elsevier and MIT Press (2001)

7. Baudet, M., Cortier, V., Delaune, S.: YAPA: a generic tool for computing intruder knowledge. ACM Trans. Comput. Log. 14(1), 4 (2013)

8. Blanchet, B.: An efficient cryptographic protocol verifier based on Prolog rules. In: 14th IEEE Computer Security Foundations Workshop (CSFW-14 2001), Cape Breton, Nova Scotia, Canada, 11–13 June 2001, pp. 82–96. IEEE Computer Society (2001)

9. Bunch, C., Satterfield, S.D., Erbatur, S., Marshall, A.M., Ringeissen, C.: Knowledge problems in protocol analysis: extending the notion of subterm convergent (2025). https://arxiv.org/abs/2401.17226

10. Chadha, R., Cheval, V., Ciobăcă, S., Kremer, S.: Automated verification of equivalence properties of cryptographic protocols. ACM Trans. Comput. Log. 17(4), 23:1–23:32 (2016)

11. Ciobăcă, S., Delaune, S., Kremer, S.: Computing knowledge in security protocols under convergent equational theories. J. Autom. Reasoning 48(2), 219–262 (2012)

12. Cohn-Gordon, K., Cremers, C., Garratt, L., Millican, J., Milner, K.: On ends-to-ends encryption: asynchronous group messaging with strong security guarantees. In: Lie, D., Mannan, M., Backes, M., Wang, X. (eds.) Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security, CCS 2018, Toronto, ON, Canada, 15–19 October 2018, pp. 1802–1819. ACM (2018)

13. Conchinha, B., Basin, D.A., Caleiro, C.: FAST: an efficient decision procedure for deduction and static equivalence. In: Schmidt-Schauß, M. (ed.) Proceedings of RTA 2011, Novi Sad, Serbia. LIPIcs, vol. 10, pp. 11–20. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2011)

14. Cortier, V., Delaune, S.: Decidability and combination results for two notions of knowledge in security protocols. J. Autom. Reasoning 48(4), 441–487 (2010). https://doi.org/10.1007/s10817-010-9208-8

15. Cremers, C.J.F.: The scyther tool: verification, falsification, and analysis of security protocols. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 414–418. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-70545-1_38

16. Dwyer Satterfield, S., Erbatur, S., Marshall, A.M., Ringeissen, C.: Knowledge problems in security protocols: going beyond subterm convergent theories. In: Gaboardi, M., van Raamsdonk, F. (eds.) 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics (LIPIcs), vol. 260, pp. 30:1–30:19. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl, Germany
(2023). https://doi.org/10.4230/LIPIcs.FSCD.2023.30. https://drops.dagstuhl.de/ entities/document/10.4230/LIPIcs.FSCD.2023.30

17. Erbatur, S., Marshall, A.M., Narendran, P., Ringeissen, C.: Deciding knowledge problems modulo classes of permutative theories. In: Bowles, J., Søndergaard, H. (eds.) LOPSTR 2024. LNCS, vol. 14919, pp. 47–63. Springer, Cham (2024). https://doi.org/10.1007/978-3-031-71294-4_3

18. Erbatur, S., Marshall, A.M., Ringeissen, C.: Notions of knowledge in combinations of theories sharing constructors. In: de Moura, L. (ed.) CADE 2017. LNCS (LNAI), vol. 10395, pp. 60–76. Springer, Cham (2017). https://doi.org/10.1007/978-3-319- 63046-5_5

19. Erbatur, S., Marshall, A.M., Ringeissen, C.: Computing knowledge in equational extensions of subterm convergent theories. Math. Struct. Comput. Sci. 30(6), 683–709 (2020)

20. Escobar, S., Meadows, C., Meseguer, J.: Maude-NPA: cryptographic protocol analysis modulo equational properties. In: Aldini, A., Barthe, G., Gorrieri, R. (eds.) FOSAD 2007-2009. LNCS, vol. 5705, pp. 1–50. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-03829-7_1

21. Jouannaud, J., Kirchner, H.: Completion of a set of rules modulo a set of equations. SIAM J. Comput. 15(4), 1155–1194 (1986). https://doi.org/10.1137/0215084

22. Kirchner, C., Klay, F.: Syntactic theories and unification. In: Logic in Computer Science, LICS 1990, Proceedings of the Fifth Annual IEEE Symposium on Logic in Computer Science, pp. 270–277 (1990). https://doi.org/10.1109/LICS.1990.113753

23. Lynch, C., Morawska, B.: Basic syntactic mutation. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol. 2392, pp. 471–485. Springer, Heidelberg (2002). https:// doi.org/10.1007/3-540-45620-1_37

24. Millen, J., Shmatikov, V.: Constraint solving for bounded-process cryptographic protocol analysis. In: Proceedings of the 8th ACM Conference on Computer and Communications Security, CCS 2001, pp. 166–175. ACM, New York (2001). https://doi.org/10.1145/501983.502007

25. Mödersheim, S., Viganò, L.: The open-source fixed-point model checker for symbolic analysis of security protocols. In: Aldini, A., Barthe, G., Gorrieri, R. (eds.) FOSAD 2007-2009. LNCS, vol. 5705, pp. 166–194. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-03829-7_6

26. Narendran, P., Otto, F.: Single versus simultaneous equational unification and equational unification for variable-permuting theories. J. Autom. Reason. 19(1), 87–115 (1997)

27. Nguyen, K.: Formal verification of a messaging protocol. Internship report (2019). Work done under the supervision of Vincent Cheval and Véronique Cortier

28. Paulson, L.C.: The inductive approach to verifying cryptographic protocols. Com- put. Secur. 6, 85–128 (1998)

29. Schmidt, B., Meier, S., Cremers, C.J.F., Basin, D.A.: Automated analysis of Diffie- Hellman protocols and advanced security properties. In: Chong, S. (ed.) 25th IEEE Computer Security Foundations Symposium, CSF 2012, Cambridge, MA, USA, 25–27 June 2012, pp. 78–94. IEEE Computer Society (2012)

30. Turuani, M.: The CL-Atse protocol analyser. In: Pfenning, F. (ed.) RTA 2006. LNCS, vol. 4098, pp. 277–286. Springer, Heidelberg (2006). https://doi.org/10. 1007/11805618_21
**Open Access** This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.

The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.

<figure><img src="image_41.png" /></figure>
# Data-Driven Runtime Complexity Analysis

Samuel Frontull(✉)D, Manuel Meitinger(✉)D, and Georg Moser(✉)D

Department of Computer Science, University of Innsbruck, Innsbruck, Austria
{samuel.frontull,georg.moser}@uibk.ac.at,
manuel.meitinger@student.uibk.ac.at

**Abstract.** We establish a data-driven method for the assessment of the runtime complexity of first-order term rewrite systems (TRSs for short). The fully automated complexity analysis of TRSs has a long tradition in rewriting and numerous sophisticated static analysis methods have been developed. The recent success in machine learning motivates the quest for data-driven analysis techniques, which, while unsound in principle, can potentially return insightful upper bounds on the runtime complexity where traditional (static) techniques fail. We present the first such technique based on bottom-up rule unfolding, akin to a variant of backward narrowing. Further, we employ a dedicated notion of data fitting that is fine-tuned to the estimation of asymptotic complexities. We provide ample experimental data indicating the viability of the approach.

**Keywords:** term rewriting · complexity analysis · automation · machine learning

## 1 Introduction

Term rewriting is a conceptually simple but powerful abstract model of computation that underlies much of declarative programming. In order to assess the complexity of a (terminating) term rewrite system it is natural to look at the maximal length of derivation sequences, as suggested by Hofbauer and Lautemann in [13]. Further, to stay true to the motivation via declarative programming one typically restricts the starting terms to so-called *basic terms*, while often also focusing on *innermost rewriting*. That is, the complexity of a TRS is captured by the notion of (*innermost*) *runtime complexity*, cf. [12] and recent years have shown significant advances in the area, cf. [3, 10, 12, 16, 18, 20, 23, 25, 31]. Here, we restrict ourselves to fully automated methods that focus on the worst-case upper bounds of the runtime complexity of rewrite systems and have given only a handful of references. Similarly, for the fully automated resource analysis of (functional) programs a plethora of techniques have been introduced, for examples see [15] for a comprehensive survey on techniques in the amortised analysis of functional programs alone.

All these analyses are *static* analyses that work fully automatically, that is, the analysis works without user intervention and is based on the “source code”,
<table><caption>**Table 1.** Experimental validation of the data-driven analysis.</caption><thead><tr><th></th><th>#</th><th>unsound (%)</th><th>compl. (%)</th><th>no val.</th><th>unk.</th><th>new (%)</th><th>acc. (%)</th></tr></thead><tbody><tr><td><strong>innermost</strong></td><td>663</td><td>81 (12.2)</td><td>486 (73.3)</td><td>75</td><td>21</td><td>215 (32.4)</td><td>138 (51.3)</td></tr><tr><td><em>poly</em></td><td>536</td><td>16 (3.0)</td><td>460 (85.8)</td><td>46</td><td>14</td><td>215 (40.1)</td><td>112 (62.9)</td></tr><tr><td><em>fp + term.</em></td><td>169</td><td>7 (4.1)</td><td>138 (81.7)</td><td>24</td><td>0</td><td>25 (14.8)</td><td>74 (74.7)</td></tr><tr><td><strong>full</strong></td><td>959</td><td>203 (21.2)</td><td>568 (59.2)</td><td>113</td><td>75</td><td>296 (30.9)</td><td>204 (40.3)</td></tr><tr><td><em>poly</em></td><td>653</td><td>31 (4.7)</td><td>519 (79.5)</td><td>74</td><td>29</td><td>296 (45.3)</td><td>155 (64.9)</td></tr><tr><td><em>fp + term.</em></td><td>111</td><td>7 (6.3)</td><td>80 (72.1)</td><td>24</td><td>0</td><td>27 (24.3)</td><td>39 (75.0)</td></tr></tbody></table>

The benchmark suite is taken from the complexity categories of the *Termi-nation Problem Database (TPDB)*; in particular it indicates the number of (i) *unsound*; (ii) *compliant*; (iii) *new*; and finally (iv) *accurately* predicted examples, respectively. Note that accuracy is defined w.r.t. known results on the (innermost) runtime complexity of TRSs. To indicate the effect of preprocessing of the data we have highlighted the effect of filtering on benchmarks of polynomial complexity ("*poly*") or those that encode (uniformly) terminating functional programs ("*fp + term.*").

the TRS in question. On the other hand, there has been immense progress in machine learning in recent years, motivating a renewed focus on *data-driven techniques*. By design, such an analysis can only be sound *in the limit*, cf. [27]. At most we can hope to prove a soundness result in relation to the number of dynamic samples we have taken from program evaluations that have been used to learn the runtime complexity of the TRS in question.

Based on the sophisticated machine learning methodologies now available, one may hope to quickly yield a powerful (and fast) tool, trading soundness for expressivity. This may be expected to be a simple exercise. Alas, a number of challenges had to be overcome to achieve this. This study is partly motivated by recent work by Pham et al. [26] on the use of data-driven methods in a hybrid amortised resource analysis of functional programs.

More precisely, we make the following contributions: 1) We develop a novel preprocessing method that synthesises *worst-case inputs*. That is, for a given TRS $\mathcal{R}$ we seek out input terms whose derivation height w.r.t. $\mathcal{R}$ is maximally large. These inputs are then used to generate a suitable number of data points for the learner. 2) We define a suitable learning method to predict the runtime complexity of $\mathcal{R}$ in the best possible way. The method is fine-tuned for *adequacy* and *compliance* of the prediction. 3) We prove a statistical soundness theorem, that is, sound "in the limit", cf. Corollary 1. 4) We provide ample experimental evidence for the viability of the method. The overview of the results is given in Table 1. The table details results on the full and innermost runtime complexity. The experimental results are also available online.<fnref n="1" /> We validated the method on

<footnote n="1">¹ See https://www.uibk.ac.at/en/theoretical-computer-science/research/ddrca/, the site also provides an interface to analyse arbitrary TRSs.</footnote>
a significantly sized benchmark suite and compared to earlier results obtained on this benchmark (see Sect. 6 for details). In line with standard terminology, we call our predictions for a TRS $\mathcal{R}$ accurate, if the correct runtime complexity of $\mathcal{R}$ is known and the prediction is optimal. We call the prediction compliant, if it does not violate known lower bounds on the runtime complexity of $\mathcal{R}$.

We emphasise that our method can provide novel results on the runtime complexity of hundreds of TRSs that so far could not be analysed by static techniques. This holds true for full or innermost rewriting, respectively. This is somewhat remarkable, as the benchmark suite represents over a decade of research on fully automated static runtime complexity analyses. As the employed benchmarks are of significant size, the “correct” complexity of the TRS in question is not necessarily known. Thus, our results also provide validation results on the expressivity of the bench-suite itself.

*Related Work.* To the best of our knowledge, this is the first data-driven runtime complexity analysis of rewrite systems. We clarify the connection of our research to related work. Our method of choosing a worst-case input to define suitable data points as prerequisite for the learner is related to techniques that analyse the (worst-case) lower bound of the runtime complexity (see e.g. [9]). The witness term obtained in this context ideally serves as worst-case input. However, in practice the corresponding certificates issued by AProVE [10] or $TCT$ [4] are only partly available, at least in a machine-parse-able format. Unfortunately, these instances are far too rare among the tested dataset, as can also be seen in the full experimental results.<fnref n="2" /> Similarly, fuzzing [8] is a related technique as well. Fuzzing is used to uncover software bugs, by changing the input over and over again in order to reach all possible control flows. However, the fact that the problem set contains arbitrary TRSs with neither a fixed start term nor checkable grammar (e.g. building an array with `::` has meaning and rules in a programming language, in a TRS it is just another function symbol) meant that this method is infeasible, as every possible symbol combination would need to be checked, without any guarantee, that the replacement chain’s result is a value and without taking the cost model into account. Pham et al. [26] establish a hybrid amortised resource analysis of functional programs. The methodology is only partly comparable, as we (i) focus on unrestricted term rewrite systems; (ii) we employ a static technique to single out worst-case input terms, rather than learning the program input distribution, as in [26]; and (iii) we target only asymptotic complexities. Further, we note that our method is more efficient.

*Outline.* In the next section, we provide a high-level overview of the methodology employed. In Sect. 3 we provide basic notions and definitions. Section 4 introduces our synthesis technique for worst-case inputs and also clarifies the challenges entailed by this endeavour for arbitrary (first-order) rewrite systems. Subsequently, in Sect. 5 we detail the learning algorithm and state our statisti-

<footnote n="2">² In principle, we could have tried to adapt the source code of these provers ourselves, but AProVE is not open source and $TCT$ only partly supports lower bound analysis.</footnote>
cal soundness theorem. The setup of the experiments is explained in Sect. 6. We conclude and sketch future work in Sect. 7.

<table><caption>**Table 2.** Motivating examples: Arithmetic functions represented as rewrite systems</caption><tr><td>1: $x-0 \to x$</td><td>1: $x \cdot 0 \to 0$</td></tr><tr><td>2: $s(x)-s(y) \to x-y$</td><td>2: $x \cdot s(y) \to (x \cdot y)+x$</td></tr><tr><td>3: $0 \div s(y) \to 0$</td><td>3: $x+s(y) \to s(x+y)$</td></tr><tr><td>4: $s(x) \div s(y) \to s((x-y) \div s(y))$</td><td>4: $x+0 \to x$</td></tr><tr><td></td><td>5: $0+x \to x$</td></tr><tr><td></td><td>6: $s(x)+y \to s(x+y)$</td></tr></table>

## 2 Overview

In this section, we give a bird's eye view on the contribution, explaining the obtained statistical analysis in a step-by-step fashion on simple motivating examples, cf. Table 2.

Consider the TRS $\mathcal{R}_1$ given to the left of Table 2. Obviously the TRS computes division of two natural numbers, represented as numerals. Further it is not difficult to see that the runtime complexity of $\mathcal{R}_1$ is linear, more precisely the number of rewrite steps to normal-form, starting with term $s^m(0) \div s^n(0)$ can be bounded precisely as $m + m/n + 1$, for $m \ge n$ and $n > 0$. In the literature on automated complexity analysis of TRS, however, one typically focuses on asymptotic bounds. Thus, in the following we will only be concerned with asymptotic bounds. Our approach correctly identifies the optimal linear (asymptotic) bound.

Now, consider TRS $\mathcal{R}_2$ given to the right of Table 2, encoding multiplication and addition, respectively. This amounts to a seemingly natural, although redundant definition. However, the redundancy makes the example no longer orthogonal, while the impredicative nature of the definition of multiplication increases its complexity, cf. [6]. Nevertheless, static analysers like AProVE [10] or TCT [4] can pinpoint its cubic runtime complexity fully automatically. Our approach also derives this optimal runtime complexity in a matter of seconds.<fnref n="3" /> The ambiguity of the examples provides some challenges for the correct preparation of the data points and synthesis of worst-case inputs. (See Sects. 4 and 5 for further details.)

**Example 1.** Reconsider the TRS $\mathcal{R}_1$. The automated analysis of its linear complexity provides some challenges. This is mainly due to the (natural) definition

<footnote n="3">³ Kindly note, however, that the “optimal” cubic upper bound is rather removed from the actual precise multivariate bound of $rc_{\mathcal{R}_2}$. The derivation height of $s^m(0) \cdot s^n(0)$ is precisely bounded by $2n + 1 + \frac{1}{2}m(n^2 + n)$.</footnote>
of division in Rule 4. First, the rule makes the system *duplicating* as the variable *x* appears twice on the right-hand side. Second, the structure of the recursive call in Rule 4 requires not too trivial techniques to upper-bound the runtime complexity fully automatically, cf. [1, 10, 25].

As the (precise) runtime complexity can be easily calculated by hand, it is natural to believe that a stochastic approach should be able to handle the example well. A prerequisite is to generate a sufficient amount of training data as basis for the learner. This data should represent rewrite sequences that are as close as possible to the actual runtime complexity of the TRS $\mathcal{R}$ in question. Thus, we seek to find a set $\{t_i | i \in I\}$ of input (basic) terms of size at most $n$, so that the maximum of $\text{dh}(t_i)_{i \in I}$ is as close as possible to $\text{rc}_{\mathcal{R}}(n)$. We call such terms *worst-case input terms*. Rather than randomly generating terms for that, we aim at a more principled approach, essentially applying a variant of *narrowing* [11] that allows for *backward reasoning*.

*Example 2 (continued from Example 1).* W.r.t. $\mathcal{R}_1$ observe that this TRS is (i) *orthogonal*, that is, there is no overlap between the defining rules of subtraction and division; and (ii) *completely defined*, that is, all evaluations eventually end up in a numeral $s^n(0)$ for some $n \ge 0$ or more generally a *value*, that is built up from constructor symbols. Put differently, $\mathcal{R}_1$ can be conceived as the translation of a first-order functional program for division. Using our algorithm—detailed in Algorithm 1 below— and grouping terms by the size of the first input numeral, worst-case input terms $s^m(0) \div s(0) (m \ge 0)$ are singled out.

This is achieved by differentiating simple rules, essentially the base cases of the definitions, from complex rules, that is, the recursive cases. Employing bottom-up rule unfolding from values and leading up to initial terms, one generates a look-up table of evaluation costs that is used to select the most likely candidates for worst-case inputs. To avoid overlooking costly evaluations this follows a breadth-first search strategy. The simplicity of our running examples obfuscates a number of challenges here. As emphasised, the example is a functional program, normal-forms are values and there is no ambiguity. Subsequently, the bottom-up approach correctly identifies the worst-case inputs. This also works best for an innermost strategy. In general, in particular for full rewriting, neither is a suitable input term easy to identify nor is it certain that the normal-forms of the rewrite system considered are actually values. Due to the inherent complexity of computing the worst-case inputs, the algorithm is computationally demanding and may simply time out. Still, its design principle is led by the assumption that the TRS in question is close to a functional program and ideally the result of a transformation step from a functional program, say in *OCaml*, cf. [2]. Based on the identification of the worst-case inputs, it is straightforward to generate data points that indicate the runtime complexity of the considered rewrite system.

*Example 3 (continued from Example 2).* In Fig. 1 we indicate the original (raw) estimation of the runtime complexity of the running TRS $\mathcal{R}_1$ (on the left-hand side). The raw data cannot be used directly. Rather, we preprocess the data. For
<figure><img src="image_42.png" /><figcaption>Fig. 1. Visualisation of the Runtime Complexity of $\mathcal{R}_1$.</figcaption></figure>

the collection of worst-case inputs $s^m(0) \div s^n(0)$, only the maximum observed derivation heights are retained. Moreover, we apply an iterative filtering process that retains only those data points where the angle between two consecutive points is at least as large as the angle between the previous two points. We refer to the resulting points as the *convex worst-case measurements*. The right-hand side of Fig. 1 shows the convex worst-case measurements obtained from the data points illustrated on the left.

Based on the convex worst-case measurements, we employ empirical techniques to estimate the asymptotic runtime complexity of the TRS. A simple fitting model is not sufficient to achieve good results on adequacy and compliance. The fitting of models to data is usually guided by a loss function that has to be minimised. As any function on a closed interval $[a, b]$ can be approximated arbitrarily well by a polynomial of degree $n$ for $n \to \infty$ (*Weierstrass Approximation Theorem*), attempting to fit the data as well as possible can lead to overly complex models that capture not only the underlying patterns but also the noise, which ultimately reduces the level of compliance. Instead, we follow the *difference rule* heuristic developed by McGeoch et al. [21]. This heuristic estimates the asymptotic complexity bounds by iteratively computing discrete derivatives to empirical data. It is guaranteed to be sound for the considered data points. That is, it provides sound upper bounds on the derivation height of the considered (worst-case) input terms. This implies that our methodology is *statistically sound*, that is sound “in the limit”. The error rate of our prediction falls in relation to the size of test data explored, cf. Corollary 1 below.

*Example 4 (continued from Example 3)*. W.r.t. the running example $\mathcal{R}_1$, the difference rule heuristic yields linear asymptotic complexity for the defined function symbols `-` and `÷`, respectively. Thus, we correctly (and optimally) conclude *linear* runtime complexity of $\mathcal{R}_1$.
# 3 Preliminaries

We briefly review standard notions in machine learning [7, 22, 24, 28] and exemplify them in our context. Consider binary classifications. Then there are four basic combinations between ground truth and prediction: (i) true positive (TP), that is, a property has been classified correctly; (ii) true negative (TN), that is, the absence of a property has been classified correctly; (iii) false positive (FP), that is, an incorrect positive classification; and finally (iv) false negative (FN), that is, an incorrect negative classification. Then the quality of a learner can be succinctly expressed. For example, its accuracy is given as the fraction $TP/(TP + TN)$, while precision indicates the ratio $TP/(TP + FP)$, etc. [22, 28]. These binary classifications are partly generalisable to multi-class classifications. In particular accuracy simply means the fraction of correct classifications over all classifications. For the examples in the TPDB concerned with (full) runtime complexity, the optimal runtime complexity is known for about 31% of the data suite, that is, 506 TRSs. Among these our method correctly predicts the runtime complexity for 204 TRSs. This gives an accuracy of $204/506 = 40.3\%$. Compliance in our context means that the classification of the runtime complexity is sound w.r.t. the known lower bounds in the test suites. Here the expected ground truth is derived from the accumulated knowledge about the TPDB, represented by the results of the so-called Virtual Best Solver in the corresponding competitions.<fnref n="4" /> In order to guarantee comparability with positive results obtained by static solvers, we relate the compliant predictions to the full test suite, rather than—as in the case for adequacy—only to those that have been predicted at all.

*Term Rewriting.* We assume familiarity with term rewriting [5,30] but briefly review basic concepts and notations. Let $\mathcal{V}$ denote a countably infinite set of variables and $\mathcal{F}$ a signature, such that $\mathcal{F}$ contains at least one constant. We write $\mathcal{Var}(t)$ to denote the set of variables occurring in term $t$. A term $t$ is called *linear* if it does not contain multiple occurrences of the same variable. The size $|t|$ of a term is defined as the number of symbols in $t$. We suppose $\mathcal{F} = \mathcal{C} \uplus \mathcal{D}$, where $\mathcal{C}$ denotes a finite, non-empty set of constructor symbols, $\mathcal{D}$ is a finite set of defined function symbols, and $\uplus$ denotes disjoint union. Constructor terms, denoted as $\mathcal{T}(\mathcal{C}, \mathcal{V})$, are usually called *values*. A context is a term containing zero, or multiple occurrences of a hole $\square$. If $\mathcal{C}$ is a context that contains exactly $n$ holes and $t_1, \dots, t_n$ are terms, then $\mathcal{C}[t_1, \dots, t_n]$ denotes the result of replacing the holes in $\mathcal{C}$ from left to right by $t_1, \dots, t_n$. If there is exactly one occurrence of $\square$ in $\mathcal{C}$, then $\mathcal{C}$ is called a one-hole context, also denoted by $\mathcal{C}[\square]$. A *substitution* $\sigma$ is a mapping of variables to terms. Substitutions are conceived as sets of assignments: $\sigma = \{x_1 \mapsto t_1, \dots, x_n \mapsto t_n\}$. We write $\text{dom}(\sigma)$ ($\text{rg}(\sigma)$) to denote the domain (range) of $\sigma$. Let $\sigma, \tau$ be substitutions such that $\text{dom}(\sigma) \cap \text{dom}(\tau) = \emptyset$. Then we denote the (disjoint) union of $\sigma$ and $\tau$ as $\sigma \uplus \tau$. Nodes in (the term tree of) $t$ are called *positions*. $\text{Pos}(t)$ denotes the set of positions in $t$ and

<footnote n="4">⁴ See https://termcomp.github.io/Y2024/.</footnote>
$\mathcal{FPos}(t) = \{p \in \mathcal{Pos}(t) | t(p) \in \mathcal{F}\}$ the set of function positions. A position in $t$ determines both a prefix and a subterm of $t$ namely the prefix with its (only) hole at position $p$, denoted by $t|_p$, and (an occurrence of) the subterm occurring at position $p$, denoted by $t|_p$. If $p$ is a position in $t$, then $t(p)$ denotes the symbol occurring in $t$ at position $p$. If $s\sigma \equiv t\sigma$, then the substitution $\sigma$ is called a unifier for $t$ and $s$. If $t$ and $s$ are unifiable, then there is, again, a most general unifier (mgu), that is, a unifier that is minimal with respect to the ordering $\preceq$ on substitutions.

A *rewrite rule* is a pair $\ell \to r$ of terms such that (i) $\mathrm{root}(\ell)$ is defined, and (ii) $\mathcal{Var}(\ell) \supseteq \mathcal{Var}(r)$, where $\mathrm{root}(\ell)$ is the root symbol of $\ell$. A rule $\ell \to r$ is called *left-linear*, if $\ell$ is linear. A (first-order) term rewrite system over $\mathcal{F}$ is a finite set of rewrite rules. In the sequel, $\mathcal{R}$ always denotes a TRS. The rewrite relation is denoted as $\to_{\mathcal{R}}$ and we use the standard notation for its transitive and reflexive closure. We simply write $\to$ for $\to_{\mathcal{R}}$ if $\mathcal{R}$ is clear from context. Let $s$ and $t$ be terms. If exactly $n$ steps are performed to rewrite $s$ to $t$, we write $s \to^n t$. A term that cannot be reduced further (w.r.t. some TRS $\mathcal{R}$) is called *normal-form*.

*Runtime Complexity Analysis.* We are sometimes only concerned with *innermost rewriting*, that is, an eager evaluation strategy. The *innermost rewrite relation* $\overset{1}{\to}_{\mathcal{R}}$ of a TRS $\mathcal{R}$ is defined on terms as follows: $s \overset{1}{\to}_{\mathcal{R}} t$ if there exists a rewrite rule $\ell \to r \in \mathcal{R}$, a context $C$, and a substitution $\sigma$ such that $s = C[l\sigma]$, $t = C[r\sigma]$, and all proper sub-terms of $l\sigma$ are normal-forms of $\mathcal{R}$.

A TRS is *left-linear* if all rules are left-linear, it is non-overlapping if there are no critical pairs, that is, no ambiguity exists in applying rules. A TRS is *orthogonal* if it is left-linear and non-overlapping. A TRS is *completely defined* if all ground normal-forms are values. Note that an orthogonal TRS is confluent. An orthogonal and completely-defined TRS, we may also simply call a *functional program*.<fnref n="5" /> Let $s$ and $t$ be terms, such that $t$ is in normal-form. Then a *derivation D*: $s \to_{\mathcal{R}}^* t$ with respect to a TRS $\mathcal{R}$ is a finite sequence of rewrite steps. The *derivation height* of a term $s$ with respect to a well-founded, finitely branching relation $\to$ is defined as: $dh(s, \to) = \max\{n \mid \exists t \ s \to^n t\}$. A term $t = f(t_1, \dots, t_k)$ is called *basic* if $f$ is defined, and all $t_i \in T(C, V)$.

We define the (*innermost*) *runtime complexity* (of $\mathcal{R}$). Let $\mathcal{R}$ be a TRS. The *runtime complexity* and the *innermost runtime complexity* of $\mathcal{R}$ are defined as follows. (i) $rc_{\mathcal{R}}(n) := \max\{dh(t, \to_{\mathcal{R}}) \mid t$ is basic and $|t| \le n\}$ and (ii) $irc_{\mathcal{R}}(n) := \max\{dh(t, \overset{1}{\to}_{\mathcal{R}}) \mid t$ is basic and $|t| \le n\}$. In the following we may also refer to the (*innermost*) *runtime complexity* as *cost* thus alluding to the connection of rewrite systems and programs.

# 4 Worst-Case Input Generation

In this section, we delineate how to synthesise worst-case input terms, that is, those input terms $(t_i)_{i \in I}$ that maximise $dh(t_i)_{i \in I}$, for some suitable defined index

<footnote n="5">⁵ It is easy to automatically verify that a TRS is orthogonal. However, for verification of completely definedness we use approximations to define the corresponding benchmark suite.</footnote>
<caption>**Algorithm 1.** Pseudo-code of work list algorithm.</caption>

```pseudo
Require: initialRules
foundRules ← ∅
pendingRules ← initialRules
delayedRules ← ∅

 loop
     while pendingRules ≠ ∅ do
         for all rule ∈ pendingRules do
             foundRules ← foundRules ∪ {rule}
             pendingRules ← pendingRules \ {rule}
             for all derivableRule ∈ computeDerivableRules rule, foundRules) do
                 if derivedRule.isRecursive then
                     delayedRules ← delayedRules ∪ {derivableRule}
                 else
                     pendingRules ← pendingRules ∪ {derivableRule}
             end if
         end for
         end for
     end while
     if delayedRules = ∅ or wallTime > maxTime then return
 else
     steps ← 0
     ▷ Find the longest recursive replacement chains...
     for all rule ∈ delayedRules do
         steps ← max(steps, rule recursiveSteps)
     end for
     for all rule ∈ delayedRules do
         if rule recursiveSteps = steps then
             pendingRules ← pendingRules ∪ {rule}
             delayedRules ← delayedRules \ {rule}
         end if
     end for
     end if
 end loop
```

set *I*. Our method singles out those initial terms that are most likely to yield the longest derivation heights, thus constitute good examples to learn the worst-case runtime complexity. For that we implemented a tool that can find the replacement chain(s) from an input basic term to a normal-form, yielding the highest derivation height (or cost). A replacement chain is a consecutive application of matching term replacement rules. Note that for arbitrary TRSs, there is no explicit *start* term—a *main* function, so to speak—every function occurring in the TRS must be considered an entry point.

We take inspiration from the realm of functional programs, where the normal-form is always a *value*, that is, consists only of constructors and variables, without
any defined function symbols.<fnref n="6" /> Replacement rules returning such a value will be referred to as *simple* rules, rules containing at least one function on the right-hand side as *complex* rules.

A rewrite rule $\ell \to^n r$ is called *simple* if $r$ does not contain any defined function symbol. Otherwise, it is *complex*. Simplifying a complex rule is combining it with a simple rule into another simple rule, or a complex rule with fewer function invocations on the right-hand side. Suppose we have a complex rule $c : \ell_1 \to^a r_1$, a simple rule $s : \ell_2 \to^b r_2$ and a unifier $\mu = \text{mgu}(r_1|_p, \ell_2)$ where $p \in \mathcal{FP}os(r_1)$. Then we define the *simplification* of $c$ with $s$, denoted as $c \lhd s$, as $\ell_1\mu \to^{a+b} r_1[r_2]_p\mu$. To illustrate, consider a function that checks the equality of integers, represented as TRS.

$$ 
\begin{array}{l@{\quad}l@{\quad}l@{\quad}l}
1: & 0 = 0 \to^1 \top & 3: & \mathfrak{s}(x) = 0 \to^1 \bot \\
2: & 0 = \mathfrak{s}(x) \to^1 \bot & 4: & \mathfrak{s}(x_1) = \mathfrak{s}(x_2) \to^1 x_1 = x_2.
\end{array}
$$

Rules 1 to 3 are simple rules, since their right-hand side is a constructor, $\top$ or $\bot$. Rule 4 is complex. Simplifying Rule 4 with, say, Rule 1, the left-hand side of the simple rule needs to match the right-hand side of the complex rule. This can be achieved with the unification $\sigma = \{x_1 \mapsto 0, x_2 \mapsto 0\}$. Thus, the rule resulting from $4 \lhd 1$ is $\mathfrak{s}(0) = \mathfrak{s}(0) \to^2 \top$. Performing this step over and over while keeping track of the number of simplifications, the resulting set of simple rules provides a *lookup table* of program input values (to the left) to their resulting output (to the right), and, more importantly, to the runtime cost (number of replacements). Essentially, this amounts to a *backward reasoning* variant of narrowing, that is, starting from values and leading up to initial terms.

Thus, for simple examples, finding the program's worst execution path for a given input becomes straightforward. (Since in general the lookup table grows exponentially, this method has its limits, though.) There is, however, another challenge that is not apparent in the simple example from before: What to do if there are multiple choices for simplification? Consider the following slightly more complex (but abstract) example.

$$ 
\begin{array}{l@{\quad}l@{\quad}l@{\quad}l}
1: & \text{main}(\llbracket\rrbracket) \to^1 0 & 2: & \text{main}(x :: t) \to^1 \text{costly}(x) + \text{main}(t) \\
3: & \text{costly}(0) \to^1 0 & 4: & \text{costly}(\mathfrak{s}(x)) \to^1 \text{costly}(x) + \text{costly}(x).
\end{array}
$$

A naive strategy would be to first compute $2 \lhd 3$, yielding the complex rule $\text{main}(0 :: t) \to^2 0 + \text{main}(t)$, followed by $(2 \lhd 3) \lhd 1$ to get $\text{main}(0 :: \llbracket\rrbracket) \to^3 0 + 0$. This simple rule can be applied arbitrarily often to simplify Rule 2 again and again, returning

$$ 
\begin{array}{l}
\text{main}(0 :: 0 :: \llbracket\rrbracket) \to^5 0 + 0 + 0, \\
\text{main}(0 :: 0 :: 0 :: \llbracket\rrbracket) \to^7 0 + 0 + 0 + 0, \dots
\end{array}
$$

<footnote n="6">⁶ The special case of functions of arity 0—effectively *constants*—are handled in a preprocessing step that simply replaces any occurrence of the constant's function symbol (LHS) with its value (RHS).</footnote>
never expanding the costly function. To mitigate this issue, the solver performs a breadth-first search strategy, that is, it keeps track of the replacement history of all used simple and complex functions, alongside the replacement cost. It employs a work-list algorithm, where all non-recursive replacements are handled first. New rules resulting in a recursion are placed in a separate secondary list. Once the primary list is finished, the replacement history of all recursive rules in the secondary list is used to compute the number of replacements (steps) since the last recursion. The rules with the largest of those numbers are then moved to the primary work list (cf. Algorithm 1). Using this heuristic prevents the stochastic analyser from being fed data of only one recursion. In other words, ordering recursive rules this way prevents the algorithm from being greedy and allows it to be complete.

**Theorem 1.** For terminating, completely defined TRSs, Algorithm 1 will yield all possible replacement chains up to a fixed length that end in a value term.

*Proof.* By induction on the length $n$ of the replacement chains. (i) Base Case $n=1$: the corresponding simple rule is already present in $\mathcal{R}$ and thus added to the `foundRules` set during the first iteration of the `while` loop. (ii) Step Case: We assume that we found all replacement chains up to length $n$, and show that all rules linking to those will be discovered by the algorithm as well. We split the not-yet-found rules into two categories: recursive and non-recursive. Non-recursive rules are added to the `pendingRules` set, which in turn is enumerated again and its rules are added to the `foundRules` set (first part of the algorithm). Recursive derivable rules—replacement chains invoking the same rule two or more times—are added to the `delayedRules` set, which is then processed in the second part of the algorithm once there are no more `pendingRules` (which must occur since $\mathcal{R}$ is finite). The second part of the algorithm guarantees that at least one rule in `delayedRules` will be moved to `pendingRules`, which in turn is moved to `foundRules`. So to prove that every delayed rule will eventually be placed in `foundRules`, we need to show that it's not possible for it to be skipped in the `recursiveSteps`-based selection indefinitely. This, however, follows by the definition (calculation) of `recursiveSteps`: If a rule is moved from `delayedRules` to `pendingRules`, any further recursive replacement chain found in the `while` loop will have a `recursiveSteps` of 1 regarding that rule. If the recursion is in a different rule, `recursiveSteps` might be higher, but since every further simplification removes at least one function symbol, this is only possible `#(\mathcal{R})` number of times, after which all new derivable rules will be queued after rules with the original `recursiveSteps`. Thus, no recursive rule is kept in the `pendingRules` set forever, and moved to `foundRules` eventually. $\square$

To clarify, the reason for choosing recursive rules with the most steps is not done because of any cost associated with steps—the algorithm is mostly cost-agnostic—its purpose is to find every possible recursive replacement chain. Think of replacement chains as paths through a directed graph, starting at some input term and resulting in a value. The latter is where the algorithm starts, i.e. with all simple rules that return a value. It then enters the aforementioned
two-parted loop, where the first part extends all found paths as far as possible, without resulting in another cycle, but stores information about possible cycles. The second part then proceeds to find the largest cycles that can be formed and adds them to the known paths, repeating the first phase, and so on. This ensures that all replacement chains are found if the algorithm runs to its *natural* end, i.e. when no more simplifications can be performed or found. The run-time is, however, also limited by a user-defined timeout, since a TRS might be too complex or not fulfil the requirements as stated in Theorem 1.

Finally, to get the worst-case input, the analyser must group the input terms for each function by length and use the aforementioned lookup table to find the highest cost. This process can be refined by taking the syntactic meaning of constructors into account, grouping input terms by factors with more semantic meaning—like input array size or input tree height—but for arbitrary TRSs where terms have no semantic connotations, term length is the most general grouping method available, as far as term costs are concerned.

<table><caption>**Table 3.** Example output of Algorithm 1 for the TRS $\mathcal{R}_2$ from Table 2.</caption><tr><td>x·0 →<sup>1</sup> 0</td><td>s(@var<sub>7</sub>) + 0 →<sup>2</sup> s(@var<sub>7</sub>)</td></tr><tr><td>x·s(y) →<sup>1</sup> (x·y)+x</td><td>0+s(@var<sub>6</sub>) →<sup>2</sup> s(@var<sub>6</sub>)</td></tr><tr><td>x+0 →<sup>1</sup> x</td><td>@var<sub>5</sub>+s(0) →<sup>2</sup> s(@var<sub>5</sub>)</td></tr><tr><td>0+x →<sup>1</sup> x</td><td>s(0)·s(@var<sub>2</sub>) →<sup>3</sup> s(s(0)·@var<sub>2</sub>)</td></tr><tr><td>x+s(y) →<sup>1</sup> s(x+y)</td><td>...</td></tr><tr><td>s(x)+y →<sup>1</sup> s(x+y)</td><td>s<sup>4</sup>(0)·s<sup>4</sup>(0) →<sup>19</sup> s<sup>12</sup>(0)+s<sup>4</sup>(0)</td></tr><tr><td>0·s(@var<sub>2</sub>) →<sup>2</sup> 0·@var<sub>2</sub></td><td>s<sup>4</sup>(0)·s<sup>4</sup>(0) →<sup>24</sup> s<sup>16</sup>(0)</td></tr><tr><td>0·s(0) →<sup>3</sup> 0</td><td>s<sup>16</sup>(0)+s<sup>10</sup>(@var<sub>74</sub>) →<sup>27</sup> s<sup>26</sup>(@var<sub>74</sub>)</td></tr><tr><td>s(0)+@var<sub>8</sub> →<sup>2</sup> s(@var<sub>8</sub>)</td><td>...</td></tr></table>

For TRSs resulting from translating a functional program, this approach might not be targeted enough and also wastes time in recursions that generate less cost. Optimising the algorithm for TRS where there is a known main term is part of future work, which is covered in more detail later, when we discuss future work (see Sect. 7). Algorithm 1 shows the pseudocode of the work list algorithm. Figure 3 displays the rules synthesised by this algorithm for TRS $\mathcal{R}_2$. This output is the basis for the data-driven analysis.

# 5 Data-Driven Analysis

In this section we describe the approach we take when analysing the data collected in the worst-case input generation phase to determine the asymptotic
complexity. To do this, we rely on the *difference rule* heuristic proposed in [21]. In contrast to conventional curve fitting methods, which focus on precise fitting to the observed data, this heuristic emphasises compliance by attempting to determine conservative upper bounds while taking into account the inherent limitations of finite data.

We define a *rule-induced measurement* as $\text{meas}(\ell \to^n r) = (\text{root}(\ell), |\ell|, n)$. For instance, consider the rule $s^{16}(0)+s^{10}(\text{var}_{74}) \to^{27} s^{26}(\text{var}_{74})$ (the last rule listed in Fig. 3). For this rule, $\text{root}(\ell) = +$ and $|\ell| = 29$. Thus, the rule-induced measurement is $(+, 29, 27)$. In Fig. 2, we visualise the rule-induced measurements obtained from the rules generated in the worst-case input generation phase of the TRS $\mathcal{R}_2$ from Table 2, where (i) the x-axis represents the term size $|\ell|$; (ii) the y-axis represents the number of steps $n$ needed to rewrite $\ell$ to $r$; and (iii) the colour and marker style of each point distinguishes the different root symbols $\text{root}(\ell)$. The first step in our analysis is to preprocess these measurements, where for each distinct root symbol $\text{root}(\ell)$, we (a) retain only the maximum $n$-value for each distinct $|\ell|$; (b) sort the corresponding measurements in increasing order of $|\ell|$ (we call the resulting list the *worst-case measurements*); and (c) compute the *convex* worst-case measurements that includes the one with the smallest $|\ell|$-value. In (5), we start with the first two measurements in the sorted list and iteratively construct the convex and non-decreasing sequence by checking whether the angle$^7$ of the next candidate point is at least as large as the angle between the last two points in the current subsequence. With this, we obtain for each function a list of $(X, Y)$ data points, where $X$ is a vector of $k$ distinct non-negative values $|l|$ arranged in increasing order. The line segments connecting these consecutive points form a *polyline*.

<figure><img src="image_43.png" /><figcaption>**Fig. 2.** Visualisation of the Runtime Complexity of $\mathcal{R}_2$.</figcaption></figure>

**Theorem 2.** *There is no worst-case measurement above the polyline formed by the convex worst-case measurements.*

<footnote>$^7$ we compute the angle between two-points $p_1 = (x_1, y_1)$ and $p_2 = (x_2, y_2)$ with $\text{angle}(p_1, p_2) = \arctan2(y_2 - y_1, x_2 - x_1)$.</footnote>
**Proof.** Let $s = ((x_0, y_0), (x_1, y_1), \dots, (x_n, y_n))$ be the convex worst-case measurements resulting from the filtering of a set of worst-case measurements $W$. Assume that there exists a measurement point $p_q = (x_q, y_q) \in W$, with $x_0 \le x_q \le x_n$, that is not included in $s$ and above the curve formed by $s$. If $x_q = x_0$, then $p_q$ would have to coincide with the first measurement point and would be included, contradicting our assumption. Therefore, we must have $x_i < x_q \le x_{i+1}$ for some $0 \le i < n$. Let $x_k$ be the largest such $x_i$. Then, we have $x_q \le x_{k+1}$. Let $a_k = \text{angle}(p_{k-1}, p_k)$ and $a_{k+1} = \text{angle}(p_k, p_{k+1})$. By assumption, we would have $a_{k+1} < \text{angle}(p_k, p_q) = a_q$. However, that would also imply $a_k \le a_q$, violating the convexity condition required for exclusion. Hence, $p_q$ would have been included, contradicting our assumption. $\square$

Thus, by Theorem 2, we can guarantee statistical soundness of the data filtering process. We estimate the asymptotic complexity of each function with the *difference rule* heuristic presented in [21].

*Difference Rule.* This heuristic estimates the asymptotic complexity bounds by iterating numerical differentiation to the empirical data. The Newton form of a polynomial $f$ of degree $k$ is expressed as: $P_k(x) = \sum_{n=0}^{k} f[x_0, \dots, x_n] \cdot \prod_{j=0}^{n-1} (x - x_j)$, where $\prod_{j=0}^{-1} (x - x_j) = 1$ and the coefficients $f[x_0, \dots, x_n]$ are the so-called $n$th Newton divided differences, recursively defined as: $f[x_j, \dots, x_n] := \frac{f[x_{j+1}, \dots, x_n] - f[x_j, \dots, x_{n-1}]}{x_n - x_j}$ with $f[x_i] := f(x_i)$. $P_k$ is computed with $k$ interpolation points $(x_0, y_0), \dots, (x_k, y_k)$ and has the property that $P_k(x_i) = y_i = f(x_i)$ for $i \in \{0, \dots, k\}$.

**Theorem 3.** If $f$ is a polynomial of degree $d$, then $f[x_0, \dots, x_k] = 0$ for $k > d$.

*Proof.* This theorem has been proven in [29]. Because of the unique solvability of the interpolating polynomial $P_k$ (Theorem 2.1.1.1 [29]), where $P_k(x_i) = y_i = f(x_i)$ for $k \ge d$, the coefficients for $x^k$ given by $f[x_0, \dots, x_k]$ must vanish for $k > d$. $\square$

This result provides a practical approach to determining the asymptotic complexity by identifying the iteration $i$ at which $f[x_0, \dots, x_i]$ vanishes. To mitigate the effects of noise in empirical data, the heuristic terminates when the correlation of the divided differences falls below a predefined threshold (which we set to 0.005). The number of iterations $i$ directly determines the asymptotic complexity of the function, given by $O(x^i)$.

*Example 5.* The first plot in Fig. 3 visualises the divided difference values computed for the *plus* function from $\mathbb{R}_2$ for $d = 1$, plotted against the corresponding $x$ values. The points exhibit a non-increasing trend, suggesting a linear complexity. For the *times* function, we plot the computed points for $d = 1, 2, 3$, where a non-increasing trend is observed for $d = 3$. This suggests that the asymptotic complexity of the *times* function is cubic.
<figure><img src="image_44.png" /><figcaption>(a) plus, $d=1$</figcaption></figure>

<figure><img src="image_45.png" /><figcaption>(b) times, $d=1$</figcaption></figure>

<figure><img src="image_46.png" /><figcaption>(c) times, $d=2$</figcaption></figure>

<figure><img src="image_47.png" /><figcaption>(d) times, $d=3$</figcaption></figure>

<caption>**Fig. 3.** Divided difference values for the *plus* and the *times* function from $R_2$ plotted against the corresponding *x*-values.</caption>

We determine the asymptotic complexity for all distinct functions in a TRS. The overall asymptotic complexity of the entire TRS is then based on the highest complexity determined for the individual functions.

**Corollary 1.** For completely defined, terminated TRSs the method presented is sound in the limit.

*Proof.* By Theorem 1, we know that for a completely defined, terminating TRS $R$, Algorithm 1 will eventually find all (worst-case) evaluations for each defined function symbol $f$. If the runtime complexity of $f$ is bounded by a polynomial of degree $d$, the filtering process allows the extraction of $k$ convex worst-case measurements. Thus, by Theorem 3, we know that whenever $k > d$, the divided difference heuristic allows to determine the correct degree $d$ on this set of measurements.

Note that the divided difference method can also be exploited to determine polynomials with their corresponding coefficients. However, in our approach, we only use it to determine the degree of the polynomial.

# 6 Experimental Evaluation

We have evaluated the method on a significantly sized benchmark suite from the *Termination Problem Database* (TPDB for short),<fnref n="8" /> a comprehensive repository of problems related to the termination and complexity analysis of rewrite systems. We tested against the results in the corresponding *full* and *innermost runtime complexity* categories of last years’ *Termination and Complexity Competition (TermComp)*.<fnref n="9" /> To verify the level of compliance of our approach, we benchmarked our results against the employed *Virtual Best Solvers (VBS)*, summarising decades of results on static runtime complexity analysis. The results are summarised in Table 1; the full benchmarks and experimental results are available online.<fnref n="10" /> Our experimental results demonstrate the potential of our data-driven approach by revealing 215 (innermost) and 296 (full) new upper bounds

<footnote n="8">⁸ See https://github.com/TermCOMP/TPDB.</footnote>

<footnote n="9">⁹ See https://termcomp.github.io/Y2024/.</footnote>

<footnote n="10">¹⁰ See https://www.uibk.ac.at/en/theoretical-computer-science/research/ddrca/.</footnote>
that were previously unknown. In particular, 166 (innermost) and 243 (full) of
these upper bounds are below exponential complexity. An illustrative example is
raML/queue.raml, whose observed data points are shown in Fig. 4. Static analy-
sis tools have not yet been able to determine an upper bound for this TRS. Using
our method, we were able to determine a quadratic upper bound for the runtime
complexity by analysing the worst-case measurements of startBreadth2, a spe-
cialised instance of the main function. However, naturally there are also cases
where our method is unable to identify worst-case measurements. As a result,
the asymptotic complexity derived from the statistical analysis of this data is
unsound.

<figure><img src="image_48.png" /><figcaption>Fig. 4. Visualisation of the Runtime Complexity of *queue* (selected functions).</figcaption></figure>

7 Conclusion and Future Work

In this paper, we have presented the first data-driven analysis of full and inner-
most runtime complexity of first-order rewrite systems. To make this method
strong in practice, we have combined it with a novel worst-case input genera-
tion method. We have evaluated the method on a significantly sized benchmark
suite from the TPDB and tested it against the *Virtual Best Solvers* for suitable
complexity categories in TermComp. Our method provides new (and compliant)
results for hundreds of tested TRSs.

In future work, we will compare these achievements directly with the data-
driven method mentioned in [26], as well as compare to other analysis methods
for functional programs (e.g. [2, 14, 17, 19]). The idea is to transform a given
functional program by defunctionalisation into a first-order rewrite system and
subsequently employ the techniques studied here. Here we would also strive
for precise upper bounds on the program cost—employing a monotonic cost
model. This is based on a complexity preserving and reflecting transformation of
(potentially) higher-order functional programs to TRSs, established by Avanzini et al. [2]. Knowing the underlying functional program of a TRS can also be used to improve the algorithm's performance of synthesising worst-case inputs (see Sect. 4). Having a specific and single entry point provides the ability of looking at all the terms occurring top-down to improve the choice of performed simplifications bottom-up. The hope here is to drastically decrease the amount of time spent following recursions that do not yield relevant information regarding said main function.

**Acknowledgements.** We would like to thank the anonymous reviewers for their work and invaluable suggestions, which greatly improved our presentation. This work is partly supported by the FWF Project AUTOSARD: "Automated Sublinear Amortised Resource Analysis of Data Structures".

## References

1. Arts, T., Giesl, J.: Termination of term rewriting using dependency pairs. Theor. Comput. Sci. 236(1-2), 133-178 (2000). https://doi.org/10.1016/S0304-3975(99)00207-8

2. Avanzini, M., Lago, U.D., Moser, G.: Analysing the complexity of functional programs: higher-order meets first-order. In: Proceedings of 20th ICFP, pp. 152-164. ACM (2015). https://doi.org/10.1145/2784731.2784753

3. Avanzini, M., Moser, G.: Complexity of Acyclic Term Graph Rewriting. In: Proceedings of 1st FSCD. LIPIcs, vol. 52, pp. 10:1-10:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2016). https://doi.org/10.4230/LIPICS.FSCD.2016.10

4. Avanzini, M., Moser, G., Schaper, M.: TcT: Tyrolean Complexity Tool. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 407-423. Springer, Heidelberg (2016). https://doi.org/10.1007/978-3-662-49674-9_24

5. Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998). https://doi.org/10.1017/CBO9781139172752

6. Bellantoni, S.J., Cook, S.A.: A new recursion-theoretic characterization of the polytime functions. Comput. Complex. 2, 97-110 (1992). https://doi.org/10.1007/BF01201998

7. Bishop, C.: Pattern Recognition and Machine Learning. Information Science and Statistics, Springer, New York (2006). https://doi.org/10.5555/1162264

8. Boehme, M., Cadar, C., Roychoudhury, A.: Fuzzing: Challenges and Reflections. IEEE Softw. 38(3), 79-86 (2021). https://doi.org/10.1109/MS.2020.3016773

9. Frohn, F., Giesl, J., Hensel, J., Aschermann, C., Ströder, T.: Lower bounds for runtime complexity of term rewriting. J. Autom. Reason. 59(1), 121-163 (2017). https://doi.org/10.1007/S10817-016-9397-X

10. Giesl, J., et al.: Analyzing Program Termination and Complexity Automatically with AProVE. J. Autom. Reason. 58(1), 3-31 (2017). https://doi.org/10.1007/S10817-016-9388-Y

11. Hanus, M.: The integration of functions into logic programming: From theory to practice. J. Log. Program. 19(20), 583-628 (1994). https://doi.org/10.1016/0743-1066(94)90034-5
12. Hirokawa, N., Moser, G.: Automated Complexity Analysis Based on the Dependency Pair Method. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 364–379. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-71070-7_32

13. Hofbauer, D., Lautemann, C.: Termination proofs and the length of derivations. In: Dershowitz, N. (ed.) RTA 1989. LNCS, vol. 355, pp. 167–177. Springer, Heidelberg (1989). https://doi.org/10.1007/3-540-51081-8_107

14. Hoffmann, J., Das, A., Weng, S.: Towards automatic resource bound analysis for OCaml. In: Proceedings of 44th POPL, pp. 359–373. ACM (2017). https://doi.org/10.1145/3009837.3009842

15. Hoffmann, J., Jost, S.: Two decades of automatic amortized resource analysis. Math. Struct. Comput. Sci. 32(6), 729–759 (2022). https://doi.org/10.1017/S0960129521000487

16. Hofmann, M., Moser, G.: Amortised Resource Analysis and Typed Polynomial Interpretations. In: Dowek, G. (ed.) RTA 2014. LNCS, vol. 8560, pp. 272–286. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-08918-8_19

17. Hofmann, M., Leutgeb, L., Obwaller, D., Moser, G., Zuleger, F.: Type-based analysis of logarithmic amortised complexity. Math. Struct. Comput. Sci. 32(6), 794–826 (2022). https://doi.org/10.1017/S0960129521000232

18. Hofmann, M., Moser, G.: Multivariate amortised resource analysis for term rewrite systems. In: Proceedings of 13th TLCA. LIPIcs, vol. 38, pp. 241–256. Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015). https://doi.org/10.4230/LIPICS.TLCA.2015.241

19. Leutgeb, L., Moser, G., Zuleger, F.: ATLAS: Automated Amortised Complexity Analysis of Self-adjusting Data Structures. In: Silva, A., Leino, K.R.M. (eds.) CAV 2021. LNCS, vol. 12760, pp. 99–122. Springer, Cham (2021). https://doi.org/10.1007/978-3-030-81688-9_5

20. Lommen, N., Meyer, É., Giesl, J.: Control-Flow Refinement for Complexity Analysis of Probabilistic Programs in KoAT (Short Paper). In: Proceedings of 12th IJCAR. LNCS, vol. 14739, pp. 233–243 (2024). https://doi.org/10.1007/978-3-031-63498-7_14

21. McGeoch, C.C., Cohen, P.R.: How to find big-oh in your data set (and how not to). In: Madigan, D., Smyth, P. (eds.) Proceedings of the Sixth International Workshop on Artificial Intelligence and Statistics. Proceedings of Machine Learning Research, vol. R1, pp. 347–354. PMLR (1997). https://doi.org/10.1007/BFb0052828

22. Mohri, M., Rostamizadeh, A., Talwalkar, A.: Foundations of Machine Learning. Adaptive Computation and Machine Learning series, MIT Press, Cambridge (2012). https://dl.acm.org/doi/10.5555/3360093

23. Moser, G., Schneckenreither, M.: Automated amortised resource analysis for term rewrite systems. Sci. Comput. Program. 185 (2020). https://doi.org/10.1016/J.SCICO.2019.102306

24. Murphy, K.: Machine Learning: A Probabilistic Perspective. Adaptive Computation and Machine Learning series, MIT Press, Cambridge (2012). https://dl.acm.org/doi/book/10.5555/2380985

25. Noschinski, L., Emmes, F., Giesl, J.: Analyzing Innermost Runtime Complexity of Term Rewriting by Dependency Pairs. JAR 51(1), 27–56 (2013). https://doi.org/10.1007/s10817-013-9277-6

26. Pham, L., Saad, F.A., Hoffmann, J.: Robust Resource Bounds with Static Analysis and Bayesian Inference. Proc. ACM Program. Lang. 8(PLDI) (2024). https://doi.org/10.1145/3656380
27. Sanders, P., Fleischer, R.: Asymptotic Complexity from Experiments? A Case Study for Randomized Algorithms. In: Näher, S., Wagner, D. (eds.) WAE 2000. LNCS, vol. 1982, pp. 135–146. Springer, Heidelberg (2001). https://doi.org/10.1007/3-540-44691-5_12

28. Shalev-Shwartz, S., Ben-David, S.: Understanding Machine Learning: From Theory to Algorithms. Cambridge University Press, Cambridge (2014). https://doi.org/10.1017/CBO9781107298019

29. Stoer, J., Bulirsch, R., Bartels, R., Gautschi, W., Witzgall, C.: Introduction to Numerical Analysis, vol. 1993. Springer, Heidelberg (1980). https://doi.org/10.1007/978-0-387-21738-3

30. TeReSe: Term Rewriting Systems, Cambridge Tracks in Theoretical Computer Science, vol. 55. Cambridge University Press, Cambridge (2003). https://doi.org/10.1017/S095679680400526X

31. Winkler, S., Moser, G.: Runtime Complexity Analysis of Logically Constrained Rewriting. In: LOPSTR 2020. LNCS, vol. 12561, pp. 37–55. Springer, Cham (2021). https://doi.org/10.1007/978-3-030-68446-4_2

**Open Access** This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.

The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
<figure><img src="image_49.png" /></figure>

# Difference of Constrained Patterns in Logically Constrained Term Rewrite Systems

Naoki Nishida(✉)D, Misaki Kojima(✉)D, and Yuto Nakamura

Graduate School of Informatics, Nagoya University, Furo-cho,
Chikusa-ku, Nagoya 4648601, Japan
{nishida,kojima}@i.nagoya-u.ac.jp

**Abstract.** Considering patterns as sets of their instances, a difference operator over patterns computes a finite set of two given patterns, which represents the difference between the dividend pattern and the divisor pattern. A complement of a pattern is a pattern set, the ground constructor instances of which comprise the complement of the ground constructor instances of the former pattern. Given finitely many unconstrained linear patterns, using a difference operator over linear patterns, a complement algorithm returns a finite set of linear patterns as a complement of the given patterns. In this paper, we extend the difference operator and complement algorithm to constrained linear patterns used in logically constrained term rewrite systems (LCTRSs, for short) that have no user-defined constructor term with a sort for built-in values. Then, as for left-linear term rewrite systems, using the complement algorithm, we show that quasi-reducibility is decidable for such LCTRSs with decidable built-in theories. For the single use of the difference operator over constrained patterns, only divisor patterns are required to be linear.

**Keywords:** Logically constrained rewriting · Complement · Unification · Quasi-reducibility

## 1 Introduction

*Complements of patterns*—terms rooted by defined symbols with constructor arguments—have been studied in the field of term rewriting due to their various usefulness [12, 15, 27, 28, 39]. A *complement* of a pattern $f(s_1, \dots, s_n)$ is a set $Q$ of patterns, the ground constructor instances of which comprise the complement set of the ground constructor instances of $f(s_1, \dots, s_n)$: $\mathcal{G}_C(Q) = \mathcal{G}_C(f(x_1, \dots, x_n)) \setminus \mathcal{G}_C(f(s_1, \dots, s_n))$, where $x_1, \dots, x_n$ are pairwise distinct variables, $C$ is a set of constructors, $T(C)$ is the set of ground constructor terms, $\mathcal{G}_C(s)$ is the set of ground constructor instances of a term $s$, and $\mathcal{G}_C(Q) = \bigcup_{s \in Q} \mathcal{G}_C(s)$.

<footnote>This work was partially supported by JSPS KAKENHI Grant Number JP24K02900, Grant-in-Aid for JSPS Fellows Grant Number JP24KJ1240, and the Kayamori Foundation of Informational Science Advancement.</footnote>
Given a finite set $P$ of linear patterns, the complement algorithm in [15,28] returns a finite set $\overline{P}$ of linear patterns as a complement of patterns in $P$: $\mathcal{G}_C(\overline{P}) = \mathcal{G}_C(\{f(x_1, \dots, x_n) \mid f \in \mathcal{D}\}) \setminus \mathcal{G}_C(P)$, where $\mathcal{D}$ is a set of considered defined symbols and $x_1, \dots, x_n$ are pairwise distinct variables. Patterns in $P$ are assumed to be pairwise non-overlapping. The algorithm is based on a difference operator $\ominus$ over linear patterns. The difference operator $\ominus$ takes two linear patterns $s, t$ as input and returns a finite set of linear patterns, which represents the difference of the dividend $s$ and the divisor $t$ w.r.t. ground constructor instances: $\mathcal{G}_C(s \ominus t) = \mathcal{G}_C(s) \setminus \mathcal{G}_C(t)$.

The operator $\ominus$ is extended for finite sets of linear patterns: Given finite sets $P, Q$ of linear patterns, $P \ominus Q$ is a finite set of linear patterns such that $\mathcal{G}_C(P \ominus Q) = \mathcal{G}_C(P) \setminus \mathcal{G}_C(Q)$. As an application, the complement algorithm implies decidability of quasi-reducibility<fnref n="1" />—non-existence of irreducible ground patterns—of left-linear TRSs: A left-linear TRS $\mathcal{R}$ is quasi-reducible if and only if $\{f(x_1, \dots, x_n) \mid f \in \mathcal{D}\} \ominus \{\ell \mid \ell \to r \in \mathcal{R}\} = \emptyset$, where $x_1, \dots, x_n$ are pairwise different variables. Quasi-reducibility is often assumed for target rewrite systems in equivalence checking based on rewriting induction [14,34].

Many compilers and interpreters of practical programming languages check the exhaustiveness of function definitions and case-statements. As for left-linear TRSs, algorithms for the exhaustiveness checking have been developed in several formulations (see, e.g., [29]). For patterns without guard conditions, the exhaustiveness (i.e., quasi-reducibility) is decidable [18,40]. On the other hand, to the best of our knowledge, there is no full exhaustiveness checker for languages that allows us to attach guard conditions, which may include user-defined predicates, to patterns. To decide it, we need decidable SMT solving for the combination of all built-in theories that the languages support, which are usually undecidable.

Recently, program verification by means of logically constrained term rewrite systems (LCTRSs, for short) [25] are well investigated [10, 14, 16, 17, 19, 20, 22, 23, 30, 32, 41]. LCTRSs are extensions of term rewrite systems (TRSs, for short) by allowing rewrite rules to have guard constraints which are evaluated under equipped built-in theories. LCTRSs combine classic term rewriting (see, e.g., [3,33]) with built-in data types and constraints from user-specified first-order theories, specifically those supported by modern SMT solvers (cf. [4,5]). This allows for a high expressivity that is useful for representing many programming language constructs directly, together with robust tool support, e.g., the tool Ctrl [26], for automated reasoning. For instance, equivalence checking by means of LCTRSs is useful to ensure the correctness of terminating functions (cf. [14]). Due to these features, LCTRSs are known to be useful computational models of not only functional but also imperative programs.

LCTRS tools [23,26,38] rely on SMT solvers and often consider decidable built-in theories for given LCTRSs. On the other hand, to the best of our knowledge, neither a difference operator nor a complement algorithm has been investigated for constrained patterns, while an SMT-based sufficient condition for

<footnote n="1">¹ Quasi-reducibility is called quasi-reductivity in some papers (e.g., [2,14,24]) and pattern completeness in the context of functional programming [40].</footnote>
left-patternless constrained rewrite systems [23,37]<fnref n="2" /> and procedural sufficient conditions for quasi-reducibility of LCTRSs [24] and conditional constrained TRSs [6] have been shown.

*Example 1.1.* Let us consider the sort set $S_1 = \{\mathit{int}, \mathit{bool}, \mathit{list}\}$, the $S_1$-sorted signature $\Sigma_1 = \{\mathit{n} : \mathit{int} \mid \mathit{n} \in \mathbb{Z}\} \cup \{\mathit{true}, \mathit{false} : \mathit{bool}, \mathit{nil} : \mathit{list}, \mathit{cons} : \mathit{int} \times \mathit{list} \to \mathit{list}, \mathit{f} : \mathit{list} \times \mathit{int} \to \mathit{int}\}$, and the following artificial LCTRS:

$$ \mathcal{R}_1 = \left\{ \begin{array}{ll} (1) & \mathit{f}(\mathit{nil}, y_1) \to 0 \quad [y_1 \le 0], \\ (2) & \mathit{f}(\mathit{cons}(x_2, xs_2), y_2) \to \mathit{f}(xs_2, y_2 - 1) \quad [x_2 \le 0 \land y_2 > 0], \\ (3) & \mathit{f}(\mathit{cons}(x_3, \mathit{cons}(z_3, zs_3)), y_3) \to x_3 + \mathit{f}(zs_3, y_3 - 2) \quad [x_3 > 0 \land y_3 > 1] \end{array} \right\} $$

Complements of unconstrained patterns $\mathit{f}(\mathit{nil}, y_1)$ and $\mathit{f}(\mathit{cons}(x_1, \mathit{nil}), y_1)$ are, e.g., $\{\mathit{f}(\mathit{cons}(x_1, xs_1), y_1)\}$ and $\{\mathit{f}(\mathit{nil}, y_1), \mathit{f}(\mathit{cons}(x_1, \mathit{cons}(z_1, zs_1)), y_1)\}$, respectively. The LCTRS $\mathcal{R}_1$ is not quasi-reducible because none of the following constrained patterns is defined:

$$ (a) \quad \mathit{f}(\mathit{nil}, y_a) \quad [\neg(y_a \le 0)] $$

$$ (b) \quad \mathit{f}(\mathit{cons}(x_b, \mathit{nil}), y_b) \quad [\neg(x_b \le 0 \land y_b > 0)] $$

$$ (c) \quad \mathit{f}(\mathit{cons}(x_c, \mathit{cons}(z_c, zs_c)), y_c) \quad [\neg(x_c \le 0 \land y_c > 0) \land \neg(x_c > 0 \land y_c > 1)] $$

It would be easy to find the first undefined constrained pattern (a) above. On the other hand, the second and third ones (b), (c) above are not so trivial because we have to consider a unified form of the left-hand sides of the second and third rules (2), (3) to compute (b), (c). For this reason, it is not so easy to know that $\mathcal{R}_1$ is not quasi-reducible. Note that the following LCTRS obtained from $\mathcal{R}_1$ by adding rules for the above undefined constrained patterns is quasi-reducible:

$$ \mathcal{R}'_1 = \mathcal{R}_1 \cup \left\{ \begin{array}{ll} (a) & \mathit{f}(\mathit{nil}, y_a) \to 0 \quad [\neg(y_a \le 0)], \\ (b) & \mathit{f}(\mathit{cons}(x_b, \mathit{nil}), y_b) \to 0 \quad [\neg(x_b \le 0 \land y_b > 0)], \\ (c) & \mathit{f}(\mathit{cons}(x_c, \mathit{cons}(z_c, zs_c)), y_c) \to 0 \quad [\neg(x_c \le 0 \land y_c > 0) \land \neg(x_c > 0 \land y_c > 1)] \end{array} \right\} $$

In this paper, we propose a difference operator and a complement algorithm for constrained patterns used in left-linear LCTRSs that have finitely many user-defined function symbols and have no user-defined constructor term with a theory sort for built-in values.<fnref n="3" /> To this end, we extend the difference operator $\ominus$ and the complement algorithm $\overline{\ominus}$ mentioned above to constrained patterns. The extended difference operator and complement algorithm are still computable for constrained patterns over signatures with decidable built-in theories. Then, as an application of the complement algorithm, we show that quasi-reducibility is decidable for the aforementioned LCTRSs with decidable built-in theories. Complete proofs for correctness of the results can be seen in the full version [31].

<footnote n="2">² The sufficient condition for reduction-completeness is applicable to quasi-reducibility.</footnote>

<footnote n="3">³ The latter is equivalent to the condition that all theory sorts are inextensible [13].</footnote>
*Example 1.2 (our goal).* Let us consider the LCTRSs $\mathcal{R}_1$ and $\mathcal{R}'_1$ in Example 1.1 again. Given the constrained patterns $f(x, ys)$ [true] and (1), the extended difference operator $\ominus$ returns $\{f(\text{nil}, y_a) [\neg(y_a \le 0)], f(\text{cons}(x, xs), y) [\text{true}]\}$ as a complement of (1). Given $\{(1), (2), (3)\}$, the extended complement algorithm $\overline{\oplus}$ returns $\{(a), (b), (c)\}$ as a complement of $\{(1), (2), (3)\}$. This implies that $\mathcal{R}_1$ is not quasi-reducible. On the other hand, given $\{(1), (2), (3), (a), (b), (c)\}$, the complement algorithm $\overline{\oplus}$ returns the empty set, and thus $\mathcal{R}'_1$ is quasi-reducible.

In addition to the extension to constrained patterns, we relax the linearity assumption of dividends of $\ominus$ over constrained patterns, i.e., we no longer assume the linearity of dividends, while the linearity is assumed for the extended complement algorithm: For $s[\phi] \ominus t[\psi]$, only the divisor $t$ is assumed to be linear; for $P \ominus Q$, both $P, Q$ are assumed to be sets of constrained linear patterns. The extended operator and complement algorithm behave in the same way as those of unconstrained patterns. Thus, a side effect of the extension to constrained patterns, for the unconstrained case with $s \ominus t$, only $t$ is assumed to be linear.

LCTRSs in this paper are assumed to have no user-defined constructor term with a theory sort. This is not a restriction for program verification by means of LCTRSs because LCTRSs obtained from practical programs by the existing transformations [14, 16, 17, 23] are left-linear systems satisfying the restriction.

The main contributions of this paper are (i) the extension of the difference operator and the complement algorithm to constrained patterns, (ii) the relaxation of the linearity assumption to dividends of $\ominus$ over (constrained) patterns, and (iii) decidability of quasi-reducibility of LCTRSs in the aforementioned class.

## 2 Preliminaries

In this section, we briefly recall LCTRSs [14, 25]. Familiarity with basic notions and notations on term rewriting [3, 33] is assumed.

This paper deals with a first-order $\mathcal{S}$-sorted signature $\Sigma$, where $\mathcal{S}$ is a set of sorts. Let $\Sigma' \subseteq \Sigma$. A term in $T(\Sigma', \mathcal{V})$ is called a $\Sigma'$-term, where $\mathcal{V}$ is a (countably infinite) set of $\mathcal{S}$-sorted variables. A term $t$ is called an instance of a term $t'$ (or $t'$ is called more general than $t$), written as $t \gtrsim t'$, if there exists a substitution $\sigma$ such that $t = t'\sigma$. We write $t > t'$ if $t \gtrsim t'$ but $t' \not\gtrsim t$. The height of a term $t$, written as $\text{height}(t)$, is recursively defined as follows: $\text{height}(t) = 0$ if $t \in \mathcal{V}$; $\text{height}(t) = 1 + \max\{\text{height}(t_1), \dots, \text{height}(t_n)\}$ if $t = f(t_1, \dots, t_n)$ for some $n$-ary function symbol $f$ and terms $t_1, \dots, t_n$ such that $n \ge 0$. Note that the height of $t$ in this paper does not correspond to the height of the corresponding tree of $t$. A position $p$ of a term $t$ is called above (strictly above) a position $q$ of $t$, written as $p \le q$ ($p < q$), if there exists a position $p'$ of $t|_p$ such that $pp' = q$ ($pp' = q$ and $p' \ne \epsilon$). Positions $p, q$ of a term $t$ are called parallel, written as $p \parallel q$, if $p \not\le q$ and $q \not\le p$. A substitution $\sigma$ is called more general than a substitution $\theta$, written as $\sigma \lesssim \theta$, if there exists a substitution $\delta$ such that $\theta = (\delta \circ \sigma)$. For a set $X$ of variables, we call $\sigma$ ground w.r.t. $X$ ($X$-ground, for short) if $\text{Dom}(\sigma) \supseteq X$ and $\mathcal{V}\text{Ran}(\sigma|_X) = \emptyset$, i.e., $x\sigma$ is ground for any variable $x \in X$. A substitution
$\sigma$ which is a sort-preserving mapping from $\mathcal{V}$ to $T(\Sigma, \mathcal{V})$ is said to be a $\Sigma'$-substitution if $\mathcal{Ran}(\sigma) \subseteq T(\Sigma', \mathcal{V})$. A term $s$ is called an instance of $t$ w.r.t. $\Sigma'$ ($\Sigma'$-instance, for short) if there exists a $\Sigma'$-substitution $\sigma$ such that $s = t\sigma$. For a substitution $\sigma$, we write $\sigma = \text{rgu}(s, t)$ if $\sigma$ is an rgu of $s, t$.

To define an LCTRS [14,25] over an $\mathcal{S}$-sorted signature $\Sigma$, we consider the following sorts, signatures, mappings, and constants: *Theory sorts* in $\mathcal{S}_{theory}$ and *term sorts* in $\mathcal{S}_{term}$ such that $\mathcal{S} = \mathcal{S}_{theory} \uplus \mathcal{S}_{term}$; a *theory signature* $\Sigma_{theory}$ and a *term signature* $\Sigma_{terms}$ such that $\Sigma = \Sigma_{theory} \cup \Sigma_{terms}$ and $\iota_1, \dots, \iota_n, \iota \in \mathcal{S}_{theory}$ for any symbol $f : \iota_1 \times \dots \times \iota_n \to \iota \in \Sigma_{theory}$; a mapping $\mathcal{I}$ that assigns to each theory sort $\iota$ a (non-empty) set $\mathcal{A}_\iota$, called the universe of $\iota$ (i.e., $\mathcal{I}(\iota) = \mathcal{A}_\iota$); a mapping $\mathcal{J}$, called an interpretation for $\Sigma_{theory}$, that assigns to each function symbol $f : \iota_1 \times \dots \times \iota_n \to \iota \in \Sigma_{theory}$ a function $f^\mathcal{J}$ in $\mathcal{I}(\iota_1) \times \dots \times \mathcal{I}(\iota_n) \to \mathcal{I}(\iota)$ (i.e., $\mathcal{J}(f) = f^\mathcal{J}$); a set $Val_\iota \subseteq \Sigma_{theory}$ of value-constants $a : \iota$ for each theory sort $\iota$ such that $\mathcal{J}$ gives a bijection from $Val_\iota$ to $\mathcal{I}(\iota)$. We denote $\bigcup_{\iota \in \mathcal{S}_{theory}} Val_\iota$ by $Val$. Note that $Val \subseteq \Sigma_{theory}$. For readability, we may not distinguish $Val_\iota$ and $\mathcal{I}(\iota)$, i.e., for each $v \in Val_\iota$, $v$ and $\mathcal{J}(v)$ may be identified. We require that $\Sigma_{terms} \cap \Sigma_{theory} \subseteq Val$. Symbols in $\Sigma_{theory} \setminus Val$ are calculation symbols, for which we may use infix notation. A term in $T(\Sigma_{theory}, \mathcal{V})$ is called a *theory term*. We recursively define the interpretation $\llbracket \cdot \rrbracket_\mathcal{J}$ of ground theory terms as $\llbracket f(s_1, \dots, s_n) \rrbracket_\mathcal{J} = \mathcal{J}(f)(\llbracket s_1 \rrbracket_\mathcal{J}, \dots, \llbracket s_n \rrbracket_\mathcal{J})$.

We typically choose a theory signature $\mathcal{S}_{theory}$ such that $\mathcal{S}_{theory} \supseteq \mathcal{S}_{core} = \{bool\}$, $Val_{bool} = \{true, false : bool\}$, $\Sigma_{theory} \supseteq \Sigma_{core} = Val_{bool} \cup \{\wedge, \vee, \Rightarrow, \Leftrightarrow : bool \times bool \to bool, \neg : bool \to bool\} \cup \{=, \neq : \iota \times \iota \to bool | \iota \in \mathcal{S}_{theory}\}$, $\mathcal{I}(bool) = \{\top, \bot\}$, and $\mathcal{J}$ interprets these symbols as expected: $\mathcal{J}(true) = \top$ and $\mathcal{J}(false) = \bot$. We omit the sort subscripts $\iota$ from $=\iota$ and $\neq\iota$ if they are clear from the context. A theory term with sort `bool` is called a *constraint*. A substitution $\gamma$ is said to respect a constraint $\phi$ if $x\gamma \in Val$ for all $x \in Var(\phi)$ and $\llbracket \phi\gamma \rrbracket_\mathcal{J} = \top$, where $Var(\phi)$ denotes the set of variables appearing in $\phi$. A constraint $\phi$ is said to be satisfiable if $\llbracket \phi\gamma \rrbracket = \top$ for some substitution $\gamma$ respecting $\phi$.

A constrained rewrite rule is a triple $\ell \to r[\varphi]$ such that $\ell$ and $r$ are terms of the same sort, $\varphi$ is a constraint, and $\ell$ is neither a theory term nor a variable. If $\varphi = \text{true}$, then we may write $\ell \to r$. We define $\mathcal{L}Var(\ell \to r[\varphi])$ as $Var(\varphi) \cup (Var(r) \setminus Var(\ell))$, the set of logical variables in $\ell \to r[\varphi]$ which are variables instantiated with value-constants in rewriting terms. We say that a substitution $\gamma$ respects $\ell \to r[\varphi]$ if $\gamma(x) \in Val$ for all $x \in \mathcal{L}Var(\ell \to r[\varphi])$ and $\llbracket \varphi\gamma \rrbracket_\mathcal{J} = \top$. Regarding the signature of $\mathcal{R}$, we denote the set $\{f(x_1, \dots, x_n) \to y | y = f(x_1, \dots, x_n)\} | f \in \Sigma_{theory} \setminus Val, x_1, \dots, x_n, y$ are pairwise distinct variables} by $\mathcal{R}_{calc}$. The elements of $\mathcal{R}_{calc}$ are called *calculation rules* and we often deal with them as constrained rewrite rules even though their left-hand sides are theory terms. The *rewrite relation* $\to_\mathcal{R}$ is a binary relation over terms, defined as follows: For a term $s$, $s[\ell\gamma]_p \to_\mathcal{R} s[r\gamma]_p$ if and only if $\ell \to r[\varphi] \in \mathcal{R} \cup \mathcal{R}_{calc}$ and $\gamma$ respects $\ell \to r[\varphi]$. A reduction step with $\mathcal{R}_{calc}$ is called a *calculation*. A logically constrained term rewrite system (LCTRS, for short) is defined as an abstract reduction system $(T(\Sigma, \mathcal{V}), \to_\mathcal{R})$, simply denoted by $\mathcal{R}$. An LCTRS is usually given by supplying $\Sigma$, $\mathcal{R}$, and an informal description of $\mathcal{I}$ and $\mathcal{J}$ if these
are not clear from the context. The set of normal forms of $\mathcal{R}$ is denoted by $NF_{\mathcal{R}}$. An LCTRS $\mathcal{R}$ is said to be left-linear if for every rule in $\mathcal{R}$, the left-hand side is linear. Note that $\mathcal{R}_{calc}$ is left-linear.

The integer signature $\Sigma_{int}$ is $\Sigma_{core} \cup \{+, -, \times, \exp, \div, \mod : int \times int \to int\} \cup \{\ge, > : int \times int \to bool\} \cup \mathcal{Val}_{int}$ where $\mathcal{S}_{theory} \supseteq \{int, bool\}$, $\mathcal{Val}_{int} = \{\mathbf{n} \mid n \in \mathbb{Z}\}$, $\mathcal{I}(int) = \mathbb{Z}$, and $\mathcal{J}(\mathbf{n}) = \mathbf{n}$ for any $\mathbf{n} \in \mathbb{Z}$—we use $\mathbf{n}$ (in sans-serif font) as the value-constant for $\mathbf{n} \in \mathbb{Z}$ (in math font). We define $\mathcal{J}$ in a natural way. An LCTRS over a signature $\Sigma$ with $\Sigma_{theory} = \Sigma_{int}$ is called an integer LCTRS.

**Example 2.1.** The term $f(\mathit{cons}(1, \mathit{cons}(2, \mathit{cons}(0, \mathit{cons}(3, \mathit{cons}(4, \mathit{nil}))))$, 5) is reduced by the LCTRS $\mathcal{R}_1$ in Example 1.1 to 4 as follows: $f(\mathit{cons}(1, \mathit{cons}(2, \mathit{cons}(0, \mathit{cons}(3, \mathit{cons}(4, \mathit{nil}))))$, 5) $\to_{\mathcal{R}_1}$ $1 + f(\mathit{cons}(0, \mathit{cons}(3, \mathit{cons}(4, \mathit{nil})))$, 5 - 2) $\to_{\mathcal{R}_1}$ $1 + f(\mathit{cons}(0, \mathit{cons}(3, \mathit{cons}(4, \mathit{nil})))$, 3) $\to_{\mathcal{R}_1}$ $1 + f(\mathit{cons}(3, \mathit{cons}(4, \mathit{nil})))$, 3 - 1) $\to_{\mathcal{R}_1}^*$ 4.

A function symbol $f$ is called a *defined symbol of* $\mathcal{R}$ if there exists a rule $f(\ell_1, \dots, \ell_n) \to r[\varphi] \in \mathcal{R} \cup \mathcal{R}_{calc}$; non-defined elements of $\Sigma$ are called *constructors of* $\mathcal{R}$. Note that all value-constants are constructors of $\mathcal{R}$. We denote the sets of defined symbols and constructors of $\mathcal{R}$ by $\mathcal{D}_{\mathcal{R}}$ and $\mathcal{C}_{\mathcal{R}}$, respectively: $\mathcal{D}_{\mathcal{R}} = \{f \mid f(\dots) \to r[\varphi] \in \mathcal{R} \cup \mathcal{R}_{calc}\}$ and $\mathcal{C}_{\mathcal{R}} = \Sigma \setminus \mathcal{D}_{\mathcal{R}}$. A $\mathcal{C}_{\mathcal{R}}$-term is called a *constructor term of* $\mathcal{R}$. A term of the form $f(t_1, \dots, t_n)$ with $f \in \mathcal{D}_{\mathcal{R}}$ and $t_1, \dots, t_n \in T(\mathcal{C}_{\mathcal{R}}, \mathcal{V})$ is called a *pattern* (or *basic*) (of $\mathcal{R}$). We call $\mathcal{R}$ a *construction system* if the left-hand side of each rule $\ell \to r[\varphi] \in \mathcal{R}$ is a pattern. An LCTRS $\mathcal{R}$ is called *quasi-reducible* if every ground pattern is a redex of $\mathcal{R}$.

**Example 2.2.** The LCTRSs $\mathcal{R}_1$ and $\mathcal{R}'_1$ in Example 1.1 are left-linear constructor integer LCTRSs, $\mathcal{R}_1$ is not quasi-reducible, and $\mathcal{R}'_1$ is quasi-reducible.

In the rest of the paper, for a signature $\Sigma$, we are interested in defined symbols and constructors without an LCTRS $\mathcal{R}$ which splits $\Sigma$ to $\mathcal{D}_{\mathcal{R}}$ and $\mathcal{C}_{\mathcal{R}}$. For this reason, without specifying $\mathcal{R}$, we often split a signature $\Sigma$ to the sets $\mathcal{D}, \mathcal{C}$ of defined symbols and constructors, respectively: $\Sigma = \mathcal{D} \uplus \mathcal{C}$.

Finally, we define constrained patterns and their instances.

**Definition 2.3 (constrained term [14,24,25]).** A constrained term over $\Sigma$ is a pair $t[\psi]$ of a term $t: \iota$ and a constraint $\psi$. The sort of $t[\psi]$ is $\iota$. A constrained term $t[\psi]$ is called linear if $t$ is linear; $t[\psi]$ is called linear w.r.t. logical variables (LV-linear, for short) if $t$ is linear w.r.t. $\mathcal{Var}(\psi)$; $t[\psi]$ is called value-free if $t \in T(\Sigma \setminus \mathcal{Var}, \mathcal{V})$; $t[\psi]$ is called a constrained pattern if $t$ is a pattern.

**Definition 2.4 (ground instances $\mathcal{G}_C(t[\psi])$).** Let $t[\psi]$ be a constrained term. We denote the set of all ground $C$-instances of $t[\psi]$ by $\mathcal{G}_C(t[\psi]): \mathcal{G}_C(t[\psi]) = \{t\sigma \mid \sigma$ is a $\mathcal{Var}(t)$-ground $C$-substitution respecting $\psi\}$. We extend $\mathcal{G}_C(\cdot)$ for sets of constrained terms: $\mathcal{G}_C(P) = \bigcup_{t[\psi] \in P} \mathcal{G}_C(t[\psi])$. The set of ground $C$-instances of an unconstrained term $s$ is denoted by $\mathcal{G}_C(s): \mathcal{G}_C(s) = \mathcal{G}_C(s[\text{true}])$.
*Convention (Convention on Term Equivalence).* From the perspective that a (constrained) pattern represents the set of its ground instances, we consider a renamed variant $t'[\psi']$ of a constrained term $t[\psi]$ to be identical with $t[\psi]$, while we require $\psi'$ to be semantically equivalent to $\psi$. To distinguish such equivalence from the usual one, we write $t[\psi] \doteq t'[\psi']$: $t[\psi] \doteq t'[\psi']$ if and only if there exists a renaming $\delta$ such that $t = t'\delta$, $\mathcal{V}ar(t) \cap \mathcal{V}ar(\psi) = \mathcal{V}ar(t'\delta) \cap \mathcal{V}ar(\psi'\delta)$, and $((\exists \vec{x}. \psi) \Leftrightarrow (\exists \vec{y}. \psi'\delta))$ is valid, where $\{\vec{x}\} = \mathcal{V}ar(\psi) \setminus \mathcal{V}ar(t)$ and $\{\vec{y}\} = \mathcal{V}ar(\psi'\delta) \setminus \mathcal{V}ar(t'\delta)$. The equivalence is also used for unconstrained terms: $t \doteq t'$ if and only if $t[\text{true}] \doteq t'[\text{true}]$. Given a set $P$ of constrained terms, $\dot{P}$ denote a minimal set that contains exactly one representative for each equivalence class of constrained terms in $P$. In computing the union of sets of constrained terms, we use the equivalence $\doteq$. To be more precise, we define the union of (constrained) term sets w.r.t. $\doteq$ as follows: $P \dot{\cup} Q := \dot{U}$, where $U = P \cup Q$. The disjoint union $\uplus$ w.r.t. $\doteq$ is defined as follows: Given sets $P, Q, U$ of constrained terms, $P \uplus Q = P \dot{\cup} Q$ if and only if both of the following statements hold: (i) for any constrained term $s[\phi] \in P$, there exists no constrained term $t[\psi]$ in $Q$ such that $s[\phi] \doteq t[\psi]$, and (ii) for any constrained term $t[\psi] \in Q$, there exists no constrained term $s[\phi]$ in $P$ such that $s[\phi] \doteq t[\psi]$. We analogously define $\dot{\cup}, \dot{\uplus}$ for unconstrained terms. We abuse $\cup$ and $\uplus$ for $\dot{\cup}$ and $\dot{\uplus}$, respectively.

### 3 Complements of Constructor Terms and Substitutions

In this section, we define complements of constructor terms and constructor substitutions and then recall the operations in [15, 27, 28] to compute finite complements of linear constructor terms and constructor substitutions. In the rest of the paper, we consider a signature $\Sigma = \mathcal{D} \uplus \mathcal{C}$ without notice. For examples in this section, we use a subsignature $\Sigma'_1 = \mathcal{D}_1 \cup \mathcal{C}'_1$ of $\Sigma_1$, where $\mathcal{D}_1 = \{\text{f}\}$ and $\mathcal{C}'_1 = \{\text{nil, cons, 0, 1}\}$.

We first define complements of $\mathcal{C}$-terms, $\mathcal{C}$-substitutions, and patterns.

**Definition 3.1 (complement).** A set $P$ of $\mathcal{C}$-terms is called a complement of a $\mathcal{C}$-term $u : \iota$ if $\mathcal{G}_C(P) = \{t \in T(\mathcal{C}) \mid t : \iota\} \setminus \mathcal{G}_C(u)$. A set $\Theta$ of $\mathcal{C}$-substitutions is called a complement of a $\mathcal{C}$-substitution $\sigma$ w.r.t. a term $t \in T(\Sigma, \mathcal{V})$ if $\mathcal{G}_C(\{t\rho \mid \rho \in \Theta, t\sigma \neq t\rho\}) = \mathcal{G}_C(t) \setminus \mathcal{G}_C(t\sigma)$. A set $P$ of patterns is called a complement of a pattern $f(s_1, \dots, s_n)$ if $\mathcal{G}_C(P) = \mathcal{G}_C(f(s_1, \dots, x_n)) \setminus \mathcal{G}_C(f(s_1, \dots, s_n))$, where $x_1, \dots, x_n$ are pairwise distinct variables. A set $P$ of patterns is called a complement of a set $Q$ of patterns if $\mathcal{G}_C(P) = \mathcal{G}_C(\{f(x_1, \dots, x_n) \mid f \in \mathcal{D}\}) \setminus \mathcal{G}_C(Q)$, where $x_1, \dots, x_n$ are pairwise distinct variables.

Note that complements are not unique in general. Note also that complements of variables and the identity substitution are the empty set.

*Example 3.2.* The set $\{\text{nil, cons}(x, \text{cons}(x', xs))\}$ is a complement of $\text{cons}(y, \text{nil})$. The set $\{\{xs \mapsto \text{nil}, y \mapsto 1\}, \{xs \mapsto \text{cons}(x', xs'), y \mapsto 0\}, \{xs \mapsto \text{cons}(x', xs'), y \mapsto 1\}\}$ is a complement of $\{xs \mapsto \text{nil}, y \mapsto 0\}$ w.r.t. $f(xs, y)$. The set $\{f(\text{nil}, 1), f(\text{cons}(x', xs'), y)\}$ is a complement of $f(\text{nil}, 0)$.
Next, we recall the constructions of complements of linear C-terms and C-substitutions. We follow the formulation in [15].

For a term $u$, if $\mathcal{G}_C(u)$ is infinite, then the linearity of $u$ w.r.t. variables with sorts for inductively defined terms such as *list* in Example 1.1 is necessary for finiteness of a complement of $u$ (cf. [27, Proposition 4.5]). For this reason, in computing complements of C-terms, we only consider linear terms.

**Definition 3.3** ($\bar{u}$ of linear C-term $u$ [15]). For a linear C-term $u$, we define a set $\bar{u}$ of terms recursively as follows: $\bar{x} = \emptyset$ for a variable $x \in V$, and $c(\bar{u}_1, \dots, \bar{u}_n) = \{c'(x_1, \dots, x_m) \mid c' \neq c, c' : \iota'_1 \times \dots \times \iota'_m \to \iota \in C\} \cup \bigcup_{i=1}^n \{c(u_1, \dots, u_{i-1}, u'_i, y_{i+1}, \dots, y_n) \mid u'_i \in \bar{u}_i\}$, where $c : \iota_1 \times \dots \times \iota_n \to \iota \in C$, $x_1, \dots, x_m$ are pairwise distinct variables, and $y_{i+1}, \dots, y_n$ are pairwise distinct fresh variables for any $i \in \{1, \dots, n\}$.

For a linear term $u : \iota, \bar{u}$ is a finite complement of $u$ (i.e., $\mathcal{G}_C(\bar{u}) = \{t \in T(C) \mid t : \iota\} \setminus \mathcal{G}_C(u)$), which is a set of linear C-terms.

*Example 3.4.* For $C'_1 = \{\text{nil}, \text{cons}, 0, 1\}$, we have that $\bar{0} = \{1\}$, $\bar{1} = \{0\}$, $\bar{\text{nil}} = \{\text{cons}(x, xs)\}$, and $\text{cons}(0, \text{cons}(z_3, zs_3)) = \{\text{nil}, \text{cons}(1, ys), \text{cons}(0, \text{nil})\}$.

The construction below for C-substitutions is based on the construction $\bar{\cdot}$ for linear C-terms, and thus it works on linear substitutions. A substitution $\sigma$ is called linear w.r.t. $X \subseteq V$ ($X$-linear, for short) if $x\sigma$ is linear for any variable $x \in X$. A $V$-linear substitution is simply called linear.

**Definition 3.5** ($\bar{\sigma}$ of linear C-substitution $\sigma$ [15]). Let $\sigma$ be a linear C-substitution. We define a set $\bar{\sigma}$ of substitutions as follows: $\bar{\sigma} = \{\rho \mid \text{Dom}(\rho) = \text{Dom}(\sigma), \rho \neq \sigma, \forall x \in \text{Dom}(\sigma). x\rho \in \bar{x\sigma} \cup \{x\sigma\}\}$.

For a linear C-substitution $\sigma$ and a linear C-term $t$, $\{\rho \mid \rho \in \bar{\sigma}, t\rho \neq t\sigma\}$ is a finite complement of $\sigma$ w.r.t. $t$ (i.e., $\mathcal{G}_C(\{t\rho \mid \rho \in \bar{\sigma}, t\rho \neq t\sigma\}) = \mathcal{G}_C(t) \setminus \mathcal{G}_C(t\sigma)$), which is a finite set of linear C-substitutions.

*Example 3.6.* For $C'_1 = \{\text{nil}, \text{cons}, 0, 1\}$, we have that $\{xs \mapsto \text{nil}, y \mapsto 0\} = \{\{xs \mapsto \text{nil}, y \mapsto 1\}, \{xs \mapsto \text{cons}(x', xs'), y \mapsto 0\}, \{xs \mapsto \text{cons}(x', xs'), y \mapsto 1\}\}$.

# 4 Difference of Constrained Patterns

In this section, we extend the difference operator $\ominus$ over unconstrained linear patterns [15,27,28] to constrained ones. Unlike [15,27,28], we do not require dividend patterns to be linear, while we still require divisor ones to be linear.

## 4.1 Difference Operator for Unconstrained Linear Patterns

We briefly recall the difference operator $\ominus$ over unconstrained linear patterns.

For unifiable patterns $s, t$ with their mgu $\sigma$ and without any common variables, the idea of $\ominus$ is based on the following property:

$$ \mathcal{G}_C(s) = \mathcal{G}_C(s\sigma) \uplus \mathcal{G}_C(\{s\rho \mid \rho \in \bar{\sigma}, s\rho \neq s\sigma\}) $$
Since $s\sigma = t\sigma$ and $\mathcal{G}_C(s) \cap \mathcal{G}_C(t) = \mathcal{G}_C(t\sigma)$, the above property implies that $\mathcal{G}_C(s) \setminus \mathcal{G}_C(t) = \mathcal{G}_C(\{s\rho \mid \rho \in \bar{\sigma}, s\rho \neq s\sigma\})$ and thus $\{s\rho \mid \rho \in \bar{\sigma}, s\rho \neq s\sigma\}$ is a complement of $s$. To compute $\bar{\sigma}$, the mgu $\sigma$ has to be a $C$-substitution. By definition, it is clear that any mgu of patterns are $C$-substitutions. We define the difference operator $\ominus$ for linear patterns as follows.

**Definition 4.1 (Over linear patterns [15]).** We define the difference operator $\ominus$ over linear patterns as follows: $s \ominus t = \{s\rho \mid \rho \in \bar{\sigma}, s\rho \neq s\sigma\}$ if $s, t'$ are unifiable, where $t' \doteq t$, $\mathcal{V}ar(s) \cap \mathcal{V}ar(t') = \emptyset$, and $\sigma = \text{mgu}(s, t')$; otherwise, $s \ominus t = \{s\}$. Note that $s \ominus s = \emptyset$.

To compute $s \ominus t$, $s$ does not have to be linear, while $\sigma|_{\mathcal{V}ar(s)}$ must be linear. A sufficient condition for $\sigma|_{\mathcal{V}ar(s)}$ being linear is linearity of $t'$ (i.e., $t$).

**Proposition 4.2.** Let $s, t$ be unifiable terms with $\mathcal{V}ar(s) \cap \mathcal{V}ar(t) = \emptyset$, and $\sigma$ be an mgu of $s, t$. If $t$ is linear, then $\sigma|_{\mathcal{V}ar(s)}$ is linear.

*Proof (Sketch).* We generalize this claim to unification problems of the form $\{u_1 =? u'_1, \dots, u_k =? u'_k\}$ and use the unification procedure in [3, Section 4.6]. To distinguish variables in $s$ and $t$, we do not swap both sides of $=?$ and prepare the **Eliminate** rule for both sides of $=?$. Then, we show that the initial unification problem $\{s =? t\}$ can be transformed into an extended solved form $\{x_1 =? t_1, \dots, x_n =? t_n, s_1 =? y_1, \dots, s_m =? y_m\}$ such that $x_1, \dots, x_n$ are pairwise distinct variables in $s$, $y_1, \dots, y_m$ are pairwise distinct variables in $t$, none of $s_1, \dots, s_m$ is a variable, $\{x_1, \dots, x_n, y_1, \dots, y_m\} \cap \mathcal{V}ar(t_1, \dots, t_n, s_1, \dots, s_m) = \emptyset$, and $t_i$ is linear for all $1 \le i \le n$. A complete proof can be seen in [31]. $\square$

For a pattern $s$ and a linear pattern $t$, $s \ominus t$ is a finite complement of patterns with sort $\iota$ w.r.t. ground $C$-instances of $s$ (i.e., $\mathcal{G}_C(s \ominus t) = \mathcal{G}_C(s) \setminus \mathcal{G}_C(t)$).

**Example 4.3.** For $\Sigma'_1 = \{\text{f}, \text{nil}, \text{cons}, 0, 1\}$, we have that $\text{f}(xs, y) \ominus \text{f}(\text{nil}, 0) = \{\text{f}(\text{nil}, 1), \text{f}(\text{cons}(x', xs'), 0), \text{f}(\text{cons}(x', xs'), 1)\}$.

## 4.2 Extension of Difference Operator to Constrained Patterns

In the definition of $\ominus$ for unconstrained patterns, for $s \ominus t$, unifiability of $s$ and $t$ is used. Thus, for the extension, we define unifiability of constrained terms.

**Definition 4.4. (unifiability of constrained terms).** Two constrained terms $s[\phi]$ and $t[\psi]$ are said to be unifiable if $s$ and $t$ are unifiable and their mgu $\theta$ with $\text{Dom}(\theta) \subseteq \mathcal{V}ar(s, t)$ satisfies both of the following: $x\theta \in \mathcal{Val} \cup \mathcal{V}$ for all variables $x \in \mathcal{V}ar(\phi, \psi)$, and $\phi\theta \wedge \psi\theta$ is satisfiable.

**Example 4.5.** The constrained terms $\text{f}(\text{nil}, y_1)$ [$y_1 \le 0$] and $\text{f}(\text{nil}, y_a)$ [$y_a > 0$] are not unifiable, but $\text{f}(\text{nil}, y_1)$ [$y_1 \le 0$] and $\text{f}(xs, y)$ [true] are unifiable by means of an mgu $\{y_1 \mapsto y, xs \mapsto \text{nil}\}$ of $\text{f}(\text{nil}, y_1)$ and $\text{f}(xs, y)$; their instance by means of the mgu is $\text{f}(\text{nil}, y)$ [$y \le 0 \wedge \text{true}$].
In considering ground constructor instances of a constrained term $s[\phi]$, logical variables—variables in $\phi$—are instantiated by value-constants but others are instantiated by arbitrary ground terms. Under our assumption that there is no user-defined constructor term with a theory sort, any variable with a theory sort is instantiated by value-constants only, and no variable with a non-theory sort is instantiated by any value-constant. For this reason, unlike the usual discussion on the instantiation of variables in the LCTRS setting (e.g., [1]), we do not take care of whether a variable is logical or not.

To compute finite complements, the constructions of complements in Sect. 3 rely on finiteness of signatures, which is usually assumed for TRSs in practice. However, signatures of LCTRSs are infinite in general. For example, signatures of integer LCTRSs include the integers and are thus infinite. For this reason, complements are often infinite, e.g., a complement of the value-constant 0 is $\{\mathbf{n} \mid n \in \mathbb{Z} \setminus \{0\}\}$. On the other hand, user-defined constructors (i.e., $C \setminus Val$) are usually finite. Since we consider constrained patterns, we can move value-constants in terms to constraints. For example, we transform the constrained pattern $f(\mathbf{nil}, 0)$ [true] into $f(\mathbf{nil}, x)$ [$x = 0$], where $x$ is a fresh variable. In summary, we consider value-free constrained patterns. Since each constrained term has an equivalent value-free constrained term [21, 24], in the rest of this paper, we assume w.l.o.g. that constrained patterns are value-free. For a constrained term $s[\phi]$, we denote its value-free variant by $\tilde{s}[\tilde{\phi}]$ [21]: $\tilde{s} = s[y_1, \dots, y_n]_{p_1, \dots, p_n}$ and $\tilde{\phi} = \phi \wedge \bigwedge_{i=1}^n (y_i = s|_{p_i})$, where $p_1, \dots, p_n$ are the positions of values in $s$, and $y_1, \dots, y_n$ are pairwise distinct variables such that $\{y_1, \dots, y_n\} \cap Var(s, \phi) = \emptyset$. It is clear that $\mathcal{G}_C(s[\phi]) = \mathcal{G}_C(\tilde{s}[\tilde{\phi}])$.

For the extension of $\ominus$ to constrained patterns, the key property of $\ominus$— $\mathcal{G}_C(s) = \mathcal{G}_C(s\sigma) \uplus \mathcal{G}_C(\{s\rho \mid \rho \in \bar{\sigma}, s\rho \neq s\sigma\})$—is adapted to unifiable constrained patterns $s[\phi], t[\psi]$ with $\sigma = mgu_C(s, t)$ as follows:

$$ \mathcal{G}_C(s[\phi]) = \mathcal{G}_C(s\sigma[\phi\sigma \wedge \psi\sigma]) \uplus \mathcal{G}_C(s\sigma[\phi\sigma \wedge \neg\psi\sigma]) \uplus \mathcal{G}_C(\{s\rho[\phi\sigma] \mid \rho \in \bar{\sigma}, s\rho \neq s\sigma\}) $$

The first and second ones are obtained by the following division of $\mathcal{G}_C(s\sigma[\phi\sigma]):$ $\mathcal{G}_C(s\sigma[\phi\sigma]) = \mathcal{G}_C(s\sigma[\phi\sigma \wedge \psi\sigma]) \uplus \mathcal{G}_C(s\sigma[\phi\sigma \wedge \neg\psi\sigma])$. The third one can be obtained similarly to the unconstrained case, but we restrict instances to those satisfying $\phi\sigma$. This is because all ground C-instances in $s[\phi]$ satisfy $\phi$, i.e., a substitution to obtain a ground C-instance in $s[\phi]$ respects $\phi$. Since $s[\phi]$ and $t[\psi]$ are assumed to be value-free, we have that $\mathcal{Ran}(\sigma|_{\mathcal{V}_{ar}(\phi, \psi)}) \subseteq \mathcal{V}$. Thus, by definition, for all substitutions $\rho \in \bar{\sigma}$, we have that $\rho|_{\mathcal{V}_{ar}(\phi, \psi)} = \sigma|_{\mathcal{V}_{ar}(\phi, \psi)}$, and hence $\phi\sigma = \phi\rho$.

Following the idea above, we extend the difference operator $\ominus$ to value-free constrained patterns.

**Definition 4.6** ($\ominus$ over value-free constrained patterns). We define a difference operator $\ominus$, which takes a value-free constrained pattern as a dividend and takes a value-free constrained linear pattern as a divisor, as follows:

$$ s[\phi] \ominus t[\psi] = \begin{cases} \{s\rho[\phi\sigma] \mid \rho \in \bar{\sigma}, s\rho \neq s\sigma\} & \text{is satisfiable} \\ \bigcup \{s\sigma[\phi\sigma \wedge \neg\psi'\sigma] \mid (\phi\sigma \wedge \neg\psi'\sigma) \text{ if } s[\phi], t'[\psi'] \text{ are unifiable} \\ \{s[\phi]\} & \text{otherwise} \end{cases} $$