Non-Termination Inference of Logic Programs

arXiv:cs/0406041v1 [] 22 Jun 2004

Etienne Payet and Fred Mesnard
IREMIA, Université de La Réunion, France

We present a static analysis technique for non-termination inference of logic programs. Our
framework relies on an extension of the subsumption test, where some specific argument
positions can be instantiated while others are generalized. We give syntactic criteria to
statically identify such argument positions from the text of a program. Atomic left looping
queries are generated bottom-up from selected subsets of the binary unfoldings of the program of interest. We propose a set of correct algorithms for automating the approach. Then,
non-termination inference is tailored to attempt proofs of optimality of left termination conditions computed by a termination inference tool. An experimental evaluation is reported.
When termination and non-termination analysis produce complementary results for a logic
procedure, then with respect to the leftmost selection rule and the language used to describe
sets of atomic queries, each analysis is optimal and together, they induce a characterization
of the operational behavior of the logic procedure.
Keywords: languages, verification, logic programming, static analysis, non-termination analysis, optimal termination condition

1

Introduction

Since the work of N. Lindenstrauss on TermiLog [20, 12], several automatic tools for termination
checking (e.g. TALP [3]) or termination inference (e.g. cTI [25, 26] or TerminWeb [17]) are now
available to the logic programmer. As the halting problem is undecidable for logic programs, such
analyzers compute sufficient termination conditions implying left termination. In most works,
only universal left termination is considered and termination conditions rely on a language for
describing classes of atomic queries. The search tree associated to any (concrete) query satisfying
a termination condition is guaranteed to be finite. When terms are abstracted using the term-size
norm, the termination conditions are (disjunctions of) conjunctions of conditions of the form “the
i-th argument is ground”. Let us call this language Lterm .
In this report, which is based on an earlier conference paper [27], we present the first approach
to non-termination inference tailored to attempt proofs of optimality of termination conditions at
verification time for pure logic programs. The aim is to ensure the existence, for each class of
atomic queries not covered by a termination condition, of one query from this class which leads to
an infinite search tree when such a query is proved using any standard Prolog engine. We shall first
present an analysis which computes classes of left looping queries, where any atomic query from
such a class is guaranteed to lead to at least one infinite derivation under the usual left-to-right
selection rule. Intuitively, we begin by computing looping queries from recursive binary clauses
of the form p(. . .) ← p(. . .). Then we try to add binary clauses of the form q(. . .) ← p(. . .) to
increase the set of looping queries. Finally by combining the result of non-termination inference
with termination inference, for each predicate, we compute the set of modes for which the overall
verification system has no information.
The main contributions of this work are:
• A new application of binary unfoldings to left loop inference. [16] introduced the binary

1

unfoldings of a logic program P as a goal independent technique to transform P into a
possibly infinite set of binary clauses, which preserves the termination property [7] while
abstracting the standard operational semantics. We present a correct algorithm to construct
left looping classes of atomic goals, where such classes are computed bottom-up from selected
subsets of the binary unfoldings of the analyzed program.
• A correct algorithm which, when combined with termination inference [23], may detect
optimal left termination conditions expressed in Lterm for logic programs. When termination
and non-termination analysis produce complementary results for a logic procedure, then with
respect to the leftmost selection rule and the language used to describe sets of atomic queries,
each analysis is optimal and together, they induce a characterization of the operational
behavior of the logic procedure.
• A report on the experimental evaluation we conduct. We have fully implemented termination
and non-termination inference for logic programs. We have run the couple of analyzers on
a set of classical logic programs, the sizes of which range from 2 to 177 clauses. The results
of this experiment should help the reader to appreciate the value of the approach.
We organize the paper as follows: Section 2 presents the notations. In Section 3 we study
loop inference for binary programs. We offer a full set of correct algorithms for non-termination
inference in Section 4 and optimality proofs of termination conditions in Section 5. Finally, in
Section 6, we discuss related works. The detailed proofs of the results can be found in Appendix B,
at the end of the article.

2
2.1

Preliminaries
Functions

Let E and F be two sets. Then, f : E → F denotes that f is a partial function from E to F and
f : E ֌ F denotes that f is a function from E to F . The domain of a partial function f from E
to F is denoted by Dom(f ) and is defined as: Dom(f ) = {e | e ∈ E, f (e) exists}. Thus, if f is a
function from E to F , then Dom(f ) = E. Finally, if f : E → F is a partial function and E ′ is a
set, then f |E ′ is the function from Dom(f ) ∩ E ′ to F such that for each e ∈ Dom(f ) ∩ E ′ , f |E ′
maps e to f (e).

2.2

Logic Programming

We strictly adhere to the notations, definitions, and results presented in [1].
N denotes the set of non-negative integers and for any n ∈ N , [1, n] denotes the set {1, . . . , n}.
If n = 0 then [1, n] = ∅.
From now on, we fix a language L of programs. We assume that L contains an infinite number
of constant symbols. The set of relation symbols of L is Π, and we assume that each relation
symbol p has a unique arity, denoted arity(p). T UL (resp. T BL ) denotes the set of all (ground
and non ground) terms of L (resp. atoms of L). A query is a finite sequence of atoms A1 , . . . , An
(where n ≥ 0). When n = 1, we say that the query is atomic. Throughout this article, the
variables of L are denoted by X, Y, Z, . . . , the constant symbols by a, b, . . . , the function symbols
by f, g, h, . . . , the relation symbols by p, q, r, . . . , the atoms by A, B, . . . and the queries by Q, Q′ ,
. . . or by A, B, . . .
Let t be a term. Then V ar(t) denotes the set of variables occurring in t. This notation is
extended to atoms, queries and clauses. Let θ := {X1 /t1 , . . . , Xn /tn } be a substitution. We
denote by Dom(θ) the set of variables {X1 , . . . , Xn } and by Ran(θ) the set of variables appearing
in t1 , . . . , tn . We define V ar(θ) = Dom(θ) ∪ Ran(θ). Given a set of variables V , θ|V denotes the
substitution obtained from θ by restricting its domain to V .

2

Let t be a term and θ be a substitution. Then, the term tθ is called an instance of t. If θ is a
renaming (i.e. a substitution that is a 1-1 and onto mapping from its domain to itself), then tθ is
called a variant of t. Finally, t is called more general than t′ if t′ is an instance of t.
A logic program is a finite set of definite clauses. In program examples, we use the ISO-Prolog
syntax. Let P be a logic program. Then ΠP denotes the set of relation symbols appearing in P .
In this paper, we only focus on left derivations i.e. we only consider the leftmost selection rule.
Consider a non-empty query B, C and a clause c. Let H ← B be a variant of c variable disjoint
θ
with B, C and assume that B and H unify. Let θ be an mgu of B and H. Then B, C =⇒(B, C)θ
c
is a left derivation step with H ← B as its input clause. If the substitution θ or the clause c is
irrelevant, we drop a reference to it.
θ2
θ1
· · · of left derivation steps is called a
Q1 =⇒
Let Q0 be a query. A maximal sequence Q0 =⇒
c1

c2

left derivation of P ∪ {Q0 } if c1 , c2 , . . . are clauses of P and if the standardization apart condition
holds, i.e. each input clause used is variable disjoint from the initial query Q0 and from the mgu’s
and input clauses used at earlier steps. A finite left derivation may end up either with the empty
query (then it is a successful left derivation) or with a non-empty query (then it is a failed left
derivation). We say Q0 left loops with respect to (w.r.t.) P if there exists an infinite left derivation
+
of P ∪ {Q0 }. We write Q =⇒ Q′ if there exists a finite non-empty prefix ending at Q′ of a left
P

derivation of P ∪ {Q}.

2.3

The Binary Unfoldings of a Logic Program

Let us present the main ideas about the binary unfoldings [16] of a logic program, borrowed from
[7]. This technique transforms a logic program P into a possibly infinite set of binary clauses.
Intuitively, each generated binary clause H ← B (where B is either an atom or the atom true
which denotes the empty query) specifies that, with respect to the original program P , a call to
H (or any of its instances) necessarily leads to a call to B (or its corresponding instance).
More precisely, let Q be an atomic query. Then A is a call in a left derivation of P ∪ {Q} if
+
Q =⇒ A, B. We denote by calls P (Q) the set of calls which occur in the left derivations of P ∪ {Q}.
P

The specialization of the goal independent semantics for call patterns for the left-to-right selection
rule is given as the fixpoint of an operator TPβ over the domain of binary clauses, viewed modulo
renaming. In the definition below, id denotes the set of all binary clauses of the form true ← true
or p(X1 , . . . , Xn ) ← p(X1 , . . . , Xn ) for any p ∈ ΠP , where arity(p) = n.


c := H ← B1 , . . . , Bm ∈ P, i ∈ [1, m],








hHj ← trueii−1
∈
X
renamed
with
fresh
variables,


j=1
β
TP (X) = (H ← B)θ Hi ← B ∈ X ∪ id renamed with fresh variables,




i < m ⇒ B 6= true






θ = mgu(hB1 , . . . , Bi i, hH1 , . . . , Hi i)

We define its powers as usual. It can be shown that the least fixpoint of this monotonic operator
always exists and we set bin unf (P ) := lfp(TPβ ). Then the calls that occur in the left derivations of
P ∪{Q} can be characterized as follows: calls P (Q) = {Bθ|H ← B ∈ bin unf (P ), θ = mgu(Q, H)}.
This last property was one of the main initial motivations of the proposed abstract semantics, enabling logic programs optimizations. Similarly, bin unf (P ) gives a goal independent representation
of the success patterns of P .
But we can extract more information from the binary unfoldings of a program P : universal
left termination of an atomic query Q with respect to P is identical to universal termination of
Q with respect to bin unf (P ). Note that the selection rule is irrelevant for a binary program and
an atomic query, as each subsequent query has at most one atom. The following result lies at the
heart of Codish’s approach to termination:
Theorem 2.1 [7] Let P be a program and Q an atomic query. Then Q left loops with respect to
P iff Q loops with respect to bin unf (P ).
3

Notice that bin unf (P ) is a possibly infinite set of binary clauses. For this reason, in the algorithms
of Section 4, we compute only the first max iterations of TPβ where max is a parameter of the
analysis. As an immediate consequence of Theorem 2.1, assume that we detect that Q loops with
respect to a subset of the binary clauses of TPβ ↑ i, with i ∈ N . Then Q loops with respect to
bin unf (P ) hence Q left loops with respect to P .
Example 2.2 Consider the following program P (see [21], p. 56–58):
p(X,Z) :- p(Y,Z),q(X,Y).

p(X,X).

q(a,b).

The binary unfoldings of P are:
TPβ
TPβ
TPβ
TPβ
TPβ
TPβ

↑0
↑1
↑2
↑3
↑4
↑5

=
=
=
=
=
=

∅
{p(X, Z) ← p(Y, Z), p(X, X) ← true, q(a, b) ← true} ∪ TPβ ↑ 0
{p(a, b) ← true, p(X, Y ) ← q(X, Y )} ∪ TPβ ↑ 1
{p(X, b) ← q(X, a), p(X, Z) ← q(Y, Z)} ∪ TPβ ↑ 2
{p(X, b) ← q(Y, a)} ∪ TPβ ↑ 3
TPβ ↑ 4 = bin unf (P )

Let Q := p(X, b). Note that Q loops w.r.t. TPβ ↑ 1, hence it loops w.r.t. bin unf (P ). So Q left
loops w.r.t. P .


3

Loop Inference Using Filters

In this paper, we propose a mechanism that, given a logic program P , generates at verification
time classes of atomic queries that left loop w.r.t. P . Our approach is completely based on
the binary unfoldings of P and relies on Theorem 2.1. It consists in computing a finite subset
BinProg of bin unf (P ) and then in inferring a set of atomic queries that loop w.r.t. BinProg. By
Theorem 2.1, these queries left loop w.r.t. P .
Hence, we reduce the problem of inferring looping atomic queries w.r.t. a logic program to
that of inferring looping atomic queries w.r.t. a binary program. This is why in the sequel, our
definitions, results and discussions mainly concentrate on binary programs only.
The central point of our method is the subsumption test, as the following lifting lemma,
specialized for the leftmost selection rule, holds:
Lemma 3.1 (One Step Lifting, [1]) Let Q =⇒ Q1 be a left derivation step, Q′ be a query that is
c

more general than Q and c′ be a variant of c variable disjoint with Q′ . Then, there exists a query
Q′1 that is more general than Q1 and such that Q′ =⇒ Q′1 with input clause c′ .
c

From this result, we derive:
Corollary 3.2 Let c := H ← B be a binary clause. If B is more general than H then H loops
w.r.t. {c}.
Corollary 3.3 Let c := H ← B be a clause from a binary program BinProg . If B loops w.r.t.
BinProg then H loops w.r.t. BinProg .
These corollaries provide two sufficient conditions that can be used to design an incremental
bottom-up mechanism that infers looping atomic queries. Given a binary program BinProg , it
suffices to build the set Q of atomic queries consisting of the heads of the clauses whose body is
more general than the head. By Corollary 3.2, the elements of Q loop w.r.t. BinProg. Then, by
Corollary 3.3, the head of the clauses whose body is more general than an element of Q can safely
been added to Q while retaining the property that every query in Q loops w.r.t. BinProg.
Notice that using this technique, we may not detect some looping queries. In [15], the authors
show that there is no algorithm that, when given a right-linear binary recursive clause (i.e. a
4

binary clause p(· · · ) ← p(· · · ) such that all variables occur at most once in the body) and given
an atomic query, always decides in a finite number of steps whether or not the resolution stops. In
the case of a linear atomic query (i.e. an atomic query such that all variables occur at most once)
however, the halting problem of derivations w.r.t. one binary clause is decidable [33, 13, 14].
It can be argued that the condition provided by Corollary 3.2 is rather weak because it fails
at inferring looping queries in some simple cases. This is illustrated by the following example.
Example 3.4 Let c be the clause p(X) ← p(f (X)). We have the infinite derivation:
p(X) =⇒ p(f (X)) =⇒ p(f (f (X))) =⇒ p(f (f (f (X)))) · · ·
c

c

c

But, since the body of c is not more general than its head, Corollary 3.2 does not allow to infer
that p(X) loops w.r.t. {c}.

In this section, we distinguish a special kind of argument positions that are “neutral” for
derivation. Our goal is to extend the relation “is more general than” by, roughly, disregarding the
predicate arguments whose position has been identified as neutral. Doing so, we aim at inferring
more looping queries.
Intuitively, a set of predicate argument positions ∆ is “Derivation Neutral” (DN for short) for
a binary clause c when the following holds. Let Q be an atomic query and Q′ be a query obtained
by replacing by any terms the predicate arguments in Q whose position is in ∆. If Q =⇒ Q1 then
c

Q′ =⇒ Q′1 where Q′1 is more general than Q1 up to the arguments whose position is in ∆.
c

Example 3.5 (Example 3.4 continued) The predicate p has only one argument position, so let
us consider ∆ := hp 7→ {1}i which distinguishes position 1 for predicate p. For any derivation
step p(s) =⇒ p(s1 ) if we replace s by any term t then there exists a derivation step p(t) =⇒ p(t1 ).
c

c

Notice that p(t1 ) is more general than p(s1 ) up to the argument of p. So, by the intuition described
above, ∆ is DN for c. Consequently, as in c the body p(f (X)) is more general than the head p(X)
up to the argument of p which is neutral, by an extended version of Corollary 3.2 there exists an
infinite derivation of {c} ∪ {p(X)}.

