Non-termination in Term Rewriting and Logic Programming

Abstract

In this paper, we define two particular forms of non-termination, namely loops and binary chains, in an abstract framework that encompasses term rewriting and logic programming. The definition of loops relies on the notion of compatibility of binary relations. We also present a syntactic criterion for the detection of a special case of binary chains. Moreover, we describe our implementation NTI and compare its results at the Termination Competition 2023 with those of leading analyzers.

1 Introduction

This paper is concerned with the abstract treatment of non-termination in structures where one rewrites elements using indexed binary relations. Such structures can be formalised by abstract reduction systems (ARSs) [2, 30], i.e., pairs $(A,\mathop {\Rightarrow }_{\Pi })$ where A is a set and $\mathop {\Rightarrow }_{\Pi }$ (the rewrite relation) is a union of binary relations on A, indexed by a set $\Pi$, i.e., $\mathop {\Rightarrow }_{\Pi } = \bigcup \{\mathop {\Rightarrow }_{\pi } \mid \pi \in \Pi \}$. Non-termination in this context corresponds to the existence of an infinite rewrite sequence $a_0 \mathop {\Rightarrow }_{\pi _0} a_1 \mathop {\Rightarrow }_{\pi _1} \cdots$. In this introduction, we provide an extended, intuitive, description of the context and content of the paper, with several examples. In Sect. 1.1, we introduce two concrete instances of ARSs. Then, in Sects. 1.2 and 1.3, we consider two special forms of non-termination. Finally, in Sect. 1.4, we describe our implementation.

1.1 Term Rewriting and Logic Programming

Term rewriting and logic programming are concrete instances of ARSs, where $\Pi$ indicates what rule is applied at what position. A crucial difference is that the rewrite relation of term rewriting (denoted by $\mathop {\rightarrow }_{\Pi }$) relies on instantiation while that of logic programming (denoted by $\mathop {\leadsto }_{\Pi }$) relies on narrowing, i.e., on unification.

Example 1.1

In term rewriting, rules are pairs of finite terms. In this context, a term rewrite system (TRS) is a set of rules over a given signature (i.e., a set of function symbols). Consider for instance the TRS that consists of the rules:

$$\begin{aligned} r_1&= \big ({\textsf{f}}(x), {\textsf{g}}({\textsf{h}}(x,\textsf{1}),x)\big ) \\ r_2&= \big (\textsf{1}, \textsf{0}\big ) \\ r_3&= \big ({\textsf{h}}(x,\textsf{0}), {\textsf{f}}^2(x)\big ) = (u_3, v_3) \end{aligned}$$

Here, ${\textsf{g}},{\textsf{h}}$ (resp. ${\textsf{f}}$) are function symbols of arity 2 (resp. 1), $\textsf{0},\textsf{1}$ are constant symbols (i.e., function symbols of arity 0), x is a variable and ${\textsf{f}}^2$ denotes 2 successive applications of ${\textsf{f}}$. Consider the term $s = {\textsf{g}}\big ({\textsf{h}}({\textsf{f}}(x),\textsf{0}),x\big )$. Its subterm $s' = {\textsf{h}}({\textsf{f}}(x),\textsf{0})$ results from applying the substitution $\theta = \{x \mapsto {\textsf{f}}(x)\}$ to $u_3$, denoted as $s' = u_3\theta$, hence it is an instance of $u_3$. Therefore, we have $s \mathop {\rightarrow }_{(r_3,p)} {\textsf{g}}(v_3\theta ,x)$, where p is the position of $s'$ in s and ${\textsf{g}}(v_3\theta ,x)$ results from replacing $s'$ by $v_3\theta$ in s, i.e., $s \mathop {\rightarrow }_{(r_3,p)} {\textsf{g}}({\textsf{f}}^3(x),x)$.

Example 1.2

In logic programming, one rewrites goals (i.e., finite sequences of terms) into goals and a rule is a pair $(u,{\overline{{v}}})$ where u is a term and ${\overline{{v}}}$ is a goal. Moreover, the rewriting always takes place at the root position of an element of a goal. In this context, a logic program (LP) is a set of rules over a given signature.

Consider for instance the LP that consists of the rule:

$$\begin{aligned} r = \big (\underbrace{{\textsf{p}}({\textsf{f}}(x,\textsf{0}))}_u, \underbrace{\langle {{\textsf{p}}(x),{\textsf{q}}(x)}\rangle }_{{\overline{{v}}}}\big ) \end{aligned}$$

Here, ${\textsf{p}},{\textsf{q}}$ (resp. ${\textsf{f}}$) are function symbols of arity 1 (resp. 2), $\textsf{0}$ is a constant symbol and x is a variable. Consider the goal ${\overline{{s}}} = \langle {{\textsf{p}}(\textsf{0}),{\textsf{p}}({\textsf{f}}(x,x)),{\textsf{p}}(x)}\rangle$. The rule $(u_1,\langle {v_1,v'_1}\rangle ) = \big ({\textsf{p}}({\textsf{f}}(x_1,\textsf{0})), \langle {{\textsf{p}}(x_1),{\textsf{q}}(x_1)}\rangle \big )$ is obtained by renaming the variables of r with variables not occurring in ${\overline{{s}}}$. The term $s_1 = {\textsf{p}}({\textsf{f}}(x,x))$ is an element of ${\overline{{s}}}$ and the substitution $\theta = \{x\mapsto \textsf{0}, x_1\mapsto \textsf{0}\}$ is a unifier of $s_1$ and $u_1$, i.e., $s_1\theta = u_1\theta$ (to be precise, $\theta$ is the most general unifier of $s_1$ and $u_1$, see Sect. 2.4). Therefore, we have ${\overline{{s}}} \mathop {\leadsto }_{(r,p)} \langle {{\textsf{p}}(\textsf{0}),v_1,v'_1,{\textsf{p}}(x)}\rangle \theta$, where p is the position of $s_1$ in ${\overline{{s}}}$ and $\langle {{\textsf{p}}(\textsf{0}),v_1,v'_1,{\textsf{p}}(x)}\rangle$ is the goal obtained from ${\overline{{s}}}$ by replacing $s_1$ by the elements of $\langle {v_1,v'_1}\rangle$, i.e., ${\overline{{s}}} \mathop {\leadsto }_{(r,p)} \langle {{\textsf{p}}(\textsf{0}),{\textsf{p}}(\textsf{0}),{\textsf{q}}(\textsf{0}),{\textsf{p}}(\textsf{0})}\rangle$. The operation which is used to rewrite ${\overline{{s}}}$ into $\langle {{\textsf{p}}(\textsf{0}),v_1,v'_1,{\textsf{p}}(x)}\rangle \theta$ is called narrowing. In this example, it is applied at a given position of a goal using an LP rule, but it can be applied similarly at a position p of a term s using a TRS rule (i.e., renaming of the rule with new variables, unification of the subterm of s at position p with the left-hand side of the renamed rule, replacement of the subterm by the right-hand side of the renamed rule and application of the most general unifier to the whole resulting term).

Another difference between term rewriting and logic programming is the effect of a rule application outside the position of the application. For instance, in Example 1.1, the application of $r_3$ at position p of s only affects the subterm of s at position p. In contrast, in Example 1.2, the application of r at position p of ${\overline{{s}}}$ also affects the terms at the other positions, because first $s_1$ is replaced by $v_1$ and $v'_1$ and then the unifier $\theta$ is applied to the whole resulting goal.

Due to these differences, termination in logic programming does not seem related to termination in term rewriting, but rather to termination in the construction of the overlap closure [14], because both use narrowing. The overlap closure of a TRS $\mathcal {R}$, denoted as ${ OC }(\mathcal {R})$, is the (possibly infinite) set defined inductively as follows. It exactly consists of the rules of $\mathcal {R}$, together with the rules resulting from narrowing elements of ${ OC }(\mathcal {R})$ with elements of ${ OC }(\mathcal {R})$. More precisely, suppose that $(u_1,v_1)$ and $(u_2,v_2)$ are in ${ OC }(\mathcal {R})$. Then,

• (Forward closure) $(u_1\theta ,v'_1) \in { OC }(\mathcal {R})$ where $\big (v_1 \mathop {\leadsto }_{((u_2,v_2),p)} v'_1\big )$, $\theta$ is the unifier used and p is the position of a non-variable subterm of $v_1$;

• (Backward closure) $(u'_2,v_2\theta ) \in { OC }(\mathcal {R})$ where $\big (u_2 \mathop {\leadsto }_{((v_1,u_1),p)} u'_2\big )$, $\theta$ is the unifier used and p is the position of a non-variable subterm of $u_2$.

Consider for instance the TRS $\mathcal {R}$ that consists of the rule $r = \big ({\textsf{f}}({\textsf{s}}(x),y), {\textsf{f}}(x,{\textsf{s}}(y))\big )$. It admits no infinite rewrite sequence, but the construction of its overlap closure will not stop as it produces each $\big ({\textsf{f}}({\textsf{s}}^k(x),y), {\textsf{f}}(x,{\textsf{s}}^k(y))\big )$, $k > 0$ (where ${\textsf{s}}^k$ denotes k successive applications of the unary function symbol ${\textsf{s}}$). Now, consider the LP that consists of r (with delimiters $\langle {\cdot }\rangle$ around the right-hand side). It admits the infinite rewrite

$$\begin{aligned} \langle {\,\underbrace{{\textsf{f}}(x,y)}_{a_0}\,}\rangle \mathop {\leadsto }^{\theta _1}_{\pi } \langle {\,\underbrace{{\textsf{f}}(x_1,{\textsf{s}}(y))}_{a_1}\,}\rangle \mathop {\leadsto }^{\theta _2}_{\pi } \langle {\,\underbrace{{\textsf{f}}(x_2,{\textsf{s}}^2(y))}_{a_2}\,}\rangle \mathop {\leadsto }^{\theta _3}_{\pi } \langle {\,\underbrace{{\textsf{f}}(x_3,{\textsf{s}}^3(y))}_{a_3}\,}\rangle \mathop {\leadsto }^{\theta _4}_{\pi } \cdots \end{aligned}$$

where $\pi = (r,\langle {1}\rangle )$ ($\langle {1}\rangle$ is the position of the leftmost term of a goal) and each step is decorated with the corresponding unifier:

$$\begin{aligned} \theta _1&= \{x \mapsto {\textsf{s}}(x_1), y_1 \mapsto y\} \\ \theta _2&= \{x_1 \mapsto {\textsf{s}}(x_2), y_2 \mapsto {\textsf{s}}(y)\} \\ \theta _3&= \{x_2 \mapsto {\textsf{s}}(x_3), y_3 \mapsto {\textsf{s}}^2(y)\} \\&\vdots \end{aligned}$$

This rewrite sequence corresponds to the infinite construction of the overlap closure of $\mathcal {R}$. Indeed, for all $k > 0$, the pair $(a_0\theta _1\dots \theta _k, a_k\theta _1\dots \theta _k)$ corresponds to the rule $\big ({\textsf{f}}({\textsf{s}}^k(x),y), {\textsf{f}}(x,{\textsf{s}}^k(y))\big )$:

$$\begin{aligned} (a_0\theta _1, a_1\theta _1)&= ({\textsf{f}}({\textsf{s}}(x_1),y), {\textsf{f}}(x_1,{\textsf{s}}(y))) \\ (a_0\theta _1\theta _2, a_2\theta _1\theta _2)&= ({\textsf{f}}({\textsf{s}}^2(x_2),y), {\textsf{f}}(x_2,{\textsf{s}}^2(y))) \\&\vdots \end{aligned}$$

1.2 Loops

The vast majority of the papers dealing with non-termination in term rewriting provide conditions for the existence of loops. While sufficient conditions are generally used to design loop-detection approaches [11, 21, 33, 36, 37], necessary conditions are rather used to prove the absence of loops [9, 38]. In this context, a loop refers to a finite rewrite sequence $a_0 \mathop {\rightarrow }_{\Pi } \cdots \mathop {\rightarrow }_{\Pi } a_n$ where $a_n$ embeds an instance of $a_0$. It is well known that then, one can go on from $a_n$, i.e., there is a finite rewrite sequence $a_n \mathop {\rightarrow }_{\Pi } \cdots \mathop {\rightarrow }_{\Pi } a_{n+m}$ where $a_{n+m}$ embeds an instance of $a_n$, hence an instance of $a_0$, and so on. Therefore, there is an infinite rewrite sequence starting from $a_0$ and in which $a_0$ is “reached” periodically (see Example 1.3 below).

The situation in logic programming is different, in the sense that there is no “official” definition of loops (at least, as far as we know). In contrast to term rewriting, where loopingness is a special form of non-termination, logic programming loops simply seem to correspond to infinite rewrite sequences, with no more precision. In this context, [25, 27] provide sufficient conditions for the existence of loops, while [3, 26,27,28] provide necessary conditions. The former are generally used to design static (i.e., compile-time) loop-detection approaches, while the latter are used to design dynamic (i.e., runtime) loop checks (i.e., rewrite sequences are pruned at runtime when it seems appropriate, with a risk of pruning a finite rewrite).

In this paper, we provide a generic definition of loops in any ARS $(A,\mathop {\Rightarrow }_{\Pi })$. It generalises TRS loops by considering any compatible relation $\phi$, not necessarily the “embeds an instance of” relation (see Definition 4.1). Compatibility means that if $a \mathop {\Rightarrow }_{\Pi } a_1$ and $a'$ is related to a via $\phi$ (denoted as $a' \in \phi (a)$) then we have $a' \mathop {\Rightarrow }_{\Pi } a'_1$ for some $a'_1 \in \phi (a_1)$ (see Definition 2.2).

Example 1.3

In Example 1.1, we have the rewrite sequence

$$\begin{aligned} \underbrace{{\textsf{f}}(x)}_{a_0} \mathop {\rightarrow }_{(r_1,p_0)} \underbrace{{\textsf{g}}({\textsf{h}}(x,\textsf{1}),x)}_{a_1} \mathop {\rightarrow }_{(r_2,p_1)} \underbrace{{\textsf{g}}({\textsf{h}}(x,\textsf{0}),x)}_{a_2} \mathop {\rightarrow }_{(r_3,p_2)} \underbrace{{\textsf{g}}({\textsf{f}}^2(x),x)}_{a_3} \end{aligned}$$

(1)

where $p_0=\epsilon$ (i.e., the root position, which is the position of a term inside itself), $p_1$ is the position of $\textsf{1}$ in $a_1$ and $p_2$ is the position of ${\textsf{h}}(x,\textsf{0})$ in $a_2$. Consider $\phi$ that relates any term s to the terms that embed an instance of s, i.e., of the form $c[s\theta ]$, where c is a context (a term with a hole in it), $\theta$ a substitution and $c[s\theta ]$ the term resulting from replacing the hole in c by $s\theta$. It is well known that $\phi$ is compatible with the rewrite relation of term rewriting, i.e., $s' \in \phi (s)$ and $s \mathop {\rightarrow }_{(r,p)} t$ imply that $s' \mathop {\rightarrow }_{(r,p')} t'$ for some position $p'$ and some $t' \in \phi (t)$. We have $a_3 \in \phi (a_0)$ because $a_3 = c[a_0\theta ]$ for $\theta = \{x \mapsto {\textsf{f}}(x)\}$ and $c = {\textsf{g}}(\square ,x)$, where $\square$ is the hole. So, (1) is a loop and, by the compatibility property, there is an infinite rewrite sequence

$$\begin{aligned} a_0 \mathop {\rightarrow }_{(r_1,p_0)} a_1 \mathop {\rightarrow }_{(r_2,p_1)} a_2 \mathop {\rightarrow }_{(r_3,p_2)} \underbrace{a_3}_{\in \phi (a_0)} \mathop {\rightarrow }_{(r_1,p_3)} \underbrace{a_4}_{\in \phi (a_1)} \mathop {\rightarrow }_{(r_2,p_4)} \underbrace{a_5}_{\in \phi (a_2)} \mathop {\rightarrow }_{(r_3,p_5)} \underbrace{a_6}_{\in \phi (a_3)} \mathop {\rightarrow }_{(r_1,p_6)} \cdots \end{aligned}$$

which is a succession of loops.

Example 1.4

In Example 1.2, we have the rewrite sequence

$$\begin{aligned} \underbrace{\langle {{\textsf{p}}({\textsf{f}}(x,\textsf{0}))}\rangle }_{{\overline{{a_0}}}} \mathop {\leadsto }_{(r,\langle {1}\rangle )} \underbrace{\langle {{\textsf{p}}(x),{\textsf{q}}(x)}\rangle }_{{\overline{{a_1}}}} \end{aligned}$$

(2)

Consider $\phi$ that relates any goal ${\overline{{s}}}$ to the goals that embed a more general goal than ${\overline{{s}}}$, i.e., of the form ${\overline{{c}}}[{\overline{{t}}}]$, where ${\overline{{c}}}$ is a context (a goal with a hole in it) and ${\overline{{t}}}$ is more general than ${\overline{{s}}}$, i.e., ${\overline{{s}}} = {\overline{{t}}}\theta$ for some substitution $\theta$ (hence, ${\overline{{s}}}$ is an instance of ${\overline{{t}}}$). We prove in this paper (Lemma 2.17) that $\phi$ is compatible with the rewrite relation of logic programming, i.e., ${\overline{{s'}}} \in \phi ({\overline{{s}}})$ and ${\overline{{s}}} \mathop {\leadsto }_{(r,p)} {\overline{{t}}}$ imply that ${\overline{{s'}}} \mathop {\leadsto }_{(r,p')} {\overline{{t'}}}$ for some position $p'$ and some ${\overline{{t'}}} \in \phi ({\overline{{t}}})$. We have ${\overline{{a_1}}} \in \phi ({\overline{{a_0}}})$ because ${\overline{{a_1}}} = {\overline{{c}}}[{\overline{{b_0}}}]$ where ${\overline{{c}}} = \langle {\square ,{\textsf{q}}(x)}\rangle$ and ${\overline{{b_0}}} = \langle {{\textsf{p}}(x)}\rangle$ is more general than ${\overline{{a_0}}}$ (we have ${\overline{{a_0}}} = {\overline{{b_0}}}\{x \mapsto {\textsf{f}}(x,\textsf{0})\}$). So, (2) is a loop and, by the compatibility property, there is an infinite rewrite sequence

