arXiv:0803.0014v2 [cs.LO] 1 Sep 2008

Automated Termination Proofs for
Logic Programs by Term Rewriting
Peter Schneider-Kamp, RWTH Aachen, Germany
Jürgen Giesl, RWTH Aachen, Germany
Alexander Serebrenik, TU Eindhoven, The Netherlands
René Thiemann, University of Innsbruck, Austria

There are two kinds of approaches for termination analysis of logic programs: “transformational”
and “direct” ones. Direct approaches prove termination directly on the basis of the logic program.
Transformational approaches transform a logic program into a term rewrite system (TRS) and
then analyze termination of the resulting TRS instead. Thus, transformational approaches make
all methods previously developed for TRSs available for logic programs as well. However, the
applicability of most existing transformations is quite restricted, as they can only be used for
certain subclasses of logic programs. (Most of them are restricted to well-moded programs.) In
this paper we improve these transformations such that they become applicable for any definite
logic program. To simulate the behavior of logic programs by TRSs, we slightly modify the notion
of rewriting by permitting infinite terms. We show that our transformation results in TRSs which
are indeed suitable for automated termination analysis. In contrast to most other methods for
termination of logic programs, our technique is also sound for logic programming without occur
check, which is typically used in practice. We implemented our approach in the termination prover
AProVE and successfully evaluated it on a large collection of examples.
Categories and Subject Descriptors: F.3.1 [Logic and Meanings of Programs]: Specifying
and Verifying and Reasoning about Programs—Mechanical verification; D.1.6 [Programming
Techniques]: Logic Programming; I.2.2 [Artificial Intelligence]: Automatic Programming—
Automatic analysis of algorithms; I.2.3 [Artificial Intelligence]: Deduction and Theorem Proving—Logic programming
General Terms: Languages, Theory, Verification
Additional Key Words and Phrases: logic programming, termination analysis, term rewriting,
dependency pairs

Supported by the Deutsche Forschungsgsmeinschaft DFG under grant GI 274/5-2.
Authors’ addresses:
Peter Schneider-Kamp, Jürgen Giesl, LuFG Informatik 2, RWTH Aachen, Ahornstr. 55, 52074
Aachen, Germany, {psk,giesl}@informatik.rwth-aachen.de
Alexander Serebrenik, Dept. of Mathematics and Computer Science, TU Eindhoven, P.O. Box
513, 5600 MB Eindhoven, The Netherlands, a.serebrenik@tue.nl
René Thiemann, Institute of Computer Science, University of Innsbruck, Technikerstr. 21a, 6020
Innsbruck, Austria, rene.thiemann@uibk.ac.at. Most of the work was carried out while R. Thiemann was at the LuFG Informatik 2, RWTH Aachen.
Permission to make digital/hard copy of all or part of this material without fee for personal
or classroom use provided that the copies are not made or distributed for profit or commercial
advantage, the ACM copyright/server notice, the title of the publication, and its date appear, and
notice is given that copying is by permission of the ACM, Inc. To copy otherwise, to republish,
to post on servers, or to redistribute to lists requires prior specific permission and/or a fee.
c 20YY ACM 1529-3785/YY/00-0001 $5.00
ACM Transactions on Computational Logic, Vol. V, No. N, 20YY, Pages 1–49.

2

·

P. Schneider-Kamp, J. Giesl, A. Serebrenik, R. Thiemann

1. INTRODUCTION
Termination of logic programs is widely studied. Most automated techniques try to
prove universal termination of definite logic programs, i.e., one tries to show that
all derivations of a logic program are finite w.r.t. the left-to-right selection rule.
Both “direct” and “transformational” approaches have been proposed in the literature (see, e.g., [De Schreye and Decorte 1994] for an overview and [Bruynooghe
et al. 2007; Codish et al. 2005; Codish et al. 2006; De Schreye and Serebrenik 2002;
Lagoon et al. 2003; Mesnard and Ruggieri 2003; Mesnard and Serebrenik 2007;
Nguyen and De Schreye 2005; 2007; Nguyen et al. 2008; Serebrenik and De Schreye
2005a; Smaus 2004] for more recent work on “direct” approaches). “Transformational” approaches have been developed in [Aguzzi and Modigliani 1993; Arts
and Zantema 1995; Chtourou and Rusinowitch 1993; Ganzinger and Waldmann
1993; Krishna Rao et al. 1998; Marchiori 1994; 1996; van Raamsdonk 1997] and
a comparison of these approaches is given in [Ohlebusch 2001]. Moreover, similar
transformational approaches also exist for other programming languages (e.g., see
[Giesl et al. 2006] for an approach to prove termination of Haskell-programs via
a transformation to term rewriting). Moreover, there is also work in progress to
develop such approaches for imperative programs.
In order to be successful for termination analysis of logic programs, transformational methods
(I) should be applicable for a class of logic programs as large as possible and
(II) should produce TRSs whose termination is easy to analyze automatically.
Concerning (I), the above existing transformations can only be used for certain subclasses of logic programs. More precisely, all approaches except [Marchiori 1994;
1996] are restricted to well-moded programs. The transformations of [Marchiori
1994; 1996] also consider the classes of simply well-typed and safely typed programs.
However in contrast to all previous transformations, we present a new transformation which is applicable for any (definite) logic program. Like most approaches
for termination of logic programs, we restrict ourselves to programs without cut
and negation. While there are transformational approaches which go beyond definite programs [Marchiori 1996], it is not clear how to transform non-definite logic
programs into TRSs that are suitable for automated termination analysis, cf. (II).
Concerning (II), one needs an implementation and an empirical evaluation to
find out whether termination of the transformed TRSs can indeed be verified automatically for a large class of examples. Unfortunately, to our knowledge there is
only a single other termination tool available which implements a transformational
approach. This tool TALP [Ohlebusch et al. 2000] is based on the transformations
of [Arts and Zantema 1995; Chtourou and Rusinowitch 1993; Ganzinger and Waldmann 1993] which are shown to be equally powerful in [Ohlebusch 2001]. So these
transformations are indeed suitable for automated termination analysis, but consequently, TALP only accepts well-moded logic programs. This is in contrast to
our approach which we implemented in our termination prover AProVE [Giesl et al.
2006]. Our experiments on large collections of examples in Section 7 show that our
transformation indeed produces TRSs that are suitable for automated termination
analysis and that AProVE is currently among the most powerful termination provers
ACM Transactions on Computational Logic, Vol. V, No. N, 20YY.

Automated Termination Proofs for Logic Programs by Term Rewriting

·

3

for logic programs.
To illustrate the starting point for our research, we briefly review related work
on connecting termination analysis of logic programs and term rewrite systems:
in Section 1.1 we recapitulate the classical transformation of [Arts and Zantema
1995; Chtourou and Rusinowitch 1993; Ganzinger and Waldmann 1993; Ohlebusch
2001] and in Section 1.2 we discuss the approach of adapting TRS-techniques to
the logic programming setting (which can be seen as an alternative to our approach
of transforming logic programs to TRSs). Then in Section 1.3 we give an overview
on the structure of the remainder of the paper.
1.1 The Classical Transformation
Our transformation is inspired by the transformation of [Arts and Zantema 1995;
Chtourou and Rusinowitch 1993; Ganzinger and Waldmann 1993; Ohlebusch 2001].
In this classical transformation, each argument position of each predicate is either
determined to be an input or an output position by a moding function m. So for
every predicate symbol p of arity n and every 1 ≤ i ≤ n, we have m(p, i) ∈ {in, out}.
Thus, m(p, i) states whether the i-th argument of p is an input (in) or an output
(out) argument.
As mentioned, the moding must be such that the logic program is well moded [Apt
and Etalle 1993]. Well-modedness guarantees that each atom selected by the left-toright selection rule is “sufficiently” instantiated during any derivation with a query
that is ground on all input positions. More precisely, a program is well moded iff
for any of its clauses H :– B1 , . . . , Bk with k ≥ 0, we have
(a) Vout (H) ⊆ Vin (H) ∪ Vout (B1 ) ∪ . . . ∪ Vout (Bk ) and
(b) Vin (Bi ) ⊆ Vin (H) ∪ Vout (B1 ) ∪ . . . ∪ Vout (Bi−1 ) for all 1 ≤ i ≤ k
Vin (B) and Vout (B) are the variables in terms on B’s input and output positions.
Example 1.1. Consider the following variant of a small example from [Ohlebusch
2001].
p(X, X).
p(f(X), g(Y )) :– p(f(X), f(Z)), p(Z, g(Y )).
Let m be a moding with m(p, 1) = in and m(p, 2) = out. Then the program is well
moded: This is obvious for the first clause. For the second clause, (a) holds since
the output variable Y of the head is also an output variable of the second body
atom. Similarly, (b) holds since the input variable X of the first body atom is also
an input variable of the head, and the input variable Z of the second body atom is
also an output variable of the first body atom.
In the classical transformation from logic programs to TRSs, two new function
symbols pin and pout are introduced for each predicate p. We write “p(~s, ~t)” to
denote that ~s and ~t are the sequences of terms on p’s in- and output positions.
• For each fact p(~s, ~t), the TRS contains the rule pin (~s) → pout (~t).
• For each clause c of the form p(~s, ~t) :– p1 (~s1 , ~t1 ), . . . , pk (~sk , ~tk ), the resulting TRS
ACM Transactions on Computational Logic, Vol. V, No. N, 20YY.

4

·

P. Schneider-Kamp, J. Giesl, A. Serebrenik, R. Thiemann

contains the following rules:
pin (~s) → uc,1 (p1in (~s1 ), V(~s))
~
uc,1 (p1out (t1 ), V(~s)) → uc,2 (p2in (~s2 ), V(~s) ∪ V(~t1 ))
...
~
~
~
uc,k (pkout (tk ), V(~s) ∪ V(t1 ) ∪ . . . ∪ V(tk−1 )) → pout (~t)
Here, V(~s) are the variables occurring in ~s. Moreover, if V(~s) = {x1 , . . . , xn },
then “uc,1 (p1in (~s1 ), V(~s))” abbreviates the term uc,1 (p1in (~s1 ), x1 , . . . , xn ), etc.
If the resulting TRS is terminating, then the original logic program terminates for
any query with ground terms on all input positions of the predicates, cf. [Ohlebusch
2001]. However, the converse does not hold.
Example 1.2. For the program of Example 1.1, the transformation results in the
following TRS R.
pin (X) → pout (X)
pin (f(X)) → u1 (pin (f(X)), X)
u1 (pout (f(Z)), X) → u2 (pin (Z), X, Z)
u2 (pout (g(Y )), X, Z) → pout (g(Y ))
The original logic program is terminating for any query p(t1 , t2 ) where t1 is a ground
term. However, the above TRS is not terminating:
pin (f(X)) →R u1 (pin (f(X)), X) →R u1 (u1 (pin (f(X)), X), X) →R . . .
In the logic program, after resolving with the second clause, one obtains a query
starting with p(f(. . .), f(. . .)). Since p’s output argument f(. . .) is already partly
instantiated, the second clause cannot be applied again for this atom. However,
this information is neglected in the translated TRS. Here, one only regards the
input argument of p in order to determine whether a rule can be applied. Note
that many current tools for termination proofs of logic programs like cTI [Mesnard
and Bagnara 2005], TALP [Ohlebusch et al. 2000], TermiLog [Lindenstrauss et al.
1997], and TerminWeb [Codish and Taboch 1999] fail on Example 1.1.
So this example already illustrates a drawback of the classical transformation:
there are several terminating well-moded logic programs which are transformed into
non-terminating TRSs. In such cases, one fails in proving the termination of the
logic program. Even worse, most of the existing transformations are not applicable
for logic programs that are not well moded.1
Example 1.3. We modify Example 1.1 by replacing g(Y ) with g(W ) in the body
of the second clause:
p(X, X).
p(f(X), g(Y )) :– p(f(X), f(Z)), p(Z, g(W )).
1 Example

1.3 is neither well moded nor simply well typed nor safely typed (using the types
“Any” and “Ground”) as required by the transformations of [Aguzzi and Modigliani 1993; Arts
and Zantema 1995; Chtourou and Rusinowitch 1993; Ganzinger and Waldmann 1993; Krishna
Rao et al. 1998; Marchiori 1994; 1996; van Raamsdonk 1997].
ACM Transactions on Computational Logic, Vol. V, No. N, 20YY.

Automated Termination Proofs for Logic Programs by Term Rewriting

·

5

Still, all queries p(t1 , t2 ) terminate if t1 is ground. But this program is not well
moded, as the second clause violates Condition (a): Vout (p(f(X), g(Y ))) = {Y } 6⊆
Vin (p(f(X), g(Y ))) ∪ Vout (p(f(X), f(Z))) ∪ Vout (p(Z, g(W ))) = {X, Z, W }. Transforming the program as before yields a TRS with the rule u2 (pout (g(W )), X, Z) →
pout (g(Y )). So non-well-moded programs result in rules with variables like Y in
the right- but not in the left-hand side. Such rules are usually forbidden in term
rewriting and they do not terminate, since Y may be instantiated arbitrarily.
Example 1.4. A natural non-well-moded example is the append-program with
the clauses
append([ ], M , M ).
append([X|L], M , [X|N ]) :– append(L, M , N ).
and the moding m(append, 1) = in and m(append, 2) = m(append, 3) = out,
i.e., one only considers append’s first argument as input. Due to the first clause
append([ ], M , M ), this program is not well moded although all queries of the form
append(t1 , t2 , t3 ) are terminating if t1 is ground.
1.2 Term Rewriting Techniques for Termination of Logic Programs
Recently, several authors tackled the problem of applying termination techniques
from term rewriting for (possibly non-well-moded) logic programs. A framework
for integrating orders from term rewriting into direct termination approaches for
logic programs is discussed in [De Schreye and Serebrenik 2002].2 However, the
automation of this framework is non-trivial in general. As an instance of this
framework, the automatic application of polynomial interpretations (well-known in
term rewriting) to termination analysis of logic programs is investigated in [Nguyen
and De Schreye 2005; 2007]. Moreover, [Nguyen et al. 2008] extend this work
further by also adapting a basic version of the dependency pair approach [Arts and
Giesl 2000] from TRSs to the logic programming setting. This provides additional
evidence that techniques developed for term rewriting can successfully be applied
to termination analysis of logic programs.
Instead of integrating each termination technique from term rewriting separately,
in the current paper we want to make all these techniques available at once. Therefore, unlike [De Schreye and Serebrenik 2002; Nguyen and De Schreye 2005; 2007;
Nguyen et al. 2008], we choose a transformational approach. Our goal is a method
which
(A) handles programs like Example 1.1 where classical transformations like the one
of Section 1.1 fail,
(B) handles non-well-moded programs like Example 1.3 where most current transformational techniques are not even applicable,
(C) allows the successful automated application of powerful techniques from rewriting for logic programs like Example 1.1 and 1.3 where current tools based on
2 But

in contrast to [De Schreye and Serebrenik 2002], transformational approaches like the one
presented in this paper can also apply more recent termination techniques from term rewriting
for termination of logic programs (e.g., refined variants of the dependency pair method like [Giesl
et al. 2005; Giesl et al. 2006; Hirokawa and Middeldorp 2005], semantic labelling [Zantema 1995],
matchbounds [Geser et al. 2004], etc.).
ACM Transactions on Computational Logic, Vol. V, No. N, 20YY.

6

·

P. Schneider-Kamp, J. Giesl, A. Serebrenik, R. Thiemann

direct approaches fail. For larger and more realistic examples we refer to the
experiments in Section 7.
1.3 Structure of the Paper
After presenting required preliminaries in Section 2, in Section 3 we modify the
transformation from logic programs to TRSs to achieve (A) and (B). So restrictions
like well-modedness, simple well-typedness, or safe typedness are no longer required.
Our new transformation results in TRSs where the notion of “rewriting” has to
be slightly modified: we regard a restricted form of infinitary rewriting, called
infinitary constructor rewriting. The reason is that logic programs use unification,
whereas TRSs use matching.
To illustrate this difference, consider the logic program p(s(X)) :– p(X) which
does not terminate for the query p(X): Unifying the query p(X) with the head
of the variable-renamed rule p(s(X1 )) :– p(X1 ) yields the new query p(X1 ). Afterwards, unifying the new query p(X1 ) with the head of the variable-renamed rule
p(s(X2 )) :– p(X2 ) yields the new query p(X2 ), etc.
In contrast, the related TRS p(s(X)) → p(X) terminates for all finite terms.
When applying the rule to some subterm t, one has to match the left-hand side ℓ of
the rule against t. For example, when applying the rule to the term p(s(s(Y ))), one
would use the matcher that instantiates X with s(Y ). Thus, p(s(s(Y ))) would be
rewritten to the instantiated right-hand side p(s(Y )). Hence, one occurrence of the
symbol s is eliminated in every rewrite step. This implies that rewriting will always
terminate. So in contrast to unification (where one searches for a substitution θ
with tθ = ℓθ), here we only use matching (i.e., we search for a substitution θ with
t = ℓθ, but we do not instantiate the term t that is being rewritten).
However, the infinite derivation of the logic program above corresponds to an
infinite reduction of the TRS above with the infinite term p(s(s(. . .))) containing
infinitely many nested s-symbols. So to simulate unification by matching, we have
to regard TRSs where the variables in rewrite rules may be instantiated by infinite
constructor terms. It turns out that this form of rewriting also allows us to analyze
the termination behavior of logic programming with infinite terms, i.e., of logic
programming without occur check.
Section 4 shows that the existing termination techniques for TRSs can easily be
adapted in order to prove termination of infinitary constructor rewriting. For a
full automation of the approach, one has to transform the set of queries that has
to be analyzed for the logic program to a corresponding set of terms that has to
be analyzed for the transformed TRS. This set of terms is characterized by a socalled argument filter and we present heuristics to find a suitable argument filter
in Section 5. Section 6 gives a formal proof that our new transformation and our
approach to automated termination analysis are strictly more powerful than the
classical ones of Section 1.1. We present and discuss an extensive experimental
evaluation of our results in Section 7 which shows that Goal (C) is achieved as
well. In other words, the implementation of our approach can indeed compete with
modern tools for direct termination analysis of logic programs and it succeeds for
many programs where these tools fail. Finally, we conclude in Section 8.
Preliminary versions of parts of this paper appeared in [Schneider-Kamp et al.
2007]. However, the present article extends [Schneider-Kamp et al. 2007] considerACM Transactions on Computational Logic, Vol. V, No. N, 20YY.

Automated Termination Proofs for Logic Programs by Term Rewriting

·

7

ably (in particular, by the results of the Sections 5 and 6). Section 6 contains a new
formal comparison with the existing classical transformational approach to termination of logic programs and proves formally that our approach is more powerful.
The new contributions of Section 5 improve the power of our method substantially
as can be seen in our new experiments in Section 7. Moreover, in contrast to
[Schneider-Kamp et al. 2007], this article contains the full proofs of all results and
a discussion on the limitations of our approach in Section 7.2.
2. PRELIMINARIES ON LOGIC PROGRAMMING AND REWRITING
We start with introducing the basics on (possibly infinite) terms and atoms. Then
we present the required notions on logic programming and on term rewriting in
Sections 2.1 and 2.2, respectively.
A signature is a pair (Σ, ∆) where Σ and ∆ are finite sets of function and predicate
symbols. Each f ∈ Σ ∪ ∆ has an arity n ≥ 0 and we often write f /n instead of
f . We always assume that Σ contains at least one constant f /0. This is not a
restriction, since enriching the signature by a fresh constant would not change the
termination behavior.
Definition 2.1 (Infinite Terms and Atoms). A term over Σ is a tree where every
leaf node is labelled with a variable X ∈ V or with f /0 ∈ Σ and every inner node
with n children (n > 0) is labelled with some f /n ∈ Σ. We write f (t1 , . . . , tn ) for
the term with root f and direct subtrees t1 , . . . , tn . A term t is called finite if all
paths in the tree t are finite, otherwise it is infinite. A term is rational if it only
contains finitely many different subterms. The sets of all finite terms, all rational
terms, and all (possibly infinite) terms over Σ are denoted by T (Σ, V), T rat (Σ, V),
and T ∞ (Σ, V), respectively. If ~t is the sequence t1 , . . . , tn , then ~t ∈ T~ ∞ (Σ, V)
means that ti ∈ T ∞ (Σ, V) for all i. T~ (Σ, V) is defined analogously. For a term
t, let V(t) be the set of all variables occurring in t. A position pos ∈ N∗ in a
(possibly infinite) term t addresses a subterm t|pos of t. We denote the empty word
(and thereby the top position) by ε. The term t[s]pos results from replacing the
subterm t|pos at position pos in t by the term s. So for pos = ε we have t|ε = t
and t[s]ε = s. Otherwise pos = i pos ′ for some i ∈ N and t = f (t1 , . . . , tn ). Then
we have t|pos = t|i pos ′ = ti |pos ′ and t[s]pos = t[s]i pos ′ = f (t1 , . . . , ti [s]pos ′ . . . , tn ).
An atom over (Σ, ∆) is a tree p(t1 , . . . , tn ), where p/n ∈ ∆ and t1 , . . . , tn ∈
T ∞ (Σ, V). A∞ (Σ, ∆, V) is the set of atoms and Arat (Σ, ∆, V) (and A(Σ, ∆, V),
resp.) are the atoms p(t1 , . . . , tn ) where ti ∈ T rat (Σ, V) (and ti ∈ T (Σ, V), resp.)
for all i. We write A(Σ, ∆) and T (Σ) instead of A(Σ, ∆, ∅) and T (Σ, ∅).
2.1 Logic Programming
A clause c is a formula H :– B1 , . . . , Bk with k ≥ 0 and H, Bi ∈ A(Σ, ∆, V). H is c’s
head and B1 , . . . , Bk is c’s body. A finite set of clauses P is a definite logic program.
A clause with empty body is a fact and a clause with empty head is a query. We
usually omit “ :– ” in queries and just write “B1 , . . . , Bk ”. The empty query is
denoted ✷. In queries, we also admit rational instead of finite atoms B1 , . . . , Bk .
Since we are also interested in logic programming without occur check we consider
infinite substitutions θ : V → T ∞ (Σ, V). Here, we allow θ(X) 6= X for infinitely
many X ∈ V. Instead of θ(X) we often write Xθ. If θ is a variable renaming
ACM Transactions on Computational Logic, Vol. V, No. N, 20YY.