Let us give some more concrete examples of DN positions.
Example 3.6 The second argument position of the relation symbol append in the program APPEND:
append([],Ys,Ys).
append([X|Xs],Ys,[X|Zs]) :- append(Xs,Ys,Zs).

% C1
% C2

is DN for C2. Notice that a very common programming technique called accumulator passing
(see for instance e.g. [28], p. 21–25) always produces DN positions. A classical example of the
accumulator passing technique is the following program REVERSE.
reverse(L,R) :- rev(L,[],R).
rev([],R,R).
rev([X|Xs],R0,R) :- rev(Xs,[X|R0],R).

% C1
% C2
% C3

Concerning termination, we may ignore the second and the third argument of rev in the recursive
clause C3 while unfolding a query with this clause. Only the first argument can stop the unfolding.

But we can be even more precise. Instead of only identifying positions that can be totaly
disregarded as in the above examples, we can try to identify positions where we can place any
terms for which a given condition holds.

5

Example 3.7 Consider the clause c := p(f (X)) ← p(f (f (X))). If we mean by a DN position
a position where we can place any terms, then the argument position of p is not DN for c. This
is because, for example, we have the derivation step p(X) =⇒ p(f (f (X1 ))) but if we replace X by
c

g(X) then there is no derivation step of {c} ∪ {p(g(X))}. However, if we mean by a DN position
a position where we can place any instances of f (X), then the argument position of p is DN for
c.

In the sequel of the section, we define more precisely DN positions as positions where we can
place any terms satisfying certain conditions identified by “filters”. We use filters to present an
extension of the relation “is more general than” and we propose an extended version of Corollary 3.2. We offer two syntactic conditions of increasing power for easily identifying DN positions
from mere inspection of the text of a logic program. The practical impact of such filters will be
tackled in Section 5.

3.1

Filters

Let us first introduce the notion of a filter. We use filters in order to distinguish atoms, some
arguments of which satisfy a given condition. A condition upon atom arguments, i.e. terms, can
be defined as a function in the following way.
Definition 3.8 (Term-condition) A term-condition is a function from the set of terms T UL to
{true, false}.
Example 3.9 The following functions are term-conditions.
ftrue : T UL
t

֌ {true, false}
7→ true

f1 : T UL

֌ {true, false}

t
f2 : T UL
t

7→

true iff t is an instance of [X|Y ]

֌ {true, false}
7→

true iff t unifies with h(a, X)


Notice that a term-condition might give distinct results for two terms which are equal modulo
renaming. For instance f2 (X) = false and f2 (Y ) = true. However, in Definition 3.12 below, we
will only consider variant independent term-conditions.
Definition 3.10 (Variant Independent Term-Condition) A term-condition f is variant independent if, for every term t, f (t) = true implies that f (t′ ) = true for every variant t′ of t.
Example 3.11 (Example 3.9 continued) ftrue and f1 are variant independent while f2 is not. 
We restrict the class of term-conditions to that of variant independent ones because we want
to extend the relation “is more general than” so that if an atom A is linked to an atom B by
the extended relation, then every variant of A is also linked to B (see Proposition 3.16 below).
This will be essential to establish the forthcoming main Proposition 3.20 which is an extension of
Corollary 3.2. Now we can define what we exactly mean by a filter.
Definition 3.12 (Filter) A filter, denoted by ∆, is a function from Π such that: for each p ∈ Π,
∆(p) is a partial function from [1, arity(p)] to the set of variant independent term-conditions.
Example 3.13 (Example 3.9 continued) Let p be a relation symbol whose arity equals 3. The
filter ∆ which maps p to the function h1 7→ ftrue , 2 →
7 f1 i and any q ∈ Π \ {p} to hi is noted
∆ := h p 7→ h1 7→ ftrue , 2 7→ f1 i i.

6

3.2

Extension of the Relation “Is More General Than”

Given a filter ∆, the relation “is more general than” can be extended in the following way: an atom
A := p(· · · ) is ∆-more general than B := p(· · · ) if the “is more general than” requirement holds
for those arguments of A whose position is not in the domain of ∆(p) while the other arguments
satisfy their associated term-condition.
Definition 3.14 (∆-more general) Let ∆ be a filter and A and B be two atoms.
• Let η be a substitution. Then A is ∆-more general than B for η if:

A = p(s1 , . . . , sn )



B = p(t1 , . . . , tn )
∀i ∈ [1, n] \ Dom(∆(p)), ti = si η



∀i ∈ Dom(∆(p)), ∆(p)(i)(si ) = true .

• A is ∆-more general than B if there exists a substitution η s.t. A is ∆-more general than B
for η.

An atomic query Q is ∆-more general than an atomic query Q′ if either Q and Q′ are both empty
or Q contains the atom A, Q′ contains the atom B and A is ∆-more general than B.
Example 3.15 (Example 3.13 continued) Let
A := p( b , X , h(a, X) )
B := p( a , [a|b] , X
)
C := p( a , [a|b] , h(Y, b) ) .
Then, A is not ∆-more general than B and C because, for instance, its second argument X is
not an instance of [X|Y ] as required by f1 . On the other hand, B is ∆-more general than A for
the substitution {X/h(a, X)} and B is ∆-more general than C for the substitution {X/h(Y, b)}.
Finally, C is not ∆-more general than A because h(Y, b) is not more general than h(a, X) and C
is not ∆-more general than B because h(Y, b) is not more general than X.

As in a filter the term-conditions are variant independent, we get the following proposition.
Proposition 3.16 Let ∆ be a filter and A and B be two atoms. If A is ∆-more general than B
then every variant of A is ∆-more general than B.
The next proposition states an intuitive result:
Proposition 3.17 Let ∆ be a filter and A and B be two atoms. Then A is ∆-more general than
B if and only if there exists a substitution η such that V ar(η) ⊆ V ar(A, B) and A is ∆-more
general than B for η.

3.3

Derivation Neutral Filters: Operational Definition

In the sequel of this paper, we focus on “derivation neutral” filters. The name “derivation neutral”
stems from the fact that in any derivation of an atomic query Q, the arguments of Q whose position
is distinguished by such a filter can be safely replaced by any terms satisfying the associated termcondition. Such a replacement does not modify the derivation process.
Definition 3.18 (Derivation Neutral) Let ∆ be a filter and c be a binary clause. We say that ∆
is DN for c if for each derivation step Q =⇒ Q1 where Q is an atomic query, for each Q′ that is
c

∆-more general than Q and for each variant c′ of c variable disjoint with Q′ , there exists a query
Q′1 that is ∆-more general than Q1 and such that Q′ =⇒ Q′1 with input clause c′ . This definition
c
is extended to binary programs: ∆ is DN for P if it is DN for each clause of P .
7

Example 3.19 The following examples illustrate the previous definition.
• Let us reconsider the program APPEND from Example 3.6 with the term-condition ftrue defined
in Example 3.9 and the filter ∆ := happend 7→ h2 7→ ftrue ii. ∆ is DN for C2. However, ∆
is not DN for APPEND because it is not DN for C1.
• Consider the following clause:
merge([X|Xs],[Y|Ys],[X|Zs]) :- merge(Xs,[Y|Ys],Zs).
The filter hmerge 7→ h2 7→ f1 ii, where the term-condition f1 is defined in Example 3.9, is
DN for this clause.
In the next subsection, we present some syntactic criteria for identifying correct DN filters. For
proving that the above filters are indeed DN, we will just check that they actually fulfill these
syntactic criteria that are sufficient conditions.

Derivation neutral filters lead to the following extended version of Corollary 3.2 (take ∆ such
that for any p, ∆(p) is a function whose domain is empty):
Proposition 3.20 Let c := H ← B be a binary clause and ∆ be a filter that is DN for c. If B is
∆-more general than H then H loops w.r.t. {c}.
We point out that the above results remain valid when the program under consideration is
restricted to its set of clauses used in the derivation steps. For instance, although the filter ∆ of
Example 3.19 is not DN for APPEND, it will help us to construct queries which loop w.r.t. C2. Such
queries also loop w.r.t. APPEND.
Notice that lifting lemmas are used in the literature to prove completeness of SLD-resolution.
As Definition 3.18 corresponds to an extended version of the One Step Lifting Lemma 3.1, it may
be worth to investigate its consequences from the model theoretic point of view.
First of all, a filter may be used to “expand” atoms by replacing every argument whose position
is distinguished by any term that satisfies the associated term-condition.
Definition 3.21 Let ∆ be a filter and A be an atom. The expansion of A w.r.t. ∆, denoted A↑∆ ,
is the set defined as
def