$$\begin{aligned} {\overline{{a_0}}} \mathop {\leadsto }_{(r,\langle {1}\rangle )} \underbrace{{\overline{{a_1}}}}_{\in \phi ({\overline{{a_0}}})} \mathop {\leadsto }_{(r,p_1)} \underbrace{{\overline{{a_2}}}}_{\in \phi ({\overline{{a_1}}})} \mathop {\leadsto }_{(r,p_2)} \underbrace{{\overline{{a_3}}}}_{\in \phi ({\overline{{a_2}}})} \mathop {\leadsto }_{(r,p_3)} \cdots \end{aligned}$$

which is a succession of loops.

1.3 Binary Chains

The infinite rewrite sequence of Example 1.3 (resp. Example 1.4) is a succession of loops that all involve the same sequence $\langle {r_1,r_2,r_3}\rangle$ (resp. $\langle {r}\rangle$) of rules. In this paper, we also consider infinite rewrite sequences that involve two sequences of rules. We call them binary chains (see Definition 5.1).

Example 1.5

Consider the contexts $c = {\textsf{g}}(\square ,\textsf{0},\square )$ and $c' = {\textsf{g}}(\square ,\textsf{1},\square )$ and the TRS that consists of the following rules:

$$\begin{aligned} \begin{array}{ll} r_1 = \big ({\textsf{f}}(x, c[y],x), {\textsf{h}}(x, y)\big ) &{} r_3 = \big ({\textsf{f}}(x, \textsf{0}, x), {\textsf{f}}(c[x], c'[x], c[x])\big ) \\ r_2 = \big ({\textsf{h}}(x, y), {\textsf{f}}(c[x], y, c[x])\big ) &{} r_4 = \big (\textsf{1}, \textsf{0}\big ) \end{array} \end{aligned}$$

We have the infinite rewrite sequence

$$\begin{aligned} \underbrace{{\textsf{f}}\big (c[\textsf{0}],c[\textsf{0}],c[\textsf{0}]\big )}_{a_0}&\mathop {\rightarrow }_{(r_1,\epsilon )} {\textsf{h}}\big (c[\textsf{0}],\textsf{0}\big ) \mathop {\rightarrow }_{(r_2,\epsilon )}{\textsf{f}}\big (c^2[\textsf{0}],\textsf{0},c^2[\textsf{0}]\big ) \\&\mathop {\rightarrow }_{(r_3,\epsilon )} \underbrace{{\textsf{f}}\big (c^3[\textsf{0}], c'[c^2[\textsf{0}]], c^3[\textsf{0}]\big )}_{a'_0} \mathop {\rightarrow }_{(r_4,p_0)} \underbrace{{\textsf{f}}\big (c^3[\textsf{0}], c^3[\textsf{0}], c^3[\textsf{0}]\big )}_{a_1} \\&\mathop {\rightarrow }_{(r_1,\epsilon )} {\textsf{h}}\big (c^3[\textsf{0}],c^2[\textsf{0}]\big ) \mathop {\rightarrow }_{(r_2,\epsilon )}{\textsf{f}}\big (c^4[\textsf{0}],c^2[\textsf{0}],c^4[\textsf{0}]\big ) \\&\mathop {\rightarrow }_{(r_1,\epsilon )} {\textsf{h}}\big (c^4[\textsf{0}],c[\textsf{0}]\big ) \mathop {\rightarrow }_{(r_2,\epsilon )}{\textsf{f}}\big (c^5[\textsf{0}],c[\textsf{0}],c^5[\textsf{0}]\big ) \\&\mathop {\rightarrow }_{(r_1,\epsilon )} {\textsf{h}}\big (c^5[\textsf{0}],\textsf{0}\big ) \mathop {\rightarrow }_{(r_2,\epsilon )}{\textsf{f}}\big (c^6[\textsf{0}],\textsf{0},c^6[\textsf{0}]\big ) \\&\mathop {\rightarrow }_{(r_3,\epsilon )} \underbrace{{\textsf{f}}\big (c^7[\textsf{0}], c'[c^6[\textsf{0}]], c^7[\textsf{0}]\big )}_{a'_1} \mathop {\rightarrow }_{(r_4,p_1)}\underbrace{{\textsf{f}}\big (c^7[\textsf{0}], c^7[\textsf{0}], c^7[\textsf{0}]\big )}_{a_2} \\&\mathop {\rightarrow }_{(r_1,\epsilon )} \cdots \end{aligned}$$

where $c^n$ denotes n embeddings of c into itself and $p_n$ is the position of $\textsf{1}$ (occurring in $c'$) in $a'_n$, for all n in the set $\mathbb {N}$ of non-negative integers. We note that for all $n \in \mathbb {N}$, from $a_n$ to $a_{n+1}$ the sequence $w_1 = \langle {r_1,r_2}\rangle$ is applied several times and then the sequence $w_2 = \langle {r_3,r_4}\rangle$ is applied exactly once. This is written as $a_n \mathop {\left( \mathop {\rightarrow }^*_{w_1} \circ \mathop {\rightarrow }_{w_2}\right) } a_{n+1}$, and hence the infinite rewrite above relies on the two sequences of rules $w_1$ and $w_2$. In Sect. 5.1, we present a syntactic criterion for detecting a special case of this form of non-termination.

1.4 Implementation

Our tool NTI (Non-Termination Inference) [24] performs automatic proofs of non-termination in term rewriting and logic programming. It specifically considers logic programming with Prolog’s leftmost selection rule, i.e., always the leftmost term is chosen in a goal for narrowing (contrary to Example 1.2, where $s_1$ is not the leftmost term of ${\overline{{s}}}$). It applies program transformation techniques as the very first step, namely, the dependency pair unfolding [22] in term rewriting and the binary unfolding [4, 8] in logic programming. The idea is to compute “compressed” forms of finite rewrite sequences that can be used in a simplified setting not polluted by technicalities, such as deeper and deeper embedding of terms (e.g., in Example 1.3, $a_3$ embeds an instance of $a_0$, $a_6$ embeds an instance of $a_3$, ...) This allows us to detect loops using a simplified version of the relations $\phi$ of Examples 1.3 and 1.4, and also to concentrate on rewrite sequences consisting of only one step (as they are “compressions” of longer sequences), see Examples 1.7, 1.8 and 1.10 below.

1.4.1 Dependency Pair Unfolding

The defined symbols of a TRS $\mathcal {R}$ are the function symbols ${\textsf{f}}$ for which there is a rule of the form $({\textsf{f}}(\dots ),\dots )$ in $\mathcal {R}$. Each defined symbol ${\textsf{f}}$ is associated with a symbol ${\textsf{F}}$ of the same arity that does not occur in $\mathcal {R}$. The set of dependency pairs of $\mathcal {R}$ is

$$\begin{aligned} \left\{ \big ({\textsf{F}}(s_1,\dots ,s_n),{\textsf{G}}(t_1,\dots ,t_m)\big ) \;\Bigg \vert \; \begin{array}{l} \big ({\textsf{f}}(s_1,\dots ,s_n),t\big ) \in \mathcal {R}\\ {\textsf{g}}(t_1,\dots ,t_m) \text { is a subterm of } t \\ {\textsf{g}}\text { is a defined symbol of }\mathcal {R}\end{array} \right\} \end{aligned}$$

The technique of [22] transforms a TRS $\mathcal {R}$ into a (possibly infinite) set ${ Unf }(\mathcal {R})$ inductively defined as follows. It exactly consists of the dependency pairs of $\mathcal {R}$, together with the rules resulting from narrowing (forwards and backwards, as for ${ OC }(\mathcal {R})$) elements of ${ Unf }(\mathcal {R})$ with rules and dependency pairs of $\mathcal {R}$; while dependency pairs are only applied at the root position, between the application of two dependency pairs there can be an arbitrary number of narrowing steps below the root, using rules of $\mathcal {R}$. The computation of ${ Unf }(\mathcal {R})$ is hence very similar to that of ${ OC }(\mathcal {R})$, except that: it also considers the dependency pairs, it only uses the initial dependency pairs and rules for narrowing elements of ${ Unf }(\mathcal {R})$ and it allows narrowing of variable subterms.

Theorem 1.6

[22] Let $\mathcal {R}$ be a TRS. If a term ${\textsf{F}}(s_1,\dots ,s_n)$ starts an infinite rewrite sequence w.r.t. ${ Unf }(\mathcal {R})$ then the term ${\textsf{f}}(s_1,\dots ,s_n)$ starts an infinite rewrite sequence w.r.t. $\mathcal {R}$.

Note that this theorem only states an implication, not an equivalence, contrary to Theorem 1.9 below in logic programming (where an “if and only if” is stated). Therefore, we do not know whether it is restrictive to detect infinite rewrite sequences w.r.t. ${ Unf }(\mathcal {R})$, instead of $\mathcal {R}$ (i.e., we do not know whether the existence of an infinite rewrite sequence w.r.t. $\mathcal {R}$ necessarily implies that of an infinite rewrite sequence w.r.t. ${ Unf }(\mathcal {R})$).

Example 1.7

(Example 1.3 continued) Let $\mathcal {R}$ be the TRS under consideration. The following rules are dependency pairs of $\mathcal {R}$ obtained from $r_1$ and $r_3$ respectively:

$$\begin{aligned} r'_1 = \big ({\textsf{F}}(x), {\textsf{H}}(x,\textsf{1})\big ) = (u'_1, v'_1) \qquad r'_3 = \big ({\textsf{H}}(x,\textsf{0}), {\textsf{F}}({\textsf{f}}(x))\big ) \end{aligned}$$

Here, $r'_1$ allows us to get rid of the context $c = {\textsf{g}}(\square ,x)$ that occurs in $r_1$. Let us simplify $\phi$ into the relation $\phi '$ that binds any term to its instances (so, compared to $\phi$, there are no more contexts). Of course, $\phi '$ is also compatible with the rewrite relation of term rewriting.

We have $v'_1 \mathop {\leadsto }_{(r_2,p')} {\textsf{H}}(x,\textsf{0})$ where $p'$ is the position of $\textsf{1}$ in $v'_1$; so, from $r'_1$ and $r_2$, the technique of [22] produces $r''_1 = \big ({\textsf{F}}(x), {\textsf{H}}(x,\textsf{0})\big ) = (u''_1,v''_1)$. Moreover, $v''_1 \mathop {\leadsto }_{(r'_3,\epsilon )} {\textsf{F}}({\textsf{f}}(x))$ so, from $r''_1$ and $r'_3$, we get $r = \big ({\textsf{F}}(x), {\textsf{F}}({\textsf{f}}(x))\big )$.

Let $\pi = (r,\epsilon )$. We have the following loop w.r.t. $\phi '$:

$$\begin{aligned} \overbrace{{\textsf{F}}(x)}^{a'_0} \mathop {\rightarrow }_{\pi } \overbrace{{\textsf{F}}({\textsf{f}}(x))}^{a'_1 \in \phi '(a'_0)} \end{aligned}$$

