Reducing Relative Termination to Dependency Pair Problems

Abstract

Relative termination, a generalized notion of termination, has been used in a number of different contexts like proving the confluence of rewrite systems or analyzing the termination of narrowing. In this paper, we introduce a new technique to prove relative termination by reducing it to dependency pair problems. To the best of our knowledge, this is the first significant contribution to Problem #106 of the RTA List of Open Problems. The practical significance of our method is illustrated by means of an experimental evaluation.

Germán Vidal is partially supported by the EU (FEDER) and the Spanish Ministerio de Economía y Competitividad under grant TIN2013-44742-C4-1-R and by the Generalitat Valenciana under grant PROMETEOII2015/013. Akihisa Yamada is supported by the Austrian Science Fund (FWF): Y757.

1 Introduction

Proving that a program terminates is a fundamental problem that has been extensively studied in almost all programming paradigms. For term rewrite systems (TRSs), termination analysis has attracted considerable attention (see, e.g., the survey of Zantema [31] and the termination portal¹), and various automated termination provers for TRSs have been developed, e.g. AProVE  [9],  [20], and NaTT  [28]. Among them the dependency pair (DP) method [2, 12] and its successor the DP framework [10] became a modern standard.

Termination of a TRS is usually checked for all possible reduction sequences. In some cases, however, one is interested in proving a generalized notion, relative termination [7, 17]. Roughly speaking, a TRS $\mathcal{R}$ is relatively terminating w.r.t. another TRS $\mathcal{B}$ (that here we call the base), when any infinite reduction using both systems contains only a finite number of steps given with rules from $\mathcal{R}$. For instance, consider the following base:

$$ \mathcal{B}_\mathsf {comlist} = \{\mathsf {cons}(x,\mathsf {cons}(y,ys)) \rightarrow \mathsf {cons}(y,\mathsf {cons}(x,ys))\} $$

specifying a property for commutative lists (i.e., that the order of elements is irrelevant). Termination of operations on commutative lists, described by a TRS $\mathcal{R}$, can be analyzed as the relative termination of $\mathcal{R}$ w.r.t. $\mathcal{B}_\mathsf {comlist}$. Note also that the base $\mathcal{B}_\mathsf {comlist}$ is clearly non-terminating.

Relative termination has been used in various contexts: proving confluence of a rewrite system [7, 13]; liveness properties in the presence of fairness [18]; and termination of narrowing [15, 24, 27], an extension of rewriting to deal with non-ground terms (see, e.g., [14]). Moreover, analyzing relative termination can also be useful for other purposes, like dealing with random values or considering rewrite systems with so called extra-variables (i.e., variables that occur in the right-hand side of a rule but not in the corresponding left-hand side). For instance, the following base $\mathcal{B}_\mathsf {rand}$ specifies a random number generator:

$$ \mathcal{B}_\mathsf {rand} = \{\mathsf {rand}(x) \rightarrow x,\ \mathsf {rand}(x) \rightarrow \mathsf {rand}(\mathsf {s}(x))\} $$

We have $\mathsf {rand}(\mathsf {0}) \rightarrow _{\mathcal{B}_\mathsf {rand}}^* \mathsf {s}^n(\mathsf {0})$ for arbitrary $n \in \mathbb {N}$. Now consider

$$ \begin{array}{@{}lllrcl@{\quad }rcll@{}} \mathcal{R}_\mathsf {quot} &{} = &{} \{\!\!&{} x - \mathsf {0} &{}\rightarrow &{} x, &{}\mathsf {s}(x) - \mathsf {s}(y) &{}\rightarrow &{} x - y,\\ &{}&{}&{}\mathsf {quot}(\mathsf {0},\mathsf {s}(y)) &{}\rightarrow &{} \mathsf {0}, &{}\mathsf {quot}(\mathsf {s}(x),\mathsf {s}(y)) &{}\rightarrow &{} \mathsf {s}(\mathsf {quot}(x-y,\mathsf {s}(y))) &{}\!\!\}\\ \end{array} $$

from [2]. Termination of $\mathcal{R}_\mathsf {quot}$ can be shown using the DP method [2]. However, it is unknown if $\mathcal{R}_\mathsf {quot}$ is relatively terminating w.r.t. $\mathcal{B}_\mathsf {rand}$ using previously known techniques. Note also that it seems not so obvious, since $\mathcal{R}_\mathsf {quot}$ is not relatively terminating w.r.t. the following similar variant $\mathcal{B}_\mathsf {gen}$:

$$ \mathcal{B}_\mathsf {gen} = \{\mathsf {gen} \rightarrow \mathsf {0},\ \mathsf {gen} \rightarrow \mathsf {s}(\mathsf {gen})\} $$

which is considered in the context of termination of narrowing [15, 24, 27]. Indeed, we can construct the following infinite reduction sequence using $\mathcal{B}_\mathsf {gen}$:

$$ \mathsf {s}(\mathsf {gen}) - \mathsf {s}(\mathsf {gen}) \rightarrow _{\mathcal{R}_\mathsf {quot}} \mathsf {gen} - \mathsf {gen} \rightarrow _{\mathcal{B}_\mathsf {gen}}^* \mathsf {s}(\mathsf {gen}) - \mathsf {s}(\mathsf {gen}) \rightarrow _{\mathcal{R}_\mathsf {quot}} \cdots $$

We expect that a similar technique can also be used to deal with TRSs with extra-variables. In principle, these systems are always non-terminating, since extra-variables can be replaced by any term. However, one can still consider an interesting termination property: is the system terminating if the extra-variables can only be instantiated with terms built from a restricted signature? Consider, e.g., the following TRS from [23]:

$$ \mathcal{R}= \{\mathsf {f}(x, \mathsf {0}) \rightarrow \mathsf {s}(x), \mathsf {g}(x) \rightarrow \mathsf {h}(x, y), \mathsf {h}(\mathsf {0}, x) \rightarrow \mathsf {f}(x, x), \mathsf {a} \rightarrow \mathsf {b}\} $$

This system is clearly non-terminating due to the extra variable in the second rewrite rule. However, by assuming that y can only take values built from constructor symbols (e.g., natural numbers), one can reformulate these rewrite rules as follows: $\mathcal{R}' = \{\mathsf {f}(x, \mathsf {0}) \rightarrow \mathsf {s}(x), \mathsf {g}(x) \rightarrow \mathsf {h}(x, \mathsf {gen}), \mathsf {h}(\mathsf {0}, x) \rightarrow \mathsf {f}(x, x), \mathsf {a} \rightarrow \mathsf {b}\}$, using $\mathcal{B}_\mathsf {gen}$ above. Obviously, $\mathcal{R}'\cup \mathcal{B}_\mathsf {gen}$ is still non-terminating since $\mathcal{B}_\mathsf {gen}$ is non-terminating. Nevertheless, one can still prove relative termination of $\mathcal{R}'$ w.r.t. $\mathcal{B}_\mathsf {gen}$, which is an interesting property since one can ensure terminating derivations by using an appropriate heuristics to instantiate extra-variables.

Another interesting application of relative termination w.r.t. $\mathcal{B}_\mathsf {rand}$ is to generate test cases. For example, in the QuickCheck technique, lists over, e.g., natural numbers are generated at random. Assume f and g are defined externally by a TRS $\mathcal{R}_{fg}$, and consider the TRS $\mathcal{R}_{test}$ consisting of the following rules:

