Constrained Regular Approximation of Logic Programs
University of Bristol
Department of Computer Science
Also issued as ACRC-97:CS-008
Constrained Regular Approximation of Logic Programs
Huseyin Salam1 and John P. Gallagher1 g
1 Department of Computer Science, University of Bristol, The Merchant Venturers Building, Woodland Road, Bristol BS8 1UB, U.K. fsaglam,firstname.lastname@example.org
Abstract. Regular approximation is a well-known and useful analy-
sis technique for conventional logic programming. Given the existence of constraint solving techniques, one may wish to obtain more precise approximations of programs while retaining the decidable properties of the approximation. Greater precision could increase the e ectiveness of applications that make use of regular approximation, such as the detection of useless clauses and type analysis. In this paper, we introduce arithmetic constraints, based on convex polyhedra, into regular approximation. In addition, Herbrand constraints can be introduced to capture dependencies among arguments.
Keywords: regular approximation, linear constraints, convex polyhedra.
Regular approximation is a program analysis technique sometimes identi ed with type inference". Type inference is the process of determining the type of program units. Type systems are designed to allow the programmer to describe the set of intended values that an argument can take. Regular approximations are not true types, but rather syntactic descriptions of the success set of programs. Thus the word type inference" is not strictly correct although for de nite logic programs the concept of type" and success set of predicates coincide quite closely for practical purposes. The practical usefulness of regular approximation is to provide a decidable description of the set of terms that can appear in each argument position in correct answers. In previous work on regular approximations, or the closely related concepts of rigid type graphs, sets of terms are given by recursive descriptions which are essentially deterministic nite automata. Certain built-in sets such as numbers can be included in the descriptions. It is possible to improve on the precision of regular type description, departing from strictly regular description, without losing decidability. One such method will be explored in this paper, namely, the addition of constraints to regular descriptions. The class of regular unary logic RUL programs was de ned by Yardeni and Shapiro 21 . They de ne a class of types called regular types, and show the
equivalence between regular types and RUL programs. They represent regular types by Deterministic Finite Automata DFA and use tuple distributive closure for types as de ned by Mishra 11 . Their formalism for describing sets of terms is adopted in 6 , and also followed in 15 and 16 as extensions of 6 . In 6 Gallagher and de Waal de ne an e cient regular approximation framework. All procedures they de ne such as upper bound and intersection, handle programs whose clauses are in a special, restricted form RUL clause. This form is given in the following de nition.
De nition 1. A canonical regular unary RUL clause is a clause of the form t0 f x1 ; : : : ; xn t1 x1 ; : : : ; tn xn n 0
where x1 ; : : : ; xn are distinct variables. By relaxing De nition 1 we make an extension to the notion of regular approximation, by allowing arithmetic and Herbrand constraints in the bodies of regular clauses. This permits us to capture dependencies between the arguments of terms, and also, in certain cases, to capture dependencies between arguments at di erent levels of a term. For example, we can capture dependencies between successive elements of a list, or every other element of a list by imposing a suitable depth bound.
2 Constrained Regular Approximation
In order to achieve the aforementioned extension, the general form of a constrained regular unary clause can be given as follows.
De nition 2. A constrained regular unary CRUL clause is a clause of the form t0 f x1 ; : : : ; xn C ; t1 x1 ; : : : ; tn xn n 0 where x1 ; : : : ; xn are distinct variables and C is a conjunction of constraints
projected onto x1 ; : : : ; xn . Note that we usually use sets to deal with conjunctions; in the de nitions below, a set of some syntactic objects, if any, stands for a conjunction of the syntactic objects.
Example 1. The following clause is a constrained regular unary clause. sorted X jY Y = Z jW ; X Z; sortedY : Note that the constraints contain local variables Z and W . There is also an implicit unary atom anyX in the body to t the de ned form, where anyX is true for all X .
Some de nitions are next given to de ne the main operations and relations on CRUL clauses.
De nition 3. Let t be a term and C a conjunction of constraints. A pair t; C is called a constrained term. Two constrained terms t1 ; C1 and t2 ; C2 overlap if there is a substitution such that both
1. t1 = t2 , and 2. C1 and C2 are satis able. We say that two CRUL clauses pu1 C1 ; t1 x1 ; : : : ; tn xn and qu2 C2 ; s1 x1 ; : : : ; sn xn overlap if the constrained terms u1 ; C1 and u2 ; C2 overlap.
De nition 4. CRUL program
A constrained regular unary logic CRUL program is a nite set of constrained regular unary clauses in which no two standardised apart clauses overlap.
De nition 5. Let P be a de nite program and P a CRUL program containing a special unary predicate approx=1. Assuming a xed interpretation of constraint predicates and functions and Herbrand interpretations of the other predicates and functions, let M P be the least model of P . Then P is a constrained regular approximation of P if M P is contained in the set A approxA 2 M P .
Note that, as in 6 , in using approx=1 we abuse notation by confusing predicate and function symbols. Using the approx predicate allows us to restrict attention to CRUL programs. Often it is omitted and a clause approxpx1 ; : : : ; xn C ; p1 x1 ; : : : ; pn xn is written as px1 ; : : : ; xn C ; p1x1 ; : : : ; pn xn .
De nition 6. Let p be a predicate. Then, in the context of some program P ,
proc p is the set of all the clauses in P whose head contains p.
De nition 7. Let p be a predicate. Then, in the context of some program P ,
def p = proc p
def p is the set of all the clauses in P de ning p, including subsidiary de nitions. Formally, def q q occurs in proc p :
2.1 Operations on Constraints and CRUL Programs
We approximate arithmetic constraints using convex polyhedra since it seems to be the most interesting approach for general use, although there are other
approaches such as a ne sub-spaces, intervals, and signed inequalities 20 , 9 , 19 , 10 . A convex polyhedron is characterised by a system of linear constraints. The set of solutions to a nite system of loose linear inequalities can be interpreted geometrically as a closed convex polyhedron of IRn . The least polyhedron containing this set is called its convex hull. There is no loss of generality in considering only loose linear inequalities since strict inequalities can be handled by adding an auxiliary variable , 0 1 as shown in 7 . Least upper bound and widening operations over polyhedra are de ned in 3 . De Backer and Beringer introduced linear relaxation" in 4 where explicit computation of the constraints de ning the convex hull is not needed. The expression is obtained by only adding new variables to the initial problem. Although it looks potentially expensive, it is easy to implement for computing the least upper bound of convex polyhedra 1 . A predicate can be given a constrained regular de nition. The clauses of the predicate require some form that allows operations to be e ciently performed. Moreover terms in constraints having unbounded depth increase the di culty of de ning a terminating xpoint computation see Section 2.3. A depth bound is needed to put an upper bound on the size of CRUL programs. This helps to ensure termination of the approximation procedure.
De nition 8. constrained regular de nition of a predicate
Let p be a unary predicate. A constrained regular de nition of p for some depth k is a constrained regular unary program whose clause heads all have predicate p, and where the maximum depth of terms in the constraints is k. Intersection of regular unary predicates is required in order to produce CRUL clauses. Let t1 x; t2 x be a conjunction. We compute a new predicate r = T t1 t2 such that 8xt1 x ^ t2 x $ rx. To simplify the presentation, let us assume that the CRUL clauses contain only Herbrand and linear arithmetic constraints in their constraint parts. That is, each CRUL clause is of the form pf x1 ; : : : ; xn H; A; p1 x1 ; : : : ; pnxn where H and A are conjunctions of Herbrand and arithmetic constraints respectively. We assume that H is of the form fv1 = t1 ; : : : ; vk = tk g where no vj occurs in t1 ; : : : ; tk .
De nition 9. intersection of constrained regular unary predicates
Let p and q be unary predicates with constrained regular de nitions procp T and procq respectively. Then their intersection p q is de ned by a predicate r with constrained regular de nition given as follows.
rt mguHp; Hq ; for each t such that pt Hp ; Ap ; p1 x1 ; : : : ; pn xn and = Ap ^ Aq ; qt Hq ; Aq ; q1 x1 ; : : : ; qn xn r1 x1 ; occur in procp and procq respectively, .. . Ap ^ Aq is satis able and : ; rn xn t; Hp ; t; Hq overlap.
where ri = pi qi , and Hp , Hq are sets of Herbrand constraints, Ap , Aq are sets of arithmetic constraints, and mguHp ; Hq is the set of equations in the solved form of Hp Hq . An upper bound operation for CRUL predicates will be de ned to reduce the number of clauses in the de nition of a predicate by merging overlapping ones. To form the upper bound of two CRUL predicates, de nitions for both predicates including the de nitions of the subsidiary predicates in the bodies of the clauses de ning the predicates are needed. We can separate the construction of upper bound of predicates into two parts. One of them is the construction of the constraint part and the other one is the construction of the regular part. Let us rst give some de nitions to de ne the upper bound of the constraint parts.
De nition 10. generalisation of terms
Let t1 and t2 be two terms. Then a term t is a generalisation of the terms t1 and t2 if there exist two substitutions 1 and 2 such that t1 = t1 and t2 = t2 .
De nition 11. most speci c generalisation of terms
0 0 0
Let t be a generalisation of the terms t1 and t2 . Then t is the most speci c generalisation of t1 and t2 , denoted msgt1 ; t2 , if for any generalisation t of t1 and t2 , there exists a substitution such that t = t 13 , 12 .
Let z1; : : : ; zk be the variables that occur on the left hand side of equations in both H1 and H2 , say z1 = t1 ; : : : ; zk = tk in H1 and z1 = s1 ; : : : ; zk = sk in H2 . Then msgH1 ; H2 is the set of equations fz1 = r1 ; : : : ; zk = rk g where hr1 ; : : : ; rk i = msg ht1 ; : : : ; tk i; hs1 ; : : : ; sk i.
De nition 12. most speci c generalisation of set of equations Let H1 = fx1 = t1 ; : : : ; xn = tn g and H2 = fy1 = s1 ; : : : ; ym = sm g.
Note that we usually use sets to deal with conjunctions; in the above de nition a set of some syntactic objects stands for a conjunction of the syntactic objects.
De nition 13. upper bound of constraints
Let H1 ; A1 and H2 ; A2 be conjunctions of Herbrand and arithmetic conF straints. Then an upper bound H; A denoted H1 ; A1 H2 ; A2 is computed as follows.
end while 9yj =w; yl=w 2 2; j 6= l; w occurs in A2 2 := 2 , fyl =wg A2 := A2 fyj = yl g end 1 := fv=yijyi =v 2 1 ; v is a variableg 2 := fw=yj jyj =w 2 2 ; w is a variableg A := CH A1 1 ; A2 2 end
where CH A1 1 ; A2 2 is the convex hull computed from the conjunctions of arithmetic constraints A1 1 and A2 2 . The purpose of this construction is to compute the most speci c generalisation msg of the Herbrand constraints, and then derive suitable renamings for the arithmetic constraints to make them compatible with the variables in the msg. During this process, aliasing among arithmetic variables which is lost in the msg is recovered, and added as arithmetic equalities. Finally the convex hull of the renamed arithmetic constraints is computed.
Example 2. Let H1 ; A1 be X = f Y; Y ; Y 0 and let H2 ; A2 be Z = f U; V ; ,U = V . Then msgH1 ; H2 = Z1 = f Z2; Z3 ; 1 = fZ1=X; Z2=Y; Z3=Y g; 2 = fZ1=Z; Z2 =U; Z3=V g: At the end of the while loops, 1 = fX=Z1; Y=Z2 g; 2 = fZ=Z1; U=Z2 ; V=Z3 g; A1 = fY 0; Z2 = Z3 g A2 = f,U = V g: Hence after applying the convex hull procedure CH A1 1 ; A2 2 , the result is H; A = Z1 = f Z2 ; Z3; ,Z2 Z3 :
H := msgH1 ; H2 1 := mguH; H1 2 := mguH; H2 while 9yi=v; yk =v 2 1; i 6= k; v occurs in A1 1 := 1 , fyk =vg A1 := A1 fyi = yk g
Lemma 14. Let C1 = H1; A1 andFC2 = H2; A2 be conjunctions of conF straints. Let their upper bound C = C1 C2 be H; A = H1 ; A1 H2 ; A2 . Assume H1 and H2 are of the form x1 = t1 ; : : : ; xn = tn and x1 = s1 ; : : : ; xn = sn respectively, which implies we can assume that H is of the form x1 = r1 ; : : : ; xn = rn . Then 8x1 ; : : : ; xn 8C1 ! C ^ C2 ! C .
Proof. Outline. Let the upper bound C = C1 C2 be H; A = H1 ; A1 H2 ; A2 , where H = msgH1 ; H2 and A = CH A1 1 ; A2 2 , 1 and 2 being variable renamings as constructed in De nition 13. Then, 8H1 ; A1 ! H since H = msgH1; H2 is the most speci c generalisation of the conjunction of Herbrand constraints H1 and H2 where the variables in H1 , H2 and H are renamed to be the same. 8H1 ; A1 ! A1 1 holds since the renaming 1 only introduces fresh variables. 8A1 1 ! CH A1 1 ; A2 2 because CH A1 1 ; A2 2 describes a polyhedron containing both A1 1 and A2 2 . Hence 8H1 ; A1 ! A. Then, since H and A are true independent of the truth of each other, 8H1 ; A1 ! H; A holds. Similarly, for H2 ; A2 , 8H2 ; A2 ! H; A holds.
Let us now de ne the upper bound of two CRUL clauses before de ning the upper bound of two predicates. We denote the upper bound of two predicates t F and s by t p s, which will be de ned in De nition 20. be two overlapping clauses, with variables renamed so that the heads are identical. Then their upper bound is
De nition 15. upper bound of two constrained regular unary clauses Let pu H1 ; A1 ; t1 x1 ; : : : ; tn xn and pu H2 ; A2 ; s1 x1 ; : : : ; sn xn
pu H; A; r1 x1 ; : : : ; rn xn F F where ri = ti p si and H; A = H1 ; A1 H2 ; A2 .
Next we show how to assign unique names to the upper bounds of predicates. This is done in order to ensure termination of the upper bound procedure. Let Pred = fp1 ; : : : ; pn g be a set of unary predicates. De ne Pred to be a set of 2n , 1 unary predicates, including p1 ; : : : ; pn . Identify each element q of Pred with a unique non-empty subset of Pred, denoted Name q. The function Name is extended to upper bounds of predicates in Pred , such that F Name q1 p q2 = Name q1 Name q2 .
t t t
Thus for all q1 ; q2 2 Pred , q1 p q2 is associated with a unique element of Pred , say q3 where Name q3 = Name q1 Name q2 .
Intuitively, a set of predicates uniquely determines their upper bound, and so Pred contains su cient predicates to name each upper bound of predicates in Pred. We next de ne an operation that converts a set of CRUL clauses into a CRUL program, by successively removing overlapping clauses. First we de ne some simple operations.
De nition 16. Let Pred be a set of unary predicates. Let r and t be predicates 2 Pred . Let s be the predicate such that Name s = Name r Fp t. Then
merge r; t is the set of clauses obtained from proc r proc t by replacing the predicates in the heads by s.
De nition 17. Let r and t be predicates and R a set of clauses. merge Rr; t is
de ned to be: ;, if R contains the predicate s such that Name s = Name r Name t; merge r; t, otherwise.
De nition 18. normalisation of a set of CRUL clauses
Let R be a set of CRUL clauses. De ne norm R as follows: norm R = R if R has no overlapping clauses; norm R = norm R ,fC1 ; C2 g fC g merge R t1 ; s1 : : : merge R tn ; sn , where C1 = A1 D1 ; t1 x1 ; : : : ; tn xn and C2F= A2 D2 ; r1 x1 ; : : : ; rn xn are overlapping clauses in R, and C = C1 c C2 .
Informally, the norm operation removes a pair of overlapping clauses, and replaces them by their upper bound. This may introduce new clauses since the upper bound can contain new predicates; the operation is repeated until no overlapping clauses remain. Note that the use of the operation merge R in the de nition of norm is necessary to ensure termination of normalisation, since it prevents the addition of clauses for predicates already in the program. Without this operation it would be possible to reintroduce overlapping clauses that had previously been removed.
Proposition 19. The operation norm P terminates.
Proof. Let Pred be the set of predicates in P . We de ne a mapping from CRUL programs onto a well-founded set. Then we show that in the recursive equation in the de nition of norm, the argument of the call to norm on the right is strictly less with respect to the associated ordering on the well-founded set than the argument of the call on the left. The well-founded set consists of pairs hN; V i, where N , V are natural numbers. The ordering is the lexicographical ordering, that is,
hN1 ; V1 i hN2 ; V2 i i N1 N2 , or N1 = N2 and V1 V2
Let P = P0 ; the computation of norm P gives rise to a sequence of calls norm P0 ; norm P1 ; norm P2 ; : : :. De ne hNj ; Vj i as follows. Nj is the number of predicates in Pred that do not appear in Pj , and Vj is the number of clauses in Pj . Consider the relationship between Pj+1 and Pj , which is given by the left and right hand sides of the recursive equation for norm. Either
1. the number of unused predicates is decreased in the case that some new predicates are introduced into Pj+1 , by the merge P components; or 2. the number of clauses in Pj+1 is one less than the number in Pj in the case that no new predicates are introduced.
In both cases hNj+1 ; Vj+1 i hNj ; Vj i. Since the relation is a well-founded order, the sequence of calls to norm is nite. Note that the number of clauses can increase during the procedure, but only in the case when the number of unused predicates symbols simultaneously decreases. We can now use the norm operation to de ne the upper bound of two predicates.
De nition 20. Let r and t be two unary predicates. Then F upper bound of the F
r and t is given by the predicate r p t such that Name r p t = Name r Name t de ned by the clauses norm R, where R = def r def t , proc r , proc t merge r; t
Also using the norm operation, we de ne the upper bound of two CRUL programs.
De nition 21. The upper bound of two CRUL programs, P and Q, denoted F
P Prog Q, is de ned to be norm P Q.
Example 3. The following program is used to give some idea of the operations de ned.
p X1|X2 :- X2= X3|X4 , X1 =0, X1 =X3, t1X2. p X1|X2 :- X2= X3|X4 , X1 =3, X1= 2*X3, s1X2. t1 X1|X2 :- X1= 2, t2X2. t2 . s1 X1|X2 :- X1= 10, s2X2. s2 .
The two clauses de ning p 1 overlap. The upper bound t13 of predicates t1 and s1 is computed to compute the upper bound of the clauses for predicate p. The resulting program is given below.
pX1 :- X1= X2,X3 , X3= 10, X2-0.3*X3 =0, X2 =0, t29X1. t29 X1|X2 :- X2= X3|X4 , X3= 10, X1-0.3*X3 =0, X1 =0, t13X2. t13 X1|X2 :- X2= , X1= 10, t14X2. t14 :- true.
An essential operation when computing a xpoint is to check inclusion of one constrained regular unary predicate in another.
De nition 22. inclusion of constrained regular unary predicates
i i n
Let p and q be de ned in a CRUL program. Then the inclusion of the predicates p and q is checked as follows.
p q i for all clauses pti Hp ; Ap ; pi1 x1 ; : : : ; pi xn ; there exists a clause qtj Hq ; Aq ; qj1 x1 ; : : : ; qj xn and there is a substitution such that
j j n
1: ti ; Hp = tj ; Hq ; and Ap Aq ; 2: pi1 qj1 ; : : : ; pi qj :
i j i j n n
De nition 23. depth-k abstraction of a CRUL clause Let pt H; A; p1 x1 ; : : : ; pn xn be a CRUL clause. Then the depth-k abstraction of the clause is pt Hk ; Ak ; p1 x1 ; : : : ; pn xn where Hk is depthbounded version of H and Ak is A projected onto the variables occurring in Hk and t. Depth-k abstraction is performed just after the intersection operation and the depth of terms does not have to be taken into account during the intersection, upper-bound, or widening operations. The depth-2 abstraction of the clause
p X1|X2 :- X2= X3,X5|X6
,X1 X3,X3 X5,qX1,rX2
Depth-3 abstraction makes no change in this case. Using depth-2 is a good compromise since it allows inferring dependencies between one level and the next, and since dependencies between terms at widely separated levels within a term do not occur frequently.
p X1|X2 :- X2= X3|X4 ,X1 X3, qX1, rX2.
2.2 Computation of a Constrained Regular Approximation
A semantic function is de ned similarly to the one in 17 . The approximation of a program P is computed by an iterative xpoint computation with widening.
A sequence of constrained regular approximations P0 ; P1 ; P2 ; : : : is computed as follows. P0 = ; Pi+1 = Pi 5Prog T Pi i 0 where F S T Pi = Pi Prog fsolveC; Pi j C 2 P g: solveC; Pi takes a clause C and a CRUL program Pi and returns a constrained regular de nition of the predicate in the head of C . The operations intersection and depth-k are included in solve. The body of C is solved in the current approximation Pi which involves unfolding the body and intersecting the predicates with the same argument. The limit of the sequence P0 ; P1 ; P2 ; : : : is the constrained regular approximation of P . F The operators 5Prog and Prog see De nition 20 are widening and upper bound operators on programs respectively. The only requirement on these operations is that they should be safe with respect to the underlying order of the approximations.
2.3 Termination of Fixpoint Computation
There are two di erent xpoint computations, taking place at the same time, to be terminated. One is for the arithmetic approximation, and the other one is for the regular approximation. For the xpoint computation of arithmetic constraints we have existing tools for applying various di erent upper bound and widening operators with di erent trade-o s of precision and e ciency and an optional narrowing operator. The operators were suggested in 3 and 2 . We use simpli ed and e cient versions of them 18 . E ective abstract interpretation procedures for computing a regular approximation of a program using RUL programs or some equivalent notation have been de ned in 8 and 6 . Several other works contain other solutions to the problem. For the termination of regular approximation we adopted the shortening" de ned in 6 . A widening" 8 operator could also be chosen.
De nition 24. shortening of CRUL predicates
Let P be a CRUL program containing predicates t and s t 6= s. Let an occurrence of predicate t depend on predicate s, and let t and s have the same function symbols in their clause heads. Then the occurrence of s is replaced by t, if s is included in t. The shortening operation de ned in 6 is less precise, but sometimes faster. In the shortening there, a recursive approximation is introduced whenever predicate t depends on predicate s, and t and s have the same function symbols in their
clause heads, without checking the inclusion. We can further improve precision comparing to 6 by taking into account the Herbrand constraints as well as the head functions.
A number of simple examples are given in this section to illustrate the approximation.
Example 4. List of sorted numbers Let us consider the constrained regular approximation of the following simple program.
sorted . sorted X :- X = 0. sorted X,Y|Z :- X = Y, sorted Y|Z .
The limit of the successive approximations of the program gives the following result.
sortedX1 :-t1X1. t1 :-true. t1 X1|X2 :-X2= ,X1 =0,anyX1,t2X2. t1 X1|X2 :-X2= X3|X4 ,X1 =0,X1-X3 =0,anyX1,t1X2. t2 :-true.
Example 5. List of uniform elements We can capture other dependencies, not necessarily arithmetic, between different levels as in the following program.
uniform . uniform X . uniform X,X|Y :- uniform X|Y .
The following CRUL program is generated as the limit of the successive approximations of the above program.
uniformX1 :-t1X1. t1 :-true. t1 X1|X2 :-X2= ,anyX1,t2X2. t1 X1|X2 :-X2= X1|X3 ,anyX1,t1X2. t2 :-true.
The redundant atoms in the clauses of above programs, such as anyX1 are not removed for the sake of implementation ease and for conforming to the de nitions on CRUL clauses.
Example 6. Let us show the intersection and upper bound of the above programs, to clarify the operations.
sorted_and_uniformX :- sortedX, uniformX. sorted_or_uniformX :- sortedX. sorted_or_uniformX :- uniformX.
The analysis gives the following CRUL program.
sorted_and_uniformX1 :-t1X1. t1 :-true. t1 X1|X2 :-X2= ,X1 =0,anyX1,t2X2. t1 X1|X2 :-X2= X1|X3 ,X1 =0,anyX1,t1X2. t2 :-true. sorted_or_uniformX1 :- t3X1. t3 :-true. t3 X1|X2 :-X2= ,anyX1,t4X2. t3 X1|X2 :-X2= X3|X4 ,anyX1,t3X2. t4 :-true.
Example 7. For a comparison, let us now consider the regular approximation and the constrained regular approximation of the following predicate taken from an alpha-beta procedure for the game of kalah.
initializekalah,boarda,0,a,0,opponent. initializekalah,totob,1,b,1,computer. initializekalah,boardc,2,c,2,computer. initializekalah,boarda,0,a,0,computer. initializekalah,boardc,2,c,2,opponent. Regular Approximation Program: initializeX1,X2,X3 :-t349X1,t378X2,t374X3. t349kalah :-true. t378boardX1,X2,X3,X4 :-t380X1,t381X2,t382X3,t383X4. t378totoX1,X2,X3,X4 :-t343X1,t344X2,t345X3,t346X4. t374opponent :-true. t374computer :-true.
t380a t380c t3810 t3812 t382a t382c t3830 t3832 t343b t3441 t345b t3461
:-true. :-true. :-true. :-true. :-true. :-true. :-true. :-true. :-true. :-true. :-true. :-true.
Constrained Regular Approximation Program: initializeX1,X2,X3 :-t326X1,t349X2,t345X3. t326kalah :-true. t349boardX1,X2,X3,X4 :-X1=c,X3=c,X2=2.0,X4=2.0,t328X1,anyX2, t329X3,anyX4. t349totoX1,X2,X3,X4 :-X1=b,X3=b,X2=1.0,X4=1.0,t322X1,anyX2, t323X3,anyX4. t349boardX1,X2,X3,X4 :-X1=a,X3=a,X2=0.0,X4=0.0,t316X1,anyX2, t317X3,anyX4. t345opponent :-true. t345computer :-true. t328c :-true. t329c :-true. t322b :-true. t323b :-true. t316a :-true. t317a :-true.
Example 8. For greater precision, we introduce some type information into the approximation, thus avoiding the overapproximation of some arguments. In the following example, numeric is such a type that describes any number. numericX can be viewed as an arithmetic constraint that is true for all numbers X, i.e. like X =:= X which would normally be removed by the constraint simpli cation.
disjunct . disjunct A,B,C,D |R :disjA,B,C,D, disjunctR. disjAa,Ad,Ba,Bd:-
gteqcBa,Aa,Ad. disjAa,Ad,Ba,Bd:gteqcAa,Ba,Bd. gteqcX,Y,C :X = Y + C. Regular Approximation Program: gteqcX1,X2,X3 :-anyX1,anyX2,anyX3. disjX1,X2,X3,X4 :-anyX1,anyX2,anyX3,anyX4. disjunctX1 :-t38X1. t38 :-true. t38 X1|X2 :-t32X1,t38X2. t32 X1|X2 :-anyX1,t33X2. t33 X1|X2 :-anyX1,t34X2. t34 X1|X2 :-anyX1,t35X2. t35 X1|X2 :-anyX1,t36X2. t36 :-true. Constrained Regular Approximation Program: gteqcX1,X2,X3 :-X1-X2-X3 =0.0. disjX1,X2,X3,X4 :-numericX1,numericX3,anyX2,anyX4. disjunctX1 :-t39X1. t39 :-true. t39 X1|X2 :-t33X1,t39X2. t33 X1|X2 :-X2= X3|X4 ,numericX1,t34X2. t34 X1|X2 :-X2= X3|X4 ,anyX1,t35X2. t35 X1|X2 :-X2= X3|X4 ,numericX1,t36X2. t36 X1|X2 :-X2= ,anyX1,t37X2. t37 :-true.
There are some dependencies that our method cannot capture. Consider the following partition predicate taken from a quicksort program.
Example 9. Partitioning a list of numbers
partition_, , , . partitionX, Y|Ys ,L, Y|G :- X = Y, partitionX,Ys,L,G. partitionX, Y|Ys , Y|L ,G :- Y X, partitionX,Ys,L,G.
The analysis gives no precise result.
where t1, t2 and t3 de ne lists of any elements. Ideally we would like to capture the information that there is a dependency between t2 and t3. If the rst argument of partition can be xed, for example in a goal directed analysis of partition3,X2,X3,X4 the dependency between the subarguments of the third and fourth arguments, that is all the elements of the third argument are strictly less than all the elements of the fourth argument, of partition can be captured. Without knowing the value of the rst argument, CRUL clauses are not expressive enough to capture the dependency.
5 Implementation and Related work
The implementation of the regular approximation procedure de ned in 6 is the basis for the implementation of this work. Recent studies on approximation of arithmetic constraints have been done in a CLP framework by Benoy and King 1 and Salam and Gallagher 18 . The g method de ned in this paper includes arithmetic approximations such as those discussed in 1 , 18 as a special case, where all predicates are arithmetic. For example, the list length analysis of the well known append predicate gives the result appendX; Y; Z Z = X + Y; X 0; Y 0; anyX ; anyY ; anyZ : The combination of Herbrand and arithmetic constraints, called "mixed disjunctive constraints", was studied in 17 which is based on the framework set out in 5 and uses abstract compilation, where constraint logic programs are used to de ne pre-interpretations as in 14 . It handles predicate arguments containing both Herbrand and arithmetic subterms. Termination is not guaranteed if the Herbrand terms are of unbounded depth. Procedures from 17 are used for the implementation of this work.
6 Conclusion and Future work
We have demonstrated a method that extends regular approximations to capture additional decidable properties of a program. We capture dependencies between the arguments of terms, and also, dependencies between arguments at di erent levels of a term. In our implementation, we provide a number of choices on upper bound and widening operators, such as coarse and upper bounds, and simple and precise widenings on arithmetic constraints, tuple-distributive upper bound and most speci c generalisations, and simple and precise widenings on term constraints, to obtain substantially di erent approximations of programs. Constrained regular approximation becomes much more e cient and less precise if we employ depth-1 for the arguments of approx 1, and depth-2 for the arguments of the
other functions, since it disregards the Herbrand dependencies between the arguments of predicates, while the top level dependencies within each argument are still preserved. Leaving aside the arithmetic constraints, the result of employing a depth bound of 1 throughout gives the same result as regular approximation. The ability that the method de ned in this paper lacks is the handling of dependencies among variable arguments of some predicates. In Example 9 one can expect an approximation that captures the information that one argument is a list of numbers which are all greater than or equal to the numbers in the other list, which is the other argument. To capture this kind of properties a parameterised regular clause de nition could be appropriate, analogous to the addition of polymorphism in types. This is a possible extension of the method. Before that this work needs to be experimented on. The stage at which depth-k abstraction is performed might change the precision and or e ciency. Currently we perform depth-k abstraction after the intersection operation. It could well be a part of widening in the approximation. The performance results and complexity analysis compared with standard regular approximation are subjects of current investigation. Integrating Boolean constraints will give a greater precision and exibility and it appears to be a natural extension of the method.
1. F. Benoy and A. King. Inferring argument size relations with CLPR. In Proceedings of the 6th International Workshop on Logic Program Synthesis and Transformation LOPSTR-96; Sweden. Springer-Verlag, 1996. 2. P. Cousot and R. Cousot. Comparing the Galois connection and widening narrowing approaches to abstract interpretation. In Proceedings of the 4th International Symposium on Programming Language Implementation and Logic Programming, PLILP'92, Leuven, Belgium, volume 631 of lncs, pages 269 295. Springer-Verlag, 1992. 3. P. Cousot and N. Halbwachs. Automatic discovery of linear restraints among variables of a program. In Proceedings of the 5th Annual ACM Symposium on Principles of Programming Languages, pages 84 96, 1978. 4. B. De Backer and H. Beringer. A CLP language handling disjunctions of linear constraints. In Proceedings of the International Conference on Logic Programming ICLP'93, pages 550 563. MIT Press, 1993. 5. J. Gallagher, D. Boulanger, and H. Salam. Practical model-based static analysis g for de nite logic programs. In J. W. Lloyd, editor, Proc. of International Logic Programming Symposium, pages 351 365. MIT Press, 1995. 6. J. Gallagher and D. A. de Waal. Fast and precise regular approximation of logic programs. In P. Van Hentenryck, editor, Proceedings of the International Conference on Logic Programming ICLP'94, Santa Margherita Ligure, Italy, pages 599 613. MIT Press, 1994. 7. N. Halbwachs, Y. E. Proy, and P. Raymond. Veri cation of linear hybrid systems by means of convex approximations. In Proceedings of the First Symposium on Static Analysis, volume 864 of lncs, pages 223 237. Springer-Verlag, September 1994.
8. P. Van Hentenryck, A. Cortesi, and B. Le Charlier. Type analysis of Prolog using type graphs. Journal of Logic Programming, 223:179 210, 1994. 9. G. Janssens, M. Bruynooghe, and V. Englebert. Abstracting numerical values in CLPH,N. Technical Report CW189, K.U. Leuven, Belgium, 1994. 10. K. Marriott and P.J. Stuckey. The 3 R's of optimizing constraint logic programs: Re nement, removal and reordering. In Proceedings of the 20th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages; Charleston, South Carolina, pages 334 344, January 1993. 11. P. Mishra. Towards a theory of types in prolog. In Proceedings of the IEEE International Symposium on Logic Programming, 1984. 12. G. Plotkin. A note on inductive generalisation. In B. Meltzer and D. Michie, editors, Machine Intelligence, Vol.5. Edinburgh University Press, 1974. 13. J. C. Reynolds. Transformational systems and the algebraic structure of atomic formulas. In B. Meltzer and D. Michie, editors, Machine Intelligence, Vol.5. Edinburgh University Press, 1974. 14. H. Salam. Static analysis of logic programs by abstract compilation into CLP. g In Proceedings of the Eighth European Summer School on Logic, Language and Information, ESSLLI'96 Student Session. Czech Technical University, Prague, Czech Republic, 1996. 15. H. Salam and J. Gallagher. Approximating logic programs using types and regug lar descriptions. Technical Report CSTR-94-19, University of Bristol, Department of Computer Science, 1994. 16. H. Salam and J. Gallagher. Approximating constraint logic programs using polyg morphic types and regular descriptions. In Proceedings of the 7th International Symposium on Programming Languages, Implementations, Logics and Programs, PLILP'95 poster abstract, Utrecht, Holland; full version is Technical Report CSTR-95-016, Department of Computer Science, University of Bristol, 1995. 17. H. Salam and J. Gallagher. Proving properties of terms using abstract compilag tion into CLP. In Proceedings of JICSLP'96 post conference Workshop on Meta Programming and Metareasoning in Logic, META'96. Uppsala University, Uppsala, Sweden, 1996. 18. H. Salam and J. Gallagher. Static analysis of logic programs using CLP as a g meta-language. Technical Report CSTR-96-003, University of Bristol, Department of Computer Science, 1996. 19. A. van Gelder. Deriving constraints among argument sizes in logic programs. In Principles of Database Systems; Nashville, Tennessee, pages 47 60, 1990. 20. K. Verschaetse and D. De Schreye. Derivation of linear size relations by abstract interpretation. In Proceedings of the 4th International Symposium on Programming Language Implementation and Logic Programming, PLILP'92, Leuven, Belgium, volume 631 of lncs, pages 296 310. Springer-Verlag, 1992. 21. E. Yardeni and E.Y. Shapiro. A type system for logic programs. Journal of Logic Programming, 102:125 154, 1990.
A This article was processed using the L TEX macro package with LLNCS style
copyright ©right 2010-2020。