MAX-PLANCK-INSTITUT FÜR

INFORMATIK

Analysis of Nonlinear Constraints in

CLP(R)

Michael Hanus

MPI–I–92–251 November 1992

[figure: I N F O R M A T I K]

Im Stadtwald W 6600 Saarbrücken

Germany Author’s Address

Michael Hanus Max-Planck-Institut für Informatik Im Stadtwald W-6600 Saarbrücken Germany

michael@mpi-sb.mpg.de

Acknowledgements

The research described in this paper was supported in part by the German Ministry for Research and Technology (BMFT) under grant ITS 9103 and by the ESPRIT Basic Research Working Group 6028 (Construction of Computational Logics). The responsibility for the contents of this publication lies with the author.

Abstract

Solving nonlinear constraints over real numbers is a complex problem. Hence constraint logic programming languages like CLP(R) or Prolog III solve only linear constraints and delay nonlinear constraints until they become linear. This efficient implementation method has the disadvantage that sometimes computed answers are unsatisfiable or infinite loops occur due to the unsatisfiability of delayed nonlinear constraints. These problems could be solved by using a more powerful constraint solver which can deal with nonlinear constraints like in RISC-CLP(Real). Since such powerful constraint solvers are not very efficient, we propose a compromise between these two extremes. We characterize a class of CLP(R) programs for which all delayed nonlinear constraints become linear at run time. Programs belonging to this class can be safely executed with the efficient CLP(R) method while the remaining programs need a more powerful constraint solver.

Keywords

Logic Programming, Constraints, Abstract Interpretation

1 Introduction

The constraint logic programming paradigm [JL87] generalizes logic programming by replacing the Herbrand universe of terms by other, in general more powerful, domains. Unification of terms is replaced by solving constraints over these domains. For instance, CLP(R) [JMSY92b, HJM^{+}91] adds real numbers to the Herbrand universe and contains equations and inequations as constraints. The system includes a constraint solver over the real numbers. Since solving nonlinear constraints is a complex problem, the constraint solver in CLP(R) is restricted to linear constraints. Nonlinear constraints are delayed until some variables in these constraints get unique values during the further computation process so that the delayed constraints become linear [JMY91] (this approach is also taken in Prolog III [Col90]). If a computation stops with some delayed nonlinear constraints, the system generates a “maybe” answer, i.e., it is not ensured that a solution exists.

Example 1.1 Consider the following CLP(R) program to compute mortgage payments:

   mortgage(P,T,IR,B,MP) :-
           T > 0, T <= 1,
           B = P*(1+T*IR) - T*MP.
   mortgage(P,T,IR,B,MP) :-
           T > 1,
           mortgage(P*(1+IR)-MP, T-1, IR, B, MP).

The parameters are the principal P, the life of the mortgage T (in months), the monthly interest rate IR, the outstanding balance B, and the monthly payment MP. Due to the constraint solving mechanism this program can be queried in different ways. The query

   ?- mortgage(100000, 180, 0.01, 0, MP).

asks for the monthly payment to finance a mortgage, and the answer constraint is MP=1200.17. The query

   ?- mortgage(100000, T, 0.01, 0, 1400).

asks for the time to finance a mortgage, and the answer constraint is T=125.901. The query

   ?- mortgage(P, 180, 0.01, B, MP).

asks for a relationship between the principal, the outstanding balance and the monthly payment, and the answer constraint is P=0.166783*B+83.3217*MP. But if we want to compute the interest rate as in the query

   ?- mortgage(1000, 2, IR, 0, 600).

CLP(R) cannot compute a solved answer due to the restriction to linear constraints. The CLP(R) system produces the “maybe” answer 600=(1000*IR+400)*(IR+1). □

The CLP(R) method of delaying nonlinear constraints and solving only linear constraints is efficient and successful for many problems. However, there are also problems where this method is not sufficient because CLP(R) continues a computation with unsatisfiable nonlinear constraints. This may generate unsatisfiable answers or infinite loops. Such problems can be avoided if a more powerful constraint solver is used. For instance, CAL [ASS^{+}88] and RISC-CLP(Real) [Hon92] do not delay nonlinear constraints but apply special methods from computer algebra to check the satisfiability of all constraints.

Example 1.2 [Hon92] Consider the following program for computing Pythagorean numbers:

   nat(X) :- X = 1.
   nat(X) :- X > 1, nat(X-1).
   pyth(X,Y,Z) :- X*X + Y*Y = Z*Z, X <= Y, nat(Z), nat(X), nat(Y).

If we ask the query ?-pyth(X,Y,Z), CLP(R) runs into an infinite loop since it does not detect that the linear and nonlinear constraints are not satisfiable, while RISC-CLP(Real) computes the

answers X=3,Y=4,Z=5, X=6,Y=8,Z=10, and so on.  □

Unfortunately, it is difficult to deal with nonlinear constraints, and constraint solvers for nonlinear constraints are not very efficient. Therefore it is undesirable to use such complex constraint solvers for problems which can be solved by the CLP(R) method. Hence we propose a compromise between these two extremes. In the following we will characterize a class of CLP(R) programs for which all delayed nonlinear constraints become linear at run time. Since such a property is undecidable in general, our characterization is based on a compile-time analysis of CLP(R) programs using abstract interpretation techniques. Consequently, we cannot give a precise characterization of this class of programs but we compute a safe approximation of it. It is ensured that the CLP(R) computation of a program belonging to this approximated class does not stop with delayed nonlinear constraints.

Our method analyses the nonlinear constraints which may occur at run time. A nonlinear constraint is an equation or inequation containing an expression X*Y where both X and Y do not have unique values. In order to decide whether such a constraint becomes linear, we must know if X or Y are constrained to unique values. Thus we need a program analysis corresponding to groundness analysis in logic programming [Bru91, Deb89, Nil88]. A groundness analysis where variables are simply abstracted into values like ground, free or any is not sufficient for our purpose since in constraint logic programming variables often become ground due to addition of new constraints. For instance, consider the following sequence of constraints:

   ?- Z = X*Y,  X = A+B,  C = 3+A,  B = 5,  C = 6.

A simple groundness analysis would infer that only B and C are ground after the left-to-right evaluation of this goal. But due to the constraint solving mechanism, also A and X become ground and therefore the constraint Z=X*Y is linear at the end of this goal.^{1} In order to provide an analysis of such situations, our method considers the dependencies of variables in constraints and approximates the grounding of variables due to constraint solving.

In the next section we give a detailed description of the syntax and the operational semantics of a restricted class of CLP(R) programs for which our analysis is designed. The abstract domain and the abstract interpretation algorithm for the analysis of nonlinear constraints in CLP(R) programs are presented in Section 3. The correctness of our method is proved in Section 4. In Section 5 we show the extension of our method to other delayed constraints which may occur in CLP(R) programs. Finally, we discuss possible applications of our method in Section 6.

1In this simple example the groundness analysis can be improved by considering all constraints in an arbitrary order instead of a left-to-right order. However, this cannot be done in general if the constraints originate from the execution of several predicates.

2 Operational semantics of CLP(R) programs

In this section we present the class of CLP(R) programs which we will analyse and the operational semantics of CLP(R) programs.

A CLP(R) program is a collection of Horn clauses where some functors and predicates have a predefined meaning. Terms are built from variables, numeric constants (real numbers), atoms (string constants), uninterpreted functor symbols with a positive arity, and the predefined arithmetic functions +, - and *.^{2} An arithmetic term does not contain atoms and uninterpreted functor symbols.^{3} A constraint is an equation t_{1}=t_{2}, where t_{1} and t_{2} are terms, or an inequation t_{1} ⊙ t_{2}, where t_{1} and t_{2} are arithmetic terms and ⊙ ∈ {<, >, <=, >=}. A literal is a defined predicate name together with a list of argument terms. Literals are sometimes considered as terms, i.e., the defined predicate names are also functor symbols. A clause has the form L :- L_{1},…,L_{n} where L is a literal and L_{1},…,L_{n} is a sequence of literals and constraints. For instance, the clauses of Examples 1.1 and 1.2 are CLP(R) programs in this sense.

The operational semantics of CLP(R) programs is similar to Prolog’s operational semantics (SLD-resolution with leftmost selection rule) but with the difference that unification is replaced by adding a new equation between the literal and the clause head, and the computation proceeds only if all constraints (except the nonlinear) are satisfiable. To give a precise definition of the operational semantics, a goal is written in the form C, D ?- G where C is a collection of satisfiable constraints, D is a collection of delayed constraints and G is a sequence of literals and constraints. Initially, C and D are empty and G is the given goal.

A computation step is performed as follows. If the first (leftmost) element of G is a constraint, then it is moved to C if it is linear, otherwise to D. If the first element of G is a literal L, then it is deleted in G and the new equational constraint L=L_{0} is generated where L_{0} :- L_{1},…,L_{n} is (a new variant of) a program clause. Solving the constraint L=L_{0} corresponds to unification in logic programming. Since L or L_{0} may contain terms of the form X*Y, L=L_{0} gives rise to a collection of constraints C′&D′ where D′ is the collection of nonlinear constraints. Hence C′ is added to C and D′ is added to D. A computation fails is the new set of linear constraints is unsatisfiable which is checked by the constraint solver.

It may be the case that a delayed constraint in D becomes linear due to the fact that the addition of new constraints in C implies the linearity of the delayed constraint because some of the variables in the initially nonlinear constraint get unique values. If this happens during a computation step, this delayed constraint is moved from D to C. More details about the operational semantics and the delay mechanism can be found in [JMSY92b, HJM^{+}91, JMY91].

A derivation is called successful if both G and D are empty. If G is empty but D not, the derivation is called conditionally successful since it is not ensured that the constraints in D are satisfiable. The main goal of this paper is the characterization of a class of programs which have no conditionally successful derivations. As an example for the operational semantics consider the following initial goal:

2Similarly to CLP(R) [JMSY92b] we assume that a CLP(R) program is well-typed, i.e., variables, uninterpreted functors and predicates are used in such a way that arithmetic constraints do not contain “junk” like atoms at run time. However, this is not required in the formal description of CLP(R) programs due to the sake of simplicity. In order to check well-typedness at compile time we may extend the language with a type system for logic programming (see, for instance, [Han91] or the collection [Pfe92]).

3In contrast to CLP(R) we do not consider other arithmetic functions like /, sin, cos, pow, abs, min and max.

These functions can be treated similarly to * in our abstract interpretation algorithm. We will discuss this subject in Section 5.

   ?- Z = X*Y,  X = A+B,  C = 3+A,  B = 5,  C = 6.

Then a successful derivation consists of the following elements:

C  D  ?- G

    ∅  ∅  ?- Z=X*Y, X=A+B, C=3+A, B=5, C=6
    ∅  {Z=X*Y} ?- X=A+B, C=3+A, B=5, C=6
    {X=A+B}  {Z=X*Y} ?- C=3+A, B=5, C=6
    {X=A+B, C=3+A}  {Z=X*Y} ?- B=5, C=6
    {X=A+B, C=3+A, B=5}  {Z=X*Y} ?- C=6
    {X=A+B, C=3+A, B=5, C=6, Z=X*Y} ∅  ?-

Note that the delayed constraint has been moved to the set of linear constraints in the last computation step because the constraints {X=A+B, C=3+A, B=5, C=6} imply the linearity of Z=X*Y. An equivalent but simplified form of the last constraint set is {X=8, A=3, B=5, C=6, Z=8*Y}.