Hence, there is an infinite rewrite sequence $a'_0 \mathop {\rightarrow }_{\pi } a'_1 \mathop {\rightarrow }_{\pi } a'_2 \mathop {\rightarrow }_{\pi } \cdots$ with $a'_1 \in \phi '(a'_0)$, $a'_2 \in \phi '(a'_1)$, ... It corresponds to that of Example 1.3, but each successive application of $r_1,r_2,r_3$ has been “compressed” into a single application of r. Moreover, it does not involve c, as well as the context that embeds an instance of $a_1$ in $a_4$, etc. By Theorem 1.6, ${\textsf{f}}(x)$ starts an infinite rewrite sequence w.r.t. $\mathcal {R}$.

Example 1.8

The following dependency pairs are obtained respectively from the rules $r_1$, $r_2$ and $r_3$ of the TRS $\mathcal {R}$ of Example 1.5:

$$\begin{aligned} r'_1&= \big ({\textsf{F}}(x, c[y], x), {\textsf{H}}(x, y)\big ) \\ r'_2&= \big ({\textsf{H}}(x, y), {\textsf{F}}(c[x], y, c[x])\big ) \\ r'_3&= \big ({\textsf{F}}(x, \textsf{0}, x), {\textsf{F}}(c[x], c'[x], c[x])\big ) \end{aligned}$$

From $r'_1$ and $r'_2$, the technique of [22] produces $r''_1 = \big ({\textsf{F}}(x, c[y], x), {\textsf{F}}(c[x], y, c[x])\big )$ and, from $r'_3$ and $r_4$, it produces $r''_3 = \big ({\textsf{F}}(x, \textsf{0}, x), {\textsf{F}}(c[x], c[x], c[x])\big )$. Let $\pi _1 = (r''_1,\epsilon )$, $\pi _3 = (r''_3,\epsilon )$ and $A_n = {\textsf{F}}\big (c^n[\textsf{0}],c^n[\textsf{0}],c^n[\textsf{0}]\big )$ for all $n \in \mathbb {N}$. We have the binary chain:

$$\begin{aligned} A_1 \mathop {\rightarrow }_{\pi _1} {\textsf{F}}\big (c^2[\textsf{0}],\textsf{0},c^2[\textsf{0}]\big ) \mathop {\rightarrow }_{\pi _3} A_3 \mathop {\rightarrow }^3_{\pi _1} {\textsf{F}}\big (c^6[\textsf{0}],\textsf{0},c^6[\textsf{0}]\big ) \mathop {\rightarrow }_{\pi _3} A_7 \mathop {\rightarrow }^7_{\pi _1} \cdots \end{aligned}$$

It corresponds to that of Example 1.5, but each application of $w_1$ (resp. $w_2$) has been “compressed” into an application of $r''_1$ (resp. $r''_3$). By Theorem 1.6, ${\textsf{f}}\big (c[\textsf{0}],c[\textsf{0}],c[\textsf{0}]\big )$ starts an infinite rewrite sequence w.r.t. $\mathcal {R}$.

1.4.2 Binary Unfolding

The binary unfolding [4, 8] is a program transformation technique that has been introduced in the context of Prolog’s leftmost selection rule. It transforms a LP P into a (possibly infinite) set ${ Binunf }(P)$ of binary rules (i.e., rules, the right-hand side of which is a goal that contains at most one term) inductively defined as follows: ${ Binunf }(P)$ exactly consists of the rules constructed by narrowing prefixes of right-hand sides of rules of P using elements of ${ Binunf }(P)$; more precisely, for all $(u,\langle {v_1,\dots ,v_n}\rangle ) \in P$:

• (A) for each $1 \le i \le n$, the goals $\langle {v_1}\rangle ,\dots ,\langle {v_{i-1}}\rangle$ are narrowed, respectively, with $(u_1,\epsilon ),\dots ,(u_{i-1},\epsilon )$ from ${ Binunf }(P)$ (where $\epsilon$ is the empty goal) to obtain a corresponding instance of $(u,\langle {v_i}\rangle )$,

• (B) for each $1 \le i \le n$, the goals $\langle {v_1}\rangle ,\dots ,\langle {v_{i-1}}\rangle$ are narrowed, respectively, with $(u_1,\epsilon ),\dots ,(u_{i-1},\epsilon )$ from ${ Binunf }(P)$ and $\langle {v_i}\rangle$ is also narrowed with $(u_i,\langle {v}\rangle )$ from ${ Binunf }(P)$ to obtain a corresponding instance of $(u,\langle {v}\rangle )$,

• (C) $\langle {v_1}\rangle ,\dots ,\langle {v_n}\rangle$ are narrowed, respectively, with $(u_1,\epsilon ),\dots ,(u_n,\epsilon )$ from ${ Binunf }(P)$ to obtain a corresponding instance of $(u,\epsilon )$.

Intuitively, each generated binary rule $(u,\langle {v}\rangle )$ specifies that, w.r.t. the leftmost selection rule, $\langle {u}\rangle$ can be rewritten, using rules of P, to a goal $\langle {v,\dots }\rangle$.

Theorem 1.9

[4] Let P be a LP and ${\overline{{s_0}}}$ be a goal. Assume that the leftmost selection rule is used. Then, ${\overline{{s_0}}}$ starts an infinite rewrite sequence w.r.t. P if and only if it starts an infinite rewrite sequence w.r.t. ${ Binunf }(P)$.

So, in this context, suppose that ${\overline{{s_0}}}$ has the form $\langle {v_0,\dots ,v_n}\rangle$ and that it starts an infinite rewrite sequence w.r.t. P. Then, by Theorem 1.9, there is an infinite rewrite sequence

$$\begin{aligned} {\overline{{s_0}}} \mathop {\leadsto }^{\theta _0}_{(r_0,p_0)} {\overline{{s_1}}} \mathop {\leadsto }^{\theta _1}_{(r_1,p_1)} \cdots \end{aligned}$$

(3)

where $r_0,r_1,\dots$ are rules of ${ Binunf }(P)$ (we decorate each step with the corresponding unifier). As the leftmost selection rule is used, $p_i$ is the position of the leftmost term of ${\overline{{s_i}}}$, for all $i \in \mathbb {N}$. So, necessarily, there is a finite (possibly empty) prefix of (3) that “erases” a (possibly empty) prefix of ${\overline{{s_0}}}$, i.e., it has the form ${\overline{{s_0}}} \mathop {\leadsto }^{\theta _0}_{(r_0,p_0)} \cdots \mathop {\leadsto }^{\theta _{m-1}}_{(r_{m-1},p_{m-1})} {\overline{{s_m}}}$ with ${\overline{{s_m}}} = \langle {v_k,\dots ,v_n}\rangle \theta _0\dots \theta _{m-1}$ and ${\overline{{t_m}}} = \langle {v_k\theta _0\dots \theta _{m-1}}\rangle$ starts an infinite rewrite sequence of the form ${\overline{{t_m}}} \mathop {\leadsto }_{(r_m,p'_m)} {\overline{{t_{m+1}}}} \mathop {\leadsto }_{(r_{m+1},p'_{m+1})} \cdots$. As the goal ${\overline{{t_m}}}$ is a singleton and the rules $r_m,r_{m+1},\dots$ are binary, we necessarily have that ${\overline{{t_{m+1}}}},{\overline{{t_{m+2}}}},\dots$ are singletons and $p'_m = p'_{m+1} = \cdots = \langle {1}\rangle$ (because, in logic programming, rewriting only takes place at the root position of a term of a goal).

So, from the non-termination point of view, and as far as Prolog’s leftmost selection rule is concerned, it is not restrictive to consider a simplified form of logic programming where one only rewrites singleton goals using binary rules. Indeed, we have shown above that if P is non-terminating in the full setting then ${ Binunf }(P)$ is necessarily non-terminating in this simplified one. Moreover, the leftmost selection rule is the most used by far (e.g., it is the only considered one in the Termination Competition [31]). In Sect. 3, for all LPs P, we define a rewrite relation $\mathop {\hookrightarrow }_P$ that models this simplified form of logic programming. It enjoys an interesting closure property (Lemma 3.6) that we will use to detect binary chains (Sect. 5.1).

Example 1.10

In Example 1.4, the binary unfolding of the LP P under consideration produces the rule $r' = \big ({\textsf{p}}({\textsf{f}}(x,\textsf{0})), \langle {{\textsf{p}}(x)}\rangle \big )$ from r (using (A) in the definition of ${ Binunf }(P)$ above, with $i = 1$). So, compared to r, we do not have the context ${\overline{{c}}} = \langle {\square ,{\textsf{q}}(x)}\rangle$ anymore and we can simplify $\phi$, i.e., we consider $\phi '$ that relates any goal ${\overline{{s}}}$ to all the goals that are more general than ${\overline{{s}}}$. Of course, $\phi '$ is also compatible with the rewrite relation of LPs. Let $\pi = (r',\langle {1}\rangle )$. We have this loop w.r.t. $\phi '$:

$$\begin{aligned} \underbrace{\langle {{\textsf{p}}({\textsf{f}}(x,\textsf{0}))}\rangle }_{{\overline{{a_0}}}} \mathop {\leadsto }_{\pi } \underbrace{\langle {{\textsf{p}}(x)}\rangle }_{{\overline{{b_0}}} \in \phi '({\overline{{a_0}}})} \end{aligned}$$

Hence, there is an infinite rewrite sequence ${\overline{{a_0}}} \mathop {\leadsto }_{\pi } {\overline{{b_0}}} \mathop {\leadsto }_{\pi } {\overline{{b_1}}} \mathop {\leadsto }_{\pi } \cdots$ where ${\overline{{b_0}}} \in \phi '({\overline{{a_0}}})$, ${\overline{{b_1}}} \in \phi '({\overline{{b_0}}})$, ... It corresponds to that of Example 1.4, but it does not involve the context that embeds a more general goal than ${\overline{{a_0}}}$ in ${\overline{{a_1}}}$, the context that embeds a more general goal than ${\overline{{a_1}}}$ in ${\overline{{a_2}}}$, ...; moreover, as ${\overline{{a_0}}}, {\overline{{b_0}}}, {\overline{{b_1}}}, \dots$ consist of only one term, the narrowing steps are all performed at position $\langle {1}\rangle$. By Theorem 1.9, ${\overline{{a_0}}}$ starts an infinite rewrite sequence w.r.t. P.

1.5 Content of the Paper

After presenting some preliminary material in Sect. 2 and abstract reduction systems in Sect. 3, we describe, in a generic way, loops in Sect. 4 and binary chains in Sect. 5, together with an automatable approach for the detection of the latter. Then, in Sect. 6, we compare our implementation NTI with the tools that participated in the Termination Competition 2023 [31]. Finally, we present related work in Sect. 7 and conclude in Sect. 8.

2 Preliminaries

We introduce some basic notations and definitions. First, in Sect. 2.1, we consider finite sequences and, in Sect. 2.2, binary relations and the related notions of chain and compatibility. Then, in Sects. 2.3 and 2.4, we define terms, contexts, substitutions and unifiers. Finally, in Sect. 2.5, we present term rewriting and logic programming.

We let $\mathbb {N}$ denote the set of non-negative integers.

2.1 Finite Sequences

Let A be a set. We let ${\overline{{A}}}$ denote the set of finite sequences of elements A; it includes the empty sequence, denoted as $\epsilon$. We generally (but not always) use the delimiters $\langle {\cdot }\rangle$ for writing elements of ${\overline{{A}}}$. Moreover, we use juxtaposition to denote the concatenation operation, e.g., $\langle {a_0,a_1}\rangle \langle {a_2,a_3}\rangle = \langle {a_0,a_1,a_2,a_3}\rangle$ and $a_0\langle {a_1,a_2}\rangle = \langle {a_0,a_1,a_2}\rangle$. The length of $w \in {\overline{{A}}}$ is denoted as $\vert {w} \vert$ and is inductively defined as: $\vert {w} \vert = 0$ if $w = \epsilon$ and $\vert {w} \vert = 1 + \vert {w'} \vert$ if $w = aw'$ for some $a \in A$ and $w' \in {\overline{{A}}}$.

2.2 Binary Relations

A binary relation $\psi$ from a set A to a set B is a subset of $A \times B$. For all $a \in A$, we let $\psi (a) = \{b \in B \mid (a,b) \in \psi \}$. Instead of $(a,b) \in \psi$, we may write $a \mathop {\psi } b$ (e.g., for binary relations that have the form of an arrow) or $b \in \psi (a)$. We let $\psi ^{-1} = \{(b,a) \in B \times A \mid (a,b) \in \psi \}$ be the inverse of $\psi$. A function f from A to B is a binary relation from A to B which is such that for all $a \in A$, f(a) consists of exactly one element.

A binary relation $\phi$ on a set A is a subset of $A^2 = A \times A$. For all $\varphi \subseteq A^2$, we let $\phi \circ \varphi$ denote the composition of $\phi$ and $\varphi$:

$$\begin{aligned} \phi \circ \varphi = \left\{ (a,a') \in A^2 \;\Bigg \vert \; \exists a_1 \in A \ (a,a_1) \in \phi \wedge (a_1,a') \in \varphi \right\} \end{aligned}$$

We let $\phi ^0$ be the identity relation and, for any $n\in \mathbb {N}$, $\phi ^{n+1}=\phi ^n \circ \phi$. Moreover, $\phi ^+ = \cup \{\phi ^n \mid n > 0 \}$ (resp. $\phi ^* = \phi ^0 \mathop {\cup } \phi ^+$) denotes the transitive (resp. reflexive and transitive) closure of $\phi$.

Definition 2.1

Let $\phi$ be a binary relation on a set A. A $\phi$-chain, or simply chain if $\phi$ is clear from the context, is a (possibly infinite) sequence $a_0, a_1, \dots$ of elements of A such that $a_{n+1} \in \phi (a_n)$ for all $n \in \mathbb {N}$. For binary relations that have the form of an arrow, e.g., $\mathop {\Rightarrow }$, we simply write it as $a_0 \mathop {\Rightarrow }a_1 \mathop {\Rightarrow }\cdots$.

The next definition resembles that of a simulation relation [20] in a state transition system: $\mathop {\Rightarrow }$ corresponds to the transition relation of the system and $\phi$ to the simulation.

Definition 2.2

Let A be a set. We say that $\mathop {\Rightarrow }\subseteq A^2$ and $\phi \subseteq A^2$ are compatible if for all $a,a',a_1 \in A$ there exists $a'_1 \in A$ such that

$$\begin{aligned} \left( a' \in \phi (a) \wedge a \mathop {\Rightarrow }a_1\right) \text { implies } \left( a'_1 \in \phi (a_1) \wedge a' \mathop {\Rightarrow }a'_1\right) \end{aligned}$$

Equivalently, $(\phi ^{-1} \circ {\mathop {\Rightarrow }}) \subseteq ({\mathop {\Rightarrow }} \circ \phi ^{-1})$. This is illustrated by the following diagram:

(solid (resp. dashed) arrows represent universal (resp. existential) quantification).

The following result is straightforward.

Lemma 2.3

Let $\mathop {\Rightarrow }$, $\hookrightarrow$ and $\phi$ be binary relations on a set A. If $\mathop {\Rightarrow }$ and $\phi$ are compatible and $\hookrightarrow$ and $\phi$ are compatible then $(\mathop {\Rightarrow }\circ \hookrightarrow )$ and $\phi$ are compatible.

Proof

Using the same notations as in Definition 2.2, we have:

$\square$

2.3 Terms

We use the same definitions and notations as [2] for terms.

Definition 2.4

A signature $\Sigma$ is a set of function symbols, each element of which has an arity in $\mathbb {N}$, which is the number of its arguments. For all $n\in \mathbb {N}$, we denote the set of all n-ary elements of $\Sigma$ by $\Sigma ^{(n)}$. The elements of $\Sigma ^{(0)}$ are called constant symbols.

Function symbols are denoted by letters or non-negative integers in the sans serif font, e.g., ${\textsf{f}},{\textsf{g}}$ or $\textsf{0},\textsf{1}$. We frequently use the superscript notation to denote several successive applications of a unary function symbol, e.g., ${\textsf{s}}^3(\textsf{0})$ is a shortcut for ${\textsf{s}}({\textsf{s}}({\textsf{s}}(\textsf{0})))$ and ${\textsf{s}}^0(\textsf{0}) = \textsf{0}$.

Definition 2.5

Let $\Sigma$ be a signature and X be a set of variables disjoint from $\Sigma$. The set $T(\Sigma , X)$ is defined as:

• $X \subseteq T(\Sigma , X)$,

• for all $n\in \mathbb {N}$, all ${\textsf{f}}\in \Sigma ^{(n)}$ and all $s_1,\dots ,s_n \in T(\Sigma , X)$, ${\textsf{f}}(s_1,\dots ,s_n) \in T(\Sigma , X)$.

For all $s \in T(\Sigma , X)$, we let $Var (s)$ denote the set of variables occurring in s. Moreover, for all $\langle {s_1,\dots ,s_n}\rangle \in {\overline{{T(\Sigma , X)}}}$, we let $Var (\langle {s_1,\dots ,s_n}\rangle ) = Var (s_1) \cup \cdots \cup Var (s_n)$.

In order to simplify the statement of the definitions and theorems of this paper, from now on we fix a signature $\Sigma$, an infinite countable set X of variables disjoint from $\Sigma$ and a constant symbol $\square$ which does not occur in $\Sigma \cup X$.

Definition 2.6

A term is an element of $T(\Sigma , X)$ and a goal an element of ${\overline{{T(\Sigma , X)}}}$. Moreover, a context is an element of $T(\Sigma \cup \{\square \}, X)$ that contains at least one occurrence of $\square$ and a goal-context is a finite sequence of the form $\langle {s_1,\dots ,s_i,\square ,s_{i+1},\dots ,s_n}\rangle$ where all the $s_i$’s are terms. A context c can be seen as a term with “holes”, represented by $\square$, in it. For all $t \in T(\Sigma \cup \{\square \}, X)$, we let c[t] denote the element of $T(\Sigma \cup \{\square \}, X)$ obtained from c by replacing all the occurrences of $\square$ by t. We use the superscript notation for denoting several successive embeddings of a context into itself: $c^0 = \square$ and, for all $n \in \mathbb {N}$, $c^{n+1} = c[c^n]$. Identically, a goal-context ${\overline{{c}}}$ can be seen as a goal with a hole, represented by $\square$. For all ${\overline{{t}}} \in {\overline{{T(\Sigma , X)}}}$, we let ${\overline{{c}}}[{\overline{{t}}}]$ denote the goal obtained from ${\overline{{c}}}$ by replacing $\square$ by the elements of ${\overline{{t}}}$.

Terms are generally denoted by a, s, t, u, v, variables by x, y, z and contexts by c, possibly with subscripts and primes. Goals and goal-contexts are denoted using an overbar.

The notion of position in a term is needed to define the operational semantics of term rewriting (see Definition 2.14).

Definition 2.7

The set of positions of $s\in T(\Sigma \cup \{\square \}, X)$, denoted as ${ Pos }(s)$, is a subset of ${\overline{{\mathbb {N}}}}$ which is inductively defined as:

• if $s \in X$, then ${ Pos }(s) = \{\epsilon \}$,

• if $s = {\textsf{f}}(s_1,\dots ,s_n)$ then ${ Pos }(s) = \{\epsilon \} \cup \bigcup _{i = 1}^n \{ip \mid p \in { Pos }(s_i)\}$.

The position $\epsilon$ is called the root position of s and the function or variable symbol at this position is the root symbol. For all $p\in { Pos }(s)$, the subterm of s at position p, denoted by ${s} \vert _{p}$ is inductively defined as: ${s} \vert _{\epsilon } = s$ and ${{\textsf{f}}(s_1,\dots ,s_n)} \vert _{ip'} = {s_i} \vert _{p'}$. Moreover, for all $t\in T(\Sigma , X)$, we denote by $s[t]_p$ the term that is obtained from s by replacing the subterm at position p by t, i.e., $s[t]_{\epsilon } = t$ and ${\textsf{f}}(s_1,\dots ,s_n)[t]_{ip'} = {\textsf{f}}(s_1,\dots ,s_i[t]_{p'},\dots ,s_n)$.

2.4 Substitutions

Definition 2.8

The set $S(\Sigma , X)$ of all substitutions consists of the functions $\theta$ from X to $T(\Sigma , X)$ such that $\theta (x) \ne x$ for only finitely many variables x. The domain of $\theta$ is the finite set ${ Dom }(\theta )=\{x \in X \mid \theta (x) \ne x\}$. We usually write $\theta$ as $\{x_1\mapsto \theta (x_1), \dots , x_n\mapsto \theta (x_n)\}$ where $\{x_1,\dots ,x_n\} = { Dom }(\theta )$. A (variable) renaming is a substitution that is a bijection on X.

The application of a substitution $\theta$ to a term or context s is denoted as $s\theta$ and is defined as:

• $s\theta = \theta (s)$ if $s\in X$,

• $s\theta = {\textsf{f}}(s_1\theta ,\dots ,s_n\theta )$ if $s = {\textsf{f}}(s_1,\dots ,s_n)$.

This is extended to goals, i.e., $\langle {s_1,\dots ,s_n}\rangle \theta = \langle {s_1\theta ,\dots ,s_n\theta }\rangle$.

Definition 2.9

Let $s,t \in T(\Sigma , X)$. We say that t is an instance of s if $t=s\theta$ for some $\theta \in S(\Sigma , X)$. Then, we also say that s is more general than t. If $\theta$ is a renaming, then t is also called a variant of s. These definitions straightforwardly extend to all ${\overline{{s}}}, {\overline{{t}}} \in {\overline{{T(\Sigma , X)}}}$.

Definition 2.10

The composition of substitutions $\sigma$ and $\theta$ is the substitution denoted as $\sigma \theta$ and defined as: for all $x \in X$, $\sigma \theta (x) = (\sigma (x))\theta$. We say that $\sigma$ is more general than $\theta$ if $\theta =\sigma \eta$ for some substitution $\eta$.

The composition of substitutions is an associative operation, i.e., for all terms s and all substitutions $\sigma$ and $\theta$, $(s\sigma )\theta =s(\sigma \theta )$. We use the superscript notation for denoting several successive compositions of a substitution with itself: $\theta ^0=\emptyset$ (the identity substitution) and, for all $n\in \mathbb {N}$, $\theta ^{n+1}=\theta \theta ^n=\theta ^n\theta$.

Definition 2.11

Let $s,t \in T(\Sigma , X)$. We say that s unifies with t (or that s and t unify) if $s\sigma =t\sigma$ for some $\sigma \in S(\Sigma , X)$. Then, $\sigma$ is called a unifier of s and t and ${ mgu }(s,t)$ denotes the most general unifier (mgu) of s and t, which is unique (up to variable renaming).

We will frequently refer to the relations “embeds an instance of” (denoted as ${ ins }$) and “embeds a more general term than” (denoted as ${ mg }$) defined as:

Definition 2.12

Using the usual notations for terms (s, t), goals (${\overline{{s}}},{\overline{{t}}}$), contexts (c) and goal-contexts (${\overline{{c}}}$), we define:

$$\begin{aligned} { ins }&= \left\{ \left( s,c[t]\right) \;\Bigg \vert \; t \text { is an instance of } s \right\} \cup \left\{ \left( {\overline{{s}}},{\overline{{c}}}[{\overline{{t}}}]\right) \;\Bigg \vert \; {\overline{{t}}} \text { is an instance of } {\overline{{s}}} \right\} \\ { mg }&= \left\{ \left( s,c[t]\right) \;\Bigg \vert \; t \text { is more general than } s \right\} \cup \left\{ \left( {\overline{{s}}},{\overline{{c}}}[{\overline{{t}}}]\right) \;\Bigg \vert \; {\overline{{t}}} \text { is more general than } {\overline{{s}}} \right\} \end{aligned}$$

2.5 Term Rewriting and Logic Programming

We refer to [2, 30] for the basics of term rewriting and to [1, 17] for those of logic programming. For the sake of simplicity and harmonisation, we consider the following notion of rule that encompasses TRS rules and LP rules (usually, the right-hand side of a TRS rule is a term, see Sect. 1.1).

Definition 2.13

A program is a subset of $T(\Sigma , X)\times {\overline{{T(\Sigma , X)}}}$, every element $(u,{\overline{{v}}})$ of which is called a rule. The term u (resp. the (possibly empty) goal ${\overline{{v}}}$) is the left-hand side (resp. right-hand side).

The rules of a program allow one to rewrite terms and goals. This is formalised by the following binary relations, where $\mathop {\rightarrow }_P$ corresponds to the operational semantics of term rewriting and $\mathop {\leadsto }_P$ to that of logic programming. For all goals ${\overline{{s}}}$ and rules $(u,{\overline{{v}}})$ and $(u',{\overline{{v}}}')$, we write $(u,{\overline{{v}}}) \ll _{{\overline{{s}}}} (u',{\overline{{v}}}')$ to denote that $(u, {\overline{{v}}})$ is a variant of $(u',{\overline{{v}}}')$ variable disjoint with ${\overline{{s}}}$, i.e., for some renaming $\gamma$, we have $u = u'\gamma$, ${\overline{{v}}} = {\overline{{v}}}'\gamma$ and $Var (u) \cap Var ({\overline{{s}}}) = Var ({\overline{{v}}}) \cap Var ({\overline{{s}}}) = \emptyset$.

Definition 2.14

For all programs P, we let

$$\begin{aligned} \mathop {\rightarrow }_P = \bigcup \left\{ \mathop {\rightarrow }_r \;\Bigg \vert \; r\in P \right\} \quad \text {and}\quad \mathop {\leadsto }_P = \bigcup \left\{ \mathop {\leadsto }_r \;\Bigg \vert \; r\in P \right\} \end{aligned}$$

where, for all $r \in P$,

$$\begin{aligned} \mathop {\rightarrow }_r = \bigcup \left\{ \mathop {\rightarrow }_{(r,p)} \;\Bigg \vert \; p \in {\overline{{\mathbb {N}}}} \right\} \quad \text {and}\quad \mathop {\leadsto }_r = \bigcup \left\{ \mathop {\leadsto }_{(r,p)} \;\Bigg \vert \; p \in {\overline{{\mathbb {N}}}} \right\} \end{aligned}$$

and, for all $p \in {\overline{{\mathbb {N}}}}$,

$$\begin{aligned} \mathop {\rightarrow }_{(r,p)}&= \left\{ \big (s,t\big ) \in T(\Sigma , X)^2 \;\Bigg \vert \; \begin{array}{l} r = (u, \langle {v}\rangle ), \ p \in { Pos }(s) \\ {s} \vert _{p} = u\theta , \ \theta \in S(\Sigma , X)\\ t = s[v\theta ]_p \end{array} \right\} \\ \mathop {\leadsto }_{(r,p)}&= \left\{ \big ({\overline{{s}}},{\overline{{t}}}\big ) \in {\overline{{T(\Sigma , X)}}}^2 \;\Bigg \vert \; \begin{array}{l} {\overline{{s}}} = \langle {s_1,\dots ,s_n}\rangle , \ p \in \{\langle {1}\rangle ,\dots ,\langle {n}\rangle \} \\ (u, \langle {v_1,\dots ,v_m}\rangle ) \ll _{{\overline{{s}}}} r, \ \theta = { mgu }(s_p, u) \\ {\overline{{t}}} = \langle {s_1,\dots ,s_{p-1},v_1, \dots ,v_m,s_{p-1},\dots ,s_n}\rangle \theta \end{array} \right\} \end{aligned}$$

Concrete examples are provided in Sect. 1.1. We note that if the rule r has the form $(u,{\overline{{v}}})$ with $\vert {{\overline{{v}}}} \vert \ne 1$ then $\mathop {\rightarrow }_{(r,p)} = \emptyset$ for all $p \in {\overline{{\mathbb {N}}}}$. On the other hand, in the definition of $\mathop {\leadsto }_{(r,p)}$, we may have $\langle {v_1,\dots ,v_m}\rangle = \epsilon$ (i.e., $m<1$).

The next lemma states some closure properties of $\mathop {\rightarrow }_{(r,p)}$ and $\mathop {\leadsto }_{(r,p)}$ under substitutions. It is needed to prove compatibility of $\mathop {\rightarrow }_r$ and ${ mg }$ (Lemma 2.17 below) as well as closure properties of abstract reduction systems (see Sect. 3.1). As $\mathop {\rightarrow }_{(r,p)}$ relies on instantiation, its closure property is almost straightforward. In contrast, $\mathop {\leadsto }_{(r,p)}$ relies on narrowing, so its closure property is more restricted and, moreover, it is more complicated to prove.

Lemma 2.15

Let $r = (u,\langle {v}\rangle )$ be a rule and $\theta$ be a substitution.

• For all positions p and all terms s, t, we have: $s \mathop {\rightarrow }_{(r,p)} t$ implies $s\theta \mathop {\rightarrow }_{(r,p)} t\theta$.

• $Var (v) \subseteq Var (u)$ implies $\langle {u\theta }\rangle \mathop {\leadsto }_{(r,\langle {1}\rangle )} \langle {v\theta }\rangle$.

Proof

Let p be a position and s, t be some terms such that $s \mathop {\rightarrow }_{(r,p)} t$. Then, by Definition 2.14, we have $p \in { Pos }(s)$, ${s} \vert _{p} = u\sigma$ and $t = s[v\sigma ]_p$ for some substitution $\sigma$. We have $p \in { Pos }(s\theta )$ and ${s\theta } \vert _{p} = {s} \vert _{p}\theta = u\sigma \theta$. So, by Definition 2.14, $s\theta \mathop {\rightarrow }_{(r,p)} s\theta [v\sigma \theta ]_p$ where $s\theta [v\sigma \theta ]_p = s[v\sigma ]_p\theta = t\theta$. Consequently, we have $s\theta \mathop {\rightarrow }_{(r,p)} t\theta$.

Now, suppose that $Var (v) \subseteq Var (u)$ and let us prove that $\langle {u\theta }\rangle \mathop {\leadsto }_{(r,\langle {1}\rangle )} \langle {v\theta }\rangle$. Let $(u\gamma ,\langle {v\gamma }\rangle )$ be a variant of r variable disjoint with $u\theta$, for some variable renaming $\gamma$. Let $\eta =\{x\gamma \mapsto x\theta \mid x\in Var (u),\ x\gamma \ne x\theta \}$.

• First, we prove that $\eta$ is a substitution. Let $(x \mapsto s)$ and $(y \mapsto t)$ be some bindings in $\eta$. By definition of $\eta$, we have $(x \mapsto s) = (x'\gamma \mapsto x'\theta )$ and $(y \mapsto t) = (y'\gamma \mapsto y'\theta )$ for some variables $x'$ and $y'$ in $Var (u)$. As $\gamma$ is a variable renaming, it is a bijection on X, so if $x=y$ then $x'=y'$ and hence $(x \mapsto s) = (y \mapsto t)$. Consequently, for any bindings $(x \mapsto s)$ and $(y \mapsto t)$ in $\eta$, $(x \mapsto s) \ne (y \mapsto t)$ implies $x\ne y$. Moreover, by definition of $\eta$, for any $(x \mapsto s) \in \eta$ we have $x \ne s$. Therefore, $\eta$ is a substitution.

• Then, we prove that $\eta$ is a unifier of $u\gamma$ and $u\theta$.

  • Let $x\in Var (u)$. Then, by definition of $\eta$, $x\gamma \eta =x\theta$. So, $u\gamma \eta = u\theta$.

  • Let $y\in { Dom }(\eta )$. Then, $y=x\gamma$ for some $x\in Var (u)$. Hence, $y\in Var (u\gamma )$. As $u\gamma$ is variable disjoint with $u\theta$, we have $y \not \in Var (u\theta )$. Therefore, we have ${ Dom }(\eta )\cap Var (u\theta )=\emptyset$, so $u\theta \eta =u\theta$.

  Consequently, we have $u\gamma \eta = u\theta \eta$.

• Finally, we prove that $\eta$ is more general than any other unifier of $u\gamma$ and $u\theta$. Let $\sigma$ be a unifier of $u\gamma$ and $u\theta$. Then, for all $x\in Var (u)$, we have $x\gamma \sigma =x\theta \sigma$. For all variables y that do not occur in ${ Dom }(\eta )$, we have $y\eta \sigma = y\sigma$ and, for all $y \in { Dom }(\eta )$, we have $y = x\gamma$ for some $x \in Var (u)$, so $y\eta \sigma = x\gamma \eta \sigma = x\theta \sigma = x\gamma \sigma = y\sigma$. Hence, $\eta \sigma =\sigma$, i.e., $\eta$ is more general than $\sigma$.

Therefore, $\eta ={ mgu }(u\gamma ,u\theta )$. So, by Definition 2.14, we have $\langle {u\theta }\rangle \mathop {\leadsto }_{(r,\langle {1}\rangle )} \langle {v\gamma \eta }\rangle$. Note that for all $x\in Var (v)$, we have $x\in Var (u)$, so $x\gamma \eta =x\theta$ by definition of $\eta$. Hence, $v\gamma \eta = v\theta$. Finally, we have $\langle {u\theta }\rangle \mathop {\leadsto }_{(r,\langle {1}\rangle )} \langle {v\theta }\rangle$. $\square$

Example 2.16

Consider the rule $r= (u,\langle {v}\rangle ) = ({\textsf{f}}(x,\textsf{1}),\langle {{\textsf{f}}(\textsf{1},x)}\rangle )$ and the substitution $\theta = \{x \mapsto \textsf{0}, y\mapsto \textsf{0}\}$. We have $\langle {u\theta }\rangle = \langle {{\textsf{f}}(\textsf{0},\textsf{1})}\rangle$, $\langle {v\theta }\rangle = \langle {{\textsf{f}}(\textsf{1},\textsf{0})}\rangle$ and $\langle {u\theta }\rangle \mathop {\leadsto }_{(r,\langle {1}\rangle )} \langle {v\theta }\rangle$.

For $s = {\textsf{f}}(\textsf{0},y)$, we also have $\langle {s}\rangle \mathop {\leadsto }_{(r,\langle {1}\rangle )} \langle {{\textsf{f}}(\textsf{1},\textsf{0})}\rangle$, but there is no rewriting of $\langle {s\theta }\rangle$ with r because $s\theta = {\textsf{f}}(\textsf{0},\textsf{0})$ does not unify with any variant of u.

The next compatibility results follow from Definitions 2.12 and 2.14 and from Lemma 2.15.

Lemma 2.17

For all rules r, $\mathop {\rightarrow }_r$ and ${ ins }$ are compatible, and so are $\mathop {\leadsto }_r$ and ${ mg }$.

Proof

Let r be a rule.

• Let $s,t,s'$ be terms such that $s' \in { ins }(s)$ and $s \mathop {\rightarrow }_r t$.

  Then, by Definition 2.12, we have $s' = c[s\sigma ]$ for some context c and some substitution $\sigma$. Moreover, by Definition 2.14, $s \mathop {\rightarrow }_{(r,p)} t$ for some $p \in {\overline{{\mathbb {N}}}}$ and r has the form $(u,\langle {v}\rangle )$.

  So, by Lemma 2.15, we have $s\sigma \mathop {\rightarrow }_{(r,p)} t\sigma$. Let $p'$ be the position of an occurrence of $\square$ in c. Then, $c[s\sigma ] \mathop {\rightarrow }_{(r,p'p)} c[t\sigma ]$ where $c[s\sigma ] = s'$ and $c[t\sigma ] \in { ins }(t)$. So, we have proved that $s' \mathop {\rightarrow }_r t'$ for some $t' \in { ins }(t)$, i.e., that $\mathop {\rightarrow }_r$ and ${ ins }$ are compatible.