8

·

P. Schneider-Kamp, J. Giesl, A. Serebrenik, R. Thiemann

(i.e., a one-to-one correspondence on V), then tθ is a variant of t, where t can be
any expression (e.g., a term, atom, clause, etc.). We write θσ to denote that the
application of θ is followed by the application of σ.
A substitution θ is a unifier of two terms s and t if and only if sθ = tθ. We call
θ the most general unifier (mgu) of s and t if and only if θ is a unifier of s and t
and for all unifiers σ of s and t there is a substitution µ such that σ = θµ.
We briefly present the procedural semantics of logic programs based on SLDresolution using the left-to-right selection rule implemented by most Prolog systems.
More details on logic programming can be found in [Apt 1997], for example.
Definition 2.2 (Derivation, Termination). Let Q be a query A1 , . . . , Am , let c
be a clause H :– B1 , . . . , Bk . Then Q′ is a resolvent of Q and c using θ (denoted
Q ⊢c,θ Q′ ) if θ is the mgu3 of A1 and H, and Q′ = (B1 , . . . , Bk , A2 , . . . , Am )θ.
A derivation of a program P and Q is a possibly infinite sequence Q0 , Q1 , . . . of
queries with Q0 = Q where for all i, we have Qi ⊢ci+1 ,θi+1 Qi+1 for some substitution
θi+1 and some fresh variant ci+1 of a clause of P. For a derivation Q0 , . . . , Qn as
above, we also write Q0 ⊢nP,θ1 ...θn Qn or Q0 ⊢nP Qn , and we also write Qi ⊢P Qi+1
for Qi ⊢ci+1 ,θi+1 Qi+1 . The query Q terminates for P if all derivations of P and Q
are finite.
Our notion of derivation coincides with logic programming without an occur
check [Colmerauer 1982] as implemented in recent Prolog systems such as SICStus
or SWI. Since we consider only definite logic programs, any program which is terminating without occur check is also terminating with occur check, but not vice versa.
So if our approach detects “termination”, then the program is indeed terminating,
no matter whether one uses logic programming with or without occur check. In
other words, our approach is sound for both kinds of logic programming, whereas
most other approaches only consider logic programming with occur check.
Example 2.3. Regard a program P with the clauses p(X) :– equal(X, s(X)), p(X)
and equal(X, X). We obtain p(X) ⊢2P p(s(s(. . .))) ⊢2P p(s(s(. . .))) ⊢2P . . ., where
s(s(. . .)) is the term containing infinitely many nested s-symbols. So the finite
query p(X) leads to a derivation with infinite (rational) queries. While p(X) is
not terminating according to Definition 2.2, it would be terminating if one uses
logic programming with occur check. Indeed, tools like cTI [Mesnard and Bagnara
2005] and TerminWeb [Codish and Taboch 1999] report that such queries are “terminating”. So in contrast to our technique, such tools are in general not sound for
logic programming without occur check, although this form of logic programming
is typically used in practice.
2.2 Term Rewriting
Now we define TRSs and introduce the notion of infinitary constructor rewriting.
For further details on term rewriting we refer to [Baader and Nipkow 1998].
Definition 2.4 (Infinitary Constructor Rewriting). A TRS R is a finite set of
3 Note that for finite sets of rational atoms or terms, unification is decidable, the mgu is unique
modulo renaming, and it is a substitution with rational terms [Huet 1976].

ACM Transactions on Computational Logic, Vol. V, No. N, 20YY.

Automated Termination Proofs for Logic Programs by Term Rewriting

·

9

rules ℓ → r with ℓ, r ∈ T (Σ, V) and ℓ ∈
/ V.4 We divide the signature into defined
symbols ΣD = {f | ℓ → r ∈ R, root(ℓ) = f } and constructors ΣC = Σ \ ΣD . R’s
infinitary constructor rewrite relation is denoted →R : for s, t ∈ T ∞ (Σ, V) we have
s →R t if there is a rule ℓ → r, a position pos and a substitution σ : V → T ∞ (ΣC , V)
∗
with s|pos = ℓσ and t = s[rσ]pos . Let →nR , →≥n
R , →R denote rewrite sequences
of n steps, of at least n steps, and of arbitrary many steps, respectively (where
n ≥ 0). A term t is terminating for R if there is no infinite sequence of the form
t →R t1 →R t2 →R . . . A TRS R is terminating if all terms are terminating for R.
The above definition of →R differs from the usual rewrite relation in two aspects:
(i) We only permit instantiations of rule variables by constructor terms.
(ii) We use substitutions with possibly non-rational infinite terms.
In Example 3.2 and 3.3 in the next section, we will motivate these modifications
and show that there are TRSs which terminate w.r.t. the usual rewrite relation,
but are non-terminating w.r.t. infinitary constructor rewriting and vice versa.
3. TRANSFORMING LOGIC PROGRAMS INTO TERM REWRITE SYSTEMS
Now we modify the transformation of logic programs into TRSs from Section 1 to
make it applicable for arbitrary (possibly non-well-moded) programs as well. We
present the new transformation in Section 3.1 and prove its soundness in Section 3.2.
Later in Section 6 we will formally prove that the classical transformation is strictly
subsumed by our new one.
3.1 The Improved Transformation
Instead of separating between input and output positions of a predicate p/n, now
we keep all arguments both for pin and pout (i.e., pin and pout have arity n).
Definition 3.1 (Transformation). A logic program P over (Σ, ∆) is transformed
into the following TRS RP over ΣP = Σ ∪ {pin /n, pout /n | p/n ∈ ∆} ∪ {uc,i | c ∈
P, 1 ≤ i ≤ k, where k is the number of atoms in the body of c }.
• For each fact p(~s) in P, the TRS RP contains the rule pin (~s) → pout (~s).
• For each clause c of the form p(~s) :– p1 (~s1 ), . . . , pk (~sk ) in P, RP contains:
pin (~s) → uc,1 (p1in (~s1 ), V(~s))
uc,1 (p1out (~s1 ), V(~s)) → uc,2 (p2in (~s2 ), V(~s) ∪ V(~s1 ))
...
uc,k (pkout (~sk ), V(~s) ∪ V(~s1 ) ∪ . . . ∪ V(~sk−1 )) → pout (~s)
The following two examples motivate the need for infinitary constructor rewriting
in Definition 3.1, i.e., they motivate Modifications (i) and (ii) in Section 2.2.
4 In

standard term rewriting, one usually requires V(r) ⊆ V(ℓ) for all rules ℓ → r. The reason
is that otherwise the standard rewrite relation is never well founded. However, the infinitary
constructor rewrite relation defined here can be well founded even if V(r) 6⊆ V(ℓ).
ACM Transactions on Computational Logic, Vol. V, No. N, 20YY.

10

·

P. Schneider-Kamp, J. Giesl, A. Serebrenik, R. Thiemann

Example 3.2. For the logic program of Example 1.1, the transformation of Definition 3.1 yields the following TRS.
pin (X, X) → pout (X, X)

(1)

pin (f(X), g(Y )) → u1 (pin (f(X), f(Z)), X, Y )
u1 (pout (f(X), f(Z)), X, Y ) → u2 (pin (Z, g(Y )), X, Y, Z)

(2)
(3)

u2 (pout (Z, g(Y )), X, Y, Z) → pout (f(X), g(Y ))

(4)

This example shows why rules of TRSs may only be instantiated with constructor
terms (Modification (i)). The reason is that local variables like Z (i.e., variables
occurring in the body but not in the head of a clause) give rise to rules ℓ → r where
V(r) 6⊆ V(ℓ) (cf. Rule (2)). Such rules are never terminating in standard term
rewriting. However, in our setting one may only instantiate Z with constructor
terms. So in contrast to the old transformation in Example 1.2, now all terms
pin (t1 , t2 ) terminate for the TRS if t1 is finite, since now the second argument
of pin prevents an infinite application of Rule (2). Indeed, constructor rewriting
correctly simulates the behavior of logic programs, since the variables in a logic
program are only instantiated by “constructor terms”.
For the non-well-moded program of Example 1.3, one obtains a similar TRS
where g(Y ) is replaced by g(W ) in the right-hand side of Rule (3) and the lefthand side of Rule (4). Again, all terms pin (t1 , t2 ) are terminating for this TRS
provided that t1 is finite. Thus, we can now handle programs where the classical transformation of [Arts and Zantema 1995; Chtourou and Rusinowitch 1993;
Ganzinger and Waldmann 1993; Ohlebusch 2001] failed, cf. Goals (A) and (B) in
Section 1.2.
Derivations in logic programming use unification, while rewriting is defined by
matching. Example 3.3 shows that to simulate unification by matching, we have to
consider substitutions with infinite and even non-rational terms (Modification (ii)).
Example 3.3. Let P be ordered(cons(X, cons(s(X), XS ))) :– ordered(cons(s(X), XS )).
If one only considers rewriting with finite or rational terms, then the transformed
TRS RP is terminating. However, the query ordered(YS ) is not terminating for P.
Thus, to obtain a sound approach, RP must also be non-terminating. Indeed, the
term t = orderedin (cons(X, cons(s(X), cons(s2 (X), . . .)))) is non-terminating with
RP ’s rule orderedin (cons(X, cons(s(X), XS ))) → u(orderedin (cons(s(X), XS )), X,
XS ). The non-rational term t corresponds to the infinite derivation with the query
ordered(YS ).
3.2 Soundness of the Transformation
We first show an auxiliary lemma that is needed to prove the soundness of the
transformation. It relates derivations with the logic program P to rewrite sequences
with the TRS RP .
Lemma 3.4 (Connecting P and RP ). Let P be a program, let ~t be terms from
≥n
T (Σ, V), let p(~t) ⊢nP,σ Q. If Q = ✷, then pin (~t)σ →R
pout (~t)σ. Otherwise, if
P
≥n
~
Q is “q(~v ), . . .”, then pin (t)σ →RP r for a term r containing the subterm qin (~v ).
rat

ACM Transactions on Computational Logic, Vol. V, No. N, 20YY.

Automated Termination Proofs for Logic Programs by Term Rewriting

·

11

Proof. Let p(~t) = Q0 ⊢c1 ,θ1 . . . ⊢cn ,θn Qn = Q with σ = θ1 . . . θn . We use
induction on n. The base case n = 0 is trivial, since Q = p(~t) and pin (~t) →0RP pin (~t).
Now let n ≥ 1. We first regard the case Q1 = ✷ and n = 1. Then c1 is a
fact p(~s) and θ1 is the mgu of p(~t) and p(~s). Note that such mgu’s instantiate all
variables with constructor terms (as symbols of Σ are constructors of RP ). We
obtain pin (~t)θ1 = pin (~s)θ1 →RP pout (~s)θ1 = pout (~t)θ1 where σ = θ1 .
Finally, let Q1 6= ✷. Thus, c1 is p(~s) :– p1 (s~1 ), . . . , pk (s~k ) and Q1 is p1 (s~1 )θ1 , . . . ,
pk (s~k )θ1 where θ1 is the mgu of p(~t) and p(~s). There is an i with 1 ≤ i ≤ k
nj
✷. Moresuch that for all j with 1 ≤ j ≤ i − 1 we have pj (~sj )σ0 . . . σj−1 ⊢P,σ
j
ni
over, if Q = ✷ then we can choose i = k and pi (~si )σ0 . . . σi−1 ⊢P,σi ✷. Othi
erwise, if Q is “q(~v ), . . .”, then we can choose i such that pi (~si )σ0 . . . σi−1 ⊢nP,σ
i
q(~v ), . . . Here, n = n1 + . . . + ni + 1, σ0 = θ1 , σ1 = θ2 . . . θn1 +1 , . . . , and
σi = θn1 +...+ni−1 +2 . . . θn1 +...+ni +1 . So σ = σ0 . . . σi .
≥n
By the induction hypothesis we have pjin (~sj )σ0 . . . σj →RPj pjout (~sj )σ0 . . . σj
≥n

and thus also pjin (~sj )σ →RPj pjout (~sj )σ. Moreover, if Q = ✷ then we also have
≥ni
piout (~si )σ where i = k. Otherwise, if Q is “q(~v ), . . .”, then the
piin (~si )σ →R
P
≥ni ′
r , where r′ contains qin (~v ). Thus
induction hypothesis implies piin (~si )σ →R
P
pin (~t)σ = pin (~s)σ →RP
≥n1
→R
P
→RP
≥n2
→R
P
≥n +...+ni−1
→RP3

uc1 ,1 (p1in (~s1 ), V(~s))σ
uc1 ,1 (p1out (~s1 ), V(~s))σ
uc1 ,2 (p2in (~s2 ), V(~s) ∪ V(~s1 ))σ
uc1 ,2 (p2out (~s2 ), V(~s) ∪ V(~s1 ))σ
uc1 ,i (piin (~si ), V(~s) ∪ V(~s1 ) ∪ . . . ∪ V(~si−1 ))σ

Moreover, if Q = ✷, then i = k and the rewrite sequence yields pout (~t)σ, since
≥ni
uc1 ,i (piout (~si ), V(~s) ∪ . . . ∪ V(~si−1 ))σ
uc1 ,i (piin (~si ), V(~s) ∪ . . . ∪ V(~si−1 ))σ →R
P
→RP pout (~s)σ = pout (~t)σ.

Otherwise, if Q is “q(~v ), . . .”, then rewriting yields a term containing qin (~v ):
≥ni
uc1 ,i (r′ , V(~s)σ ∪ . . . ∪ V(~si−1 )σ).
uc1 ,i (piin (~si ), V(~s) ∪ . . . ∪ V(~si−1 ))σ →R
P

For the soundness proof, we need another lemma which states that we can restrict
ourselves to non-terminating queries which only consist of a single atom.
Lemma 3.5 (Non-Terminating Queries). Let P be a logic program. Then
for every infinite derivation Q0 ⊢P Q1 ⊢P . . ., there is a Qi of the form “q(~v ), . . .”
with i > 0 such that the query q(~v ) is also non-terminating.
Proof. Assume that for all i > 0, the first atom in Qi does not have an infinite
derivation. Then for each Qi there are two cases: either the first atom fails or
it can successfully be proved. In the former case, there is no infinite reduction
from Qi which contradicts the infiniteness of the derivation from Q0 . Thus for all
i > 0, the first atom of Qi is successfully proved in ni steps during the derivation
Q0 ⊢P Q1 ⊢P . . . Let m be the number of atoms in Q1 . But then Q1+n1 +...+nm is
the empty query ✷ which again contradicts the infiniteness of the derivation.
We use argument filters to characterize the classes of queries whose termination
we want to analyze. Related definitions can be found in, e.g., [Arts and Giesl 2000;
ACM Transactions on Computational Logic, Vol. V, No. N, 20YY.

12

·

P. Schneider-Kamp, J. Giesl, A. Serebrenik, R. Thiemann

Leuschel and Sørensen 1996].
Definition 3.6 (Argument Filter). A function π : Σ ∪ ∆ → 2N is an argument
filter π over a signature (Σ, ∆) if and only if π(f /n) ⊆ {1, . . . , n} for every f /n ∈
Σ ∪ ∆. We extend π to terms and atoms by defining π(x) = x if x is a variable and
π(f (t1 , . . . , tn )) = f (π(ti1 ), . . . , π(tik )) if π(f /n) = {i1 , . . . , ik } with i1 < . . . < ik .
Here, the new terms and atoms are from the filtered signature (Σπ , ∆π ) where
f /n ∈ Σ implies f /k ∈ Σπ and likewise for ∆π . For a logic program P we write
(ΣPπ , ∆Pπ ) instead of ((ΣP )π , (∆P )π ). For any TRS R, we define π(R) = {π(ℓ) →
π(r) | ℓ → r ∈ R}. The set of all argument filters over a signature (Σ, ∆) is denoted
by AF (Σ, ∆). We write AF (Σ) instead of AF (Σ, ∅) and speak of an argument filter
“over Σ”. We also write π(f ) instead of π(f /n) if the arity of f is clear from the
context.
An argument filter π ′ is a refinement of a filter π if and only if π ′ (f ) ⊆ π(f ) for
all f ∈ Σ ∪ ∆.
Argument filters specify those positions which have to be instantiated with finite
ground terms. Then, we analyze termination of all queries Q where π(Q) is a
(finite) ground atom. In Example 1.1, we wanted to prove termination for all
queries p(t1 , t2 ) where t1 is finite and ground. These queries are described by the
filter π(h) = {1} for all h ∈ {p, f, g}. Thus, we have π(p(t1 , t2 )) = p(π(t1 )).
Note that argument filters also operate on function instead of just predicate
symbols. Therefore, they can describe more sophisticated classes of queries than
the classical approach of [Arts and Zantema 1995; Chtourou and Rusinowitch 1993;
Ganzinger and Waldmann 1993; Ohlebusch 2001] which only distinguishes between
input and output positions of predicates. For example, if one wants to analyze all
queries append(t1 , t2 , t3 ) where t1 is a finite list, one would use the filter π(append) =
{1} and π(•) = {2}, where “•” is the list constructor (i.e., •(X, L) = [X|L]). Of
course, our method can easily prove that all these queries are terminating for the
program of Example 1.4.
Now we show the soundness theorem: to prove termination of all queries Q where
π(Q) is a finite ground atom, it suffices to show termination of all those terms pin (~t)
for the TRS RP where π(pin (~t)) is a finite ground term and where ~t only contains
function symbols from the logic program P. Here, π has to be extended to the new
function symbols pin by defining π(pin ) = π(p).
Theorem 3.7 (Soundness of the Transformation). Let P be a logic program and let π be an argument filter over (Σ, ∆). We extend π such that π(pin ) =
π(p) for all p ∈ ∆. Let S = {pin (~t) | p ∈ ∆, ~t ∈ T~ ∞ (Σ, V), π(pin (~t)) ∈ T (ΣPπ ) }.
If all terms s ∈ S are terminating for RP , then all queries Q ∈ Arat (Σ, ∆, V) with
π(Q) ∈ A(Σπ , ∆π ) are terminating for P.5
Proof. Assume that there is a non-terminating query p(~t) as above with p(~t) ⊢P
Q1 ⊢P Q2 ⊢P . . . By Lemma 3.5 there is an i1 > 0 with Qi1 = q1 (~v1 ), . . . and an
1
infinite derivation q1 (~v1 ) ⊢P Q′1 ⊢P Q′2 ⊢P . . . From p(~t) ⊢iP,σ
q1 (~v1 ), . . . and
0
≥i
1
Lemma 3.4 we get pin (~t)σ0 →RP r1 , where r1 contains the subterm q1in (~v1 ).
5 It

is currently open whether the converse holds as well. For a short discussion see Section 7.2.

ACM Transactions on Computational Logic, Vol. V, No. N, 20YY.

Automated Termination Proofs for Logic Programs by Term Rewriting

·

13

By Lemma 3.5 again, there is an i2 > 0 with Q′i2 = q2 (~v2 ), . . . and an infinite
2
derivation q2 (~v2 ) ⊢P Q′′1 ⊢P . . . From q1 (~v1 ) ⊢iP,σ
q2 (~v2 ), . . . and Lemma 3.4 we
1
≥i
≥i
2
1
~
get pin (t)σ0 σ1 →RP r1 σ1 →RP r2 , where r2 contains the subterm q2in (~v2 ).
Continuing this reasoning we obtain an infinite sequence σ0 , σ1 , . . . of substitutions. For each j ≥ 0, let µj = σj σj+1 . . . result from the infinite composition of
these substitutions.6 Since rj µj is an instance of rj σj . . . σn for all n ≥ j, we obtain
that pin (~t)µ0 is non-terminating for RP :
≥i3
≥i2
1
pin (~t)µ0 →≥i
RP r1 µ1 →RP r2 µ2 →RP . . .