In order to keep the abstract interpretation algorithm simple, we transform CLP(R) programs into flat CLP(R) programs where each literal has the form p(X_{1}, …, X_{n}) (all X_{i} are distinct variables) and each constraint has one of the following forms (X, Y, Y_{1},…,Y_{n}, Z are variables, c is an atom or numeric constant and f is an uninterpreted functor symbol):

   X = Y         X = c         X = f(Y_{1},. . .,Y_{n})
   X = Y+Z       X = Y-Z       X = Y*Z
   X < Y         X > Y         X <= Y         X >= Y

It is obvious that every CLP(R) program can be transformed into a flat CLP(R) program by replacing terms by new variables and adding equations between the replaced terms and the corresponding new variables. For instance, consider the mortgage program in Example 1.1. This CLP(R) program is transformed into the following equivalent flat CLP(R) program:

   mortgage(P,T,IR,B,MP) :-
           A = 0, T > A, C = 1, T <= C,
           D = T*IR, E = C+D, F = P*E,
           G = T*MP, B = F-G.
   mortgage(P,T,IR,B,MP) :-
           A = 1, T > A,
           C = A+IR, D = P*C, E = D-MP, F = T-A,
           mortgage(E, F, IR, B, MP).

This transformation does not change the principal answer behaviour. The only difference is that the transformed programs have more derivation steps (for the new equations) and additional equational constraints for the new variables. In the following we assume that all programs are flat CLP(R) programs.

3 Abstract interpretation of CLP(R) programs

In this section we present a method for the compile-time analysis of nonlinear constraints in CLP(R), i.e., a method for checking at compile time whether all nonlinear constraints become linear during the execution of the program. Obviously, a precise analysis requires a solution to the halting problem. Therefore we present an approximation to it based on an abstraction of the concrete behaviour of the program. If this approximation yields a positive answer, then it is ensured that all nonlinear constraints become linear at run time.

We assume familiarity with basic ideas of abstract interpretation techniques (see, for instance, the collection [AH87]). After the fundamental work of Cousot and Cousot [CC77] on systematic methods for program analysis several frameworks for the abstract interpretation of logic programs have been developed (see, for instance, [Bru91, LCMVH91, Nil90]). These frameworks can also be used for the analysis of CLP(R) programs because of the similar operational semantics (SLDresolution with left-to-right selection rule). The only differences to logic programming are:

• Substitutions are replaced by collections of constraints. E.g., the substitution {X↦1,Y↦f(a)} can be represented by the constraints {X=1,Y=f(a)}.

• Unification of a goal literal L and a clause head H is replaced by adding the constraint L=H to the current constraint set. The existence of a unifier is then equivalent to the satisfiability of the extended constraint set.

• The composition of substitutions (e.g., combining the computed unifier with the previous substitution) is replaced by the conjunction of constraints.

Therefore we must define an appropriate abstraction of constraints (the abstract domain) and of constraint solving (the abstract operations). The correctness of the abstract interpretation algorithm can be proved by relating the abstractions to the concrete constraints. In the following we present the abstract domain and the abstract operations. The relation to concrete computations is presented in Section 4.

3.1 An abstract domain for the analysis of nonlinear constraints

The most important component of an abstract interpretation procedure is an abstract domain which approximates subsets of the concrete domain by finite representations. An element of the abstract domain describes common properties of a subset of the concrete domain. In our case the concrete domain is the set of all constraints where a constraint is a conjunction of equations and inequations. The following properties of constraints are important for the analysis of nonlinear constraints:

1. Which variables are ground, i.e., which variables have unique values in all solutions of the constraint?

2. Which nonlinear elements are contained in the constraint?

The precise form of the nonlinear elements is not relevant for the analysis. Only the name of the variables in the nonlinear elements are important in order to decide the linearity of the elements. Therefore our abstract domain contains elements of the form

delay(X or Y)

representing a potential nonlinear constraint which will become linear if X or Y are constrained to unique values. Thus a correct abstraction of the constraint set

                         X = Y*Z, X = A*B, T = A*C, B = 3

must contain the elements delay(Y or Z) and delay(A or C). It may also contain the element delay(A or B) if the information “B is unique” is not available. Note that the order of the variables in delay(X or Y) is not relevant, i.e., in the following we identify the elements delay(X or Y) and delay(Y or X).

A simple abstraction of groundness information of variables is a list of variables which are definitely ground [Nil88] or an assignment of variables to the values ground, free or any [Bru91]. However, this is not sufficient in our case since in constraint logic programming variables become ground not only by unification but also, and more important, by solving constraints when new constraints are added or delayed nonlinear constraints are awakened (like in CLP(R)). For instance, if the current constraints contain X=Y*Z, T=3+Y, then the addition of the new constraint T=5 would cause Y to become ground and Y*Z to become linear. Hence our abstractions contain information about the dependencies between variables. To be more precise, our abstract domain contains elements of the form

V ⇒X

representing the fact that the variables in the set V uniquely determines the value of the variable X. As an extreme case, the abstraction element ∅⇒X represents the fact that X has unique value, i.e., X is ground. For instance, an abstraction of the constraints A=B+C, D=3+A may contain the elements

{B,C}⇒A, {A,C}⇒B, {A,B}⇒C, {A}⇒D, {D}⇒A .

In our abstract interpretation algorithm we analyse the goal and each clause occurring in the program. The abstractions computed in this algorithm contain information about the variables in the goal or clause. Hence each abstraction A has a domain dom(A) which is usually a set of variables occurring in some clause or goal. All variables occurring in A must belong to dom(A).

Altogether, the abstract domain A contains the element ⊥ (representing the empty subset of the concrete domain) and sets containing the following elements (such sets are called abstractions and denoted by A, A_{1} etc):

Element: Meaning:
V ⇒X

the values of V determine the value of X

delay(X or Y) there is a delayed constraint which will be awakened if X or Y are ground, i.e., if X or Y have a unique value

delay

there is a delayed constraint which depends on arbitrary variables

Obviously, the finiteness of dom(A) imply the finiteness of A. The additional element delay is the “worst case” in the algorithm and will be used if the dependencies between nonlinear constraints and their variables are too complex for a finite representation in the algorithm. For convenience we simply write “X” instead of “∅⇒X”. Hence an element “X” in an abstraction means that variable X has a unique value.

For the sake of simplicity we will sometimes generate abstractions containing redundant information. The following normalization rules eliminate some redundancies in abstractions:

Normalization rules for abstractions:

A ∪ {Z, V ∪ {Z}⇒X} ⟶ A ∪ {Z, V ⇒X}  (N1)
A ∪ {X, delay(X or Y)} ⟶ A ∪ {X}  (N2)
A ∪ {V_{1}⇒X, V_{2}⇒X}  ⟶ A ∪ {V_{1}⇒X}  if V_{1} ⊆ V_{2}  (N3)

An abstraction A is called normalized if none of these normalization rules is applicable to A. Later we will see that the normalization rules are invariant w.r.t. the concrete constraints corresponding to abstractions. Therefore we can assume that we compute only with normalized abstractions in the abstract interpretation algorithm.

It is possible to add further normalization rules to delete some obvious redundancies, like

A ∪ {V ∪ {X}⇒X} ⟶ A
A ∪ {delay(X or Y), delay} ⟶ A ∪ {delay}

This should be done in a concrete implementation in order to keep the abstractions as small as possible. However, these rules are not necessary for our intended results. Therefore we omit these rules since it simplifies the correctness proofs in Section 4.

3.2 The abstract interpretation algorithm

The abstract interpretation algorithm is based on abstract operations corresponding to concrete operations during program execution. The most important concrete operations are the processing of a new constraint, the call of a clause for a predicate and the exit of a clause. In the following we describe the corresponding abstract operations.

First we describe the processing of a new constraint at the abstract level. It is the most important operation in constraint logic programming and corresponds to unification in logic programming. At the abstract level it is a function ai-con(α, C) which takes an element of the abstract domain α ∈ A and a single constraint C (equation or inequation) as input and produces another abstract domain element as the result. α is an abstraction of the possible given constraints and the result should be an abstraction of the given constraints together with the new constraint C. Since we are dealing with flat CLP(R) programs where all constraints have a restricted form (compare Section 2), it is sufficient to define ai-con by the following equations:

ai-con(⊥, C)  = ⊥
ai-con(A, X=Y)  = A ∪ {{X}⇒Y, {Y}⇒X}
ai-con(A, X=c)  = A ∪ {X}
ai-con(A, X=f(Y_{1},…,Y_{n})) = A ∪ {{Y_{1},…,Y_{n}}⇒X, {X}⇒Y_{1}, …, {X}⇒Y_{n}}
ai-con(A, X=Y+Z)  = A ∪ {{Y,Z}⇒X, {X,Z}⇒Y, {X,Y}⇒Z}
ai-con(A, X=Y-Z)  = A ∪ {{Y,Z}⇒X, {X,Z}⇒Y, {X,Y}⇒Z}
ai-con(A, X=Y*Z)  = A ∪ {{Y,Z}⇒X, delay(Y or Z)}
ai-con(A, X⊙Y)  = A  if ⊙ ∈ {<, >, <=, >=}

The constraint X=Y implies a mutual dependency between both variables while the constraint X=f(Y_{1},…,Y_{n}) implies a dependency between X and the argument variables of the compound term. The variable X becomes ground by the constraint X=c while it may become ground by the constraints X=Y+Z or X=Y-Z if two of the three variables are ground. The situation for X=Y*Z is a little bit different. Here X is ground if Y and Z are ground. But Y becomes ground only if X and Z are ground and Z ≠ 0. Since we have no access to the concrete values in our abstract domain, we cannot formulate this condition at the abstract level.^{4} Similarly, we cannot express the fact that X becomes ground by the constraint X=Y*Z if Y or Z have a zero value. This is also the reason why inequations have no influence on the abstraction, i.e., implicit equations generated by inequations (e.g., the inequations X<=1,X>=1 generate the implicit equation X=1) are not detected at the abstract level.

Note that the function ai-con adds information to the current abstraction. The processing of this information (corresponding to constraint solving) is performed by the normalization rules. For instance, consider the goal

   ?- Z = X*Y,  U = V+X,  U = 5,  V = 3.

If we apply ai-con to the constraints from left to right starting with the empty abstraction, we obtain the abstraction

   { {X,Y}⇒Z, delay(X or Y), {V,X}⇒U, {U,X}⇒V, {U,V}⇒X, U, V }

which is not normalized. But this abstraction can be transformed by the normalization rules as follows:

    { {X,Y}⇒Z, delay(X or Y), {V,X}⇒U, {U,X}⇒V, {U,V}⇒X, U, V }

→ { {X,Y}⇒Z, delay(X or Y), {U,X}⇒V, {U,V}⇒X, U, V }  (by rule N3)
→ { {X,Y}⇒Z, delay(X or Y), {U,V}⇒X, U, V }  (by rule N3)
→ { {X,Y}⇒Z, delay(X or Y), {V}⇒X, U, V }  (by rule N1)
→ { {X,Y}⇒Z, delay(X or Y), X, U, V }  (by rule N1)
→ { {X,Y}⇒Z, X, U, V }  (by rule N2)
→ { {Y}⇒Z, X, U, V }  (by rule N1)

