January 01, 1970
Monotonic semantic path orders and weighted path orders are powerful reduction orders for proving termination of term rewrite systems. In this paper we present their simple unification as reduction orders and reduction pairs. We also discuss the use of it as ground total reduction orders.
We present a generalization of monotonic semantic path orders (MSPOs) [1] and weighted path orders (WPOs) [2]. In the FroCoS 2023 paper [3] we showed that WPOs as reduction orders are instances of MSPOs. In this note we adopt the opposite approach: First we introduce a generalization of WPOs dubbed GWPOs, and then show that MSPOs are instances of GWPOs. We see that desirable properties of WPO carry over to GWPOs. Full details on these contributions are found in the first author’s dissertation [4].
This section considers reduction orders, which are well-founded orders on terms that are closed under contexts and substitutions. It is known that a TRS \(\mathcal{R}\) is terminating if and only if there exists a reduction order \(>\) with \(\mathcal{R}\subseteq {>}\).
The basic ingredient of our unified orders (GWPOs) is reduction triples, originally introduced for MSPOs. Formally, a triple \(({\geqslant},{\sqsupseteq}, {\sqsupset})\) is a reduction triple if \(\geqslant\) is a rewrite preorder on terms, \(({\sqsupseteq},{\sqsupset})\) is a stable order pair on terms with \(\sqsupset\) well-founded, and \(\sqsupseteq\) is harmonious to \(\geqslant\). Here, rewrite preorder means preorder (or quasi-order) closed under substitutions and contexts; the stability condition means that \(\sqsupseteq\) and \(\sqsupset\) are both closed under substitutions; and the harmony condition means that \(t_i \geqslant u\) implies \(f(t_1,\ldots,t_i,\ldots,t_n) \sqsupseteq f(t_1,\ldots,u,\ldots,t_n)\) for all \(n\)-ary function symbols \(f\), terms \(t_1, \ldots, t_n, u\) and integers \(1 \leqslant i \leqslant n\).
For example, given a reduction pair \(({\geqslant}, {>})\) (which is a key notion in the dependency pair method [5]), the triple \(({\geqslant}, {\geqslant}, {>})\) is a reduction triple. Also, given a weakly monotone and well-founded algebra \(\mathcal{A}\) (say, a linear polynomial interpretation on natural numbers), the triple \(({\geqslant_\mathcal{A}}, {\geqslant_\mathcal{A}}, {>_\mathcal{A}})\) is a reduction triple. Moreover, given a precedence \(\succeq\), the triple \(({\mathcal{T}\times \mathcal{T}}, {\sqsupseteq}, {\sqsupset})\) is a reduction triple. Here, \(\mathcal{T}\times \mathcal{T}\) is the universal relation relating every pair of terms, and \(\sqsupseteq\) and \(\sqsupset\) are defined as comparison of head symbols w.r.t. \(\succeq\).
We are ready to define the unified order GWPO. Note that it generalizes GWPO in the sense of our earlier paper [3].
Definition 1. Let \(({\sqsupseteq_A}, {\sqsupset_A})\) and \(({\sqsupseteq_B}, {\sqsupset_B})\) be pairs of relations on terms. The generalized weighted path order* \(>_\mathsf{G}\) (GWPO) is defined as follows: \(s >_\mathsf{G}t\) if*
\(s \sqsupset_A t\), or
\(s = f({s_1},\dots,{s_{m}}) \sqsupseteq_A t\) and one of the following conditions holds:
a. \(s_i = t\) or \(s_i >_\mathsf{G}t\) for some \(1 \leqslant i \leqslant m\).
b. \(t = g({t_1},\dots,{t_{n}})\), \(s >_\mathsf{G}t_j\) for all \(1 \leqslant j \leqslant n\), and moreover
i. *$s \sqsupset_B t$, or*
ii. *$s \sqsupseteq_B t$ and
$({s_1},\dots,{s_{m}}) >_\mathsf{G}^\mathsf{lex}({t_1},\dots,{t_{n}})$.*Now, let \(({\geqslant_A}, {\sqsupseteq_A}, {\sqsupset_A})\) and \(({\geqslant_B}, {\sqsupseteq_B}, {\sqsupset_B})\) be triples of relations on terms. The monotonic generalized weighted path order (MGWPO) \(>_\mathsf{MG}\) is the intersection \({\geqslant_A} \cap {\geqslant_B} \cap {>_\mathsf{G}}\) where \(>_\mathsf{G}\) is induced by \(({\sqsupseteq_A}, {\sqsupset_A})\) and \(({\sqsupseteq_B}, {\sqsupset_B})\).
Technically, we take the intersection \({\geqslant_A} \cap {\geqslant_B} \cap {>_\mathsf{G}}\) because \(>_\mathsf{G}\) may not be closed under contexts. This technique is due to Borralleras, Ferreira and Rubio [1].
To simplify the presentation, we globally assume that the signature is finite. A relation \(\leadsto\) on terms is said to have the subterm property if \(s \leadsto t\) holds whenever \(t\) is a proper subterm of \(s\).
Theorem 1. For reduction triples \(({\geqslant_A}, {\sqsupseteq_A}, {\sqsupset_A})\) and \(({\geqslant_B}, {\sqsupseteq_B}, {\sqsupset_B})\) with \(\sqsupseteq_A\) having the subterm property, the induced MGWPO \(>_\mathsf{MG}\) is a reduction order.
Example 1. We show the termination of the TRS \(\mathcal{R}= \{ \mathsf{p}(\mathsf{s}(x)) \to x, \mathsf{f}(\mathsf{s}(x)) \to \mathsf{f}(\mathsf{p}(\mathsf{s}(x))) \}\). Let \(\mathcal{A}\) and \(\mathcal{B}\) be the algebras on \(\mathbb{N}\) with \(\mathsf{p}_\mathcal{A}(x) = \mathsf{f}_\mathcal{A}(x) = x\), \(\mathsf{s}_\mathcal{A}(x) = \mathsf{f}_\mathcal{B}(x) = \mathsf{s}_\mathcal{B}(x) = x + 1\), and \(\mathsf{p}_\mathcal{B}(x) = \max \{ 0, x - 1 \}\). Then \(({\geqslant_\mathcal{A}},{\geqslant_\mathcal{A}},{>_\mathcal{A}})\) and \(({\geqslant_\mathcal{B}},{\geqslant_\mathcal{B}},{>_\mathcal{B}})\) are reduction triples and \({\geqslant_\mathcal{A}}\) has the subterm property. We conclude that \(\mathcal{R}\) is terminating because the induced MGWPO satisfies \(\mathcal{R}\subseteq {>_\mathsf{MG}}\).
A WPO is parameterized by an algebra \(\mathcal{A}\) (assumed weakly simple), and a precedence \(\succeq\). The WPO is identical to the MGWPO whose reduction triple \(A\) is induced from \(\mathcal{A}\) and \(B\) is induced by \(\succeq\). (So actually, the subterm property of \(\sqsupseteq_A\) assumed in 1 is an analog of the weak simplicity of \(\mathcal{A}\) required by the WPO.)
The same goes for the MSPO: An MSPO is parameterized by a single reduction triple \(({\geqslant},{\sqsupseteq}, {\sqsupset})\). The MSPO is identical to the MGWPO whose reduction triple \(A\) is the trivial one \(({\mathcal{T}\times \mathcal{T}}, {\mathcal{T}\times \mathcal{T}}, {\varnothing})\) and \(B\) is \(({\geqslant},{\sqsupseteq}, {\sqsupset})\). Equivalently, the MSPO can be defined as follows.
Definition 2. Let \(({\sqsupseteq}, {\sqsupset})\) be a pair of relations on terms. The semantic path order* \(>_\mathsf{S}\) is defined on terms as follows: \(s >_\mathsf{S}t\) if \(s = f({s_1},\dots,{s_{m}})\) and one of the next conditions holds.*
a. \(s_i = t\) or \(s_i >_\mathsf{S}t\) for some \(1 \leqslant i \leqslant m\).
b. \(t = g({t_1},\dots,{t_{n}})\) and \(s >_\mathsf{S}t_j\) for all \(1 \leqslant j \leqslant n\), and moreover
i. *$s \sqsupset t$, or*
ii. *$s \sqsupseteq t$ and
$({s_1},\dots,{s_{m}}) >_\mathsf{S}^{\mathsf{lex}} ({t_1},\dots,{t_{n}})$.*For a reduction triple \(({\geqslant},{\sqsupseteq}, {\sqsupset})\), The monotonic semantic path order* \(s >_\mathsf{MS}t\) is defined as the intersection \({\geqslant} \cap {>_\mathsf{S}}\), where \(>_\mathsf{S}\) is induced by \(({\sqsupseteq}, {\sqsupset})\).*
Theorem 2 ([1]). Every MSPO is a reduction order.
Conversely, MGWPOs can be seen as instances of MSPOs.
Theorem 3. Let \(>_\mathsf{MG}\) be the MGWPO induced by reduction triples \(({\geqslant_A}, {\sqsupseteq_A}, {\sqsupset_A})\) and \(({\geqslant_B}, {\sqsupseteq_B}, {\sqsupset_B})\) with the subterm property of \(\sqsupseteq_A\). Then \(>_\mathsf{MG}\) and the MSPO \(>_\mathsf{MS}\) are identical, where \(>_\mathsf{MS}\) is induced by \(({\geqslant_A \cap \geqslant_B}, {\sqsupseteq_{AB}}, {\sqsupset_{AB}})\) and \(({\sqsupseteq_{AB}}, {\sqsupset_{AB}})\) is the lexicographic combination of \(({\sqsupseteq_{A}}, {\sqsupset_{A}})\) and \(({\sqsupseteq_{B}}, {\sqsupset_{B}})\).
This is an analog of a main result of the FroCoS paper stating that WPOs are MSPOs [3]. In fact, this result can be traced back to Geser’s observation ([6]) that a version of the Knuth–Bendix order can be simulated by the semantic path order (SPO) [7].
What is the point of having the unified order? One way of defending our GWPO concerns ground totality, which is a crucial property for theorem proving methods like the superposition calculus. On one hand, every WPO \(>_\mathsf{W}\) satisfying totality of the precedence and the ordered algebra is ground total, meaning that either \(s >_\mathsf{W}t\) or \(t >_\mathsf{W}s\) holds for all terms \(s \neq t\). On the other hand, this does not go naturally for the MSPO. Based on this observation, we can construct a distinctive ground-total MGWPO. For instance, we can construct a ground-total MGWPO \(>_\mathsf{MG}\) orienting the equations of the combinators \(\mathsf{S}\) and \(\mathsf{K}\): \[\begin{align} (x \cdot z) \cdot (y \cdot z) & {}>_\mathsf{MG}((\mathsf{S} \cdot x) \cdot y) \cdot z & (\mathsf{K} \cdot x) \cdot y & >_\mathsf{MG}x \end{align}\] Moreover, such an MGWPO can be found by employing the standard techniques for automating path orders. To our knowledge, this is not possible by existing constructions. See [4] for the details of the construction.
Another point, again crucial for theorem proving, is that the MGWPO provides a way to optimize comparison by an MSPO: Given an instance \(>_\mathsf{G}\) of the GWPO, one can conclude \(s >_\mathsf{G}t\) immediately from a strict decrease \(s \sqsupset_A t\), without recursive checks. This is not possible for the simulating SPO \(>_\mathsf{S}\), compare 1 2. Although this does not improve worst-case complexity, one can actually improve it by further imposing the subterm property on the strict order \(\sqsupset_A\).
Let \(({\sqsupseteq_A}, {\sqsupset_A})\) and \(({\sqsupseteq_B}, {\sqsupset_B})\) be order pairs and \(>_\mathsf{G}\) the GWPO induced by them. Suppose that \(\sqsupset_A\) and \(\sqsupseteq_A\) have the subterm property. Then \(s >_\mathsf{G}t\) if and only if
\(s \sqsupset_A t\), or
\(s = f({s_1},\dots,{s_{m}}) \sqsupseteq_A g({t_1},\dots,{t_{n}}) = t\), and one of the following conditions holds:
i. \(s \sqsupset_B t\), or
ii. \(s \sqsupseteq_B t\) and \(({s_1},\dots,{s_{m}}) >_\mathsf{G}^\mathsf{lex}({t_1},\dots,{t_{n}})\)
[prop:kbo-like-gwpo] provides a definition of the GWPO in a similar fashion to the Knuth–Bendix order (KBO). The KBO runs in linear time while the lexicographic path order (LPO) runs in quadratic time (even with the best known algorithm). Combining these, we obtain a procedure for deciding \(s >_\mathsf{MG}t\) in linear complexity in \(|s| + |t|\), where the measure is the number of comparisons by the base relations of the reduction triples \(A\) and \(B\). This is not immediate from the definition of the MSPO which is similar to the LPO.
A reduction pair \(({\geqslant}, {>})\) is an order pair defined on terms such that \(\geqslant\) is a rewrite preorder and \(>\) is a well-founded order closed under substitutions. In its simplest form, the dependency pair method states that a TRS \(\mathcal{R}\) is terminating if and only if there is a reduction pair \(({\geqslant}, {>})\) such that \(\mathcal{R}\subseteq {\geqslant}\) and \(\mathsf{DP}(\mathcal{R}) \subseteq {>}\), where \(\mathsf{DP}(\mathcal{R})\) is the set of dependency pairs, see [5], [8].
Let us consider a reduction pair version of the MGWPO incorporating partial statuses, as is done for the original WPO [2]. A partial status \(\pi\) is a function that maps each \(n\)-ary function symbol to a list \([i_1, \ldots, i_m]\) with \(1 \leqslant i_1 < \cdots < i_m \leqslant n\). For an \(n\)-ary function symbol \(f\) and terms \(t_1, \ldots, t_n\), we write \(\pi(f)(t_1, \ldots, t_n)\) for the list \([t_{i_1}, \ldots, t_{i_m}]\) where \(\pi(f) = [i_1, \ldots, i_m]\), and \(\pi\) is called total if \(\pi(f) = [1,\ldots, n]\) for all \(n\)-ary function symbols \(f\).
Definition 3. Let \(\pi\) be a partial status, and let \(({\geqslant_A}, {\sqsupseteq_A}, {\sqsupset_A})\) and \(({\geqslant_B}, {\sqsupseteq_B}, {\sqsupset_B})\) be triples of relations on terms. The generalized weighted path order \(({\geqslant_\mathsf{G}}, {>_\mathsf{G}})\) is a pair of relations on terms defined simultaneously as follows: \(s \geqslant_\mathsf{G}t\) if
\(s \sqsupset_A t\) or
\(s \sqsupseteq_A t\) and one of the following conditions holds.
a. \(s = f({s_1},\dots,{s_{m}})\) and \(s_i \geqslant_\mathsf{G}t\) for some \(i \in \pi(f)\).
b. \(s = f({s_1},\dots,{s_{m}})\), \(t = g({t_1},\dots,{t_{n}})\), \(s >_\mathsf{G}t_j\) for all \(j \in \pi(g)\), and
i. *$s \sqsupset_B t$ or*
ii. *$s \sqsupseteq_B t$ and
$\pi(f)({s_1},\dots,{s_{m}}) \geqslant_\mathsf{G}^\mathsf{lex}\pi(g)({t_1},\dots,{t_{n}})$.*c. \(s \in \mathcal{V}\) and \(s = t\)
The relation \(>_\mathsf{G}\) is defined by cases 1, 2a and 2b where \(\geqslant_\mathsf{G}^\mathsf{lex}\) is replaced by \(>_\mathsf{G}^\mathsf{lex}\). Here \(({\geqslant_\mathsf{G}^\mathsf{lex}}, {>_\mathsf{G}^\mathsf{lex}})\) is the lexicographic extension of \(({\geqslant_\mathsf{G}}, {>_\mathsf{G}})\). The monotonic generalized weighted path order* \(\geqslant_\mathsf{MG}\) is defined as \({{\geqslant_A} \cap {\geqslant_B} \cap {\geqslant_\mathsf{G}}}\), where \(({\geqslant_\mathsf{G}}, {>_\mathsf{G}})\) is induced by \(({\sqsupseteq_A}, {\sqsupset_A})\) and \(({\sqsupseteq_B}, {\sqsupset_B})\).*
For a partial status \(\pi\), a relation \(\leadsto\) on terms is simple with respect to \(\pi\) if \(f(t_1, \ldots, t_n) \leadsto t_i\) for all \(n\)-ary function symbols \(f\), terms \({t_1},\dots,{t_{n}}\) and \(i \in \pi(f)\). This is a generalized version of the subterm property corresponding to the notion of \(\pi\)-simple algebra for WPOs.
Theorem 4. Let \(\pi\) be a partial status, and \(({\geqslant_A}, {\sqsupseteq_A}, {\sqsupset_A})\) and \(({\geqslant_B}, {\sqsupseteq_B}, {\sqsupset_B})\) reduction triples. If \(\sqsupseteq_A\) is simple with respect to \(\pi\), then \(({\geqslant_\mathsf{MG}}, {>_\mathsf{G}})\) is a reduction pair.
Again, WPOs as reduction pairs can be constructed as GWPOs by constructing \(A\) from algebras and \(B\) from precedences. While we are not aware of a dedicated version of (M)SPOs as reduction pairs in any preceding work, it can be defined as GWPO whose first reduction triple is trivial.
Definition 4. Let \(\pi\) be a partial status, and \(({\geqslant}, {\sqsupseteq}, {\sqsupset})\) a reduction triple. The semantic path order* \(({\geqslant_\mathsf{S}}, {>_\mathsf{S}})\) induced by \(\pi\) and \(({\sqsupseteq}, {\sqsupset})\) is defined inductively as follows: \(s \geqslant_\mathsf{S}t\) if*
\(s = f({s_1},\dots,{s_{m}})\) and \(s_i \geqslant_\mathsf{S}t\) for some \(i \in \pi(f)\).
\(s = f({s_1},\dots,{s_{m}})\), \(t = g({t_1},\dots,{t_{n}})\), \(s >_\mathsf{S}t_j\) for all \(j \in \pi(g)\), and
a. \(s \sqsupset t\) or
b. \(s \sqsupseteq t\) and \(\pi(f)({s_1},\dots,{s_{m}}) \geqslant_\mathsf{S}^\mathsf{lex}\pi(g)({t_1},\dots,{t_{n}})\).
\(s \in \mathcal{V}\) and \(s = t\)
The relation \(>_\mathsf{S}\) is defined by cases 1, 2a and 2b where \(\geqslant_\mathsf{S}^\mathsf{lex}\) is replaced by \(>_\mathsf{S}^\mathsf{lex}\). Here \(({\geqslant_\mathsf{S}^\mathsf{lex}}, {>_\mathsf{S}^\mathsf{lex}})\) is the lexicographic extension of \(({\geqslant_\mathsf{S}}, {>_\mathsf{S}})\). The monotonic semantic path order* \(\geqslant_\mathsf{MS}\) is defined as \({\geqslant} \cap {\geqslant_\mathsf{S}}\), where \(({\geqslant_\mathsf{S}}, {>_\mathsf{S}})\) is induced by \(({\sqsupseteq}, {\sqsupset})\).*
Corollary 1. Let \(\pi\) be a partial status, and \(({\geqslant}, {\sqsupseteq}, {\sqsupset})\) a reduction triple. Then \(({\geqslant_\mathsf{MS}}, {>_\mathsf{S}})\) is a reduction pair.
For a term \(t = f({t_1},\dots,{t_{n}})\) we define \(t^!\) as \(f^!({t_1},\dots,{t_{n}})\). Here \(f^!\) is a fresh function symbol. Let \(\mathcal{A}\) be a weakly monotone well-founded algebra. We write \(s \sqsupseteq_\mathcal{A}t\) if either \(s\) and \(t\) are the same variable or they are not variables and \(s^! \geqslant_\mathcal{A}t^!\). Similarly, we write \(s^! >_\mathcal{A}t^!\) if \(s\) and \(t\) are not variables and \(s^! >_\mathcal{A}t^!\). Then \(({\geqslant_\mathcal{A}},{\sqsupseteq_\mathcal{A}},{\sqsupset_\mathcal{A}})\) is a reduction triple.
Example 2. Consider the TRS \(\mathcal{R}\) taken from the Termination Problem Database (TRS_Standard/Zantema_05/z08):1 \[\begin{align}
\mathsf{f}(\mathsf{a}, \mathsf{f}(\mathsf{b}, \mathsf{f}(\mathsf{a}, x))) & \to \mathsf{f}(\mathsf{a}, \mathsf{f}(\mathsf{b}, \mathsf{f}(\mathsf{b}, \mathsf{f}(\mathsf{a}, x))))
&
\mathsf{f}(\mathsf{b}, \mathsf{f}(\mathsf{b}, \mathsf{f}(\mathsf{b}, x))) & \to \mathsf{f}(\mathsf{b}, \mathsf{f}(\mathsf{b}, x))
\end{align}\] The set \(\mathsf{DP}(\mathcal{R})\) consists of the two dependency pairs: \[\begin{align}
\mathsf{F}(\mathsf{a},\mathsf{f}(\mathsf{b}, \mathsf{f}(\mathsf{a}, x))) &\to \mathsf{F}(\mathsf{a}, \mathsf{f}(\mathsf{b}, \mathsf{f}(\mathsf{b}, \mathsf{f}(\mathsf{a}, x))))
&
\mathsf{F}(\mathsf{a}, \mathsf{f}(\mathsf{b}, \mathsf{f}(\mathsf{a}, x))) \to \mathsf{F}(\mathsf{b}, \mathsf{f}(\mathsf{b}, \mathsf{f}(\mathsf{a}, x)))
\end{align}\] Here, \(\mathsf{F}\) is the tuple symbol for \(\mathsf{f}\) introduced by the dependency pair method. Let \(\mathcal{A}\) be the algebra
on \(\mathbb{N}\) with \(\mathsf{F}^{(!)}_\mathcal{A}(x, y) = \mathsf{f}_\mathcal{A}(x,y) = x\), \(\mathsf{f}^!_\mathcal{A}(x,y) = y\), \(\mathsf{a}^{(!)}_\mathcal{A}= 1\), and \(\mathsf{b}^{(!)}_\mathcal{A}= 0\); and let \(\pi\) be the partial status with \(\pi(\mathsf{F}) = [2]\) and \(\pi(\mathsf{f}) = \pi(\mathsf{a}) = \pi(\mathsf{b}) = [\,]\). The reduction pair \(({\geqslant_\mathsf{MS}},{>_\mathsf{S}})\)
induced from \(({\geqslant_\mathcal{A}},{\sqsupseteq_\mathcal{A}},{\sqsupset_\mathcal{A}})\) satisfies \(\mathcal{R}\subseteq {\geqslant_\mathsf{MS}}\) and \(\mathsf{DP}(\mathcal{R}) \subseteq {>_\mathsf{S}}\), from which we conclude that \(\mathcal{R}\) is terminating. In particular, \(\mathsf{F}(\mathsf{a},\mathsf{f}(\mathsf{b}, \mathsf{f}(\mathsf{a}, x))) >_\mathsf{S}\mathsf{F}(\mathsf{a}, \mathsf{f}(\mathsf{b}, \mathsf{f}(\mathsf{b}, \mathsf{f}(\mathsf{a}, x))))\) follows by case 2b and \(\mathsf{f}(\mathsf{b}, \mathsf{f}(\mathsf{a}, x)) >_\mathsf{S}\mathsf{f}(\mathsf{b}, \mathsf{f}(\mathsf{b}, \mathsf{f}(\mathsf{a}, x)))\), which in turn follows from case 2a and \(\mathsf{f}^{!}(\mathsf{b}, \mathsf{f}(\mathsf{a}, x)) >_\mathcal{A}\mathsf{f}^{!}(\mathsf{b}, \mathsf{f}(\mathsf{b}, \mathsf{f}(\mathsf{a}, x)))\). The last inequality is confirmed by calculation: \[\mathsf{f}^{!}_\mathcal{A}(\mathsf{b}_\mathcal{A}, \mathsf{f}_\mathcal{A}(\underline{\mathsf{a}_\mathcal{A}}, x)) = 1 > 0 = \mathsf{f}^{!}_\mathcal{A}(\mathsf{b}_\mathcal{A},
\mathsf{f}_\mathcal{A}(\underline{\mathsf{b}_\mathcal{A}}, \mathsf{f}_\mathcal{A}(\mathsf{a}_\mathcal{A}, x)))\] The underlined parts correspond to the values \(1\) and \(0\). Note
that WPOs with linear polynomial interpretations are unable to satisfy those inclusions.
Next we investigate an analog of 3. Let \(({\geqslant_\mathsf{MG}}, {>_\mathsf{G}})\) be the generalized weighted path order (3) induced by a partial status \(\pi\) and reduction triples \(({\geqslant_A}, {\sqsupseteq_A}, {\sqsupset_A})\) and \(({\geqslant_B}, {\sqsupseteq_B}, {\sqsupset_B})\), and let \(({\geqslant_\mathsf{MS}}, {>_\mathsf{MS}})\) be the semantic path order (4) induced by \(\pi\) and \(({\geqslant_A \cap \geqslant_B}, {\sqsupseteq_{AB}}, {\sqsupset_{AB}})\).
Theorem 5. Assume that \(\sqsupseteq_A\) is simple with respect to \(\pi\). Then the inclusions \({\geqslant_\mathsf{MS}} \subseteq {\geqslant_\mathsf{MG}}\) and \({>_\mathsf{S}} \subseteq {>_\mathsf{G}}\) hold. If \(\pi\) is total, then \(({\geqslant_\mathsf{MS}}, {>_\mathsf{S}})\) is identical to \(({\geqslant_\mathsf{MG}}, {>_\mathsf{G}})\).
For the second claim, the assumption that \(\pi\) is total is essential.
Example 3. Suppose that the signature only contains a unary function symbol \(\mathsf{f}\). Let \(\pi\) be the partial status with \(\pi(\mathsf{f}) = [\,]\), let \(\mathcal{A}\) be the algebra on \(\mathbb{N}\) defined by \(\mathsf{f}_\mathcal{A}(x) = x + 1\), and let \(({\sqsupseteq_B}, {\sqsupset_B})\) be an arbitrary pair of relations (e.g., one induced by a precedence to consider the original WPO). On one hand, the GWPO \(({\geqslant_\mathsf{G}}, {>_\mathsf{G}})\) induced by \(({\geqslant_\mathcal{A}}, {>_\mathcal{A}})\) and \(({\sqsupseteq_B}, {\sqsupset_B})\) satisfies \(\mathsf{f}(x) \geqslant_\mathsf{G}x\) and \(\mathsf{f}(x) >_\mathsf{G}x\) by case 1. On the other hand, no SPO \(({\geqslant_\mathsf{S}}, {>_\mathsf{S}})\) (regardless of the underlying order pair) satisfies neither \(\mathsf{f}(x) \geqslant_\mathsf{S}x\) nor \(\mathsf{f}(x) >_\mathsf{S}x\), because only possible case 1 is blocked by \(\pi(\mathsf{f}) = [\,]\).
All in all, in the setting of 5 in which \(\sqsupseteq_A\) is simple with respect to \(\pi\), the GWPO is always preferred over the SPO. In contrast, if the simplicity condition is not satisfied, the SPO provides a way to construct a reduction pair (1), by combining the reduction triples \(A\) and \(B\) lexicographically into the single one. In other words, the SPO allows us to virtually bypass the simplicity condition of 4.
In order to evaluate the GWPO and SPO as reduction pairs, we implemented a prototype termination tool based on the dependency pair method and the presented reduction pairs. The problem set for the experiment consists of 1528 finite TRSs from version 11.5 of the Termination Problem Database, and one-minute time limit is set for the benchmark. Overall, one obtains more termination proofs by switching from the original WPO to our methods, see [4] for the details. However, compared to state-of-the-art termination provers, every problem solved by our tool is also solved by AProVE or NaTT. So the authors do not know if any new problem can be solved by our methods.
To grasp the evaluation results, we pick up the following three kinds of reduction pairs:
the WPO induced by a linear polynomial interpretation and a precedence;
the GWPO (4) induced by reduction triples \(A\) and \(B\); and
the SPO (1) induced by the lex combination of reduction triples \(A\) and \(B\).
Here, \(A\) is induced by a linear polynomial interpretation on natural numbers, and for linear polynomial interpretations \(\mathcal{A}\) (including those for the WPO) we demand \(a_1, \ldots, a_n \in \{ 0, 1 \}\) for each interpretation \(f_\mathcal{A}(x_1, \ldots, x_n) = a_0 + a_1 x_1 + \cdots + a_n x_n\). Only for the WPO and the GWPO, we additionally impose simplicity with respect to the partial status. The other reduction triple \(B\) is induced by a max/plus interpretation \(\mathcal{B}\) on natural numbers in which \(b_1, \ldots, b_n \in \{ 0, 1 \}\) and \(c_0 \geqslant 0\) are required for each interpretation \(f_\mathcal{B}(x_1, \ldots, x_n) = \max \{ c_0, b_1 x_1 + c_1, \ldots, b_n x_n + c_n \}\). For \(\mathcal{B}\), the integers \(c_1, \ldots, c_n\) are allowed to be negative. So interpretations like \(f_\mathcal{B}(x) = \max \{0, x - 1 \}\) belong to this class. We construct \(A\) and \(B\) for the SPO and \(B\) for the GWPO in the way described before 2, using fresh symbols \(f^!\). Note that this construction cannot be used for \(A\) of the GWPO due to the simplicity requirement.
In this setting, the WPO, the GWPO, and the SPO (each of which is used with the dependency pair framework) prove termination of 486, 591, and 595 systems, respectively. Actually, the three configurations solve different sets of problems. There are two reasons:
In theory, the GWPO subsumes the WPO as the max/plus interpretation generalizes precedence. However, due to the one-minute time limit imposed in our experiment, the GWPO misses 7 problems handled by the WPO.
Already in theory, the SPO considered here is incomparable with the WPO and the GWPO. In fact, the SPO does not require \(\mathcal{A}\) to be weakly simple with respect to the partial status. So 5 does not apply; see also 3.