As π(p(~t)) ∈ A(Σπ , ∆π ) and thus π(pin (~t)) = π(pin (~t)µ0 ) ∈ T (ΣPπ ), this is a
contradiction.
4. TERMINATION OF INFINITARY CONSTRUCTOR REWRITING
One of the most powerful methods for automated termination analysis of rewriting
is the dependency pair (DP) method [Arts and Giesl 2000] which is implemented
in most current termination tools for TRSs. However, since the DP method only
proves termination of term rewriting with finite terms, its use is not sound in
our setting. Nevertheless, we now show that only very slight modifications are
required to adapt dependency pairs from ordinary rewriting to infinitary constructor
rewriting. So any rewriting tool implementing dependency pairs can easily be
modified in order to prove termination of infinitary constructor rewriting as well.
Then, it can also analyze termination of logic programs using the transformation
of Definition 3.1.
Moreover, dependency pairs are a general framework that permits the integration
of any termination technique for TRSs [Giesl et al. 2005, Thm. 36]. Therefore,
instead of adapting each technique separately, it is sufficient only to adapt the DP
framework to infinitary constructor rewriting. Then, any termination technique
can be directly used for infinitary constructor rewriting. In Section 4.1, we adapt
the notions and the main termination criterion of the dependency pair method to
infinitary constructor rewriting and in Section 4.2 we show how to automate this
criterion by adapting the “DP processors” of the DP framework.
4.1 Dependency Pairs for Infinitary Rewriting
Let R be a TRS. For each defined symbol f /n ∈ ΣD , we extend the set of constructors ΣC by a fresh tuple symbol f ♯ /n. We often write F instead of f ♯ . For
6 The

composition of infinitely many substitutions σ0 , σ1 , . . . is defined as follows. The definition
ensures that tσ0 σ1 . . . is an instance of tσ0 . . . σn for all terms (or atoms) t and all n ≥ 0. It
suffices to define the symbols at the positions of tσ0 σ1 . . . for any term t. Obviously, pos is a
position of tσ0 σ1 . . . iff pos is a position of tσ0 . . . σn for some n ≥ 0. We define that the symbol
of tσ0 σ1 . . . at such a position pos is f ∈ Σ iff f is at position pos in tσ0 . . . σm for some m ≥ 0.
Otherwise, (tσ0 . . . σn )|pos = X0 ∈ V. Let n = i0 < i1 < . . . be the maximal (finite or infinite)
sequence with σij +1 (Xj ) = . . . = σij+1 −1 (Xj ) = Xj and σij+1 (Xj ) = Xj+1 for all j. We
require Xj 6= Xj+1 , but permit Xj = Xj ′ otherwise. If this sequence is finite (i.e., it has the
form n = i0 < . . . < im ), then we define (tσ0 σ1 . . .)|pos = Xm . Otherwise, the substitutions
perform infinitely many variable renamings. In this case, we use one special variable Z∞ and
define (tσ0 σ1 . . .)|pos = Z∞ . So if σ0 (X) = Y , σ1 (Y ) = X, σ2 (X) = Y , σ3 (Y ) = X, etc., we
define Xσ0 σ1 . . . = Y σ0 σ1 . . . = Z∞ .
ACM Transactions on Computational Logic, Vol. V, No. N, 20YY.

14

·

P. Schneider-Kamp, J. Giesl, A. Serebrenik, R. Thiemann

t = g(~t) with g ∈ ΣD , let t♯ denote g ♯ (~t).
Definition 4.1 (Dependency Pair [Arts and Giesl 2000]). The set of dependency
pairs for a TRS R is DP (R) = {ℓ♯ → t♯ | ℓ → r ∈ R, t is a subterm of r,
root(t) ∈ ΣD }.
Example 4.2. Consider again the logic program of Example 1.1 which was transformed into the following TRS R in Example 3.2.
pin (X, X) → pout (X, X)

(1)

pin (f(X), g(Y )) → u1 (pin (f(X), f(Z)), X, Y )
u1 (pout (f(X), f(Z)), X, Y ) → u2 (pin (Z, g(Y )), X, Y, Z)

(2)
(3)

u2 (pout (Z, g(Y )), X, Y, Z) → pout (f(X), g(Y ))

(4)

For this TRS R, we have ΣD = {pin , u1 , u2 } and DP (R) is
Pin (f(X), g(Y )) → Pin (f(X), f(Z))
Pin (f(X), g(Y )) → U1 (pin (f(X), f(Z)), X, Y )

(5)
(6)

U1 (pout (f(X), f(Z)), X, Y ) → Pin (Z, g(Y ))
U1 (pout (f(X), f(Z)), X, Y ) → U2 (pin (Z, g(Y )), X, Y, Z)

(7)
(8)

While Definition 4.1 is from [Arts and Giesl 2000], all following definitions and
theorems are new. They extend existing concepts from ordinary to infinitary constructor rewriting.
For termination, one tries to prove that there are no infinite chains of dependency
pairs. Intuitively, a dependency pair corresponds to a function call and a chain represents a possible sequence of calls that can occur during rewriting. Definition 4.3
extends the notion of chains to infinitary constructor rewriting. To this end, we
use an argument filter π that describes which arguments of function symbols have
to be finite terms. So if π does not delete arguments (i.e., if π(f ) = {1, . . . , n} for
all f /n), then this corresponds to ordinary (finitary) constructor rewriting and if
π deletes all arguments (i.e., if π(f ) = ∅ for all f ), then this corresponds to full
infinitary constructor rewriting. In Definition 4.3, the TRS D usually stands for a
set of dependency pairs. (Note that if R is a TRS, then DP (R) is also a TRS.)
Definition 4.3 (Chain). Let D, R be TRSs and π be an argument filter. A (possibly infinite) sequence of pairs s1 → t1 , s2 → t2 , . . . from D is a (D, R, π)-chain iff
• for all i ≥ 1, there are substitutions σi : V → T ∞ (ΣC , V) such that ti σi →∗R
si+1 σi+1 , and
• for all i ≥ 1, we have π(si σi ), π(ti σi ) ∈ T (Σπ ). Moreover, if the rewrite sequence
from ti σi to si+1 σi+1 has the form ti σi = q0 →R . . . →R qm = si+1 σi+1 , then
for all terms in this rewrite sequence we have π(q0 ), . . . , π(qm ) ∈ T (Σπ ) as well.
So all terms in the sequence have finite ground terms on those positions which
are not filtered away by π.
In Example 4.2, “(6), (7)” is a chain for any argument filter π: if one instantiates
X and Z with the same finite ground term, then (6)’s instantiated right-hand side
rewrites to an instance of (7)’s left-hand side. Note that if one uses an argument
ACM Transactions on Computational Logic, Vol. V, No. N, 20YY.

Automated Termination Proofs for Logic Programs by Term Rewriting

·

15

filter π which permits an instantiation of X and Z with the infinite term f(f(. . .)),
then there is also an infinite chain “(6), (7), (6), (7), . . . ”
In order to prove termination of a program P, by Theorem 3.7 we have to show
that all terms pin (~t) are terminating for RP whenever π(pin (~t)) is a finite ground
term and ~t only contains function symbols from the logic program (i.e., ~t contains no
defined symbols of the TRS RP ). Theorem 4.4 states that one can prove absence of
infinite (DP (RP ), RP , π ′ )-chains instead. Here, π ′ is a filter which filters away “at
least as much” as π. However, π ′ has to be chosen in such a way that the filtered
TRSs π ′ (DP (RP )) and π ′ (RP ) satisfy the “variable condition”, i.e., V(π ′ (r)) ⊆
V(π ′ (ℓ)) for all ℓ → r ∈ DP (RP ) ∪ RP . Then the filter π ′ detects all potentially
infinite subterms in rewrite sequences (i.e., all subterms which correspond to “nonunification-free parts” of P, i.e., to non-ground subterms when “executing” the
program P).
Theorem 4.4 (Proving Infinitary Termination). Let R be a TRS over Σ
and let π be an argument filter over Σ. We extend π to tuple symbols such that
π(F ) = π(f ) for all f ∈ ΣD . Let π ′ be a refinement of π such that π ′ (DP (R)) and
π ′ (R) satisfy the variable condition.7 If there is no infinite (DP (R), R, π ′ )-chain,
then all terms f (~t) with ~t ∈ T~ ∞ (ΣC , V) and π(f (~t)) ∈ T (Σπ ) are terminating for
R.
Proof. Assume there is a non-terminating term f (~t) as above. Since ~t does
not contain defined symbols, the first rewrite step in the infinite sequence is on
the root position with a rule ℓ = f (~ℓ) → r where ℓσ1 = f (~t). Since σ1 does not
introduce defined symbols, all defined symbols of rσ1 occur on positions of r. So
there is a subterm r′ of r with defined root such that r′ σ1 is also non-terminating.
Let r′ denote the smallest such subterm (i.e., for all proper subterms r′′ of r′ ,
the term r′′ σ1 is terminating). Then ℓ♯ → r′♯ is the first dependency pair of the
infinite chain that we construct. Note that π(ℓσ1 ) and thus, π(ℓ♯ σ1 ) and hence,
also π ′ (ℓ♯ σ1 ) = π ′ (F (~t)) is a finite ground term by assumption. Moreover, as
ℓ♯ → r′♯ ∈ DP (R) and as π ′ (DP (R)) satisfies the variable condition, π ′ (r′♯ σ1 ) is
finite and ground as well.
The infinite sequence continues by rewriting r′ σ1 ’s proper subterms repeatedly.
During this rewriting, the left-hand sides of rules are instantiated by constructor
substitutions (i.e., substitutions with range T ∞ (ΣC , V)). As π ′ (R) satisfies the
variable condition, the terms remain finite and ground when applying the filter
π ′ . Finally, a root rewrite step is performed again. Repeating this construction
infinitely many times results in an infinite chain.
The following corollary combines Theorem 3.7 and Theorem 4.4. It describes
how we use the DP method for proving termination of logic programs.
7 To see why the variable condition is needed in Theorem 4.4, let R = {g(X) → f(X), f(s(X)) →
f(X)} and π = π ′ where π ′ (g) = ∅, π ′ (f) = π ′ (F) = π ′ (s) = {1}. R’s first rule violates the
variable condition: V(π ′ (f(X))) = {X} 6⊆ V(π ′ (g(X))) = ∅. There is no infinite chain, since π ′
does not allow us to instantiate the variable X in the dependency pair F(s(X)) → F(X) by an
infinite term. Nevertheless, there is a non-terminating term g(s(s(. . .))) which is filtered to a finite
ground term π ′ (g(s(s(. . .)))) = g.

ACM Transactions on Computational Logic, Vol. V, No. N, 20YY.

16

·

P. Schneider-Kamp, J. Giesl, A. Serebrenik, R. Thiemann

Corollary 4.5 (Termination of Logic Prog. by Dependency Pairs).
Let P be a logic program and let π be an argument filter over (Σ, ∆). We extend
π to ΣP and to tuple symbols such that π(pin ) = π(Pin ) = π(p) for all p ∈ ∆. For
all other symbols f /n that are not from Σ or ∆, we define π(f /n) = {1, . . . , n}.
Let π ′ be a refinement of π such that π ′ (DP (RP )) and π ′ (RP ) satisfy the variable
condition. If there is no infinite (DP (RP ), RP , π ′ )-chain, then all queries Q ∈
Arat (Σ, ∆, V) with π(Q) ∈ A(Σπ , ∆π ) are terminating for P.
Example 4.6. We want to prove termination of Example 1.1 for all queries Q
where π(Q) is finite and ground for the filter π(h) = {1} for all h ∈ {p, f, g}. By
Corollary 4.5, it suffices to show absence of infinite (DP (R), R, π ′ )-chains. Here,
R is the TRS {(1), . . . , (4)} from Example 3.2 and DP (R) are Rules (5) – (8) from
Example 4.2. The filter π ′ has to satisfy π ′ (h) ⊆ π(h) = {1} for h ∈ {f, g} and
moreover, π ′ (pin ) and π ′ (Pin ) must be subsets of π(pin ) = π(Pin ) = π(p) = {1}.
Moreover, we have to choose π ′ such that the variable condition is fulfilled. So while
π is always given, π ′ has to be determined automatically. Of course, there are only
finitely many possibilities for π ′ . In particular, defining π ′ (h) = ∅ for all symbols
h is always possible. But to obtain a successful termination proof afterwards, one
should try to generate filters where the sets π ′ (h) are as large as possible, since such
filters provide more information about the finiteness of arguments. We will present
suitable heuristics for finding such filters π ′ in Section 5. In our example, we use
π ′ (pin ) = π ′ (Pin ) = π ′ (f) = π ′ (g) = {1}, π ′ (pout ) = π ′ (u1 ) = π ′ (U1 ) = {1, 2},
and π ′ (u2 ) = π ′ (U2 ) = {1, 2, 4}. For the non-well-moded Example 1.3 we choose
π ′ (g) = ∅ instead to satisfy the variable condition.
So to automate the criterion of Corollary 4.5, we have to tackle two problems:
(I) We start with a given filter π which describes the set of queries whose termination should be proved. Then we have to find a suitable argument filter π ′ that
refines π in such a way that the variable condition of Theorem 4.4 is fulfilled and
that the termination proof is “likely to succeed”. This problem will be discussed
in Section 5.
(II) For the chosen argument filter π ′ , we have to prove that there is no infinite
(DP (RP ), RP , π ′ )-chain. We show how to do this in the following subsection.
4.2 Automation by Adapting the DP Framework
Now we show how to prove absence of infinite (DP (R), R, π)-chains automatically.
To this end, we adapt the DP framework of [Giesl et al. 2005] to infinitary rewriting.
In this framework, we now consider arbitrary DP problems (D, R, π) where D and
R are TRSs and π is an argument filter. Our goal is to show that there is no infinite
(D, R, π)-chain. In this case, we call the problem finite. Termination techniques
should now be formulated as DP processors which operate on DP problems instead
of TRSs. A DP processor Proc takes a DP problem as input and returns a new
set of DP problems which then have to be solved instead. Proc is sound if for
all DP problems d, d is finite whenever all DP problems in Proc(d) are finite. So
termination proofs start with the initial DP problem (DP (R), R, π). Then this
problem is transformed repeatedly by sound DP processors. If the final processors
return empty sets of DP problems, then termination is proved.
ACM Transactions on Computational Logic, Vol. V, No. N, 20YY.

Automated Termination Proofs for Logic Programs by Term Rewriting

·

17

In Theorem 4.9, 4.11, and 4.13 we will recapitulate three of the most important
existing DP processors [Giesl et al. 2005] and describe how they must be modified
for infinitary constructor rewriting. To this end, they now also have to take the
argument filter π into account. The first processor uses an estimated dependency
graph to estimate which dependency pairs can follow each other in chains.
Definition 4.7 (Estimated Dependency Graph). Let (D, R, π) be a DP problem.
The nodes of the estimated (D, R, π)-dependency graph are the pairs of D and there
is an arc from s → t to u → v iff CAP (t) and a variant u′ of u unify with an mgu
µ where π(CAP (t)µ) = π(u′ µ) is a finite term. Here, CAP (t) replaces all subterms
of t with defined root symbol by different fresh variables.
Example 4.8. For the DP problem (DP (R), R, π ′ ) from Example 4.6 we obtain:
(5) oo

(7)
ee

%%

(6)

// (8)

For example, there is an arc (6) → (7), as CAP (U1 (pin (f(X), f(Z)), X, Y )) =
U1 (V, X, Y ) unifies with U1 (pout (f(X ′ ), f(Z ′ )), X ′ , Y ′ ) by instantiating the arguments of U1 with finite terms. But there are no arcs (5) → (5) or (5) → (6), since
Pin (f(X), f(Z)) and Pin (f(X ′ ), g(Y ′ )) do not unify, even if one instantiates Z and
Y ′ by infinite terms (as permitted by the filter π ′ (Pin ) = {1}).
Note that filters are used to detect potentially infinite arguments, but these arguments are not removed, since they can still be useful in the termination proof. In
Example 4.8, they are needed to determine that (5) has no outgoing arcs.
If s → t, u → v is a (D, R, π)-chain then there is an arc from s → t to u → v
in the estimated dependency graph. Thus, absence of infinite chains can be proved
separately for each maximal strongly connected component (SCC) of the graph.
This observation is used by the following processor to modularize termination proofs
by decomposing a DP problem into sub-problems. If there are n SCCs in the graph
and if Di are the dependency pairs of the i-th SCC (for 1 ≤ i ≤ n), then one can
decompose the set of dependency pairs D into the subsets D1 , . . . , Dn .
Theorem 4.9 (Dependency Graph Processor). For a DP problem (D, R,
π), let Proc return {(D1 , R, π), . . . , (Dn , R, π)} where D1 , . . . , Dn are the sets of
nodes of the SCCs in the estimated dependency graph. Then Proc is sound.
Proof. We prove that if s → t, u → v is a chain, then there is an arc from s → t
to u → v in the estimated dependency graph. This suffices for Theorem 4.9, since
then every infinite (D, R, π)-chain corresponds to an infinite path in the graph. This
path ends in an SCC with nodes Di and thus, there is also an infinite (Di , R, π)chain. Hence, if all (Di , R, π) are finite DP problems, then so is (D, R, π).
Let s → t, u → v be a (D, R, π)-chain, i.e., tσ1 →∗R uσ2 for some constructor
substitutions σ1 , σ2 where π(tσ1 ) and π(uσ2 ) are finite. Let pos 1 , . . . , pos n be the
top positions where t has defined symbols. Then CAP (t) = t[Y1 ]pos 1 . . . [Yn ]pos n
for fresh variables Yj . Moreover, let the variant u′ result from u by replacing every
X ∈ V(u) by a fresh variable X ′ . Thus, the substitution σ with σ(X ′ ) = σ2 (X)
for all X ∈ V(u), σ(X) = σ1 (X) for all X ∈ V(t), and σ(Yj ) = uσ2 |pos j unifies
CAP (t) and u′ . So there is also an mgu µ where σ = µτ for some substitution τ .
ACM Transactions on Computational Logic, Vol. V, No. N, 20YY.

18

·

P. Schneider-Kamp, J. Giesl, A. Serebrenik, R. Thiemann

Moreover, since π(uσ2 ) = π(u′ σ) is finite, the term π(u′ µ) is finite, too. Hence, by
Definition 4.7 there is indeed an arc from s → t to u → v.
Example 4.10. In Example 4.8, the only SCC consists of (6) and (7). Thus, the
dependency graph processor transforms the initial DP problem (DP (R), R, π ′ ) into
({(6), (7)}, R, π ′ ), i.e., it deletes the dependency pairs (5) and (8).
The next processor is based on reduction pairs (%, ≻) where % and ≻ are relations
on finite terms. Here, % is reflexive, transitive, monotonic (i.e., s % t implies
f (. . . s . . .) % f (. . . t . . .) for all function symbols f ), and stable (i.e., s % t implies
sσ % tσ for all substitutions σ) and ≻ is a stable well-founded order compatible
with % (i.e., % ◦ ≻ ⊆ ≻ or ≻ ◦ % ⊆ ≻). There are many techniques to search
for such relations automatically (recursive path orders, polynomial interpretations,
etc. [Dershowitz 1987]).
For a DP problem (D, R, π), we now try to find a reduction pair (%, ≻) such that
all filtered R-rules are weakly decreasing (w.r.t. %) and all filtered D-dependency
pairs are weakly or strictly decreasing (w.r.t. % or ≻).8 Requiring π(ℓ) % π(r) for
all ℓ → r ∈ R ensures that in chains s1 → t1 , s2 → t2 , . . . with ti σi →∗R si+1 σi+1
as in Definition 4.3, we have π(ti σi ) % π(si+1 σi+1 ). Hence, if a reduction pair
satisfies the above conditions, then the strictly decreasing dependency pairs (i.e.,
those s → t ∈ D where π(s) ≻ π(t)) cannot occur infinitely often in chains. So the
following processor deletes these pairs from D. For any TRS D and any relation ≻,
let D≻π = {s → t ∈ D | π(s) ≻ π(t)}.
Theorem 4.11 (Reduction Pair Processor). Let (%, ≻) be a reduction
pair. Then the following DP processor Proc is sound. For (D, R, π), Proc returns
• {(D \ D≻π , R, π)}, if D≻π ∪ D%π = D and R%π = R
• {(D, R, π)}, otherwise
Proof. We prove this theorem by contradiction, i.e., we assume that (D, R, π)
is infinite and then proceed to show that (D \ D≻π , R, π) has to be infinite, too.
From the assumption that (D, R, π) is infinite, we know that there is an infinite
(D, R, π)-chain s1 → t1 , s2 → t2 , . . . with ti σi →∗R si+1 σi+1 . For any term t we
have π(tσ) = π(t)π(σ) where π(σ)(x) = π(σ(x)) for all x ∈ V. So by stability of ≻
and %, D≻π ∪ D%π = D implies
π(si σi ) = π(si )π(σi ) ( %) π(ti )π(σi ) = π(ti σi ).

(9)