A↑∆ = {A} ∪ {B ∈ T BL | B is ∆-more general than A for ǫ}
where ǫ denotes the empty substitution.
Notice that in this definition, we do not necessary have the inclusion
{A} ⊆ {B ∈ T BL | B is ∆-more general than A for ǫ} .
For instance, suppose that A := p(f (X)) and that ∆ maps p to the function h1 7→ f i where f is
the term-condition mapping any term t to true iff t is an instance of g(X). Then
{B ∈ T BL | B is ∆-more general than A} = {p(t) | t is an instance of g(X)}
with A 6∈ {p(t) | t is an instance of g(X)}.
Term interpretations in the context of logic programming were first introduced in [6] and further
investigated in [11] and then in [22]. A term interpretation for L is identified with a (possibly
empty) subset of the term base T BL . So, as for atoms, a term interpretation can be expanded by
a filter.
Definition 3.22 Let ∆ be a filter and I be a term interpretation for L. Then I↑∆ is the term
interpretation for L defined as:
def [
I↑∆ =
A↑∆ .
A∈I

8

For any logic program P , we denote by C(P ) its least term model.
Theorem 3.23 Let P be a binary program and ∆ be a DN filter for P . Then C(P )↑∆ = C(P ).
Proof. The inclusion C(P ) ⊆ C(P )↑∆ is straightforward so let us concentrate on the other one
i.e. C(P )↑∆ ⊆ C(P ). Let A′ ∈ C(P )↑∆ . Then there exists A ∈ C(P ) such that A′ ∈ A↑∆ . A well
known result states:
C(P ) = {B ∈ T BL | there exists a successful derivation of P ∪ {B}}

(1)

Consequently, there exists a successful derivation ξ of P ∪{A}. Therefore, by successively applying
Definition 3.18 to each step of ξ, one construct a successful derivation of A′ . So by (1) A′ ∈ C(P ).

3.4

Some Particular DN Filters

In this section, we provide two sufficient syntactic conditions for identifying DN filters.
3.4.1

DN Sets of Positions

The first instance we consider corresponds to filters, the associated term-conditions of which are
all equal to ftrue (see Example 3.9). Within such a context, as the term-conditions are fixed, each
filter ∆ is uniquely determined by the domains of the partial functions ∆(p) for p ∈ Π. Hence the
following definition.
Definition 3.24 (Set of Positions) A set of positions, denoted by τ , is a function from Π to 2N
such that: for each p ∈ Π, τ (p) is a subset of [1, arity(p)].
Example 3.25 Let append and append3 be two relation symbols. Assume that arity(append ) = 3
and arity(append3 ) = 4. Then τ := h append 7→ {2}, append3 7→ {2, 3, 4} i is a set of positions.

Not surprisingly, the filter that is generated by a set of positions is defined as follows.
Definition 3.26 (Associated Filter) Let τ be a set of positions and ftrue be the term-condition
defined in Example 3.9. The filter ∆[τ ] defined as:
for each p ∈ Π, ∆[τ ](p) is the function from τ (p) to {ftrue }
is called the filter associated to τ .
Example 3.27 (Example 3.25 continued) The filter associated to τ is
∆[τ ] :=

happend 7→ h2 7→ ftrue i, append3 7→ h2 7→ ftrue , 3 7→ ftrue , 4 7→ ftrue ii.


Now we define a particular kind of sets of positions. These are named after “DN” because, as
stated by Theorem 3.30 below, they generate DN filters.
Definition 3.28 (DN Set of Positions) Let τ be a set of positions. We say that τ is DN for a
binary clause p(s1 , . . . , sn ) ← q(t1 , . . . , tm ) if:

 si is a variable
si occurs only once in p(s1 , . . . , sn )
∀i ∈ τ (p),

∀j ∈ [1, m], si ∈ V ar(tj ) ⇒ j ∈ τ (q) .

A set of positions is DN for a binary program P if it is DN for each clause of P .

9

The intuition of Definition 3.28 is the following. If for instance we have a clause c :=
p(X, Y, f (Z)) ← p(g(Y, Z), X, Z) then in the first two positions of p we can put any terms and get
a derivation step w.r.t. c because the first two arguments of the head of c are variables that appear
exactly once in the head. Moreover, X and Y of the head reappear in the body but again only in
the first two positions of p. So, if we have a derivation step p(s1 , s2 , s3 ) =⇒ p(t1 , t2 , t3 ), we can rec

place s1 and s2 by any terms s′1 and s′2 and get another derivation step p(s′1 , s′2 , s3 ) =⇒ p(t′1 , t′2 , t′3 )
where t′3 is the same as t3 up to variable names.

c

Example 3.29 (Example 3.25 continued) τ is DN for the program:
append([X|Xs],Ys,[X|Zs]) :- append(Xs,Ys,Zs).
append3(Xs,Ys,Zs,Ts) :- append(Xs,Ys,Us).
which is a subset of the binary unfoldings of the program APPEND3:
append([],Ys,Ys).
append([X|Xs],Ys,[X|Zs]) :- append(Xs,Ys,Zs).
append3(Xs,Ys,Zs,Ts) :- append(Xs,Ys,Us), append(Us,Zs,Ts).

DN sets of positions generate DN filters.
Theorem 3.30 Let τ be a DN set of positions for a binary program P . Then ∆[τ ] is DN for P .
Proof. As we will see in Section 3.4.2, this theorem is a particular case of Theorem 3.39.
Notice that the set of DN sets of positions of any binary program P is not empty because, by
Definition 3.28, τ0 := hp 7→ ∅ | p ∈ Πi is DN for P . Moreover, an atom A is ∆[τ0 ]-more general
than an atom B iff A is more general than B.
3.4.2

DN Sets of Positions with Associated Terms

Now we consider another instance of Definition 3.18. As we will see, it is more general than the
previous one. It corresponds to filters whose associated term-conditions have all the form “is an
instance of t” where t is a term that uniquely determines the term-condition. Notice that such
term-conditions are variant independent, so it makes sense to consider such filters. Hence the
following definition.
Definition 3.31 (Sets of Positions with Associated Terms) A set of positions with associated
terms, denoted by τ + , is a function from Π such that: for each p ∈ Π, τ + (p) is a partial function
from [1, arity(p)] to T UL .
Example 3.32 Let p and q be two relation symbols whose arity is 2. Then
τ + := h p 7→ h2 7→ Xi, q 7→ h2 7→ g(X)i i
is a set of positions with associated terms.



The filter that is generated by a set of positions with associated terms is defined as follows.
Definition 3.33 (Associated Filter) Let τ + be a set of positions with associated terms. The filter
associated to τ + , denoted by ∆[τ + ], is defined as: for each p ∈ Π, ∆[τ + ](p) is the function
Dom(τ + (p))
i

֌ The set of term-conditions
(
T UL ֌ {true, false}
7→
t
7→ true iff t is an instance of τ + (p)(i)
10

Example 3.34 (Example 3.32 continued) The filter associated to τ + is
∆[τ + ] :=
where

f1 : T UL
t
f2 : T UL
t

h p 7→ h2 7→ f1 i, q 7→ h2 7→ f2 i i

֌ {true, false}
7→

true iff t is an instance of X

֌ {true, false}
7→

true iff t is an instance of g(X)


As for sets of positions, we define a special kind of sets of positions with associated terms.
Definition 3.35 (DN Sets of Positions with Associated Terms) Let τ + be a set of positions with
associated terms. We say that τ + is DN for a binary clause p(s1 , . . . , sn ) ← q(t1 , . . . , tm ) if these
conditions hold:
• (DN1) ∀i ∈ Dom(τ + (p)), ∀j ∈ [1, n] \ {i}: V ar(si ) ∩ V ar(sj ) = ∅,
• (DN2) ∀hi 7→ ui i ∈ τ + (p): si is more general than ui ,
• (DN3) ∀hj 7→ uj i ∈ τ + (q): tj is an instance of uj ,
• (DN4) ∀i ∈ Dom(τ + (p)), ∀j 6∈ Dom(τ + (q)): V ar(si ) ∩ V ar(tj ) = ∅.
A set of positions with associated terms is DN for a binary program P if it is DN for each clause
of P .
This definition says that any si where i is in the domain of τ + (p) (i.e. position i is distinguished
by τ + ): (DN1) does not share its variables with the other arguments of the head, (DN2) is more
general than the term ui that i is mapped to by τ + (p), (DN4) distributes its variables to some tj
such that j is in the domain of τ + (q) (i.e. position j is distinguished by τ + ). Moreover, (DN3)
says that any tj , where j is distinguished by τ + , is such that tj is an instance of the term uj that
j is mapped to by τ + (q).
Example 3.36 (Example 3.32 continued) τ + is DN for the following program:
p(f(X),Y) :- q(X,g(X)).
q(a,g(X)) :- q(a,g(b)).
The preceding notion is closed under renaming:
Proposition 3.37 Let c be a binary clause and τ + be a set of positions with associated terms that
is DN for c. Then τ + is DN for every variant of c.
Notice that a set of positions is a particular set of positions with associated terms in the
following sense.
Proposition 3.38 Let τ be a set of positions and X be a variable. Let τ + be the set of positions
with associated terms defined as: for each p ∈ Π, τ + (p) := ( τ (p) ֌ {X} ). Then, the following
holds.
1. An atom A is ∆[τ ]-more general than an atom B iff A is ∆[τ + ]-more general than B.
2. For any binary clause c, τ is DN for c iff τ + is DN for c.
Proof. A proof follows from these remarks.
11

• Item 1 is a direct consequence of the definition of “∆-more general” (see Definition 3.14)
and the definition of the filter associated to a set of positions (see Definition 3.26) and to a
set of positions with associated terms (see Definition 3.33).
• Item 2 is a direct consequence of the definition of DN sets of positions (see Definition 3.28)
and DN sets of positions with associated terms (see Definition 3.35).
The sets of positions with associated terms of Definition 3.35 were named after “DN” because
of the following result.
Theorem 3.39 Let P be a binary program and τ + be a set of positions with associated terms that
is DN for P . Then ∆[τ + ] is DN for P .
As in the case of sets of positions, the set of DN sets of positions with associated terms of any
binary program P is not empty because, by Definition 3.35, τ0+ := hp 7→ hi | p ∈ Πi is DN for
P . Moreover, an atom A is ∆[τ0+ ]-more general than an atom B iff A is more general than B.
Finally, in Appendix A, we give an incremental algorithm (see Section 4.2) that computes a DN
set of positions with associated terms. Its correctness proof is also presented.

3.5

Examples

This section presents some examples where we use filters obtained from DN sets of positions and
DN sets of positions with associated terms to infer looping queries. As the filters we use in each
case are not “empty” (i.e. are not obtained from τ0 or τ0+ ), we are able to compute more looping
queries than using the classical subsumption test.
Example 3.40 Consider the program APPEND that we introduced in Example 3.6. Every infinite
derivation w.r.t. APPEND starting from an atomic query only uses the non-unit clause C2. Therefore, as we aim at inferring looping atomic queries w.r.t. APPEND, we only focus on C2 in the
sequel of this example.
As in C2 the body, which is append (Xs, Ys, Zs), is more general than the head, which is
append ([X |Xs], Ys, [X |Zs]), by Corollary 3.2 we have that the query append ([X |Xs], Ys, [X |Zs])
loops w.r.t. {C2}. Consequently, by the One Step Lifting Lemma 3.1, each query that is more
general than append ([X |Xs], Ys, [X |Zs]) also loops w.r.t. {C2}.
But we can be more precise than that. According to Definition 3.28, τ := h append 7→ {2} i
is a DN set of positions for {C2}. The filter associated to τ (see Definition 3.26) is ∆[τ ] :=
h append 7→ h2 7→ ftrue i i. By Theorem 3.30, ∆[τ ] is a DN filter for {C2}. Consequently, by
Definition 3.18, each query that is ∆[τ ]-more general than append ([X |Xs], Ys, [X |Zs]) loops w.r.t.
{C2}. This means that


t2 is any term and
append (t1 , t2 , t3 ) ∈ TB L
t1 , t3 is more general than [X |Xs], [X |Zs]
is a set of atomic queries that loop w.r.t. {C2}, hence w.r.t. APPEND. This set includes the ’welltyped’ query append (As, [ ], Bs).

Example 3.41 Consider the program REVERSE that was introduced in Example 3.6. As in the
example above, in order to infer looping atomic queries w.r.t. REVERSE, we only focus on the
non-unit clauses C1 and C3 in the sequel of this example. More precisely, we process the relation
symbols of the program in a bottom-up way, so we start the study with clause C3 and end it with
clause C1.
According to Definition 3.28, τ := h rev 7→ {2, 3} i is a DN set of positions for {C3}. The
filter associated to τ (see Definition 3.26) is ∆[τ ] := h rev 7→ h2 7→ ftrue , 3 7→ ftrue i i. By
Theorem 3.30, ∆[τ ] is DN for {C3}. As rev (Xs, [X |R0 ], R) (the body of C3) is ∆[τ ]-more general
than rev ([X |Xs], R0 , R) (the head of C3), by Proposition 3.20 we get that rev ([X |Xs], R0 , R) loops
w.r.t. {C3}. Notice that, unlike the example above, here we do not get this result from Corollary 3.2
12

as rev (Xs, [X |R0 ], R) is not more general than rev ([X |Xs], R0 , R). Finally, as ∆[τ ] is DN for
{C3}, by Definition 3.18 we get that each query that is ∆[τ ]-more general than rev ([X |Xs], R0 , R)
loops w.r.t. {C3}, hence w.r.t. REVERSE. This means that


t2 and t3 are any terms and
Q := rev (t1 , t2 , t3 ) ∈ TB L
t1 is more general than [X |Xs]
is a set of atomic queries that loop w.r.t. REVERSE. This set includes the ’well-typed’ query
rev (As, [ ], [ ]).
Now, consider clause C1. As rev (L, [], R) (its body) is an element of Q, then rev (L, [], R) loops
w.r.t. {C3}, hence w.r.t. {C1, C3}. Consequently, by Corollary 3.3, reverse(L, R) (the head of C1)
loops w.r.t. {C1, C3}. Let τ ′ := h rev 7→ {2, 3}, reverse 7→ {2} i. By Definition 3.28, τ ′ is DN for
{C1, C3}, so ∆[τ ′ ] is DN for {C1, C3}. Consequently, each query that is ∆[τ ′ ]-more general than
reverse(L, R) also loops w.r.t. {C1, C3} hence w.r.t. REVERSE. This means that

reverse(X, t) ∈ TB L | X is a variable and t is any term
is a set of atomic queries that loop w.r.t. REVERSE. This set includes the ’well-typed’ query
reverse(As, [ ]).


Example 3.42 Consider the two recursive clauses of the program MERGE where we have removed
the inequalities:
merge([X|Xs],[Y|Ys],[X|Zs]) :- merge(Xs,[Y|Ys],Zs). % C3
merge([X|Xs],[Y|Ys],[Y|Zs]) :- merge([X|Xs],Ys,Zs). % C4
Every set of positions τ that is DN for {C3} is such that τ (merge) = ∅ because each argument
of the head of C3 is not a variable (see Definition 3.28). Hence, using Proposition 3.20 with
a filter obtained from a DN set of positions leads to the same results as using Corollary 3.2:
as merge(Xs, [Y |Ys], Zs) is more general than merge([X |Xs], [Y |Ys], [X |Zs]), by Corollary 3.2
merge([X |Xs], [Y |Ys], [X |Zs]) loops w.r.t. {C3}. So, by the One Step Lifting Lemma 3.1, each
query that is more general than merge([X |Xs], [Y |Ys], [X |Zs]) also loops w.r.t. {C3}, hence w.r.t.
MERGE.
But we can be more precise than that. According to Definition 3.35, τ + := hmerge 7→ h2 7→
[Y |Ys]i i is a set of positions with associated terms that is DN for {C3}. Hence, by Theorem 3.39,
the associated filter ∆[τ + ] (see Definition 3.33) is DN for {C3}. So, by Definition 3.18, each query
that is ∆[τ + ]-more general than merge([X |Xs], [Y |Ys], [X |Zs]) loops w.r.t. {C3}. This means that


t is any instance of [Y |Ys] and
merge(t1 , t2 , t3 ) ∈ TB L 2
t1 , t3 is more general than [X |Xs], [X |Zs]
is a set of atomic queries that loop w.r.t. MERGE. Notice that this set includes the ’well-typed’ query
merge(As, [0], Bs). Finally, let us turn to clause C4. Reasoning exactly as above with the set of
positions with associated terms hmerge 7→ h1 7→ [X |Xs]i i which is DN for {C4}, we conclude that:


t1 is any instance of [X |Xs] and
merge(t1 , t2 , t3 ) ∈ TB L
t2 , t3 is more general than [Y |Ys], [Y |Zs]
is a set of atomic queries that loop w.r.t. MERGE. Notice that this set includes the ’well-typed’ query
merge([0], As, Bs).


4

Algorithms

We have designed a set of correct algorithms for full automation of non-termination analysis of
logic programs. These algorithms are given in Appendix A with their correctness proofs. In this
section, we present the intuitions and conceptual definitions underlying our approach.
13

4.1

Loop Dictionaries

Our technique is based on a data structure called dictionary which is a set of pairs (BinSeq, τ + )
where BinSeq is a finite ordered sequence of binary clauses and τ + is a set of positions with
associated terms. In the sequel, we use the list notation of Prolog and a special kind of dictionaries
that we define as follows.
Definition 4.1 (Looping Pair, Loop Dictionary) A pair (BinSeq, τ + ), where the list BinSeq is a
finite ordered sequence of binary clauses and τ + is a set of positions with associated terms, is a
looping pair if τ + is DN for BinSeq and:
• either BinSeq = [H ← B] and B is ∆[τ + ]-more general than H,
• or BinSeq = [H ← B, H1 ← B1 | BinSeq 1 ] and there exists a set of positions with associated
terms τ1+ such that ([H1 ← B1 | BinSeq 1 ], τ1+ ) is a looping pair and B is ∆[τ1+ ]-more general
than H1 .
A loop dictionary is a finite set of looping pairs.
Example 4.2 The pair (BinSeq := [H1 ← B1 , H2 ← B2 , H3 ← B3 ], τ1+ ) where
H1 ← B1 := r(X) ← q(X, f (f (X)))
H2 ← B2 := q(X, f (Y )) ← p(f (X), a)
H3 ← B3 := p(f (g(X)), a) ← p(X, a)
and τ1+ := hp 7→ h2 7→ ai, q 7→ h2 7→ f (X)ii is a looping pair:
• Let τ3+ := hp 7→ h2 7→ aii. Then τ3+ is a DN set of positions with associated terms for
[H3 ← B3 ]. Moreover, B3 is ∆(τ3+ )-more general than H3 . Consequently, ([H3 ← B3 ], τ3+ )
is a looping pair.
• Notice that B2 is ∆(τ3+ )-more general than H3 . Now, let τ2+ := τ1+ . Then τ2+ is DN for
[H2 ← B2 , H3 ← B3 ]. So, ([H2 ← B2 , H3 ← B3 ], τ2+ ) is a looping pair.
• Finally, notice that B1 is ∆(τ2+ )-more general than H2 . As τ1+ is DN for BinSeq, we conclude
that (BinSeq, τ1+ ) is a looping pair.

A looping pair immediately provides an atomic looping query. It suffices to take the head of
the first clause of the binary program of the pair:
Proposition 4.3 Let ([H ← B|BinSeq], τ + ) be a looping pair. Then H loops with respect to
[H ← B|BinSeq].
Proof. By induction on the length of BinSeq using Proposition 3.20, Corollary 3.3 and Theorem 3.39. So, a looping pair denotes a proof outline for establishing that H left loops. Moreover,
looping pairs can be built incrementally in a simple way as described below.

4.2

Computing a Loop Dictionary

Given a logic program P and a positive integer max , the function infer loop dict from Appendix A first computes TPβ ↑ max (the first max iterations of the operator TPβ ), which is a
finite subset of bin unf (P ). Then, using the clauses of TPβ ↑ max , it incrementally builds a loop
dictionary Dict as follows.
At start, Dict is set to ∅. Then, for each clause H ← B in TPβ ↑ max , the following actions
are performed.
• infer loop dict tries to extract from H ← B the most simple form of a looping pair: it
computes a set of positions with associated terms τ + that is DN for H ← B, then it tests if
B is ∆[τ + ]-more general than H. If so, the looping pair ([H ← B], τ + ) is added to Dict .
14

• infer loop dict tries to combine H ← B to some looping pairs that have already been
added to Dict in order to build other looping pairs. For each ([H1 ← B1 |BinSeq 1 ], τ1+ ) in
Dict, if B is ∆[τ1+ ]-more general than H1 , then a set of positions with associated terms
τ + that is DN for [H ← B, H1 ← B1 |BinSeq 1 ] is computed and the looping pair ([H ←
B, H1 ← B1 |BinSeq 1 ], τ + ) is added to Dict .
Notice that in the second step above, we compute τ + that is DN for [H ← B, H1 ← B1 |BinSeq 1 ].
As we already hold τ1+ that is DN for [H1 ← B1 |BinSeq 1 ], it is more interesting, for efficiency
reasons, to compute τ + from τ1+ instead of starting from the ground. Indeed, starting from τ1+ ,
one uses the information stored in τ1+ about the program [H1 ← B1 |BinSeq 1 ], which may speed
up the computation substantially. This is why we have designed a function dna that takes two
arguments as input, a binary program BinProg and a set of positions with associated terms τ + . It
computes a set of positions with associated terms that is DN for BinProg and that refines τ + . On
+
the other hand, the function unit loop calls dna with τmax
which is the initial set of positions with
+
+
associated terms defined as follows: Dom(τmax (p)) = [1, arity(p)] for each p ∈ Π and τmax
(p)(i) is
a variable for each i ∈ [1, arity(p)].
Example 4.4 Consider the program APPEND3
append3(Xs,Ys,Zs,Us) :- append(Xs,Ys,Vs), append(Vs,Zs,Us).
β
augmented with the APPEND program. The set TAPPEND3
↑ 2 includes:

append([A|B],C,[A|D]) :- append(B,C,D).
append3(A,B,C,D) :- append(A,B,E).
append3([],A,B,C) :- append(A,B,C).

% BC1
% BC2
% BC3

From clause BC1 we get the looping pair (BinSeq 1 , τ1+ ) where


BinSeq 1 = append ([X1 |X2 ], X3 , [X1 |X4 ]) ← append (X2 , X3 , X4 )

and τ1+ (append ) = h2 7→ X3 i. From this pair and the clause BC2, we get the looping pair
(BinSeq 2 , τ2+ ) where:

BinSeq 2 =
append3 (X1 , X2 , X3 , X4 ) ← append (X1 , X2 , X5 ),

append ([X1 |X2 ], X3 , [X1 |X4 ]) ← append (X2 , X3 , X4 )

and τ2+ (append ) = h2 7→ X3 i and τ2+ (append3 ) = h2 7→ X2 , 3 7→ X3 , 4 7→ X4 i.
Finally, from (BinSeq 1 , τ1+ ) and BC3, we get the looping pair (BinSeq 3 , τ3+ ) where:

BinSeq 3 =
append3 ([], X1 , X2 , X3 ) ← append (X1 , X2 , X3 ),

append ([X1 |X2 ], X3 , [X1 |X4 ]) ← append (X2 , X3 , X4 )

and τ3+ (append ) = h2 7→ X3 i and τ3+ (append3 ) = h3 7→ X2 i.
Example 4.5 Consider the program PERMUTE:
delete(X,[X|Xs],Xs).
delete(Y,[X|Xs],[X|Ys]) :- delete(Y,Xs,Ys).

permute([],[]).
permute([X|Xs],[Y|Ys]) :- delete(Y,[X|Xs],Zs), permute(Zs,Ys).
β
The set TPERMUTE
↑ 1 includes:

15



delete(B,[C|D],[C|E]) :- delete(B,D,E).
permute([B|C],[D|E]) :- delete(D,[B|C],F).

% BC1
% BC2

From clause BC1 we get the looping pair (BinSeq 1 , τ1+ ) where


BinSeq 1 = delete(X1 , [X2 |X3 ], [X2 |X4 ]) ← delete(X1 , X3 , X4 )

and τ1+ (delete) = h1 7→ X1 i. From this pair and BC2, we get the looping pair (BinSeq 2 , τ2+ ) where:

BinSeq 2 =
permute([X1 |X2 ], [X3 |X4 ]) ← delete(X3 , [X1 |X2 ], X5 ),
delete(X1 , [X2 |X3 ], [X2 |X4 ]) ← delete(X1 , X3 , X4 )

and τ2+ (delete) = h1 7→ X1 i and τ2+ (permute) = h2 7→ [X3 |X4 ]i.

4.3



Looping Conditions

One of the main purposes of this article is the inference of classes of atomic queries that left loop
w.r.t. a given logic program. Classes of atomic queries we consider are defined by pairs (A, τ + )
where A is an atom and τ + is a set of positions with associated terms. Such a pair denotes the
set of queries A↑τ + , the definition of which is similar to that of the expansion of an atom, see
Definition 3.21.
Definition 4.6 Let A be an atom and τ + be a set of positions with associated terms. Then A↑τ +
denotes the class of atomic queries defined as:
def

A↑τ + = {A} ∪ {B ∈ T BL | B is ∆[τ + ]-more general than A} .
Once each element of A↑τ + left loops w.r.t. a logic program, we get what we call a looping
condition for that program:
Definition 4.7 (Looping Condition) Let P be a logic program. A looping condition for P is a
pair (A, τ + ) such that each element of A↑τ + left loops w.r.t. P .
The function infer loop cond takes as arguments a logic program P and a non-negative
integer max . Calling infer loop dict(P, max ), it first computes a loop dictionary Dict . Then,
it computes from Dict looping conditions for P as follows. The function extracts the pair (H, τ + )
from each element ([H ← B|BinSeq], τ + ) of Dict . By Proposition 4.3, H loops w.r.t. [H ←
B|BinSeq]. As τ + , hence ∆[τ + ], is DN for [H ← B|BinSeq], by Definition 3.18 each element of
H↑τ + loops w.r.t. [H ← B|BinSeq]. Finally, as [H ← B|BinSeq] ⊆ TPβ ↑ max ⊆ bin unf (P ), by
Theorem 2.1, each element of H↑τ + left loops w.r.t. P .
Example 4.8 (Example 4.4 continued) From each looping pair we have infered, we get the following information.
• (append ([X1 |X2 ], X3 , [X1 |X4 ]), τ1+ ) is a looping condition. So, each query append (t1 , t2 , t3 ),
where [X1 |X2 ] = t1 η and [X1 |X4 ] = t3 η for a substitution η and t2 is an instance of X3
(because τ1+ (append )(2) = X3 ), left loops w.r.t. APPEND3. In other words, each query
append (t1 , t2 , t3 ), where [X1 |X2 ] = t1 η and [X1 |X4 ] = t3 η for a substitution η and t2 is
any term, left loops w.r.t. APPEND3.
• (append3 (X1 , X2 , X3 , X4 ), τ2+ ) is a looping condition. As we have τ2+ (append3 )(2) = X2 ,
τ2+ (append3 )(3) = X3 and τ2+ (append3 )(4) = X4 , this means that each query of form
append3 (x1 , t2 , t3 , t4 ), where t2 , t3 and t4 are any terms, left loops w.r.t. APPEND3.
• (append3 ([], X1 , X2 , X3 ), τ3+ ) is a looping condition. So, as τ3+ (append3 )(3) = X2 , this
means that each query of form append3 ([], X1 , t, X3 ), where t is any term, left loops w.r.t.
APPEND3.

16

Example 4.9 (Example 4.5 continued) From each looping pair we have infered, we get the following information.
• (delete(X1 , [X2 |X3 ], [X2 |X4 ]), τ1+ ) is a looping condition. As τ1+ (delete)(1) = X1 , this means
that each query of form delete(t1 , t2 , t3 ), where t1 is any term and [X2 |X3 ] = t2 η and
[X2 |X4 ] = t3 η for a substitution η, left loops w.r.t. PERMUTE.
• (permute([X1 |X2 ], [X3 |X4 ]), τ2+ ) is a looping condition. As τ2+ (permute)(2) = [X3 |X4 ], this
means that each query of form permute(t1 , t2 ), where t1 is more general than [X1 |X2 ] and
t2 is any instance of [X3 |X4 ], left loops w.r.t. PERMUTE.


5

An Application: Proving Optimality of Termination Conditions

[26] presents a tool for inferring termination conditions that are expressed as multi-modes, i.e.
as disjunctions of conjunctions of propositions of form “the i-th argument is ground”. In this
section, we describe an algorithm that attempts proofs of optimality of such conditions using the
algorithms for non-termination inference of the previous section.

5.1

Optimal Terminating Multi-modes

Let P be a logic program and p ∈ ΠP be a relation symbol, with arity(p) = n. First, we describe
the language we use for abstracting sets of atomic queries:
Definition 5.1 (Mode) A mode mp for p is a subset of [1, n], and denotes the following set of
atomic goals: [mp ] = {p(t1 , . . . , tn ) ∈ TB L | ∀i ∈ mp Var (ti ) = ∅}. The set of all modes for p,
i.e. 2[1,n] , is denoted modes(p).
Note that if mp = ∅ then [mp ] = {p(t1 , . . . , tn ) ∈ TB L }. Since a logic procedure may have
multiple uses, we generalize:
Definition 5.2 (Multi-mode) A multi-mode Mp for p is a finite set of modes for p and denotes
the following set of atomic queries: [Mp ] = ∪m∈Mp [m].
Note that if Mp = ∅, then [Mp ] = ∅. Now we can define what we mean by terminating and
looping multi-modes:
Definition 5.3 (Terminating mode, terminating multi-mode) A terminating mode mp for p is a
mode for p such that any query in [mp ] left terminates w.r.t. P . A terminating multi-mode TM p
for p is a finite set of terminating modes for p.
Definition 5.4 (Looping mode, looping multi-mode) A looping mode mp for p is a mode for p
such that there exists a query in [mp ] which left loops w.r.t. P . A looping multi-mode LM p for p
is a finite set of looping modes for p.
As left termination is instantiation-closed, any mode that is “below” (less general than) a
terminating mode is also a terminating mode. Similarly, as left looping is generalization-closed,
any mode that is “above” (more general than) a looping mode is also a looping mode. Let us be
more precise:
Definition 5.5 (Less general, more general) Let Mp be a multi-mode for the relation symbol p.
We set:
less general (Mp ) =
more general (Mp ) =

{m ∈ modes(p) | ∃m′ ∈ Mp [m] ⊆ [m′ ]}
{m ∈ modes(p) | ∃m′ ∈ Mp [m′ ] ⊆ [m]}

17

looping modes(L, p):
in: L: a finite set of looping conditions
p: a predicate symbol
out: a looping multi-mode for p
1: LM p := ∅
2: for each (p(t1 , . . . , tn ), τ + ) ∈ L do
3:
mp := Dom(τ + (p)) ∪ {i ∈ [1, n] | Var (ti ) = ∅}
4:
LM p := LM p ∪ {mp }
5: return LM p
Figure 1:
We are now equipped to present a definition of optimality for terminating multi-modes:
Definition 5.6 (Optimal terminating multi-mode) A terminating multi-mode TM p for p is optimal if there exists a looping multi-mode LM p verifying:
modes(p) = less general (TM p ) ∪ more general (LM p )
Otherwise stated, given a terminating multi-mode TM p , if each mode which is not less general
than a mode of TM p is a looping mode, then TM p characterizes the operational behavior of p
w.r.t. left termination and our language for defining sets of queries.
Example 5.7 Consider the program APPEND. A well-known terminating multi-mode is the set
TM append = {{1}, {3}}. Indeed, any query of the form append(t,Ys,Zs) or append(Xs,Ys,t),
where t is a ground term ( i.e. such that Var(t) = ∅), left terminates. We have:
less general (TM append ) = {{1}, {3}, {1, 2}, {1, 3}, {2, 3}, {1, 2, 3}}
On the other hand, append(Xs,[],Zs) left loops. Hence LM append = {{2}} is a looping condition
and more general (LM append ) = {∅, {2}}.
Since modes(append ) = less general (TM append ) ∪ more general (LM append ), we conclude that
the terminating multi-mode TM append is optimal.


5.2

Algorithms

Suppose we hold a finite set L of looping conditions for P . Then, each element (p(t1 , . . . , tn ), τ + )
of L provides an obvious looping mode for p: it suffices to take {i ∈ [1, n] | Var(ti ) = ∅}. But
actually, we can extract more information from L. Let p(t′1 , . . . , t′n ) be an atom such that:
• for each hi 7→ ui i ∈ τ + (p), t′i is a ground instance of ui ,
• for each i in [1, n] \ Dom(τ + (p)), t′i = ti .
Then, p(t′1 , . . . , t′n ) belongs to p(t1 , . . . , tn )↑τ + , hence it left loops w.r.t. P . Consequently, we
have that Dom(τ + (p)) ∪ {i ∈ [1, n] | Var (ti ) = ∅} is a looping mode for p. The function
looping modes of Fig. 1 is an application of these remarks.
Now we have the essential material for the design of a tool that attempts proofs of optimality
of left terminating multi-modes computed by a termination inference tool as e.g. cTI [26] or
TerminWeb [17]. For each pair (p, ∅) in the set the function optimal tc of Fig. 2 returns, we can
conclude that the corresponding TM p is the optimal terminating multi-mode which characterizes
the operational behavior of p with respect to Lterm .

18

optimal tc(P , max , {TM p }p∈ΠP ):
in: P : a logic program
max : a non-negative integer
{TM p }p∈ΠP : a finite set of terminating multi-modes
out: a finite set of pairs (p, Mp ) such that p ∈ ΠP and
Mp is a multi-mode for p with no information w.r.t. its left behaviour
note: if for each p ∈ Πp , Mp = ∅, then {TM p }p∈ΠP is optimal
1:
2:
3:
4:
5:
6:
7:

Res := ∅
L := infer loop cond(P, max )
for each p ∈ ΠP do
LM p := looping modes(L, p)
Mp := modes(p) \ (less general(TM p ) ∪ more general(LM p ))
Res := Res ∪ {(p, Mp )}
return Res
Figure 2:

Example 5.8 (Example 4.8 continued) We apply our algorithm to the program APPEND3 of Example 4.4. We get that
L := { (append ([X1 |X2 ], X3 , [X1 |X4 ]),
(append3 (X1 , X2 , X3 , X4 ),
(append3 ([], X1 , X2 , X3 ),

τ1+ ),
τ2+ ),
τ3+ )

}

is a finite set of looping conditions for APPEND3 (see Example 4.8) with
Dom(τ1+ (append ))

=

{2}

Dom(τ2+ (append3 )) =

{2, 3, 4}

Dom(τ3+ (append3 ))

{3}

=

So, for append we have:
LM append :=
more general(LM append ) =

looping modes(L, append ) = {{2}}
{∅, {2}}

TM append
less general(TM append )

=
=

{{1}, {3}}
{{1}, {3}, {1, 2}, {1, 3}, {2, 3}, {1, 2, 3}}

Mappend

=

{}

For append3 , we get:
• the looping mode {2, 3, 4} from (append3 (X1 , X2 , X3 , X4 ), τ2+ ) and
• the looping mode mp := {1, 3} from (append3 ([], X1 , X2 , X3 ), τ3+ ) (notice that 3 ∈ mp because
Dom(τ3+ (append3 )) = {3} and 1 ∈ mp because of constant [] which is the first argument of
append3 ([], X1 , X2 , X3 ).)

19

So, we have:
LM append3 :=
more general(LM append3 ) =

looping modes(L, append3 ) = {{2, 3, 4}, {1, 3}}
{∅, {1}, {2}, {3}, {4}, {1, 3}, {2, 3}, {2, 4},
{3, 4}, {2, 3, 4}}

TM append3
less general(TM append3 )
Mappend3

=
=

{{1, 2}, {1, 4}}
{{1, 2}, {1, 4}, {1, 2, 3}, {1, 2, 4}, {1, 3, 4},

=

{1, 2, 3, 4}}
{}

Hence in both cases, we have characterized the left behaviour of the predicates by using two complementary tools.


5.3

An Experimental Evaluation

We have implemented1 the algorithms presented in Sections 4 and 5.2. The binary unfoldings
algorithm is derived from the one described in [7], where we added time stamps to precisely
control what is computed at each iteration. Looping modes are computed starting from the leaves
of the call graph then moving up to its roots. The cTI termination inference tool2 is detailed in
[26, 24]. Here is the configuration we used for this experiment: Intel 686, 2.4GHz, 512Mb, Linux
2.4, SICStus Prolog 3.10.1, 24.8 MLips. Timings in seconds are average over 10 runs.
First we have applied them on some small programs from standard benchmarks of the termination analysis literature [30, 2, 9] (predefined predicates were erased). The column opt? of Table
1 indicates whether the result of cTI (see [26]) is proved optimal (X) or not (? ). The column
max gives the least non-negative integer implying optimality or the least non-negative integer n
where it seems we get the most precise information from non-termination inference (i.e. for n and
n + 1, the analyser delivers the same results). Then timings in seconds (t[s]) appear, followed by
a pointer to a comment to the notes below.
Notes:
1. The predicate fold/3 is defined by:
fold(X,[],X).
fold(X,[Y|Ys],Z) :- op2(X,Y,V), fold(V,Ys,Z).
When the predicate op2/3 is defined by the fact op2(A,B,C), the result of cTI is optimal.
When the predicate op2/3 is defined by the fact op2(a,b,c), no looping mode is found and
the result of cTI is indeed sub-optimal as the query fold(X,Y,Z) terminates.
2. Termination proofs for mergesort require the list-size norm, while cTI applies the term-size
norm.
3. The result of cTI is not optimal. The analyzed program:
p(A,B) :- q(A,C),p(C,B).
p(A,A).
q(a,b).
has finite binary unfoldings because there is no function symbol. Hence its termination is
decidable (see [7]). This could be easily detected at analyze time. We notice that no looping
mode is found. But as any constant is mapped to 0 by the term-size norm, the modes
modes(p) remain undecided for cTI while they all terminate.
1 Available
2 Available

from http://www.univ-reunion.fr/~gcc
from http://www.cs.unipr.it/cTI

20

Table 1: Some De Schreye’s, Apt’s, and Plümer’s programs.
program
permute
duplicate
sum
merge
dis-con
reverse
append
list
fold
lte
map
member
mergesort
mergesort ap
naive rev
ordered
overlap
permutation
quicksort
select
subset
sum peano
pl2.3.1
pl3.5.6
pl4.4.6a
pl4.5.2
pl4.5.3a
pl5.2.2
pl7.2.9
pl7.6.2a
pl7.6.2b
pl7.6.2c
pl8.3.1a
pl8.4.1
pl8.4.2

top-level predicate
permute(X,Y)
duplicate(X,Y)
sum(X,Y,Z)
merge(X,Y,Z)
dis(X)
reverse(X,Y,Z)
append(X,Y,Z)
list(X)
fold(X,Y,Z)
goal
map(X,Y)
member(X,Y)
mergesort(X,Y)
mergesort ap(X,Y,Z)
naive rev(X,Y)
ordered(X)
overlap(X,Y)
permutation(X,Y)
quicksort(X,Y)
select(X,Y,Z)
subset(X,Y)
sum(X,Y,Z)
p(X,Y)
p(X)
perm(X,Y)
s(X,Y)
p(X)
turing(X,Y,Z,T)
mult(X,Y,Z)
reach(X,Y,Z)
reach(X,Y,Z,T)
reach(X,Y,Z,T)
minsort(X,Y)
even(X)
e(X,Y)

cTI
term-cond
X
X ∨Y
X ∨Y ∨Z
(X ∧ Y ) ∨ Z
X
X
X ∨Z
X
Y
1
X ∨Y
Y
0
Z
X
X
X ∧Y
X
X
Y ∨Z
X ∧Y
Y ∨Z
0
X
X
0
0
0
X ∧Y
0
0
Z∧T
X
X
X

21

t[s]
0.01
0.01
0.01
0.02
0.02
0.02
0.01
0.01
0.01
0.01
0.01
0.01
0.04
0.08
0.02
0.01
0.01
0.03
0.05
0.01
0.01
0.01
0.01
0.01
0.02
0.03
0.01
0.08
0.02
0.02
0.02
0.02
0.03
0.02
0.05

opt?
X
X
X
X
X
X
X
X
?
X
X
X
?
?
X
X
X
X
X
X
X
X
?
X
X
X
X
?
X
?
?
?
X
X
X

Optimal
max
t[s]
1
0.01
1
0.01
1
0.01
1
0.01
2
0.01
1
0.01
1
0.01
1
0.01
2
0.01
1
0.01
2
0.01
1
0.01
2
0.01
2
0.02
1
0.01
1
0.01
2
0.01
1
0.01
1
0.01
1
0.01
2
0.01
1
0.01
1
0.01
2
0.01
1
0.01
1
0.01
1
0.01
2
0.03
4
0.03
1
0.01
1
0.01
2
0.02
2
0.02
2
0.01
3
0.04

cf.

note 1

note 2

note 3

note 4
note 5
note 6

Table 2: Some middle-sized programs.
program
name
ann
bid
boyer
browse
credit
peephole
plan
qplan
rdtok
read
warplan

clauses
177
50
136
30
57
134
29
148
55
88
101

cTI
Q%
48
100
84
53
100
88
100
61
44
52
32

t[s]
1.00
0.14
0.30
0.26
0.11
1.08
0.11
1.13
0.65
1.72
0.49

max=1
Opt%
t[s]
46
0.14
55
0.02
80
0.03
46
0.03
91
0.02
23
0.06
68
0.02
50
0.11
44
0.11
39
0.04
37
0.07

Optimal
max=2
Opt%
t[s]
68
1.34
90
0.08
96
0.22
80
0.18
95
0.11
70
3.62
81
0.09
79
1.60
88
40.2
47
0.80
83
0.99

max=3
Opt%
t[s]
74
32.4
95
0.50
100
3.66
100
6.05
100
4.46
70
406
81
0.37
81
1911
?
> 3600
47
10.9
91
21.5

4. The analyzed program (from [30], p. 64) simulates a Turing machine. The result of cTI is
optimal.
5. With respect to the program:
mult(0,A,0).
mult(s(A),B,C) :- mult(A,B,D),add(D,B,C).
add(0,A,A).
add(s(A),B,s(C)) :- add(A,B,C).

the query mult(s(s(0)),A,B) is automatically detected as looping, although mult(0,A,B)
and mult(s(0),A,B) do terminate.
6. These three programs propose various definitions of the reachability relation between two
nodes in a list of edges. For the first and the third definition, cTI is indeed optimal. For the
second one, cTI is not optimal.
Next, we have applied the couple of analyzers to some middle-sized Prolog programs, see Table
2. Again, predefined predicates were all erased, while they are usually taken into account for cTI
which of course improves the analysis. In other words, we only consider the logic programming
skeleton of each program. The first two columns give the name of the file and its size (number of
clauses). The fourth column indicates the running time (in seconds) of the termination analysis,
while the third column is the ratio of predicates for which a non-false termination condition is
computed over the total number of predicates defined in the program. For instance, cTI is able
to show that there is at least one terminating mode for 48% of the predicates defined in the
program ann. We ran the non-termination analyzer with 1 ≤ max ≤ 3 iterations. For each value
of max, we give the running time (in seconds) and the ratio of predicates for which looping modes
complement terminating modes. For example, with respect to the program ann, for max = 2 we
get the full complete mode termination behavior of 68% of all the defined predicates.
We note that when we increase max, we obtain better results but the running times also
increase, which is fairly obvious. For max = 3, we get good to optimal results but the binary
unfoldings approach reveals its potentially explosive nature: we aborted the analysis of rdtok
after one hour of computation.
In conclusion, from such a naive implementation, we were rather surprised by the quality of the
combined analysis. Adopting some more clever implementation schemes, for instance computing
the binary unfoldings in a demand driven fashion, could be investigated to improve the running
times.
22

6

Related Works

Some extensions of the Lifting Theorem with respect to infinite derivations are presented in [18],
where the authors study numerous properties of finite failure. The non-ground finite failure set
of a logic program is defined as the set of possibly non-ground atoms which admit a fair finitely
failed SLD-tree w.r.t. the program. This denotation is shown correct in the following sense. If two
programs have the same non-ground finite failure set, then any ground or non-ground goal which
finitely fails w.r.t. one program also finitely fails w.r.t. the other. Such a property is false when we
consider the standard ground finite failure set. The proof of correctness of the non-ground finite
failure semantics relies on the following result. First, a derivation is called non-perpetual if it is
a fair infinite derivation and there exists a finite depth from which unfolding does not instantiate
the original goal any more. Then the authors define the definite answer goal of a non-perpetual
derivation as the maximal instantiation of the original goal. A crucial lemma states that any
instance of the definite answer goal admits a similar non-perpetual derivation. Compared to our
work, note that we do not need fairness as an hypothesis for our results. On the other hand,
investigating the relationships between non-ground arguments of the definite answer and neutral
arguments is an interesting problem.
In [35], the authors present a dynamic approach to characterize (in the form of a necessary
and sufficient condition) termination of general logic programs. Their technique employs some
key dynamic features of an infinite generalized SLDNF-derivation, such as repetition of selected
subgoals and recursive increase in term size.
Loop checking in logic programming is also a subject related to our work. In this area, [5] sets
up some solid foundations. A loop check is a device to prune derivations when it seems appropriate.
A loop checker is defined as sound if no solution is lost. It is complete if all infinite derivations
are pruned. A complete loop check may also prune finite derivations. The authors show that even
for function-free programs (also known as Datalog programs), sound and complete loop checks are
out of reach. Completeness is shown only for some restricted classes of function-free programs.
We now review loop checking in more details. To our best knowledge, among all existing
loop checking mechanisms only OS-check [32], EVA-check [34] and VAF-check [36] are suitable for
logic programs with function symbols. They rely on a structural characteristic of infinite SLDderivations, namely, the growth of the size of some generated subgoals. This is what the following
theorem states.
Theorem 6.1 Consider an infinite SLD-derivation ξ where the leftmost selection rule is used.
Then there are infinitely many queries Qi1 , Qi2 , . . . (with i1 < i2 < . . . ) in ξ such that for
any j ≥ 1, the selected atom Aij of Qij is an ancestor of the selected atom Aij+1 of Qij+1 and
size(Aij+1 ) ≥ size(Aij ).
Here, size is a given function that maps an atom to its size which is defined in terms of the number
of symbols appearing in the atom. As this theorem does not provide any sufficient condition to
detect infinite SLD-derivations, the three loop checking mechanisms mentioned above may detect
finite derivations as infinite. However, these mechanisms are complete w.r.t. the leftmost selection
rule i.e. they detect all infinite loops when the leftmost selection rule is used.
OS-check (for OverSize loop check) was first introduced by Shalin [31, 32] and was then formalized by Bol [4]. It is based on a function size that can have one of the three following definitions:
for any atoms A and B, either size(A) = size(B), either size(A) (resp. size(B)) is the count of
symbols appearing in A (resp. B), either size(A) ≤ size(B) if for each i, the count of symbols of
the i-th argument of A is smaller than or equal to that of the i-th argument of B. OS-check says
that an SLD-derivation may be infinite if it generates an atomic subgoal A that is oversized, i.e.
that has ancestor subgoals which have the same predicate symbol as A and whose size is smaller
than or equal to that of A.
EVA-check (for Extented Variant Atoms loop check) was introduced by Shen [34]. It is based
on the notion of generalized variants (if Gi and Gj (i < j) are two goals in an SLD-derivation, an
atom A in Gj is a generalized variant of an atom A′ in Gi if A is a variant of A′ except for some
arguments whose size increases from A′ to A via a set of recursive clauses.) EVA-check says that
23

an SLD-derivation may be infinite if it generates an atomic subgoal A that is a generalized variant
of some of its ancestor A′ . Here the size function that is used applies to predicate arguments,
i.e. to terms, and it is fixed: it is defined as the the count of symbols that appear in the terms.
EVA-check is more reliable than OS-check because it is less likely to mis-identify infinite loops
[34]. This is mainly due to the fact that, unlike OS-check, EVA-check refers to the informative
internal structure of subgoals.
VAF-check (for Variant Atoms loop check for logic programs with Functions) was proposed by
Shen et al. [36]. It is based on the notion of expanded variants. An atom A is an expanded variant
of an atom A′ if, after variable renaming, A becomes B that is the same as A′ except that there
may be some terms at certain positions in A′ , each A′ [i] . . . [k] of which grows in B into a function
B[i] . . . [k] = f (. . . , A′ [i] . . . [k], . . . ) (here, we use A′ [i] . . . [k] (resp. B[i] . . . [k]) to refer to the k-th
argument of . . . of the i-th argument of A′ (resp. B)). VAF-check says that an SLD-derivation
may be infinite if it generates an atomic subgoal A that is an expanded variant of some of its
ancestor A′ . VAF-check is as reliable as and more efficient than EVA-check [36].
The main difference with our work is that we want to infer atomic queries which are guaranteed
to be left looping. Hence, we consider sufficient conditions for looping, in contrast to the above
mentioned methods which consider necessary conditions. Our technique returns a set of queries
for which it has pinpointed one infinite derivation. Hence, we are not interested in soundness
as we do not care of finite derivations, nor in completeness, as the existence of just one infinite
derivation suffices. Of course, using the ∆-subsumption test as a loop checker leads to a device that
is neither sound (since ∆-subsumption is a particular case of subsumption) nor complete (since
the ∆-subsumption test provides a sufficient but not necessary condition). This is illustrated by
the following example.
Example 6.2 Let c := p(X, X) ← p(f (X), f (X)). As the arguments of the head of c have one
common variable X, every set of positions with associated terms τ + that is DN for {c} is such
that the domain of τ + (p) is empty (see (DN1) in Definition 3.35). Notice that from the head
p(X, X) of c we get
p(X, X) =⇒ p(f (X), f (X)) =⇒ · · · =⇒ p(f n (X), f n (X)) =⇒ · · ·
c

c

c

c

As the arguments of p grow from step to step, there cannot be any query in the derivation that is
∆[τ + ]-more general than one of its ancestors. Consequently, we can not conclude that p(X, X)
left loops w.r.t {c}.

On the other hand, using loop checking approaches to infer classes of atomic left looping queries
is not satisfactory because, as we said above, non-looping queries may be mis-identified as looping.
Example 6.3 We cannot replace, in Corollary 3.2, the subsumption test by the expanded variant
test used in VAF-check because, for instance, in the clause c := p(a) ← p(f (a)), we have: p(f (a))
is an expanded variant of p(a), but p(a) does not loop w.r.t. c.
Finally, [10] is also related to our study. In this paper, the authors describe an algorithm for
detecting non-terminating queries to clauses of the type p(· · · ) ← p(· · · ). The algorithm is able to
check if such a given clause has no non-terminating queries or has a query which either loops or fails
due to occur check. Moreover, given a linear atomic goal (i.e. a goal where all variable occurs at
most once), the algorithm is able to check if the goal loops or not w.r.t. the clause. The technique
of the algorithm is based on directed weighted graphs [14] and on a necessary and sufficient
condition for the existence of non-terminating queries to clauses of the type p(· · · ) ← p(· · · ). This
condition is proved in [8] and is expressed in terms of rational trees.

7

Conclusion

We have presented a extension of the subsumption test which allows to disregard some arguments,
termed neutral arguments, while checking for subsumption. We have proposed two syntactic
24

criteria for statically identifying neutral arguments. From these results, in the second part of this
report we have described algorithms for automating non-termination analysis of logic programs,
together with correctness proofs. Finally, we have applied these techniques to check the optimality
of termination conditions for logic programs.
This paper leaves numerous questions open. For instance, it might be interesting to try to
generalize this approach to constraint logic programming [19]. Can we obtain higher level proofs
compared to those we give? Can we propose more abstract criteria for identifying neutral arguments? A first step in this direction is presented in [29]. Also, our work aims at inferring classes
of atomic left looping queries, using a bottom-up point of view. Experimental data show that it
may sometimes lead to prohibitive time/space costs. How can we generate only the useful binary
clauses without fully computing the iterations of this TP -like operator? Or can we adapt our
algorithms towards a more efficient correct top-down approach for checking non-termination?

Acknowledgments
We thank Ulrich Neumerkel for numerous discussions on this topic, Roberto Bagnara and anonymous referees for interesting suggestions.

References
[1] K. R. Apt. From Logic Programming to Prolog. Prentice Hall, 1997.
[2] K. R. Apt and D. Pedreschi. Modular termination proofs for logic and pure Prolog programs.
In G. Levi, editor, Advances in Logic Programming Theory, pages 183–229. Oxford University
Press, 1994.
[3] T. Arts and H. Zantema. Termination of logic programs using semantic unification.
In Logic Program Synthesis and Transformation, volume 1048 of Lecture Notes in Computer Science. Springer-Verlag, Berlin, 1996. TALP can be used online at the address:
http://bibiserv.techfak.uni.biekefeld.de/talp/.
[4] R. N. Bol. Loop checking in partial deduction. Journal of Logic Programming, 16:25–46,
1993.
[5] R. N. Bol, K. R. Apt, and J. W. Klop. An analysis of loop checking mechanisms for logic
programs. Theoretical Computer Science, 86:35–79, 1991.
[6] K. L. Clark. Predicate logic as a computational formalism. Technical Report Doc 79/59,
Logic Programming Group, Imperial College, London, 1979.
[7] M. Codish and C. Taboch. A semantic basis for the termination analysis of logic programs.
Journal of Logic Programming, 41(1):103–123, 1999.
[8] D. De Schreye, M. Bruynooghe, and K. Verschaetse. On the existence of nonterminating
queries for a restricted class of Prolog-clauses. Artificial Intelligence, 41:237–248, 1989.
[9] D. De Schreye and S. Decorte. Termination of logic programs : the never-ending story. Journal
of Logic Programming, 19-20:199–260, 1994.
[10] D. De Schreye, K. Verschaetse, and M. Bruynooghe. A practical technique for detecting nonterminating queries for a restricted class of Horn clauses, using directed, weighted graphs. In
Proc. of ICLP’90, pages 649–663. The MIT Press, 1990.
[11] P. Deransart and G. Ferrand. Programmation en logique avec négation: présentation
formelle. Technical Report 87/3, Laboratoire d’Informatique, Département de Mathématiques
et d’Informatique, Université d’Orleans, 1987.
25

[12] N. Dershowitz, N. Lindenstrauss, Y. Sagiv, and A. Serebrenik. A general framework
for automatic termination analysis of logic programs. Applicable Algebra in Engineering,Communication and Computing, 12(1/2):117–156, 2001.
[13] P. Devienne. Weighted graphs, a tool for expressing the behavious of recursive rules in logic
programming. pages 397–404. OHMSHA Ltd. Tokyo and Springer-Verlag, 1988. Proc. of the
Inter. Conf. on Fifth Generation Computer Systems 88, Tokyo, Japan.
[14] P. Devienne. Weighted graphs: A tool for studying the halting problem and time complexity
in term rewriting systems and logic programming. Theoretical Computer Science, 75(2):157–
215, 1990.
[15] P. Devienne, P.Lebègue, and J-C. Routier. Halting problem of one binary Horn clause is
undecidable. In LNCS, volume 665, pages 48–57. Springer-Verlag, 1993. Proc. of STACS’93.
[16] M. Gabbrielli and R. Giacobazzi. Goal independency and call patterns in the analysis of
logic programs. In Proceedings of the ACM Symposium on applied computing, pages 394–399.
ACM Press, 1994.
[17] S. Genaim and M. Codish. Inferring termination condition for logic programs using backwards
analysis. In Proceedings of Logic for Programming, Artificial intelligence and Reasoning,
Lecture Notes in Computer Science. Springer-Verlag, Berlin, 2001. TerminWeb can be used
online from http://www.cs.bgu.ac.il/~codish.
[18] R. Gori and G. Levi. Finite failure is and-compositional. Journal of Logic and Computation,
7(6):753–776, 1997.
[19] J. Jaffar and J. L. Lassez. Constraint logic programming. In Proc. of the ACM Symposium
on Principles of Programming Languages, pages 111–119. ACM Press, 1987.
[20] N. Lindenstrauss. TermiLog: a system for checking termination of queries to logic programs,
1997. http://www.cs.huji.ac.il/~naomil.
[21] J. W. Lloyd. Foundations of Logic Programming. Springer-Verlag, 1987.
[22] M. Martelli M. Falaschi, G. Levi and C. Palamidessi. A model-theoretic reconstruction of the
operational semantics of logic programs. Information and Computation, 102(1):86–113, 1993.
[23] F. Mesnard. Inferring left-terminating classes of queries for constraint logic programs by
means of approximations. In M. J. Maher, editor, Proc. of the 1996 Joint Intl. Conf. and
Symp. on Logic Programming, pages 7–21. MIT Press, 1996.
[24] F. Mesnard and R. Bagnara. cTI: a constraint-based termination inference tool for ISOProlog. Theory and Practice of Logic Programming, 2004. To appear.
[25] F. Mesnard and U. Neumerkel. cTI: a tool for inferring termination conditions of ISO-Prolog,
april 2000. http://www.complang.tuwien.ac.at/cti.
[26] F. Mesnard and U. Neumerkel. Applying static analysis techniques for inferring termination
conditions of logic programs. In P. Cousot, editor, Static Analysis Symposium, volume 2126
of Lecture Notes in Computer Science, pages 93–110. Springer-Verlag, Berlin, 2001.
[27] F. Mesnard, E. Payet, and U. Neumerkel. Detecting optimal termination conditions of logic
programs. In M. Hermenegildo and G. Puebla, editors, Proc. of the 9th International Symposium on Static Analysis, volume 2477 of Lecture Notes in Computer Science, pages 509–525.
Springer-Verlag, Berlin, 2002.
[28] R. O’Keefe. The Craft of Prolog. MIT Press, 1990.

26

[29] E. Payet and F. Mesnard. Non-termination inference of logic programs. In R. Giacobazzi,
editor, Proc. of the 11th International Symposium on Static Analysis, volume 3148 of Lecture
Notes in Computer Science. Springer-Verlag, Berlin, 2004.
[30] L. Plümer. Terminations proofs for logic programs. Number 446 in LNAI. Springer-Verlag,
Berlin, 1990.
[31] D. Sahlin. The mixtus approach to automatic partial evaluation of full Prolog. In S. Debray and M. Hermenegildo, editors, Proc. of the 1990 North American Conference on Logic
Programming, pages 377–398. MIT Press, Cambridge, MA, 1990.
[32] D. Sahlin. Mixtus: an automatic partial evaluator for full Prolog. New Generation Computing,
12(1):7–51, 1993.
[33] M. Schmidt-Schauss. Implication of clauses is undecidable. Theoretical Computer Science,
59:287–296, 1988.
[34] Y-D. Shen. An extended variant of atoms loop check for positive logic programs. New
Generation Computing, 15(2):187–204, 1997.
[35] Y-D. Shen, J-H. You, L-Y. Yuan, S. Shen, and Q. Yang. A dynamic approach to characterizing
termination of general logic programs. ACM Transactions on Computational Logic, 4(4):417–
434, 2003.
[36] Y-D. Shen, L-Y. Yuan, and J-H. You. Loops checks for logic programs with functions. Theoretical Computer Science, 266(1-2):441–461, 2001.

27

A

Algorithms

First, we define a pre-order relation over sets of positions with associated terms. Such a relation
is useful for the design of the algorithms that we present in the sequel of this section.
+
Definition A.1 (4 and τmax
)

• τ1+ 4 τ2+ if for each p ∈ Π, Dom(τ1+ (p)) ⊆ Dom(τ2+ (p)) and for each i ∈ Dom(τ1+ (p)),
τ2+ (p)(i) is more general than τ1+ (p)(i).
+
+
• τmax
denotes a set of positions with associated terms s.t. Dom(τmax
(p)) = [1, arity(p)] for
+
each p ∈ Π and τmax (p)(i) is a variable for each i ∈ [1, arity(p)].

A.1

DN Sets of Positions with Associated Terms for Binary Programs

We present below an algorithm for computing DN sets of positions with associated terms.

dna BinProg, τ1+ :
in: BinProg: a finite set of binary clauses
τ1+ : a set of positions with associated terms
out: τ2+ s.t. τ2+ 4 τ1+ and τ2+ is DN for BinProg
1:
2:
3:
4:
5:
6:
7:

τ2+ := τ1+
τ2+ := satisfy DN1(BinProg, τ2+ )
τ2+ := satisfy DN2(BinProg, τ2+ )
τ2+ := satisfy DN3(BinProg, τ2+ )
while satisfy DN4(BinProg, τ2+ ) 6= τ2+ do
τ2+ := satisfy DN4(BinProg, τ2+ )
return τ2+

The algorithm dna calls four auxiliary functions that correspond to conditions (DN1), (DN2)
(DN3) and (DN4) in the definition of a DN set of positions with associated terms (see Definition 3.35). These functions are detailed below.
After τ2+ := satisfy DN1(BinProg , τ2+ ) at line 2 of dna, τ2+ satisfies item (DN1) of Definition 3.35.

satisfy DN1 BinProg, τ1+ :
1: τ2+ := τ1+
2: for each p(s1 , . . . , sn ) ← B ∈ BinProg do
3:
E := {i ∈ [1, n] | Var (si ) ∩ Var ({sj | j 6= i}) = ∅}
4:
τ2+ (p) := τ2+ (p)|(Dom(τ2+ (p)) ∩ E)
5: return τ2+

After τ2+ := satisfy DN2(BinProg , τ2+ ) at line 3 of dna, τ2+ satisfies item (DN2) of Definition 3.35. Notice that less general at line 5 of satisfy DN2 is a function that returns the less
general term of two given terms; if none of the given terms is less general than the other, then
this function returns undefined.

28


satisfy DN2 BinProg , τ1+ :

1: τ2+ := τ1+
2: for each p(s1 , . . . , sn ) ← B ∈ BinProg do
3:
F := ∅
4:
for each i ∈ Dom(τ2+ (p)) do
5:
ui := less general(si , τ2+ (p)(i))
6:
if ui = undefined then F := F ∪ {i}
7:
else τ2+ (p)(i) := ui
8:
τ2+ (p) := τ2+ (p)|(Dom(τ2+ (p)) \ F )
9: return τ2+
After τ2+ := satisfy DN3(BinProg , τ2+ ) at line 4 of dna, τ2+ satisfies item (DN3) of Definition 3.35. The function satisfy DN3 is detailed below.

satisfy DN3 BinProg, τ1+ :
1: τ2+ := τ1+
2: for each H ← q(t1 , . . . , tm ) ∈ BinProg do
3:
F := ∅
4:
for each i ∈ Dom(τ2+ (q)) do
5:
if τ2+ (q)(i) is not more general than ti then F := F ∪ {i}
6:
τ2+ (q) := τ2+ (q)|(Dom(τ2+ (q)) \ F )
7: return τ2+

Finally, the function satisfy DN4 is defined as follows. After line 6 of dna, the set of positions
with associated terms τ2+ satisfies item (DN4) of Definition 3.35.

satisfy DN4 BinProg, τ1+ :
1: τ2+ := τ1+
2: for each p(s1 , . . . , sn ) ← q(t1 , . . . , tm ) ∈ BinProg do
3:
F := ∅
4:
for each i ∈ Dom(τ2+ (p)) do
5:
for each j ∈ [1, m] \ Dom(τ2+ (q)) do
6:
if Var(si ) ∩ Var (tj ) 6= ∅ then F := F ∪ {i}
+
7:
τ2 (p) := τ2+ (p)|(Dom(τ2+ (p)) \ F )
8: return τ2+

Proposition A.2 (Correctness of dna) Let BinProg be a binary program and τ1+ be a set of
positions with associated terms.
1. satisfy DN1(BinProg, τ1+ ), . . . , satisfy DN4(BinProg, τ1+ ) terminate;
2. satisfy DN1(BinProg, τ1+ ) 4 τ1+ , . . . , satisfy DN4(BinProg , τ1+ ) 4 τ1+ ;
3. dna(BinProg, τ1+ ) terminates;
4. dna(BinProg , τ1+ ) 4 τ1+ and dna(BinProg, τ1+ ) is a set of positions with associated terms that
is DN for BinProg .
Proof. We have:
1. satisfy DN1(BinProg, τ1+ ) terminates because, as BinProg is a finite set of binary clauses,
the loop at lines 2–4 terminates. Concerning satisfy DN2–4, the inner loops terminate since
for each p ∈ Π, Dom(τ2+ (p)) ⊆ [1, arity(p)] and the outer loop terminates as BinProg is a
finite set of binary clauses.
29

• satisfy DN1(BinProg , τ1+ ) 4 τ1+ :
Line 1, we start from τ1+ . Line 4, we have for each relation symbol p from the heads of
the clauses of BinProg :

2.

Dom(τ2+ (p)) ⊆ Dom(τ1+ (p)) and ∀i ∈ Dom(τ2+ (p)), τ2+ (p)(i) = τ1+ (p)(i) .
Hence, when we reach line 5, we have: satisfy DN1(BinProg, τ1+ ) 4 τ1+ .
• satisfy DN2(BinProg , τ1+ ) 4 τ1+ :
Line 1, we start from τ1+ . Then, for each relation symbol p from the heads of the
clauses of BinProg and for each i ∈ Dom(τ2+ (p)), either τ2+ (p)(i) is set to a less general
term than τ2+ (p)(i) (line 7) or i is removed from the domain of τ2+ (p) (lines 6 and 8).
Therefore, when we reach line 9, we have: satisfy DN2(BinProg , τ1+ ) 4 τ1+ .
• satisfy DN3(BinProg , τ1+ ) 4 τ1+ :
Line 1, we start from τ1+ . Line 6, we have for each relation symbol q from the bodies
of the clauses of BinProg:
Dom(τ2+ (q)) ⊆ Dom(τ1+ (q)) and ∀i ∈ Dom(τ2+ (q)), τ2+ (q)(i) = τ1+ (q)(i) .
Hence, when we reach line 7, we have: satisfy DN3(BinProg, τ1+ ) 4 τ1+ .
• satisfy DN4(BinProg , τ1+ ) 4 τ1+ :
Line 1, we start from τ1+ . Line 7, we have for each relation symbol p from the heads of
the clauses of BinProg :
Dom(τ2+ (p)) ⊆ Dom(τ1+ (p)) and ∀i ∈ Dom(τ2+ (p)), τ2+ (p)(i) = τ1+ (p)(i) .

(2)

Hence, when we reach line 8, we have: satisfy DN4(BinProg, τ1+ ) 4 τ1+ .
3. Each call to satisfy DN1, . . . , satisfy DN4 terminate. Moreover, concerning function
satisfy DN4, we mentioned above that (2) holds. As ⊂ is a well-founded relation over
the set of sets, the loop at lines 5–6 terminates.
4. Line 1, we start from τ1+ . Then satisfy DN1, . . . , satisfy DN4 weaken τ1+ with respect to
Definition 3.35. When we reach the fixpoint, the property holds.


A.2

Loop Dictionaries

A.2.1

Proof of Proposition 4.3, page 14

We proceed by induction on the length n of BinSeq.
• Basis. If n = 0, then, as ([H ← B], τ + ) is a looping pair, B is ∆[τ + ]-more general than H
and τ + is DN for H ← B, i.e. ∆[τ + ] is DN for H ← B by Theorem 3.39. Consequently, by
Proposition 3.20, H loops w.r.t. [H ← B].
• Induction. Suppose that for an n ≥ 0, each looping pair ([H ← B|BinSeq], τ + ) with BinSeq
of length n is such that H loops w.r.t. [H ← B|BinSeq].
If BinSeq is of length n + 1, it has form [H1 ← B1 |BinSeq 1 ] with BinSeq 1 of length n.
Moreover, as ([H ← B|BinSeq], τ + ) is a looping pair, there exists a set of positions with
associated terms τ1+ such that ([H1 ← B1 |BinSeq 1 ], τ1+ ) is a looping pair and B is ∆[τ1+ ]more general than H1 . So, by the induction hypothesis, H1 loops w.r.t. [H1 ← B1 |BinSeq 1 ]
i.e. H1 loops w.r.t. BinSeq. As B is ∆[τ1+ ]-more general than H1 and ∆[τ1+ ] is DN for
BinSeq, by Definition 3.18 B loops w.r.t. BinSeq. Therefore, by Corollary 3.3, H loops
w.r.t. [H ← B|BinSeq].

30

A.2.2

Computing a Loop Dictionary

The top-level function for inferring loop dictionaries from a logic program is the following. It uses
the auxiliary functions unit loop and loops from dict described below.
infer loop dict(P , max ):
in: P : a logic program
max : a non-negative integer
out: a loop dictionary, each element (BinSeq, τ + ) of which
is such that BinSeq ⊆ TPβ ↑ max
1: Dict := ∅
2: for each H ← B ∈ TPβ ↑ max do
3:
Dict := unit loop(H ← B, Dict )
4:
Dict := loops from dict(H ← B, Dict )
5: return Dict
The function unit loop is used to extract from a binary clause the most simple form of a
looping pair:
unit loop(H ← B, Dict):
in: H ← B: a binary clause
Dict: a loop dictionary
out: Dict′ : a loop dictionary, every element (BinSeq, τ + ) of which is
such that either (BinSeq, τ + ) ∈ Dict or BinSeq = [H ← B]
1:
2:
3:
4:
5:

Dict′ := Dict
+
τ + := dna([H ← B], τmax
)
+
if B is ∆[τ ]-more general than H then
Dict ′ := Dict ′ ∪ {([H ← B], τ + )}
return Dict ′

Termination of unit loop relies on that of dna. Partial correctness is deduced from the next
theorem.
Theorem A.3 (Partial correctness of unit loop) Let H ← B be a binary clause and Dict be a
loop dictionary. Then unit loop(H ← B, Dict) is a loop dictionary, every element (BinSeq, τ + )
of which is such that either (BinSeq, τ + ) ∈ Dict or BinSeq = [H ← B].
Proof. Let τ + be the set of positions with associated terms computed at line 2. If B is not
∆[τ + ]-more general than H then, at line 5 of unit loop, we have Dict ′ = Dict, so the theorem
holds.
Now suppose that B is ∆[τ + ]-more general than H. Then, at line 5 we have Dict ′ := Dict ∪
{([H ← B], τ + )} where Dict is a loop dictionary, τ + is DN for H ← B and B is ∆[τ + ]-more
general than H. So at line 5 Dict ′ is a loop dictionary, every element (BinSeq, τ + ) of which is
such that either (BinSeq, τ + ) ∈ Dict or BinSeq = [H ← B].
The function loops from dict is used to combine a binary clause to some looping pairs that
have already been infered in order to get some more looping pairs.

31

loops from dict(H ← B, Dict ):
in: H ← B: a binary clause
Dict: a loop dictionary
out: Dict ′ : a loop dictionary, every element (BinSeq, τ + ) of which is
such that (BinSeq, τ + ) ∈ Dict or BinSeq = [H ← B|BinSeq 1 ]
for some (BinSeq 1 , τ1+ ) in Dict
1: Dict ′ := Dict

2: for each [H1 ← B1 |BinSeq 1 ], τ1+ ∈ Dict do
3:
if B is ∆[τ1+ ]-more general than H1 then

4:
τ + := dna([H ← B, H1 ← B1 |BinSeq 1 ], τ1+ )
5:
Dict ′ := Dict ′ ∪ {([H ← B, H1 ← B1 |BinSeq 1 ], τ + )}
6: return Dict ′
Termination of loops from dict follows from finiteness of Dict (because Dict is a loop dictionary) and termination of dna. Partial correctness follows from the result below.
Theorem A.4 (Partial correctness of loops from dict) Let H ← B be a binary clause and Dict
be a loop dictionary. Then loops from dict(H ← B, Dict) is a loop dictionary, every element
(BinSeq, τ + ) of which is such that (BinSeq, τ + ) ∈ Dict or BinSeq = [H ← B|BinSeq 1 ] for some
(BinSeq 1 , τ1+ ) in Dict .
Proof. Upon initialization at line 1, Dict ′ is a loop dictionary. Suppose that before an iteration of
the loop at line 2, Dict ′ is a loop dictionary. Let ([H1 ← B1 |BinSeq 1 ], τ1+ ) ∈ Dict.
If the condition at line 3 is false, then Dict ′ remains unchanged, so after the iteration Dict ′
is still a loop dictionary. Otherwise, the pair ([H ← B, H1 ← B1 |BinSeq 1 ], τ + ) is added to
Dict ′ at line 5. Notice that this pair is a looping one because τ + defined at line 4 is DN for
[H ← B, H1 ← B1 |BinSeq 1 ] and ([H1 ← B1 |BinSeq 1 ], τ1+ ) is a looping pair and B is ∆[τ1+ ]-more
general than H1 . Therefore, after the iteration, Dict ′ is a loop dictionary. Finally, notice that as
Dict is a finite set, the loop at line 2 terminates. Hence, at line 6 Dict ′ is a finite set of looping
pairs i.e. Dict ′ is a loop dictionary.
Moreover, at line 1, each element of Dict ′ belongs to Dict . Then, during the loop, pairs of form
([H ← B|BinSeq 1 ], τ + ) are added to Dict ′ where BinSeq 1 is such that there exists (BinSeq 1 , τ1+ ) ∈
Dict . Consequently, at line 6 each element (BinSeq, τ + ) of Dict ′ is such that either (BinSeq, τ + ) ∈
Dict or BinSeq = [H ← B|BinSeq 1 ] for some (BinSeq 1 , τ1+ ) in Dict .
Finally, here is the correctness proof of the function infer loop dict.
Theorem A.5 (Correctness of infer loop dict) Let P be a logic program and max be a nonnegative integer. Then, infer loop dict(P, max ) terminates and returns a loop dictionary, every
element (BinSeq, τ + ) of which is such that BinSeq ⊆ TPβ ↑ max .
Proof. At line 1, Dict is initialized to ∅ which is a loop dictionary. Suppose that before an
iteration of the loop at line 2, Dict is a loop dictionary. Then at lines 3 and 4 unit loop and
loops from dict fullfil their specifications. Hence, the call to these functions terminates and after
the iteration Dict is still a loop dictionary. Finally, as TPβ ↑ max is a finite set, the loop at line 2
terminates and at line 5 Dict is a loop dictionary.
Moreover, at line 1 each element (BinSeq, τ + ) of Dict is such that BinSeq ⊆ TPβ ↑ max . Then,
during the loop, unit loop and loops from dict are called with clauses from TPβ ↑ max . So, by
Theorem A.3 and Theorem A.4, after the iteration each element (BinSeq, τ + ) of Dict is such that
BinSeq ⊆ TPβ ↑ max .

A.3

Looping Conditions

The following function computes a finite set of looping conditions for any given logic program.

32

infer loop cond(P , max ):
in: P : a logic program
max : a non-negative integer
out: a finite set of looping conditions for P
1:
2:
3:
4:
5:

L := ∅
Dict := infer loop dict(P, max )
for each ([H ← B|BinSeq], τ + ) ∈ Dict do
L := L ∪ {(H, τ + )}
return L

A call to infer loop cond(P , max ) terminates for any logic program P and any non-negative
integer max because infer loop dict(P, max ) at line 2 terminates and the loop at line 3 has a
finite number of iterations (because, by correctness of infer loop dict, Dict is finite.) Partial
correctness of infer loop cond follows from the next theorem.
Theorem A.6 (Partial correctness of infer loop cond) Let P be a logic program and max be a
non-negative integer. Then infer loop cond(P, max ) is a finite set of looping conditions for P .
Proof. By correctness of infer loop dict, Dict is a loop dictionary.
Let ([H ← B|BinSeq], τ + ) ∈ Dict . Then ([H ← B|BinSeq], τ + ) is a looping pair. Consequently, by Proposition 4.3, H loops w.r.t. [H ← B|BinSeq]. As τ + , hence ∆[τ + ], is DN for
[H ← B|BinSeq], by Definition 3.18 every atom that is ∆[τ + ]-more general than H loops w.r.t.
[H ← B|BinSeq].
As ([H ← B|BinSeq], τ + ) ∈ Dict , by Theorem A.5 we have
[H ← B|BinSeq] ⊆ TPβ ↑ max ⊆ bin unf (P ) .
So, by Theorem 2.1, H left loops w.r.t. P and every atom that is ∆[τ + ]-more general than H left
loops w.r.t. P . So, (H, τ + ) is a looping condition for P . Consequently, at line 5, L is a finite set
of looping conditions for P because, as Dict is finite, the loop at line 3 iterates a finite number of
times.

B

Proofs

B.1

Two Useful Lemmas

Lemma B.1 Let c := H ← B be a binary clause. Then, for every variant cγ of c such that
Var (cγ) ∩ Var (H) = ∅, we have H =⇒ Bγ ′ where γ ′ := γ|Var(B) \ Var (H).
c

Proof. Let µ := {xγ/x|x ∈ Var (H)}. By Claim B.2 below, µ is an mgu of Hγ and H. Hence, as
µ
Var (cγ) ∩ Var(H) = ∅, we have the left derivation step H =⇒ Bγµ where cγ is the input clause
c
used.
µ
If Var(B) = ∅, then Bγµ = Bγ ′ , so we have H =⇒ Bγ ′ i.e. H =⇒ Bγ ′ .
c

If Var(B) 6= ∅, take a variable x ∈ Var(B):
• if x ∈ Var(H), then x(γµ) = (xγ)µ = x by definition of µ,
• if x 6∈ Var(H), then x(γµ) = (xγ)µ = xγ by definition of µ.
µ

Hence, Bγµ = Bγ ′ , so we have H =⇒ Bγ ′ i.e. H =⇒ Bγ ′ .
c

c

Claim B.2 µ is an mgu of Hγ and H.

33

c

Proof. Let p(s1 , . . . , sn ) := H. The set of unifiers of Hγ and H is the same as that of E1 :=
{s1 γ = s1 , . . . , sn γ = sn }. Let E2 := {xγ = x | x ∈ Var (H)}. Notice that, as γ is a renaming,
if x, y ∈ Var (H) then x 6= y ⇒ xγ 6= yγ. Moreover, for each x ∈ Var(H), xγ 6= x because
Var (cγ) ∩ Var (H) = ∅. So, E2 is solved. Consequently, by Lemma 2.15 page 32 of [1], µ is an
mgu of E2 . Notice that, by Claim B.3 below, the set of unifiers of E1 is that of E2 . So µ is an
mgu of E1 i.e. µ is an mgu of Hγ and H.
Claim B.3 E1 and E2 have the same set of unifiers.
Proof. Let θ be a unifier of E1 . Let x ∈ Var (H) and let i ∈ [1, n] such that x ∈ Var (si ). Then
si γθ = si θ, so, if xk is an occurrence of x in si , we have xk γθ = xk θ i.e. (xk γ)θ = xk θ. As x
denotes any variable of H, we conclude that θ is a unifier of E2 . Conversely, let θ be a unifier of
E2 . Then, for each i ∈ [1, n], (si γ)θ = si θ by definition of E2 . Hence, θ is a unifier of E1 .
Lemma B.4 Let c := H ← B be a binary clause, cγ be a variant of c such that Var (cγ) ∩
Var (H) = ∅ and γ ′ := γ|Var (B)\Var (H). Then, there exists a renaming γ ′′ such that Bγ ′ = Bγ ′′ .
Proof. Let A := {x | x ∈ Ran(γ ′ ) and x 6∈ Dom(γ ′ )} and B := {x | x ∈ Dom(γ ′ ) and x 6∈
Ran(γ ′ )}. Notice that Ran(γ ′ ) and Dom(γ ′ ) have the same number of elements, so A and B have
the same number of elements. Let σ be a 1-1 and onto mapping from A to B. Then, γ ′′ := γ ′ ∪ σ
is a well-defined substitution, is such that Dom(γ ′′ ) = Ran(γ ′′ ), is 1-1 and is onto. Consequently,
γ ′′ is a renaming.
Now, let us prove that Bγ ′ = Bγ ′′ . If Var (B) = ∅, then the result is straightforward.
Otherwise, let x ∈ Var(B).
• If x ∈ Var (H) then, as Dom(γ ′ ) ⊆ Var (B) \ Var (H), we have x 6∈ Dom(γ ′ ), so xγ ′ = x.
Moreover, xγ ′′ = x(γ ′ ∪σ) = xσ = x because Dom(σ) ⊆ Ran(γ ′ ) and Ran(γ ′ )∩Var (H) = ∅.
Consequently, we have xγ ′ = xγ ′′ .
• If x 6∈ Var (H) and x ∈ Dom(γ ′ ) then xγ ′′ = x(γ ′ ∪ σ) = xγ ′ .
• If x 6∈ Var (H) and x 6∈ Dom(γ ′ ) then xγ ′ = x.
Now, suppose that x ∈ Dom(σ). Then, as Dom(σ) ⊆ Ran(γ ′ ) ⊆ Ran(γ), we have x ∈
Ran(γ). But, as γ is a renaming, Ran(γ) = Dom(γ), so we have x ∈ Dom(γ). As
x ∈ Var (B), as x 6∈ Var(H) and as γ ′ := γ|Var (B) \ Var (H), we have x ∈ Dom(γ ′ ).
Contradiction.
Consequently, x 6∈ Dom(σ), so xσ = x and xγ ′′ = x(γ ′ ∪ σ) = xσ = x. Finally, we have
proved that xγ ′ = xγ ′′ .

B.2

Proof of Corollary 3.2, page 4

By Lemma B.1 and Lemma B.4, we have H =⇒ Bγ ′′ where γ ′′ is a renaming. As by hypothesis
c

B is more general than H, then Bγ ′′ is more general than H. Therefore, by the One Step Lifting
Lemma 3.1, H loops w.r.t. {c}.

B.3

Proof of Corollary 3.3, page 4

By Lemma B.1 and Lemma B.4, we have H =⇒ Bγ ′′ where γ ′′ is a renaming. As Bγ ′′ is more
c

general than B and as B loops w.r.t. P , then, by the One Step Lifting Lemma 3.1, Bγ ′′ loops
w.r.t. P , so H loops w.r.t. P .

34

B.4

Proof of Proposition 3.16, page 7

If A is ∆-more general than B, we have, for a substitution η:

A = p(s1 , . . . , sn )



B = p(t1 , . . . , tn )
∀i ∈ [1, n] \ Dom(∆(p)), ti = si η



∀i ∈ Dom(∆(p)), ∆(p)(i)(si ) = true .

Let A′ be a variant of A. Then, there exists a renaming γ such that A′ = Aγ. As for each
i ∈ Dom(∆(p)), ∆(p)(i) is a variant independent term-condition, we have:
 ′
A = p(s1 γ, . . . , sn γ)



B = p(t1 , . . . , tn )
∀i ∈ [1, n] \ Dom(∆(p)), ti = si η = (si γ)(γ −1 η)



∀i ∈ Dom(∆(p)), ∆(p)(i)(si γ) = true .
Consequently, A′ is ∆-more general than B for γ −1 η, i.e. A′ is ∆-more general than B.

B.5

Proof of Proposition 3.17, page 7

⇐ By definition.
⇒ Let p(s1 , . . . , sn ) := A and p(t1 , . . . , tn ) := B. As A is ∆-more general than B, there exists a
substitution σ such that A is ∆-more general than B for σ. Notice that A is also ∆-more
general than B for the substitution obtained by restricting the domain of σ to the variables
appearing in the positions of A not distinguished by ∆. More precisely, let
η := σ|V ar({si | i ∈ [1, n] \ Dom(∆(p))}) .
Then,
Dom(η) ⊆ V ar(A)

(3)

and A is ∆-more general than B for η.
Now, let x ∈ Dom(η). Then, there exists i ∈ [1, n] \ Dom(∆(p)) such that x ∈ V ar(si ).
As A is ∆-more general than B for η and i ∈ [1, n] \ Dom(∆(p)), we have ti = si η. So, as
x ∈ V ar(si ), xη is a subterm of ti . Consequently, V ar(xη) ⊆ V ar(ti ), so V ar(xη) ⊆ V ar(B).
So, we have proved that for each x ∈ Dom(η), V ar(xη) ⊆ V ar(B), i.e. we have proved that
Ran(η) ⊆ V ar(B) .

(4)

Finally, (3) and (4) imply that Dom(η) ∪ Ran(η) ⊆ V ar(A, B) i.e. that
V ar(η) ⊆ V ar(A, B) .

B.6

Proof of Proposition 3.20, page 8

By Lemma B.1 and Lemma B.4, we have H =⇒ Bγ ′′ where γ ′′ is a renaming. As by hypothesis B
c

is ∆-more general than H, then by Proposition 3.16 Bγ ′′ is ∆-more general than H. Therefore,
as ∆ is DN for c, by Definition 3.18, H loops w.r.t. {c}.

B.7

Proof of Proposition 3.37, page 11

Let c := p(s1 , . . . , sn ) ← q(t1 , . . . , tm ) and c′ := p(s′1 , . . . , s′n ) ← q(t′1 , . . . , t′m ) be a variant of c.
Then, there exists a renaming γ such that c′ = cγ.

35

(DN1) Let i ∈ Dom(τ + (p)). Suppose that there exists j 6= i such that V ar(s′i ) ∩ V ar(s′j ) 6= ∅
and let us derive a contradiction.
Let x′ ∈ V ar(s′i ) ∩ V ar(s′j ). As s′j = sj γ, there exists x ∈ V ar(sj ) such that x′ = xγ.
For such an x, as j 6= i and as V ar(si ) ∩ V ar(sj ) = ∅ (because τ + is DN for c), we
have x 6∈ V ar(si ). So, as γ is a 1-1 and onto mapping from its domain to itself, we have
xγ 6∈ V ar(si γ)3 , i.e. x′ 6∈ V ar(s′i ). Contradiction!
Consequently, V ar(s′i ) ∩ V ar(s′j ) = ∅.
(DN2) Let hi 7→ ui i ∈ τ + (p). As si is more general than ui (because τ + is DN for c) and as s′i
is a variant of si , s′i is more general than ui .
(DN3) Let hj 7→ uj i ∈ τ + (q). As tj is an instance of uj (because τ + is DN for c) and as t′j is a
variant of tj , t′j is an instance of uj .
(DN4) Let i ∈ Dom(τ + (p)). Suppose there exists j 6∈ Dom(τ + (q)) such that V ar(s′i )∩V ar(t′j ) 6=
∅. Let us derive a contradiction.
Let x′ ∈ V ar(s′i ) ∩ V ar(t′j ). As t′j = tj γ and x′ ∈ V ar(t′j ), there exists x ∈ V ar(tj ) such that
x′ = xγ. For such an x, as the elements of V ar(si ) only occur in those tk s.t. k ∈ Dom(τ + (q))
(because τ + is DN for c) and as x ∈ V ar(tj ) with j 6∈ Dom(τ + (q)), we have x 6∈ V ar(si ).
So, as γ is a 1-1 and onto mapping from its domain to itself, we have xγ 6∈ V ar(si γ) (see
footnote 3), i.e. x′ 6= V ar(s′i ). Contradiction! So, for each j 6∈ Dom(τ + (q)), we have
V ar(s′i ) ∩ V ar(t′j ) = ∅.
Finally, we have established that τ + is DN for c′ .

B.8

DN Sets of Positions with Associated Terms Generate DN Filters

In this section, we give a proof of Theorem 3.39, page 12.
B.8.1

Context

All the results of this section are parametric to the following context:
• P is a binary program and τ + is a set of positions with associated terms that is DN for P ,
θ

• Q =⇒ Q1 is a left derivation step where
c

– c ∈ P,
– Q := p(t1 , . . . , tn ),
– c1 := p(s1 , . . . , sn ) ← B is the input clause used (consequently, c1 is a variant of c that
is variable disjoint from Q),
• Q′ := p(t′1 , . . . , t′n ) is ∆[τ + ]-more general than Q i.e., by Proposition 3.17, there exists a
substitution η such that V ar(η) ⊆ V ar(Q, Q′ ) and Q′ is ∆[τ + ]-more general than Q for η.
3 Because if xγ ∈ V ar(s γ), then either x ∈ V ar(s ), either xγ ∈ V ar(s ) and (xγ)γ = xγ. The former case is
i
i
i
impossible because we said that x 6∈ V ar(si ). The latter case is impossible too because (xγ)γ = xγ implies that
xγ 6∈ Dom(γ) i.e. x 6∈ Dom(γ) (because γ is a 1-1 and onto mapping from its domain to itself); so, x = xγ i.e., as
xγ ∈ V ar(si ), x ∈ V ar(si ).

36

B.8.2

Technical Definitions and Lemmas

Definition B.5 (Technical Definition) Let c′1 := p(s′1 , . . . , s′n ) ← B ′ be a binary clause such that
• V ar(c′1 ) ∩ V ar(Q, Q′ ) = ∅ and
• c1 = c′1 γ for some renaming γ satisfying V ar(γ) ⊆ V ar(c1 , c′1 ).
As c′1 is a variant of c1 and c1 is a variant of c, then c′1 is a variant of c. Moreover, as τ +
is DN for c, by Proposition 3.37, τ + is DN for c′1 . So, by (DN2) in Definition 3.35, for each
hi 7→ ui i ∈ τ + (p) there exists a substitution δi such that ui = s′i δi .
Moreover, as p(t′1 , . . . , t′n ) is ∆[τ + ]-more general than p(t1 , . . . , tn ), for each hi 7→ ui i ∈ τ + (p),
′
ti is an instance of ui . So, there exists a substitution δi′ such that t′i = ui δi′ .
For each i ∈ Dom(τ + (p)), we set
def

σi = (δi δi′ )|V ar(s′i ) .
Moreover, we set:
def

[

σ =

σi .

i∈Dom(τ + (p))

Lemma B.6 The set σ of Definition B.5 is a well-defined substitution.
Proof. Notice that, as τ + is DN for c′1 , by (DN1) in Definition 3.35, we have
∀i ∈ Dom(τ + (p)), ∀j ∈ [1, n] \ {i}, V ar(s′i ) ∩ V ar(s′j ) = ∅ .
Consequently,
∀i, j ∈ Dom(τ + (p)), i 6= j ⇒ Dom(σi ) ∩ Dom(σj ) = ∅ .
Moreover, for each i ∈ Dom(τ + (p)), σi is a well-defined substitution. So, σ is a well-defined
substitution.
Lemma B.7 (Technical Lemma) Let c′1 := p(s′1 , . . . , s′n ) ← B ′ be a binary clause such that
• V ar(c′1 ) ∩ V ar(Q, Q′ ) = ∅ and
• c1 = c′1 γ for some renaming γ satisfying V ar(γ) ⊆ V ar(c1 , c′1 ).
Let σ be the substitution of Definition B.5.
p(t′1 , . . . , t′n ) and p(s′1 , . . . , s′n ).

Then, the substitution σηγθ is a unifier of

Proof. The result follows from the following facts.
• For each hi 7→ ui i ∈ τ + (p), we have:
s′i σ = s′i σi = s′i δi δi′ = (s′i δi )δi′ = ui δi′ = t′i
and t′i σ = t′i because Dom(σ) ⊆ V ar(c′1 ) and V ar(Q′ ) ∩ V ar(c′1 ) = ∅. So, s′i σ = t′i σ and
s′i σηγθ = t′i σηγθ.
• For each i ∈ [1, n] \ Dom(τ + (p)), we have:
s′i ηγθ = (s′i η)γθ = s′i γθ = (s′i γ)θ = si θ
and
t′i ηγθ = (t′i η)γθ = ti γθ = (ti γ)θ = ti θ
θ

and si θ = ti θ because θ is a unifier of p(s1 , . . . , sn ) and p(t1 , . . . , tn ) (because Q =⇒ Q1 with
c

c1 as input clause used). So,

s′i ηγθ = t′i ηγθ
37

(5)

• For each i ∈ [1, n] \ Dom(τ + (p)), we also have:

– s′i σ = s′i because Dom(σ) = V ar {s′j | j ∈ Dom(τ + (p))} and, by (DN1) in Defini
tion 3.35, V ar {s′j | j ∈ Dom(τ + (p))} ∩ V ar(s′i ) = ∅;
– t′i σ = t′i because Dom(σ) ⊆ V ar(c′1 ) and V ar(Q′ ) ∩ V ar(c′1 ) = ∅.
Therefore, because of (5), s′i σηγθ = t′i σηγθ.
B.8.3

∆-Propagation

Now we extend, in the case of left derivations with atomic queries and binary clauses, the following
Propagation Lemma that is proved by Apt in [1] p. 54–56.
Lemma B.8 (Propagation) Let G, G1 , G′ and G′1 be some queries such that
G =⇒ G1

G′ =⇒ G′1

and

c

c

and

• G is an instance of G′
• in G and G′ atoms in the same positions are selected.
Then, G1 is an instance of G′1 .
First we establish the following result.
θ′

Lemma B.9 Suppose there exists a left derivation step of form Q′ =⇒ Q′1 where the input clause
c

is c′1 such that V ar(Q) ∩ V ar(c′1 ) = ∅. Then, Q′1 is ∆[τ + ]-more general than Q1 .
Proof. Notice that we have
V ar(Q) ∩ V ar(c1 ) = V ar(Q, Q′ ) ∩ V ar(c′1 ) = ∅ .
Moreover, as c1 is a variant of c′1 , there exists a renaming γ such that
V ar(γ) ⊆ V ar(c1 , c′1 ) and

c1 = c′1 γ .

Let c′1 := p(s′1 , . . . , s′n ) ← B ′ . Then,
Q1 = Bθ

and

Q′1 = B ′ θ′ .

τ + is DN for c and c′1 is a variant of c. So, by Proposition 3.37, τ + is DN for c′1 . Let σ be the
substitution of Definition B.5.
′
Let q(v1′ , . . . , vm
) := B ′ . As B = B ′ γ, B has form q(v1 , . . . , vm ).
• For each hj 7→ uj i ∈ τ + (q), vj′ is an instance of uj (because τ + is DN for c′1 and (DN3) in
Definition 3.35.)
• For each j ∈ [1, m] \ Dom(τ + (q)) we have:
vj′ σηγθ = (vj′ σ)ηγθ = vj′ ηγθ
because, by (DN4) in Definition 3.35

V ar(vj′ ) ∩ V ar {s′i | i ∈ Dom(τ + (p))} = ∅

with Dom(σ) = V ar {s′i | i ∈ Dom(τ + (p))} . Moreover,
vj′ ηγθ = (vj′ η)γθ = vj′ γθ

because V ar(η) ⊆ V ar(Q, Q′ ) and V ar(c′1 ) ∩ V ar(Q, Q′ ) = ∅. Finally,
vj′ γθ = (vj′ γ)θ = vj θ
because B = B ′ γ.
38

Consequently, we have proved that
′
q(v1′ , . . . , vm
) is ∆[τ + ]-more general than q(v1 , . . . , vm )θ for σηγθ

i.e. that B ′ is ∆[τ + ]-more general than Bθ for σηγθ i.e. that
B ′ is ∆[τ + ]-more general than Q1 for σηγθ .

(6)

But, by the Technical Lemma B.7, σηγθ is a unifier of p(s′1 , . . . , s′n ) and p(t′1 , . . . , t′n ). As θ′ is an
θ′

mgu of p(s′1 , . . . , s′n ) and p(t′1 , . . . , t′n ) (because Q′ =⇒ Q′1 with c′1 as input clause), there exists δ
c

such that σηγθ = θ′ δ. Therefore, we conclude from (6) that B ′ is ∆[τ + ]-more general than Q1
for θ′ δ which implies that B ′ θ′ is ∆[τ + ]-more general than Q1 for δ i.e. that Q′1 is ∆[τ + ]-more
general than Q1 for δ. Finally, we have proved that Q′1 is ∆[τ + ]-more general than Q1 .
Using the Propagation Lemma B.8, the preceding result can be extended as follows.
θ′

Proposition B.10 (∆-Propagation) Suppose there exists a left derivation step Q′ =⇒ Q′1 . Then
c

Q′1 is ∆[τ + ]-more general than Q1 .
θ′

Proof. Let c′1 be the input clause used in Q′ =⇒ Q′1 . Take a variant Q′′ of Q such that
c

V ar(Q′′ ) ∩ V ar(c′1 ) = ∅
and a variant c′′1 of c such that

V ar(c′′1 ) ∩ V ar(Q′′ ) = ∅ .

Then, the left resolvent Q′′1 of Q′′ and c exists with the input clause c′′1 . So, for some θ′′ , we have
θ ′′

Q′′ =⇒ Q′′1 with input clause c′′1 . Consequently, we have:
c

θ

Q =⇒ Q1
c

θ ′′

and Q′′ =⇒ Q′′1 .
c

Q and Q′′ are instances of each other because Q′′ is a variant of Q. So, by the Propagation
Lemma B.8 used twice, Q′′1 is an instance of Q1 and Q1 is an instance of Q′′1 . So,
Q′′1 is a variant of Q1 .
But we also have

θ ′′

Q′′ =⇒ Q′′1
c

′

θ′

and Q′ =⇒ Q′1
c

+

with Q that is ∆[τ ]-more general than Q′′ (because Q′′ is a variant
with input clauses
and
′
of Q and Q is ∆[τ ]-more general than Q) and V ar(Q′′ ) ∩ V ar(c′1 ) = ∅. So, by Lemma B.9,
c′′1
+

c′1 ,

(7)

Q′1 is ∆[τ + ]-more general than Q′′1 .

(8)

Finally, from (7) and (8) we have: Q′1 is ∆[τ + ]-more general than Q1 .
B.8.4

Epilogue

Theorem 3.39 is a direct consequence of the following result.
Proposition B.11 (One Step ∆-Lifting) Let c′ be a variant of c variable disjoint with Q′ . Then,
θ′

there exist θ′ and a query Q′1 that is ∆[τ + ]-more general than Q1 such that Q′ =⇒ Q′1 with input
c

clause c′ .

39

Proof. Let c′1 := p(s′1 , . . . , s′n ) ← B ′ be a variant of c1 . Then there exists a renaming γ such that
V ar(γ) ⊆ V ar(c1 , c′1 ) and c1 = c′1 γ. Suppose also that
V ar(c′1 ) ∩ V ar(Q, Q′ ) = ∅ .
By the Technical Lemma B.7, p(s′1 , . . . , s′n ) and p(t′1 , . . . , t′n ) unify. Moreover, as V ar(c′1 ) ∩
V ar(Q′ ) = ∅, p(s′1 , . . . , s′n ) and p(t′1 , . . . , t′n ) are variable disjoint. Notice that the following claim
holds.
Claim B.12 Suppose that the atoms A and H are variable disjoint and unify. Then, A also
unifies with any variant H ′ of H variable disjoint with A.
Proof. For some γ such that Dom(γ) ⊆ V ar(H ′ ), we have H = H ′ γ. Let θ be a unifier of A and
H. Then, Aγθ = Aθ = Hθ = H ′ γθ, so A and H ′ unify.
Therefore, as c′ is a variant of c′1 and c′ is variable disjoint with Q′ , p(t′1 , . . . , t′n ) and the head
of c′ unify. As they also are variable disjoint, we have
θ′

Q′ =⇒ Q′1
c

for some θ′ and Q′1 where c′ is the input clause used. Moreover, by the ∆-Propagation Proposition B.10, Q′1 is ∆[τ + ]-more general than Q1 .

40