The last normalized abstraction is a correct abstraction of the simplified answer constraint Z=2*Y, X=2, U=5, V=3. But note that {Z}⇒Y is not contained in the last abstraction since the concrete value of X is not present in this abstraction.

We also need abstract operations for the abstract interpretation of literals (defined predicates). The next operation restricts an abstraction A to a set of variables W ⊆ dom(A). It will be used in a predicate call to omit the information about variables not passed from the predicate call to the applied clause:

call-restrict(⊥, W) = ⊥
call-restrict(A, W) = {V ⇒X ∈ A | {X} ∪ V ⊆ W }

This operation also deletes all delay information in the given abstraction. This is justified since all omitted information is reconsidered after the predicate call (see below).

At the end of a clause a similar operation is necessary to forget the information about local clause variables. Hence we define:

exit-restrict(⊥, W) = ⊥

4This can be improved by including information about the sign of variables in our abstract domain. For instance, we could include (strict) inequalities between variables and the constant 0 as in the abstract domain Ineq of [JMM91].

exit-restrict(A, W) = {V ⇒X ∈ A | {X} ∪ V ⊆ W }
∪ {delay(X or Y) ∈ A | X, Y ∈ W }
∪ {delay | delay ∈ A or delay(X or Y) ∈ A with {X, Y} ⊈ W }

The restriction operation for clause exits transforms an abstraction element delay(X or Y) into the element delay if one of the involved variables is not contained in W, i.e., it is noted that there may be a delayed constraint which depends on local variables at the end of the clause, but the possible dependencies are too complex for a finite abstract analysis.

The least upper bound operation is used to combine the results of different clauses for a predicate call:

⊥ ⊔ A = A
A ⊔ ⊥ = A
A_{1} ⊔ A_{2} = {V_{1} ∪ V_{2}⇒X | V_{1}⇒X ∈ A_{1}, V_{2}⇒X ∈ A_{2}}
∪ {delay(X or Y) | delay(X or Y) ∈ A_{1} or delay(X or Y) ∈ A_{2}}
∪ {delay | delay ∈ A_{1} or delay ∈ A_{2}}

Now we are able to present the algorithm for the abstract interpretation of a flat CLP(R) program. It is specified as a function ai(α, L) which takes an abstract domain element α and a literal or constraint L and yields a new abstract domain element as result. Clearly, ai(⊥, L) =⊥ and ai(A, C) = ai-con(A, C) for all constraints C. The interesting case is the abstract interpretation of a literal (defined predicate call) ai(A, p(X_{1}, …, X_{n})) which is computed by the following steps (var(ξ) denotes the set of all variables occurring in the syntactic construction ξ):

1. Let p(Z_{1}, …, Z_{n}) :- L_{1}, …, L_{k} be a clause for predicate p (if necessary, rename the clause variables such that they are disjoint from X_{1}, …, X_{n}) Compute A_{call} = call-restrict(A, {X_{1}, …, X_{n}})

A_{0} = ⟨replace all X_{i} by Z_{i} in A_{call}⟩ (i.e., dom(A_{0}) = {Z_{1}, …, Z_{n}} ∪ ⋃_{i=1}^{k} var(L_{i}))

A_{1} = ai(A_{0}, L_{1})
A_{2} = ai(A_{1}, L_{2})
⋮
A_{k} = ai(A_{k−1}, L_{k})
A_{out} = exit-restrict(A_{k}, {Z_{1}, …, Z_{n}})
A_{exit} = ⟨replace all Z_{i} by X_{i} in A_{out}⟩ (i.e., dom(A_{exit}) = dom(A))

2. Let A_{exit}^{1}, …, A_{exit}^{m} be the exit substitutions of all clauses for p as computed in step 1. Then define A_{success} = A_{exit}^{1} ⊔ … ⊔ A_{exit}^{m}

3. ai(A, p(X_{1}, …, X_{n})) = A_{success} ∪ (A − A_{call}) if A_{success} ≠⊥, else ⊥

Step 1 interprets a clause in the following way. Firstly, the call abstraction is computed, i.e., the information contained in the abstraction for the predicate call is restricted to the argument variables (A_{call}). The domain is changed to the clause variables by mapping argument variables to the corresponding variables of the applied clause (A_{0}). Then each literal in the clause body is interpreted. The resulting abstraction (A_{k}) is restricted to the variables in the clause head, i.e., we forget the information about the local variables in the clause. Potential delayed constraints which are not awakened at the clause end are passed to the abstraction A_{out} by the exit-restrict operation. In the last step the domain is changed to the original variables by renaming the variables of the clause head into the variables of the predicate call (A_{exit}). If all clauses defining the called predicate p are interpreted in this way, all possible interpretations are combined by the least upper bound of all abstractions (A_{success}). The combination of this abstraction with the information which was forgotten by the restriction at the beginning of the predicate call yields the abstraction after the predicate call (step 3).

Unfortunately, this abstract interpretation algorithm does not terminate in case of recursive programs. Since this problem is solved in all frameworks for abstract interpretation, we do not develop a new solution to this problem but we use one of the well-known techniques. Following Bruynooghe’s framework [Bru91] we construct a rational abstract AND-OR-tree representing the computation of the abstract interpretation algorithm (see also Section 4.3). During the construction of the tree we check before the interpretation of a predicate call P whether there is an ancestor node P′ with a call to the same predicate and the same call abstraction (up to renaming of variables). If this is the case we take the success abstraction of P′ (or ⊥ if it is not available) as the success abstraction of P instead of interpreting P. If the further abstract interpretation computes a success abstraction A′ for P′ which differs from the success abstraction used for P, we start a recomputation beginning at P with A′ as new success abstraction. This iteration terminates because all operations used in the abstract interpretation are monotone (w.r.t. the order on A defined in Section 4) and the abstract domain is finite. A detailed description of this method is given in Section 4.3.

3.3 Examples

The following CLP(R) program computes the product of all elements of a list of arithmetic expressions:

   prod([], 1).
   prod([E|R], E*P) :- prod(R, P).

The corresponding flat CLP(R) program is:

   prod(A, B) :- A = [],     B = 1.
   prod(A, B) :- A = [E|R],  B = E*P,  prod(R, P).

If we query this program with a list of numbers, as in

   ?- prod([2,3,4],Pr).

then the answer constraint is Pr=24. Our abstract interpretation algorithm computes the following abstractions for the initial goal prod(L,Pr) and the initial abstraction {L} (specifying the groundness of the first argument):

ai({L}, prod(L,Pr)):

Interpret the first clause: ai({A}, A=[]) = {A} ai({A}, B=1) = {A, B}

Interpret the second clause: ai({A}, A=[E|R]) = {A, E, R} ai({A, E, R}, B=E*P) = {A, E, R, {P}⇒B}

    ai({A, E, R, {P}⇒B}, prod(R,P)):

Recursive call: Take ⊥ as result since success abstraction of ancestor call not available:

    [figure: ^{{L} prod(L,Pr) {L,Pr}}; OR; ^{{A} prod(A,B) {A,B}  {A} prod(A,B) {A,B}}; AND; ^{{A} A=[]  {A}  B=1 {A,B}}; AND; {A} A=[E|R] A_{1} B=E*P A_{2} prod(R,P) A_{3}]

          A_{1} = {A, E, R}  A_{2} = {A, E, R, {P}⇒B}  A_{3} = {A, E, R, B, P}

Figure 1: Final AND-OR-tree for the abstract interpretation of prod(L,Pr)

ai({L}, prod(L,Pr)) = {L, Pr}⊔ ⊥= {L, Pr}

Recursive call prod(R,P) again: Take the new success abstraction {R, P} of ancestor call: ai({A, E, R, {P}⇒B}, prod(R,P)) = {A, E, R, {P}⇒B, P} → {A, E, R, B, P}

ai({L}, prod(L,Pr)) = {L, Pr} ⊔ {L, Pr} = {L, Pr}

Hence the computed success abstraction is {L, Pr}. This means that after a successful computation of the goal prod(L,Pr) the variable Pr is bound to a ground term and there are no delayed constraints. The final AND-OR-tree for this abstract interpretation is shown in Figure 1 (the abstractions are written to the left and right of the corresponding literal).

In a similar way one can compute the success abstraction of the goal prod(L,Pr) w.r.t. the initial abstraction {Pr}. The result is ai({Pr}, prod(L,Pr)) = {Pr, delay} (compare Section 4.4) indicating that there may be a delayed constraint at the end of the concrete computation. In fact, the CLP(R) computation of the goal

   ?- prod([A,B,C],24).

produces the “maybe” nonlinear answer constraint 24=A*B*C.

Similarly, our abstract interpretation algorithm computes the expected answers (w.r.t. to the delay information) to all queries shown in Example 1.1.

4 Correctness of the abstract interpretation algorithm

In this section we will prove the correctness of the presented abstract interpretation algorithm. As mentioned in Section 3 we use Bruynooghe’s framework [Bru91] for abstract interpretation of logic programs with the modifications listed in the beginning of Section 3. Therefore we have to relate the abstract domain to the concrete domain of constraints by defining a concretisation function. If we can prove that the abstract operations defined in Section 3.2 are correct w.r.t. the corresponding operations on the concrete domain, the correctness of our algorithm is a direct consequence of Bruynooghe’s work.

4.1 Relating abstractions to concrete constraints

Our abstract interpretation algorithm is useless if we have no proposition about the relationship of the computed abstract properties of a flat CLP(R) program and the concrete constraints which can occur at run time. Therefore we have to define a concretisation function γ:A → 2^{C} which maps an abstraction into a subset of the concrete domain. In our case the concrete domain C is the set of all collections of constraints of the form

   X = Y           X = c           X = f(Y_{1},. . .,Y_{n})
   X = Y+Z         X = Y-Z         X = Y*Z
   X < Y           X > Y           X <= Y           X >= Y

where X, Y, Y_{1},…,Y_{n}, Z are variables, c is an atom or numeric constant and f is an uninterpreted functor symbol. These are the constraints accumulated during the execution of a flat CLP(R) program and therefore sometimes called flat constraints. In practice a collection of such constraints is transformed into a simplified non-flat form in order to get a more efficient satisfiability check and readable answer constraints, but this is not relevant for our purpose. The meaning of a collection C ∈ C of constraints is the conjunction of all its elements, i.e., it specifies a set of solutions (mappings from variables into elements of the underlying constraint structure) satisfying each single constraint (cf. [JL87]):

Sol(C) := {σ | σ is a valuation where σ(c) is true for all c ∈ C}

The notion of “groundness” in logic programming corresponds to “uniqueness” of solutions in constraint logic programming. We say that variable X is unique in the constraints C if σ_{1}(X) = σ_{2}(X) for all σ_{1}, σ_{2} ∈ Sol(C). Moreover, we say that a variable set V determines X in C if σ_{1}(X) = σ_{2}(X) for all σ_{1}, σ_{2} ∈ Sol(C) with σ_{1} =_{V} σ_{2}.^{5} In this case we write V ⇒^{C}X. Hence ∅⇒^{C}X is equivalent to X unique in C. We call the arithmetic term X*Y nonlinear in the constraints C if both X and Y are not unique in C, i.e., a constraint containing this term would be delayed in CLP(R).

Now we are able to present the precise definition of the concretisation function γ:A → 2^{C} which relates an abstraction to a set of constraints:

γ(⊥) = ∅
γ(A) = {C ∈ C | 1. V ⇒^{C}X for all V ⇒X ∈ A

2. X=Y*Z ∈ C with Y, Z ∈ dom(A) and Y*Z nonlinear in C ⟹ delay ∈ A or delay(Y or Z) ∈ A }