$$\begin{aligned} \mathsf {rands}(\mathsf {0},y)&\rightarrow \mathsf {done}(y)&\mathsf {rands}(\mathsf {s}(x),y)&\rightarrow \mathsf {rands}(x, \mathsf {cons}(\mathsf {rand}(\mathsf {0}), y))\\ \mathsf {tests}(\mathsf {0})&\rightarrow \mathsf {true}&\mathsf {tests}(\mathsf {s}(x))&\rightarrow \mathsf {test}(\mathsf {rands}(\mathsf {rand}(\mathsf {0}),\mathsf {nil})) \wedge \mathsf {tests}(x) \\ \mathsf {eq}(x,x)&\rightarrow \mathsf {true}&\mathsf {test}(\mathsf {done}(y))&\rightarrow \mathsf {eq}(f(y),g(y)) \end{aligned}$$

where lists are built from $\mathsf {nil}$ and $\mathsf {cons}$. Execution of $\mathsf {tests}(\mathsf {s}^n(\mathsf {0}))$ tests the equivalence between f and g by feeding them random inputs n times. Even when f and g are defined by $f(x) \rightarrow x$ and $g(x) \rightarrow x$, AProVE fails to prove relative termination of $\mathcal{R}_{test} \cup \mathcal{R}_{fg}$ w.r.t. $\mathcal{B}_\mathsf {rand}$.

In this paper, we present a new technique for proving relative termination by reducing it to the finiteness of dependency pair problems. To the best of our knowledge, we provide the first significant contribution to Problem #106 of the RTA List of Open Problems:² “Can we use the dependency pair method to prove relative termination?” We implemented the proposed method in the termination tool NaTT  ³ and showed its significance through experiments. Using results of this paper and [29], NaTT can prove relative termination of $\mathcal{R}_\mathsf {quot}$ w.r.t. $\mathcal{B}_\mathsf {rand}$, and relative termination of $\mathcal{R}_{test}\cup \mathcal{R}_{fg}$ w.r.t. $\mathcal{B}_\mathsf {rand}$ for e.g., naive and tail recursive definitions of summation as f and g.

This paper is organized as follows. In Sect. 2, we briefly review some notions and notations of term rewriting. In Sects. 3–5, we present our main contributions for reducing relative termination to a dependency pair problem. Moreover, some subtle features about minimality are discussed in Sect. 6. Then, Sect. 7 describes implementation issues and presents selected results from an experimental evaluation. Finally, Sect. 8 compares our technique with some related work, and Sect. 9 concludes and points out some directions for future research. Missing proofs of technical results can be found in the appendix.

2 Preliminaries

We assume some familiarity with basic concepts and notations of term rewriting. We refer the reader to, e.g., [4] for further details.

A signature $\mathcal{F}$ is a set of function symbols. Given a set of variables $\mathcal{V}$ with $\mathcal{F}\cap \mathcal{V}=\emptyset$, we denote the domain of terms by $\mathcal{T}(\mathcal{F},\mathcal{V})$. We use $\mathsf {f},\mathsf {g},\ldots$ to denote function symbols and $x,y,\ldots$ to denote variables. The root symbol of a term $t = f(t_1,\dots ,t_n)$ is f and denoted by $\mathsf {root}(t)$. We assume an extra fresh constant $\Box$ called a hole. Then, $C\in \mathcal{T}(\mathcal{F}\cup \{\Box \},\mathcal{V})$ is called a context on $\mathcal{F}$. We use the notation $C[\,]$ for the context containing one hole, and if $t\in \mathcal{T}(\mathcal{F},\mathcal{V})$, then C[t] denotes the result of placing t in the hole of $C[\,]$.

A position p in a term t is represented by a finite sequence of natural numbers, where $\epsilon$ denotes the root position. We let $t|_p$ denote the subterm of t at position p, and $t[s]_p$ the result of replacing the subterm $t|_p$ by the term s. We denote by $s\trianglerighteq t$ that t is a subterm of s, and by $s\vartriangleright t$ that it is a proper subterm.

$\mathsf {{\mathcal{V}}ar}(t)$ denotes the set of variables appearing in t. A substitution is a mapping $\sigma : \mathcal{V}\rightarrow \mathcal{T}(\mathcal{F},\mathcal{V})$, which is extended to a morphism from $\mathcal{T}(\mathcal{F},\mathcal{V})$ to $\mathcal{T}(\mathcal{F},\mathcal{V})$ in a natural way. We denote the application of a substitution $\sigma$ to a term t by $t\sigma$.

A rewrite rule $l \rightarrow r$ is a pair of terms such that $l \notin \mathcal{V}$ and $\mathsf {{\mathcal{V}}ar}(l) \supseteq \mathsf {{\mathcal{V}}ar}(r)$. The terms l and r are called the left-hand side and the right-hand side of the rule, respectively. A term rewriting system (TRS) is a set of rewrite rules. Given a TRS $\mathcal{R}$, we write $\mathcal{F}_\mathcal{R}$ for the set of function symbols appearing in $\mathcal{R}$, $\mathcal{D}_\mathcal{R}$ for the set of the defined symbols, i.e., the root symbols of the left-hand sides of the rules, and $\mathcal{C}_\mathcal{R}$ for the set of constructors; $\mathcal{C}_\mathcal{R}= \mathcal{F}_\mathcal{R}\setminus \mathcal{D}_\mathcal{R}$.

For a TRS $\mathcal{R}$, we define the associated rewrite relation as follows: given terms $s,t\in \mathcal{T}(\mathcal{F},\mathcal{V})$, holds iff there exist a position p in s, a rewrite rule $l \rightarrow r \in \mathcal{R}$ and a substitution $\sigma$ with $s|_p = l\sigma$ and $t = s[r\sigma ]_p$; the rewrite step is often denoted by to make the rewritten position explicit, and if the position is strictly below the root. Given a binary relation $\rightarrow$, we denote by $\rightarrow ^{+}$ the transitive closure of $\rightarrow$ and by $\rightarrow ^{*}$ its reflexive and transitive closure.

Now we recall the formal definition of relative termination:

Definition 1

(Relative Termination [17]). Given two TRSs $\mathcal{R}$ and $\mathcal{B}$, we define the relation as $\rightarrow _\mathcal{B}^*\cdot \rightarrow _\mathcal{R}\cdot \rightarrow _\mathcal{B}^*$. We say that $\mathcal{R}$ relatively terminates w.r.t. $\mathcal{B}$, or simply that $\mathcal{R}/\mathcal{B}$ is terminating, if the relation is terminating. We say that a term t is ${\mathcal{R}/\mathcal{B}}$ -nonterminating if it starts an infinite derivation, and ${\mathcal{R}/\mathcal{B}}$ -terminating otherwise.

In other words, $\mathcal{R}/\mathcal{B}$ is terminating if every (possibly infinite) $\rightarrow _{\mathcal{R}\cup \mathcal{B}}$ derivation contains only finitely many $\rightarrow _{\mathcal{R}}$ steps. Note that sequences of $\rightarrow _{\mathcal{B}}$ steps are “collapsed” and seen as a single step. Hence, an infinite derivation must contain an infinite number of $\rightarrow _{\mathcal{R}}$ steps and thus only finite $\rightarrow _{\mathcal{B}}$ subderivations.

The Dependency Pair Framework.

The dependency pair (DP) framework [2, 10] enables analyzing cyclic dependencies between rewrite rules, and has become one of the most popular approaches to proving termination in term rewriting. Indeed, it underlies virtually all modern termination tools for TRSs.