• Let ${\overline{{s}}},{\overline{{t}}},{\overline{{s'}}}$ be goals such that ${\overline{{s'}}} \in { mg }({\overline{{s}}})$ and ${\overline{{s}}} \mathop {\leadsto }_r {\overline{{t}}}$. Then, by Definition 2.12, we have ${\overline{{s'}}} = {\overline{{c}}}[{\overline{{a}}}]$ for some goal-context ${\overline{{c}}}$ and some goal ${\overline{{a}}}$ that is more general than ${\overline{{s}}}$. Moreover, by Definition 2.14, we have ${\overline{{s}}} \mathop {\leadsto }_{(r,p)} {\overline{{t}}}$ for some $p \in {\overline{{\mathbb {N}}}}$. Let $r'$ be a variant of r that is variable disjoint with ${\overline{{s'}}}$. Then, $r'$ is also variable disjoint with ${\overline{{a}}}$. So, by the One Step Lifting Lemma 3.21 at page 59 of [1], for some goal ${\overline{{b}}}$ that is more general than ${\overline{{t}}}$, we have ${\overline{{a}}} \mathop {\leadsto }_{(r,p)}^{\theta } {\overline{{b}}}$, where $r'$ and $\theta$ are respectively the variant of r and the unifier used. As $r'$ is also variable disjoint with ${\overline{{c}}}$, we have ${\overline{{c}}}[{\overline{{a}}}] \mathop {\leadsto }_{(r,p'+p)}^{\theta } ({\overline{{c}}}\theta )[{\overline{{b}}}]$ where $r'$ is the variant of r used and $p'$ is the position of $\square$ in ${\overline{{c}}}$. We note that ${\overline{{c}}}[{\overline{{a}}}] = {\overline{{s'}}}$ and $({\overline{{c}}}\theta )[{\overline{{b}}}] \in { mg }({\overline{{t}}})$. So, we have proved that ${\overline{{s'}}} \mathop {\leadsto }_r {\overline{{t'}}}$ for some ${\overline{{t'}}} \in { mg }({\overline{{t}}})$, i.e., that $\mathop {\leadsto }_r$ and ${ mg }$ are compatible.

$\square$

Example 2.18

In Example 1.1, $s = {\textsf{g}}\big ({\textsf{h}}({\textsf{f}}(x),\textsf{0}),x\big )$ and $s \mathop {\rightarrow }_{(r_3,p)} {\textsf{g}}({\textsf{f}}^3(x),x)$ where $p = \langle {1}\rangle$. Let $\sigma = \{x\mapsto \textsf{0}\}$. Then, $s\sigma = {\textsf{g}}\big ({\textsf{h}}({\textsf{f}}(\textsf{0}),\textsf{0}),\textsf{0}\big )$ and $s\sigma \mathop {\rightarrow }_{(r_3,p)} {\textsf{g}}({\textsf{f}}^3(\textsf{0}),\textsf{0})$, i.e., $s\sigma \mathop {\rightarrow }_{(r_3,p)} {\textsf{g}}({\textsf{f}}^3(x),x)\sigma$, where $s\sigma \in { ins }(s)$ and ${\textsf{g}}({\textsf{f}}^3(x),x)\sigma \in { ins }({\textsf{g}}({\textsf{f}}^3(x),x))$.

3 Abstract Reduction Systems

The following notion (see, e.g., Chapter 2 of [2] or Chapter 1 of [30]) generalises the semantics of term rewriting and logic programming presented above.

Definition 3.1

An abstract reduction system (ARS) is a pair $(A,\mathop {\Rightarrow }_{\Pi })$ consisting of a set A and a rewrite relation $\mathop {\Rightarrow }_{\Pi }$, which is the union of binary relations on A indexed by a set $\Pi$, i.e., $\mathop {\Rightarrow }_{\Pi } = \bigcup \{\mathop {\Rightarrow }_{\pi } \mid \pi \in \Pi \}$.

We have $A = T(\Sigma , X)$ in term rewriting and $A = {\overline{{T(\Sigma , X)}}}$ in logic programming; moreover, $\Pi$ is a program in both cases.

We formalise non-termination as the existence of an infinite chain in an ARS.

Definition 3.2

A chain in an ARS $\mathcal {A}= (A,\mathop {\Rightarrow }_{\Pi })$ is a (possibly infinite) $\mathop {\Rightarrow }_{\Pi }$-chain.

3.1 Closure Under Substitutions

In Sect. 5.1, we prove that the existence of finite chains $u_1 \mathop {\Rightarrow }^+_{\Pi } v_1$ and $u_2 \mathop {\Rightarrow }^+_{\Pi } v_2$ of a special form implies that of an infinite chain that involves instances of $u_1$, $v_1$, $u_2$ and $v_2$ (see Definition 5.5 and Corollary 5.13). The proof relies on the following property of ARSs. In the rest of this paper, for all ARSs $(A,\mathop {\Rightarrow }_{\Pi })$ and all $w = \langle {\pi _1,\dots ,\pi _n}\rangle$ in ${\overline{{\Pi }}}$, we let $\mathop {\Rightarrow }_w = (\mathop {\Rightarrow }_{\pi _1} \circ \cdots \circ \mathop {\Rightarrow }_{\pi _n})$, where $\mathop {\Rightarrow }_{\epsilon }$ is the identity relation.

Definition 3.3

Let $\mathcal {A}= (A,\mathop {\Rightarrow }_{\Pi })$ be an ARS where $A \subseteq T(\Sigma , X)\cup {\overline{{T(\Sigma , X)}}}$. We say that $\mathcal {A}$ is closed under substitutions if, for all $s,t \in A$, all $w \in {\overline{{\Pi }}}$ and all substitutions $\theta$, $s \mathop {\Rightarrow }_w t$ implies $s\theta \mathop {\Rightarrow }_w t\theta$.

The following result is a consequence of Lemma 2.15.

Lemma 3.4

For all programs P, $(T(\Sigma , X), \mathop {\rightarrow }_P)$ is closed under substitutions.

Proof

Let P be a program, s, t be terms, $w \in {\overline{{P}}}$ and $\theta$ be a substitution. Suppose that $s \mathop {\rightarrow }_w t$. We prove by induction on $\vert {w} \vert$ that $s\theta \mathop {\rightarrow }_w t\theta$.

• (Base: $\vert {w} \vert = 0$) Here, $\mathop {\rightarrow }_w$ is the identity relation. As $s \mathop {\rightarrow }_w t$, we have $s = t$, hence $s\theta = t\theta$, and so $s\theta \mathop {\rightarrow }_w t\theta$.

• (Induction) Suppose that $\vert {w} \vert = n + 1$ for some $n \in \mathbb {N}$. Suppose also that for all terms $s',t'$, all $w' \in {\overline{{P}}}$ with $\vert {w'} \vert = n$ and all substitutions $\sigma$, $s' \mathop {\rightarrow }_{w'} t'$ implies $s'\sigma \mathop {\rightarrow }_{w'} t'\sigma$. As $\vert {w} \vert = n + 1$, we have $w = rw'$ for some $r \in P$ and some $w' \in {\overline{{P}}}$ with $\vert {w'} \vert = n$. Therefore, $s \mathop {\rightarrow }_r s' \mathop {\rightarrow }_{w'} t$ for some term $s'$. By definition of $\mathop {\rightarrow }_r$, we have $r = (u, \langle {v}\rangle )$, so, by Lemma 2.15, $s\theta \mathop {\rightarrow }_r s'\theta$. As $\vert {w'} \vert = n$, by induction hypothesis we have $s'\theta \mathop {\rightarrow }_{w'} t\theta$. Hence, $s\theta \mathop {\rightarrow }_r s'\theta \mathop {\rightarrow }_{w'} t\theta$, i.e., $s\theta \mathop {\rightarrow }_w t\theta$.$\square$

However, for all programs P, $({\overline{{T(\Sigma , X)}}}, \mathop {\leadsto }_P)$ is not closed under substitutions, see Example 2.16. Hence, based on Lemma 2.15, we introduce the following restricted form of logic programming, where one only rewrites singleton goals using rules, the right-hand side of which is a singleton goal.

Definition 3.5

For all programs P, we let $\mathop {\hookrightarrow }_P = \bigcup \left\{ \mathop {\hookrightarrow }_r \;\Bigg \vert \; r\in P \right\}$ where, for all $r \in P$, $\mathop {\hookrightarrow }_r = \left\{ (u\theta , v\theta ) \in T(\Sigma , X)^2 \;\Bigg \vert \; r = (u, \langle {v}\rangle ),\ Var (v) \subseteq Var (u),\ \theta \in S(\Sigma , X)\right\}$.

We note that $\mathop {\hookrightarrow }_r \subseteq \mathop {\rightarrow }_{r,\epsilon }$. Moreover, $\mathop {\hookrightarrow }_r = \emptyset$ if $r = (u,{\overline{{v}}})$ with $Var ({\overline{{v}}}) \not \subseteq Var (u)$ or $\vert {{\overline{{v}}}} \vert \ne 1$. Now, we have a counterpart of Lemma 3.4 in logic programming:

Lemma 3.6

For all programs P, $(T(\Sigma , X), \mathop {\hookrightarrow }_P)$ is closed under substitutions.

Proof

Let P be a program, s, t be terms, $w \in {\overline{{P}}}$ and $\theta$ be a substitution. Suppose that $s \mathop {\hookrightarrow }_w t$. We prove by induction on $\vert {w} \vert$ that $s\theta \mathop {\hookrightarrow }_w t\theta$.

• (Base: $\vert {w} \vert = 0$) Here, $\mathop {\hookrightarrow }_w$ is the identity relation. As $s \mathop {\hookrightarrow }_w t$, we have $s = t$, hence $s\theta = t\theta$, and so $s\theta \mathop {\hookrightarrow }_w t\theta$.

• (Induction) Suppose that $\vert {w} \vert = n + 1$ for some $n \in \mathbb {N}$. Suppose also that for all terms $s',t'$, all $w' \in {\overline{{P}}}$ with $\vert {w'} \vert = n$ and all substitutions $\sigma$, $s' \mathop {\hookrightarrow }_{w'} t'$ implies $s'\sigma \mathop {\hookrightarrow }_{w'} t'\sigma$. As $\vert {w} \vert = n + 1$, we have $w = rw'$ for some $r \in P$ and some $w' \in {\overline{{P}}}$ with $\vert {w'} \vert = n$. Therefore, $s \mathop {\hookrightarrow }_r s' \mathop {\hookrightarrow }_{w'} t$ for some term $s'$. By Definition 3.5, we have $r = (u, \langle {v}\rangle )$, $Var (v) \subseteq Var (u)$, $s = u\sigma$ and $s' = v\sigma$ for some substitution $\sigma$; moreover, $u\sigma \theta \mathop {\hookrightarrow }_r v\sigma \theta$; so, $s\theta \mathop {\hookrightarrow }_r s'\theta$. As $\vert {w'} \vert = n$, by induction hypothesis we have $s'\theta \mathop {\hookrightarrow }_{w'} t\theta$. Hence, $s\theta \mathop {\hookrightarrow }_r s'\theta \mathop {\hookrightarrow }_{w'} t\theta$, i.e., $s\theta \mathop {\hookrightarrow }_w t\theta$.$\square$

It follows from the next result that the existence of an infinite $\mathop {\hookrightarrow }_P$-chain implies that of an infinite $\mathop {\leadsto }_P$-chain, i.e., non-termination in the restricted form of logic programming implies non-termination in full logic programming.

Lemma 3.7

For all programs P, terms s, t and $w \in {\overline{{P}}}$, $s \mathop {\hookrightarrow }_w t$ implies $\langle {s}\rangle \mathop {\leadsto }_w \langle {t}\rangle$.

Proof

Let P be a program, s, t be terms and $w \in {\overline{{P}}}$. Suppose that $s \mathop {\hookrightarrow }_w t$. We prove by induction on $\vert {w} \vert$ that $\langle {s}\rangle \mathop {\leadsto }_w \langle {t}\rangle$.

• (Base: $\vert {w} \vert = 0$) Here, $\mathop {\hookrightarrow }_w$ and $\mathop {\leadsto }_w$ are the identity relation. As $s \mathop {\hookrightarrow }_w t$, we have $s = t$, hence $\langle {s}\rangle = \langle {t}\rangle$, and so $\langle {s}\rangle \mathop {\leadsto }_w \langle {t}\rangle$.

• (Induction) Suppose that $\vert {w} \vert = n + 1$ for some $n \in \mathbb {N}$. Suppose also that for all terms $s',t'$ and all $w' \in {\overline{{P}}}$ with $\vert {w'} \vert = n$, $s' \mathop {\hookrightarrow }_{w'} t'$ implies $\langle {s'}\rangle \mathop {\leadsto }_{w'} \langle {t'}\rangle$. As $\vert {w} \vert = n + 1$, we have $w = rw'$ for some $r \in P$ and some $w' \in {\overline{{P}}}$ with $\vert {w'} \vert = n$. Therefore, $s \mathop {\hookrightarrow }_r s' \mathop {\hookrightarrow }_{w'} t$ for some term $s'$. By definition of $\mathop {\hookrightarrow }_r$, we have $r = (u, \langle {v}\rangle )$, $Var (v) \subseteq Var (u)$, $s = u\theta$ and $s' = v\theta$ for some substitution $\theta$. So, by Lemma 2.15, we have $\langle {s}\rangle \mathop {\leadsto }_r \langle {s'}\rangle$. As $\vert {w'} \vert = n$, by induction hypothesis we have $\langle {s'}\rangle \mathop {\leadsto }_{w'} \langle {t}\rangle$. Hence, $\langle {s}\rangle \mathop {\leadsto }_r \langle {s'}\rangle \mathop {\leadsto }_{w'} \langle {t}\rangle$, i.e., $\langle {s}\rangle \mathop {\leadsto }_w \langle {t}\rangle$.

$\square$

4 Loops

In Sect. 1.2, we have provided an informal description of loops. Now, we propose a formal definition in an abstract setting.

Definition 4.1

Let $\mathcal {A}= (A,\mathop {\Rightarrow }_{\Pi })$ be an ARS, $w \in {\overline{{\Pi }}}$ and $\phi$ be a binary relation on A which is compatible with $\mathop {\Rightarrow }_{\Pi }$. A $(w,\phi )$-loop in $\mathcal {A}$ is a pair $(a,a') \in A^2$ such that $a \mathop {\Rightarrow }_w a'$ and $a' \in \phi (a)$.

By definition of compatibility (Definition 2.2), the existence of a loop immediately leads to that of an infinite chain.

Lemma 4.2

Suppose that there is a $(w,\phi )$-loop $(a,a')$ in an ARS $(A,\mathop {\Rightarrow }_{\Pi })$. Then, there is an infinite $\mathop {\Rightarrow }_w$-chain that starts with $a \mathop {\Rightarrow }_w a'$.

Proof

Let $a_0 = a$ and $a_1 = a'$. As $(a,a')$ is a $(w,\phi )$-loop, we have $a_0 \mathop {\Rightarrow }_w a_1$ and $a_1 \in \phi (a_0)$. Moreover, $\mathop {\Rightarrow }_{\Pi }$ and $\phi$ are compatible. Therefore, by the definition of $\mathop {\Rightarrow }_w$ and Lemma 2.3, $\mathop {\Rightarrow }_w$ and $\phi$ are compatible. So, we have $a_1 \mathop {\Rightarrow }_w a_2$ for some $a_2 \in \phi (a_1)$. Again by compatibility of $\mathop {\Rightarrow }_w$ and $\phi$, we have $a_2 \mathop {\Rightarrow }_w a_3$ for some $a_3 \in \phi (a_2)$, etc. $\square$

We note that the infinite chain $a_0 \mathop {\Rightarrow }_w a_1 \mathop {\Rightarrow }_w \cdots$ corresponding to a $(w,\phi )$-loop is such that for all $n \in \mathbb {N}$, $a_0 \mathop {\Rightarrow }^n_w a_n$ and $a_n \in \phi ^n(a_0)$, i.e., elements that are somehow “similar” to $a_0$ w.r.t. $\phi$ (i.e., $a_n \in \phi ^n(a_0)$) are periodically “reached” via $\mathop {\Rightarrow }_w$. The name loop stems from this observation.

Moreover, the chain $a_0 \mathop {\Rightarrow }_w a_1 \mathop {\Rightarrow }_w \cdots$ only relies on a single sequence w of elements of $\Pi$. In the next section, we will consider more elaborated chains based on two sequences.

Example 4.3

In Example 1.3, we have

$$\begin{aligned} \underbrace{{\textsf{f}}(x)}_{a_0} \mathop {\rightarrow }_{r_1} {\textsf{g}}({\textsf{h}}(x,\textsf{1}),x) \mathop {\rightarrow }_{r_2} {\textsf{g}}({\textsf{h}}(x,\textsf{0}),x) \mathop {\rightarrow }_{r_3} \underbrace{{\textsf{g}}({\textsf{f}}^2(x),x)}_{a_3} \end{aligned}$$

i.e., $a_0 \mathop {\rightarrow }_w a_3$ for $w = \langle {r_1, r_2, r_3}\rangle$. Moreover, $a_3 \in { ins }(a_0)$ and $\mathop {\rightarrow }_P$ and ${ ins }$ are compatible, where $P = \{r_1,r_2,r_3\}$ (see Lemma 2.17). So, $(a_0, a_3)$ is a $(w,{ ins })$-loop in $(T(\Sigma , X),\mathop {\rightarrow }_P)$. Therefore, by Lemma 4.2, there is an infinite $\mathop {\rightarrow }_w$-chain that starts with $a_0 \mathop {\rightarrow }_w a_3$. Indeed, we have

$$\begin{aligned} \underbrace{{\textsf{f}}(x)}_{a_0} \mathop {\rightarrow }_w \underbrace{{\textsf{g}}({\textsf{f}}^2(x),x)}_{a_3} \mathop {\rightarrow }_w \underbrace{{\textsf{g}}\big ({\textsf{g}}({\textsf{f}}^3(x),{\textsf{f}}(x)),x\big )}_{a_6} \mathop {\rightarrow }_w \cdots \end{aligned}$$

where $a_3 \in { ins }(a_0)$, $a_6 \in { ins }(a_3)$, ... We note that in this chain, the rules are applied at positions that vary gradually (e.g., $r_1$ is applied to subterms of the form ${\textsf{f}}(\cdots )$ that occur at deeper and deeper positions).

Example 4.4

In Example 1.4, we have

$$\begin{aligned} \underbrace{\langle {{\textsf{p}}({\textsf{f}}(x,\textsf{0}))}\rangle }_{{\overline{{a_0}}}} \mathop {\leadsto }_r \underbrace{\langle {{\textsf{p}}(x),{\textsf{q}}(x)}\rangle }_{{\overline{{a_1}}}} \end{aligned}$$

i.e., ${\overline{{a_0}}} \mathop {\rightarrow }_w {\overline{{a_1}}}$ for $w = \langle {r}\rangle$. Moreover, ${\overline{{a_1}}} \in { mg }({\overline{{a_0}}})$ and $\mathop {\leadsto }_P$ and ${ mg }$ are compatible, where $P = \{r\}$ (see Lemma 2.17). So, $({\overline{{a_0}}},{\overline{{a_1}}})$ is a $(w,{ mg })$-loop in $({\overline{{T(\Sigma , X)}}},\mathop {\leadsto }_P)$. Therefore, by Lemma 4.2, there is an infinite $\mathop {\leadsto }_w$-chain that starts with ${\overline{{a_0}}} \mathop {\leadsto }_w {\overline{{a_1}}}$. Indeed, we have

$$\begin{aligned} \underbrace{\langle {{\textsf{p}}({\textsf{f}}(x,\textsf{0}))}\rangle }_{{\overline{{a_0}}}} \mathop {\leadsto }_w \underbrace{\langle {{\textsf{p}}(x),{\textsf{q}}(x)}\rangle }_{{\overline{{a_1}}}} \mathop {\leadsto }_w \underbrace{\langle {{\textsf{p}}(x_1),{\textsf{q}}(x_1), {\textsf{p}}({\textsf{f}}(x_1,\textsf{0}))}\rangle }_{{\overline{{a_2}}}} \mathop {\leadsto }_w \cdots \end{aligned}$$

where ${\overline{{a_1}}} \in { mg }({\overline{{a_0}}})$, ${\overline{{a_2}}} \in { mg }({\overline{{a_1}}})$, ...

5 Binary Chains

In Sect. 4 we have considered infinite chains that rely on a single sequence w of elements of $\Pi$. A natural way to extend this class is to consider infinite chains based on two sequences $w_1$ and $w_2$ as in Definition 5.1 below. In principle, one could also define many other forms of similar chains. In this paper, we concentrate on this form only as it covers interesting examples found in the literature or in [32] (e.g., Examples 5.2, 5.3, 5.4 below) and, moreover, we are able to provide an automatable approach for the detection of a special case (see Sect. 5.1); this case allows one for instance to encode the semantics of vector addition systems [16].

Definition 5.1

A binary chain in an ARS $(A,\mathop {\Rightarrow }_{\Pi })$ is an infinite $(\mathop {\Rightarrow }^*_{w_1} \circ \mathop {\Rightarrow }_{w_2})$-chain for some $w_1,w_2 \in {\overline{{\Pi }}}$.

Of course, as $\mathop {\Rightarrow }_w = (\mathop {\Rightarrow }^0_w \circ \mathop {\Rightarrow }_w)$, the infinite chain $a_0 \mathop {\Rightarrow }_w a_1 \mathop {\Rightarrow }_w \cdots$ corresponding to a $(w,\phi )$-loop is also binary. Moreover, any infinite chain of the form $a_0 \mathop {(\mathop {\Rightarrow }^*_{w_1} \circ \mathop {\Rightarrow }^*_{w_2})} a_1 \mathop {(\mathop {\Rightarrow }^*_{w_1} \circ \mathop {\Rightarrow }^*_{w_2})} \cdots$ is binary, because any sequence $a_i \mathop {\Rightarrow }_{w_2} a'_i \mathop {\Rightarrow }_{w_2} a''_i$ has the form $a_i \mathop {\Rightarrow }^0_{w_1} a_i \mathop {\Rightarrow }_{w_2} a'_i \mathop {\Rightarrow }^0_{w_1} a'_i \mathop {\Rightarrow }_{w_2} a''_i$.

Example 5.2

[5, 9, 34] Consider the rules

$$\begin{aligned} r_1 = \big ({\textsf{b}}({\textsf{c}}), \langle {{\textsf{d}}({\textsf{c}})}\rangle \big ) \qquad r_2 = \big ({\textsf{b}}({\textsf{d}}(x)), \langle {{\textsf{d}}({\textsf{b}}(x))}\rangle \big ) \qquad r_3 = \big ({\textsf{a}}({\textsf{d}}(x)), \langle {{\textsf{a}}({\textsf{b}}^2(x))}\rangle \big ) \end{aligned}$$

For the sake of readability, let us omit parentheses and write for instance $\textsf{adc}$ instead of ${\textsf{a}}({\textsf{d}}({\textsf{c}}))$. Let $w_1 = \langle {r_2}\rangle$ and $w_2 = \langle {r_3,r_1}\rangle$. We have the infinite $(\mathop {\rightarrow }^*_{w_1} \circ \mathop {\rightarrow }_{w_2})$-chain

$$\begin{aligned} \textsf{adc}&\mathop {\rightarrow }^0_{r_2} \textsf{adc} \mathop {\rightarrow }_{r_3} \textsf{ab}^2{\textsf{c}}\mathop {\rightarrow }_{r_1} \textsf{abdc} \\&\mathop {\rightarrow }^1_{r_2} \textsf{adbc} \mathop {\rightarrow }_{r_3} \textsf{ab}^3{\textsf{c}}\mathop {\rightarrow }_{r_1} \textsf{ab}^2\textsf{dc} \\&\mathop {\rightarrow }^2_{r_2} \textsf{adb}^2{\textsf{c}}\mathop {\rightarrow }_{r_3} \textsf{ab}^4{\textsf{c}}\mathop {\rightarrow }_{r_1} \textsf{ab}^3\textsf{dc} \\&\mathop {\rightarrow }^3_{r_2} \cdots \end{aligned}$$

We note that in this chain, the rule $r_3$ is always applied at the root position but that $r_1$ and $r_2$ are applied at positions that vary.

Example 5.3

(TRS_Standard/Zantema_15/ex11.xml in [32]) Consider the rules

$$\begin{aligned} r_1 = \big ({\textsf{f}}(x, {\textsf{s}}(y)), \langle {{\textsf{f}}({\textsf{s}}(x), y)}\rangle \big ) \qquad r_2 = \big ({\textsf{f}}(x, \textsf{0}), \langle {{\textsf{f}}({\textsf{s}}(\textsf{0}), x)}\rangle \big ) \end{aligned}$$

Let $w_1 = \langle {r_1}\rangle$ and $w_2 = \langle {r_2}\rangle$. We have the infinite $(\mathop {\hookrightarrow }^*_{w_1} \circ \mathop {\hookrightarrow }_{w_2})$-chain

$$\begin{aligned} {\textsf{f}}({\textsf{s}}(\textsf{0}), \textsf{0})&\mathop {\hookrightarrow }^0_{r_1} {\textsf{f}}({\textsf{s}}(\textsf{0}), \textsf{0}) \mathop {\hookrightarrow }_{r_2}{\textsf{f}}({\textsf{s}}(\textsf{0}), {\textsf{s}}(\textsf{0})) \\&\mathop {\hookrightarrow }^1_{r_1} {\textsf{f}}({\textsf{s}}^2(\textsf{0}), \textsf{0}) \mathop {\hookrightarrow }_{r_2} {\textsf{f}}({\textsf{s}}(\textsf{0}), {\textsf{s}}^2(\textsf{0})) \\&\mathop {\hookrightarrow }^2_{r_1} {\textsf{f}}({\textsf{s}}^3(\textsf{0}), \textsf{0}) \mathop {\hookrightarrow }_{r_2} {\textsf{f}}({\textsf{s}}(\textsf{0}), {\textsf{s}}^3(\textsf{0})) \\&\mathop {\hookrightarrow }^3_{r_1} \cdots \end{aligned}$$

For instance, $u_1 = {\textsf{f}}({\textsf{s}}(\textsf{0}), {\textsf{s}}(\textsf{0}))$ and $u_2 = {\textsf{f}}({\textsf{s}}^2(\textsf{0}), \textsf{0})$ correspond to the integer vectors $v_1 = (1,1)$ and $v_2 = (2,0)$, respectively, and the chain $u_1 \mathop {\hookrightarrow }_{r_1} u_2$ models the componentwise addition of the vector $(1,-1)$ to $u_1$. The programs ex12.xml and ex14.xml in the same directory of [32] are similar.

Example 5.4

[38] Consider the rules

$$\begin{aligned} r_1 = \big ({\textsf{f}}({\textsf{c}}, {\textsf{a}}(x), y), \langle {{\textsf{f}}({\textsf{c}}, x, {\textsf{a}}(y))}\rangle \big ) \qquad r_2 = \big ({\textsf{f}}({\textsf{c}}, {\textsf{a}}(x), y), \langle {{\textsf{f}}(x, y, {\textsf{a}}^2({\textsf{c}}))}\rangle \big ) \end{aligned}$$

Let $w_1 = \langle {r_1}\rangle$ and $w_2 = \langle {r_2}\rangle$. We have the infinite $(\mathop {\hookrightarrow }^*_{w_1} \circ \mathop {\hookrightarrow }_{w_2})$-chain

$$\begin{aligned} {\textsf{f}}({\textsf{c}}, {\textsf{a}}({\textsf{c}}), {\textsf{a}}^2({\textsf{c}}))&\mathop {\hookrightarrow }^0_{r_1} {\textsf{f}}({\textsf{c}}, {\textsf{a}}({\textsf{c}}), {\textsf{a}}^2({\textsf{c}})) \mathop {\hookrightarrow }_{r_2} {\textsf{f}}({\textsf{c}}, {\textsf{a}}^2({\textsf{c}}), {\textsf{a}}^2({\textsf{c}})) \\&\mathop {\hookrightarrow }^1_{r_1} {\textsf{f}}({\textsf{c}}, {\textsf{a}}({\textsf{c}}), {\textsf{a}}^3({\textsf{c}})) \mathop {\hookrightarrow }_{r_2} {\textsf{f}}({\textsf{c}}, {\textsf{a}}^3({\textsf{c}}), {\textsf{a}}^2({\textsf{c}})) \\&\mathop {\hookrightarrow }^2_{r_1} {\textsf{f}}({\textsf{c}}, {\textsf{a}}({\textsf{c}}), {\textsf{a}}^4({\textsf{c}})) \mathop {\hookrightarrow }_{r_2} {\textsf{f}}({\textsf{c}}, {\textsf{a}}^4({\textsf{c}}), {\textsf{a}}^2({\textsf{c}})) \\&\mathop {\hookrightarrow }^3_{r_1} \cdots \end{aligned}$$

5.1 Recurrent Pairs

Now, we present a new criterion for the detection of binary chains. It is based on two specific chains $u_1 \mathop {\Rightarrow }^+_{\Pi } v_1$ and $u_2 \mathop {\Rightarrow }^+_{\Pi } v_2$ such that a context is removed from $u_1$ to $v_1$ while it is added again from $u_2$ to $v_2$. This is formalised as follows. In the next definition, we consider a new hole symbol $\square '$ that does not occur in $\Sigma \cup X \cup \{\square \}$ and we let $c_1$ be a context with at least one occurrence of $\square$ and $\square '$; moreover, for all terms $t,t'$, we let $c_1[t,t']$ be the term obtained from $c_1$ by replacing the occurrences of $\square$ (resp. $\square '$) by t (resp. $t'$). On the other hand, we let $c_2$ be a context with occurrences of $\square$ only (as in Definition 2.6).

Definition 5.5

Let $\mathcal {A}= (T(\Sigma , X),\mathop {\Rightarrow }_{\Pi })$ be an ARS closed under substitutions. A recurrent pair in $\mathcal {A}$ is a pair $(u_1 \mathop {\Rightarrow }_{w_1} v_1, u_2 \mathop {\Rightarrow }_{w_2} v_2)$ of finite chains in $\mathcal {A}$ such that

• $u_1 = c_1[x, c_2[y]]$, $v_1 = c_1[c_2^{n_1}[x], y]$, $u_2 = c_1[x, c_2^{n_2}[s]]$ and $v_2 = c_1[c_2^{n_3}[t], c_2^{n_4}[x]]$

• $x \ne y$ and $\{x,y\} \cap Var (c_1) = \emptyset$

• $Var (c_2) = Var (s) = \emptyset$

• $t \in \{x,s\}$

• $n_4 \ge n_2$

The ARS $\left( T(\Sigma , X),\mathop {\rightarrow }_{\{r_1,r_2,r_3\}}\right)$ of Example 5.2 is not covered by this definition because it only involves function symbols of arity 0 or 1 (hence, one cannot find a context $c_1$ with at least one occurrence of $\square$ and $\square '$).

Example 5.6

In Example 1.5, we have the chains ${\textsf{f}}(x, c[y], x) \mathop {\rightarrow }_{w_1} {\textsf{f}}(c[x], y, c[x])$ and ${\textsf{f}}(x, \textsf{0}, x) \mathop {\rightarrow }_{w_2} {\textsf{f}}(c[x], c[x], c[x])$. As $\big (T(\Sigma , X),\mathop {\rightarrow }_{\{r_1,r_2,r_3,r_4\}}\big )$ is closed under substitutions (Lemma 3.4), these chains form a recurrent pair, with $c_1 = {\textsf{f}}(\square ,\square ',\square )$, $c_2 = c = {\textsf{g}}(\square ,\textsf{0},\square )$, $(n_1,n_2,n_3,n_4) = (1,0,1,1)$, $s = \textsf{0}$ and $t = x$.

Example 5.7

In Example 5.3, we have the chains ${\textsf{f}}(x, {\textsf{s}}(y)) \mathop {\hookrightarrow }_{w_1} {\textsf{f}}({\textsf{s}}(x), y)$ and ${\textsf{f}}(x, \textsf{0}) \mathop {\hookrightarrow }_{w_2} {\textsf{f}}({\textsf{s}}(\textsf{0}), x)$. As $\big (T(\Sigma , X),\mathop {\hookrightarrow }_{\{r_1,r_2\}}\big )$ is closed under substitutions (Lemma 3.6), these chains form a recurrent pair, with $c_1 = {\textsf{f}}(\square ,\square ')$, $c_2 = {\textsf{s}}(\square )$, $(n_1,n_2,n_3,n_4) = (1,0,1,0)$ and $s = t = \textsf{0}$.

Example 5.8

In Example 5.4, we have the chains ${\textsf{f}}({\textsf{c}}, {\textsf{a}}(x), y) \mathop {\hookrightarrow }_{w_1} {\textsf{f}}({\textsf{c}}, x, {\textsf{a}}(y))$ and ${\textsf{f}}({\textsf{c}}, {\textsf{a}}({\textsf{c}}), y) \mathop {\hookrightarrow }_{w_2} {\textsf{f}}({\textsf{c}}, y, {\textsf{a}}^2({\textsf{c}}))$. As $\big (T(\Sigma , X),\mathop {\hookrightarrow }_{\{r_1,r_2\}}\big )$ is closed under substitutions (Lemma 3.6), these chains form a recurrent pair, with $c_1 = {\textsf{f}}({\textsf{c}},\square ',\square )$, $c_2 = {\textsf{a}}(\square )$, $(n_1,n_2,n_3,n_4) = (1,0,1,0)$ and $s = t = {\textsf{a}}({\textsf{c}})$.

It is proved in [23] that the existence of a recurrent pair of a more restricted form (i.e., $\vert {w_1} \vert = \vert {w_2} \vert = 1$, $c_1 = {\textsf{f}}(\square ,\square ')$ and $n_2 = 0$, as in Example 5.3) leads to that of a binary chain. The generalisation to any sequences $w_1,w_2$, any context $c_1$ and any $n_2 \in \mathbb {N}$ satisfying the constraints above is presented below (Corollary 5.13). In some special situations, the obtained binary chain actually relies on a single sequence (e.g., if $n_2 = n_3 = n_4 = 0$ then we have $c_1[s,s] \mathop {\rightarrow }_{w_2} c_1[s,s] \mathop {\rightarrow }_{w_2} \cdots$), but this is not always the case (see the examples above). The next statements are parametric in an ARS $\mathcal {A}$ closed under substitutions and a recurrent pair in $\mathcal {A}$, with the notations of Definition 5.5 as well as this new one (introduced for the sake of readability):

Definition 5.9

For all $m, n \in \mathbb {N}$, we let $c_1[m, n]$ denote the term $c_1[c_2^m[s],c_2^n[s]]$.

Then, we have the following two results. Lemma 5.10 states that $w_1$ allows one to iteratively move a tower of $c_2$’s from the positions of $\square '$ to those of $\square$ in $c_1$. Conversely, Lemma 5.11 states that $w_2$ allows one to copy a tower of $c_2$’s from the positions of $\square$ to those of $\square '$ in just one application of $\mathop {\Rightarrow }_{w_2}$.

Lemma 5.10

For all $m,n \in \mathbb {N}$, $c_1[m, n+1] \mathop {\Rightarrow }_{w_1} c_1[m + n_1, n]$. Consequently, for all $m,n \in \mathbb {N}$ with $n \ge n_2$, we have $c_1[m, n] \mathop {\Rightarrow }^{n-n_2}_{w_1} c_1[m + (n-n_2) \times n_1, n_2]$.

Proof

Let $m,n \in \mathbb {N}$. Then, $c_1[m, n+1] = c_1[c_2^m[s], c_2^{n+1}[s]] = u_1\theta$ where $\theta = \{x \mapsto c_2^m[s], y \mapsto c_2^n[s]\}$. So, as $u_1 \mathop {\Rightarrow }_{w_1} v_1$ and $\mathcal {A}$ is closed under substitutions, we have $c_1[m, n+1] \mathop {\Rightarrow }_{w_1} v_1\theta$ where $v_1\theta = c_1[c_2^{m + n_1}[s],c_2^n[s]] = c_1[m + n_1, n]$.

Now, we prove the second part of the lemma by induction on n.

• (Base: $n = n_2$) Here, $\mathop {\Rightarrow }^{n-n_2}_{w_1}$ is the identity relation. Hence, for all $m \in \mathbb {N}$, we have $c_1[m, n] \mathop {\Rightarrow }^{n-n_2}_{w_1} c_1[m, n]$, where $c_1[m, n] = c_1[m + (n-n_2) \times n_1, n_2]$.

• (Induction) Suppose that for some $n \ge n_2$ we have $c_1[m, n] \mathop {\Rightarrow }^{n-n_2}_{w_1} c_1[m + (n-n_2) \times n_1, n_2]$ for all $m \in \mathbb {N}$. Let $m \in \mathbb {N}$. By the first part of the lemma, $c_1[m, n+1] \mathop {\Rightarrow }_{w_1} c_1[m + n_1, n]$. Moreover, by induction hypothesis, $c_1[m + n_1, n] \mathop {\Rightarrow }^{n-n_2}_{w_1} c_1[(m + n_1) + (n-n_2) \times n_1, n_2]$, i.e., $c_1[m + n_1, n] \mathop {\Rightarrow }^{n-n_2}_{w_1} c_1[m + (n + 1 - n_2) \times n_1, n_2]$. Consequently, finally we have $c_1[m, n+1] \mathop {\Rightarrow }^{n+1 - n_2}_{w_1} c_1[m + (n + 1 - n_2) \times n_1, n_2]$.$\square$

Lemma 5.11

For all $m \in \mathbb {N}$, we have $c_1[m, n_2] \mathop {\Rightarrow }_{w_2} c_1[m' + n_3, m + n_4]$ where $m' = 0$ if $t = s$ and $m' = m$ if $t = x$.

Proof

Let $m \in \mathbb {N}$. We have $c_1[m, n_2] = c_1[c_2^m[s], c_2^{n_2}[s]] = u_2\{x \mapsto c_2^m[s]\}$. Hence, as $u_2 \mathop {\Rightarrow }_{w_2} v_2$ and $\mathcal {A}$ is closed under substitutions, we have $c_1[m, n_2] \mathop {\Rightarrow }_{w_2} v_2\{x \mapsto c_2^m[s]\}$.

• If $t = s$ then $v_2\{x \mapsto c_2^m[s]\} = c_1[c_2^{n_3}[s],c_2^{m+n_4}[s]] = c_1[n_3, m+n_4]$.

• If $t = x$ then $v_2\{x \mapsto c_2^m[s]\} = c_1[c_2^{m+n_3}[s],c_2^{m+n_4}[s]] = c_1[m+n_3, m+n_4]$.$\square$

By combining Lemmas 5.10 and 5.11, one gets:

Proposition 5.12

For all $m,n \in \mathbb {N}$ with $n \ge n_2$, there exist $m',n' \in \mathbb {N}$ such that $n' \ge n_2$ and $c_1[m, n] \mathop {(\mathop {\Rightarrow }^*_{w_1} \circ \mathop {\Rightarrow }_{w_2})} c_1[m', n']$.

Proof

Let $m,n \in \mathbb {N}$ with $n \ge n_2$. By Lemma 5.10, $c_1[m, n] \mathop {\Rightarrow }^{n-n_2}_{w_1} c_1[l, n_2]$ where $l = m + (n-n_2) \times n_1$. Moreover, by Lemma 5.11, $c_1[l, n_2] \mathop {\Rightarrow }_{w_2} c_1[l' + n_3, l + n_4]$ where $l' = 0$ if $t = s$ and $l' = l$ if $t = x$. Therefore, for $m' = l' + n_3$ and $n' = l + n_4$, we have $c_1[m, n] \mathop {(\mathop {\Rightarrow }^{n-n_2}_{w_1} \circ \mathop {\Rightarrow }_{w_2})} c_1[m', n']$ and we note that $n' \ge n_2$ because, by Definition 5.5, $n_4 \ge n_2$. $\square$

The next result is a straighforward consequence of Proposition 5.12.

Corollary 5.13

For all $m,n \in \mathbb {N}$ with $n \ge n_2$, $c_1[m, n]$ starts an infinite $\mathop {(\mathop {\Rightarrow }^*_{w_1} \circ \mathop {\Rightarrow }_{w_2})}$-chain.

Example 5.14

(Example 5.6 continued) An infinite $\mathop {(\mathop {\rightarrow }^*_{w_1} \circ \mathop {\rightarrow }_{w_2})}$-chain that starts from ${\textsf{f}}(c[\textsf{0}],c[\textsf{0}],c[\textsf{0}]) = c_1[1,1]$ is provided in Example 1.5.

Example 5.15

(Example 5.7 (resp 5.8) continued) An infinite $\mathop {(\mathop {\hookrightarrow }^*_{w_1} \circ \mathop {\hookrightarrow }_{w_2})}$-chain that starts from ${\textsf{f}}({\textsf{s}}(\textsf{0}),\textsf{0}) = c_1[1,0]$ (resp. ${\textsf{f}}({\textsf{c}}, {\textsf{a}}({\textsf{c}}), {\textsf{a}}^2({\textsf{c}})) = c_1[1,0]$) is provided in Example 5.3 (resp. 5.4).

6 Experimental Evaluation

Table 1 Termination Competition 2023—Category TRS Standard

In [21, 22, 25], we have provided details and experimental evaluations with numbers about the loop detection approach of NTI. Since then, the tool has evolved, as we have fixed several bugs and implemented the syntactic criterion of Sect. 5.1 for detecting binary chains. Hence, we present an updated evaluation based on the results of NTI at the Termination Competition 2023 [31]. NTI participated in two categories.

• Category Logic Programming (315 LPs, 2 participants: AProVE[10, 12] and NTI). Here, NTI was the only tool capable of detecting non-termination. In total, it found 58 non-terminating LPs; 45 of them were detected from a loop and the other 13 from a recurrent pair.

• Category TRS Standard (1523 TRSs, 7 participants: AProVE, AutoNon[7], MnM[15], MU-TERM[18], NaTT[35], NTI, $\textsf{T}_{\textsf{T}}\textsf{T}_{\textsf{2}}$ [29]).

  We report some results in Table 1. For each participant, column “NO’s” reports the number of NO answers, i.e., of TRSs proved non-terminating (with, in parentheses, the number of these TRSs detected by the participant only). The Virtual Best Solver (VBS) collects the best consistent claim for each benchmark since at least 2018; column “% VBS” reports the percentage of NO’s of each participant w.r.t. the 340 NO’s that the VBS collected in total. Then, the following columns report the number of NO’s for 4 particular directories of [32]: (E12) corresponds to TRS_Standard/EEG_IJCAR_12 (49 TRSs), (P21) to TRS_Standard/payet_21 (3 TRSs), (P23) to TRS_Standard/Payet_23 (10 TRSs) and (Z15) to TRS_Standard/Zantema_15 (16 TRSs).

  Globally, the number of non-terminating TRSs detected by NTI is the second highest, just behind AProVE.

  As far as we know, MnM, MU-TERM, NaTT and $\textsf{T}_{\textsf{T}}\textsf{T}_{\textsf{2}}$ only detect loops. We note that the number of loops found by MnM is the highest among these 4 participants. It is even very likely that it is the highest among all the participants but we could not verify this precisely.

  On the other hand, AProVE, AutoNon and NTI are able to detect loops as well as other forms of non-termination (usually called non-loops).

  In order to detect non-loops, NTI tries to find recurrent pairs while AProVE implements the approach of [6, 19] and AutoNon that of [7] (see Sect. 7 below). To illustrate their technique, the authors of these tools submitted several TRSs admitting no loop to the organizers of the competition (see directory (E12) for AProVE, (P21)+(P23) for NTI and (Z15) for AutoNon). The 10 non-terminating TRSs that NTI is the only one to detect are those of (P23). Moreover, we note that NTI finds 3 recurrent pairs in (Z15), see Example 5.3, and none in (E12)¹, while AProVE fails on the TRSs of (P21)+(P23) and AutoNon succeeds on those of (P21) only. We guess that AutoNon fails on (P23) because all the TRSs of this directory are not left-linear.

  The version of NTI that participated in the Termination Competition 2023 relies on a weaker variation of Definition 5.5 where $n_2 = 0$ (actually, the idea of adding $n_2$ to this definition came after the competition). Since then, we have extended the code to handle $n_2$ and now NTI is able to find recurrent pairs for 5 TRSs in the directory TRS_Standard/Waldmann_06 of [32] (jwno2.xml, jwno3.xml, jwno5.xml, jwno7.xml, jwno8.xml) and also for the TRS TRS_Standard/Mixed_TRS/6.xml. Therefore, together with the 3 TRSs in TRS_Standard/Zantema_15 (see Example 5.3), NTI is able to find recurrent pairs for 9 TRSs that already occurred in [32] before we added (P21) and (P23). All these 9 TRSs are also proved non-terminating by AutoNon but not by AProVE.

7 Related Work

In [21, 25] we have presented an extended description of related work in term rewriting and in logic programming. The state of the art has not evolved much since then. To the best of our knowledge, the only significant new results have been introduced in [6, 7, 19, 34] for string and term rewriting.

• In [19], the author presents an approach to detect infinite chains in string rewriting. It uses rules between string patterns of the form $u v^n w$ where u, v, w are strings and n can be instantiated by any natural number. This idea is extended in [6] to term rewriting. String patterns are replaced by pattern terms that describe sets of terms and have the form $t\sigma ^n\mu$ where t is a term, $\sigma ,\mu$ are substitutions and n is any natural number. A pattern rule $(t_1\sigma _1^n\mu _1, t_2\sigma _2^n\mu _2)$ is correct if, for all $n\in \mathbb {N}$, $t_1\sigma _1^n\mu _1 \mathop {\rightarrow }^+_P t_2\sigma _2^n\mu _2$ holds, where P is the TRS under consideration. Several inference rules are introduced to derive correct pattern rules from a TRS automatically. A sufficient condition on the derived pattern rules is also provided to detect non-termination.

  Currently, we do not have a clear idea of the links between the infinite chains considered in these papers and those of Sect. 5. The experimental results reported in Sect. 6 suggest that these papers address a form of non-termination which is not connected to recurrent pairs. Indeed, AProVE fails on the TRSs of (P21)+(P23) while NTI fails to find recurrent pairs for those of (E12).

• In [7], an automatable approach is presented to prove the existence of infinite chains for TRSs. The idea is to find a non-empty regular language of terms that is closed under rewriting and does not contain normal forms. It is automated by representing the language by a finite tree automaton and expressing these requirements in a SAT formula whose satisfiability implies non-termination. A major difference w.r.t. our work is that this technique only addresses left-linear TRSs; in contrast, the approach of Sect. 5.1 applies to any ARS which is closed under substitution, and left-linearity is not needed. On the other hand, using the notations of Sect. 5.1, the set $\{c_1[m,n] \mid m,n \in \mathbb {N},\ n \ge n_2\}$ is a non-empty regular language of terms which is closed under $\mathop {\Rightarrow }^+_{\Pi }$ and does not contain normal forms (see Proposition 5.12), i.e., it is precisely the kind of set that the approach of [7] tries to find.

• The concept of inner-looping chain is presented and studied in [34]. It corresponds to infinite chains that have the form

  $$\begin{aligned} c_1[c_2^{n_0}s\theta ^{n_0}] \mathop {\rightarrow }^+_P c_1[c_2^{n_1}s\theta ^{n_1}] \mathop {\rightarrow }^+_P \cdots \end{aligned}$$

  where P is a program, $c_1,c_2$ are contexts, s is a term, $\theta$ is a substitution and the $n_i$’s are non-negative integers (here, $c_2^n s \theta ^n = c_2[\cdots c_2[c_2[s\theta ]\theta ]\theta \cdots ]$ where $c_2$ and $\theta$ repeat n times). For instance, the infinite chain of Example 5.2 is inner-looping because it has the form $a_0 \mathop {\rightarrow }^+_P a_1 \mathop {\rightarrow }^+_P \cdots$ where, for all $n \in \mathbb {N}$, $a_n = \textsf{ab}^n\textsf{dc} = c_1[c_2^n s \theta ^n]$ with $c_1 = {\textsf{a}}(\square )$, $c_2 = {\textsf{b}}(\square )$, $s = \textsf{dc}$ and $\theta = \emptyset$.

  We do not know how inner-looping chains are connected to the infinite chains considered in Sect. 5.

The notion of recurrent set [13] used to prove non-termination of imperative programs is also related to our work. It can be defined as follows in our formalism.

Definition 7.1

Let $\mathcal {A}= (A,\mathop {\Rightarrow }_{\Pi })$ be an ARS. A set B is recurrent for $\mathcal {A}$ if $B \ne \emptyset$, $B \subseteq A$ and $(\mathop {\Rightarrow }^+_{\Pi }(b) \mathop {\cap } B) \ne \emptyset$ for all $b\in B$.

For instance, in Sect. 5.1, the set $\{c_1[m,n] \mid m,n \in \mathbb {N},\ n \ge n_2\}$ is recurrent (see Proposition 5.12). Moreover, the regular languages of terms computed by the approach of [7] are non-empty and closed under rewriting, hence they are also recurrent.

8 Conclusion

We have considered two forms of non-termination, namely, loops and binary chains, in an abstract framework that encompasses term rewriting and logic programming. We have presented a syntactic criterion to detect a special case of binary chains and implemented it successfully in our tool NTI. As for future work, we plan to investigate the connections between the infinite chains considered in [6, 34] and in this paper.