The first condition expresses that for all abstraction elements V ⇒X ∈ A the variables in V determine the value of X in all constraints corresponding to A. We also say that the constraints C satisfy the variable condition V ⇒X if this condition holds. Hence X ∈ A implies that X is unique in all concrete constraints corresponding to A.

5σ_{1} =_{V} σ_{2} is equivalent to the condition σ_{1}(Z) = σ_{2}(Z) for all Z ∈ V.

The second condition ensures that all nonlinear parts of constraints are contained in A. If this condition holds, we say that the nonlinear term Y*Z is covered by A. But note that only nonlinear terms having variables in the domain of A must be covered by A. This is due to the fact that A contains abstract information about the variables of one clause but during the concrete computation the accumulated constraints may contain nonlinear parts from arbitrary clauses. Since we are interested in the analysis of all nonlinear constraints, we will prove in Theorem 4.8 that the nonlinear constraints with variables outside dom(A) are also covered by the abstraction A.

Since our abstract interpretation algorithm always simplifies the computed abstractions by the normalization rules of Section 3.1, we have to show that these rules are invariant w.r.t. the concrete interpretation of abstractions. This is the purpose of the following lemma.

Lemma 4.1 If A and A′ are abstractions with A → A′, then γ(A) = γ(A′).

Proof: First we show γ(A) ⊆ γ(A′). Let C ∈ γ(A). We prove C ∈ γ(A′) by a case analysis on the applied normalization rule:

N1: Let A = A_{0}∪{Z, V ∪ {Z}⇒X} and A′ = A_{0}∪{Z, V ⇒X}. Since the only difference between A and A′ is the transformation of “V ∪ {Z}⇒X” into “V ⇒X”, we have to show V ⇒^{C}X. Z is unique in C since Z ∈ A and C ∈ γ(A). Let σ_{1}, σ_{2} ∈ Sol(C) with σ_{1} =_{V} σ_{2}. Then σ_{1} =_{V ∪{Z}} σ_{2} by uniqueness of Z in C. This implies σ_{1}(X) = σ_{2}(X) by V ∪ {Z}⇒X ∈ A.

Hence V ⇒^{C}X.

N2: Let A = A_{0} ∪ {X, delay(X or Y)} and A′ = A_{0} ∪ {X}. If the abstraction element delay(X or Y) covers the nonlinear term X*Y in C, then X is not unique in C. But this is a contradiction to X ∈ A. Therefore C cannot contain the nonlinear term X*Y.

N3: Let A = A_{0} ∪ {V_{1}⇒X, V_{2}⇒X} and A′ = A_{0} ∪ {V_{1}⇒X} with V_{1} ⊆ V_{2}. Obviously, C ∈ γ(A′) since the variable condition V_{2}⇒X is omitted in A′.

Next we show γ(A) ⊇ γ(A′). Let C ∈ γ(A′). As before we prove C ∈ γ(A) by a case analysis on the applied normalization rule:

N1: Let A = A_{0} ∪ {Z, V ∪ {Z}⇒X} and A′ = A_{0} ∪ {Z, V ⇒X}. Obviously, C ∈ γ(A) since

V ⇒^{C}X implies V ∪ {Z}⇒^{C}X.

N2: Let A = A_{0} ∪ {X, delay(X or Y)} and A′ = A_{0} ∪ {X}. This case is trivial since A contains the additional abstraction element “delay(X or Y)”.

N3: Let A = A_{0} ∪ {V_{1}⇒X, V_{2}⇒X} and A′ = A_{0} ∪ {V_{1}⇒X} with V_{1} ⊆ V_{2}. We have to show that C satisfies that variable condition V_{2}⇒X. Let σ_{1}, σ_{2} ∈ Sol(C) with σ_{1} =_{V_{2}} σ_{2}. Then σ_{1} =_{V_{1}} σ_{2} since V_{1} ⊆ V_{2}. Hence σ_{1}(X) = σ_{2}(X) by V_{1}⇒X ∈ A′ and C ∈ γ(A′).

Due to this lemma it makes no difference to use an abstraction A or the normalization of A if we want to prove a proposition like C ∈ γ(A). We will use this property in the correctness proofs for the abstract operations (cf. Section 4.2).

For the termination of the abstract interpretation algorithm it is important that all operations on the abstract domain are monotone. Therefore we define the following order relation on normalized abstractions:

(a) ⊥⊑ α for all α ∈ A
(b) A ⊑ A′ ⟺ 1. V′⇒X ∈ A′ ⟹ ∃V ⊆ V′ with V ⇒X ∈ A
2. delay(X or Y) ∈ A ⇒ delay(X or Y) ∈ A′
3. delay ∈ A ⇒ delay ∈ A′

It is easy to prove that ⊑ is a reflexive, transitive and anti-symmetric relation on normalized abstractions. Moreover, the operation ⊔ defined in Section 3.2 computes the least upper bound of two abstractions:

Lemma 4.2 A_{1} ⊔ A_{2} is a least upper bound of A_{1}, A_{2} ∈ A.

Proof: We assume A_{1} ≠⊥ and A_{2} ≠⊥, otherwise the lemma is obviously true.

First we show that A_{1} ⊔ A_{2} is an upper bound of A_{1} (the case for A_{2} is symmetric): Let V ⇒X ∈ A_{1} ⊔ A_{2}. By definition of ⊔, there are V_{1}⇒X ∈ A_{1} and V_{2}⇒X ∈ A_{2} with V = V_{1} ∪ V_{2}. Hence V_{1}⇒X ∈ A_{1} and V_{1} ⊆ V (condition 1 of ⊑). If α is an abstraction element of the form delay(X or Y) or delay, then α ∈ A_{1} implies α ∈ A_{1} ⊔ A_{2} by definition of ⊔ (conditions 2, 3 of ⊑). Therefore A_{1} ⊑ A_{1} ⊔ A_{2}.

To show that A_{1} ⊔ A_{2} is a least upper bound, assume an abstraction A with A_{1} ⊑ A and A_{2} ⊑ A. If V ⇒X ∈ A, then there are V_{1} ⊆ V and V_{2} ⊆ V with V_{1}⇒X ∈ A_{1} and V_{2}⇒X ∈ A_{2} (by definition of ⊑). This implies V_{1} ∪ V_{2}⇒X ∈ A_{1} ⊔ A_{2} and V_{1} ∪ V_{2} ⊆ V. If δ is an abstraction element of the form delay(X or Y) or delay, then δ ∈ A_{1} ⊔ A_{2} implies δ ∈ A_{1} or δ ∈ A_{2} and hence δ ∈ A by definition of ⊑. Therefore A_{1} ⊔ A_{2} ⊑ A.

It is also easy to show that γ is a monotone function:

Lemma 4.3 If A ⊑ A′, then γ(A) ⊆ γ(A′).

Proof: Let A ⊑ A′ and C ∈ γ(A). (the case A =⊥ is trivial). We have to show C ∈ γ(A′).

Let V′⇒X ∈ A′. Since A ⊑ A′, there is a set V ⊆ V′ with V ⇒X ∈ A. Since C ∈ γ(A), V ⇒^{C}X. This immediately implies V′⇒^{C}X. Hence C satisfies V′⇒X.

Let X=Y*Z ∈ C with Y, Z ∈ dom(A) and Y*Z nonlinear in C. Since C ∈ γ(A), A contains a corresponding delay element covering this nonlinear term. But this delay element is also contained in A′ by definition of ⊑.

It is also not difficult to show that all abstract operations defined in Section 3.2 (call and exit restriction, abstract constraint solving etc.) are monotone. As an example we show the monotonicity of the restriction operation for clause exits.

Lemma 4.4 The abstract operation exit-restrict is monotone.

Proof: Let A_{1} ⊑ A_{2} and A′_{1} := exit-restrict(A_{1}, W), A′_{2} := exit-restrict(A_{2}, W). We have to show: A′_{1} ⊑ A′_{2}.

If A_{1} =⊥, then A′_{1} =⊥ and thus A′_{1} ⊑ A′_{2}. Hence we assume A_{1} ≠⊥ which implies A_{2} ≠⊥ and A′_{1} ≠⊥, A′_{2} ≠⊥.

1. V ⇒X ∈ A′_{2}: By definition of exit-restrict, V ⇒X ∈ A_{2} and {X} ∪ V ⊆ W. Since A_{1} ⊑ A_{2}, there is a set V_{1} ⊆ V with V_{1}⇒X ∈ A_{1}. Hence V_{1}⇒X ∈ A′_{1} because {X}∪V_{1} ⊆ {X}∪V ⊆ W.

2. delay(X or Y) ∈ A′_{1}: By definition of exit-restrict, delay(X or Y) ∈ A_{1} and X, Y ∈ W. This implies delay(X or Y) ∈ A_{2} and thus delay(X or Y) ∈ A′_{2}.

3. delay ∈ A′_{1}: By definition of exit-restrict, either delay ∈ A_{1} which implies delay ∈ A_{2} and delay ∈ A′_{2}, or delay(X or Y) ∈ A_{1} with {X, Y } ⊈ W. The latter case implies delay(X or Y) ∈ A_{2} and delay ∈ A′_{2}.

4.2 Correctness of abstract operations

Following the framework presented in [Bru91], the correctness of the abstract interpretation algorithm can be proved by showing the correctness of each basic operation of the algorithm (like abstract constraint solving, clause entry and clause exit). Correctness means in this context that all concrete computations, i.e., the results of the concrete constraint solving, clause entry and clause exit (cf. Section 2) are subsumed by the abstractions computed by the corresponding abstract operations. In this section we will prove the correctness of each of these operations.

First we prove that the abstract constraint solving ai-con covers all possible concrete constraints obtained by adding a new constraint to a given set of constraints.

Theorem 4.5 (Correctness of abstract constraint solving) Let A be an abstraction, c be a flat constraint (as defined in Section 4.1) with var(c) ⊆ dom(A). Then C ∪ {c} ∈ γ(ai-con(A, c)) for all C ∈ γ(A).

Proof: First we prove the theorem for equational constraints. Let A be an abstraction, X=t be a flat constraint with {X} ∪ var(t) ⊆ dom(A), and C ∈ γ(A). We prove the theorem for each of the possible cases for t. \underline{t = Y}: Then

A′ := ai-con(A, X=Y) = A ∪ {{X}⇒Y, {Y}⇒X}

We have to show: C′ := C ∪ {X=Y} ∈ γ(A′).

1. {Y}⇒X ∈ A′: Let σ_{1}, σ_{2} ∈ Sol(C′) with σ_{1}(Y) = σ_{2}(Y). Since σ_{i} is a solution of X=Y, σ_{i}(X) = σ_{i}(Y) (i = 1, 2). This implies σ_{1}(X) = σ_{2}(X).

2. {X}⇒Y ∈ A′: Symmetric to the previous case.

3. V ⇒Z ∈ A: Let σ_{1}, σ_{2} ∈ Sol(C′) with σ_{1} =_{V} σ_{2}. Since σ_{1}, σ_{2} ∈ Sol(C) and C ∈ γ(A), σ_{1}(Z) = σ_{2}(Z). Hence V ⇒^{C′}Z. Therefore C′ satisfies all variable conditions of A′.