Let us briefly recall the fundamentals of the DP framework. Here, we consider that the signature $\mathcal{F}$ is implicitly extended with fresh function symbols $f^\sharp$ for each defined function $f\in \mathcal{D}_\mathcal{R}$. Also, given a term with $f\in \mathcal{D}_\mathcal{R}$, we let $t^\sharp$ denote . Here, is an abbreviation for $t_1,\ldots ,t_n$ for an appropriate n. If $l \rightarrow r \in \mathcal{R}$ and t is a subterm of r with a defined root symbol, then the rule $l^\sharp \rightarrow t^\sharp$ is a dependency pair of $\mathcal{R}$. The set of all dependency pairs of $\mathcal{R}$ is denoted by $\mathsf {DP}(\mathcal{R})$. Note that $\mathsf {DP}(\mathcal{R})$ is also a TRS.

A key ingredient in this framework is the notion of a chain, which informally represents a sequence of calls that can occur during a reduction. In the following, $\mathcal{P}$ will often denote a set of dependency pairs. A $(\mathcal{P},\mathcal{R})$ -chain (à la [12]) is a possibly infinite rewrite sequence . The basic result from [2] is then that a TRS $\mathcal{R}$ is terminating iff there is no infinite $(\mathsf {DP}(\mathcal{R}),\mathcal{R})$-chain. In order to check absence of infinite chains, the DP framework introduces the notions of a DP problem. A DP problem is just a pair $(\mathcal{P},\mathcal{R})$, and is called finite if there is no infinite $(\mathcal{P},\mathcal{R})$-chain. To prove DP problems finite, we can use several techniques implemented in current termination tools, e.g., AProVE, , and NaTT.

3 Relative Termination as a Dependency Pair Problem

Let us start with some basic conditions in terms of dependency pair problems. First, it is folklore that, given two TRSs $\mathcal{R}$ and $\mathcal{B}$, termination of $\mathcal{R}\cup \mathcal{B}$ implies the relative termination of $\mathcal{R}$ w.r.t. $\mathcal{B}$. Therefore, an obvious sufficient condition for relative termination can be stated as follows:

Proposition 1

Let $\mathcal{R}$ and $\mathcal{B}$ be TRSs. $\mathcal{R}/\mathcal{B}$ is terminating if the DP problem $(\mathsf {DP}(\mathcal{R}\cup \mathcal{B}),\mathcal{R}\cup \mathcal{B})$ is finite.

Observe that $\mathsf {DP}(\mathcal{R})\cup \mathsf {DP}(\mathcal{B})\subseteq \mathsf {DP}(\mathcal{R}\cup \mathcal{B})$ but $\mathsf {DP}(\mathcal{R}\cup \mathcal{B}) = \mathsf {DP}(\mathcal{R})\cup \mathsf {DP}(\mathcal{B})$ is not true when there are shared symbols.

On the other hand, using a proof technique from the standard DP framework, we can easily prove the following necessary condition for relative termination.

Proposition 2

Let $\mathcal{R}$ and $\mathcal{B}$ be TRSs. If $\mathcal{R}/\mathcal{B}$ is terminating, then the DP problem $(\mathsf {DP}(\mathcal{R}),\mathcal{R}\cup \mathcal{B})$ is finite.

Now, we aim at finding more precise characterizations of relative termination in terms of DP problems. First we need some auxiliary definitions and results.

Definition 2

(Order Pair). We say that $(\succsim ,\succ )$ is a (well-founded) order pair on carrier A if $\;\succsim$ is a quasi-ordering on A, $\succ$ is a (well-founded) strict order on A, and $\succsim$ and $\succ$ are compatible (i.e., ${\succsim } \circ {\succ } \circ {\succsim } \subseteq {\succ }$).

The multiset extension of an order pair $({\succsim },{\succ })$ on A is the order pair $({\succsim ^\mathrm {mul}},\mathrel {}{\succ ^\mathrm {mul}})$ on multisets over A which is defined as follows: $X \succsim ^\mathrm {mul}Y$ if X and Y are written $X = X' \uplus \{x_1,\ldots ,x_n\}$ and $Y = Y' \uplus \{y_1,\ldots ,y_n\}$|where “$\uplus$” denotes union on multisets|such that

• $\forall y \in Y'.\ \exists x \in X'.\ x \succ y$, and

• $\forall i \in \{1,\ldots ,n\}.\ x_i \succsim y_i$.

We have $X \succ ^\mathrm {mul}Y$ if it also holds that $X' \ne \emptyset$. It is shown that the multiset extension of a well-founded order pair is also a well-founded order pair [26].

In the following, we will consider a particular order pair:

Definition 3

For two TRSs $\mathcal{R}$ and $\mathcal{B}$, the pair $(\succsim _{\mathcal{R}/\mathcal{B}},\succ _{\mathcal{R}/\mathcal{B}})$ of relations on terms is defined as follows: ${\succsim }_{\mathcal{R}/\mathcal{B}} = ({\rightarrow _{\mathcal{R}\cup \mathcal{B}}}\cup {\vartriangleright })^*$ and ${\succ }_{\mathcal{R}/\mathcal{B}} = ({\rightarrow _{\mathcal{R}/\mathcal{B}}}\cup {\vartriangleright })^+$.

The relations $\succsim _{\mathcal{R}/\mathcal{B}}$ and $\succ _{\mathcal{R}/\mathcal{B}}$ enjoy the following key property:

Lemma 1

For two TRSs $\mathcal{R}$ and $\mathcal{B}$, $(\succsim _{\mathcal{R}/\mathcal{B}},\succ _{\mathcal{R}/\mathcal{B}})$ is a well-founded order pair on ${\mathcal{R}/\mathcal{B}}$-terminating terms.

Proof

For an ${\mathcal{R}/\mathcal{B}}$-terminating term t, $t \rightarrow _{\mathcal{R}\cup \mathcal{B}} t'$ implies that $t'$ is also ${\mathcal{R}/\mathcal{B}}$-terminating. Furthermore, $t \vartriangleright t'$ implies that $t'$ is also ${\mathcal{R}/\mathcal{B}}$-terminating. Using these facts, the required properties are straightforward from the definition.    $\square$

We now introduce the multisets that we will use to prove our main results.

Definition 4

Let $\mathcal{R}$ be a TRS and t a term. The multiset $\triangledown _{\!\mathcal{R}}(t)$ of maximal $\mathcal{R}$ -defined subterms of t is defined as follows:

• $\triangledown _{\!\mathcal{R}}(x) = \emptyset$ if $x \in \mathcal{V}$,

• $\triangledown _{\!\mathcal{R}}(f(t_1,\dots ,t_n)) = \triangledown _{\!\mathcal{R}}(t_1) \cup \cdots \cup \triangledown _{\!\mathcal{R}}(t_n)$ if $f \notin \mathcal{D}_\mathcal{R}$, and

• $\triangledown _{\!\mathcal{R}}(f(t_1,\dots ,t_n)) = \{ f(t_1,\dots ,t_n) \}$ if $f \in \mathcal{D}_\mathcal{R}$.

An essential property is that an $\rightarrow _\mathcal{R}$ reduction step corresponds to a decrease in $\succ _{\mathcal{R}/\mathcal{B}}^\mathrm {mul}$, which is stated as follows:

Lemma 2

