### Paper Menu >>

### Journal Menu >>

J. Software Engineering & Applications, 2010, 3: 198-207 doi:10.4236/jsea.2010.33025 Published Online March 2010 (http://www.SciRP.org/journal/jsea) Copyright © 2010 SciRes. JSEA Incremental Computation of Success Patterns of Logic Programs Lunjin Lu Department of Computer Science and Engineering, Oakland University, Rochester, USA. Email: lunjin@acm.org 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 stt 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 Copyright © 2010 SciRes. JSEA 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 Copyright © 2010 SciRes. JSEA 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 dT(_)),( fa (_)),(fa (_)),(fa =3 1 dT 2 d T 2 d 2 ,d (_)}(_), hf (_))),(( ff (,(_))) fp 2 d = 2 d T ))(()), cfb ( 2bd , (_))}((_)),({=2 1fpfb dT, (_))}((_)),({=3 1fpfb dT, and (_))}((_)),((_)),({= 1fpfbfa dT . 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. 0k 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 Copyright © 2010 SciRes. JSEA 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 0k 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 , 0j),(),( 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 Copyright © 2010 SciRes. JSEA Incremental Computation of Success Patterns of Logic Programs Copyright © 2010 SciRes. JSEA 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 ωpabqabqrsprsTT 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 [()wfwf1].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 NTerms 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 tgsssj 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 Copyright © 2010 SciRes. JSEA 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 Copyright © 2010 SciRes. JSEA 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. Copyright © 2010 SciRes. JSEA Incremental Computation of Success Patterns of Logic Programs Copyright © 2010 SciRes. JSEA 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. |