4. Let Z=Z_{1}*Z_{2} ∈ C′ with Z_{1}, Z_{2} ∈ dom(A) and Z_{1}*Z_{2} nonlinear in C′. Clearly, Z_{1}*Z_{2} is also nonlinear in C. Thus C ∈ γ(A) implies that delay ∈ A ⊆ A′ or delay(Z_{1} or Z_{2}) ∈ A ⊆ A′. In any case the nonlinear term Z_{1}*Z_{2} is also covered by A′.

\underline{t = f(Y_{1},…,Y_{n})} with f an uninterpreted functor symbol: Then

A′ := ai-con(A, X=f(Y_{1},…,Y_{n})) = A ∪ {{Y_{1},…,Y_{n}}⇒X, {X}⇒Y_{1}, …, {X}⇒Y_{n}}

We have to show: C′ := C ∪ {X=f(Y_{1},…,Y_{n})} ∈ γ(A′).

1. {Y_{1},…,Y_{n}}⇒X ∈ A′: Let σ_{1}, σ_{2} ∈ Sol(C′) with σ_{1} =_{{Y_{1},…,Y_{n}}} σ_{2}. Since σ_{1} and σ_{2} are solutions of X=f(Y_{1},…,Y_{n}),

σ_{1}(X) = σ_{1}(f(Y_{1},…,Y_{n})) = σ_{2}(f(Y_{1},…,Y_{n})) = σ_{2}(X)

2. {X}⇒Y_{i} ∈ A′ for some i ∈ {1, …, n}: Let σ_{1}, σ_{2} ∈ Sol(C′) with σ_{1}(X) = σ_{2}(X). Since σ_{1} and σ_{2} are solutions of X=f(Y_{1},…,Y_{n}),

σ_{1}(f(Y_{1},…,Y_{n})) = σ_{1}(X) = σ_{2}(X) = σ_{2}(f(Y_{1},…,Y_{n}))

This equation implies σ_{1}(Y_{i}) = σ_{2}(Y_{i}) because f is an uninterpreted functor symbol in the domain of CLP(R).

3. V ⇒Z ∈ A: This is identical to the case t = Y.

4. Let Z=Z_{1}*Z_{2} ∈ C′ with Z_{1}, Z_{2} ∈ dom(A) and Z_{1}*Z_{2} nonlinear in C′. This case is also identical to t = Y.

\underline{t = c}: This is a particular case of t = f(Y_{1},…,Y_{n}). \underline{t = Y_{1}+Y_{2}}: Then

A′ := ai-con(A, X=Y_{1}+Y_{2}) = A ∪ {{Y_{1},Y_{2}}⇒X, {X,Y_{1}}⇒Y_{2}, {X,Y_{2}}⇒Y_{1}}

We have to show: C′ := C ∪ {X=Y_{1}+Y_{2}} ∈ γ(A′).

1. {Y_{1},Y_{2}}⇒X ∈ A′: Let σ_{1}, σ_{2} ∈ Sol(C′) with σ_{1} =_{{Y_{1},Y_{2}}} σ_{2}. Since σ_{1} and σ_{2} are solutions of

X=Y_{1}+Y_{2},

σ_{1}(X) = σ_{1}(Y_{1}) + σ_{1}(Y_{2}) = σ_{2}(Y_{1}) + σ_{2}(Y_{2}) = σ_{2}(X)

(note that + is the addition function on real numbers while + is the syntactic denotation for an addition constraint). Hence {Y_{1}, Y_{2}}⇒^{C′}X.

2. {X,Y_{1}}⇒Y_{2} ∈ A′: Let σ_{1}, σ_{2} ∈ Sol(C′) with σ_{1} =_{{X,Y_{1}}} σ_{2}. Since σ_{1} and σ_{2} are solutions of

X=Y_{1}+Y_{2}

σ_{1}(Y_{2}) = σ_{1}(X) − σ_{1}(Y_{1}) = σ_{2}(X) − σ_{2}(Y_{1}) = σ_{2}(Y_{2})

Hence {X, Y_{1}}⇒^{C′}Y_{2}.

3. {X,Y_{2}}⇒Y_{1} ∈ A′: This is symmetric to the previous case.

4. V ⇒Z ∈ A: This is identical to the case t = Y.

5. Let Z=Z_{1}*Z_{2} ∈ C′ with Z_{1}, Z_{2} ∈ dom(A) and Z_{1}*Z_{2} nonlinear in C′. This case is also identical to t = Y.

\underline{t = Y_{1}-Y_{2}}: Analogous to the case t = Y_{1}+Y_{2}. \underline{t = Y_{1}*Y_{2}}: Then

A′ := ai-con(A, X=Y_{1}*Y_{2}) = A ∪ {{Y_{1},Y_{2}}⇒X, delay(Y_{1} or Y_{2})}

We have to show: C′ := C ∪ {X=Y_{1}*Y_{2}} ∈ γ(A′).

1. {Y_{1},Y_{2}}⇒X ∈ A′: Analogous to the case t = Y_{1}+Y_{2}.

2. V ⇒Z ∈ A: This is identical to the case t = Y.

3. Let X=Y_{1}*Y_{2} ∈ C′ with Y_{1}*Y_{2} nonlinear in C′. This nonlinear term is covered by A′ because delay(Y_{1} or Y_{2}) ∈ A′.

4. Let Z=Z_{1}*Z_{2} ∈ C′ with Z=Z_{1}*Z_{2} ≠ X=Y_{1}*Y_{2}, Z_{1}, Z_{2} ∈ dom(A) and Z_{1}*Z_{2} nonlinear in C′. This is identical to the case t = Y.

It remains to prove the theorem for inequations. Let A be an abstraction, X⊙Y be an inequation with ⊙ ∈ {<, >, <=, >=} and X, Y ∈ dom(A), and C ∈ γ(A). Since ai-con(A, X⊙Y) = A, we have to show: C′ := C ∪ {X⊙Y} ∈ γ(A).

1. V ⇒Z ∈ A: Let σ_{1}, σ_{2} ∈ Sol(C′) with σ_{1} =_{V} σ_{2}. Since σ_{1} and σ_{2} are also solutions of C and C ∈ γ(A), σ_{1}(Z) = σ_{2}(Z). Hence V ⇒^{C′}Z.

2. Let Z=Z_{1}*Z_{2} ∈ C′ with Z_{1}, Z_{2} ∈ dom(A) and Z_{1}*Z_{2} nonlinear in C′. This case is also identical to the corresponding case for X=Y.

Next we want to prove that the abstract operations performed at the entry of a clause are correct w.r.t. the concrete operational semantics.

Theorem 4.6 (Correctness of clause entry) Let P = p(X_{1}, …, X_{n}) be a predicate call with abstraction A and C ∈ γ(A). Let p(Z_{1}, …, Z_{n}) :- L_{1}, …, L_{k} be a (renamed) clause and A_{0} be the abstraction computed by algorithm ai. Then C ∪ {p(X_{1}, …, X_{n})=p(Z_{1}, …, Z_{n})} ∈ γ(A_{0}).

Proof: Let A_{0} be the abstraction after clause entry, i.e., A_{0} is identical to A except that all delay abstractions are omitted and the variables are restricted to {X_{1}, …, X_{n}} and then renamed to {Z_{1}, …, Z_{n}}. Hence dom(A_{0}) = var(p(Z_{1}, …, Z_{n}) :- L_{1}, …, L_{k}). Let C′ := C ∪ {p(X_{1}, …, X_{n})=p(Z_{1}, …, Z_{n})}. We have to show: C′ ∈ γ(A_{0}).

1. V ⇒Z ∈ A_{0}: Let ρ be the bijective renaming mapping ρ = {Z_{1} ↦ X_{1}, …, Z_{n} ↦ X_{n}}. By definition of A_{0}, ρ(V)⇒ρ(Z) ∈ A. Let σ_{1}, σ_{2} ∈ Sol(C′) with σ_{1} =_{V} σ_{2}. Since σ_{1} and σ_{2} are solutions of p(X_{1}, …, X_{n})=p(Z_{1}, …, Z_{n}), σ_{1} =_{ρ(V)} σ_{2}. Since C ∈ γ(A) and ρ(V)⇒ρ(Z) ∈ A, ρ(V)⇒^{C}ρ(Z), and therefore σ_{1}(ρ(Z)) = σ_{2}(ρ(Z)). This implies σ_{1}(Z) = σ_{2}(Z). Hence V ⇒^{C′}Z.

2. X=Y*Z ∈ C′ with Y, Z ∈ dom(A_{0}) and Y*Z nonlinear in C′. This case cannot occur since the only constraint in C′ with variables from dom(A_{0}) is p(X_{1}, …, X_{n})=p(Z_{1}, …, Z_{n}) (recall that the applied clause is a new variant and has no variables in common with the previous computation).

Next we prove the correctness of the abstract clause exit operations, i.e., we show that all constraints occurring at the end of a clause applied to a predicate call are covered by the abstract interpretation algorithm. Since the execution of a clause only adds new constraints to the constraints present at the beginning of the predicate call, it is sufficient to formulate the correctness criterion as in the following theorem.

Theorem 4.7 (Correctness of clause exit) Let P = p(X_{1}, …, X_{n}) be a predicate call with abstraction A_{in} and C_{in} ∈ γ(A_{in}). Let A = ai(A_{in}, P) = A_{success} ∪ (A_{in} − A_{call}) be the abstraction after the predicate call computed by the abstract interpretation algorithm ai. Let L:- L_{1}, …, L_{k} be a (renamed) clause for P, and A_{k} be the abstraction computed for the clause end in ai. If C_{k} ∈ γ(A_{k}) is an extension of C_{in} and the constraint P =L, i.e., C_{k} = C_{in} ∪ {P =L} ∪ C for some constraints C, then C_{k} ∈ γ(A).

Proof: We show C_{k} ∈ γ(A) if the conditions of the theorem are satisfied. Let L = p(Z_{1}, …, Z_{n}) and ρ be the bijective renaming mapping ρ = {X_{1} ↦ Z_{1}, …, X_{n} ↦ Z_{n}}.

1. V ⇒X ∈ A: We can distinguish two different cases:

(a) V ⇒X ∈ A_{in} − A_{call}: Then V ⇒X ∈ A_{in} and hence V ⇒^{C_{in}}X. This implies V ⇒^{C_{k}}X because C_{k} = C_{in} ∪ {P =L} ∪ C.

(b) V ⇒X ∈ A_{success}: By definition of A_{success}, there exists V′ ⊆ V with ρ(V′)⇒ρ(X) ∈ A_{k} and ρ(V′) ∪ {ρ(X)} ⊆ {Z_{1}, …, Z_{n}}. Hence C_{k} ∈ γ(A_{k}) implies ρ(V′)⇒^{C_{k}}ρ(X). Since each solution of C_{k} is also a solution of X_{i}=Z_{i} (i = 1, …, n), we obtain V′⇒^{C_{k}}X and therefore

V ⇒^{C_{k}}X.

2. X=Y*Z ∈ C_{k} with Y, Z ∈ dom(A) and Y*Z nonlinear in C_{k}. Since C_{k} = C_{in} ∪ {P =L} ∪ C and C contains only new constraints with clause variables which are different from dom(A), the constraint X=Y*Z must occur in C_{in}. Clearly, Y*Z is nonlinear in C_{in} since it is nonlinear in C_{k}. Therefore C_{in} ∈ γ(A_{in}) implies delay ∈ A_{in} or delay(Y or Z) ∈ A_{in}. This delay abstraction is also contained in A because A_{in} −A_{call} ⊆ A and A_{call} does not contain any delay abstractions (by definition of call-restrict). Hence the nonlinear term Y*Z is covered by A.