Note that π(si σi ) and π(ti σi ) are finite. Thus, comparing them with % is possible.
Similarly, by the observation π(tσ) = π(t)π(σ) we also get that ti σi →∗R si+1 σi+1
implies π(ti σi ) →∗π(R) π(si+1 σi+1 ). As R%π = R means that π(R)’s rules are decreasing w.r.t. %, by monotonicity and stability of % we get π(ti σi ) % π(si+1 σi+1 ).
With (9), this implies π(s1 σ1 ) ( %) π(t1 σ1 ) % π(s2 σ2 ) ( %) π(t2 σ2 ) % . . . As ≻ is compatible with % and well founded, π(si σi ) ≻ π(ti σi ) only holds for finitely many i.
So sj → tj , sj+1 → tj+1 , . . . is an infinite (D \ D≻π , R, π) chain for some j and thus,
the DP problem (D \ D≻π , R, π) is infinite.
8 We

only consider filtered rules and dependency pairs. Thus, % and ≻ are only used to compare
those parts of terms which remain finite for all instantiations in chains.
ACM Transactions on Computational Logic, Vol. V, No. N, 20YY.

Automated Termination Proofs for Logic Programs by Term Rewriting

·

19

Example 4.12. For the DP problem ({(6), (7)}, R, π ′ ) in Example 4.10, one can
easily find a reduction pair9 where the dependency pair (7) is strictly decreasing
and where (6) and all rules are weakly decreasing after applying the filter π ′ :
Pin (f(X)) % U1 (pin (f(X)), X)
pin (X)
U1 (pout (f(X), f(Z)), X) ≻ Pin (Z)
pin (f(X))
u1 (pout (f(X), f(Z)), X)
u2 (pout (Z, g(Y )), X, Z)

%
%
%
%

pout (X, X)
u1 (pin (f(X)), X)
u2 (pin (Z), X, Z)
pout (f(X), g(Y ))

Thus, the reduction pair processor can remove (7) from the DP problem which
results in ({(6)}, R, π ′ ). By applying the dependency graph processor again, one
obtains the empty set of DP problems, since now the estimated dependency graph
only has the node (6) and no arcs. This proves that the initial DP problem
(DP (R), R, π ′ ) from Example 4.6 is finite and thus, the logic program from Example 1.1 terminates for all queries Q where π(Q) is finite and ground. Note that
termination of the non-well-moded program from Example 1.3 can be shown analogously since finiteness of the initial DP problem can be proved in the same way.
The only difference is that we obtain g instead of g(Y ) in the last inequality above.
As in Theorem 4.9 and 4.11, many other existing DP processors [Giesl et al. 2005]
can easily be adapted to infinitary constructor rewriting as well. Finally, one can
also use the following processor to transform a DP problem (D, R, π) for infinitary
constructor rewriting into a DP problem (π(D), π(R), id) for ordinary rewriting.
Afterwards, any existing DP processor for ordinary rewriting becomes applicable.10
Since any termination technique for TRSs can immediately be formulated as a DP
processor [Giesl et al. 2005, Thm. 36], now any termination technique for ordinary
rewriting can be directly used for infinitary constructor rewriting as well.
Theorem 4.13 (Argument Filter Processor).
Let Proc( (D, R, π) ) =
{(π(D), π(R), id)} where id(f ) = {1, . . . , n} for all f /n. Then Proc is sound.
Proof. If s1 → t1 , s2 → t2 , . . . is an infinite (D, R, π)-chain with the substitutions σi as in Definition 4.3, then π(s1 ) → π(t1 ), π(s2 ) → π(t2 ), . . . is an infinite
(π(D), π(R), id)-chain with the substitutions π(σi ). The reason is that ti σi →∗R
si+1 σi+1 implies π(ti )π(σi ) = π(ti σi ) →∗π(R) π(si+1 σi+1 ) = π(si+1 )π(σi+1 ). Moreover, by Definition 4.3, all terms in the rewrite sequence π(ti σi ) →∗π(R) π(si+1 σi+1 )
are finite.
5. REFINING THE ARGUMENT FILTER
In Section 3 we introduced a new transformation from logic programs P to TRSs RP
and showed that to prove the termination of a class of queries for P, it is sufficient
to analyze the termination behavior of RP . Our criterion to prove termination of
logic programs was summarized in Corollary 4.5.
9 For example, one can use the polynomial interpretation |P (t )| = |p (t )| = |U (t , t )| =
1 1 2
in 1
in 1
|u1 (t1 , t2 )| = |u2 (t1 , t2 , t3 )| = |t1 |, |pout (t1 , t2 )| = |t2 |, |f(t1 )| = |t1 | + 1, and |g(t1 )| = 0.
10 If (D, R, π) results from the transformation of a logic program, then for (π(D), π(R), id) it is
even sound to apply the existing DP processors for innermost rewriting [Giesl et al. 2005; Giesl
et al. 2006]. These processors are usually more powerful than those for ordinary rewriting. The
framework presented in [Giesl et al. 2005] even supports constructor rewriting.

ACM Transactions on Computational Logic, Vol. V, No. N, 20YY.

20

·

P. Schneider-Kamp, J. Giesl, A. Serebrenik, R. Thiemann

The transformation itself is trivial to automate and as shown in Section 4, existing
systems implementing the DP method can easily be adapted to prove termination
of infinitary constructor rewriting. The missing part in the automation is the generation of a suitable argument filter from the user input, cf. Task (I) at the end
of Section 4.1. After presenting the general algorithm to refine argument filters in
Section 5.1, we introduce suitable heuristics in Sections 5.2 and 5.3. Finally, we
extend the general algorithm for the refinement of argument filters by integrating
a mode analysis based on argument filters in Section 5.4. This allows us to handle
logic programs where a predicate is used with several different modes (i.e., where
different occurrences of the same predicate have different input and output positions). The usefulness of the different heuristics from Sections 5.2 and 5.3 and the
power of our extension in Section 5.4 will be evaluated empirically in Section 7.
5.1 Refinement Algorithm for Argument Filters
In our approach of Corollary 4.5, the user supplies an initial argument filter π to
describe the set of queries whose termination should be proved. There are two
issues with this approach. First, while argument filters provide the user with a
more expressive tool to characterize classes of queries, termination problems are
often rather posed in the form of a moding function for compatibility reasons.
Fortunately, it is straightforward to extract an appropriate initial argument filter
from such a moding function m: we define π(p) = {i | m(p, i) = in} for all p ∈ ∆
and π(f /n) = {1, . . . , n} for all function symbols f /n ∈ Σ.
Second, and less trivially, the variable condition V(π(r)) ⊆ V(π(ℓ)) for all rules
ℓ → r ∈ DP (RP ) ∪ RP does not necessarily hold for the argument filter π. Thus,
a refinement π ′ of π must be found such that the variable condition holds for π ′ .
Then, our method from Corollary 4.5 can be applied.
Unfortunately, there are often many refinements π ′ of a given filter π such that
the variable condition holds. The right choice of π ′ is crucial for the success of the
termination analysis. As already mentioned in Example 4.6, the argument filter
that simply filters away all arguments of all function symbols in the TRS, i.e., that
has π ′ (f ) = ∅ for all f ∈ ΣP , is a refinement of every argument filter π and it
obviously satisfies the variable condition. But of course, only termination of trivial
logic programs can be shown when using this refinement π ′ .
Example 5.1. We consider the logic program of Example 1.1. As shown in Example 3.2, the following rule results (among others) from the translation of the
logic program.
pin (f(X), g(Y )) → u1 (pin (f(X), f(Z)), X, Y )

(2)

Suppose that we want to prove termination of all queries p(t1 , t2 ) where both t1 and
t2 are (finite) ground terms. This corresponds to the moding m(p, 1) = m(p, 2) =
in, i.e., to the initial argument filter π with π(p) = {1, 2}.
In Corollary 4.5, we extend π to pin and Pin by defining it to be {1, 2} as well.
In order to prove termination, we now have to find a refinement π ′ of π such that
π ′ (DP (RP )) and π ′ (RP ) satisfy the variable condition and such that there is no
infinite (DP (RP ), RP , π ′ )-chain.
Let us first try to define π ′ = π. Then π ′ does not filter away any arguments.
ACM Transactions on Computational Logic, Vol. V, No. N, 20YY.

Automated Termination Proofs for Logic Programs by Term Rewriting

·

21

Thus, π ′ (pin ) = {1, 2}, π ′ (u1 ) = {1, 2, 3}, and π ′ (f) = π ′ (g) = {1}. But then
clearly, the variable condition does not hold as Z occurs in π ′ (r) but not in π ′ (ℓ) if
ℓ → r is Rule (2) above.
So we have to choose a different refinement π ′ . There remain three choices how
we can refine π to π ′ in order to filter away the variable Z in the right-hand side of
Rule (2): we can filter away the first argument of f by defining π ′ (f) = ∅, we can
filter away pin’s second argument by defining π(pin ) = {1}, or we can filter away
the first argument of u1 by defining π(u1 ) = {2, 3}.
The decision which of the three choices above should be taken must be done by a
suitable heuristic. The following definition gives a formalization for such heuristics.
Here we assume that the choice only depends on the term t containing a variable
that leads to a violation of the variable condition and on the position pos of the
variable. Then a refinement heuristic ρ is a function such that ρ(t, pos) returns a
function symbol f /n and an argument position i ∈ {1, . . . , n} such that filtering
away the i-th argument of f would erase the position pos in the term t. For
instance, if t is the right-hand side u1 (pin (f(X), f(Z)), X, Y ) of Rule (2) and pos is
the position of the variable Z in this term (i.e., pos = 121), then ρ(t, pos) can be
either (f, 1), (pin , 2), or (u1 , 1).
Definition 5.2 (Refinement Heuristic). A refinement heuristic is a mapping ρ :
T (ΣP , V) × N∗ → ΣP × N such that whenever ρ(t, pos) = (f, i), then there is a
position pos ′ with pos ′ i being a prefix of pos and root(t|pos ′ ) = f .
Given a TRS RP resulting from the transformation of a logic program P and a
refinement heuristic ρ, Algorithm 1 computes a refinement π ′ of a given argument
filter π such that the variable condition holds for DP (RP ) and RP .
Input: argument filter π, refinement heuristic ρ, TRS RP
Output: refined argument filter π ′ such that π ′ (DP (RP )) and π ′ (RP ) satisfy
the variable condition
1. π ′ := π
2. If there is a rule ℓ → r from DP (RP ) ∪ RP
and a position pos with r|pos ∈ V(π ′ (r)) \ V(π ′ (ℓ)), then:
2.1. Let (f, i) be the result of ρ(r, pos), i.e., (f, i) := ρ(r, pos).
2.2. Modify π ′ by removing i from π ′ (f ), i.e., π ′ (f ) := π ′ (f ) \ {i}.
For all other symbols from ΣP , π ′ remains unchanged.
2.3. Go back to Step 2.
Algorithm 1: General Refinement Algorithm
Termination of this algorithm is obvious as RP is finite and each change of the
argument filter in Step 2.2 reduces the number of unfiltered arguments. Note also
that ρ(r, pos) is always defined since pos is never the top position ε. The reason is
that the TRS RP is non-collapsing (i.e., it has no right-hand side consisting just of
ACM Transactions on Computational Logic, Vol. V, No. N, 20YY.

22

·

P. Schneider-Kamp, J. Giesl, A. Serebrenik, R. Thiemann

a variable). The algorithm is correct as it only terminates if the variable condition
holds for every dependency pair and every rule.
Note that if π ′ (F ) = π ′ (f ) for every defined function symbol f and if we do not
filter away the first argument position of the function symbols uc,i , i.e., 1 ∈ π ′ (uc,i ),
then the satisfaction of the variable condition for RP implies that the variable
condition for DP (RP ) holds as well. Thus, for heuristics that guarantee the above
properties, we only have to consider RP in the above algorithm.
5.2 Simple Refinement Heuristics
The following definition introduces two simple possible refinement heuristics. If a
term t has a position pos with a variable that violates the variable condition, then
these heuristics filter away the respective argument position of the innermost resp.
the outermost function symbol above the variable.
Definition 5.3 (Innermost/Outermost Refinement Heuristic). Let t be a term
and let “pos i” resp. “i pos” be a position in t. The innermost refinement heuristic
ρim is defined as follows:
ρim (t, pos i) = (root(t|pos ), i)
The outermost refinement heuristic ρom is defined as follows:
ρom (t, i pos) = (root(t), i)
So if t is again the term u1 (pin (f(X), f(Z)), X, Y ), then the innermost refinement
heuristic would result in ρim (t, 121) = (f, 1) and the outermost refinement heuristic
gives ρom (t, 121) = (u1 , 1).
Both heuristics defined above are simple but problematic, as shown in Example 5.4. Filtering the innermost function symbol often results in the removal of
an argument position that is relevant for termination of another rule. Filtering
the outermost function symbol excludes the possibility of filtering the arguments
of function symbols from the signature Σ of the original logic program. Moreover,
the outermost heuristic also often removes the first argument of some uc,i -symbol.
Afterwards, a successful termination proof is hardly possible anymore.
Example 5.4. Consider again the logic program of Example 1.1 which was transformed into the following TRS in Example 3.2.
pin (X, X) → pout (X, X)
pin (f(X), g(Y )) → u1 (pin (f(X), f(Z)), X, Y )

(1)
(2)

u1 (pout (f(X), f(Z)), X, Y ) → u2 (pin (Z, g(Y )), X, Y, Z)
u2 (pout (Z, g(Y )), X, Y, Z) → pout (f(X), g(Y ))

(3)
(4)

As shown in Example 4.2 we obtain the following dependency pairs for the above
rules.
Pin (f(X), g(Y )) → Pin (f(X), f(Z))
Pin (f(X), g(Y )) → U1 (pin (f(X), f(Z)), X, Y )

(5)
(6)

U1 (pout (f(X), f(Z)), X, Y ) → Pin (Z, g(Y ))
U1 (pout (f(X), f(Z)), X, Y ) → U2 (pin (Z, g(Y )), X, Y, Z)

(7)
(8)

ACM Transactions on Computational Logic, Vol. V, No. N, 20YY.

Automated Termination Proofs for Logic Programs by Term Rewriting

·

23

