Loop checks for logic programs with functions.
Two complete loop checking mechanisms have been presented in the literature for logic programs with functions: OS-check and EVA-check. OS-check is computationally efficient but quite unreliable in that it often misidentifies infinite loops, whereas EVA-check is reliable for a majority of cases but quite expensive. In this paper, we develop a series of new complete loop checking mechanisms, called VAF-checks. The key technique we introduce is the notion of expanded variants, which captures a key structural characteristic of in finite loops. We show that our approach is superior to both OS-check and EVA-check in that it is as efficient as OS-check and as reliable as EVA-check. Copyright 2001 Elsevier Science B.V.
Introduction
The recursive nature of logic programs leads to possibilities of running into innite loops with top-down
query evaluation. By an innite loop we refer to any innite SLD-derivation. An illustrative
example is the evaluation of the goal p(a) against the logic program
which leads to the innite loop
Another very representative logic program is
Currently on leave at Department of Computing Science, University of Alberta, Edmonton, Alberta, Canada
T6G 2H1. Email: ydshen@cs.ualberta.ca. Fax: (780) 492-1071.
against which evaluating the query p(g(a)) generates the innite loop
Loop checking is a long recognized problem in logic programming. 1 Although many loop
checking mechanisms have been proposed during the last decade (e.g. [1, 2, 6, 7, 9, 12, 14, 17, 19, 20,
22, 23]), a majority of them (e.g. [1, 2, 6, 7, 9, 12, 19, 20, 22, 23]) are suitable only for function-free
logic programs because they determine innite loops by checking if there are variant goals/subgoals
in SLD-derivations. Variant goals/subgoals are the same goals/subgoals up to variable renaming.
Hence, an innite loop like L 2 can not be detected because no variant goals/subgoals occur in the
derivation.
An important fact is that for function-free logic programs, innite loops can be completely
avoided by appealing to tabling techniques [4, 5, 18, 21, 23, 24]. However, innite loops with
functions remain unresolved even in tabling systems [13].
To our best knowledge, among all existing loop checking mechanisms only two can deal with
innite loops like L 2 . One is called OS-check (for OverSize loop check) [14] and the other EVA-check
(for Extended Variant Atoms loop check) [17].
OS-check, rst introduced by Sahlin [14, 15] and further formalized by Bol [3], determines
innite loops based on two parameters: a depth bound d and a size function size. Informally, OS-
check says that an SLD-derivation may go into an innite loop if it generates an OverSized subgoal.
A subgoal A is said to be OverSized if it has d ancestor subgoals in the SLD-derivation that have
the same predicate symbol as A and whose size is smaller than or equal to A. For example, if we
choose is an innite loop.
It is proved that OS-check is complete in the sense that it cuts all innite loops. However,
because it merely takes the number of repeated predicate symbols and the size of subgoals as its
decision parameters, without referring to the informative internal structure of the subgoals, the
underlying decision is fairly unreliable; i.e. many non-loop derivations may be pruned unless the
depth bound d is set su-ciently large.
EVA-check, proposed by Shen [17], determines innite loops based on a depth bound d and
generalized variants. Informally, EVA-check says that an SLD-derivation may go into an innite
loop if it generates a subgoal A 0 that is a generalized variant of all its d ancestor subgoals. A
subgoal A 0 is said to be a generalized variant of a subgoal A if it is the same as A up to variable
renaming except for some arguments whose size increases from A via a set of recursive clauses.
Recursive clauses are of the form like C 21 in P 2 , one distinct property of which is that repeatedly
applying them may lead to recursive increase in size of some subgoals.
1 There are two dierent topics on termination of logic programs. One is termination analysis (see [8] for a detailed
survey), and the other is loop checking (see [1, 23]). In this paper, we study loop checking.
Recursive increase in term size is a key feature of innite loops with functions. That is, any
innite loops with innitely large subgoals are generated by repeatedly applying a set of recursive
clauses. Due to this fact, EVA-check is complete and much more reliable than OS-check in the
sense that it is less likely to mis-identify innite loops [17].
OS-check has the obvious advantage of simplicity, but it is unreliable. In contrast, EVA-check
is reliable in a majority of cases, but it is computationally expensive. The main cost of EVA-check
comes from the computation of recursive clauses. On the one hand, given a logic program we need
to determine which clauses in it are recursive clauses. On the other hand, for any subgoals A and
A 0 in an SLD-derivation, in order to determine if A 0 is a generalized variant of A, we need to check
if A 0 is derived from A by applying some set of recursive clauses. Our observation shows that both
processes are time-consuming.
In this paper, we continue to explore complete loop checking mechanisms, which have proved
quite useful as stopping criteria for partial deduction in logic programming [11] (see [3] for the
relation between stopping criteria for partial deduction and loop checking). On the one hand, unlike
OS-check, we will fully employ the structural characteristics of innite loops to design reliable loop
checking mechanisms. On the other hand, instead of relying on the expensive recursive clauses,
we extract structural information on innite loops directly from individual subgoals. We will
introduce a new concept expanded variants, which captures a key structural characteristic of
certain subgoals in an innite loop. Informally, a subgoal A 0 is an expanded variant of a subgoal A
if it is a variant of A except for some terms (i.e. variables or constants or functions) in A each of
which grows in A 0 into a function containing the term.
The notion of expanded variants provides a very useful tool by which a series of complete loop
checking mechanisms can be dened. In this paper, we develop four such VAF-checks (for Variant
Atoms loop checks for logic programs with Functions) V AF 1 4 (d), where d is a depth bound.
loops based on expanded variants. V AF 2 (d) enhances V AF 1 (d) by
taking into account one (innitely) repeated clause. V AF 3 (d) enhances V AF 2 (d) with a constraint
of a set of (innitely) repeated clauses. And V AF 4 (d) enhances V AF 3 (d) with a constraint of
recursive clauses. The reliability increases from V AF 1 (d) to V AF 4 (d), but the computational
overhead increases, too. By balancing between the two key factors, we choose V AF 2 (d) as the best
for practical applications. V AF 2 (d) has the same complexity as OS-check, but is far more reliable
than OS-check. When d  2, V AF 2 (d) is reliable for a vast majority of logic programs. Moreover,
while no less reliable than EVA-check, V AF 2 (d) is much more e-cient than EVA-check (because
like OS-check it does not compute recursive clauses).
The plan of this paper is as follows. In Section 2, we review basic concepts concerning loop
checking. In Section 3, we introduce expanded variants and examine their properties. In Section
4, we dene four VAF-checks and prove their completeness. In Section 5, we make a comparison
of the VAF-checks with OS-check and EVA-check.
Preliminaries
In this section, we review some basic concepts concerning loop checking. We assume familiarity
with the basic concepts of logic programming, as presented in [10]. Here and throughout, by a
logic program we always mean a positive logic program. Variables begin with a capital letter,
and predicate symbols, function symbols and constants with a lower case letter. Let A be an
atom/function. The size of A, denoted jAj, is the count of function symbols, variables and constants
in A. We use rel(A) to refer to the predicate/function symbol of A, and use A[i] to refer to the
i-th argument of A, A[i][j] to refer to the j-th argument of the i-th argument, and A[i]:::[k] to refer
to the k-th argument of . of the i-th argument. For example, let
Denition 2.1 By a variant of an SLD-derivation (resp. a goal, subgoal, atom or function) D we
mean a derivation (resp. a goal, subgoal, atom or function) D 0 that is the same as D up to variable
renaming.
Denition 2.2 ([1, 3]) Let P be a logic program, G 0 a top goal and S a computation rule.
1. Let L be a set of SLD-derivations of P [ fG 0 g under S. Dene
that is a proper subderivation of Dg.
L is subderivation free if
2. A (simple) loop check is a computable set L of nite SLD-derivations such that L is closed
under variants and is subderivation free.
Observe that a loop check L formally denes a certain type of innite loops generated from
under S; i.e. an SLD-derivation G 0 is said to step into an innite
loop at G k if G 0 ) is in L. Therefore, whenever such an innite loop is detected, we
should cut it immediately below G k . This leads to the following denition.
Denition 2.3 Let T be the SLD-tree of P [ fG 0 g under S and L a loop check. Let
the SLD-derivation from the top goal G 0 to G 0 is in Lg. By applying L to T we obtain a new
SLD-tree which consists of T with all the nodes (goals) in CUT pruned. By pruning a node
from an SLD-tree we mean removing all its descendants.
In order to justify a loop check, Bol et al. introduced the following criteria.
Denition 2.4 ([1]) Let S be a computation rule. A loop check L is weakly sound if the following
condition holds: for every logic program P , top goal G 0 and SLD-tree T of P [ fG 0 g under S, if T
contains a successful branch, then contains a successful branch. A loop check L is complete if
every innite SLD-derivation is pruned by L. (Put another way, a loop check L is complete if for
any logic program P and top goal G 0
An ideal loop check would be both weakly sound and complete. Unfortunately, since logic
programs have the full power of the recursive theory, there is no loop check that is both weakly
sound and complete even for function-free logic programs [1]. As mentioned in the Introduction,
in this paper we explore complete loop checking mechanisms. So in order to compare dierent
complete loop checks, we introduce the following concept.
Denition 2.5 A complete loop check L 1 is said to be more reliable 2 than a complete loop check
logic program P and top goal G 0 , the successful SLD-derivations in TL1 are not less
than those in TL2 , and not vice versa.
It is proved that EVA-check is more reliable than OS-check [17]. In the Introduction, we
mentioned a notion of ancestor subgoals.
Denition 2.6 ([17]) For each subgoal A in an SLD-tree, its ancestor list ALA is dened recursively
as follows:
1. If A is at the root, then fg.
2. Let Am be a node in the SLD-tree, with A 1 being selected to resolve against a
clause A 0
1 . So M has a child node
Let the ancestor list of each A i at M be ALA i . Then the ancestor list ALB i  of each B i  at
N is ALA1 [ fA 1 g and the ancestor list ALA j  of each A j  is ALA j .
Obviously, for any subgoals A and B, if A is in the ancestor list of B, i.e. A 2 ALB , the proof
of A requires the proof of B.
Denition 2.7 Let G i and G k be two nodes in an SLD-derivation and A and B the selected
subgoals in G i and G k , respectively. We say A is an ancestor subgoal of B, denoted A ANC B, if
The following result shows that the ancestor relation ANC is transitive.
Theorem 2.1 If A 1 ANC A 2 and A 2 ANC A 3 , then A 1 ANC A 3 .
Proof. By the denition of ancestor lists, for any subgoal A if A 2 ALA 0 , then ALA  ALA 0 . So
ALA 3
. Thus A 1 2 ALA 2
ALA3
implies A 1 2 ALA 3
. That is, A 1 ANC A 3 . 2
In [17], it is phrased as more sound.
With no loss in generality, in the sequel we assume the leftmost computation rule. So the
selected subgoal at each node is the leftmost subgoal. For convenience, for any node (goal) G i ,
unless otherwise specied we use A i to refer to the leftmost subgoal of G i .
3 Expanded Variants
To design a complete and reliable loop check, we rst need to determine what principal characteristics
that an innite loop possesses. Consider the innite loop L 2 (see the Introduction) again.
We notice that for any i  0, the subgoal p(f(::f(f(g(a)))::)) at the (i + 1)-th node G i+1 is a
variant of the subgoal p(f(::f(g(a))::)) at the i-th node G i except for the function g(a) at G i that
grows into a function f(g(a)) at G i+1 . However, If we replace g(a) with a constant a in L 2 , then
p(f(::f(f(a))::)) at G i+1 is a variant of p(f(::f(a)::)) at G i except for the constant a at G i that
grows into a function f(a) at G i+1 . Furthermore, If we replace g(a) with a variable X in L 2 , then
p(f(::f(f(X))::)) at G i+1 is a variant of p(f(::f(X)::)) at G i except for the variable X at G i that
grows into a function f(X) at G i+1 .
As another example, consider the program
Let the top goal G Z). Then we will get an innite loop L 3 as depicted in Fig.1. Observe
that for any i > 0, the subgoal at G 2(i+1) is a variant of that at G 2i except that the variable Y at
G 2i grows into f(a; Y ) at G 2(i+1) .
Fig.1 The innite loop L 3 .
These observations reveal a key structural characteristic of some subgoals in an innite loop
with functions, which can be formalized as follows.
Denition 3.1 Let A and A 0 be two atoms/functions. A 0 is said to be an expanded variant of A,
denoted A 0 wEV A, if A 0 is a variant of A except that there may be some terms at certain positions
in A each A[i]:::[k] of which grows in A 0 into a function A 0 Such terms
like A[i]:::[k] in A are then called growing terms w.r.t. A 0 .
The following result is immediate.
Theorem 3.1 If A is a variant of B, then A wEV B.
Example 3.1 At each of the following lines, A 0 is an expanded variant of A because it is a variant
of A except for the growing terms GT .
However, at the following lines no A 0 is an expanded variant of A.
c) /*c and b are not uniable
is not in f(X)
to the case that p(X; X) is not a variant of p(Y; X)
In the above example, p(X; f(X)) is an expanded variant of p(X; X). It might be doubtful
how that would happen in an innite loop. Here is an example.
Example 3.2 Let P be a logic program and G
a top goal. We have the following innite loop:
Clearly, for any i  0, the subgoal A i+1 at G i+1 is the subgoal A i at G i with the second X growing
to f(X). That is, A i+1 is a variant of A i except for A i+1
Any expanded variant has the following properties.
3 This example is suggested by an anonymous referee.
Theorem 3.2 Let A 0 wEV A.
(1) jAj  jA 0 j.
(2) For any i, ., k, jA[i]:::[k]j  jA 0 [i]:::[k]j.
(3) When are variants.
When jAj 6= jA 0 j, there exists i such that jA[i]j < jA 0 [i]j.
Proof: (1) and (2) are immediate from Denition 3.1. By (2), when
That is, there is no growing term in A, so by Denition 3.1 A 0 is a variant
of A. This proves (3). Finally, (4) is immediate from (2). 2
These properties are useful for the computation of expanded variants. That is, if jA 0 j < jAj,
we conclude A 0 is not an expanded variant of A. Otherwise, if we determine if both are
variants. Otherwise, we proceed to their arguments (recursively) to nd growing terms and check
if they are variants except for the growing terms.
The relation \variant of" dened in Denition 2.1 yields an equivalent relation; it is re
exive
(i.e., A is a variant of itself), symmetric (i.e., A being a variant of B implies B is a variant of
A), and transitive (i.e., if A is a variant of B and B is a variant of C, then A is a variant of C).
However, the relation wEV is not an equivalent relation.
Theorem 3.3 (1) A wEV A.
(2) A wEV B does not imply B wEV A.
(3) A wEV B and B wEV C does not imply A wEV C.
does not imply B wEV C.
Proof. (1) Straightforward by Theorem 3.1. (2) Here is a counter-example: p(f(X)) wEV p(X),
but p(X) 6w EV p(f(X)). (3) Immediate by letting
and Immediate by letting
Although wEV is not transitive, the sizes of a set of expanded variants are transitively decreas-
ing. The following result is immediate from Theorem 3.2.
Corollary 3.4 If A wEV B and B wEV C, then jAj  jCj.
The concept of expanded variants provides a basis for designing loop checking mechanisms for
logic programs with functions. This claim is supported by the following theorem.
Theorem 3.5 Let be an innite SLD-derivation with
innitely large subgoals. Then there are innitely many goals G such that for any j  1,
Proof. Since D is innite, by the justication given by Bol [3] (page 40) D has an innite
subderivation D 0 of the form
where for any j  1, A 0
. Since any logic program has only a nite number of clauses,
there must be a set of clauses in the program that are invoked an innite number of times in D 0 .
be the set of all dierent clauses that are used an innite number of times in
must have an innite subderivation D 00 of the form
where for any j  1, A 00
and
any logic program has only a
nite number of predicate/function/constant symbols and D contains innitely large subgoals, there
must be an innite sequence of A 00
s in such that for any j  1, A i j ANC A i j+1
and A i j is a variant of A i j+1 except for a few terms in A i j+1 whose size increases. Note that such
an innite increase in term size in D 00 must result from some clauses in S that cause some terms
I to grow into functions of the form f(:::I:::) each cycle S is applied. This means that A i j is a
variant of A i j+1 except for some terms I that grow in A i j+1 into f(:::I:::), i.e., A i j+1 wEV A i j with
VAF-Checks
Based on expanded variants, we can dene a series of loop checking mechanisms for logic programs
with functions. In this section, we present four representative VAF-checks and prove their
completeness.
Denition 4.1 Let P be a logic program, G 0 a top goal, and d  1 a depth bound. Dene
in which there are up to d goals
that satisfy the following conditions:
(1) For each j  d, A i j ANC A i j+1 and A i j+1 wEV A i j .
(2) For any j  d, jA or for any j  d, jA
Theorem 4.1 (1) V AF 1 (d) is a (simple) loop check. (2) V AF 1 (d) is complete w.r.t. the leftmost
computation rule.
Proof. (1) Straightforward from Denition 2.2.
(2) Let be an innite SLD-derivation. Since P has
only a nite number of clauses, there must be a set of clauses in P that are invoked an innite
4 Note that (1) the order of clauses in fC j 1
is not necessarily the same as that in S, say fC
may contain duplicated clauses, say fC
C1g.
number of times during the derivation. Let be the set of all distinct clauses that
are applied an innite number of times in D. Then, by the proof of Theorem 3.5 D has an innite
sub-derivation of the form
where for any j  1, fC
distinguish between two cases.
(i) There is no subgoal in D whose size is innitely large. Because any logic program has only a
nite number of predicate symbols, function symbols and constants, there must be innitely
many atoms in T that are variants. Let fB 1 be the rst in T that
are variants. Then, by Theorem 3.1, for each 1  j  d B j+1 wEV B j with jB j+1
the conditions of V AF 1 (d) are satised, which leads to the derivation D being pruned at the
node with the leftmost subgoal B d+1 .
(ii) There is a subgoal in D with innitely large size. Then by Theorem 3.5, there must be innitely
many atoms in T that are expanded variants with growing terms. Let fB 1
be the rst in T such that for each 1  j  d, B j+1 wEV B j with jB j+1 j > jB j j.
Again, the conditions of V AF 1 (d) are satised, so that the derivation D will be pruned. 2
is complete for any d  1, taking d ! 1 leads to the following immediate
corollary to Theorem 4.1.
Corollary 4.2 For any innite SLD-derivation, there is an innite sub-derivation of the form
such that all A i j s satisfy the two conditions of V AF 1 (d) (d !1).
Observe that V AF 1 (d) identies innite loops only based on expanded variants of selected
subgoals. More reliable loop checks can be built by taking into account the clauses selected to
generate those expanded variants.
Denition 4.2 Let P be a logic program, G 0 a top goal, and d  1 a depth bound. Dene
in which there are up to d goals
that satisfy the following conditions:
(1) For each j  d, A i j ANC A i j+1 and A i j+1 wEV A i j .
(2) For any j  d, jA or for any j  d, jA
(3) For all j  d, the clause selected to resolve with A i j s is the same. g)
Theorem 4.3 (1) V AF 2 (d) is a (simple) loop check. (2) V AF 2 (d) is complete w.r.t. the leftmost
computation rule.
Proof. (1) Straightforward.
(2) By Corollary 4.2, for any innite SLD-derivation D, there is an innite sub-derivation in
D of the form
such that all A 0
s satisfy the rst two conditions of V AF 2 (d). Since any logic program has only
a nite number of clauses, there must be a clause C k that resolves with innitely many A 0
s in
the sub-derivation. Let A d be the rst d A 0
s that resolve with C k . The third condition of
(d) is then satised, so we conclude the proof. 2
Again, taking d !1 leads to the following immediate corollary to Theorem 4.3.
Corollary 4.4 For any innite SLD-derivation, there is an innite sub-derivation of the form
such that all A i j s satisfy the two conditions of V AF 1 (d) (d !1).
(d) is a special case of V AF 1 (d), any SLD-derivation pruned by V AF 2 (d) must be
pruned by V AF 1 (d), but the converse is not true. As an example, consider the SLD-derivation
It will be cut by V AF 1 (2) but not by V AF 2 (2) because condition (3) is not satised. This leads to
the following.
Theorem 4.5 V AF 2 (d) is more reliable than V AF 1 (d).
considers only the repetition of one clause in an innite SLD-derivation. More constrained
loop checks can be developed by considering the repetition of a set of clauses.
Denition 4.3 Let P be a logic program, G 0 a top goal, and d  1 a depth bound. Dene
in which there are up to d goals
that satisfy the following conditions:
(1) For each j  d, A i j ANC A i j+1 and A i j+1 wEV A i j .
(2) For any j  d, jA or for any j  d, jA
(3) For all j  d, the clause selected to resolve with A i j s is the same.
(4) For all j  d, the set S of clauses used to derive A i j+1 from A i j is the same. g)
Theorem 4.6 (1) V AF 3 (d) is a (simple) loop check. (2) V AF 3 (d) is complete w.r.t. the leftmost
computation rule.
Proof. (1) Straightforward.
(2) By Corollary 4.4, for any innite SLD-derivation D, there is an innite sub-derivation in
D of the form
such that all A 0
s satisfy the rst two conditions of V AF 3 (d). Obviously, the third condition of
is satised as well. Since any logic program has only a nite number of clauses, there
must be an innite sequence, A 0
l 1
l j
; :::, of A 0
in the sub-derivation such that the set S of
clauses used to derive A 0
l j+1
from A 0
l j
is the same. Let A be the rst
s.
The fourth condition of V AF 3 (d) is then satised. 2
Taking d !1 leads to the following immediate corollary to Theorem 4.6.
Corollary 4.7 For any innite SLD-derivation, there is an innite sub-derivation of the form
such that all A i j s satisfy the three conditions of V AF 2 (d) (d ! 1) and that for any j  1,
g.
Obviously, any SLD-derivation pruned by V AF 3 (d) must be pruned by V AF 2 (d). But the
converse is not true. Consider the SLD-derivation
It will be cut by V AF 2 (2) but not by V AF 3 (2) because condition (4) is not satised. This leads to
the following.
Theorem 4.8 V AF 3 (d) is more reliable than V AF 2 (d).
Before introducing another more constrained loop check, we recall a concept of recursive
clauses, which was introduced in [16].
Denition 4.4 ([16]) A set of clauses, fR are called recursive clauses if they are of the
form (or similar forms)
where for any 0 < i < m, q i (:::X i 1 :::) in R i 1 is uniable with q i (:::X i :::) in R i with an mgu
containing in Rm is uniable with q 0 (:::X 0 :::) in R 0 with an mgu
containing f(:::X m :::)=X 0 . Put another way, fR is a set of recursive clauses if starting
from the head of R 0 ( replacing X 0 with X) applying them successively leads to an inference chain
of the form
such that the last atom q 0 (:::f (:::X:::):::) is uniable with the head of R 0 with an mgu containing
Example 4.1 The sets of clauses, fC 11 g in P 1 , fC 21 g in P 2 , fC in P 3 , and fC 41 g in P 4 ,
are all recursive clauses.
Recursive clauses cause some subgoals to increase their size recursively; i.e., each cycle fR
is applied, the size of q 0 (:) increases by a constant. If fR can be repeatedly applied an
innite number of times, a subgoal q 0 (:) will be generated with innitely large size (note that not
any recursive clauses can be repeatedly applied). Since any logic program has only a nite number
of clauses, if there exist no recursive clauses in a program, there will be no innite SLD-derivations
with innitely large subgoals, because no subgoal can increase its size recursively. This means that
any innite SLD-derivation with innitely large subgoals is generated by repeatedly applying a
certain set of recursive clauses. This leads to the following.
Denition 4.5 Let P be a logic program, G 0 a top goal, and d  1 a depth bound. Dene
in which there are up to d goals
that satisfy the following conditions:
(1) For each j  d, A i j ANC A i j+1 and A i j+1 wEV A i j .
(2) For any j  d, jA or for any j  d, jA
(3) For all j  d, the clause selected to resolve with A i j s is the same.
(4) For all j  d, the set S of clauses used to derive A i j+1 from A i j is the same.
(5) If for any j  d jA contains recursive clauses that lead
to the size increase. g)
Theorem 4.9 (1) V AF 4 (d) is a (simple) loop check. (2) V AF 4 (d) is complete w.r.t. the leftmost
computation rule.
Proof. (1) Straightforward.
(2) By Corollary 4.7, for any innite SLD-derivation D, there is an innite sub-derivation E
in D of the form
such that all A 0
s satisfy the rst four conditions of V AF 4 (d) (d !1). Now assume that for any
j. Then E contains A 0
innitely large size. Such innitely increase in
term size in E must be generated by the repeated applications of some recursive clauses. This
means that there must be an innite sequence, A 0
l 1
l j
; :::, of A 0
s in E such that the clauses
used to derive A 0
l j+1
from A 0
l j
contain recursive clauses that lead to the size increase from A 0
l j
to
l j+1
. Let A be the rst
s. Then all A i j s satisfy the ve conditions of
When d !1, we obtain the following corollary to Theorem 4.9.
Corollary 4.10 For any innite SLD-derivation, there is an innite sub-derivation of the form
such that for any j  1, A g, and for
all or for all where the size increase results from the
application of a set of recursive clauses in fC k ; :::; C n j g.
is an enhancement of V AF 3 (d), any SLD-derivation pruned by V AF 4 (d) must
be pruned by V AF 3 (d). But the converse is not true. Consider the program that consists of the
clauses p(f(a)). The SLD-derivation
p(a) )C1 p(f(a)) )C2 2
will be cut by V AF 3 (1) but not by V AF 4 (1) because there are no recursive clauses in the program.
So we have the following result.
Theorem 4.11 V AF 4 (d) is more reliable than V AF 3 (d).
Example 4.2 Let us choose the depth bound d = 1. Then by applying any one of the four VAF-
checks, all the four illustrating innite loops introduced earlier, will be cut
at some node. That is, L 1 , L 2 and L 4 will be pruned at G 1 (the second node from the root), and
pruned at G 4 .
Example 4.3 Consider the following list-reversing program (borrowed from [3])
and the top goal G Z). Note that C 53 is a recursive clause.
Again, let us choose d = 1. After successively applying the clauses C 52 , C 53 and C 53 , we get the
following SLD-derivation:
It is easy to check that there is no expanded variant, so we continue to expand G 3 . We rst apply
C 51 to G 3 , generating a successful node 2; we then apply C 52 to G 3 , generating a node
As A 3 ANC A 5 and A 5 wEV A 3 with jA 5 are satised, which stop expanding
G 5 . We then apply C 53 to G 3 , generating a node
Obviously, A 3 ANC A 6 and A 6 wEV A 3 with jA 6 j > jA 3 j where the size increase of A 6 is via the
recursive clause C 53 , so V AF 1 4 (1) are satised again, which stop expanding G 6 . Since V AF 1 4 (1)
cut all innite branches while retaining the (shortest) successful SLD-derivation
they are weakly sound for g.
Observe that each condition of the above VAF-checks captures one characteristic of an innite
loop. Obviously, except (1) and (5), all the conditions (2) (4) make sense only when d > 1.
Because expanded variants capture a key structural characteristic of subgoals in innite loops, all
the VAF-checks with are weakly sound for a majority of representative logic programs (see
the above examples). However, considering the undecidable nature of the loop checking problem,
choosing d > 1 would be safer. 5 The following example, although quite articial, illustrates this
point.
Example 4.4 Consider the following logic program
p(f(a)). C 62
and the following successful SLD-derivation D for the top goal G
5 As mentioned by Bol [3], the question of which depth bound is optimal remains open. However, our experiments
show that V AF2(2) is weakly sound for a vast majority of logic programs.
Obviously, p(a) ANC p(f(a)), p(f(a)) wEV p(a), and C 61 is a recursive clause. If we choose
the derivation D will be pruned at G 1 by all the above four VAF-checks. That is, V AF 1 4 (1) are
not weakly sound for this program. Apparently, V AF 1 4 (2) are weakly sound.
Observe that from V AF 1 (d) to V AF 4 (d), the reliability increases, but the computational overhead
increases as well. Therefore, we need to consider a trade-o in choosing among these VAF-
checks. For practical applications, when d > 1 we suggest choosing the VAF-checks in the following
(d). The basic reasons for such a preference are
(i) our experience shows that V AF 2 (2) is weakly sound for a vast majority of logic programs, and
(ii) the check of condition (3) of V AF 2 (d) takes little time, whereas the check of recursive clauses
(condition (5) of V AF 4 (d)) is rather costly.
5 Comparison with OS-Check and EVA-Check
Because OS-check, EVA-check and V AF 1 4 (d) are complete loop checks, we make the comparison
based on the two key factors: reliability and computational overhead.
5.1 Comparison with OS-Check
We begin by recalling the formal denition of OS-check.
Denition 5.1 ([3, 14]) Let P be a logic program, G 0 a top goal, and d  1 a depth bound. Let
size be a size-function on atoms. Dene
in which there are up to d goals
such that for any 1  j  d
There are three versions of OS-check, depending on how the size-function size is dened [14, 3].
In the rst version, atoms A and B, so condition (2) will always hold
and thus can be ignored. In the second version, atom A. And in the third
version, for any atoms A and B with the same arity n,
jA[i]j  jB[i]j. Obviously, the third version is more reliable than the rst two versions so we can
focus on the third version for the comparison.
OS-check is complete [3], but is too weak in that it identies innite loops mainly based on the
size-function, regardless of what the internal structure of atoms is. Therefore, in order to increase
its reliability, we have to choose the depth bound d as large as possible. For example, in [14]
However, because the internal structure of atoms with functions may vary
drastically in dierent application programs, using only a large depth bound together with the
size-function as the loop checking criterion could in general be ineective/ine-cient. For example,
when applying OSC(10; size) to the programs would generate a lot of redundant
nodes. The following example further illustrates this fact.
Example 5.1 Consider the following logic program and top goal:
100). C 7;100
The successful SLD-derivation for is as follows:
| {z }
It is easy to see that OSC(d; size) is not weakly sound for this program unless we choose d  100.
In contrast, in our approach the common structural features of repeated subgoals in in-
nite loops are characterized by expanded variants. Based on expanded variants the VAF-checks
are weakly sound with small depth bounds (e.g. d  2) for a majority of logic
programs. For instance, V AF 1 4 (1) are weakly sound for P 7 in the above example, which shows a
dramatical dierence.
The above discussion is summarized in the following results
Theorem 5.1 Let size be the size-function of the third version of OS-check. For any atoms A and
B, A wEV B implies size(B)  size(A).
Proof. Immediate from Theorem 3.2. 2
Theorem 5.2 For any 1  i  4, V AF i (d) is more reliable than OSC(d; size).
Proof. By Theorem 5.1 and Corollary 3.4, OSC(d; size) will be satised whenever condition (1)
of V AF i (d) holds. So any SLD-derivations pruned by V AF i (d) will be pruned by OSC(d; size)
as well. But the reverse is not true. As a counter-example, when d < 100, the SLD-derivation in
Example 5.1 will be pruned by OSC(d; size) but not by V AF i (d). 2
We now discuss computational overhead. First note that in both OS-check and the VAF-
checks, the ancestor checking, A i j ANC A i j+1 , is required. Moreover, for each ancestor subgoal
A i j of A k , in OSC(d; size) we compute
Although the computation of expanded variants is a little more expensive than
that of the size-function, both are processes of two strings (i.e. atoms). Since string processing
is far faster than ancestor checking (which needs to scan the goal-stack), we can assume that the
two kinds of string computations take constant time w.r.t. scanning the goal-stack. Under such an
assumption, the complexity of OSC(d; size) and V AF 1 2 (d) is the same (note that the check of
conditions (2) and (3) of the VAF-checks takes little time).
Since the check of condition (4) of the VAF-checks requires scanning the goal-stack, V AF 3 (d)
is more expensive than OSC(d; size). Furthermore, condition (5) of the VAF-checks, i.e. the
computation of recursive clauses, is quite expensive because on the one hand, given a logic program
we need to determine which clauses in it are recursive clauses, and on the other hand, for two
subgoals A i j and A i j+1 with jA in an SLD-derivation, we need to nd if the size
increase from A i j to A i j+1 results from some recursive clauses. This means that V AF 4 (d) could be
much more expensive than OSC(d; size).
The above discussion further suggests that V AF 2 (d) is the best choice (balanced between
reliability and overhead) among OSC(d; size) and V AF 1 4 (d).
5.2 Comparison with EVA-Check
We begin by reproducing the denition of EVA-check.
Denition 5.2 ([17]) Let P be a logic program, G 0 a top goal, and d  1 a depth bound. Dene
in which there are up to d goals
such that for any 1  j  d
(2) A k is a generalized variant of A i j .g)
Here, a subgoal A 0 is said to be a generalized variant of a subgoal A if it is a variant of A except
that there may be some arguments whose size increases from A via a set of recursive clauses.
The following characterization of generalized variants is immediate from the above denition
and Denition 3.1.
Theorem 5.3 For any subgoals A 0 and A in an SLD-derivation, A 0 is a generalized variant of A
if and only if A 0 wEV A and if jA 0 j > jAj then the size increase is via a set of recursive clauses.
EV A(d) relies heavily on recursive clauses, so its complexity is similar to V AF 4 (d). Since
the computation of recursive clauses is too expensive, we will not choose EV A(d) in practical
applications unless it is more reliable than some V AF i (d). However, the following example shows
that EV A(d) can not be more reliable than any of the four VAF-checks.
Example 5.2 Consider the following logic program and top goal:
p(f(a)). C 83
A successful SLD-derivation for is as follows:
It can be easily seen that fC 81 ; C 82 g and fC 82 g are two sets of recursive clauses. Let us choose
2. Then A 2 is a generalized variant of both A 0 and A 1 , so EV A(2) will cut the derivation at
. However, this SLD-derivation will never be cut by any V AF i (2) because condition (2) of the
VAF-checks is not satised (i.e. we have jA
6 Conclusions
We have developed four VAF-checks for logic programs with functions based on the notion of
expanded variants. We observe that the key structural feature of innite loops is repetition (of
selected subgoals and clauses) and recursive increase (in term size). Repetition leads to variants
(because a logic program has only a nite number of clauses and predicate/function/constant
recursive increase introduces growing terms. The notion of expanded variants
exactly catches such a structural characteristic of certain subgoals in innite loops. Due to this,
the VAF-checks are much more reliable than OS-check and no less reliable than EVA-check even
with small depth bounds (see Examples 5.1 and 5.2). On the other hand, since the structural
information is extracted directly from individual subgoals, without appealing to recursive clauses,
the VAF-checks (except V AF 4 (d)) are much more e-cient than EVA-check.
In balancing between the reliability and computational overhead, we choose V AF 2 (d) as the
best one for practical applications. Although V AF 2 (2) is reliable for a vast majority of logic
programs, due to the undecidability of the loop checking problem, like any other complete loop
checks, V AF 2 (d) in general cannot be weakly sound for any xed d. The only way to deal with this
problem is by heuristically tuning the depth bound in practical applications. Methods of carrying
out such a heuristic tuning then present an interesting open problem for further study.

Acknowledgements

We thank the anonymous referees for their constructive comments, which have greatly improved the
presentation. The rst author is supported in part by Chinese National Natural Science Foundation
and Trans-Century Training Programme Foundation for the Talents by the Chinese Ministry of
Education.



--R

An analysis of loop checking mechanisms for logic programs
Towards more e-cient loop checks
Loop checking in partial deduction
Tabulated resolution for the Well-Founded semantics
Tabled evaluation with delaying for general logic programs
Eliminating unwanted loops in Prolog
A further note on loops in Prolog
Termination of logic programs: the never-ending story
Redundancy elimination and loop checks for logic pro- grams
Foundations of Logic Programming
Partial evaluation in logic programming
On eliminating loops in Prolog
The XSB Programmer's Manual (Version 1.8)
The mixtus approach to automatic partial evaluation of full Prolog
Mixtus: an automatic partial evaluator for full Prolog
Verifying local strati
An extended variant of atoms loop check for positive logic programs
Linear tabulated resolution for the well founded semantics
An abstract approach to some loop detection problems

OLD resolution with tabulation

the power of logic
Memoing for logic programs
--TR
Controlling recursive inference
OLD resolution with tabulation
Efficient loop detection in Prolog using the tortoise-and-hare technique
Foundations of logic programming; (2nd extended ed.)
Recursive query processing: the power of logic
An analysis of loop checking mechanisms for logic programs
Partial evaluation in logic programming
The Mixtus approach to automatic partial evaluation of full Prolog
Towards more efficient loop checks
Memoing for logic programs
Mixtus
Sound and complete partial deduction with unfolding based on well-founded measures
Redundancy elimination and loop checks for logic programs
Tabled evaluation with delaying for general logic programs
An extended variant of atoms loop check for positive logic programs
An abstract approach to some loop detection problems
Linear Tabulated Resolutions for the Well-Founded Semantics

--CTR
Yi-Dong Shen , Jia-Huai You , Li-Yan Yuan , Samuel S. P. Shen , Qiang Yang, A dynamic approach to characterizing termination of general logic programs, ACM Transactions on Computational Logic (TOCL), v.4 n.4, p.417-430, October
Etienne Payet , Fred Mesnard, Nontermination inference of logic programs, ACM Transactions on Programming Languages and Systems (TOPLAS), v.28 n.2, p.256-289, March 2006
Alexander Serebrenik , Danny De Schreye, Inference of termination conditions for numerical loops in Prolog, Theory and Practice of Logic Programming, v.4 n.5-6, p.719-751, September 2004
logic programming;loop checking