4.3 Correctness of the abstract interpretation algorithm

In the last section we have proved the local correctness of the three elementary operations of the abstract interpretation algorithm. Bruynooghe [Bru91] has shown that these local correctness criteria are sufficient for the global correctness of the abstract interpretation algorithm. As already sketched in Section 3.2, the abstract interpretation algorithm generates an abstract AND-OR-tree which represents all concrete computations. To avoid infinite paths, this tree is a rational AND-OR-tree, i.e., if a predicate call is identical to (or a variant of) a predicate call in an ancestor node, then this call node is identified with the ancestor node and the abstract success information of the

[figure: A P A′; OR; A_{1}^{in} H_{1} A_{1}^{out}  …  A_{m}^{in} H_{m} A_{m}^{out}]

Figure 2: OR-node for clause entry

[figure: A^{in} H A^{out}; AND; A_{0} L_{1} A_{1}  …  A_{k−1} L_{k} A_{k}]

Figure 3: AND-node for a clause

ancestor node is passed to this predicate call. Since the success abstraction of the predicate call may influence the success abstraction of the corresponding ancestor, the algorithm loops until these two abstractions are identical. The monotonicity property of all abstract operations together with the finite domain avoids an infinite looping in this graph. Now we present the abstract interpretation algorithm in more detail.

The abstract interpretation procedure generates the abstract AND-OR-graph as follows. In the first step, the root is created. It is marked with the initial goal (w.l.o.g. we assume that the initial goal contains only one literal) and the initial abstraction for this goal. Then this initial graph is extended by computing the success abstraction for this goal. The success abstraction A′ of a single constraint c with abstraction A is computed by abstract constraint solving, i.e., A′ = ai-con(A, c) (compare Section 3.2). We distinguish the following cases for the computation of the success abstraction A′ of a node with a predicate call P and abstraction A:

1. There is no ancestor node with the same predicate call and the same call abstraction^{6} (up to renaming of variables): First of all, we add an OR-node as shown in Figure 2 (H_{1}, …, H_{m} are the heads of all clauses for P). A_{i}^{in} is the abstraction computed by our abstract operations for the entry of clause H_{i}:- ⋯ (i.e., A_{0} in algorithm ai in Section 3.2). Then for each new clause head H an AND-node is added as shown in Figure 3 where H:- L_{1}, …, L_{k} is the corresponding clause. After copying the abstraction of the head to the abstraction of the first body literal (A_{0} = A^{in}) the success abstraction of each literal in the clause body is computed. Then the success abstraction A^{out} of the entire clause is calculated by restricting A_{k} to the head variables (i.e., A^{out} is identical to A_{out} in algorithm ai in Section 3.2). When all success abstractions of all clauses for the predicate call P are computed, they are renamed, combined

6Recall that the call abstraction of a predicate is the abstraction given before the predicate call restricted to the argument variables of the predicate call (compare operation call-restrict in Section 3.2).

[figure: A′_{in} P′ A′_{out}; OR; AND; …  A_{in} P A_{out}  …]

Figure 4: Recursive call: P is a renaming of P′ and A_{in} restricted to call P is a renaming of A′_{in} restricted to call P′

by the least upper bound operation and then combined with the elements of abstraction A which were deleted in the call abstraction (compare algorithm ai).

2. There is an ancestor node P′ with the same predicate call and the same call abstraction (up to renaming of variables) (Figure 4): Then the success abstraction of P′ (A′_{out} without the elements already present in A′_{in}, i.e., A_{success} in algorithm ai in Section 3.2) is taken as the success abstraction of P (or ⊥ if it is not available). The combination of this success abstraction with the remaining elements of A_{in} yields A_{out} (step 3 of algorithm ai) and we proceed with the abstract interpretation procedure (i.e., we connect P to P′). If we reach the node P′ at some point during the further computation and we compute a success abstraction for P′ which differs from the old success abstraction taken for P, we recompute the success abstractions beginning at P where we take the new success abstraction of P′ as new success abstraction for P. The monotonicity property of the abstract operations and the finite domain ensures that this iteration terminates.

Bruynooghe [Bru91] has shown that this algorithm computes a superset of all concrete proof trees if the abstract operations for built-ins (here: constraints), clause entry and clause exit satisfies certain correctness conditions. We have mentioned at the beginning of Section 3 that this framework can also be applied to constraint logic programming if the notions of substitution and unification are replaced by constraints and constraint solving. Therefore theorems 4.5, 4.6 and 4.7 imply exactly the necessary correctness conditions of Bruynooghe’s framework applied to constraint logic programming. Hence we can infer the correctness of our abstract interpretation algorithm.

There is one remaining problem with our abstract interpretation algorithm. The main motivation of this paper is the characterization of a class of CLP(R) programs where all nonlinear constraints become linear during the computation. If we analyse a CLP(R) program with our algorithm, the absence of delay elements in the success abstraction of the goal does not necessarily indicate that there are no delayed nonlinear constraints at the end of the computation. Due to the definition of our concretisation function γ, this indicates that there are no delayed nonlinear constraints containing goal variables. But it does not exclude the case that there are delayed constraints with variables local to some clauses. The next theorem shows that this case cannot occur since all delayed constraints are covered by our algorithm. We need the notion of “equivalence” of variables w.r.t. a constraint to formulate this theorem. Hence we call two variables X, Y equivalent w.r.t. constraint C, denoted X∼_{C}Y, if C constrains X and Y to the same values, i.e., σ(X) = σ(Y) for all σ ∈ Sol(C).

Theorem 4.8 (Completeness of delay abstractions) Let L be a flat literal or constraint with abstraction A and A′ = ai(A, L). Let C ∈ γ(A) and C′ ∈ γ(A′) with C′ = C ∪C_{L} where C_{L} are the new constraints added to C during the execution of L. Then delay ∈ A′ or for all Z=Z_{1}*Z_{2} ∈ C_{L} with Z_{1}*Z_{2} nonlinear in C′ there exists delay(Z′_{1} or Z′_{2}) ∈ A′ with Z_{1}∼_{C′}Z′_{1} and Z_{2}∼_{C′}Z′_{2}.

Proof: We prove the theorem by induction on the depth of the concrete proof tree (AND-tree) for the literal L. Since all concrete proof trees are represented by the abstract rational AND-OR-tree computed by the abstract interpretation algorithm (cf. [Bru91]), we yield the proposition by comparing the concrete proof tree with the abstractions in the corresponding abstract tree. For the base case we consider the possible single constraints for L:

• L = X=Y, L = X=c, L = X=f(Y_{1},…,Y_{n}), L = X=Y_{1}+Y_{2}, L = X=Y_{1}-Y_{2}, or L = X⊙Y with ⊙ ∈ {<, >, <=, >=}: Since the evaluation of these constraints does not generate any new nonlinear constraints in C_{L}, the proposition is trivially true.

• L = X=Y_{1}*Y_{2}: In this case we have C_{L} = {X=Y_{1}*Y_{2}}. Since A is extended to A′ = A ∪ {{Y_{1},Y_{2}}⇒X, delay(Y_{1} or Y_{2})}, this new nonlinear constraint is obviously covered by A′.

For the induction step we assume that L = p(X_{1}, …, X_{n}) and L_{0} :- L_{1}, …, L_{k} is the clause selected for the proof of L. Then the root of the proof tree for L is marked with L and has proof trees for L_{1}, …, L_{k} as sons. The constraints C_{0} present before L_{1} is proved are C_{0} = C ∪ {L=L_{0}}. If A_{0} is the abstraction computed from A and this clause in the corresponding abstract AND-OR-tree, then C_{0} ∈ γ(A_{0}) by Theorem 4.6. Thus we can apply our induction hypothesis to the proof tree for L_{1} and we obtain that all nonlinear constraints in C_{L_{1}} (where C_{L_{1}} is the set of constraints added during execution of L_{1}) are covered by the success abstraction of L_{1}. Moreover, Theorem 4.7 ensures that the constraints after execution of L_{1} are contained in the concretisation of the corresponding abstraction. Therefore we can apply our induction hypothesis also to L_{2}, and so on. Thus a simple induction on L_{1}, L_{2}, …, L_{k} yields the following result: If A_{k} is the success abstraction of L_{k}, then delay ∈ A_{k} or for all Z=Z_{1}*Z_{2} ∈ C_{k} (where C_{k} is the set of constraints added during execution of L_{1}, L_{2}, …, L_{k}, i.e., C_{L} = {L=L_{0}}∪C_{k}) with Z_{1}*Z_{2} nonlinear in C′ there exists delay(Z′_{1} or Z′_{2}) ∈ A_{k} with Z_{1}∼_{C′}Z′_{1} and Z_{2}∼_{C′}Z′_{2}. Hence we distinguish the following cases:

1. delay ∈ A_{k}: Then delay ∈ A by definition of A in algorithm ai.

2. delay(Z′_{1} or Z′_{2}) ∈ A_{k} with Z′_{1} ∉ var(L_{0}) or Z′_{2} ∉ var(L_{0}): Then delay ∈ A by definition of A in algorithm ai.

3. delay(Z′_{1} or Z′_{2}) ∈ A_{k} with Z′_{1}, Z′_{2} ∈ var(L_{0}): Let L_{0} = p(Y_{1}, …, Y_{n}). Then Z′_{1} = Y_{i} and Z′_{2} = Y_{j} for some i, j ∈ {1, …, n}. By definition of A in algorithm ai, delay(X_{i} or X_{j}) ∈ A. Moreover, X_{i}∼_{C′}Y_{i} and X_{j}∼_{C′}Y_{j} because p(X_{1}, …, X_{n})=p(Y_{1}, …, Y_{n}) ∈ C′. Thus Z_{1}∼_{C′}X_{i} and Z_{2}∼_{C′}X_{j} since ∼_{C′} is an equivalence relation.

Altogether, the proposition is true in all cases.

Due to this theorem our abstract interpretation algorithm characterizes a class of CLP(R) programs (those containing no new delay elements in the success abstraction of the goal) for which all nonlinear constraints become linear at run time.

4.4 Example: Construction of an abstract AND-OR-tree

In the following we want to present an example which shows the construction of an abstract AND-OR-tree and the iteration over this tree by the abstract interpretation algorithm. The following flat CLP(R) program, introduced in Section 3.3, relates a list of numbers with the product of all its elements:

   prod(A, B) :- A = [],     B = 1.
   prod(A, B) :- A = [E|R],  B = E*P,  prod(R, P).

The execution of this program may generate delayed nonlinear constraints if the first argument is not a list of numbers with unique values. For instance, the answer to the goal

   ?- prod([X,Y,Z],10).

is “maybe 10=X*Y*Z”. We will show the computation of our abstract interpretation algorithm for such kind of goals. The initial goal is prod(L,Pr) with abstraction {Pr}, i.e., the abstraction indicates that the second argument is a unique value while the first argument is arbitrary. The abstract interpretation algorithm applied to this goal and abstraction generates the abstract AND-OR-tree shown in Figure 5. This tree is constructed during the computation of the abstractions A_{1}, A_{2}, A_{3} etc. It is finite since the rightmost leaf prod(S,Q) has the same call abstraction as its ancestor OR-node prod(R,P). In the following we present the results of the stepwise computations of abstractions in this tree:

Initialization:

A_{0} = {Pr}

Abstract interpretation of the first clause:

A_{1} = {B}
A_{2} = {B}
A_{3} = {A, B}
A_{4} = {A, B}
A_{5} = {A, B}

Abstract interpretation of the second clause:

    [figure: A_{0} prod(L,Pr) A_{23}; OR; A_{1} prod(A,B) A_{5}  A_{6} prod(A,B) A_{22}; AND; A_{2} A=[]  A_{3}  B=1 A_{4}; AND; A_{7} A=[E|R] A_{8} B=E*P A_{9} prod(R,P) A_{21}; OR; A_{10} prod(C,D) A_{14}  A_{15} prod(C,D) A_{20}; AND; A_{11} C=[]  A_{12}  D=1 A_{13}; AND; A_{16} C=[F|S] A_{17} D=F*Q A_{18} prod(S,Q) A_{19}]

Figure 5: AND-OR-tree for the abstract interpretation of prod(L,Pr)

A_{6} = {B}
A_{7} = {B}
A_{8} = {B, {E,R}⇒A, {A}⇒E, {A}⇒R}
A_{9} = {B, {E,R}⇒A, {A}⇒E, {A}⇒R, {E,P}⇒B, delay(E or P)}

→ {B, {E,R}⇒A, {A}⇒E, {A}⇒R, delay(E or P)}

The call abstraction part of A_{9} is ∅ which is different from A_{0}. Hence it is not a recursive call and therefore a new OR-node is generated for the call prod(R,P):

\begin{aligned}A_{10} & = & ∅ \\ A_{11} & = & ∅ \\ A_{12} & = & \{C\} \\ A_{13} & = & \{C, D\} \\ A_{14} & = & \{C, D\} \end{aligned}

Abstract interpretation of the second clause for prod(R,P):

A_{15} = ∅
A_{16} = ∅
A_{17} = {{F,S}⇒C, {C}⇒F, {C}⇒S}
A_{18} = {{F,S}⇒C, {C}⇒F, {C}⇒S, {F,Q}⇒D, delay(F or Q)}

The call abstraction part of A_{18} and A_{9} is ∅ in both cases. Hence it is a recursive call. Instead of creating a new OR-node, the success abstraction of the ancestor call (A_{21}) is taken as a first success approximation of this recursive call. This is ⊥ because the success abstraction of the ancestor is currently not available:

A_{19} = ⊥
A_{20} = ⊥
A_{21} = A_{9} ∪ {R, P}  (since A_{14} ⊔ A_{20} = {C, D})

         →^{∗} {B, R, P, {E}⇒A, {A}⇒E}

The success abstraction of the ancestor node of the recursive call becomes available at this point. Hence we recompute the recursive call with the renamed second success approximation of prod(R,P), i.e., with {S,Q}:

A_{19} = A_{18} ∪ {S, Q} = {S, Q, {F,S}⇒C, {C}⇒F, {C}⇒S, {F,Q}⇒D, delay(F or Q)}
→^{∗} {S, Q, {F}⇒C, {C}⇒F, {F}⇒D}
A_{20} = ∅
A_{21} = A_{9} ∪ ∅ = A_{9}  (since A_{14} ⊔ A_{20} = ∅)

The success abstraction of the ancestor node of the recursive call has changed. Hence we recompute the recursive call with the renamed third success approximation of prod(R,P): ∅

A_{19} = A_{18} ∪ ∅ = {{F,S}⇒C, {C}⇒F, {C}⇒S, {F,Q}⇒D, delay(F or Q)}
A_{20} = {delay}
A_{21} = A_{9} ∪ {delay}  (since A_{14} ⊔ A_{20} = {delay})
= {B, {E,R}⇒A, {A}⇒E, {A}⇒R, delay(E or P), delay}

The success abstraction of the ancestor node of the recursive call has changed again. Fourth success approximation of the recursive call prod(R,P): {delay}

A_{19} = A_{18} ∪ {delay} = {{F,S}⇒C, {C}⇒F, {C}⇒S, {F,Q}⇒D, delay(F or Q), delay}
A_{20} = {delay}
A_{21} = A_{9} ∪ {delay}  (since A_{14} ⊔ A_{20} = {delay})
= {B, {E,R}⇒A, {A}⇒E, {A}⇒R, delay(E or P), delay}

No further iteration is necessary since the success abstraction of prod(R,P) has not changed:

A_{22} = {B, delay}
A_{23} = {Pr, delay}  (since A_{5} ⊔ A_{22} = {B, delay})

The element delay in the success abstraction of the initial goal indicates that the concrete computation may stop with a delayed nonlinear constraint.

5 Extension to other delayed constraints

In Section 2 we have defined the subclass of CLP(R) programs which we can analyse by our abstract interpretation algorithm. However, CLP(R) programs may also contain the arithmetic functions /, sin, cos, pow, abs, min and max which are also delayed until particular conditions are satisfied. For instance, the constraint Z=sin(X) is delayed until X is ground while the constraint Z=abs(X) is delayed until X is ground, Z=0 or Z is ground and negative [HJM^{+}91]. Since the exact value of a ground variable is not available in our abstract domain, we can only approximate this behaviour on the abstract level. In order to analyse these new constraints we have to extend our algorithm as follows:

1. Define a new element in the abstract domain appropriate to the abstract description of the delayed constraint.

2. Extend the abstract constraint solver ai-con to the new constraint.

3. Extend the normalization rules for abstractions to describe the wakeup conditions of the delayed constraint.

In the following we demonstrate the necessary extensions by two examples.

Z=sin(X): This constraint delays until X is ground. Therefore we introduce the element delay(X) in our abstract domain and extend the definition of ai-con to:

ai-con(A, Z=sin(X)) = A ∪ {{X}⇒Z, delay(X)}

The wakeup condition for this kind of constraints is described by the following normalization rule for abstractions:

A ∪ {X, delay(X)} ⟶ A ∪ {X}

Z=min(X,Y): This constraint delays until X and Y are ground. Therefore we introduce the element delay(X and Y) in our abstract domain and extend the definition of ai-con to:

ai-con(A, Z=min(X,Y)) = A ∪ {{X,Y}⇒Z, delay(X and Y)}

The wakeup condition for this kind of constraints is described by the following normalization rule:

A ∪ {X, Y, delay(X and Y)} ⟶ A ∪ {X, Y }

All other types of delayed constraints can be handled in a similar way. Although we have not explicitly mentioned the necessary changes to exit-restrict, it is obvious how to adapt the definition of exit-restrict to the new kinds of constraints.

6 Applications

We have presented an algorithm to approximate the potential run-time occurrences of nonlinear constraints in a CLP(R) program. In this section we will outline possible applications of this algorithm.

6.1 Better user support

In CLP(R) the programmer can formulate arbitrary arithmetic constraints. However, during the computation process only linear arithmetic constraints are actively used to restrict the search space and control the computation. The programmer is responsible for writing the programs in such a way that all nonlinear constraints become linear during the computation. If this is not the case, the program may stop with a set of complex nonlinear constraints for which the satisfiability is difficult to decide. Unfortunately, it is not easy to see whether constraints become linear because this depends on the dataflow and the constraint solving in the program. Our algorithm is able to support the user in this difficult question since the algorithm can be applied in the following ways:

1. We start the algorithm with a particular goal and an initial abstraction. If the success abstraction computed for this goal contains no delay elements, then all computed answer constraints are linear, i.e., the CLP(R) constraint solver can decide the satisfiability of the final answer. Conditionally successful answers cannot occur in this case.

2. If the user is interested not only in the final answer constraints but also in constraints produced during the computation process, we start the algorithm with a goal and an abstraction and consider at the end of the abstract interpretation the call and success abstractions of all literals in the program (i.e., the entire abstract AND-OR-tree as shown in Section 4.4). Since these abstractions are valid approximations of all constraints which occur at run time, we can infer properties of intermediate constraints. For instance, if none of these abstractions contains a delay element, then the programmer can be sure that the CLP(R) constraint solver is able to decide the satisfiability of all constraints during the entire execution and therefore useless derivations with unsolvable nonlinear constraints are not explored. On the other hand, delay elements in some abstraction indicate the program points where nonlinear constraints may occur at run time. This can be a useful information for the programmer.^{7}

6.2 More efficient implementations

The knowledge about the potential presence of nonlinear constraints can be used to optimize the implementation of logic programs with arithmetic constraints. In this case it is necessary to consider the call and success abstractions of all literals rather than the success abstraction of the main goal (similarly to item 2 in Section 6.1 above). There are at least two potential optimizations:

1. If none of the abstractions contains a delay element, then nonlinear constraints cannot occur at run time. Hence the program can be compiled without the delay mechanism for nonlinear constraints [JMY91]. Moreover, general instructions for creating nonlinear constraints can be specialized to simpler instructions for creating linear constraints [JMSY92a].

2. The RISC-CLP(Real) system [Hon92] allows the formulation of nonlinear arithmetic constraints which are not delayed but checked by a powerful constraint solver. But this constraint solver is very complex and therefore sometimes too inefficient for solving simple linear constraints. Our algorithm can be used to optimize the RISC-CLP(Real) system since our algorithm determines the program points where nonlinear constraints may occur and where all constraints are definitively linear. Hence we can call a more efficient linear constraint solver for the latter program points without restricting the computational power of the RISC-CLP(Real) system.

7For such an application it may be necessary to change the definition of call-restrict so that delay elements are passed into the applied clause. Then the potential presence of nonlinear constraints can be immediately seen by considering the local abstraction without including the abstractions of ancestor nodes in the tree.

6.3 Improving the termination behaviour

One of the principles of constraint logic programming is the satisfiability check during computation: a derivation proceeds only if all accumulated constraints are solvable [JL87]. This allows an early failure detection and avoids infinite derivation paths which may be present in pure logic programming. However, in CLP(R) this advantage is sometimes lost since nonlinear constraints are not checked for satisfiability. For instance, consider the following CLP(R) program for computing factorial numbers:

   fac(0,1).
   fac(N,N*F) :- N >= 1,  fac(N-1,F).

To compute a factorial we start with the goal ?-fac(8,F) and obtain the answer constraint F=40320. If we want to know whether a given number is a factorial, we try to prove a goal like ?-fac(N,24). In this case CLP(R) computes the answer constraint N=4 after some backtracking steps. Although nonlinear constraints are generated during this computation, they become linear if the first clause is used and binds the unknown first argument. But if we try to prove a (unsolvable) goal like ?-fac(N,10), CLP(R) runs into an infinite loop by applying the second clause again and again. The accumulated nonlinear constraints are not solvable but this is not detected by CLP(R) due to the delay mechanism. If we use a more powerful constraint solver which is able to treat nonlinear constraints (like in CAL [ASS^{+}88] or RISC-CLP(Real) [Hon92]), this infinite loop can be avoided.

We can use our abstract interpretation algorithm to find such sources of nontermination. For this purpose we compute the call abstraction of each literal in the program. If the abstraction of a recursive call contains a delay element, we may do the following:

1. We warn the user that there may be delayed nonlinear constraints before the recursive call which can cause an infinite loop if these constraints are not solvable.

2. We use a powerful constraint solver for nonlinear constraints before the recursive call at run time in order to avoid the described source of nontermination. This seems to be a good compromise between the efficiency of the CLP(R) system and the power of the RISC-CLP(Real) system.