As in Example 5.1 we want to prove termination of p(t1 , t2 ) for all ground terms
t1 and t2 . Hence, we start with the argument filter π that does not filter away
any arguments, i.e., π(f /n) = {1, . . . , n} for all f ∈ ΣP . We will now illustrate
Algorithm 1 using our two heuristics.
Using the innermost refinement heuristic ρim in the algorithm, for the second
DP (6) we get ρim (U1 (pin (f(X), f(Z)), X, Y ), 121) = (f, 1). This requires us to
filter away the only argument of f, i.e., π ′ (f) = ∅. Now Z is contained in the
right-hand side of the third DP (7), but not in the filtered left-hand side anymore.
Thus, we now have to filter away the first argument of Pin , i.e., π ′ (Pin ) = {2}.
Due to the DP (6), we now also have to remove the second argument X of U1 , i.e.,
π ′ (U1 ) = {1, 3}. Consequently, we lose the information about finiteness of p’s first
argument and therefore cannot show termination of the program anymore. More
precisely, there is an infinite (DP (RP ), RP , π ′ )-chain consisting of the dependency
pairs (6) and (7) using a substitution that instantiates the variables X and Z by
the infinite term f(f(. . .)). This is indeed a chain since all infinite terms are filtered
away by the refined argument filter π ′ . Hence, the termination proof fails.
Using the outermost refinement heuristic ρom instead, for the second DP (6) we
get ρom (U1 (pin (f(X), f(Z)), X, Y ), 121) = (U1 , 1), i.e., π ′ (U1 ) = {2, 3}. Considering
the third DP (7) we have to filter away the first argument of Pin , i.e., π ′ (Pin ) = {2}.
Due to the DP (6), we now also have to remove the second argument of U1 , i.e.,
π ′ (U1 ) = {3}. So we obtain the same infinite chain as above since we lose the
information about finiteness of p’s first argument. Hence, we again cannot show
termination.
A slightly improved version of the outermost refinement heuristic can be achieved
by disallowing the filtering of the first arguments of the symbols uc,i and Uc,i .
Definition 5.5 (Improved Outermost Refinement Heuristic). Let t be a term and
pos be a position in t. The improved outermost refinement heuristic ρom′ is defined
as:
(
ρom′ (t|i , pos) if i = 1 and either root(t) = uc,i or root(t) = Uc,i
ρom′ (t, i pos) =
(root(t), i)
otherwise
Example 5.6. Reconsider Example 5.4. Using the improved outermost refinement heuristic, for the second rule (2) we get ρom′ (u1 (pin (f(X), f(Z)), X, Y ), 121) =
ρom′ (pin (f(X), f(Z)), 21) = (pin , 2) requiring us to filter away the second argument
of pin , i.e., π ′ (pin ) = {1}. Consequently, the algorithm filters away the third
arguments of both u1 and u2 , i.e., π ′ (u1 ) = {1, 2} and π ′ (u2 ) = {1, 2, 4}. Now
the variable condition holds for RP . Therefore, by defining π ′ (Pin ) = π ′ (pin ),
π ′ (u1 ) = π ′ (U1 ), and π ′ (u2 ) = π ′ (U2 ), the variable condition also holds for DP (RP ).
(As mentioned at the end of Section 5.1, by filtering tuple symbols F in the same
way as the original symbols f and by ensuring 1 ∈ π ′ (uc,i ), it suffices to check the
variable condition only for the rules RP and not for the dependency pairs DP (RP ).)
This argument filter corresponds to the one chosen in Example 4.6 and as shown
in Section 4.2 one can now easily prove termination.
ACM Transactions on Computational Logic, Vol. V, No. N, 20YY.

24

·

P. Schneider-Kamp, J. Giesl, A. Serebrenik, R. Thiemann

5.3 Type-Based Refinement Heuristic
The improved outermost heuristic from Section 5.2 only filters symbols of the form
pin , pout , Pin , and Pout . Therefore, the generated argument filters are similar to
modings. However, there are cases where one needs to filter function symbols from
the original logic program, too. In this section we show how to obtain a more
powerful refinement heuristic using information from inferred types.
There are many approaches to (direct) termination analysis of logic programs
that use type information in order to guess suitable “norms” or “ranking functions”,
e.g., [Bossi et al. 1992; Bruynooghe et al. 2007; Decorte et al. 1993; Martin et al.
1996]. In contrast to most of these approaches, we do not consider typed logic
programs, but untyped ones and we use types only as a basis for a heuristic to
prove termination of the transformed TRS. To our knowledge, this is the first time
that types are considered in the transformational approach to termination analysis
of logic programs.
Example 5.7. Now we regard the logic program from Example 1.3. The rules
after the transformation of Definition 3.1 are:
pin (X, X) → pout (X, X)

(1)

pin (f(X), g(Y )) → u1 (pin (f(X), f(Z)), X, Y )
u1 (pout (f(X), f(Z)), X, Y ) → u2 (pin (Z, g(W )), X, Y, Z)

(2)
(10)

u2 (pout (Z, g(W )), X, Y, Z) → pout (f(X), g(Y ))

(11)

Using the improved outermost refinement heuristic ρom′ we start off as in Example 5.6 and obtain π ′ (pin ) = {1}, π ′ (u1 ) = {1, 2}, and π ′ (u2 ) = {1, 2, 4}. However,
due to the last rule (11) we now get ρom′ (pout (f(X), g(Y )), 21) = (pout , 2), i.e.,
π ′ (pout ) = {1}. Considering the third rule (10), we have to filter pin once more and
obtain π ′ (pin ) = ∅. So we again lose the information about finiteness of p’s first
argument and cannot show termination. Similar to Example 5.4, the innermost
refinement heuristic which filters away the only argument of f also fails for this
program.
So in the example above, neither the innermost nor the (improved) outermost
refinement heuristic succeed. We therefore propose a better heuristic which is
like the innermost refinement heuristic, but which avoids the filtering of certain
arguments of original function symbols from the logic program. Close inspection
of the cases where filtering such function symbols is required reveals that it is not
advisable to filter away “reflexive” arguments. Here, we call an argument position i
of a function symbol f reflexive (or “recursive”), if the arguments on position i
have the same “type” as the whole term f (. . .) itself, cf. [Walther 1994]. A type
assignment associates a predicate p/n with an n-tuple of types for its arguments
and, similarly, a function f /n with an (n + 1)-tuple where the last element specifies
the result type of f .
Definition 5.8 (Types). Let Θ be a set of types (i.e., a set of names). A type
assignment τ over a signature (Σ, ∆) and a set of types Θ is a mapping τ : Σ ∪ ∆ →
Θ∗ such that τ (p/n) ∈ Θn for all p/n ∈ ∆ and τ (f /n) ∈ Θn+1 for all f /n ∈ Σ.
Let f /n ∈ Σ be a function symbol and τ be a type assignment with τ (f ) =
ACM Transactions on Computational Logic, Vol. V, No. N, 20YY.

Automated Termination Proofs for Logic Programs by Term Rewriting

·

25

(θ1 , . . . , θn , θn+1 ). Then the set of reflexive positions of f /n is Reflexive τ (f /n) =
{i | 1 ≤ i ≤ n and θi = θn+1 }.
To infer a suitable type assignment for a logic program, we use the following
simple algorithm. However, since we only use types as a heuristic to find suitable
argument filters, any other type assignment would also yield a correct method
for termination analysis. In other words, the choice of the type assignment only
influences the power of our method, not its soundness. So unlike [Bruynooghe
et al. 2007], the correctness of our approach does not depend on the logic program
or the query being well-typed. More sophisticated type inference algorithms were
presented in [Bruynooghe et al. 2005; Charatonik and Podelski 1998; Gallagher and
Puebla 2002; Janssens and Bruynooghe 1992; Lu 2000; Vaucheret and Bueno 2002],
for example.
In our simple type inference algorithm, we define ≃ as the reflexive and transitive closure of the following “similarity” relation on the argument positions: Two
argument positions of (possibly different) function or predicate symbols are “similar” if there exists a program clause such that the argument positions are occupied
by identical variables. Moreover, if a term f (. . .) occurs in the i-th position of a
function or predicate symbol p, then the argument position of f ’s result is similar
to the i-th argument position of p. (For a function symbol f /n we also consider
the argument position n + 1 which stands for the result of the function.) After
having computed the relation ≃, we then use a type assignment which corresponds
to the equivalence classes imposed by ≃. So our simple type inference algorithm is
related to sharing analysis [Bruynooghe et al. 1996; Cortesi and Filé 1999; Lagoon
and Stuckey 2002], i.e., the program analysis that aims at detecting program variables that in some program execution might be bound to terms having a common
variable.
Example 5.9. As an example, we compute a suitable type assignment for the
logic program from Example 1.3:
p(X, X).
p(f(X), g(Y )) :– p(f(X), f(Z)), p(Z, g(W )).
Let pi denote the i-th argument position of p, etc. Then due to the first clause
we obtain p1 ≃ p2 , since both argument positions are occupied by the variable X.
Moreover, since Z occurs both in the first argument positions of f and p in the
second clause, we also have p1 ≃ f1 . Finally, since an f-term occurs in the first
and second argument of p and since a g-term occurs in the second argument of p
we also have f2 ≃ p1 ≃ p2 and g2 ≃ p2 . In other words, the relation ≃ imposes
the two equivalence classes {p1 , p2 , f1 , f2 , g2 } and {g1 }. Hence, we compute a type
assignment with two types a and b where a and b correspond to {p1 , p2 , f1 , f2 , g2 }
and {g1 }, respectively. Thus, the type assignment is defined as τ (p) = τ (f) = (a, a)
and τ (g) = (b, a).
Note that the first argument of f has the same type a as its result and hence, this
argument position is reflexive. On the other hand, the first argument of g has a
different type than its result and is therefore not reflexive. Hence, Reflexive τ (f) =
{1} and Reflexive τ (g) = ∅.
Now we can define the following heuristic based on type assignments. It is like
ACM Transactions on Computational Logic, Vol. V, No. N, 20YY.

26

·

P. Schneider-Kamp, J. Giesl, A. Serebrenik, R. Thiemann

the innermost refinement heuristic of Definition 5.3, but now reflexive arguments
of function symbols from Σ (i.e., from the original logic program) are not filtered
away.
Definition 5.10 (Type-based Refinement Heuristic). Let t be a term, let “pos i”
be a position in t, and let τ be a type assignment. The type-based refinement
heuristic ρτtb is defined as follows:

(root(t|pos ), i) if root(t|pos ) ∈
/ Σ or i ∈
/ Reflexive τ (root(t|pos ))
τ
ρtb (t, pos i) =
ρτtb (t, pos)
otherwise
Note that the heuristic ρτtb never filters away the first argument of a symbol uc,i
or Uc,i from the TRSs DP (RP ) and RP . Therefore, as mentioned at the end of
Section 5.1, we only have to check the variable condition for the rules of RP , but
not for the dependency pairs.

Example 5.11. We continue with the logic program from Example 1.3 and use
the type assignment computed in Example 5.9 above. The rules after the transformation of Definition 3.1 are the following, cf. Example 5.7.
pin (X, X) → pout (X, X)
pin (f(X), g(Y )) → u1 (pin (f(X), f(Z)), X, Y )

(1)
(2)

u1 (pout (f(X), f(Z)), X, Y ) → u2 (pin (Z, g(W )), X, Y, Z)

(10)

u2 (pout (Z, g(W )), X, Y, Z) → pout (f(X), g(Y ))

(11)

Due to the occurrence of Z in the right-hand side of the second rule (2), we compute:
ρτtb (u1 (pin (f(X), f(Z)), X, Y ), 121)
= ρτtb (u1 (pin (f(X), f(Z)), X, Y ), 12) as f ∈ Σ and 1 ∈ Reflexive τ (f)
= (pin , 2)
as pin 6∈ Σ
Thus, we filter away the second argument of pin , i.e., π ′ (pin ) = {1}. Consequently,
we obtain π ′ (u1 ) = {1, 2} and π ′ (u2 ) = {1, 2, 4}.
Considering the fourth rule (11) we compute:
ρτtb (pout (f(X), g(Y )), 21)
= (g, 1)
as 1 6∈ Reflexive τ (g)
Thus, we filter away the only argument of g, i.e., π ′ (g) = ∅. By filtering the
tuple symbols in the same way as the corresponding “lower-case” symbols, now the
variable condition holds for RP and therefore also for DP (RP ). Indeed, this is
the argument filter chosen in Example 4.6. With this filter, one can easily prove
termination of the program, cf. Section 4.2.
For the above example, it is sufficient only to avoid the filtering of reflexive
positions. However, in general one should also avoid the filtering of all “unbounded”
argument positions. An argument position of type θ is “unbounded” if it may
contain subterms from a recursive data structure, i.e., if there exist infinitely many
terms of type θ. The decrease of the terms on such argument positions might be
the reason for the termination of the program and therefore, they should not be
filtered away. To formalize the concept of unbounded argument positions, we define
the set of constructors of a type θ to consist of all function symbols whose result
ACM Transactions on Computational Logic, Vol. V, No. N, 20YY.

Automated Termination Proofs for Logic Programs by Term Rewriting

·

27

has type θ. Then an argument position of a function symbol f is unbounded if it is
reflexive or if it has a type θ with a constructor that has an unbounded argument
position. For the sake of brevity, we also speak of just unbounded positions when
referring to unbounded argument positions.
Definition 5.12 (Unbounded Positions). Let θ ∈ Θ be a type and τ be a type assignment. A function symbol f /n with τ (f /n) = (θ1 , . . . , θn , θn+1 ) is a constructor
of θ iff θn+1 = θ. Let Constructors τ (θ) be the set of all constructors of θ.
For a function symbol f /n as above, we define the set of unbounded positions
as the smallest set such that Reflexive τ (f /n) ⊆ Unbounded τ (f /n) and such that
i ∈ Unbounded τ (f /n) if there is a g/m ∈ Constructorsτ (θi ) and a 1 ≤ j ≤ m with
j ∈ Unbounded τ (g/m).
In the logic program from Examples 1.3 and 5.9, we had τ (p) = τ (f) = (a, a) and
τ (g) = (b, a). Thus, Constructors τ (a) = {f, g} and Constructors τ (b) = ∅. Since
the first argument position of f is reflexive, it is also unbounded. The first argument
position of g is not unbounded, since it is not reflexive and there is no constructor
of type b with an unbounded argument position. So in this example, there is no
difference between reflexive and unbounded positions.
However, we will show in Example 5.14 that there are programs where these two
notions differ. For that reason, we now improve our type-based refinement heuristic
and disallow the filtering of unbounded (instead of just reflexive) positions.
Definition 5.13 (Improved Type-based Refinement Heuristic). Let t be a term,
let “pos i” be a position in t, and let τ be a type assignment. The improved typebased refinement heuristic ρτtb ′ is defined as follows:
ρτtb ′ (t, pos

i) =



(root(t|pos ), i) if root(t|pos ) ∈
/ Σ or i ∈
/ Unbounded τ (root(t|pos ))
otherwise
ρτtb ′ (t, pos)

Example 5.14. The following logic program inverts an integer represented by a
sign (neg or pos) and by a natural number in Peano notation (using s and 0). So
the integer number 1 is represented by the term pos(s(0)), the integer number −1
is represented by neg(s(0)), and the integer number 0 has the two representations
pos(0) and neg(0). Here nat(t) holds iff t represents a natural number (i.e., if t is a
term containing just s and 0) and inv simply exchanges the function symbols neg and
pos. The main predicate safeinv performs the desired inversion where safeinv(t1 , t2 )
only holds if t1 really represents an integer number and t2 is its inversion.
nat(0).
nat(s(X))
:– nat(X).
inv(neg(X), pos(X)).
inv(pos(X), neg(X)).
safeinv(X, neg(Y ))
:– inv(X, neg(Y )), nat(Y ).
safeinv(X, pos(Y ))
:– inv(X, pos(Y )), nat(Y ).
ACM Transactions on Computational Logic, Vol. V, No. N, 20YY.

28

·

P. Schneider-Kamp, J. Giesl, A. Serebrenik, R. Thiemann

The rules after the transformation of Definition 3.1 are:
natin (0) → natout (0)
natin (s(X)) → u1 (natin (X), X)
u1 (natout (X), X) → natout (s(X))
invin (neg(X), pos(X)) → invout (neg(X), pos(X))
invin (pos(X), neg(X)) → invout (pos(X), neg(X))

(12)
(13)
(14)
(15)
(16)

safeinvin (X, neg(Y )) → u2 (invin (X, neg(Y )), X, Y )
u2 (invout (X, neg(Y )), X, Y ) → u3 (natin (Y ), X, Y )

(17)
(18)

u3 (natout (Y ), X, Y ) → safeinvout (X, neg(Y ))
safeinvin (X, pos(Y )) → u4 (invin (X, pos(Y )), X, Y )

(19)
(20)

u4 (invout (X, pos(Y )), X, Y ) → u5 (natin (Y ), X, Y )
u5 (natout (Y ), X, Y ) → safeinvout (X, pos(Y ))

(21)
(22)

Let us assume that the user wants to prove termination of all queries safeinv(t1 , t2 )
where t1 is ground. So we use the moding m(safeinv, 1) = in and m(safeinv, 2) =
out. Thus, as initial argument filter π we have π(safeinv) = {1} and hence
π(safeinvin ) = π(SAFEINV in ) = {1}, while π(f /n) = {1, . . . , n} for all f ∈
/ {safeinv,
safeinvin , SAFEINVin }. In Rule (17) one has to filter away the second argument of
invin or the only argument of neg in order to remove the “extra” variable Y on the
right-hand side. From a type inference for these rules we obtain the type assignment
τ with τ (s) = (b, b), τ (0) = (b), and τ (neg) = τ (pos) = (b, a). So “a” corresponds to
the type of integers and “b” corresponds to the type of naturals. The constructors
of the naturals are Constructors τ (b) = {s, 0}. This is a recursive data structure
since s has an unbounded argument: 1 ∈ Reflexive τ (s) ⊆ Unbounded τ (s). Thus,
while neg’s first argument position of type b is not reflexive, it is still unbounded,
i.e., 1 ∈ Unbounded τ (neg). Hence, our improved type-based heuristic decides to
filter away the second argument of invin (as invin is not from the original signature
Σ). Now termination is easy to show.
If one had considered the original type-based heuristic instead, then the nonreflexive first argument of neg would be filtered away. Due to Rule (17), then also
the last argument of u2 has to be removed by the filter. But then the variable Y
would not occur anymore in the filtered left-hand side of Rule (18). So to satisfy
the variable condition for Rule (18), we would have to filter away the only argument
of natin . Similarly, the only argument of the corresponding tuple symbol NATin
would also be filtered away, blocking any possibility for a successful termination
proof.
5.4 Mode Analysis based on Argument Filters and an Improved Refinement Algorithm
In logic programming, it is not unusual that a predicate is used with different modes
(i.e., that different occurrences of the predicate have different input and output
positions). Uniqueness of moding can then be achieved by creating appropriate
copies of these predicate symbols and their clauses for every different moding.
ACM Transactions on Computational Logic, Vol. V, No. N, 20YY.

Automated Termination Proofs for Logic Programs by Term Rewriting

·

29

Example 5.15. Consider the following logic program for rotating a list taken
from [Codish 2007]. Let P be the append-program consisting of the clauses from
Example 1.4 and the new clause
rotate(N , O ) :– append(L, M , N ), append(M , L, O ).

(23)

with the moding m(rotate, 1) = in and m(rotate, 2) = out. For this moding, the
program is terminating.
But while the first use of append in Clause (23) supplies it with a ground term
only on the last argument position, the second use in (23) is with ground terms
only on the first two argument positions. Although the append-clauses are even
well moded for both kinds of uses, the whole program is not.
The logic program is transformed into the following TRS. As before, “[X|L]” is
an abbreviation for •(X, L), i.e., • is the constructor for list insertion.
appendin ([ ], M, M ) → appendout ([ ], M, M )

(24)

appendin (•(X, L), M, •(X, N )) → u1 (appendin (L, M, N ), X, L, M, N ) (25)
u1 (appendout (L, M, N ), X, L, M, N ) → appendout (•(X, L), M, •(X, N ))
(26)
rotatein (N, O) → u2 (appendin (L, M, N ), N, O)
u2 (appendout (L, M, N ), N, O) → u3 (appendin (M, L, O), L, M, N, O)
u3 (appendout (M, L, O), L, M, N, O) → rotateout (N, O)

(27)
(28)
(29)

Due to the “extra” variables L and M in the right-hand side of Rule (27) and the
“extra” variable O in the right-hand side of Rule (28),11 the only refined argument
filter which would satisfy the variable condition of Corollary 4.5 is the one where
π(appendin ) = ∅.12 As we can expect, for the queries described by this filter, the
append-program is not terminating and, thus, our new approach fails, too.
The common solution [Apt 1997] is to produce two copies of the append-clauses
and to rename them apart. This is often referred to as “mode-splitting”. First, we
create labelled copies of the predicate symbol append and label the predicate of each
append-atom by the input positions of the moding in which it is used. Then, we
extend our moding to m(append{3} , 3) = m(append{1,2} , 1) = m(append{1,2} , 2) =
in and m(append{3} , 1) = m(append{3} , 2) = m(append{1,2} , 3) = out. In our
example, termination of the resulting logic program can easily be shown using both
the classical transformation from Section 1.1 or our new transformation:
rotate(N , O )
:– append{3} (L, M , N ), append{1,2} (M , L, O ).
{3}
append ([ ], M , M ).
append{3} ([X|L], M , [X|N ]) :– append{3} (L, M , N ).
append{1,2} ([ ], M , M ).
append{1,2} ([X|L], L, [X|N ]) :– append{1,2} (L, M , N ).
11 In the left-hand side of Rule (27), the variable O in the second argument of rotate
in is removed
by the initial filter that describes the desired set of queries given by the user. Consequently, one
also has to filter away the last argument of u2 . Hence, then O is indeed an “extra” variable in the
right-hand side of Rule (28).
12 Alternatively, one could also filter away the first arguments of u and u . But then one
2
3
would also have to satisfy the variable condition for the dependency pairs and one would obtain π(APPENDin ) = ∅. Hence, the termination proof attempt would fail as well.

ACM Transactions on Computational Logic, Vol. V, No. N, 20YY.

30

·

P. Schneider-Kamp, J. Giesl, A. Serebrenik, R. Thiemann

In the example above, a pre-processing based on modings was sufficient for a successful termination proof. In general, though, this is insufficient to handle queries
described by an argument filter. The following example demonstrates this.
Example 5.16. Consider again the logic program P from Example 5.15 which
is translated to the TRS RP = {(24), . . . , (29)}. This time we want to show termination for all queries of the form rotate(t1 , t2 ) where t1 is a finite list (possibly
containing non-ground terms as elements). So t1 is instantiated by terms of the form
•(r1 , •(r2 , . . . •(rn , [ ]) . . .)) where the ri can be arbitrary terms possibly containing
variables.13
To specify these queries, the user would provide the initial argument filter π
with π(rotate) = {1} and π(•) = {2}. Now our aim is to prove termination of all
queries that are ground under the filter π. Thus, the first argument of rotate is not
necessarily a ground term (it is only guaranteed to be ground after filtering away
the second argument of •).
Therefore, if one wanted to pre-process the program using modings, then one
could not assume that the first argument of rotate were ground. Instead, one would
have to use the moding m(rotate, 1) = m(rotate, 2) = out. Therefore, in the calls to
append, all argument positions would be considered as “out”. As a consequence, no
renamed-apart copies of clauses would be created and the termination proof would
fail.
In general, our refinement algorithm from Section 5.1 (Algorithm 1) aims to
compute an argument filter that filters away as few arguments as possible while
ensuring that the variable condition holds. In this way we make sure that the
maximal amount of information remains for the following termination analysis.
But as Examples 5.15 and 5.16 above demonstrate, there are cases where we need
to create renamed-apart copies of clauses for certain predicates in order to obtain
a viable refined argument filter. To this end, a first idea might be to combine an
existing mode inference algorithm with Algorithm 1. However, it is not clear how
to do such a combination. The problem is that we already need to know the refined
argument filter in order to create suitable copies of clauses. At the same time, we
already need the renamed-apart copies of the clauses in order to compute the refined
argument filter. Thus, we have a classical “chicken-and-egg” problem. Moreover,
such an approach would always fail for programs like Example 5.16 where there
exists no suitable pre-processing based on modings.
Therefore, we replace Algorithm 1 by the following new Algorithm 2 that simultaneously refines the argument filter and creates renamed-apart copies on demand.
The idea of the algorithm is the following. Whenever our refinement heuristic
suggests to filter away an argument of a symbol pin , then instead of changing the
13 Such

a termination problem can also result from an initial termination problem that was described by modings. To demonstrate this, we could extend the program by the following clauses.
p(X, O)
:– s2ℓ(X, N ), rotate(N, O).
s2ℓ(0, [ ]).
s2ℓ(s(X), [Y |N ]) :– s2ℓ(X, N ).

To prove termination of all queries described by the moding m(p, 1) = in and m(p, 2) = out, one
essentially has to show termination for all queries of the form rotate(t1 , t2 ) where t1 is a finite list.
ACM Transactions on Computational Logic, Vol. V, No. N, 20YY.

Automated Termination Proofs for Logic Programs by Term Rewriting

·

31

Input: argument filter π, refinement heuristic ρ, TRS RP
Output: refined argument filter π ′ and modified TRS R′P
such that π ′ (R′P ) satisfies the variable condition
′
1. RP := RP ∪ {ℓπ(p) → rπ(p) | ℓ → r ∈ RP (p), p/n ∈ ∆, π(p) ( {1, . . . , n}}

for all f ∈ Σ (i.e., for functions of P)
 π(f ),
2. π ′ (f ) := I,
for all f = pIin with p ∈ ∆

{1, . . . , n}, for all other symbols f /n
3. If there is a rule ℓ → r from R′P
and a position pos with r|pos ∈ V(π ′ (r)) \ V(π ′ (ℓ)), then:

3.1. Let (f, i) be the result of ρ(r, pos), i.e., (f, i) := ρ(r, pos).
3.2. We perform a case analysis depending on whether f has the form
pIin for some p ∈ ∆. Here, unlabelled symbols of the form pin /n
are treated as if they were labelled with I = {1, . . . , n}.
• If f = pIin , then we must have r = u(pIin (...), . . .) for some
I\{i}
with
symbol u. We introduce a new function symbol pin
I\{i}
′
π (pin ) = I \ {i} if it has not yet been introduced. Then:
I\{i}

◦ We replace pIin by pin
R′P

:=

I\{i}

where r = u(pin

R′P

in the right-hand side of ℓ → r:
\ {ℓ → r} ∪ {ℓ → r},

(...), . . .).

◦ R′P := R′P ∪ {sI\{i} → tI\{i} | s → t ∈ R′P (p)}.
If this introduces new labelled function symbols f /n where
π ′ was not yet defined on, we define π ′ (f ) = {1, . . . , n}.
◦ Let ℓ′ → r′ be the rule in R′P with ℓ′ = u(pIout (...), . . .). We
I\{i}
now replace pIout by pout in the left-hand side of ℓ′ → r′ :
R′P := R′P \ {ℓ′ → r′ } ∪ {ℓ′ → r′ },
I\{i}

where ℓ′ = u(pout (...), . . .).
• Otherwise (i.e., if f does not have the form pin or pIin ), then
modify π ′ by removing i from π ′ (f ), i.e., π ′ (f ) := π ′ (f ) \ {i}.
3.3. Go back to Step 3.
Algorithm 2: Improved Refinement Algorithm

argument filter appropriately, we introduce a new copy of the symbol pin . To
distinguish the different copies of the symbols pin , we label them by the argument
positions that are not filtered away.
In general, a removal of argument positions of pin can already be performed
by the initial filter π that the user provides in order to describe the desired set
of queries. Therefore, if π(p) does not contain all arguments {1, . . . , n} for some
ACM Transactions on Computational Logic, Vol. V, No. N, 20YY.

32

·

P. Schneider-Kamp, J. Giesl, A. Serebrenik, R. Thiemann
π(p)

predicate symbol p/n, then we already introduce a new symbol pin and new copies
π(p)
of the rewrite rules originating from p. In these rules, we use the new symbol pin
instead of pin .
Let us reconsider Example 5.16. To prove termination of all queries rotate(t1 , t2 )
with a finite list t1 , the user would select the argument filter π that eliminates the
second argument of rotate and the first argument of the list constructor •. So we
have π(rotate) = {1}, π(•) = {2}, and π(append) = {1, 2, 3}. Then in addition to
{1}
the rules (27) - (29) for the symbol rotatein we also introduce the symbol rotatein .
{1}
Moreover, in order to ensure that rotatein does the same computation as rotatein ,
we add the following copies of the rewrite rules (27) - (29) originating from the
predicate rotate. Here, all root symbols of left- and right-hand sides are labelled
with {1}.
{1}

{1}

rotatein (N, O) → u2 (appendin (L, M, N ), N, O)
{1}

(30)

{1}

u2 (appendout (L, M, N ), N, O) → u3 (appendin (M, L, O), L, M, N, O) (31)
{1}

{1}

u3 (appendout (M, L, O), L, M, N, O) → rotateout (N, O)

(32)

So in Step 1 of the algorithm, we initialize R′P to contain all rules of RP . But
in addition, R′P contains labelled copies of the rules resulting from those predicates
p/n where π(p) ( {1, . . . , n}. In these rules, the root symbols of left- and right-hand
sides are labelled with π(p).
Formally, for every predicate symbol p ∈ ∆, let RP (p) denote those rules of RP
which result from p-clauses (i.e., from clauses whose head is built with the predicate
p). So RP (rotate) consists of the rule for rotatein and the rules for u2 and u3 , i.e.,
RP (rotate) = {(27), (28), (29)}.
Then for a term t = f (t1 , . . . , tn ) and a set of argument positions I ⊆ N, let
tI denote f I (t1 , . . . , tn ). So for t = rotatein (N, O) and I = {1}, we have tI =
{1}
rotatein (N, O). Hence if π(rotate) = {1}, then we extend R′P by copies of the
rules in RP (rotate) where the root symbols are labelled by {1}. In other words, we
have to add the rules {ℓπ(p) → rπ(p) | ℓ → r ∈ RP (rotate)} = {(30), (31), (32)}.
In Step 2, we initialize our desired argument filter π ′ . This filter does not yet
eliminate any arguments except for original function symbols from the logic program
and for symbols of the form pIin . Since in our example, the initial argument filter π
{1}
of the user is π(rotate) = {1}, we have π ′ (rotatein ) = {1, 2}, but π ′ (rotatein ) = {1}.
I
So for symbols pin , the label I describes those arguments that are not filtered away.
However, this does not hold for the other labelled symbols. So the labelling of the
{1}
{1}
{1}
symbols u2 , u3 , and appendout only represents that they “belong” to the symbol
{1}
rotatein . But the argument filter for these symbols can be determined arbitrarily.
{1}
Initially, π ′ would not filter away any of their arguments, i.e., π ′ (u2 ) = {1, 2, 3},
{1}
{1}
π ′ (u3 ) = {1, 2, 3, 4, 5}, and π ′ (rotateout ) = {1, 2}. The filter for original function
symbols of the logic program is taken from the user-defined argument filter π. So
since the user described the desired set of queries by setting π(•) = {2}, we also
have π ′ (•) = {2}.
In Steps 3 and 3.1, we look for rules violating the variable condition as in
Algorithm 1. Again, we use a refinement heuristic ρ to suggest a suitable function
ACM Transactions on Computational Logic, Vol. V, No. N, 20YY.

Automated Termination Proofs for Logic Programs by Term Rewriting

·

33

symbol f and an argument position i that should be filtered away. As before, we
restrict ourselves to refinement heuristics ρ which never select the first argument
of a symbol uc,i . In this way, we only have to examine the rules (and not also the
dependency pairs) for possible violations of the variable condition.
If f is not a (possibly labelled) symbol of the form pin or pIin , then we proceed
in Step 3.2 as before (i.e., as in Step 2.2 of Algorithm 1). But if f is a (possibly
labelled) symbol of the form pin or pIin , then we do not modify the filter for f . If
I are the non-filtered argument positions of f , then we introduce a new function
symbol labelled with I \ {i} instead and replace f by this new function symbol in
the rule that violated the variable condition.
In our example, we had R′P = {(24), . . . , (29), (30), (31), (32)} and π ′ was the
{1}
filter that does not eliminate any arguments except for π ′ (rotatein ) = {1} and
′
π (•) = {2}.
The rules (25), (27), and (30) violate the variable condition. In the following, we
mark the violating variables by boxes. Let us regard Rule (25) first:
appendin (•(X, L), M, •(X, N )) → u1 (appendin (L, M, N ), X , L, M, N )

(25)

To remove the variable X from the right-hand side, in Step 3.1 any refinement
heuristic must suggest to filter away the second argument of u1 . As u1 does not
have the form pIin , we use the second case of Step 3.2. Thus, we change π ′ such
that π ′ (u1 ) = {1, 2, 3, 4, 5}\{2} = {1, 3, 4, 5}. Indeed, now this rule does not violate
the variable condition anymore.
We reach Step 3.3 and, thus, go back to Step 3 where we again choose a rule
that violates the variable condition. Let us now regard Rule (30):
{1}

{1}

rotatein (N, O) → u2 (appendin ( L , M , N ), N, O )

(30)

To remove the first violating variable L, in Step 3.1 our refinement heuristic suggests to filter away the first argument of the symbol appendin . But instead of chang{2,3}
{2,3}
with π ′ (appendin ) =
ing π ′ (appendin ), we introduce a new symbol appendin
{2, 3}. Moreover, we replace the symbol appendin in the right-hand side of Rule
{2,3}
(30) by the new symbol appendin . Thus, Rule (30) is modified to
{1}

{1}

{2,3}

rotatein (N, O) → u2 (appendin

(L, M , N ), N, O ).

(33)

{2,3}

has rewrite rules corresponding to the rules of
To make sure that appendin
appendin , we now have to add copies of all rules that result from the appendpredicate. However, here we label every root symbol by {2, 3}. In other words, we
have to add the following rules to R′P :
{2,3}

appendin

{2,3}

([ ], M, M ) → appendout ([ ], M, M )

{2,3}
appendin (•(X, L), M, •(X, N ))
{2,3}
(appendout (L, M, N ), X, L, M, N )
u1

(34)

→

{2,3}
u1
(appendin (L, M, N ), X, L, M, N )

(35)

→

{2,3}
appendout (•(X, L), M, •(X, N ))

(36)

{2,3}

Now the result of rewriting a term appendin (. . .) will always be a term of the
{2,3}
{2,3}
form appendout (. . .). Therefore, we have to replace appendout by appendout in
the left-hand side of Rule (31) (since (31) is the rule that always “follows” (30)).
ACM Transactions on Computational Logic, Vol. V, No. N, 20YY.

34

·

P. Schneider-Kamp, J. Giesl, A. Serebrenik, R. Thiemann

So the original rule (31)
{1}

{1}

u2 (appendout (L, M, N ), N, O) → u3 (appendin (M, L, O), L, M, N, O)

(31)

is replaced by the modified rule
{1}

{2,3}

{1}

u2 (appendout (L, M, N ), N, O) → u3 (appendin (M, L, O), L, M, N, O).

(37)

R′P

Thus, after the execution of Step 3.2, we have
= {(24) − (29), (33) − (36), (37),
{2,3}
(32)}. In this way, we have introduced three new labelled symbols appendin ,
{2,3}
{2,3}
u1 , and appendout . On the unlabelled symbols, the argument filter π ′ did
{2,3}
{2,3}
) =
not change, but we now additionally have π ′ (appendin ) = {2, 3}, π ′ (u1
{2,3}
{1, 2, 3, 4, 5}, and π ′ (appendout ) = {1, 2, 3}.
We reach Step 3.3 and, thus, go back to Step 3 where we again choose a rule that
violates the variable condition. Let us again regard Rule (30), albeit in its modified
form as Rule (33). The variable M still violates the variable condition. In Step 3.1,
the refinement heuristic suggests to filter away the second argument of the symbol
{2,3}
appendin . Instead of changing π ′ , we again introduce a new symbol, namely
{2,3}
{3}
{3}
in the
appendin with π ′ (appendin ) = {3}, and replace the symbol appendin
{3}
right-hand side of Rule (33) by appendin . Thus, we obtain a further modification
of Rule (33):
{1}

{1}

{3}

rotatein (N, O) → u2 (appendin (L, M, N ), N, O )

(38)

{3}

Again, we have to ensure that appendin has rewrite rules corresponding to the rules
of appendin . Thus, we add copies of all rules that result from the append-predicate
where every root symbol is labelled by {3}:
{3}

{3}

appendin ([ ], M, M ) → appendout ([ ], M, M )
{3}
appendin (•(X, L), M, •(X, N ))

→

{3}
u1 (appendout (L, M, N ), X, L, M, N )

→

{3}
u1 (appendin (L, M, N ), X, L, M, N )
{3}
appendout (•(X, L), M, •(X, N ))

{2,3}

(39)
(40)
(41)

{3}

We also have to replace appendout by appendout in the left-hand side of Rule (37)
(since (37) is the rule that always “follows” (33)). So the rule (37) is replaced by
the modified rule
{1}

{3}

{1}

u2 (appendout (L, M, N ), N, O) → u3 (appendin (M, L, O), L, M, N, O)

(42)

Thus, after the execution of Step 3.2, we have R′P = {(24)−(29), (38)−(41), (34)−
{3}
(36), (42), (32)}. Again we have introduced three new labelled symbols appendin ,
{3}
{3}
u1 , and appendout . On the unlabelled symbols, the argument filter π ′ did not
{3}
{3}
change, but we now additionally have π ′ (appendin ) = {3}, π ′ (u1 ) = {1, 2, 3, 4, 5},
{3}
and π ′ (appendout ) = {1, 2, 3}.
We reach Step 3.3 and, thus, go back to Step 3 where we again choose a
rule that violates the variable condition. We again regard Rule (30), albeit in its
modified form as Rule (38). The variable O still violates the variable condition. In
Step 3.1, any refinement heuristic must suggest to filter away the third argument
ACM Transactions on Computational Logic, Vol. V, No. N, 20YY.

Automated Termination Proofs for Logic Programs by Term Rewriting
{1}

·

35

{1}

of the symbol u2 . As u2 does not have the form pIin , we use the second case of
{1}
Step 3.2. Thus, we change π ′ such that π ′ (u2 ) = {1, 2, 3} \ {3} = {1, 2}. Indeed,
now Rule (38) does not violate the variable condition anymore.
We reach Step 3.3 and, thus, go back to Step 3 where we again choose a rule
that still violates the variable condition. Let us now regard Rule (42):
{1}

{3}

{1}

u2 (appendout (L, M, N ), N, O) → u3 (appendin (M, L, O ), L, M, N, O ) (42)
Here our refinement heuristic suggests to filter away the third argument of the
symbol appendin in order to remove the extra variable O. Instead of changing π ′ , we
{1,2}
{1,2}
with π ′ (appendin ) = {1, 2},
again introduce a new symbol, namely appendin
{1,2}
and replace the symbol appendin in the right-hand side of Rule (42) by appendin .
Thus, we obtain a further modification of Rule (42):
{1}

{3}

{1}

{1,2}

u2 (appendout (L, M, N ), N, O) → u3 (appendin

(M, L, O), L, M, N, O ) (43)

{1,2}

has rewrite rules corresponding to the
Again, we have to ensure that appendin
rules of appendin . Thus, we add copies of all rules that result from the appendpredicate where every root symbol is labelled by {1, 2}:
{1,2}

appendin

{1,2}

([ ], M, M ) → appendout ([ ], M, M )

{1,2}
appendin (•(X, L), M, •(X, N ))
{1,2}
(appendout (L, M, N ), X, L, M, N )
u1

(44)

→

{1,2}
(appendin (L, M, N ), X, L, M, N )
u1

(45)

→

{1,2}
appendout (•(X, L), M, •(X, N ))

(46)

{1,2}

We also have to replace appendout by appendout in the left-hand side of Rule
(32) (since (32) is the rule that always “follows” (42)). So the rule (32) is replaced
by the modified rule
{1}

{1,2}

{1}

u3 (appendout (M, L, O), L, M, N, O) → rotateout (N, O)

(47)

Thus, after the execution of Step 3.2, we now have R′P = {(24) − (29), (38) −
(41), (34) − (36), (43) − (46), (47)}. Again we have introduced three new labelled
{1,2}
{1,2} {1,2}
symbols appendin , u1 , and appendout . On the unlabelled symbols, the argu{1,2}
ment filter π ′ did not change, but we now additionally have π ′ (appendin ) = {1, 2},
{1,2}
{1,2}
π ′ (u1
) = {1, 2, 3, 4, 5}, and π ′ (appendout ) = {1, 2, 3}.
Note that now we have indeed separated the two copies of the append-rules where
{3}
appendin corresponds to the version of append that has the third argument as input
{1,2}
and appendin is the version where the first two arguments serve as input. This
copying of predicates works although the initial argument filter already filtered
away arguments of function symbols like “•” (i.e., the initial argument filter was
already beyond the expressivity of modings).
Step 3 is repeated until the variable condition is not violated anymore. Note that
Algorithm 2 always terminates since there are only finitely many possible labelled
variants for every symbol. In our example, we obtain the following set of rules R′P :
ACM Transactions on Computational Logic, Vol. V, No. N, 20YY.

36

·

P. Schneider-Kamp, J. Giesl, A. Serebrenik, R. Thiemann

appendin ([ ], M, M ) → appendout ([ ], M, M )

(24)

appendin (•(X, L), M, •(X, N )) → u1 (appendin (L, M, N ), X, L, M, N )
u1 (append out (L, M, N ), X, L, M, N ) → appendout (•(X, L), M, •(X, N ))
rotatein (N, O) →
{3}
u2 (appendout (L, M, N ), N, O)

{3}
u2 (appendin (L, M, N ), N, O)

→ u3 (appendin (M, L, O), L, M, N, O)

(25)
(26)
(48)
(49)

u3 (appendout (M, L, O), L, M, N, O) → rotateout (N, O)

(29)

{1}
rotatein (N, O)

→

(38)

{1}
{3}
u2 (appendout (L, M, N ), N, O)
{1}
{1,2}
u3 (append out (M, L, O), L, M, N, O)

→
→

{1}
{3}
u2 (append in (L, M, N ), N, O)
{1}
{1,2}
u3 (append in (M, L, O), L, M, N, O)
{1}
rotateout (N, O)

→

{2,3}
appendout ([ ], M, M )

(34)

→

{2,3}
{2,3}
u1
(appendin (L, M, N ), X, L, M, N )

(50)

→

{2,3}
appendout (•(X, L), M, •(X, N ))

(51)

→

{3}
appendout ([ ], M, M )

(39)

→

{3}
{3}
u1 (append in (L, M, N ), X, L, M, N )
{3}
appendout (•(X, L), M, •(X, N ))

(52)

{2,3}
appendin ([ ], M, M )
{2,3}
appendin (•(X, L), M, •(X, N ))
{2,3}
{2,3}
u1
(appendout (L, M, N ), X, L, M, N )
{3}
appendin ([ ], M, M )
{3}
appendin (•(X, L), M, •(X, N ))
{3}
{3}
u1 (append out (L, M, N ), X, L, M, N )
{1,2}

appendin

→

{1,2}

([ ], M, M ) → appendout ([ ], M, M )

{1,2}
appendin (•(X, L), M, •(X, N ))
{1,2}
{1,2}
(appendout (L, M, N ), X, L, M, N )
u1

→
→

(43)
(47)

(53)
(44)

{1,2}
{1,2}
u1
(appendin (L, M, N ), X, L, M, N )
{1,2}
appendout (•(X, L), M, •(X, N ))

(54)
(55)

The refined argument filter π ′ is given by
π ′ (appendin ) = {1, 2, 3}
π ′ (appendout ) = {1, 2, 3}
π ′ (•)
= {2}
π ′ (u1 )
= {1, 3, 4, 5}
π ′ (rotatein ) = {1, 2}
π ′ (u2 )
= {1, 2, 3}
{3}
π ′ (appendin ) = {3}
{3}
π ′ (appendout ) = {1, 2, 3}
′
π (u3 )
= {1, 2, 3, 4, 5}
π ′ (rotateout ) = {1, 2}

{1}

π ′ (rotatein )
= {1}
{1}
π ′ (u2 )
= {1, 2}
{1}
π ′ (u3 )
= {1, 2, 3, 4}
{1,2}
π ′ (appendin ) = {1, 2}
{1,2}
π ′ (appendout ) = {1, 2, 3}
{1}
′
π (rotateout )
= {1, 2}

{2,3}

π ′ (appendin ) = {2, 3}
{2,3}
π ′ (appendout ) = {1, 2, 3}
{2,3}
π ′ (u1
)
= {1, 4, 5}
{3}
= {1, 5}
π ′ (u1 )
{1,2}
π ′ (u1
)
= {1, 3, 4}

Termination for R′P w.r.t. the terms specified by π ′ is now easy to show using
our results from Section 4.
If one is only interested in termination of queries rotate(t1 , t2 ) for a specific predicate symbol like rotate, then one can remove superfluous (copies of) rules from the
TRS before starting the termination proof. For example, if one only wants to prove
termination of queries rotate(t1 , t2 ) for finite lists t1 , then it now suffices to prove
{1}
termination of the above TRS for those “start terms” rotatein (. . .) that are finite
{1}
and ground under the filter π ′ and where the arguments of rotatein do not contain
any function symbols except • and [ ]. Since the rules for rotatein , appendin , and
ACM Transactions on Computational Logic, Vol. V, No. N, 20YY.

Automated Termination Proofs for Logic Programs by Term Rewriting

·

37

{2,3}

appendin (i.e., the rules (24) - (26), (29), (34), and (48) - (51)) are not reachable
from these “start terms”, they can immediately be removed. In other words, for the
{3}
{1,2}
{1}
queries rotate(t1 , t2 ) we indeed need rules for rotatein , appendin , and appendin ,
{2,3}
but the rules for rotatein , appendin , and appendin are superfluous.
Note however that such superfluous copies of rules are never problematic for
{3}
the termination analysis. If the rules for appendin are terminating for terms that
{2,3}
are finite and ground under the filter π ′ , then this also holds for the appendin ′
and the appendin -rules, since here π filters away less arguments. A corresponding
{1}
statement holds for the connection between the rotatein - and the rotatein -rules.
The following theorem proves the correctness of Algorithm 2. More precisely,
it shows that one can use π ′ and R′P instead of π and RP in Theorem 3.7. So
π(p)
it is sufficient to prove that all terms in the set S ′ = {pin (~t) | p ∈ ∆, ~t ∈
π(p)
T~ ∞ (Σ, V), π ′ (pin (~t)) ∈ T (ΣPπ′ ) } are terminating w.r.t. the modified TRS R′P .
{1}
In Example 5.16, S ′ would be the set of all terms rotatein (t1 , t2 ) that are ground
after filtering with π ′ . Hence, this includes all terms where the first argument is a
finite list.
If all terms in S ′ are terminating w.r.t. R′P , we can conclude that all queries
Q ∈ Arat (Σ, ∆, V) with π(Q) ∈ A(Σπ , ∆π ) are terminating for the original logic
program. Since π ′ satisfies the variable condition for the TRS R′P (and also for
DP (R′P ) if 1 ∈ π ′ (uc,i ) for all symbols of the form uc,i ), one can also use π ′ and R′P
for the termination criterion of Corollary 4.5. In other words, then it is sufficient
to prove that there is no infinite (DP (R′P ), R′P , π ′ )-chain.
Theorem 5.17 (Soundness of Algorithm 2). Let P be a logic program and
let π be an argument filter over (Σ, ∆). Let π ′ and R′P result from π and RP by
Algorithm 2. Let S = {pin (~t) | p ∈ ∆, ~t ∈ T~ ∞ (Σ, V), π(pin (~t)) ∈ T (ΣPπ ) }.
π(p)
π(p)
Furthermore, let S ′ = {pin (~t) | p ∈ ∆, ~t ∈ T~ ∞ (Σ, V), π ′ (pin (~t)) ∈ T (ΣPπ′ ) }.
All terms s ∈ S are terminating for RP if all terms s′ ∈ S ′ are terminating for
R′P .
Proof. We first show that every reduction of a term from S with RP can
be simulated by the reduction of a term from S ′ with R′P . More precisely, we
show the following proposition where Sn = {t | pin (~t) →nRP t for some p ∈ ∆,
∗
~
~t ∈ T~ ∞ (Σ, V), and π(pin (~t)) ∈ T (ΣPπ ) } and S′ = {t | pπ(p)
in (t) → ′ t for some
RP

π(p)
p ∈ ∆, ~t ∈ T~ ∞ (Σ, V), and π ′ (pin (~t)) ∈ T (ΣPπ′ ) }

If s ∈ Sn and s′ ∈ S′ with Unlab(s′ ) = s, then s →RP t implies
that there is a t′ with Unlab(t′ ) = t and s′ →R′P t′ .

(56)

Here, Unlab removes all labels introduced by Algorithm 2:
(
f (Unlab(s1 ), . . . , Unlab(sn )), if s = f I (s1 , . . . , sn )
Unlab(s) =
s,
otherwise
We prove (56) by induction on n. There are three possible cases for s and for
the rule that is applied in the step from s to t.
ACM Transactions on Computational Logic, Vol. V, No. N, 20YY.

38

·

P. Schneider-Kamp, J. Giesl, A. Serebrenik, R. Thiemann

Case 1: n = 0 and thus, s = pin (~s)
So s ∈ S and there is a rule ℓ → r ∈ RP with ℓ = pin (~ℓ) such that s = ℓσ and
t = rσ for some substitution σ with terms from T ∞ (Σ, V).
π(p)
Let s′ ∈ S′ with Unlab(s′ ) = s. Thus, we also have s′ ∈ S ′ where s′ = pin (~s)
(since a term with a root symbol pIin cannot be obtained from S ′ if one has performed at least one rewrite step with R′P ). Due to the construction of R′P , there
exists a rule ℓπ(p) → r′ ∈ R′P where Unlab(r′ ) = r. We define t′ to be r′ σ. Then
we clearly have s′ = ℓπ(p) σ →R′P r′ σ = t′ and Unlab(t′ ) = t.
q ), s →RP t, t = uc,i (t, ~q)
Case 2: n ≥ 1 and s = uc,i (s, ~
n
Since s ∈ S , there exists a pin (~s) with ~s ∈ T~ ∞ (Σ, V) such that pin (~s) →∗RP s, i.e.,
s ∈ Sm for some m ∈ N. Since the reduction from pin (~s) to s is shorter than the
overall reduction that led to s, we obtain that m < n.
Let s′ ∈ S′ with Unlab(s′ ) = s. Hence, we have s′ = uIc,i (s′ , ~q) for some label I
and Unlab(s′ ) = s. Since s′ ∈ S′ , there exists a pJin (~s) with ~s ∈ T~ ∞ (Σ, V) such that
pJin (~s) →∗R′ s′ . Hence, s′ ∈ S′ as well. Now the induction hypothesis implies that
P

there exists a t′ such that s′ →R′P t′ and Unlab(t′ ) = t. We define t′ = uIc,i (t′ , ~q).
Then we clearly have s′ →R′P t′ and Unlab(t′ ) = t.
Case 3: n ≥ 1 and s = uc,i (pout (~s), ~q)
Here, there exists a rule ℓ → r ∈ RP with ℓ = uc,i (pout (~ℓ), ~x) such that s = ℓσ and
t = rσ.
Let s′ ∈ S′ with Unlab(s′ ) = s. Hence, we have s′ = uIc,i (pJout (~s), ~q) for some labels
I and J. Since s′ ∈ S′ , s′ resulted from rewriting the term uIc,i (pJin (~s), ~q) which must
be an instantiated right-hand side of a rule from R′P . Due to the construction of
R′P , then there also exists a rule ℓ′ → r′ ∈ R′P where ℓ′ = uIc,i (pJout (~ℓ), ~x) and
Unlab(r′ ) = r. We define t′ = r′ σ. Then we have s′ = ℓ′ σ →R′P r′ σ = t′ and
clearly Unlab(t′ ) = t.
We now proceed to prove the theorem by contradiction. Assume there is a term
s0 ∈ S that is non-terminating w.r.t. RP , i.e., there is an infinite sequence of terms
s0 , s1 , s2 , . . . with si →RP si+1 . We must have s0 = pin (~t) with ~t ∈ T~ ∞ (Σ, V) and
π(p)
π(p)
π(pin (~t)) ∈ T (ΣPπ ). Let s′0 = pin (~t). Then s′0 ∈ S ′ , since π ′ (pin (~t)) ∈ T (ΣPπ′ ).
π(p)
The reason is that π ′ (pin ) = π(p) = π(pin ) and for all f ∈ Σ we have π ′ (f ) ⊆ π(f ).
So by (56), s′0 ∈ S′ and Unlab(s′0 ) = s0 imply that there is an s′1 with Unlab(s′1 ) =
s1 and s′0 →R′P s′1 . Clearly, this also implies s′1 ∈ S′ . By applying (56) repeatedly,
we therefore obtain an infinite sequence of labelled terms s′0 , s′1 , s′2 , . . . with s′i →R′P
s′i+1 .
6. FORMAL COMPARISON OF THE TRANSFORMATIONAL APPROACHES
In this section we formally compare the power of the classical transformation from
Section 1.1 with the power of our new approach. In the classical approach, the
class of queries is characterized by a moding function whereas in our approach, it is
characterized by an argument filter. Therefore, the following definition establishes
a relationship between modings and argument filters.
ACM Transactions on Computational Logic, Vol. V, No. N, 20YY.

Automated Termination Proofs for Logic Programs by Term Rewriting

·

39

Definition 6.1 (Argument Filter Induced by Moding). Let (Σ, ∆) be a signature
and let m be a moding over the set of predicate symbols ∆. Then for every predicate
symbol p ∈ ∆ we define the induced argument filter πm over ΣP as πm (pin ) =
πm (Pin ) = {i | m(p, i) = in} and πm (pout ) = {i | m(p, i) = out}. All other
function symbols f from ΣP are not filtered, i.e., πm (f /n) = {1, . . . , n}.
Example 6.2. Regard again the well-moded logic program from Example 1.1.
p(X, X).
p(f(X), g(Y )) :– p(f(X), f(Z)), p(Z, g(Y )).
We used the moding m with m(p, 1) = in and m(p, 2) = out. Thus, for the induced
argument filter πm we have πm (pin ) = πm (Pin ) = {1} and πm (pout ) = {2}.
As the classical approach is only applicable to well-moded logic programs, we
restrict our comparison to this class. For non-well-moded programs, our new approach is clearly more powerful, since it can often prove termination (cf. Section 7),
whereas the classical transformation is never applicable.
Our goal is to show the connection between the TRSs resulting from the two
′
transformations. If one refines πm to a filter πm
by Algorithm 1 using any arbitrary
refinement heuristic, then the TRS of the classical transformation corresponds to
′
the TRS of our new transformation after filtering it with πm
.
Example 6.3. We continue with Example 6.2. The TRS RP resulting from our
new transformation was given in Example 3.2:
pin (X, X) → pout (X, X)

(1)

pin (f(X), g(Y )) → u1 (pin (f(X), f(Z)), X, Y )
u1 (pout (f(X), f(Z)), X, Y ) → u2 (pin (Z, g(Y )), X, Y, Z)

(2)
(3)

u2 (pout (Z, g(Y )), X, Y, Z) → pout (f(X), g(Y ))

(4)

If we apply the induced argument filter πm , then we obtain the TRS πm (RP ):
pin (X) → pout (X)
pin (f(X)) → u1 (pin (f(X)), X, Y )
u1 (pout (f(Z)), X, Y ) → u2 (pin (Z), X, Y, Z)
u2 (pout (g(Y )), X, Y, Z) → pout (g(Y ))
The second rule has the “extra” variable Y on the
not satisfy the variable condition. Thus, we have to
′
′
′
′
ter πm
with πm
(u1 ) = πm
(U1 ) = {1, 2} and πm
(u2 )
′
resulting TRS πm (RP ) is identical to the TRS Rold
P
transformation, cf. Example 1.2:

right-hand side, i.e., it does
refine the filter πm to a fil′
= πm
(U2 ) = {1, 2, 4}. The
resulting from the classical

pin (X) → pout (X)
pin (f(X)) → u1 (pin (f(X)), X)
u1 (pout (f(Z)), X) → u2 (pin (Z), X, Z)
u2 (pout (g(Y )), X, Z) → pout (g(Y ))
The following theorem shows that our approach (with Corollary 4.5) succeeds
whenever the classical transformation of Section 1.1 yields a terminating TRS.
ACM Transactions on Computational Logic, Vol. V, No. N, 20YY.

40

·

P. Schneider-Kamp, J. Giesl, A. Serebrenik, R. Thiemann

Theorem 6.4 (Subsumption of the Classical Transformation). Let P
be a well-moded logic program over a signature (Σ, ∆) w.r.t. the moding m. Let
Rold
P be the result of applying the classical transformation of Section 1.1 and let
RP be the result of our new transformation from Definition 3.1. Then there is a
′
′
′
refinement of πm
of πm such that (a) πm
(RP ) and πm
(DP (RP )) satisfy the variable
condition and (b) if Rold
is
terminating
(with
ordinary
rewriting), then there is no
P
′
infinite (DP (RP ), RP , πm
)-chain. Thus, in particular, termination of Rold
P implies
that RP is terminating (with infinitary constructor rewriting) for all terms pin (~t)
with p ∈ ∆, ~t ∈ T~ ∞ (Σ, V), and π(pin (~t)) ∈ T (ΣPπ ).
′
Proof. Let πm
result from Algorithm 1 using any refinement heuristic ρ which
does not filter away the first argument of any uc,i .
′
We now analyze the structure of the TRS πm
(RP ). For any predicate symbol
~
~
p ∈ ∆, let “p(~s, t)” denote that ~s and t are the sequences of terms on p’s in- and
output positions w.r.t. the moding m.
′
When Algorithm 1 is applied to compute the refinement πm
of πm , one looks for
a rule ℓ → r from πm (RP ) such that V(r) 6⊆ V(ℓ). Such a rule cannot result from
the facts of the logic program. The reason is that for each fact p(~s, ~t), πm (RP )
contains the rule

pin (~s) → pout (~t)
and by well-modedness, we have V(~t) ⊆ V(~s).
For each rule c of the form p(~s, ~t) :– p1 (~s1 , ~t1 ), . . . , pk (~sk , ~tk ) in P, the TRS
πm (RP ) contains:
pin (~s) → uc,1 (p1in (~s1 ), V(~s) ∪ V(~t))
uc,1 (p1out (~t1 ), V(~s) ∪ V(~t)) → uc,2 (p2in (~s2 ), V(~s) ∪ V(~t) ∪ V(~s1 ) ∪ V(~t1 ))
..
.
uc,k (pkout (~tk ), V(~s) ∪ V(~t) ∪ V(~s1 ) ∪ V(~t1 ) ∪ . . . ∪ V(~sk−1 ) ∪ V(~tk−1 )) → pout (~t)
For the first rule, by well-modedness we have V(~s1 ) ⊆ V(~s) and thus, the only
“extra” variables on the right-hand side of the first rule must be from V(~t). There
is only one possibility to refine the argument filter in order to remove them: one
has to filter away the respective argument positions of uc,1 . Hence, the filtered
right-hand side of the first rule is uc,1 (p1in (~s1 ), V(~s)) and the filtered left-hand side
of the second rule is uc,1 (p1out (~t1 ), V(~s)).
Similarly, for the second rule, well-modedness implies V(~s2 )∪V(~s)∪V(~s1 )∪V(~t1 ) ⊆
V(~t1 ) ∪ V(~s). So the only “extra” variables on the right-hand side of the second
rule are again from V(~t). As before, to remove them one has to filter away the
respective argument positions of uc,2 . Moreover, since V(~s1 ) ⊆ V(~s) we obtain
the filtered right-hand side uc,2 (p2in (~s2 ), V(~s) ∪ V(~t1 )) for the second rule and the
filtered left-hand side uc,2 (p2out (~t2 ), V(~s) ∪ V(~t1 )) side in the third rule.
An analogous argument holds for the other rules. The last rule has no extra
variables, since V(~t) ⊆ V(~s) ∪ V(~t1 ) ∪ . . . ∪ V(~tk ) by well-modedness.
ACM Transactions on Computational Logic, Vol. V, No. N, 20YY.

Automated Termination Proofs for Logic Programs by Term Rewriting

·

41

′
So for any rule c of the logic program P, πm
(RP ) has the following rules:

pin (~s) → uc,1 (p1in (~s1 ), V(~s))
uc,1 (p1out (~t1 ), V(~s)) → uc,2 (p2in (~s2 ), V(~s) ∪ V(~t1 ))
..
.
uc,k (pkout (~tk ), V(~s) ∪ V(~t1 ) ∪ . . . ∪ V(~tk−1 )) → pout (~t)
′
′
Hence, πm
(RP ) = Rold
P . Since the refined argument filter πm does not filter away
′
′
the first argument of any uc,i , by defining πm (Uc,i ) := πm (uc,i ), then the variable
′
′
condition is satisfied for both πm
(RP ) and πm
(DP (RP )) and, thus, (a) is fulfilled.
old
Now to prove (b), we assume that RP is terminating. We have to show that
′
then there is no infinite (DP (RP ), RP , πm
)-chain. By the soundness of the argument filter processor (Theorem 4.13), it suffices to show that there is no infinite
′
′
(πm
(DP (RP )), πm
(RP ), id)-chain.
′
′
Note that πm (DP (RP )) = DP (πm
(RP )). The reason is that all uc,i only occur
on the root level in RP . Moreover, all pin -symbols only occur in the first argument
′
of a uc,i and 1 ∈ πm
(uc,i ). In other words, occurrences of defined function symbols
′
. So we have
are not removed by the filter πm
′
u → v ∈ πm
(DP (RP ))
′
′
iff there is a rule ℓ → r ∈ RP with u = πm
(ℓ♯ ), v = πm
(t♯ )
for a subterm t of r with defined root
′
′
iff there is a rule ℓ → r ∈ RP with u = (πm
(ℓ))♯ , v = (πm
(t))♯
′
′
for a subterm πm (t) of πm (r) with defined root
′
(RP ) with u = ℓ♯ , v = t♯
iff there is a rule ℓ → r ∈ πm
for a subterm t of r with defined root
′
iff u → v ∈ DP (πm
(RP ))
old
′
′
′
(RP ) = Rold
Hence, πm
P and πm (DP (RP )) = DP (πm (RP )) = DP (RP ). Thus,
old
old
it suffices to show absence of infinite (DP (RP ), RP , id)-chains. But this follows
from termination of Rold
P , cf. [Arts and Giesl 2000, Thm. 6], since (P, R, id)-chains
correspond to chains for ordinary (non-infinitary) rewriting.
~
Hence by Theorem 4.4, termination of Rold
P also implies that all terms pin (t) with
p ∈ ∆, ~t ∈ T~ ∞ (Σ, V), and π(pin (~t)) ∈ T (ΣPπ ) are terminating w.r.t. RP (using
infinitary constructor rewriting).

The reverse direction of the above theorem does not hold, though. As a counterexample, regard again the logic program from Example 1.1, cf. Example 6.3.
As shown in Example 1.2, the TRS resulting from the classical transformation is
′
not terminating. Still, for the filter πm
from Example 6.3, there is no infinite
′
(DP (RP ), RP , πm )-chain and thus, our method of Corollary 4.5 succeeds with the
termination proof. In other words, our new approach is strictly more powerful than
the classical transformation, even on well-moded programs.
Thus, a termination analyzer based on our new transformation should be strictly
more successful in practice, too. That this is in fact the case will be demonstrated
in the next section.
ACM Transactions on Computational Logic, Vol. V, No. N, 20YY.

42

·

P. Schneider-Kamp, J. Giesl, A. Serebrenik, R. Thiemann

7. EXPERIMENTS AND DISCUSSION
We integrated our approach (including all refinements presented) in the termination
tool AProVE [Giesl et al. 2006] which implements the DP framework. To evaluate
our results, we tested AProVE against four other representative termination tools
for logic programming: TALP [Ohlebusch et al. 2000] is the only other available
tool based on transformational methods (it uses the classical transformation of
Section 1.1), whereas Polytool [Nguyen and De Schreye 2007], TerminWeb [Codish
and Taboch 1999], and cTI [Mesnard and Bagnara 2005] are based on direct approaches. Section 7.1 describes the results of our experimental evaluation and in
Section 7.2 we discuss the limitations of our approach.
7.1 Experimental Evaluation
We ran the tools on a set of 296 examples in fully automatic mode.14 This set
includes all logic programming examples from the Termination Problem Data Base
[TPDB 2007] which is used in the annual international Termination Competition
[Marché and Zantema 2007]. It contains collections provided by the developers of
several different tools including all examples from the experimental evaluation of
[Bruynooghe et al. 2007]. However, to eliminate the influence of the translation
from Prolog to logic programs, we removed all examples that use non-trivial builtin predicates or that are not definite logic programs after ignoring the cut operator.
All tools were run locally on an AMD Athlon 64 at 2.2 GHz under GNU/Linux 2.6.
For each example we used a time limit of 60 seconds. This is similar to the way
that tools are evaluated in the annual competitions for termination tools.
Successes
Failures
Timeouts

AProVE
232
57
7

Polytool
204
82
10

TerminWeb
177
118
1

cTI
167
129
0

TALP
163
112
21

As shown in the table above, AProVE succeeds on more examples than any other
tool. The comparison of AProVE and TALP shows that our approach improves
significantly upon the previous transformational method that TALP is based on, cf.
Goals (A) and (B). In particular, TALP fails for all non-well-moded programs.
While we have shown our technique to be strictly more powerful than the previous
transformational method, due to the higher arity of the function symbols produced
by our transformation, proving termination could take more time in some cases.
However, in the above experiments this did not affect the practical power of our
implementation. In fact, AProVE is able to prove termination well within the time
limit for all examples where TALP succeeds. Further analysis shows that while
AProVE never takes more than 15 seconds longer than TALP, there are indeed 6
examples where AProVE is more than 15 seconds faster than TALP.
14 We

combined termsize and list-length norm for TerminWeb and allowed 5 iterations before
widening for cTI. Apart from that, we used the default settings of the tools. For both AProVE and
Polytool we used the (fully automated) original executables from the Termination Competition
2007 [Marché and Zantema 2007]. To refine argument filters, this version of AProVE uses the
refinement heuristic ρtb ′ from Definition 5.13. For a list of the main termination techniques used
in AProVE, we refer to [Giesl et al. 2005; Giesl et al. 2006]. Of these techniques, only the ones in
Section 4.2 were adapted to infinitary constructor rewriting.
ACM Transactions on Computational Logic, Vol. V, No. N, 20YY.

Automated Termination Proofs for Logic Programs by Term Rewriting

·

43

The comparison with Polytool, TerminWeb, and cTI demonstrates that our new
transformational approach is not only comparable in power, but usually more powerful than direct approaches. In fact, there is only a single example where one of
the other tools (namely Polytool) succeeds and AProVE fails. This is the rather
contrived example from (2) in Section 7.2 which we developed to demonstrate the
limitations of our method. Polytool is only able to handle this example via a preprocessing step based on partial evaluation [Nguyen et al. 2006; Serebrenik and
De Schreye 2003; Tamary and Codish 2004]. In this example, this pre-processing
step results in a trivially terminating logic program. Thus, if one combined this
pre-processing with any of the other tools, then they would also be able to prove
termination of this particular example.15 Integrating some form of partial evaluation into AProVE might be an interesting possibility for further improvement.
For all other examples, AProVE can show termination whenever at least one of
the other tools succeeds. Moreover, there are several examples where AProVE succeeds whereas no other tool shows the termination. These include examples where
the termination proof requires more complex orders. For instance, termination
of the example SGST06/hbal tree.pl can be proved using recursive path orders
with status and termination of talp/apt/mergesort ap.pl is shown using matrix
orders.16
Note that 52 examples in this collection are known to be non-terminating, i.e.,
there are at most 244 terminating examples. In other words, there are only at most
12 terminating examples where AProVE did not manage to prove termination. With
this performance, AProVE won the Termination Competition with Polytool being
the second most powerful tool. The best tool for non-termination analysis of logic
programs was NTI [Payet and Mesnard 2006].
However, from the experiments above one should not draw the conclusion that the
transformational approach is always better than the direct approach to termination
analysis of logic programs. There are several extensions (e.g., termination inference
[Codish and Taboch 1999; Mesnard and Bagnara 2005], non-termination analysis
[Payet and Mesnard 2006], handling numerical data structures [Serebrenik and De
Schreye 2004; 2005b]) that can currently only be handled by direct techniques and
tools.
Regarding the use of term rewriting techniques for termination analysis of logic
programs, it is interesting to note that the currently most powerful tool for direct termination analysis of logic programs (Polytool) implements the framework
of [Nguyen and De Schreye 2005; 2007] for applying techniques from term rewriting (most notably polynomial interpretations) to logic programs directly. This
framework forms the basis for further extensions to other TRS-termination techniques. For example, it can be extended further by adapting also basic results of
the dependency pair method to the logic programming setting [Nguyen et al. 2008].
Preliminary investigations with a prototypical implementation indicate that in this
way, one can prove termination of several examples where the transformational
15 Similarly,

with such a pre-processing the existing “direct” tools would also be able to prove
termination of the program in Example 1.1.
16 For recursive path orders with status and matrix orders see [Lescanne 1983] resp. [Endrullis
et al. 2006].
ACM Transactions on Computational Logic, Vol. V, No. N, 20YY.

44

·

P. Schneider-Kamp, J. Giesl, A. Serebrenik, R. Thiemann

approach with AProVE currently fails.
So transformational and direct approaches both have their advantages and the
most powerful solution might be to combine direct tools like Polytool with a transformational prover like AProVE which is based on the contributions of this paper.
But it is clear that it is indeed beneficial to use termination techniques from TRSs
for logic programs, both for direct and for transformational approaches.
In addition to the experiments described above (which compare different termination provers), we also performed experiments with several versions of AProVE in
order to evaluate the different heuristics and algorithms for the computation of argument filters from Section 5. The following table shows that indeed our improved
type-based refinement heuristic (tb′ ) from Section 5.3 significantly outperforms the
simple improved outermost (om′ ) and innermost (im) heuristics from Section 5.2. In
fact, all examples that could be proved terminating by any of the simple heuristics
can also be proved terminating by the type-based heuristic.
Successes
Failures
Timeouts

AProVE tb′
232
57
7

AProVE om′
218
76
2

AProVE im
195
98
3

So far, for all experiments we used Algorithm 2 (from Section 5.4) in order to
compute a refined argument filter from the initial one. To evaluate the advantage of
this improved algorithm over Algorithm 1 (from Section 5.1), we performed experiments with the two algorithms (again using the type-based refinement heuristic tb′
from Section 5.3). The following table shows that Algorithm 2 is indeed significantly
more powerful than Algorithm 1.
Successes
Failures
Timeouts

AProVE Algorithm 2
232
57
7

AProVE Algorithm 1
212
74
10

As mentioned in Section 1.3, preliminary versions of parts of this paper appeared
in [Schneider-Kamp et al. 2007]. However, the table below clearly shows that the
results of Section 5 (which are new compared to [Schneider-Kamp et al. 2007])
improve the power of termination analysis substantially. To this end, we compare
our new implementation that uses the improved type-based refinement heuristic
(tb′ ) and the improved refinement algorithm (Algorithm 2) from Section 5 with
the version of AProVE from the Termination Competition 2006 that only contains
the results of [Schneider-Kamp et al. 2007]. To find argument filters, it uses a
simple ad-hoc heuristic which turns out to be clearly disadvantageous to the new
sophisticated techniques from Section 5.
Successes
Failures
Timeouts

AProVE tb′
232
57
7

AProVE [Schneider-Kamp et al. 2007]
208
69
19

To run AProVE, for details on our experiments, and to access our collection of
examples, we refer to http://aprove.informatik.rwth-aachen.de/eval/TOCL/.
ACM Transactions on Computational Logic, Vol. V, No. N, 20YY.

Automated Termination Proofs for Logic Programs by Term Rewriting

·

45

7.2 Limitations
Our experiments also contain examples which demonstrate the limitations of our approach. Of course, our implementation in AProVE usually fails if there are features
outside of pure logic programming (e.g., built-in predicates, negation as failure,
meta programming, etc.). We consider the handling of meta-logical features such
as cuts and meta programming as future work. We think that techniques from term
rewriting are especially well-suited to handle meta programming as term rewriting
does not rely on a distinction between predicate and function symbols.
In the following, we discuss the limitations of the approach when applying it for
pure logic programming. In principle, there could be three points of failure:
(1) The transformation of Theorem 3.7 could fail, i.e., there could be a logic program which is terminating for the set of queries, but not all corresponding terms
are terminating in the transformed TRS. We do not know of any such example.
It is currently open whether this step is in fact complete.
(2) The approach via dependency pairs (Theorem 4.4) can fail to prove termination
of the transformed TRS, although the TRS is terminating. In particular, this
can happen because of the variable condition required for Theorem 4.4. This
is demonstrated by the following logic program P:
p(X)
:– q(f(Y )), p(Y ).
p(g(X)) :– p(X).
q(g(Y )).
The resulting TRS RP is
pin (X) → u1 (qin (f(Y )), X)
u1 (qout (f(Y )), X) → u2 (pin (Y ), X, Y )
u2 (pout (Y ), X, Y ) → pout (X)
pin (g(X)) → u3 (pin (X), X)
u3 (pout (X), X) → pout (g(X))
qin (g(Y )) → qout (g(Y ))
and there are the following dependency pairs.
Pin (X) → Qin (f(Y ))

(57)

Pin (X) → U1 (qin (f(Y )), X)

(58)

U1 (qout (f(Y )), X) → Pin (Y )
U1 (qout (f(Y )), X) → U2 (pin (Y ), X, Y )

(59)
(60)

Pin (g(X)) → Pin (X)
Pin (g(X)) → U3 (pin (X), X)

(61)
(62)

We want to prove termination of all queries p(t) where t is finite and ground
(i.e., m(p, 1) = in). Looking at the logic program P, it is obvious that they
are all terminating. However, there is no argument filter π such that π(RP )
and π(DP (RP )) satisfy the variable condition and such that there is no infinite
(DP (RP ), RP , π)-chain.
ACM Transactions on Computational Logic, Vol. V, No. N, 20YY.

46

·

P. Schneider-Kamp, J. Giesl, A. Serebrenik, R. Thiemann

To see this, note that if π(Pin ) = ∅ or π(g) = ∅ then we can build an infinite
chain with the last dependency pair where we instantiate X by the infinite term
g(g(. . .)). So, let π(Pin ) = π(g) = {1}. Due to the variable condition of the
dependency pair (59) we know π(f) = π(qout ) = {1} and 1 ∈ π(U1 ). Hence, to
satisfy the variable condition in dependency pair (58) we must set π(qin ) = ∅.
But then the last rule of π(RP ) does not satisfy the variable condition.
(3) Finally it can happen that the resulting DP problem of Theorem 4.4 is finite, but
that our implementation fails to prove it. The reason can be that one should
apply other DP processors or DP processors with other parameters. After
all, finiteness of DP problems is undecidable. This is shown by the following
example where we are interested in all queries f(t1 , t2 ) where t1 and t2 are
ground terms:
f(X, Y )
:– g(s(s(s(s(s(X))))), Y ).
f(s(X), Y )
:– f(X, Y ).
g(s(s(s(s(s(s(X)))))), Y ) :– f(X, Y ).
Termination can (for example) be proved if one uses a polynomial order with
coefficients from {0, 1, 2, 3, 4, 5}. But the current automation does not use such
polynomials and thus, it fails when trying to prove termination of this example.
While the DP method can also be used for non-termination proofs if one considers ordinary rewriting, this is less obvious for infinitary constructor rewriting. The
reason is that the main termination criterion is “complete” for ordinary rewriting,
but incomplete for infinitary constructor rewriting (cf. the counterexample (2) to
the completeness of Theorem 4.4 above). Therefore, in order to also prove nontermination of logic programs, a combination of our method with a loop-checker
for logic programs would be fruitful. As mentioned before, a very powerful nontermination tool for logic programs is NTI [Payet and Mesnard 2006]. Our collection
of 296 examples contains 233 terminating examples (232 of these can be successfully shown by AProVE), 52 non-terminating examples, and 11 examples whose
termination behavior is unknown. NTI can prove non-termination of 42 of the
52 non-terminating examples. Hence, a combination of AProVE and NTI would
successfully analyze the termination behaviour of 274 of the 296 examples.
8. CONCLUSION
In this paper, we developed a new transformation from logic programs P to TRSs
RP . To prove the termination of a class of queries for P, it is now sufficient to
analyze the termination behavior of RP on a corresponding class of terms w.r.t.
infinitary constructor rewriting. This class of terms is characterized by a so-called
argument filter and we showed how to generate such argument filters from the
given class of queries for P. Our approach is even sound for logic programming
without occur check. To prove termination of infinitary rewriting automatically, we
showed how to adapt the DP framework of [Arts and Giesl 2000; Giesl et al. 2005;
Giesl et al. 2006] from ordinary term rewriting to infinitary constructor rewriting.
Then the DP framework can be used for termination proofs of RP and thus, for
automated termination analysis of P. Since any termination technique for TRSs
can be formulated as a DP processor [Giesl et al. 2005], now any such technique
ACM Transactions on Computational Logic, Vol. V, No. N, 20YY.

Automated Termination Proofs for Logic Programs by Term Rewriting

·

47

can also be used for logic programs.
In addition to the results presented in [Schneider-Kamp et al. 2007], we showed
that our new approach subsumes the classical transformational approach to termination analysis of logic programs. We also provided new heuristics and algorithms
for refining the initial argument filter that improve the power of our method (and
hence, also of its implementation) substantially.
Moreover, we implemented all contributions in our termination prover AProVE
and performed extensive experiments which demonstrate that our results are indeed
applicable in practice. More precisely, due to our contributions, AProVE has become
the currently most powerful automated termination prover for logic programs.
ACKNOWLEDGMENTS

We thank Mike Codish, Danny De Schreye, and Fred Mesnard for helpful comments
and discussions on the results presented here and Roberto Bagnara, Samir Genaim,
and Manh Thang Nguyen for help with the experiments.
REFERENCES
Aguzzi, G. and Modigliani, U. 1993. Proving Termination of Logic Programs by Transforming
them into Equivalent Term Rewriting Systems. In FSTTCS ’93. LNCS, vol. 761. 114–124.
Apt, K. R. and Etalle, S. 1993. On the Unification Free Prolog Programs. In MFCS ’93. LNCS,
vol. 711. 1–19.
Apt, K. R. 1997. From Logic Programming to Prolog. Prentice Hall, London.
Arts, T. and Zantema, H. 1995. Termination of Logic Programs Using Semantic Unification.
In LOPSTR ’95. LNCS, vol. 1048. 219–233.
Arts, T. and Giesl, J. 2000. Termination of Term Rewriting Using Dependency Pairs. Theoretical Computer Science 236, 133–178.
Baader, F. and Nipkow, T. 1998. Term Rewriting and All That. Cambridge University Press.
Bossi, A., Cocco, N., and Fabris, M. 1992. Typed Norms. In ESOP ’92. LNCS, vol. 582. 73–92.
Bruynooghe, M., Demoen, B., Boulanger, D., Denecker, M., and Mulkers, A. 1996. A
Freeness and Sharing Analysis of Logic Programs Based on a Pre-Interpretation. In SAS ’96.
LNCS, vol. 1145. 128–142.
Bruynooghe, M., Gallagher, J. P., and Van Humbeeck, W. 2005. Inference of Well-Typings
for Logic Programs with Application to Termination Analysis. In SAS ’05. LNCS, vol. 3672.
35–51.
Bruynooghe, M., Codish, M., Gallagher, J. P., Genaim, S., and Vanhoof, W. 2007. Termination Analysis of Logic Programs through Combination of Type-Based Norms. ACM Transactions on Programming Languages and Systems 29, 2, Article 10.
Charatonik, W. and Podelski, A. 1998. Directional Type Inference for Logic Programs. In
SAS ’98. LNCS, vol. 1503. 278–294.
Chtourou, M. and Rusinowitch, M. 1993. Méthode Transformationelle pour la Preuve de
Terminaison des Programmes Logiques. Unpublished manuscript.
Codish, M. and Taboch, C. 1999. A Semantic Basis for Termination Analysis of Logic Programs.
Journal of Logic Programming 41, 1, 103–123.
Codish, M., Lagoon, V., and Stuckey, P. 2005. Testing for Termination with Monotonicity
Constraints. In ICLP ’05. LNCS, vol. 3668. 326–340.
Codish, M., Lagoon, V., Schachte, P., and Stuckey, P. 2006. Size-Change Termination
Analysis in k-Bits. In ESOP ’06. LNCS, vol. 3924. 230–245.
Codish, M. 2007. Collection of Benchmarks. Available at http://lvs.cs.bgu.ac.il/~ mcodish/
suexec/terminweb/bin/terminweb.cgi?command=examples.
Colmerauer, A. 1982. Prolog and Infinite Trees. In Logic Programming, K. L. Clark and
S. Tärnlund, Eds. Academic Press, Oxford.
ACM Transactions on Computational Logic, Vol. V, No. N, 20YY.

48

·

P. Schneider-Kamp, J. Giesl, A. Serebrenik, R. Thiemann

Cortesi, A. and Filé, G. 1999. Sharing is Optimal. Journal of Logic Programming 38, 3,
371–386.
De Schreye, D. and Decorte, S. 1994. Termination of Logic Programs: The Never-Ending
Story. Journal of Logic Programming 19-20, 199–260.
De Schreye, D. and Serebrenik, A. 2002. Acceptability with General Orderings. In Computational Logic: Logic Programming and Beyond. Essays in Honour of Robert A. Kowalski, Part
I, A. C. Kakas and F. Sadri, Eds. LNCS, vol. 2407. 187–210.
Decorte, S., De Schreye, D., and Fabris, M. 1993. Automatic Inference of Norms: A Missing
Link in Automatic Termination Analysis. In ILPS ’93. MIT Press, Boston, 420–436.
Dershowitz, N. 1987. Termination of Rewriting. Journal of Symbolic Computation 3, 1–2,
69–116.
Endrullis, J., Waldmann, J., and Zantema, H. 2006. Matrix Interpretations for Proving Termination of Term Rewriting. In IJCAR ’06. LNAI, vol. 4130. 574–588.
Gallagher, J. P. and Puebla, G. 2002. Abstract Interpretation over Non-deterministic Finite
Tree Automata for Set-Based Analysis of Logic Programs. In PADL ’02. LNCS, vol. 2257.
243–261.
Ganzinger, H. and Waldmann, U. 1993. Termination Proofs of Well-moded Logic Programs
via Conditional Rewrite Systems. In CTRS ’92. LNCS, vol. 656. 430–437.
Geser, A., Hofbauer, D., and Waldmann, J. 2004. Match-Bounded String Rewriting Systems.
Applicable Algebra in Engineering, Communication and Computing 15, 3–4, 149–171.
Giesl, J., Thiemann, R., and Schneider-Kamp, P. 2005. The Dependency Pair Framework:
Combining Techniques for Automated Termination Proofs. In LPAR ’04. LNAI, vol. 3452.
301–331.
Giesl, J., Schneider-Kamp, P., and Thiemann, R. 2006. AProVE 1.2: Automatic Termination
Proofs in the DP Framework. In IJCAR ’06. LNAI, vol. 4130. 281–286.
Giesl, J., Swiderski, S., Schneider-Kamp, P., and Thiemann, R. 2006. Automated Termination
Analysis for Haskell: From Term Rewriting to Programming Languages. In RTA ’06. LNCS,
vol. 4098. 297–312.
Giesl, J., Thiemann, R., Schneider-Kamp, P., and Falke, S. 2006. Mechanizing and Improving
Dependency Pairs. Journal of Automated Reasoning 37, 3, 155–203.
Hirokawa, N. and Middeldorp, A. 2005. Automating the Dependency Pair Method. Information and Computation 199, 1,2, 172–199.
Huet, G. 1976. Résolution d’Equations dans les Langages d’Ordre 1, 2, . . . , ω. PhD thesis.
Janssens, G. and Bruynooghe, M. 1992. Deriving Descriptions of Possible Values of Program
Variables by Means of Abstract Interpretation. Journal of Logic Programming 13, 2–3, 205–258.
Krishna Rao, M. R. K., Kapur, D., and Shyamasundar, R. K. 1998. Transformational Methodology for Proving Termination of Logic Programs. Journal of Logic Programming 34, 1, 1–41.
Lagoon, V. and Stuckey, P. J. 2002. Precise Pair-Sharing Analysis of Logic Programs. In
PPDP ’02. ACM Press, New York, 99–108.
Lagoon, V., Mesnard, F., and Stuckey, P. J. 2003. Termination Analysis with Types Is More
Accurate. In ICLP ’03. LNCS, vol. 2916. 254–268.
Lescanne, P. 1983. Computer Experiments with the REVE Term Rewriting System Generator.
In POPL ’83. ACM Press, New York, 99–108.
Leuschel, M. and Sørensen, M. H. 1996. Redundant Argument Filtering of Logic Programs.
In LOPSTR ’96. LNCS, vol. 1207. 83–103.
Lindenstrauss, N., Sagiv, Y., and Serebrenik, A. 1997. TermiLog: A System for Checking
Termination of Queries to Logic Programs. In CAV ’97. LNCS, vol. 1254. 444–447.
Lu, L. 2000. A Precise Type Analysis of Logic Programs. In PPDP ’00. ACM Press, New York,
214–225.
Marché, C. and Zantema, H. 2007. The Termination Competition. In RTA ’07. LNCS, vol.
4533. 303–313. See also http://www.lri.fr/~ marche/termination-competition/.
Marchiori, M. 1994. Logic Programs as Term Rewriting Systems. In ALP ’94. LNCS, vol. 850.
223–241.
ACM Transactions on Computational Logic, Vol. V, No. N, 20YY.

Automated Termination Proofs for Logic Programs by Term Rewriting

·

49

Marchiori, M. 1996. Proving Existential Termination of Normal Logic Programs. In AMAST ’96.
LNCS, vol. 1101. 375–390.
Martin, J., King, A., and Soper, P. 1996. Typed Norms for Typed Logic Programs. In
LOPSTR ’96. LNCS, vol. 1207. 224–238.
Mesnard, F. and Ruggieri, S. 2003. On Proving Left Termination of Constraint Logic Programs.
ACM Transactions on Computational Logic 4, 2, 207–259.
Mesnard, F. and Bagnara, R. 2005. cTI: A Constraint-Based Termination Inference Tool for
ISO-Prolog. Theory and Practice of Logic Programming 5, 1&2, 243–257.
Mesnard, F. and Serebrenik, A. 2007. Recurrence with Affine Level Mappings is P-Time
Decidable for CLP(R). Theory and Practice of Logic Programming 8, 1, 111–119.
Nguyen, M. T. and De Schreye, D. 2005. Polynomial Interpretations as a Basis for Termination
Analysis of Logic Programs. In ICLP ’05. LNCS, vol. 3668. 311–325.
Nguyen, M. T., Bruynooghe, M., De Schreye, D., and Leuschel, M. 2006. Program Specialisation as a Pre-Processing Step for Termination Analysis. In WST ’06. 7–11. Available at
http://www.easychair.org/FLoC-06/WST-preproceedings.pdf.
Nguyen, M. T. and De Schreye, D. 2007. Polytool: Proving Termination Automatically Based
on Polynomial Interpretations. In LOPSTR ’06. LNCS, vol. 4407. 210–218.
Nguyen, M. T., Giesl, J., Schneider-Kamp, P., and De Schreye, D. 2008. Termination
Analysis of Logic Programs based on Dependency Graphs. In LOPSTR ’07. LNCS, vol. 4915.
8–22.
Ohlebusch, E., Claves, C., and Marché, C. 2000. TALP: A Tool for the Termination Analysis
of Logic Programs. In RTA ’00. LNCS, vol. 1833. 270–273.
Ohlebusch, E. 2001. Termination of Logic Programs: Transformational Methods Revisited.
Applicable Algebra in Engineering, Communication and Computing 12, 1–2, 73–116.
Payet, E. and Mesnard, F. 2006. Nontermination Inference of Logic Programs. ACM Transactions on Programming Languages and Systems 28, 2, 256–289.
van Raamsdonk, F. 1997. Translating Logic Programs into Conditional Rewriting Systems. In
ICLP ’97. MIT Press, Boston, 168–182.
Schneider-Kamp, P., Giesl, J., Serebrenik, A., and Thiemann, R. 2007. Automated Termination Analysis for Logic Programs by Term Rewriting. In LOPSTR ’06. LNCS, vol. 4407.
177–193.
Serebrenik, A. and De Schreye, D. 2003. Proving Termination with Adornments. In
LOPSTR ’03. LNCS, vol. 3018. 108–109.
Serebrenik, A. and De Schreye, D. 2004. Inference of Termination Conditions for Numerical
Loops in Prolog. Theory and Practice of Logic Programming 4, 5&6, 719–751.
Serebrenik, A. and De Schreye, D. 2005a. On Termination of Meta-Programs. Theory and
Practice of Logic Programming 5, 3, 355–390.
Serebrenik, A. and De Schreye, D. 2005b. Termination of Floating Point Computations.
Journal of Automated Reasoning 34, 2, 141–177.
Smaus, J.-G. 2004. Termination of Logic Programs Using Various Dynamic Selection Rules. In
ICLP ’04. LNCS, vol. 3132. 43–57.
Tamary, L. and Codish, M. 2004. Abstract Partial Evaluation for Termination Analysis. In
WST ’04. 47–50. Available at http://aib.informatik.rwth-aachen.de/2004/2004-07.pdf.
TPDB 2007. The Termination Problem Data Base 4.0 (May 24, 2007). Available at http:
//www.lri.fr/~ marche/tpdb/.
Vaucheret, C. and Bueno, F. 2002. More Precise Yet Efficient Type Inference for Logic Programs. In SAS ’02. LNCS, vol. 2477. 102–116.
Walther, C. 1994. On Proving the Termination of Algorithms by Machine. Artificial Intelligence 71, 1, 101–157.
Zantema, H. 1995. Termination of Term Rewriting by Semantic Labelling. Fundamenta Informaticae 24, 1–2, 89–105.
Received March 2008; accepted July 2008
ACM Transactions on Computational Logic, Vol. V, No. N, 20YY.

