J. Software Engineering & Applications, 2010, 3: 198-207
doi:10.4236/jsea.2010.33025 Published Online March 2010 (http://www.SciRP.org/journal/jsea)
Incremental Computation of Success Patterns of
Logic Programs
Lunjin Lu
Department of Computer Science and Engineering, Oakland University, Rochester, USA.
Received October 28th, 2009; revised November 26th, 2009; accepted November 30th, 2009.
ABSTRACT
A method is presented for incrementally computing success patterns of logic programs. The set of success patterns of a
logic program with respect to an abstraction is formulated as the success set of an equational logic program modulo an
equality theory that is induced by the abstraction. The method is exemplified via depth and stump abstractions. Also
presented are algorithms for computing most general unifiers modulo equality theories induced by depth and stump
abstractions.
Keywords: Incremental Analysis, Success Patterns, Abstract Interpretation, Depth Abstract, Stump Abstraction, Logic
Programs
1. Introduction
In abstract interpretation, program analyses are viewed as
program execution over non-standard data domains.
Cousot and Cousot first laid solid logical foundations for
abstract interpretations [1,2]. Their idea is to define a
collecting semantics for a program which associates each
program point with the set of all storage states that are
possibly obtained when the execution reaches the point.
In practice, an abstraction of the collecting semantics is
calculated by simulating over a non-standard data do-
main the computation of the collecting semantics over
the standard data domain. The standard data domain and
the non-standard domain are called the concrete domain
and the abstract domain respectively.
Abstract interpretation has been used to perform vari-
ous analyses of logic programs such as occur check
analysis [3], mode analysis [4–6], sharing analysis [7,8]
and type analysis [6,9,10]. Further more, a number of
abstract interpretation frameworks for logic programs
have been brought about [5], Jones et al. [11], Bruy-
nooghe [9] and Marriott et al. [12]. With an abstract in-
terpretation framework, the design of a particular analy-
sis reduces to the design of an abstract domain and a
number of abstract operations on the abstract domain.
The safeness of the analysis is verified by formalizing a
correspondence between the concrete domain and the
abstract domain and proving that the abstract operations
safely simulate the concrete operations with respect to
the correspondence. The correspondence between the
abstract domain and the concrete domain can be formal-
ized either as an abstraction (function) from the concrete
domain to the abstract domain, or as a concretization
(function) from the abstract domain to the concrete do-
main, or as a joined pair of abstraction and concretization,
or as a relation between the concrete domain and the ab-
stract domain. We assume that the correspondence is
given as a surjective abstraction from the domain of con-
crete terms into a domain of abstract terms1.
A program analysis is currently performed with re-
spect to a fixed abstraction; and different analyses corre-
sponding to different abstractions are performed sepa-
rately even when there is a strong relationship between
them. Take depth abstractions for example, a depth 3
analysis will be performed separately from a depth 2
analysis even if the result of the depth 2 analysis can be
used to perform the depth 3 analysis, as we will show
later in this paper. This paper is concerned with refining
program analyses whereby the result of a coarser analysis
corresponding to a stronger abstraction is used to obtain a
finer analysis corresponding to a weaker abstraction. In
particular, we are concerned with obtaining finer success
patterns of a logic program from coarser success patterns
of the same program. We introduce an ordering relation
on abstractions of terms. We then argue, for a class of
1In case an abstraction is not surjective, we can always construct a new
of abstract terms by eliminating those abstract terms that are not im-
ages of any concrete term under the abstraction. The abstraction is a
surjective abstraction from the domain of concrete terms to the new
domain of abstract terms.

Incremental Computation of Success Patterns of Logic Programs199
abstractions, that the set of success patterns of a logic
program P with respect to an abstraction α is tantamount
to the success set of the equational logic program
where E
α is an equality theory induced by α.
Therefore, either the fixpoint semantics or the procedural
semantics defined for equational logic programs can be
used to compute success patterns of logic programs.
From this observation, the success patterns of a logic
program P can be computed by incremental refinement.
A set of coarser success patterns of P relative to a
stronger abstraction α1 can be obtained by computing the
fixpoint semantics of the equational logic pro-
gram . If the success patterns are not fine enough
for the application at hand, candidates for finer success
patterns relative to a weaker abstraction α2 can be gener-
ated from the coarser success patterns and verified by
using either the procedural or the fixpoint semantics of
equational logic program. This refinement proc-
ess is repeated until success patterns are fine enough for
the application.
α
PE
P1
α
E
2
α
PE
The remainder of this paper is organized as follows.
Section 2 presents a fixed-point and a procedural abstract
semantics of logic programs for a class of abstractions
and lays a foundation for incremental refinement of suc-
cess patterns of logic programs with respect to that class
of abstractions. Sections 3 and 4 devote to incremental
refinement of success patterns of logic programs for
depth abstractions and stump abstractions respectively. In
Section 5, we conclude this paper with a summary of the
paper and some points to future work in analysis refine-
ment.
2. A Foundation for Incremental Refinement
Let be respectively a set of function symbols,
a set of predicate symbols and a denumerable set of
variables. denotes the set of terms con-
structible from and V, and denotes the
set of atoms constructible from and where
is a set of terms. The Herbrand universe are
theHerbrand base of a logic program
Vars,,
Term ),( V


),( SAtom 
S S

P
are
),(= Term

and
),(= 



Atom
respectively. Let . Let be
a set of abstract terms, and
),(= VarsTermTerm 

Term

be an abstraction from
to . Term

Term

induces an equivalence relation
on Term ,

))(=)((=)(2121 tttt






/
=TermTerm
. So, abstract
terms in is identified with equivalence classes of
. That is, .

Term



is called stable if
))().((.,




ststSubTermst 





where
is the set of substitutions. Let . is an
equality theory on Term . We extend
Sub
}{=

E

E

to an
abstraction from ),( TermAtom

to
as follows:
)

Term,(
))
n
t
Atom
,),((=)),,(( 11 ntpttp(



 .


and are extended accordingly.

E
) (,AtomorTermst Let

and Sub


,.

is an
-unifier of and if

Ets



stt

E E
. and are
-unifiable if they have one or more -unifiers.
s


is more general than

with respect to , denoted as

E



E

, iff there is an Sub


such that



XX

for all VarsX

. An -unifier

E

of t and s is a
maximally general -unifier (-mgu) of

E

E
t
and s iff,
for any other -unifier

E

of t and s,



E
 .
2.1 Fixpoint and Procedural Abstract Semantics
This section presents a fixpoint and a procedural abstract
semantics of a definite logic program
P
with respect to
a stable abstraction

. It is well known that the success
set of
P
is tantamount to the least fixpoint of the
following function )()(:  

T
1
()={:.,, m
by van
Emden and Kowalski [13].
.
I
HHBBP

T


1} m
BIBI

 

 (1)
For any logic program
P
and any abstraction

,
is an equational logic program. The fixpoint
semantics of given by Jaffar et al. [14] is

EP 

EP 


T()(: /


  with ) /





T
#
1
()={[]:.,
α
α
IHσσ
being defined as follows.
,
m.
H
BBP
 T
##
1
[][ ]}
m
α
BσIBσ

α
I


]([)(



 TAAEP 


) 
(2)
According to Jaffar et al. [14],
for any

A 

T. We adopt as the fixpoint
abstract semantics of
P
relative to

. The following
lemma states the is a safe approximation of
with respect to


T
 T

.
Lemma 1 If

is a stable abstraction then
)][.( 


 TT AAA 

.
The procedural semantics of an equational logic
program is the equational SLD resolution with

EP 

Incremental Computation of Success Patterns of Logic Programs 200
respect to the equality theory , denoted as .
plays same role for as SLD for

E
P

SLD

SLD

E
P
.
differs from SLD in the sense that, in ,
-unification plays the role of normal unification in
SLD. In the following, we adapt so that it works
on equivalence classes of

SLD

E

SLD

SLD


on . Define Atom
)(=][=][





tt 

t. Notice that equivalence classes
of terms (resp. atoms) are identified with abstract terms
(resp. abstract atoms). The application of a substitution

to an equivalence class can accomplished by
applying


][t

to any term in taking t


][t




][ as
the result because of the stability of
t

which also
allows us to define an -mgu of and as
an -mgu of

E


][t


][s

E
t
and
s
. The basic step in can
now be defined as follows.

SLD
#
p
A
#
W

E
Definition 1 Let and
be a variant of a clause of P.
is called -derived from and using -mgu
#,,
j
A
#,
#C
1
A
#
G
,G
q
BB ,,
1

E
HC 

if (1)

is an -mgu of and

E#
j
A)(H

; and (2)
., # 
p
A,, #
1

j
A )(,q B,  )
1
B(,,,#
1
#
1

j
AA 
(α PE
=
#
W 
It is proven by Jaffar et al. [14] that
)( []
αα
A



]

SLD

[A
)
]
SLD
AP
[

where denotes that is provable
from P using . This implies that can be
used to verify whether an abstract atom is a
success pattern of P with respect to


]AP SLD


[
SLD
A



according to
lemma 1. In summary,
(PEα) ([]AA )
α
ω([] )PA
α
SLD

α
α

T
(3)
2.2 Foundation for Incremental Refinement
Let 1

and be two abstractions. Define
2

12

 
12
iff for all . When ss tt

2


1Termt,s

 ,
we say that 1

is weaker or finer than and that
is stronger or coarser than
2

2

1

. Note that if 12


1
α
 then
for any . In other words,
2
][


t
1
][

tTermt 

is
a finer partition on (and ) than Term Atom2
α

. If
12

  then 1
α
E2
α
E. Therefore, we have
12
() 1
α
(( )PEαα
2
(
α
PE)) (4)
By Equations (3) and (4),
))]([)].(([)( 2
2
1
1
21





  TT AAA HB
(5)
Equation (5) lays a foundation for incremental refine-
ment of success patterns of logic programs. An initial set
of the success patterns of a logic program
P
can be
obtained by computing which is a safe appro-
ximation of relative to


T
 T

. If the success
patterns in are not finer enough for the
application at hand then finer success patterns can be
computed by a generate-and-test approach as follows.
Firstly, a weaker abstraction


T


 
is formed and candi-
dates elements for are generated from .
The formation of


T 

T


and generation of candidates
elements for can be done by splitting one or
more equivalence classes of . Secondly, is
used to verify if a particular candidate element is in
. This process of refinement is repeated until
success patterns are fine enough.




T




SLD




T
If αα

, for any , i.e., the



][][AA A



equivalence class including
A
is contained in the


equivalence class including
A
. Let be a
refinement operator that splits an equivalence class
into the set of


 ,
R


C



equivalence classes contained in
. C
}=][:]{[=)(
,CAAACR

 


HB
Then candidates elements for can be
generated from by applying to
where is defined .




T
*
, 

R
,,
()
cs αα
RC




T 

T
*
, 

R*()=
αα
RS
For a given set S of


equivalence classes,
returns the union of the sets of equivalence classes
resulting from applying to equivalence
classes in .
*
, 

R





 ,
R


S
2.3 An Example of Incremental Refinement
We illustrate the idea of incremental refinement of
success patterns of logic programs by means of depth
abstractions proposed by Sato et al. [15]. A depth
abstraction partitions Term into a finite number of
equivalent classes. Two terms belong to the same class
iff their term trees are identical to a certain depth n,
called the depth of abstraction. For example,
is equivalent to to depth 2.
Let denote depth abstraction. replaces
each sub-term of t at depth n with a _ that denotes any
))(),(( bgafh
n
d
))(),(( agbfh
)(tdn n

Incremental Computation of Success Patterns of Logic Programs201
term. Letting , we have p
=))(bg (_))(_),(=))(),(((),(((11 gfpagbfpdafpd .
Deferring a formal presentation of depth abstractions
until Section 3, we now show how can be used
when it is necessary to increase the depth of abstraction.

SLD
Example 1 Let 1 =d

and P={a(f(c)). b(f(h(c))). p(x)
 a(x), b(x). }. We have ,  =0
1
d
T
(_))}({=1
1fb
dT(_)),( fa
(_)),(fa
(_)),(fa
=3
1
dT
 
2
d
T
2
d
2
,d
(_)}(_), hf
(_))),(( ff
(,(_))) fp
2
d
=
2
d
 T
))(()), cfb
(
2bd
,
(_))}((_)),({=2
1fpfb
dT,
(_))}((_)),({=3
1fpfb
dT,
and
(_))}((_)),((_)),({=
1fpfbfa
dT
 .
Suppose now we want to be more precise and decide
to compute . Note that the set of ground atoms
that approximates is a subset of the set of
ground atoms that approximates. Instead of
computing the least fixpoint of , we compute
by a generate-and-test approach. We first
generate a set of candidate elements for and
then use resolution to eliminate false candi-
dates. The generation of candidates is accomplished by
applying the refinement operator defined in
Section 3 to elements in . For each element in
, generates a set of candidates by subs-
tituting each occurrence of _ with every element from
. Thus, the set of candidates is

SLD
1
d
,

2
d
T
 
 R
{=
1
/c
d

 
1
d
T
1
d
T
2
d
T
1
d
R
2
d
T
1
d
T

 
2
d
T
2
,d
 
{ (_))),(()),(((_))),(()),((ffbcfbhfaacfa
(_)))(((_))),(()),((( hfpffpchfb }.
After eliminating candidates that are not provable from
P using ,we have SLD
(_)))}(()),(({ hfbcfa .
p(f(c)) has been eliminated as follows. First, ←p(f(c))
is resolved with the clause resulting
in .Then goal is resolved
with the unit clause . However,
cannot be resolved with b(f(h(c))) because d2(b(f(c)))=
d2(b(f(c))) while .
)(),()( xbxaxp 
))(( cfa
))(c
(_)))((=)))) hfbc
(( cfa
(
(fa
((hf
))(( cfb
The following two sections demonstrate incremental
refinement of success patterns of logic programs by
considering two families of abstractions, namely depth
abstractions and stump abstractions.
3. Depth Abstractions
The idea of enumerating success patterns of logic
programs to a certain depth is due to Sato and Tamaki
[15]. Depth abstraction has been used to ensure
termination of an analysis, e.g. [10,16,17]. All terms
(resp. atoms) identical to a certain depth are considered
equivalent. For example, both and
have main functor and the
first and the third of their arguments are same. Both of
their second arguments have as main functor. If
this information is enough, then we can use either
or as a repre-
sentative of them. Since we are not interested in the
arguments of we shall replace each argument of
with a special symbol _, denoting any term, that is,
we use f(a,g(_,_),b) to represent both
and .actually repre-
sents an infinite number of terms.
)(0),1),(,( bhgaf
/3f
/2
)(0))),( bhh
(0),1),(,(hgaf
)_),(_, b
)(0))),((2,,(bhhgaf
)(0),1),(,( bhgaf
/2g
/2g
(0))),((2,,(hhgaf
g
(2,
,g
,(gaf
)b(af
)b
This section defines depth abstractions, constructs a
refinement operator and an equational unification algo-
rithm for such abstractions, and exemplifies incremental
refinement of success patterns with respect to depth
abstractions.
3.1 Depth Abstractions
Let be a term. Then t is a depth 0
sub-term of t, and a term s is a depth k sub-term of t if s
is a depth
),,(=1m ttft
1)(

k sub-term of ti for some mi

1.
Definition 2 Let t be a term. The depth k abstraction of
t, denoted by , is obtained by replacing each depth
k sub-term of t with an _.
)(tdk
0>))(,),((=)),,((
0=_=)(
1111ktdtdfttfd
ktd
mkkmk
k
 
For instance, the depth 2 abstraction of (( ,),
f
gXY
( ()))
g
hZ
(f
is , and its depth 3 abstrac-
tion is .
(_))_),(_,( ggf
(_)))(),, hgYX(g
Lemma 2 For any , dk is stable. 0k
3.2 A Refinement Operator for Depth
Abstractions
Let be an abstract term denoting an equiva-
lence class.
#
t1 k
d
)){_},((){_},(:
~
 TermTermd 
defined below splits by replacing each _ in with
an abstract term from in every possible way.
#
t# t
1
dl


Incremental Computation of Success Patterns of Logic Programs 202
}|_),(_,{=(_)
~
ffd 
)}(.1|),,({=)),,((
~
11 jjmm tdsmjssgttgd 
Its extension yields a refinement operator
))){_},(,(:
~
TermAtomd
)){_},(,(( 

TermAtom.
)}(
~
.1 | ),,({=)),,((
~
11 jjnn tdsnjsspttpd 
)){_},(()){_},((:
~
* TermTermd 
~
is the extension of to sets of abstract atoms. d
)(
~
=)(
~
#
#
*AdSd
SA


Lemma 3 If then  dR k
d
k
d
~
=
1
, and * ,1 dd
kk
R

for any .
*
=d
0k
3.3 An -Unification Algorithm
k
d
E
Now we present an -unification algorithm and prove
its correctness. The following algorithm for -unifi-
cation results from modifying Robinson's unification
algorithm [18]. Function is true iff
k
d
E
k
d
E
),,( tXkoccur
X
occurs in at any depth . tkj <
Algorithm 1 This algorithm decides if and
are -unifiable and, if -unifiable, returns an
-mgu of and .
1
t2 t
k
d
Ek
d
E
k
d
E1
t2 t
01 function Dunify(k,,) (
1
t2 t

,unifiable )
02 begin
03 if then 0=k),(),(  trueunifiable

04 else if or is a variablethen
1
t2 t
05 begin let X be the variable and t the other
term
06 if then tX = ),(),(

trueunifiable

07 else if then ),,( tXkoccur
{,,( XtXk })),(tDunifyunifiable 

08 else )})({,(),( tdXtrueunifiable k


09 end else
10 begin let t1 = f(x1,…,xn) and t2 = g(x1,…,xm)
11 if f ≠ g or m ≠ n then falseunifiable

else
12 begin ,
0j),(),( 0

trueunifiable

13 while and do mj <unifiable
14 begin 1

jj
15 ( unifuable,τj)←Dunify (k-1,xjσj-1,yjσj-1)
16 if then
unifiable jjj



1

17 end
18 m



19 end
20 end
21 return ),(

unifiable
22 end
The line 07 in algorithm 1 deals with -unification
of X and t where X occurs in t at some depth . This
does not necessarily mean failure of the -unification
of X and t. For instance,
k
d
E
k
d
E
)}
kj <
({= YfX

is a -mgu
of X and f(X). Algorithm 1 reduces the problem of
-unification of X and t into the problem of
-unification of X and .
1
d
E
k
d
E
k
d
E}{ tXt
Lemma 4 If two terms and are -unifiable,
then algorithm 1 terminates and gives a unique (module
renaming) -mgu of and . Otherwise, the
algorithm terminates and reports the fact.
1
t
1
t
2
t
2
t
k
d
E
k
d
E
3.4 Refinement of Success Patterns for Depth
Abstractions
All depth abstractions are comparable with respect to .
Abstractions corresponding to bigger depths are finer
than those corresponding to smaller depths. Formally,

Lemma 5 For any kj


0, .
kj
dd
Lemma 5 implies that, for any , if
then . This enables
us to refine success patterns of P by increasing abstra-
ction depth. Suppose that success patterns in
are not fine enough and it is necessary to compute
. Rather than throwing away and
computing from scratch, we compute
by
A
1k
d
T
 
1k
d
T
k
d
T
 

k
d
k
d
AT][
 
k
d
T

k
d
T
  


1
1
][k
d
k
d
AT
 
  
1) applying to resulting in a set of
candidate elements for since
*
~
d
k
d
T
 
1k
d
T

 
k
d
T
 
k
d
dT)(
~
1
*;
2) applying to eliminate those candidate
elements that are not provable from P using .
k
d
SLD
k
d
SLD
The following two examples illustrate incremental
refinement of success patterns of logic programs with
respect to depth abstractions.
Example 2 Let
={( ,),(,)(,),( ,), ((),())(,)}
P
pabpXYqXYqab qrXsYqXY


We have

Incremental Computation of Success Patterns of Logic Programs 203
(_))}(_),((_)),(_),(),,(),,({=4
(_))}(_),((_)),(_),(),,(),,({=3
(_))}(_),(),,(),,({=2
)},(),,({=1
=0
1
1
1
1
1
srpsrqbaqbap
srpsrqbaqbap
srqbaqbap
baqbap
d
d
d
d
d





T
T
T
T
T
11
=4={( ,),(,),( (_),(_)),( (_),(_))}
dd
ωpabqabqrsprsTT
Example 3 Let P be the same as example 2 and
suppose that success patterns in are not fine
enough. We compute as follows. We first apply
 
1
d
T
 
2
d
T
*
~
d to resulting in the following candidate
elements for .
 
1
d
T
2
d
T  
So,
(_)))((_)),(((_))),((_)),(()),((_)),(()),((_)),((
(_))),((_)),(((_))),((_)),(()),((_)),(()),((_)),((
(_))),(),(((_))),(),(()),(),(()),(),(((_))),(),((
(_))),(),(()),(),(()),(),(((_))),((_)),((
(_))),((_)),(()),((_)),(()),((_)),(((_))),((_)),((
(_))),((_)),(()),((_)),(()),((_)),(((_))),(),((
(_))),(),(()),(),(()),(),(((_))),(),((
(_))),(),(()),(),(()),(),((),,(),,(
sssrprssrpbssrpassrp
ssrrprsrrpbsrrpasrrp
ssbrprsbrpbsbrpasbrpssarp
rsarpbsarpasarpsssrq
rssrqbssrqassrqssrrq
rsrrqbsrrqasrrqssbrq
rsbrqbsbrqasbrqssarq
rsarqbsarqasarqbaqbap
We then applyto eliminate those candidate
2
d
SLD
elements that are not provable from P by using ,
2
d
SLD
we have
2
d

T = p(a,b),q(a,b),q(r(a)),s(b)),q(r(r(_)),s(s(_))),
p(r(a),s(b)),p(r(r(_)),s(s(_)))
(_)))((_)),(( ssrrq has not been removed because it is
provable from P by using . The -refutation
2
d
SLD 2
d
SLD
process is as follows.
(_)))((_)),((=
0ssrrqG
2)}(1/2),(1/{=
1)1,(1))(1),((=
{
0
0
YsYXrX
YXqYsXrqC


2))(2),((=
1YsXrqG 
2}3/3,3/{=
3)3,(3))(3),((=
{
1
1
YYXX
YXqYsXrqC


2)2,(=
2YXqG 
}2/,2/{=
),(=
{
2
2
bYaX
baqC


=
3
G
Variables 2
X
and 2
Y
in
2)}(1/2),(1/{=
0YsYXrX

,
occur neither in nor in the head of . They are
introduced by -unification to indicate that they can
be replaced by any other terms.
0
G
2
d
0
C
E
(_))))((_)),(( rssrp has been eliminated because it is
not a provable from P by using . The -
refutation process is as follows.
2
d
SLD 2
d
E
(_))))((_)),((
0rssrpG


1)1,(1)1,(=
0YXqYXpC 
2))}((1/2)),((1/{=
0YrsYXsrX

2)))((2)),(((
1YssXrrqG


1=((3),(3)) (3,3)CqrXsY qXY
1= {3 /(4),3 /(4)}XrXYsY

2=G( (4),(4))qrX sY

The -refutation fails because no clause head -
unifies with .
2
d
E2
d
E
4))(4),(( YsXrq
4. Stump Abstractions
Xu and Warren have introduced a family of abstractions,
called stump abstractions, that reflect recursiveness [19].
The idea is to detail each atom in to the extent in
which some function symbol has been repeated for a
given times.
 T
This section defines stump abstractions, constructs a
refinement operator and an equational unification
algorithm for such abstractions, and exemplifies
incremental refinement of success patterns of logic
programs with respect to stump abstractions.
4.1 Stump Abstractions
Let t be a term and s a sub-term of t. We define
as a function which, for each function symbol g in
),( tsfc

,
registers the number of nodes labelled by g in the path
from the root of the term tree of t to but excluding the
root of the term tree of s. Let where N is
the set of natural numbers. Define
)( Nw 
=wf

[()wfwf1]

 and if then 0>)( fw !=wf

Incremental Computation of Success Patterns of Logic Programs 204
[()wfwf1].Define
as follows. Ifthen
TermTermfc 
=),( tsfc
:(Σ)N
.0fts 

. If
and for some ),,(=1m ttft wts i=),fc(mi


1
then (,)=
f
cst w
),,(= 1k ssgs 
),( tsrd
= (tf
((3, 2),)=2rd ft
1
((
,, ))
wm
sf
t t
.Otherwise, is undefined. If
then the repetition depth of s in t, denoted
as is defined as.For instance,
letting,
, and .
f
(1),h
rd
t
,( tsrd
(
=(_,
fs

(g
),( tsfc
))(,( gtsfc
(1, 2)),(((1),ghfh
(1,2),(g1=)t
Termw 
=s
)(=) gw
!1 !
( ),,())
, _)
wfwfm
ts t
(3, 2))))f
N )(tsw
),,( 1k ssg
_),(_,g
( )0
() = 0
wf
fw
Definition 3 Let , and .
is obtained by replacing each sub-term
of t satisfying with .
Formally,
f




(_))(gr
w
)
=


1,{= grw
N 
Σ.()( )

(1)))))(((( gsgrsw
(, Nyx 
For instance, letting ,
.
1}0, s
=
Lemma 6 For any , sw is stable.
4.2 A Refinement Operator for Stump
Abstractions
Let and define
x
yf xfyf
yx
 .
As shown later,
x
ys s. Intuitively, the bigger
the limit for each function symbol, the weaker the
abstraction.
Definition 4 Define
)){_},((  Term)N(: s
as follows.
1
{(_,
{(,
f
ft
w
Σg

(, )=
(, ) =
f
f
,_)}
, )|
mj
t t

N
()=0
)}()0
wf
wf(!,swfg
f
sw
sw 
For given and , ),( fw
)){_},
s
w
s
(
is the
set of the abstract terms identifying the equivalence
classes of those ground terms whose main functors is f.

(
The following defined function
){_},()(:
~

Term NTerms
splits an equivalence class of ground terms for a coarser
stump abstraction into the set of equivalence classes of
ground terms for a finer stump abstraction.
Σ
(,_)=(, )
f
s
ws

)|
w
1 .
f 
mm

))={
11
(, ,(,(, ,(!,)}
jj
s
wgt tgsssj m s wgt

Its extension as in the following gives rise to a refine-
ment operator for stump abstractions
,{_}(,()(:
~




TermAtomNs 
))){_},(,(()) 



TermAtom
),,({=)),,(,(
~
11 mm sspttpws 
)},(
~
.1| jj twssmj




))){_},(,(()(:
~
* TermAtomNs 
))){_},(,(( 



TermAtom
is the extension of s
~
to sets of abstract atoms.
#
*#
(,)=(,)
As
s
wS swA

 
Lemma 7 For any
x
y , ),(
~
=
,ysR y s
x
s and
),(
~
=**
,ysR y s
x
s.
4.3 An -Unification Algorithm
w
s
E
The -unification algorithm is given in algorithm 2.
The function Sunif has three parameters. The first
parameter w maps each function symbol into the limit of
its repetition depth. The second and third parameters are
terms to be unified. For any variable X and term t,
is true iff X occurs in .
w
s
E
,(w),tXoccur )(tsw
Algorithm 2 This algorithm decides if t1 and t2 are
-unifiable and, if so, returns an -mgu of t1 and t2.
w
s
Ew
s
E
01 function Sunify(, ,) (w1 t2 t

,unifiable )
02 begin
03 if or is a variable then
1
t2 t
04 begin let
X
be the variable and
t
the other
term
05 if then tX= ),(),(

trueunifiable

06 else if then ),,( tXwoccur )),(

unifiable
}{,,(tXtXwSunify 
07 else )})({,(),(tsXtrueunifiablew 

08 end else
09 begin let and ),,(= 11 n xxft ),,(= 12 m xxgt 
1 0 if f ≠ g or m ≠ n then else falseunifiable
1
1 if then
0=)( fw ),(),(

trueunifiable

else
12 begin j←0, ),(),( 0

trueunifiable

13 while and do mj <unifiable
1 4 begin 1

jj
15 (unifiable, τj)←Sunify(w!f,xjσj-1,yjσj-1)
16 if then unifiable jjj



1

17 end
18 m



19 end
20 end

Incremental Computation of Success Patterns of Logic Programs205
21 return ),(

unifiable
22 end
The line 06 in algorithm 2 deals with -unification
of X and t where X occurs in by reducing the
problem of -unification of X and t into the problem
of -unification of X and .
w
s
E
)(tsw
}t
w
s
E
w
s
E{Xt
Lemma 8 Let and be terms. If and are
-unifiable, then algorithm 2 terminates and gives an
unique (module renaming) -mgu of and
.Otherwise, the algorithm terminates and reports the fact.
1
t2 t1 t2 t
1
t
w
s
E
2
t
w
s
E
4.4 Refinement of Success Patterns for
Stump Abstractions
The following lemma establishes the appropriateness of
incremental refinement method for stump abstractions.
Lemma 9 For any )(, Nyx

, yx
x
yss .
Lemma 9 implies that if then
for any
 

y
s
y
s
AT][
 

x
s
x
s
AT][
x
y . This enables us to refine
success patterns of P by increasing repetition depths for
some function symbols. Suppose that success patterns in
are not fine enough and it is necessary to
compute for some y such that
 
x
s
T
 
y
s
T
x
y
y
s
T

. Rather
than throwing away and computing
from scratch, we compute by
 

y
s
T
x
s
T  
1) applying ),(
~
*ys to resulting in a set of
candidate elements for since
 
x
s
T
 
y
s
Tsyω

T
;
*(, sx
sy ωT
)
2) applying to eliminate those candidate
elements that are not from
y
s
SLD
P
using .
y
s
SLD
The following two examples illustrate incremental
refinement of success patterns for stump abstractions.
Example 4 Let
={(,),(, )(,),(,),((),())(,)}PpabpXYqXYqab qrXsYqXY
We have
0
.1  f
s

T=
1
.1  f
s

T= )},(),,({ baqbap
2
.1  f
s

T= ))}(),((),,(),,({ bsarqbaqbap
4=5
(_)))((_)),(((_))),((_)),((
)),(),(()),(),((),,(),,(
=4
(_)))((_)),(()),(),((
)),(),((),,(),,(
=3
.1.1
.1
.1















f
s
f
s
f
s
f
s
ssrrpssrrq
bsarpbsarqbaqbap
ssrrqbsarp
bsarqbaqbap



TT
T
T
So, =5=.1.1 f
s
f
s

 TT






(_)))((_)),(((_))),((_)),((
)),(),(()),(),((),,(),,(
ssrrpssrrq
bsarpbsarqbaqbap
Example 5 Let P be the same as example 4. Suppose
that success patterns in are not fine enough.
We compute as follows. We first compute
and then use to eliminate
those candidates in



.1f
s
T
.2,(



.2f
s
T
)  .2,(
~.1
*

 f
s
fs T.2f
s
SLD

)
~
.1
*

 f
s
fT
.2f
s
SLD

 s that are not
provable from P using . The result is











(_))))(((_))),((((_)))),(((_))),(((
))),(()),((())),(()),(((
)),(),(()),(),((),,(),,(
=
.2
sssrrrpsssrrrq
bssarrpbssarrq
bsarpbsarqbaqbap
f
s


T
(_))))(((_))),((( sssrrrq has not been removed because
it is provable from
P
using as follows.
.2f
s
SLD

0
0
0
=( ( ( (_))),( ( (_))))
= (( 1),(1))( 1,1)
={1/( (2)),1/( (2))}
Gqrrr sss
CqrXsY qXY
σXrrX YssY


=(((2)),((2)))GqrrXssY
1
1
1
2
2
2
3
3
3
4
=( (3),(3)) (3,3)
={3/(2),3/ ( 2)}
=( (2),(2))
=(( 4),(4))( 4,4)
={4/2, 4/2}
=(2, 2)
=(,)
={2/,2/ }
=
CqrXsY qXY
σXrXYsY
GqrXsY
CqrXsY qXY
σXXYY
GqXY
Cqab
σXaYb
Gε





(_))))(())),(((( sssasrrq has been eliminated because it
can not proved from P using as shown in the
following.
.2f
s
SLD

0
G=( ( ( ())),( ( (_))))qrrsasss

0= ((1),(1))( 1,1)CqrXsYqXY
0={1/(()),1/( (2))}XrsaYssY

1
G=( (()),((2)))qrsa ssY

1=((3),(3)) (3,3)CqrXsY qXY
1={3/(),3/(2)}XsaYsY

2
G=( (),(2))qsa sY

The refutation process fails because there is no clause
of P whose head -unifies with .
.2f
s
E

2))(),((Ysasq

Incremental Computation of Success Patterns of Logic Programs 206
5. Conclusions and Future Work
We have proposed a method for incrementally computing
success patterns of logic programs for stable abstractions.
We have introduced a partial order on abstractions to
reflect relative strength of abstractions. The method
makes use of a fixed-point and a procedural abstract
semantics of logic programs with respect to stable ab-
stractions, a refinement operator that splits an equi-
valence class induced by a coarser abstraction into a set
of equivalence classes induced by a finer abstraction, and
equational unification. The refinement operator is specified.
We have applied the method for incremental refine-
ment of success patterns of logic programs for depth
abstractions and stump abstractions by constructing
suitable refinement operators and equational unification
algorithms. For depth abstractions, abstraction depth can
be increased uniformly while for stump abstractions,
repetition depth for each function symbol can be incre-
ased independently.
For depth abstractions, abstraction depth can only be
increased uniformly. That means that every equivalence
class has to be split when analysis is refined. It would be
better to be able to split some equivalence classes and
keep others intact. However, it is not clear if such a
fine-tuning approach will guarantee the stability of the
resulting abstraction α which is a prerequisite of using
to eliminate false candidates.

SLD
Another interesting topic on incremental refinement of
success patterns of logic programs is to study the
possibility of applying to eliminate false candidates
where is the abstraction resulting from refinement.
Yet another interesting topic on incremental refinement
of success patterns of logic programs is to combine
domain refinement such as that proposed in this paper
with compositional approach towards logic program ana-
lysis proposed by Codish et al. [3] since compositional
approach is the only feasible way to analyze large
programs. It is necessary to study the interaction between
the refinement of analyses of program modules and the
composition of analyses of program modules.
 
T


6. Acknowledgements
This work was supported, in part, by NSF grant CCR-
0131862.
REFERENCES
[1] P. Cousot and R. Cousot, “Systematic design of program
analysis frameworks,” Proceedings of the 6th ACM
SIGACT-SIGPLAN Symposium on Principles of
Programming Languages, The ACM Press, New York, pp.
269–282, 1979.
[2] P. Cousot and R. Cousot, “Abstract interpretation and
application to logic programs,” The Journal of Logic
Programming, Vol. 13, No. 2–3, pp. 103–179, 1992.
[3] H. Søndergaard, “An application of abstract interpretation
of logic programs: Occur check problem,” In: B. Robinet
and R. Wilhelm, Ed., European Symposium on Progr-
amming, Lecture Notes in Computer Science, Springer,
Vol. 213, pp. 324–338, 1986.
[4] C. Mellish, “Some global optimizations for a Prolog
compiler,” Journal of Logic Programming, Vol. 2, No. 1,
pp. 43–66, 1985.
[5] C. Mellish, “Abstract interpretation of Prolog programs,”
In: S. Abramsky and C. Hankin, Ed., Abstract interp-
retation of declarative languages, Ellis Horwood Ltd., pp.
181–198, 1987.
[6] M. Bruynooghe and G. Janssens, “An instance of abstract
interpretation integrating type and mode inferencing,”
Proceedings of the Fifth International Conference and
Symposium on Logic Programming, The MIT Press,
Seattle, pp. 669–683, 15–19 August 1988.
[7] D. Jacobs and A. Langen, “Static analysis of logic prog-
rams for independent and parallelism,” Journal of Logic
Programming, Vol. 13, No. 2–3, pp. 291–314, 1992.
[8] X. Li, A. King, and L. Lu, “Collapsing closures,” In: S.
Etalle and M. Truszczynski, Ed., Proceedings of the
Twenty Second International Conference on Logic
Programming, Lecture Notes in Computer Science, Vol.
4079, pp. 148–162, 2006.
[9] M. Bruynooghe, G. Janssens, A. Callebaut, and B. Demoen,
“Abstract interpretation: Towards the global optimisation
of Prolog programs,” Proceedings of the 1987 Symposium
on Logic Programming, The IEEE Computer Society
Press, San Francisco, pp. 192–204, 31 August–4
September 1987.
[10] L. Lu, “Improving precision of type analysis using non-
discriminative union,” Theory and Practice of Logic
Programming, Vol. 8, pp. 33–80, 2008.
[11] K. Marriott, H. Søndergaard, and N. D. Jones, “Denota-
tional abstract interpretation of logic programs,” ACM
Transactions on Programming Languages and Systems,
Vol. 16, No. 3, pp. 607–648, 1994.
[12] K. Marriott and H. Søndergaard, “Bottom-up abstract
interpretation of logic programs,” Proceedings of the
Fifth International Conference and Symposium on Logic
Pro- gramming, The MIT Press, Seattle, pp. 733–748,
15–19 August 1988.
[13] M. H. van Emden and R. A. Kowalski, “The semantics of
predicate logic as a programming language,” Artificial
Intelligence, Vol. 23, No. 10, pp. 733–742, 1976.
[14] J. Jaffar, J. L. Lassez, and M. J. Maher, “Theory of
complete logic programs with equality,” Journal of Logic
Programming, Vol. 1, No. 3, pp. 211–23, October 1984.
[15] T. Sato and H. Tamaki, “Enumeration of success patterns
in logic programs,” Theoretical Computer Science, Vol.
34, No. 1, pp. 227–240, 1984.
[16] P. M. Hill and F. Spoto, “Generalizing Def and Pos to
type analysis,” Journal of Logic and Computation, Vol.

Incremental Computation of Success Patterns of Logic Programs 207
12, No. 3, pp. 497–542, 2002.
[17] M. Li, Z. Li, H. Chen, and T. Zhou, “A novel derivation
framework for definite logic program,” Electronic Notes
in Theoretical Computer Science, Vol. 212, pp. 71–85,
2008.
[18] J. A. Robinson, “A machine-oriented logic based on the
resolution principle,” Journal of the ACM, Vol. 12, No. 1,
pp. 23–41, 1965.
[19] J. Xu and D. S. Warren, “A type inference system for
Prolog,” Proceedings of the 5th International Conference
and Symposium on Logic Programming, The MIT Press,
Seattle, pp. 604–619, 15–19 August 1988.
[20] M. Codish, S. K. Debray, and R. Giacobazzi, “Composi-
tional analysis of modular logic programs,” Proceedings
of the 20th Annual ACM Symposium on Principles of
Programming Languages, The ACM Press, New York,
USA, pp. 451–464, January 1993.