If a solver for nonlinear constraints is integrated in the system, it should also be used at the end of a computation whenever the success abstraction of the initial goal contains delay elements.

7 Conclusions and related work

We have presented a method for the analysis of nonlinear constraints occurring at run time in the execution of a CLP(R) program. Since an exact analysis is impossible at compile time, we have used an abstract interpretation algorithm to approximate the possible delayed nonlinear constraints and the variable dependencies occurring at run time. The application of this algorithm to various examples shows that our algorithm has enough precision for practical programs. The information produced by this algorithm can be used to support the programmer when using the delay mechanism of the CLP(R) system or to optimize the program when using a more powerful constraint solver like RISC-CLP(Real).

We have developed our analysis algorithm on the basis of a given framework for the abstract interpretation of logic programs [Bru91] since the operational semantics of CLP(R) is very similar to logic programming. The only difference is the use of sets of constraints instead of substitutions. Therefore any other framework may also be applicable. Marriott and Søndergaard [MS90] have developed a particular framework for the abstract interpretation of constraint logic programming languages based on a denotational description of the semantics. They have also shown the application of their framework to the freeness and groundness analysis of CLP programs. However, they have not applied their method to a particular domain of constraints. Therefore they have not precisely described a solution to one of the main difficulties in a concrete application: the abstraction of the freeness or uniqueness of a variable w.r.t. a given concrete set of constraints. This is one of the main points addressed in this paper. We have derived uniqueness information w.r.t. arithmetic constraints over the real numbers by considering the variable dependencies caused by constraints. The normalization rules for our abstract domain corresponds to constraint solving in the concrete domain.

Most of the well-known abstract interpretation algorithms for the derivation of groundness information of variables or mode information for predicates in logic programs use a small number of abstract values like ground, free or any (see, for instance, [Mel85, Nil88, Bru91] or [JMM91] for the case of CLP(R)). Such a domain yields quite good results for many practical logic programs. But for constraint logic programming it must be refined since the possible reasons for the groundness of variables are much more complicated. For instance, the arithmetic constraint X=Y+Z implies the groundness of Y if X and Z are ground but not the groundness of Y and Z if X is ground. A typical programming methodology in constraint logic programming is “test and generate” [JMSY92b, VH89] where variables are instantiated by generators after the creation of a network of constraints between these variables. The following simple digital circuit program uses this technique (recall that we assume a left-to-right strategy for the evaluation of subgoals):

   p(X,Y,Z) :- not(X,NX), and(NX,Y,NXY), not(Z,NZ), and(NXY,NZ,1), % test
               bit(X), bit(Y), bit(Z).                             % generate
   not(A,NA) :- NA = 1-A.
   and(A,B,AB) :- AB = A*B.
   bit(0).
   bit(1).

The unique answer constraint to the goal ?-p(X,Y,Z) is X=0,Y=1,Z=0, i.e., there are no delayed nonlinear constraints in the answer. However, a simple mode analysis as in [JMM91] would infer that the predicate and is called with free variables in the first and second argument position and hence there may be a delayed nonlinear constraint at run time. In order to improve the accuracy of the analysis, we have used implications of the form V ⇒X to describe dependencies between different variables. For the last example our algorithm infer the dependencies {X}⇒NX, {NX,Y}⇒NXY and {Z}⇒NZ (among others). Since the variables X, Y and Z are bound to ground terms by the last bit-literals in the first clause, our algorithm infers (using the variable dependencies) that there are no delayed nonlinear constraints in the answer. This example shows that our algorithm has a better precision than other algorithms for groundness analysis which is due to the fact that grounding variables by constraint solving and awakening delayed constraints can be easily described on the abstract level with our abstract domain.

Marriott and Søndergaard have also proposed an abstract domain P rop for a more precise analysis of groundness information [MSD90, CFW91]. Their domain contains propositional formulas over the program variables and the logical connectives ∨, ∧ and ↔. Such a domain is appropriate for pure logic programming since the groundness information after a unification like X=f(Y,Z) can be expressed by the propositional formula X ↔ Y∧Z meaning that the groundness of X is equivalent to the groundness of Y and Z. But in constraint logic languages the instantiation of variables can have different reasons as shown above by the constraint X=Y+Z. These different possibilities can be easily expressed in our abstract domain of variable dependencies.

Our abstract domain has some similarities to the abstract domain used for the analysis of residuating logic programs [Han92]. This is due to the fact that the analysis of variable dependencies is also essential for a precise analysis of residuating logic programs. However, the meaning of abstractions is quite different in both approaches. In case of residuating logic programs the concrete domain consists of substitutions and residuated equations and therefore substitutions must be interpreted w.r.t. the current set of residuated equations. In our case abstractions have a more direct meaning in the concrete domain and therefore the concretisation function and the correctness proofs are simpler. Further essential differences show up in the definition of abstract unification which is more sophisticated in the case of constraint logic programs.

Recently, García de la Banda and Hermenegildo [GdlBH92] have independently developed a framework for the analysis of constraint logic programs by extending Bruynooghe’s framework. Although they were mainly interested in the derivation of groundness information and did not include information about nonlinear constraints in their abstract domain, the abstract representation of variable dependencies is very similar to our approach. They also associate to each variable sets of variables which uniquely determine the value of that variable. However, they have given a direct definition of abstract constraint solving which results in more complicated definitions than our approach using normalization rules to simplify abstractions after abstract constraint solving.

Although our algorithm yields quite good results for practical programs, the precision of the uniqueness analysis can be improved in various ways. For instance, we do not consider the free variables in constraints and thus we do not detect the uniqueness of these variables in some cases. E.g., the constraint 3=5*X-2*X restricts variable X to the unique value 1. But our analysis algorithm does not infer that X is unique since the information that both subexpressions contain the same free variable is not present in the corresponding abstraction. Hence the analysis can be improved if the abstract domain is refined to store information about variables in expressions. Another possibility for improving the precision of the analysis is to derive information about possible values of variables. This would allow to detect that the constraints X=3,6=X*Y restricts Y to a unique value or that the constraints X>2,Z=1,X<Z are unsolvable.

Acknowledgements. The author is grateful to Peter Barth and Frank Zartmann for discussions and their careful reading of this paper.

References

[AH87] S. Abramsky and C. Hankin, editors. Abstract Interpretation of Declarative Languages. Ellis Horwood, 1987.

[ASS^{+}88] A. Aiba, K. Sakai, Y. Sato, D.J. Hawley, and R. Hasegawa. Constraint Logic Programming Language CAL. In Proc. Int. Conf. on Fifth Generation Computer Systems, pp. 263–276, 1988.

[Bru91] M. Bruynooghe. A Practical Framework for the Abstract Interpretation of Logic Programs. Journal of Logic Programming (10), pp. 91–124, 1991.

[CC77] P. Cousot and R. Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction of approximation of fixpoints. In Proc. of the 4th ACM Symposium on Principles of Programming Languages, pp. 238–252, 1977.

[CFW91] A. Cortesi, G. File, and W. Winsborough. Prop revisited: Propositional Formula as Abstract Domain for Groundness Analysis. In Proc. IEEE Symposium on Logic in Computer Science, pp. 322–327, 1991.

[Col90] A. Colmerauer. An Introduction to Prolog III. Communications of the ACM, Vol. 33, No. 7, pp. 69–90, 1990.

[Deb89] S.K. Debray. Static Inference of Modes and Data Dependencies in Logic Programs. ACM Transactions on Programming Languages and Systems, Vol. 11, No. 3, pp. 418– 450, 1989.

[GdlBH92] M.J. García de la Banda and M. Hermenegildo. A Practical Approach to the Global Analysis of Constraint Logic Programs. Technical Report, Universidad Politecnica de Madrid, 1992.

[Han91] M. Hanus. Parametric Order-Sorted Types in Logic Programming. In Proc. of the TAPSOFT ’91, pp. 181–200. Springer LNCS 494, 1991.

[Han92] M. Hanus. On the Completeness of Residuation. In Proc. of the 1992 Joint International Conference and Symposium on Logic Programming, pp. 192–206. MIT Press, 1992.

[HJM^{+}91] N. Heintze, J. Jaffar, S. Michaylov, P. Stuckey, and R. Yap. The CLP(R) Programmer’s Manual, Version 1.1. IBM Thomas J. Watson Research Center, Yorktown Heights, 1991.

[Hon92] H. Hong. Non-linear Real Constraints in Constraint Logic Programming. In Proc. of the 3rd International Conference on Algebraic and Logic Programming, pp. 201–212. Springer LNCS 632, 1992.

[JL87] J. Jaffar and J.-L. Lassez. Constraint Logic Programming. In Proc. of the 14th ACM Symposium on Principles of Programming Languages, pp. 111–119, Munich, 1987.

[JMM91] N. Jørgensen, K. Marriott, and S. Michaylov. Some Global Compile-Time Optimizations for CLP(R). In Proc. 1991 International Logic Programming Symposium, pp. 420–434. MIT Press, 1991.

[JMSY92a] J. Jaffar, S. Michaylov, P.J. Stuckey, and R.H.C. Yap. An Abstract Machine for CLP(R). In Proc. SIGPLAN Conference on Programming Language Design and Implementation, pp. 128–139. SIGPLAN Notices, Vol. 27, No. 7, 1992.

[JMSY92b] J. Jaffar, S. Michaylov, P.J. Stuckey, and R.H.C. Yap. The CLP(R) Language and System. ACM Transactions on Programming Languages and Systems, Vol. 14, No. 3, pp. 339–395, 1992.

[JMY91] J. Jaffar, S. Michaylov, and R.H.C. Yap. A Methodology for Managing Hard Constraints in CLP Systems. In Proc. ACM SIGPLAN’91 Conference on Programming Language Design and Implementation, pp. 306–316. SIGPLAN Notices, Vol. 26, No. 6, 1991.

[LCMVH91] B. Le Charlier, K. Musumbu, and P. Van Hentenryck. A Generic Abstract Interpretation Algorithm and its Complexity Analysis. In Proc. International Conference on Logic Programming, pp. 64–78. MIT Press, 1991.

[Mel85] C.S. Mellish. Some Global Optimizations for a Prolog Compiler. Journal of Logic Programming (1), pp. 43–66, 1985.

[MS90] K. Marriott and H. Søndergaard. Analysis of Constraint Logic Programs. In Proc. of the 1990 North American Conference on Logic Programming, pp. 531–547. MIT Press, 1990.

[MSD90] K. Marriott, H. Søndergaard, and P. Dart. A Characterization of Non-Floundering Logic Programs. In Proc. of the 1990 North American Conference on Logic Programming, pp. 661–680. MIT Press, 1990.

[Nil88] U. Nilsson. Towards a Framework for the Abstract Interpretation of Logic Programs. In Proc. of the Workshop on Programming Language Implementation and Logic Programming, pp. 68–82, Orléans, 1988. Springer LNCS 348.

[Nil90] U. Nilsson. Systematic Semantic Approximations of Logic Programs. In Proc. of the 2nd Int. Workshop on Programming Language Implementation and Logic Programming, pp. 293–306. Springer LNCS 456, 1990.

[Pfe92] F. Pfenning, editor. Types in Logic Programming. MIT Press, 1992.

[VH89] P. Van Hentenryck. Constraint Satisfaction in Logic Programming. MIT Press, 1989.