Let $\mathcal{R}$ and $\mathcal{B}$ be TRSs. If $s \rightarrow _\mathcal{R}t$ then $\triangledown _{\!\mathcal{R}}(s) \succ _{\mathcal{R}/\mathcal{B}}^\mathrm {mul}\triangledown _{\!\mathcal{R}}(t)$.

Proof

Let and q be the shortest prefix of p such that $\mathsf {root}(s|_q) \in \mathcal{D}_\mathcal{R}$, that is, $\triangledown _{\!\mathcal{R}}(s) = \triangledown _{\!\mathcal{R}}(s[\,]_q) \cup \{ s|_q \}$. Note that q always exists since $\mathsf {root}(s|_p) \in \mathcal{D}_\mathcal{R}$. We distinguish the following cases:

• Suppose that $q < p$. Since $\mathsf {root}(s|_q) = \mathsf {root}(t|_q) \in \mathcal{D}_\mathcal{R}$, we have $\triangledown _{\!\mathcal{R}}(t) = \triangledown _{\!\mathcal{R}}(s[\,]_q) \cup \{ t|_q \}$. Trivially $s|_q \succ _{\mathcal{R}/\mathcal{B}} t|_q$, and thus $\triangledown _{\!\mathcal{R}}(s) \succ _{\mathcal{R}/\mathcal{B}}^\mathrm {mul}\triangledown _{\!\mathcal{R}}(t)$.

• Suppose that $p = q$. We have $\triangledown _{\!\mathcal{R}}(t) = \triangledown _{\!\mathcal{R}}(s[\,]_p) \cup \triangledown _{\!\mathcal{R}}(t|_p)$. For every $t' \in \triangledown _{\!\mathcal{R}}(t|_p)$, we have $s|_p \rightarrow _\mathcal{R}t|_p \trianglerighteq t'$ and thus $s|_p \succ _{\mathcal{R}/\mathcal{B}} t'$. We conclude $\triangledown _{\!\mathcal{R}}(s) \succ _{\mathcal{R}/\mathcal{B}} \triangledown _{\!\mathcal{R}}(t)$.   $\square$

Unfortunately, a $\rightarrow _\mathcal{B}$ reduction does not generally imply a weak decrease in $\succsim _{\mathcal{R}/\mathcal{B}}^\mathrm {mul}$ without further conditions. Hence, we introduce the following notion:

Definition 5

( $\mathcal{R}/\mathcal{B}$ Weak-Decreasing). Let $\mathcal{R}$ and $\mathcal{B}$ be TRSs. We say that $\mathcal{R}/\mathcal{B}$ is weak-decreasing if $t \rightarrow _\mathcal{B}t'$ implies $\triangledown _{\!\mathcal{R}}(t) \succsim _{\mathcal{R}/\mathcal{B}}^\mathrm {mul}\triangledown _{\!\mathcal{R}}(t')$.

Keen readers may notice that $\mathcal{R}/\mathcal{B}$ weak-decreasingness is somewhat related to the notion of a rank non-increasing TRS from [22]. Intuitively speaking, given two disjoint signatures, the rank of a term is given by the number of nested functions from different sets. E.g., given signatures $\mathcal{F}_1=\{\mathsf {f},\mathsf {a}\}$ and $\mathcal{F}_2=\{\mathsf {g}\}$, the term $\mathsf {f}(\mathsf {f}(\mathsf {a}))$ has rank 1, while $\mathsf {f}(\mathsf {f}(\mathsf {g}(\mathsf {a})))$ has rank 3. A TRS $\mathcal{R}$ is then called rank non-increasing if $t \rightarrow _\mathcal{R}t'$ implies that the rank of t is equal or greater than the rank of $t'$. The following example illustrates the difference between our notion of $\mathcal{R}/\mathcal{B}$ weak-decreasingness and that of rank non-increasingness:

Example 1

Consider the two TRSs $\mathcal{R}= \{\mathsf {a} \rightarrow \mathsf {b}\}$ and $\mathcal{B}= \{\mathsf {b} \rightarrow \mathsf {a}\}$. Clearly, $\mathcal{R}\cup \mathcal{B}$ is rank non-increasing (there are no nested functions, so the rank is always 1). On the other hand, $\mathcal{R}/\mathcal{B}$ is not weak-decreasing since $\mathsf {b}\rightarrow _\mathcal{B}\mathsf {a}$ but $\triangledown _{\!\mathcal{R}}(\mathsf {b}) = \{\,\} \not \succsim _{\mathcal{R}/\mathcal{B}}^\mathrm {mul}\{\mathsf {a}\} = \triangledown _{\!\mathcal{R}}(\mathsf {a})$. Not also that $\mathcal{R}/\mathcal{B}$ is not terminating.

Now we can show the following result using Lemmas 1 and 2, and the fact that the multiset extension preserves well-foundedness.

Lemma 3

Let $\mathcal{R}$ and $\mathcal{B}$ be TRSs such that $\mathcal{R}/\mathcal{B}$ is weak-decreasing. A term s is ${\mathcal{R}/\mathcal{B}}$-terminating if all elements in $\triangledown _{\!\mathcal{R}}(s)$ are ${\mathcal{R}/\mathcal{B}}$-terminating.

Now we recall the notion of minimal (nonterminating) terms. We say that an ${\mathcal{R}/\mathcal{B}}$-nonterminating term is minimal if all its proper subterms are ${\mathcal{R}/\mathcal{B}}$-terminating. It is clear that any ${\mathcal{R}/\mathcal{B}}$-nonterminating term has some minimal ${\mathcal{R}/\mathcal{B}}$-nonterminating subterm.

Lemma 4

Let $\mathcal{R}$ and $\mathcal{B}$ be TRSs such that $\mathcal{R}/\mathcal{B}$ is weak-decreasing. If t is a minimal $\mathcal{R}/\mathcal{B}$-nonterminating term, then $\mathsf {root}(t)\in \mathcal{D}_\mathcal{R}$.

Proof

We prove the claim by contradiction. Consider a minimal $\mathcal{R}/\mathcal{B}$-nonterminating term s such that $\mathsf {root}(s) \notin \mathcal{D}_\mathcal{R}$. Since $\mathsf {root}(s) \notin \mathcal{D}_\mathcal{R}$, all elements in $\triangledown _{\!\mathcal{R}}(s)$ are proper subterms of s, which are $\mathcal{R}/\mathcal{B}$-terminating due to minimality. Lemma 3 implies that s is $\mathcal{R}/\mathcal{B}$-terminating, hence we have a contradiction.

Using the previous results, we can state the following sufficient condition which states that relative termination of $\mathcal{R}$ w.r.t. $\mathcal{B}$ coincides with the finiteness of the DP problem $(\mathsf {DP}(\mathcal{R}), \mathcal{R}\cup \mathcal{B})$, even if $\mathcal{B}$ is non-terminating. To facilitate the following discussion, besides ${\mathcal{R}/\mathcal{B}}$ weak-decreasingness we further impose that $\mathcal{R}$ and $\mathcal{B}$ share no defined symbol, $i.e.,$ $\mathcal{D}_\mathcal{R}\cap \mathcal{D}_\mathcal{B}= \emptyset$. This condition will be relaxed in the later development. The proof of the following theorem is analogous to the standard dependency pair proof scheme.

Theorem 1

Let $\mathcal{R}$ and $\mathcal{B}$ be TRSs such that $\mathcal{R}/\mathcal{B}$ is weak-decreasing and $\mathcal{D}_\mathcal{R}\cap \mathcal{D}_\mathcal{B}= \emptyset$. Then, $\mathcal{R}/\mathcal{B}$ is terminating iff the DP problem $(\mathsf {DP}(\mathcal{R}), \mathcal{R}\cup \mathcal{B})$ is finite.

Theorem 1 is not yet applicable in practice; whether $\mathcal{R}/\mathcal{B}$ is weak-decreasing or not is obviously undecidable in general. Thus in the next section, we provide decidable syntactic conditions to ensure $\mathcal{R}/\mathcal{B}$ weak-decreasingness.

4 Syntactic Conditions for Weak-Decreasingness

In this section, we focus on finding syntactic and decidable conditions that ensure $\mathcal{R}/\mathcal{B}$ weak-decreasingness. For this purpose, this time we require $\mathcal{B}$ to be non-duplicating, i.e., no variable has more occurrences in the right-hand side of a rule than in its left-hand side, together with the following condition:

Definition 6

(Dominance). We say that a TRS $\mathcal{R}$ dominates a TRS $\mathcal{B}$ iff the right-hand sides of all rules in $\mathcal{B}$ contain no symbol from $\mathcal{D}_\mathcal{R}$.

Before proving that the above two conditions ensure $\mathcal{R}/\mathcal{B}$ weak-decreasingness, we state an auxiliary result. Let $\mathsf {\mathcal{M}\mathcal{V}ar}(s)$ denote the multiset of variables occurring in a term s. The following lemma can easily be proved.

Lemma 5

Let $\mathcal{R}$ and $\mathcal{B}$ be TRSs such that $\mathcal{R}$ dominates $\mathcal{B}$. For every term t and substitution $\sigma$, $\triangledown _{\!\mathcal{R}}(t\sigma ) \succsim _{\mathcal{R}/\mathcal{B}}^\mathrm {mul}\biguplus _{x \in \mathsf {\mathcal{M}\mathcal{V}ar}(t)} \triangledown _{\!\mathcal{R}}(x\sigma )$.

The following lemma is the key result of this section:

Lemma 6

Let $\mathcal{R}$ and $\mathcal{B}$ be TRSs such that $\mathcal{R}$ dominates $\mathcal{B}$ and $\mathcal{B}$ is non-duplicating. Then $\mathcal{R}/\mathcal{B}$ is weak-decreasing.

Proof

We prove that implies $\triangledown _{\!\mathcal{R}}(t) \succsim _{\mathcal{R}/\mathcal{B}}^\mathrm {mul}\triangledown _{\!\mathcal{R}}(t')$ for arbitrary terms t and $t'$ and a position p. We distinguish the following two cases:

• First, assume that p has a prefix q such that $t|_q \in \triangledown _{\!\mathcal{R}}(t)$. Then, we have

  $$\begin{aligned} \triangledown _{\!\mathcal{R}}(t)&= \triangledown _{\!\mathcal{R}}(t[\,]_q) \cup \{ t|_q \}&\text {and}&\triangledown _{\!\mathcal{R}}(t')&= \triangledown _{\!\mathcal{R}}(t[\,]_q) \cup \{ t'|_q \} \end{aligned}$$

  Since $t|_q \rightarrow _\mathcal{B}t'|_q$, we have $t|_q \succsim _{\mathcal{R}/\mathcal{B}}^\mathrm {mul}t'|_q$ and thus $\triangledown _{\!\mathcal{R}}(t) \succsim _{\mathcal{R}/\mathcal{B}}^\mathrm {mul}\triangledown _{\!\mathcal{R}}(t')$.

• Assume now that $t_q \notin \triangledown _{\!\mathcal{R}}(t)$ for any prefix q of p. Let $l \rightarrow r \in \mathcal{B}$, $t|_p = l\sigma$, and $t' = t[r\sigma ]_p$. In this case, we have

  $$\begin{aligned} \triangledown _{\!\mathcal{R}}(t)&= \triangledown _{\!\mathcal{R}}(t[\,]_p) \cup \triangledown _{\!\mathcal{R}}(l\sigma )&\text {and}&\triangledown _{\!\mathcal{R}}(t')&= \triangledown _{\!\mathcal{R}}(t[\,]_p) \cup \triangledown _{\!\mathcal{R}}(r\sigma ) \end{aligned}$$

  From Lemma 5, we have $\triangledown _{\!\mathcal{R}}(l\sigma ) \succsim _{\mathcal{R}/\mathcal{B}}^\mathrm {mul}\bigcup _{x \in \mathsf {\mathcal{M}\mathcal{V}ar}(l)} \triangledown _{\!\mathcal{R}}(x\sigma )$. Since $\mathcal{R}$ dominates $\mathcal{B}$, r cannot contain symbols from $\mathcal{D}_\mathcal{R}$. Therefore,

  $$\begin{aligned} \triangledown _{\!\mathcal{R}}(l\sigma )&\succsim _{\mathcal{R}/\mathcal{B}}^\mathrm {mul}\textstyle \bigcup _{x \in \mathsf {\mathcal{M}\mathcal{V}ar}(l)} \triangledown _{\!\mathcal{R}}(x\sigma )&\text {and}&\triangledown _{\!\mathcal{R}}(r\sigma )&= \textstyle \bigcup _{x \in \mathsf {\mathcal{M}\mathcal{V}ar}(r)} \triangledown _{\!\mathcal{R}}(x\sigma ) \end{aligned}$$

  Since $\mathcal{B}$ is non-duplicating, we have $\mathsf {\mathcal{M}\mathcal{V}ar}(l) \supseteq \mathsf {\mathcal{M}\mathcal{V}ar}(r)$ and thus $\triangledown _{\!\mathcal{R}}(l\sigma ) \supseteq \triangledown _{\!\mathcal{R}}(r\sigma )$. Therefore, we conclude that $\triangledown _{\!\mathcal{R}}(t) \succsim _{\mathcal{R}/\mathcal{B}}^\mathrm {mul}\triangledown _{\!\mathcal{R}}(t')$.   $\square$

Finally, the following result is a direct consequence of Theorem 1 and Lemma 6.

Corollary 1

Let $\mathcal{R}$ and $\mathcal{B}$ be TRSs such that $\mathcal{R}$ dominates $\mathcal{B}$, $\mathcal{B}$ is non-duplicating, and $\mathcal{D}_\mathcal{R}\cap \mathcal{D}_\mathcal{B}= \emptyset$. Then, $\mathcal{R}/\mathcal{B}$ is terminating iff the DP problem $(\mathsf {DP}(\mathcal{R}), \mathcal{R}\cup \mathcal{B})$ is finite.

The following simple example illustrates that Corollary 1 indeed advances the state-of-the-art in proving relative termination.

Example 2

Consider the following two TRSs:

$$ \mathcal{R}= \{\mathsf {g}(\mathsf {s}(x),y) \rightarrow \mathsf {g}(\mathsf {f}(x,y),y)\} ~~~~ \mathcal{B}= \{\mathsf {f}(x,y) \rightarrow x, ~ \mathsf {f}(x,y) \rightarrow \mathsf {f}(x,\mathsf {s}(y))\} $$

Since they satisfy the conditions of Corollary 1, we obtain the DP problem $(\mathsf {DP}(\mathcal{R}),\mathcal{R}\cup \mathcal{B})$, where $\mathsf {DP}(\mathcal{R}) = \{ \mathsf {g}^\sharp (\mathsf {s}(x),y) \rightarrow \mathsf {g}^\sharp (\mathsf {f}(x,y),y) \}$. The DP problem can be proved finite using classic techniques, e.g. polynomial interpretation ${\mathcal {P}\! ol }$ such that $\mathsf {f}_{\mathcal {P}\! ol }(x,y) = x$. On the other hand, all the tools we know that support relative termination, namely AProVE (ver. 2014), (ver. 1.15), Jambox (ver. 2006) [6], and TPA (ver. 1.1) [19], fail on this problem.

The dominance condition and the non-duplication condition are indeed necessary for Corollary 1 to hold. It is clear that the former condition is necessary from Example 1, which violates the dominance condition. For the latter condition, the following example illustrates that it is also necessary.

Example 3

Consider the following two TRSs:

$$\begin{aligned} \mathcal{R}&= \{\mathsf {a} \rightarrow \mathsf {b}\}&\mathcal{B}&= \{\mathsf {f}(x) \rightarrow \mathsf {c}(x,\mathsf {f}(x))\} \end{aligned}$$

We have the following infinite -derivation:

$$ \mathsf {f}(\mathsf {a}) \rightarrow _\mathcal{B}\mathsf {c}(\mathsf {a},\mathsf {f}(\mathsf {a})) \rightarrow _\mathcal{R}\mathsf {c}(\mathsf {b},\mathsf {f}(\mathsf {a})) \rightarrow _\mathcal{B}\mathsf {c}(\mathsf {b},\mathsf {c}(\mathsf {a},\mathsf {f}(\mathsf {a}))) \rightarrow _\mathcal{R}\mathsf {c}(\mathsf {b},\mathsf {c}(\mathsf {b},\mathsf {f}(\mathsf {a}))) \rightarrow _\mathcal{B}\cdots $$

However, there is no infinite $(\mathsf {DP}(\mathcal{R}),\mathcal{R}\cup \mathcal{B})$-chain since $\mathsf {DP}(\mathcal{R})=\emptyset$. Note that this is a counterexample against [15, Theorem 5].

5 Improving Applicability

In contrast to dominance and non-duplication, the condition $\mathcal{D}_\mathcal{R}\cap \mathcal{D}_\mathcal{B}= \emptyset$ is not necessary. In order to show that this is indeed the case, let us recall the following result from [7]:

Proposition 3

Let $\mathcal{R}$, $\mathcal{B}'$ and $\mathcal{B}''$ be TRSs. Then, $(\mathcal{R}\cup \mathcal{B}')/\mathcal{B}''$ is terminating iff both $\mathcal{R}/(\mathcal{B}'\cup \mathcal{B}'')$ and $\mathcal{B}'/\mathcal{B}''$ are terminating.

Therefore, we have the following corollary in our context:

Corollary 2

Let $\mathcal{R}$ and $\mathcal{B}$ be TRSs with $\mathcal{B}= \mathcal{B}'\cup \mathcal{B}''$. If $(\mathcal{R}\cup \mathcal{B}')/\mathcal{B}''$ is terminating, then $\mathcal{R}/\mathcal{B}$ is terminating.

Now we state the first theorem of this section.

Theorem 2

Let $\mathcal{R}$ and $\mathcal{B}$ be TRSs such that $\mathcal{R}$ dominates $\mathcal{B}$ and $\mathcal{B}$ is non-duplicating. If the DP problem $(\mathsf {DP}(\mathcal{R}), \mathcal{R}\cup \mathcal{B})$ is finite then $\mathcal{R}/\mathcal{B}$ is terminating.

Proof

Let $\mathcal{B}'$ be the set of rules in $\mathcal{B}$ that define $\mathcal{D}_\mathcal{R}$ symbols, $i.e.,$ $\mathcal{B}' = \{ l \rightarrow r \in \mathcal{B}\mid \mathsf {root}(l) \in \mathcal{D}_\mathcal{R}\}$, and let $\mathcal{B}'' = \mathcal{B}\setminus \mathcal{B}'$. Since the right-hand sides of $\mathcal{B}'$ rules cannot contain symbols from $\mathcal{D}_\mathcal{R}$ $(=\mathcal{D}_{\mathcal{R}\cup \mathcal{B}'})$, we have $\mathsf {DP}(\mathcal{R}\cup \mathcal{B}') = \mathsf {DP}(\mathcal{R})$.

Now, observe that $\mathcal{R}\cup \mathcal{B}'$ dominates $\mathcal{B}''$, $\mathcal{D}_{\mathcal{R}\cup \mathcal{B}'} \cap \mathcal{D}_{\mathcal{B}''} = \emptyset$, and $\mathcal{B}''$ is non-duplicating. Thus, Corollary 1 implies the relative termination of $\mathcal{R}\cup \mathcal{B}'$ w.r.t. $\mathcal{B}''$ and Corollary 2 implies the relative termination of $\mathcal{R}$ w.r.t. $\mathcal{B}$.   $\square$

Unfortunately, the remaining two, namely the dominance and non-duplication conditions, might be too restrictive in practice. For instance, only six out of 44 examples in the relative TRS category of the TPDB satisfy both conditions.

Luckily, we can employ again Corollary 2 to relax the conditions. Consider TRSs $\mathcal{R}$ and $\mathcal{B}$ such that we want to prove that $\mathcal{R}/\mathcal{B}$ is terminating but the conditions of Theorem 2 do not hold. Then, we might still find a partition $\mathcal{B}= \mathcal{B}'\uplus \mathcal{B}''$ such that $\mathcal{R}\cup \mathcal{B}'$ and $\mathcal{B}''$ satisfy the conditions.

If we succeed, then by Theorem 2 and Corollary 2, we have that $\mathcal{R}/\mathcal{B}$ is terminating (i.e., by Theorem 2, $(\mathcal{R}\cup \mathcal{B}')/\mathcal{B}''$ is terminating and, by Corollary 2, $\mathcal{R}/(\mathcal{B}'\cup \mathcal{B}'')$ is also terminating with $\mathcal{B}'\cup \mathcal{B}''=\mathcal{B}$).

Corollary 3

Let $\mathcal{R}$ and $\mathcal{B}$ be TRSs. If $\mathcal{B}$ is split into $\mathcal{B}= \mathcal{B}'\uplus \mathcal{B}''$ such that (1) $\mathcal{B}''$ is non-duplicating, (2) $\mathcal{R}\cup \mathcal{B}'$ dominates $\mathcal{B}''$, and (3) the DP problem $(\mathsf {DP}(\mathcal{R}\cup \mathcal{B}'),\mathcal{R}\cup \mathcal{B})$ is finite, then $\mathcal{R}/\mathcal{B}$ is terminating.

Example 4

Consider the following TRSs $\mathcal{R}$ and $\mathcal{B}$:

$$\begin{aligned} \mathcal{R}&= \{\mathsf {a} \rightarrow \mathsf {b}\}&\mathcal{B}&= \{ \mathsf {f}(\mathsf {s}(x)) \rightarrow \mathsf {c}(x,\mathsf {f}(x)),\ \mathsf {c}(x,\mathsf {c}(y,z)) \rightarrow \mathsf {c}(y,\mathsf {c}(x,z)) \} \end{aligned}$$

The first rule of $\mathcal{B}$ is duplicating, and hence Theorem 2 does not apply. However, we can split $\mathcal{B}$ into the following TRSs $\mathcal{B}'$ and $\mathcal{B}''$:

$$\begin{aligned} \mathcal{B}'&= \{\mathsf {f}(\mathsf {s}(x)) \rightarrow \mathsf {c}(x,\mathsf {f}(x))\}&\mathcal{B}''&= \{\mathsf {c}(x,\mathsf {c}(y,z)) \rightarrow \mathsf {c}(y,\mathsf {c}(x,z))\} \end{aligned}$$

so that Corollary 3 applies. Now, we have $\mathsf {DP}(\mathcal{R}\cup \mathcal{B}') = \{\,\mathsf {f}^\sharp (\mathsf {s}(x)) \rightarrow \mathsf {f}^\sharp (x)\,\}$, whose finiteness can be proved using standard techniques.

Corollary 3 requires the rules in $\mathcal{B}$ that are duplicating or violate the dominance condition to be relatively terminating w.r.t. other rules in $\mathcal{B}$. This is not overly restrictive, as shown by the following two examples.

Example 5

Consider again the TRS $\mathcal{B}$ of Example 3, which is duplicating and nonterminating. We can construct an infinite $\rightarrow _{\mathcal{R}/\mathcal{B}}$-reduction as in Example 3 for any nonempty TRS $\mathcal{R}$; thus, any nonempty TRS is not relatively terminating w.r.t. $\mathcal{B}$.

Example 6

Consider the two TRSs $\mathcal{R}= \{\, \mathsf {a} \rightarrow \mathsf {b} \,\}$ and $\mathcal{B}= \{\, \mathsf {d} \rightarrow \mathsf {c}(\mathsf {a},\mathsf {d}) \,\}$. Note that $\mathcal{R}$ does not dominate $\mathcal{B}$. The DP problem $(\mathsf {DP}(\mathcal{R}), \mathcal{R}\cup \mathcal{B}) = (\emptyset ,\mathcal{R}\cup \mathcal{B})$ is trivially finite. However, $\mathcal{R}$ is not relatively terminating w.r.t. $\mathcal{B}$, as the following infinite derivation exists:

$$ \mathsf {d} \rightarrow _\mathcal{B}\mathsf {c}(\mathsf {a},\mathsf {d}) \rightarrow _\mathcal{R}\mathsf {c}(\mathsf {b},\mathsf {d}) \rightarrow _\mathcal{B}\mathsf {c}(\mathsf {b},\mathsf {c}(\mathsf {a},\mathsf {d})) \rightarrow _\mathcal{R}\mathsf {c}(\mathsf {b},\mathsf {c}(\mathsf {b},\mathsf {d})) \rightarrow _\mathcal{B}\cdots $$

6 Relative Termination and Minimality

A DP chain is said to be minimal if every $t_i^\sharp$ is terminating w.r.t. $\mathcal{R}$. It is well-known that absence of infinite minimal $(\mathsf {DP}(\mathcal{R}),\mathcal{R})$-chains implies absence of infinite $(\mathsf {DP}(\mathcal{R}),\mathcal{R})$-chains and thus termination of $\mathcal{R}$. A couple of techniques, namely usable rules and the subterm criterion have been proposed to prove absence of infinite minimal chains [12].

Unfortunately, for the DP problems produced by our relative termination criteria, the minimality property cannot be assumed. Therefore, usable rules and subterm criterion do not apply in general.

Example 7

Consider the TRSs $\mathcal{R}= \{\, \mathsf {f}(\mathsf {s}(x)) \rightarrow \mathsf {f}(x)\, \}$ and $\mathcal{B}= \{\, \mathsf {inf} \rightarrow \mathsf {s}(\mathsf {inf})\, \}$. Theorem 2 yields the DP problem $(\{ \mathsf {f}^\sharp (\mathsf {s}(x)) \rightarrow \mathsf {f}^\sharp (x) \}, \mathcal{R}\cup \mathcal{B})$, which satisfies the subterm criterion in the argument of $\mathsf {f}^\sharp$. Moreover, since no rule is usable from the dependency pair $\mathsf {f}^\sharp (\mathsf {s}(x)) \rightarrow \mathsf {f}^\sharp (x)$, the usable rule technique would yield the DP problem $(\{ \mathsf {f}^\sharp (\mathsf {s}(x)) \rightarrow \mathsf {f}^\sharp (x) \}, \emptyset )$, which any standard technique proves finite. However, $\mathcal{R}/\mathcal{B}$ is not terminating as the following infinite reduction exists:

$$ \mathsf {f}(\mathsf {s}(\mathsf {inf})) \rightarrow _\mathcal{R}\mathsf {f}(\mathsf {inf}) \rightarrow _\mathcal{B}\mathsf {f}(\mathsf {s}(\mathsf {inf})) \rightarrow _\mathcal{R}\mathsf {f}(\mathsf {inf}) \rightarrow _\mathcal{B}\cdots $$

Nonetheless, we show that both the subterm criterion and usable rules are still applicable when $\mathcal{B}$ satisfies the following condition:

Definition 7

(Quasi-Termination [5]). We say that a TRS $\mathcal{R}$ is quasi-terminating iff the set is finite for every term s.

Now we naturally extend the notion of minimality to relative termination.

Definition 8

(Relative DP Problem). A relative DP problem is a triple of TRSs, written $(\mathcal{P},\mathcal{R}/\mathcal{B})$. A $(\mathcal{P},\mathcal{R}/\mathcal{B})$ -chain is a possibly infinite sequence

and is called minimal if every $t_i$ is $\mathcal{R}/\mathcal{B}$-terminating. The relative DP problem is minimally finite if it admits no infinite minimal chain.

Clearly, finiteness of $(\mathsf {DP}(\mathcal{R}),\mathcal{R}/\mathcal{B})$ is equivalent to that of $(\mathsf {DP}(\mathcal{R}),\mathcal{R}\cup \mathcal{B})$. Hence our previous results hold as well for the corresponding relative DP problems.

When the base $\mathcal{B}$ is quasi-terminating, we can apply the subterm criterion. A simple projection $\pi$ assigns each n-ary symbol $f^\sharp$ an argument position $i \in \{ 1, \dots , n \}$. For a term $t^\sharp = f^\sharp (t_1,\dots ,t_n)$ and $i = \pi (f^\sharp )$, we denote $t_i$ by $\pi (t^\sharp )$. For a relation $\sqsupset$ on terms, $\sqsupset ^\pi$ is defined as follows: $s \sqsupset ^\pi t$ iff $\pi (s) \sqsupset \pi (t)$.

Theorem 3

(Relative Subterm Criterion). Let $\mathcal{B}$ be a quasi-terminating TRS, $(\mathcal{P},\mathcal{R}/\mathcal{B})$ a relative DP problem and $\pi$ a simple projection such that ${\mathcal{P}} \subseteq {\unrhd ^\pi }$. Then, $(\mathcal{P},\mathcal{R}/\mathcal{B})$ is finite if $({\mathcal{P}} \setminus {\rhd ^\pi }, \mathcal{R}/\mathcal{B})$ is finite.

The proof of the above theorem mimics that of [12, Theorem11], but here we need the relative termination of $\rhd /\mathcal{B}$.

The quasi-termination condition also enables the usable rules technique.

Theorem 4

(Relative Usable Rules). If $\mathcal{B}$ is quasi-terminating, then the usable rule argument can be applied to the relative DP problem $(\mathcal{P},\mathcal{R}/\mathcal{B})$.

Proof

(Sketch). The proof basically follows the standard case of [12, Theorem 29]. Note however that we require $\mathcal{B}$ to be quasi-terminating, in order for the interpretation $I_\mathcal {G}$ to be well-defined for all $\mathcal{R}/\mathcal{B}$-terminating terms.   $\square$

It is well-known that, unfortunately, the quasi-termination condition is undecidable [5]. In our implementation, we only use a trivial sufficient condition, size-non-increasingness. We admit that this is quite restrictive, and thus leave it for future work to find more useful syntactic condition for this purpose.

From Example 7, it is clear that the usable rule argument does not apply to the rules in $\mathcal{B}$ if they are not quasi-terminating. Nonetheless, we conjecture that the usable rule argument may be still applicable to the rules in $\mathcal{R}$.

7 Experimental Evaluation

A key technique for proving finiteness of DP problems are reduction pairs [2]: A reduction pair is a well-founded order pair $({\gtrsim },{>})$ on terms such that $\gtrsim$ is closed on contexts and substitutions, and $>$ is closed on substitutions.

Proposition 4

([2, 10]). Let $(\mathcal{P},\mathcal{R})$ be a DP problem and $({\gtrsim },{>})$ a reduction pair such that $\mathcal{P}\cup \mathcal{R}\subseteq {\gtrsim }$. The DP problem $(\mathcal{P},\mathcal{R})$ is finite iff $(\mathcal{P}\setminus {>},\mathcal{R})$ is.

In the experiments, we use the following reduction pairs:

• polynomial interpretations with negative constants [2, 11, 21],

• the lexicographic path order [16],

• the weighted path order with partial status [29], and

• (2- or 3-dimensional) matrix interpretations [6].

Geser [7] proposed a technique to reduce relative termination of TRSs to relative termination of simpler TRSs. This technique is incorporated into the DP framework for proving standard termination, as rule removal processors [10]. We say a reduction pair $({\gtrsim },{>})$ is monotone if $>$ is closed under contexts.

Proposition 5

(Relative Rule Removal Processor). Let $\mathcal{R}$ and $\mathcal{B}$ be TRSs, and $({\gtrsim },{>})$ a monotone reduction pair such that $\mathcal{R}\cup \mathcal{B}\subseteq {\gtrsim }$. Then $\mathcal{R}$ is relatively terminating w.r.t. $\mathcal{B}$ if and only if $\mathcal{R}\setminus {>}$ is relatively terminating w.r.t. $\mathcal{B}\setminus {>}$.

For monotone reduction pairs, we use polynomial and matrix interpretations with top-left elements of coefficients being at least 1 [6].

We implemented our technique into the termination prover NaTT (ver.1.2). In the following, we show the significance of our technique through an experimental evaluation. The experiments⁴ were run on a server equipped with a quad-core Intel Xeon E5-3407v2 processor running at a clock rate of 2.40GHz and 32GB of main memory. NaTT uses z3  4.3.2 ⁵ as a back-end SMT solver.

The first test set consists of the 44 examples in the “TRS Relative” category of the termination problem database (TPDB) 9.0.⁶ The results are presented in the left half of Table 1. In the first two rows, we directly apply Theorem 2 and Corollary 3, and then apply the aforementioned reduction pairs. We observe that they are of limited applicability on the TPDB set of problems due to the non-duplication and dominance conditions. Nonetheless, Corollary 3 could prove relative termination of two problems⁷ which no tools participating in the termination competition 2014 were able to prove. For comparison, we include results for rule removal processors by matrix interpretations in the third row.

We also prepared 44 examples by extending examples of [3] with the random number generator $\mathcal{B}_\mathsf {rand}$ or the commutative list specification $\mathcal{B}_\mathsf {comlist}$. The results are presented in the right half of Table 1. In these examples, the power of our method should be clear. Theorem 2 is already able to prove relative termination of 29 examples, while AProVE succeeds only in 14 examples.

The DP framework allows combining termination proving techniques. In the fourth row, we combine the rule removal processors and the technique presented in this paper. This combination indeed boosts the power of NaTT; e.g., by combining Proposition 5 and Corollary 3, NaTT can prove relative termination for a total of 60 examples (out of 88), while AProVE can only prove it for 41 examples.⁸ Therefore, we can conclude that our technique improves the state-or-the-art methods for proving relative termination.

Table 1. Experiments

8 Related Work

One of the most comprehensive works on relative termination is Geser’s PhD thesis [7]. One of the main results in this work is formulated in Proposition 5 in the previous section. A similar technique has been used, e.g., to prove confluence in [13]. Of course dependency pairs are not considered in [7] since it was introduced almost a decade later. Dependency pairs are considered in [6], but they are mainly used to prove termination of a TRS $\mathcal{R}$ by proving the termination of $\mathsf {DP}(\mathcal{R})/\mathcal{R}$, which is quite a different purpose from ours.

Giesl and Kapur [8] adapted the dependency pair method for proving termination of equational rewriting, a special case of relative termination where the base is symmetric ($\mathcal{B}= \mathcal{B}^{-1}$). For more specific associative-commutative (AC) rewriting, a number of papers exist (e.g., [1]). The key technique behind them is to compute an extension of $\mathcal{R}$ w.r.t. the considered equations. This operation allows symbols in $\mathcal{B}$ (e.g., AC symbols) to be defined also in $\mathcal{R}$, and hence no counterpart of the dominance condition is required. However, such extensions are computable only for certain equations (e.g., AC), and thus they are not appropriate in our setting, where an arbitrary base $\mathcal{B}$ is considered.

The closer approach is [15], where the main aim was proving termination of narrowing [14] by proving relative termination of a corresponding rewrite relation, similarly to [24, 27]. In [15], a first attempt to reduce relative termination to a DP problem is made by requiring $\mathcal{R}$ and $\mathcal{B}$ to form a so called hierarchical combination (HC) [25], i.e., $\mathcal{D}_\mathcal{R}\cap \mathcal{F}_\mathcal{B}= \emptyset$. Unfortunately, we found that [15, Theorem 5] was incorrect since requiring $\mathcal{B}$ to be non-duplicating is also necessary. In fact, Example 3 is a counterexample to [15, Theorem 5]. The present paper corrects and significantly extends [15]; namely, all results in Sects. 3, 5 and 6 are new, and those in Sect. 4 correct and extend the previous result of [15]. Note also that the HC condition of [15] is a special case of our dominance condition. Moreover, we developed an implementation that allowed us to experimentally verify that our technique indeed pays off in practice.

9 Conclusion

In this paper, we have introduced a new approach to proving relative termination by reducing it to DP problems. The relevance of such a result should be clear, since it allows one to prove relative termination by reusing many existing techniques and tools for proving termination within the DP framework. Indeed, such an approach was included in the RTA List of Open Problems (Problem #106). To the best of our knowledge, this work makes the first significant contribution to positively answering this problem. Moreover, as shown in Sect. 7, our method is competitive w.r.t. state-of-the-art provers for the problems in TPDB, and is clearly superior for examples including the generation of random values or the simulation of extra-variables, as discussed in Sect. 1.

As future work, we plan to improve the precision of our technique by extending the DP framework to be more suitable for proving relative termination. We will also continue the research on finding less restrictive conditions on $\mathcal{R}$ and $\mathcal{B}$ so that the technique becomes more widely applicable.