A Generic Algorithm for CLP Analysis^{∗}

(Extended Abstract)

Nevin Heintze^{†} and Joxan Jaffar^{‡}

June 13, 1995

Logic program analyzers typically employ abstract interpretation and consist of two main components: an abstract domain and a generic iterative fixed-point computation or “engine”. In earlier work, we presented a new engine based on an unfolding operation, and showed that it was uniformly more accurate than the standard engine. This unfolding engine however had a crucial limitation: it could not be generalized to constraint logic programming (CLP).

In this paper, we develop a fundamentally different view of unfolding, based on a uniform treatment of constraints. The result is a family of analysis algorithms which is modular in the sense that CLP is modular over computation domains. Not only is the new engine more general, but it is also simpler and more flexible. In particular, it provides new opportunities for tuning efficiency/accuracy tradeoffs. At one end of the spectrum, the engine can be used to describe the standard engine; at the other end is an algorithm that is more accurate than the old unfolding engine for traditional logic programs. The main technical result however is that the new engine is uniformly more accurate than a comparable abstract interpretation algorithm for CLP, whatever the constraint and abstract domains used.

Keywords: (constraint) logic programming, program analysis, abstract interpretation

∗This length of the body of this manuscript is 5034 words (according to delatex and wc).

† School of Computer Science, Carnegie Mellon University, Pittsburgh, PA 15213; nch@cs.cmu.edu ‡ IBM T.J. Watson Research Center, PO Box 704, Yorktown Heights, NY 10598; joxan@watson.ibm.com

1 Introduction

Most algorithms for logic program (LP) analysis are based on abstract interpretation, and consist of two components: an abstract domain (and associated functions) and an iterative fixed-point computation. Substantive differences between algorithms typically appear in the abstract domain, and design of this component that is the main focus of algorithm development (in fact it is the choice of this component that largely determines both the accuracy and cost of the analysis). In contrast, differences in the fixed-point components are relatively minor, and it is possible to speak of an idealized generic algorithm or “engine” that encompasses the essence of the fixed-point computation. Some specific descriptions of engines are [9], for logic programs, and more recently, [10], for constraint logic programs.

In earlier work [6], a new engine, called the unfolding engine, was presented for the analysis of logic programs. Its main advantage was improved accuracy over the standard engine, regardless of the abstract domain used. A fundamental difference between the unfolding and standard engines is that the standard engine iterates over a fixed collection of semantic equations, whereas the unfolding engine iterates over dynamically changing equations. Roughly speaking, the unfolding engine combines set constraint techniques [4, 5, 3] with abstract interpretation techniques [1]. The former provides a superior ability to reason about term structures, but ignores all dependencies between variables; the latter provides an ability to reason about dependencies. Unfortunately, the unfolding engine relies directly on a specialized representation using substitutions, which cannot be lifted to constraint logic programming (CLP). This is a pity since analysis for CLP is arguably more important than for LP – the opportunities for compiler optimizations are considerably greater (see eg. [11]).

This paper presents an unfolding engine for CLP. The main technical difference from the previous engine is a novel use of input/output variables in the constraints, as opposed to the manipulation of substitutions. What results is not just a more general engine, but a far simpler and more accurate one. Specifically:

• It provides an elegant, generic algorithm based on the well-understood primitive operation of unfolding.

• It is provides new opportunities for tuning efficiency/accuracy tradeoffs. Not only can one consider modifying the abstract domain, but various aspects of the engine itself can be controlled. At one end of the spectrum, the engine can be used to describe the standard engine; at the other end is an algorithm that provides significantly richer information that in general cannot be computed using the standard engine (no matter what abstract domain is used).

• In the special case of traditional logic programs, it is simpler, more efficient and uniformly more accurate than the old engine.

• It is uniformly more accurate than the standard engine for CLP, whatever abstract and constraint domains are used. This in fact represents the main technical result of this paper.

We next illustrate some differences between a standard abstract interpretation algorithm, and the old and new engines. Consider the abstract domain LSign [11, 12] which abstracts the coefficients in linear arithmetic expressions by their sign. Thus for example, 3X − 4Y = 5 is described by the LSign formula ⊕X ⊖ Y = ⊕ where ⊕ denotes some positive number, and ⊖ some negative number.

    ?- p(X,Y), q(X).
    p(A,B) :- A - 2*B = 3.
    q(A) :- A = 5.

                               ?- p(f(Y,3)).
                               p(U) :- q(U).
                               q(f(2+2,V)).

                                                  ?- p(X), r(X,Y).
                                                  p(U) :- q(U).
                                                  q(f(A,B)) :- A - 2*B = 3.
                                                  r(f(A,B),B) :- A + 2*B = 7.

For the first CLP(R) [7] program, the standard algorithm using this domain would be able to infer that Y is ground (because it can combine the formula ⊕X ⊖ Y = ⊕ obtained from the first rule with the formula ⊕X = ⊕ obtained from the second rule). It cannot however infer the same for Y in the second program, which requires a completely different kind of reasoning, that over partially instantiated term structures. Here a set constraint approach would have been useful, if only it could handle arithmetic expressions and constraints. The third program serves as a combination of the first two, and exemplifies where the new engine, which will infer the exact value for Y, retains the power of all previous engines, and more.

2 Preliminary Definitions

Let V, Σ, Π_{p} and Π_{c} be countably infinite collections of variables, function symbols, program predicates and constraint predicates respectively. Each function and predicate symbol has a given arity. A term is either a variable or of the form f(t_{1}, …, t_{n}) where f ∈ Σ has arity n and the t_{i} are terms. An atom is of the form p(t_{1}, …, t_{n}) where p ∈ Π_{p} has arity n ≥ 0 and each t_{i} is a term. An atomic constraint is an expression of the form p(t_{1}, …, t_{n}) where p ∈ Π_{c} has arity n ≥ 0 and each t_{i} is a term. A program is a collection of rules of the form H ← B_{1}, …, B_{m}, where m ≥ 0, H is an atom, and each B_{i} is either an atom or an atomic constraint. We refer to H as the head of the rule, and to the sequence B_{1}, …, B_{m} as the body of the rule.

A constraint is either an atomic constraint or of one of the forms (∃X)(c) or c_{1} ∧ ⋯ ∧ c_{n} where c, c_{1}, …, c_{n} are constraints, and X is a program variable. Bound and free occurrences of variables in a constraint are defined in the usual manner. Let var(e) denote the set of free variables in the expression e. Then if S = {X_{1}, …, X_{n}} is a set of variables, we write (∃_{S})(c) to denote (∃X_{1}) ⋯ (∃X_{n})(c), and we write (∃\overline{S})(c) to denote (∃_{T})(c) where T = var(c) − S.

A substitution θ is a mapping from variables into terms. Where e is some expression, eθ denotes the simultaneous replacement of each free occurrence of a variable X in e by Xθ (bound variables are appropriately renamed to avoid “variable capture”, so that if θ maps X into Y, then (∃Y)(X = f(Y)) is mapped to (∃Y′)(Y = f(Y′)) under θ). A renaming substitution θ is an injection from V into V; we say that θ renames away from an expression e if the range of θ is disjoint from var(e).

The meaning of constraints is given by a structure J that defines the underlying domain of computation, X, assigns a meaning J (f) : X^{n} → X to each n-ary function symbol in f ∈ Σ, and assigns a meaning J (p) : X^{n} → {true, false} to each n-ary constraint predicate in p ∈ Π_{c}. X is also referred to as the constraint domain of the CLP language. Given a valuation ρ, which maps variables into X, and given a structure J, the meanings of terms and constraints are defined in the obvious inductive manner. If for some valuation ρ, the meaning of a constraint c is true, then we say that c is satisfiable.

We define a bottom-up operational semantics of a program P as follows. An atom A succeeds with answer constraint c from P if c is satisfiable and there exists some rule H ← B_{1}, …, B_{n} in P such that c is (∃\overline{var(A)})(A = Hθ ∧ c_{1}θ ∧ ⋯ ∧ c_{n}θ) where θ renames away from A, and for each 1 ≤ i ≤ n, either B_{i} is an atom that succeeds with answer constraint c_{i}, or else B_{i} is the atomic constraint c_{i}. Note that the free variables in the answer constraint c are exactly the variables in A.

A central concept from abstract interpretation of CLP is the notion of an abstract domain for representing constraints.

Definition 1 An abstract domain is a set of abstract formulas together with (a) an abstraction function abs which takes a set of constraints and returns an abstract formula, and (b) a concretization function conc which takes an abstract formula and returns a set of constraints satisfying conc(abs(C)) ⊇ C for constraint sets C. (Typically, some further algebraic conditions are specified, but these will not concern us here.)

Using such domains, the Appendix presents an idealized abstract interpretation engine for CLP that encompasses the essence of the iterative fixed-point algorithms used in the literature.

3 Semantic Equations

We now give an equational formulation of the bottom-up semantics defined in the previous section. Whereas the previous definition of the operational semantics focuses on answer constraints generated for a specific atom, the following equational definition focuses on the constraints generated from the body of a rule. To this end, let the rules of program P be R_{1}, …, R_{N}, and let H_{i} denote the head of the rule R_{i}. Now, for each 1 ≤ i ≤ N, let c denote the conjunction of the atomic constraints appearing in the body of R_{i}, let A_{1}, …, A_{m} denote the subsequence of atoms appearing in the body of R_{i}, and construct the equation

Ψ_{i} = ⋃_{j_{1},...,j_{m}}\{c ∧ ( \begin{matrix}∃_{S_{1}} (B_{1} = H_{j_{1}}θ ∧ c_{1}θ) \\ ∧ ⋯ ∧ \\ ∃_{S_{n}} (B_{m} = H_{j_{m}}θ ∧ c_{m}θ) \end{matrix}) : c_{1} ∈ Ψ_{j_{1}}, …, c_{m} ∈ Ψ_{j_{m}} \}

where j_{1}, …, j_{m} ranges over m − tuples such that H_{j_{1}}, …, H_{j_{m}} (after being suitably renamed) unifies with B_{1}, …, B_{m}, and θ renames away from B_{1}, …, B_{m}. This formulation of semantic equations represents, for each rule R_{i}, the set of collected constraints on the variables of R_{i} obtained from executing the body of R_{i}. Intuitively, a semantic equation Ψ_{i} = ⋯ provides a definition for the variables in the rule R_{i}. A solution of such equations is a mapping I from each Ψ_{i} into a set of constraints whose free variables are from var(R_{i}), such that each equation is satisfied^{1}. For example, consider the CLP(R) program:

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

After introducing variables Ψ_{1}, Ψ_{2} and Ψ_{3} corresponding to rules 1, 2 and 3 respectively, we have the semantic equations

Ψ_{1} = {true}

Ψ_{2} = {true}

Ψ_{3} = \begin{matrix}\{(N > 1) ∧ (F = N ∗ F 1) ∧ (fac(N − 1, F 1) = fac(0, 1)) ∧ cθ : c ∈ Ψ_{1}\} & ⋃ \\ \{(N > 1) ∧ (F = N ∗ F 1) ∧ (fac(N − 1, F 1) = fac(1, 1)) ∧ cθ : c ∈ Ψ_{2}\} & ⋃ \\ \{(N > 1) ∧ (F = N ∗ F 1) ∧ ∃N′∃F′ (fac(N − 1, F 1) = fac(N′, F′) ∧ cθ) : c ∈ Ψ_{3}\} \end{matrix}

where true denotes the empty conjunction of constraints, and the new variables N′ and S′ are renamings of N and S by θ. The following is a solution of these constraints:

Ψ_{1} = {true}
Ψ_{2} = {true} Ψ_{3} = \{( \begin{matrix}N = 2 \\ F = 2 \\ F 1 = 1 \end{matrix} ) , ( \begin{matrix}N = 3 \\ F = 6 \\ F 1 = 2 \end{matrix} ) , ( \begin{matrix}N = 4 \\ F = 24 \\ F 1 = 6 \end{matrix} ) , …\}

This is in fact the least such solution (solutions are ordered component-wise: I_{1} ≤ I_{2} iff I_{1}(Ψ_{i}) ⊆ I_{2}(Ψ_{i}) for each Ψ_{i}), and it coincides exactly with the program’s meaning. That is, Ψ_{i} consists of just the answer constraints obtained when the body of the i^{th} rule is executed as a goal. We conclude this section with a formal statement connecting the original operational semantics with the equational formulation.

Proposition 1 Let SE_{P} be the semantic equations for a program P, and let I be the least model of SE_{P}. Then, an atom A succeeds with answer constraint c iff, for some i, there is a constraint c_{i} ∈ I(Ψ_{i}) such that c is (∃\overline{var(A)}(A = H_{i}θ ∧ c_{i}θ)) where θ renames away from A.

4 Unfolding Semantic Equations

At the heart of our algorithm is the notion of unfolding semantic equations by substituting one semantic equation into another. In essence, the individual expressions in semantic equations define fragments of constraints, which are then combined to give the semantics of the entire program. To see this, recall that each semantic equation has the form Ψ_{i} = exp_{1} ∪ ⋯ ∪ exp_{r} where each exp_{l} has the form

1We tacitly identify constraints that are semantically equivalent (i.e. are satisfied by the same valuations). This issue is discussed in section 6.

\{c ∧ ( \begin{matrix}∃\overline{var(B_{1})} (B_{1} = H_{j_{1}}θ ∧ c_{1}θ) \\ ∧ ⋯ ∧ \\ ∃\overline{var(B_{m})} (B_{m} = H_{j_{m}}θ ∧ c_{m}θ) \end{matrix}) : c_{1} ∈ Ψ_{j_{1}}, …, c_{m} ∈ Ψ_{j_{m}} \} (4.1)

Now, consider the expressions of the form

∃\overline{var(B_{k})} (B_{k} = H_{j_{k}}θ ∧ c_{k}θ), 1 ≤ k ≤ m (4.2)

appearing in each exp_{l}. Recall that Ψ_{i} is interpreted as a set of constraints whose free variables are from var(R_{i}). Hence c_{k} is a constraint whose free variables are from var(R_{j_{k}}). Moreover, all of the free variables in H_{j_{k}}θ and c_{k}θ will be bound by ∃\overline{var(B_{k})}. One can therefore view (4.2) as a function that maps a constraint c_{k} with free variables from var(R_{j_{k}}) into a constraint with free variables from var(R_{i}).

The central component of this function is the pair of terms B_{k} and H_{j_{k}}, since these two terms completely determine the connection between the variables in var(R_{i}) and var(R_{j_{k}}). In effect H_{j_{k}} matches with the variables in c_{k}, and the “constraint fragment” B_{k} = H_{j_{k}} can be thought of as mapping c_{k} into a constraint on var(R_{i}). Intuitively, we would like to write B_{k} = H_{j_{k}} as a constraint and consider conjoining it with c_{k}, but we cannot do so because the variables in H_{j_{k}} must be renamed (θ appears in (4.1) for precisely this reason). At a conceptual level, we can avoid this issue by viewing the variables B_{k} and H_{j_{k}} as coming from two disjoint name spaces – that is, view the variables in B_{k} as “output” variables and those in H_{j_{k}} as “input” variables.

To formalize this, consider augmenting the universe of variables V by two parallel universes : the input variables V↑ and the output variables V↓. Both V↑ and V↓ are assumed to be countably infinite and disjoint from each other and from V. We shall view these new sets of variables as “copies” (or renamings) of V. For each variable X ∈ V, let X^{↑} and X^{↓} denote the corresponding variables in V↑ and V↓. Define a distinguished substitution ↑ as follows: (X^{↓})↑ = X, (X)↑ = X^{↑}, (X^{↑})↑ = X^{↑}. In other words, ↑ is a “shift up” operation that maps V^{↓} into V, and maps V into V^{↑}, and is the identity on V^{↑}. Similarly, we have a distinguished substitution ↓ as follows: (X^{↑})↓ = X, (X)↓ = X^{↓}, (X^{↓})↓ = X^{↓}.

Using these definitions, we can write the constraint B_{k}↑ = H_{j_{k}}↓ to represent the connection between B_{k} and H_{j_{k}}. That is, B_{k} is written using output variables, and H_{j_{k}} uses input variables. Note that B_{k}↑ = H_{j_{k}}↓ can be treated as a standard constraint (for example, we can apply usual constraint simplification procedures to it). Formulas of the form (4.1) can now be written concisely as

( \begin{matrix}[c↑] & ⋆ \\ [B_{1}↑ = H_{j_{1}}↓] & j_{1} \\ ⋯ \\ [B_{m}↑ = H_{j_{m}}↓] & j_{m} \end{matrix} )

We call such expressions clusters. In general, a cluster has the following form^{2}

2If c_{0} is the empty conjunction true, then we sometimes omit it.

( \begin{matrix}[c_{0}]_{⋆} \\ [c_{1}]_{j_{1}} \\ ⋯ \\ [c_{n}]_{j_{n}} \end{matrix} ) (4.3)

where each c_{k}, 0 ≤ k ≤ n, is a constraint, subject to the following invariant: if the cluster appears on the right hand side of the equation for Ψ_{i}, then

• the free variables in c_{0} are from R_{i}↑, and

• the free variables in each c_{k}, k ≥ 1, are from R_{i}↑ and R_{j_{k}}↓.

Each expression [c_{k}]_{j_{k}} is called a group, and j_{k} is called the dependency of the group (indicating which Ψ_{i} variable the group depends on). The group [c_{0}]_{⋆} is said to be a terminal group since it does not depend on any Ψ_{i}. Given a function I that maps from each Ψ_{i} to a set of constraints whose free variables are from var(R_{i}), the cluster (4.3) is interpreted as the following collection of constraints:

\{( \begin{matrix}c_{0} ∧ \\ (∃_{S_{1}})(c_{1}↑ ∧ c′_{1}) \\ ∧ ⋯ ∧ \\ (∃_{S_{n}})(c_{n}↑ ∧ c′_{n}) \end{matrix})↓ : c′_{1} ∈ I(Ψ_{j_{1}}), …, c′_{n} ∈ I(Ψ_{j_{n}})\}

where each S_{k} is var(R_{j_{k}}). To explain this definition, suppose that this cluster appears on the right hand side of the equation for Ψ_{i}. Then each c_{k}, k ≥ 1, is a constraint whose free variables are either input variables from var(R_{j_{k}}↓) or output variables from var(R_{i}↑), and each c′_{k} will be a constraint whose free variables come from var(R_{j_{k}}). Hence, in (c_{k}↑ ∧ c′_{k}), the input variables of c_{k} are mapped to the variables var(R_{j_{k}}), matching up with those in c′_{k}. The output variables in c_{k} are unaffected by the ↑ operation. So, each expression (∃_{S_{k}})(c_{k}↑ ∧ c′_{k}) denotes a constraint whose free variables are from var(R_{i}↑). Finally, a ↓ operation is applied to the conjunction of c_{0} and these n constraints, and the result is a constraint whose free variables are from var(R_{i}).

For example, when writing the equations for the factorial program in this new format (and doing some obvious constraint simplification), we obtain:

Ψ_{1} = ()
Ψ_{2} = ()

Ψ_{3} = ([false]_{1}) ⋃ ([ \begin{matrix}N^{↑} = 2 \\ F^{↑} = 2 \\ F 1^{↑} = 1 \end{matrix} ]_{2}) ⋃ ([ \begin{matrix}N^{↑} > 1 \\ F^{↑} = N^{↑} ∗ F 1^{↑} \\ N^{↑} − 1 = N^{↓} \\ F 1^{↑} = F^{↓} \end{matrix} ]_{3})

Consider below another example program and its semantic equations, illustrating constraints and clusters of more than one group.

   1.   p(X, Y, Z) :- X - Y = 1,
                      q(X, Y),
                      r(Z).
   2.   q(U, V) :- U + V = 3.
   3.   r(42).

Ψ_{1} = ( \begin{matrix}[X^{↑} − Y^{↑} = 1]_{⋆} \\ [ \begin{matrix}X^{↑} = U^{↓} \\ Y^{↑} = V^{↓} \end{matrix} ] & 2 \\ [Z^{↑} = 42] & 3 \end{matrix} ) Ψ_{2} = ([U^{↑} + V^{↑} = 3]_{⋆}) Ψ_{3} = ()

Note that the semantic equations we have defined correspond to a bottom-up execution of the program P at hand. We can also define semantic equations corresponding to a top-down execution of P. In what follows, the term semantic equations shall mean either the equations corresponding to bottom-up or top-down program execution. Our engine can be applied in either case.

We now describe the basic step of our engine: the unfolding of semantic equations. Consider a cluster containing only groups with null dependencies. Such a cluster has a fixed interpretation (it does not depend on the assignment to any Ψ_{i} variable). Call such clusters G terminal. For example, for the semantic equations corresponding to the program above, the clusters appearing in the equations for Ψ_{2} and Ψ_{3} are both terminal. Now, let C_{1}, C_{2} and C_{3} denote the clusters on the right hand sides of the equations for Ψ_{1}, Ψ_{2} and Ψ_{3} respectively, and consider substituting the terminal cluster C_{2} into the first group of C_{1} (since this group depends on Ψ_{2}). The resulting cluster (after some constraint simplification) is

( \begin{matrix}[X^{↑} − Y^{↑} = 1]_{⋆} \\ [X^{↑} + Y^{↑} = 3]_{⋆} \\ [Z^{↑} = 42]_{3} \end{matrix} )

which can be further simplified into ([X^{↑} = 2∧Y^{↑} = 1]_{⋆} [Z^{↑} = 42]_{3}). Call this resulting cluster C_{4}. Since C_{4} is just a more “explicit” version of information already present in the semantic equations, we can add it to the equation Ψ_{1} to obtain

Ψ_{1} = ( \begin{matrix}[X^{↑} − Y^{↑} = 1]_{⋆} \\ [ \begin{matrix}X^{↑} = U^{↓} \\ Y^{↑} = Y^{↓} \end{matrix} ] & 2 \\ [Z^{↑} = 42] & 3 \end{matrix} ) ⋃ ( \begin{matrix}[ \begin{matrix}X^{↑} = 2 \\ Y^{↑} = 1 \end{matrix} ] & ⋆ \\ [Z^{↑} = 42] & 3 \end{matrix} )

and still preserve the meaning of the constraints. We could similarly substitute C_{3} into the resulting C_{4} to obtain the new cluster ([X^{↑} = 2 ∧ Y^{↑} = 1 ∧ Z^{↑} = 42]_{⋆}), which could again be added to the equation for Ψ_{1}. Note that this last cluster is a terminal cluster: in principal it could therefore be used to substitute into clusters that depend on Ψ_{1} (although there are no such clusters in this example).

In summary, the unfolding step operates on (a) a cluster that contains an occurrence of a group with dependency i (hence the meaning of the cluster depends on the value of Ψ_{i}) and (b) a terminal cluster that appears in the right hand side of the equation for Ψ_{i}. The unfolding step substitutes the terminal cluster for Ψ_{i} in the group with dependency i. This results in a new cluster, which is added to the semantic equations. The effect of the unfolding is to collect and combine constraint fragments from various parts of the program in a way that makes information in the semantic equations more explicit. That is, after an unfolding step, more of the least solution of the semantic equations is represented in terminal clusters.

Intuitively, if we could exhaustively apply this unfolding step, then eventually all the information about the least solution would be “explicit” in the terminal clusters (in fact we could delete all non-terminal clusters without changing the least solution). However, unfolding may not terminate. For example, consider the semantic equations for the factorial program. Here unfolding produces the following sequence of terminal groups:

([ \begin{matrix}N^{↑} = 2 \\ F^{↑} = 2 \\ F 1^{↑} = 1 \end{matrix} ]_{⋆}), ([ \begin{matrix}N^{↑} = 3 \\ F^{↑} = 6 \\ F 1^{↑} = 2 \end{matrix} ]_{⋆}), ([ \begin{matrix}N^{↑} = 4 \\ F^{↑} = 24 \\ F 1^{↑} = 6 \end{matrix} ]_{⋆}), ([ \begin{matrix}N^{↑} = 5 \\ F^{↑} = 120 \\ F 1^{↑} = 24 \end{matrix} ]_{⋆}), ⋯

To obtain a terminating algorithm from this unfolding process, we employ an abstract domain. In effect, we check to see if the size of groups grows during unfolding. If so, we approximate groups by abstract formulas, in addition to maintaining partial information about the (exact) constraints. We give the details in the next section.

5 The Engine

We first extend the definition of clusters given in the previous section to include approximate groups. An approximate group is defined wrt a given abstract domain D; it is simply of the form [A] where A ∈ D. An exact group is of the form [c]_{⋆} or [c]_{k} where c is a constraint, and the dependency k is the index of some program rule R_{k}. Some exact groups may be marked residual during execution of the engine. A group is an exact or approximate group. A cluster is of the form (G_{1}, …, G_{n}) where each G_{i} is a group. Our algorithm starts with the semantic equations of a program P and then modifies these equations using unfolding steps. At all times, corresponding to each rule R_{k}, there is one semantic equation of the form Ψ_{k} = C_{1} ∪ ⋯ ∪ C_{n} where the C_{i} are clusters. Moreover, the following invariants on the free variables of the groups in C_{i} shall be maintained:

• if [A] appears in C_{i} then var(conc(A)) ⊆ var(R_{k})

• if [c]_{j} appears in C_{i} then var(c) ⊆ var(R_{k}↑) ∪ var(R_{j}↓)

• if [c]_{⋆} appears in C_{i} then var(c) ⊆ var(R_{k}↑)

Given a function I that maps from each Ψ_{i} to a set of constraints whose free variables are from var(R_{i}), each group and cluster is interpreted as a collection of constraints:

• I([A]) =^{def} conc(A),

• I([c]_{⋆}) =^{def} {c↓},

• I([c]_{k}) =^{def} {((∃_{var(R_{k})})(c↑ ∧ c′))↓ : c′ ∈ I(Ψ_{k})}, and

• I ((G_{1}, …, G_{n})) =^{def} {c_{1} ∧ ⋯ ∧ c_{n} : c_{i} ∈ I(G_{i})}.

The basic operation of our algorithm involves the substitution one cluster into another. This is defined via substitution at the level of groups. First define the composition of an exact group with an approximate group as follows:

[c]_{i} ∘ [A] =^{def} abs ({((∃_{var(R_{i})})(c↑ ∧ c′))↓ : c′ ∈ conc(A)})

Next, define the composition of an exact group [c_{1}]_{i} with an exact group [c_{2}]_{j} as follows^{3}

[c_{1}]_{i} ∘ [c_{2}]_{j} =^{def} [(∃_{var(R_{i})})(c_{1}↑ ∧ c_{2}↓)]_{j}

Now, to embed a notion of approximation into the composition [c_{1}]_{i} ∘ [c_{2}]_{j} of groups, define the “approximate composition” [c_{1}]_{i}⋄[c_{2}]_{j} as follows. First, compute [c_{1}]_{i}∘[c_{2}]_{j} and let the result be [c]_{j}. Then, [c_{1}]_{i} ⋄ [c_{2}]_{j} is defined to consist of two groups. The first group is simply the D-approximation of [c_{1}]_{i} ∘ [c_{2}]_{j}, that is, [abs(c)].

The second group is [select_{c_{1},c_{2}}(c)]_{j} where select_{c_{1},c_{2}} returns a constraint. The purpose of select is to maintain some of the information in [c_{1}]_{i} ∘ [c_{2}]_{j} while preventing unbounded growth in the semantic equations. At this point, we do not require an exact definition of select; we just need that it returns a weaker constraint. The definition of select is a parameter of the engine, and we say more about it later.

We are now in a position to define the main step of our engine. A cluster is said to be in substitution form if it contains only approximate, terminal and residual groups. Then:

Definition 2 (Unfolding Step) Let C_{1} be a cluster containing a non-terminal group G. Let C_{2} be a cluster in substitution form. Construct a new cluster by replacing G in C_{1} by all of the following groups:

• G◯_{R} , that is, the group G marked as \underline{residual};

• G ∘ [A], for all approximate groups [A] ∈ C_{2}, and

• G ⋄ [c]_{i}, for all exact (i.e. terminal or residual) groups [c]_{i} ∈ C_{2}.

We say that this new cluster is the result of \underline{substituting} C_{2} \underline{into} C_{1} \underline{at} G.

Example 1 Consider the abstract domain LSign. The following presents clusters C_{1}, C_{2}, and C_{3} respectively. C_{3} is the result of substituting C_{2} into C_{1}. input a program P; obtain the semantic equations associated with P; repeat

3Note that unlike examples in the previous section, we do not require j to be ⋆ in this definition. This extension relates to the use of residual groups, described later.

apply an effective unfolding step if possible;

until no effective unfolding step is possible; delete all clusters not in substitution form; delete all residual groups^{4}; output the resulting equations;

Figure 1: The Unfolding Engine

( [ \begin{matrix}X^{↑} = U^{↓} + 1 \\ Y^{↑} = V^{↓} − 2 \end{matrix} ]_{i} ) ( [ \begin{matrix}5 × U^{↑} + 9 × V^{↑} = 20 \\ U^{↑} ≥ 0 \end{matrix} ]_{⋆} ) ( \begin{matrix}[ \begin{matrix}X^{↑} = U^{↓} + 1 \\ Y^{↑} = V^{↓} − 2 \end{matrix} ] & ◯_{R}_{i} \\ [ X^{↑} ≥ 1 ] & ⋆ \\ [ & ⊕X ⊕ Y = ⊕ & ] \end{matrix} )

Consider C_{3}. The group in C_{1} becomes residual in C_{3}. The group [X^{↑} ≥ 1]_{⋆} in C_{3} is obtained from select, as a truncation of the composition

[ \begin{matrix}X^{↑} = U^{↓} + 1 \\ Y^{↑} = V^{↓} − 2 \end{matrix} ]_{i} ∘ [ \begin{matrix}5 × U^{↑} + 9 × V^{↑} = 20 \\ U^{↑} ≥ 0 \end{matrix} ]_{⋆} = [ \begin{matrix}5 × X^{↑} + 9 × Y^{↑} = 7 \\ X^{↑} ≥ 1 \end{matrix} ]_{⋆} (5.4)

(Note that there are really many ways to write the constraints resulting from this composition. The behavior of select will depend on which “canonical form” is chosen. We discuss this issue in the next section.) The third group [⊕X ⊕ Y = ⊕] is approximate, and is obtained by applying abs to the composition described in (5.4).

An unfolding step is applied to a collection of semantic equations as follows. Let C_{1} appear in the semantic equation for Ψ_{i}, and let [c]_{j} ∈ C_{1}. Let C_{2} appear in the semantic equation for Ψ_{j}. If substituting C_{2} into C_{1} at [c]_{j} results in a cluster C that does not already appear in the semantic equation for Ψ_{i}, then C is added to this equation and we say that the unfolding step was effective.

The complete engine is presented in Figure 1. It is essentially an exhaustive application of the unfolding step just defined. When no more effective unfolding steps can be performed, all clusters in substitution form are output after first deleting the residual groups therein. Such clusters represent fixed sets of constraints because the groups therein are not recursively defined in terms of other groups and/or Ψ_{i} variables. The important point here is that the output is an explicit representation of a set of constraints for each Ψ_{i}. A post-processing phase may then be applied to extract the specific information sought.

4We remark that these groups in fact do contain additional information. More complex post-processing algorithms can be designed to take advantage of this.

Example 2 To exemplify the use of residual groups, consider the following CLP(R) program, and its semantic equations (after some basic simplification):

   p(X, Y) :- q(f(X, Y)), s(Y).
   q(U) :- r(U).
   r(f(V, W)) :- V + W = 3.
   s(Z) :- Z = 1.

Ψ_{1} = ( \begin{matrix}[f(X^{↑}, Y^{↑}) = U^{↓}]_{2} \\ [Y^{↑} = Z^{↓}]_{4} \end{matrix} )◯_{1} Ψ_{2} = ([U^{↑} = f(V^{↓}, W^{↓})]_{3})◯_{2} Ψ_{3} = ([V^{↑} + W^{↑} = 3]_{⋆})◯_{3} Ψ_{4} = ([Z^{↑} = 1]_{⋆})◯_{4}

Now consider the execution of the engine, again using the LSign domain. The initial semantic equations contain two clusters in substitution form: ◯_{3} and ◯_{4}. The following two unfolding steps can be performed: cluster ◯_{3} can be substituted into ◯_{2} and cluster ◯_{4} can be substituted into ◯_{1}, yielding

( \begin{matrix}[U^{↑} = f(V^{↓}, W^{↓})]◯_{R}_{3} \\ [⊤]_{⋆} \end{matrix} )◯_{5}  ( \begin{matrix}[f(X^{↑}, Y^{↑}) = U^{↓}]_{2} \\ [Y^{↑} = 1]_{⋆} \end{matrix} )◯_{6}

where ⊤ is the least informative abstract formula. Thus ◯_{5}, as a result of approximation and select, provides no new information, except that it now contains a residual group. Note also that we have omitted residual and approximate groups from ◯_{6} because they would have been redundant; select, in this case, did not change its input constraints. Now, these new clusters are added to the equations for Ψ_{2} and Ψ_{1} respectively. Next, cluster ◯_{5} is substituted into ◯_{6} at the first group, and this yields

( \begin{matrix}[f(X^{↑}, Y^{↑}) = U^{↓}]◯_{R}_{2} \\ [X^{↑} = V^{↓} ∧ Y^{↑} = W^{↓}]_{3} \\ [⊤]_{⋆} \\ [Y^{↑} = 1]_{⋆} \end{matrix} )◯_{7}

which is added to the equation for Ψ_{1}. Finally, cluster ◯_{3} can be substituted into ◯_{7} at the second group to produce ◯_{8}, which in turn can be simplified into ◯_{9}.

( \begin{matrix}[f(X^{↑}, Y^{↑}) = U^{↓}]◯_{R}_{2} \\ [X^{↑} + Y^{↑} = 3]_{⋆} \\ [⊤]_{⋆} \\ [Y^{↑} = 1]_{⋆} \end{matrix} )◯_{8}  ( \begin{matrix}[f(X^{↑}, Y^{↑}) = U^{↓}]◯_{R}_{2} \\ [X^{↑} = 2 ∧ Y^{↑} = 1]_{⋆} \end{matrix} )◯_{9}

Note that the residual group was used maintain the connection between X, Y and U, because the abstract domain was not sufficiently expressive to represent the constraints U^{↑} = f(V^{↓}, W^{↓}) ∧ X^{↑}+ Y^{↑} = 3.

At this point the engine terminates, and outputs all clusters in substitution form: ◯_{3}, ◯_{4}, ◯_{5} and ◯_{8}. The output of interest is ◯_{8}, corresponding to Ψ_{1}, which represents the constraint X = 2 ∧ Y = 1.

For this example we could make ad hoc extensions to the domain to increase its expressiveness: for example, consider a domain that combines a domain for representing term structure with LSign so that we can represent linear constraints between sub-expressions of a structure. However, not only is such a domain computationally expensive, but it also limited: we can always construct a program that exceeds the inherent bounds of the domain. In contrast, residuals essentially borrow from set constraints the ability to represent unbounded properties of program structure.

An additional example, illustrating the execution of the engine on a CLP program involving boolean constraints, is presented in the Appendix.

6 Termination: Solved Forms and Select

To simplify our presentation so far, we have treated semantically equivalent constraints as equal. Moreover, we have freely allowed constraints to be rewritten into an equivalent but simpler form (for example, constraints such as f(X, Y) = f(U, V) have been rewritten into X = U ∧ Y = V). However, such an abstract view of the unfolding engine glosses over an important issue: how are constraints represented and manipulated by the algorithm? This question has particular relevance to the select function, whose definition is typically in terms of some notion of growth of constraints during the substitution step. Such notions cannot be formalized without fixing the constraint representation.

We address this issue by explicitly introducing a constraints simplification procedure simplify, which is invoked on each constraint considered by the algorithm. Specifically, we shall invoke simplify on every constraint in the initial semantic equations, and on every new constraint constructed during the execution of the algorithm. For example, when we construct new constraints by computing [c_{1}]_{i} ∘ [c_{2}]_{j}, we shall actually compute

[simplify ((∃_{S})(c_{1}↑ ∧ c_{2}↓))]_{j}

rather than [(∃_{S})(c_{1}↑ ∧ c_{2}↓)]_{j}. In effect, simplify defines a notion of “solved form” constraints, and these solved form constraints are the basis of our constraint representation: the algorithm maintains all constraints in solved form.

Typically, we will choose simplify to be a suitable constraint solver for the constraint domain at hand. For the domain of finite trees, it would be appropriate to use a unification algorithm (in effect this is what is used in [6]). For the domain of infinite trees, one would use an infinite tree unification algorithm. For linear equalities, a version of Gaussian Elimination could be appropriate. For more complex constraint domains, such as that of CLP(R), the choices are less obvious. We could for example use a complete solver for finite trees and real numbers, but this would be expensive. At the other end of the spectrum, we could use a trivial solver: the identity function. This would be cheap, but new constraints would always grow and so the accuracy of the algorithm would more likely suffer (because of select). There is an obvious accuracy/efficiency tradeoff here.

However, more important than this tradeoff is the intended purpose of the analysis. If the analysis is used to obtain general semantic properties about a program, then any simplify is appropriate. On the other hand, if we are using the analysis for the purposes of optimizing the execution of a program on a particular CLP system, then it is important to choose simplify to be compatible with the CLP system at hand. For example, in the context of the CLP(R) system [8], it would be appropriate for simplify to solve tree equations, linear equations and linear inequalities, but not arbitrary non-linear constraints. In general, we want simplify to be weaker than the solver of the CLP system.

We next discuss the select operation. It is a parameter to our engine, and it serves to ensure termination. Ideally, select is the identity function; in reality, this choice may not be possible nor practical. The appropriate choice is clearly dependent on many factors, such as the underlying constraint and abstract domains, the runtime properties sought, and of course requirements on accuracy and efficiency. For this paper, we simply require that

• select returns a weaker constraint, that is, c ⊧ select_{c_{1},c_{2}}(c) for all c, c_{1}, c_{2};

• the set of constraints returned during execution of the engine is bounded.

For example, an intuitive way of defining select is via a metric ∇ on constraints that satisfies the following condition: given a constraint c, there are only a finite number of constraints c′ such that var(c′) ⊆ var(c) and ∇(c′) ≤ ∇(c). For equations over term structures, ∇ can just count the symbols appearing in the constraints (c.f. [6]). However, for constraints such as those in CLP(R), there can be infinite collections of constraints of the form {X = 1, X = 2, X = 3, …} and so here ∇ must also take into account the size of constants appearing in constraints. Now, select can be any function such that

∇(select_{c_{1},c_{2}}(c)) ≤ max(∇(c_{1}), ∇(c_{2})).

For example, select_{c_{1},c_{2}}(c) can simply truncate c so that ∇ is sufficiently reduced.

7 Main Results

We first address the correctness of the algorithm. The proof here has two parts. The first part shows that the algorithm terminates. The second shows that, on termination, the unfolding transformation has been applied sufficiently often so that the output clusters contain a conservative (superset) approximation of the least model of the original semantic equations.

Theorem 1 (Correctness and Termination) Let P be a program and let D be a finite^{5} abstract domain. Then the unfolding engine terminates on P using D, and the output semantic equations are a conservative approximation of the initial semantic equations for P.

Proof outline: The key to termination is select. In essence we need to establish, for the specific select and simplify functions at hand, that the following sets G_{i}, 1 ≤ i ≤ N, are finite:

• G_{i} contains all exact groups [c]_{j} that appear on the right hand side of the equation for Ψ_{i} in the initial semantic equations;

• if [c_{1}]_{j} ∈ G_{i}, [c_{2}]_{k} ∈ G_{j} and [c_{1}]_{j} ∘ [c_{2}]_{k} is [c]_{k} then select_{c_{1},c_{2}}(simplify(c)) ∈ G_{i}

Typically, select shall be defined with this kind of property in mind (for example, see the discussion in the end of the previous section that outlines the use of a metric ∇ to define select).

To argue correctness of the algorithm, first observe that the main body of the algorithm serves to add expressions to the right hand side of the constraints. Hence, it is clear that at the end of the main loop of the algorithm, that the resulting semantic equations – call them SE_{loop} – are such that their least solution is a superset of the solution of the original semantic equations. This follows directly from monotonicity of the semantic equation formulation. The next step of the proof establishes that the substitution form clusters of SE_{loop} in fact describe the least model of the SE_{loop}. In essence this step proves a form of completeness of the unfolding step. The final step shows that when residual groups are deleted from a cluster, the resulting cluster describes a superset of the constraints described by the cluster with residuals. The proof here involves establishing a non-local invariant of the algorithm.

In order to compare the standard engine (formalized in the Appendix) with the unfolding engine, we now formulate the operation of the standard engine using our framework of groups clusters, composition etc. Recall that in our framework, we can perform bottom-up or top-down analysis simply by using the appropriate semantic equations. Now, the standard engine proceeds exactly as the unfolding engine, except that:

• all terminal groups [c] are initially replaced by abs(c);

• the unfolding step is simplified so that no residual groups are produced.

The main effect of these changes is that clusters in substitution form contain only approximate groups (and no terminal or residual groups). Hence the only operation required during unfolding is the composition [E] ∘ [A] of an exact and approximate group.

Proposition 2 This formulation correctly describes the standard engine.

Clearly these modified unfolding steps are less accurate than the unfolding step used in the (full) unfolding engine. Hence we can verify that Theorem 2 The unfolding engine is uniformly more accurate than the standard engine in the sense: given a finite abstract domain, the output of the unfolding engine, for any program, is more accurate than that of the standard engine.

5Some algorithms use domains satisfying a weaker condition such as the “finite chain” property. Our engine can in general be adapted to terminate on such domains. We omit the details for simplicity.

8 Conclusion

We presented a generic engine for CLP analysis, based on unfolding. To highlight its advantages, we now make two comparison. The first is to an earlier unfolding engine for traditional logic programs [6]. The new engine represents a substantial advance because:

• The old engine was designed around a specific representation of substitutions that cannot be generalized to CLP. In contrast, the new engine is based on a very general and uniform treatment of constraints.

• The new engine is more efficient, conceptually simpler and avoids some ad hoc steps contained in the previous engine.

• When used to analyze logic programs, the new engine is strictly more accurate than the old engine. This is because residuals are now represented as constraints and hence can be “bidirectional” in the sense that they can transfer structural information in both directions. In contrast, the previous engine essentially truncated residual groups so that they were essentially substitutions mapping input variables into output variables. For example, the old engine would truncate the residual group [X_{1}↑ = f(Y_{1}↓), f(X_{2}↑) = Y_{2}↓]◯_{R} into [X_{1}↑ = f(Y_{1}↓)]◯_{R} , whereas the new engine maintains the entire residual group (since it does not rely on using substitution forms).

Our second comparison is with traditional CLP analysis. The framework of the new engine is conceptually simple and yet general; it includes the standard CLP engine as a special case. The new engine is also flexible, and provides new new opportunities for tuning efficiency/accuracy tradeoffs. By varying aspects of the engine, one can obtain a wide spectrum of behaviors. Finally, regardless of tuning, constraint domain, or abstract domain, the new unfolding engine is uniformly more accurate than the traditional CLP engine.

References

[1] P. Cousot and R. Cousot, “Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints”, Proc. 4^{th} ACM-POPL, 1977, pp 238–252.

[2] M. Garcia de la Banda and M. Hermenegildo, “A Practical Approach to the Global Analysis of CLP Programs”, Proc. Int. Symp. on Logic Programming, 1993, pp 437–455.

[3] N. Heintze, “Set Based Program Analysis”, Ph.D. thesis, School of Computer Science, Carnegie Mellon University, October 1992.

[4] N. Heintze and J. Jaffar, “A Finite Presentation Theorem for Approximating Logic Programs”, Proc. 17^{th} ACM-POPL, 1990, pp 197–209.

[5] N. Heintze and J. Jaffar, “A Decision Procedure for a Class of Herbrand Set Constraints”, Proceedings 5^{th} IEEE-LICS, 1990, pp 42–51.

[6] N. Heintze and J. Jaffar, “An Engine for Logic Program Analysis”, Proc. 7^{th} IEEE-LICS, pp 318–328, 1992.

[7] J. Jaffar and J.-L. Lassez, “Constraint Logic Programming”, Proc. 14^{th} ACM-POPL, 1990, pp 111– 119.

[8] J. Jaffar, S. Michaylov, P. Stuckey and R. Yap, “The CLP(R) Language and System”, ACM TOPLAS, 14(3), pp 339–395, 1992.

[9] N.D. Jones and H. Søndergaard, “A Semantics-based Framework for the Abstract Interpretation of PROLOG”, in Abstract Interpretation of Declarative Languages, (S. Abramsky and C. Hankin, Eds), Ellis Horwood, 1987, pp 123–142.

[10] K. Marriott and H. Søndergaard, “Analysis of Constraint Logic Programs”, Proc. 1990 North American Conf. on Logic Programming, 531-547, 1990.

[11] K. Marriot and P. Stuckey, “The 3 R’s of Optimizing Constraint Logic Programs: Refinment, Removal and Reordering”, Proc. 20^{th} ACM-POPL, 1993, pp 334–344.

[12] K. Marriot and P. Stuckey, “LSign: Approximating Possible Interaction between Linear Arithmetic Constraints”, to appear, Proc. Int. Symp. on Logic Programming, 1994.

Appendix

Standard Engine for CLP

It is difficult to characterize every algorithm for logic program analysis using a single algorithm. This is because each algorithm is designed with different criteria — ad hoc approximations are often introduced for efficiency reasons. However, these differences are rarely fundamental from a conceptual point of view. Consequently, it is possible to define an idealized engine which encompasses the essence of the abstract interpretation technique that underlies these algorithms, and is at least as accurate as any of them. We call this idealized engine the standard engine, and it can be argued that this algorithm is the most obvious embodiment of an abstract domain into an analyzer. More detailed formalizations of this engine can be obtained from [10] and [2].

In general, each analysis algorithm starts by associating a value from the chosen abstract domain D with designated parts of the program. The operation of the algorithm then consists of repeatedly recomputing each value from the values previously computed. In what follows, we give, for the sake of completeness, an informal definition of the standard engine for bottom-up analysis; other analyses, such as top-down, can be similarly described.

1.   Initialize the array abs formula[1..N];
2.   loop {
3.        for (1 ≤ i ≤ N) {
4.             let c denote the constraints of rule i;
4.             let B̃ denote the body atoms of rule i;

5. new abs formula[i] := ⋃_{H̃} D-solve(c, B̃, H̃, abs formula[ ])

                     where H̃ ranges over sequences of rule heads matching B̃;
6.  }

7. if (new abs formula[ ] = abs formula[ ]) break;

8. abs formula[ ] := new abs formula[ ];

9. }

10. output abs formula[ ];

where the operation D-solve uses the abstraction and concretization functions associated with D to implement the basic operational step of obtaining a new abstract formula from a given old abstract formula and a new (concrete) constraint. Formally, let B̃ be B_{1}, ⋯, B_{m}, and let H̃ be H_{j_{1}}, ⋯, H_{j_{m}}. Then D-solve(c, B̃, H̃, abs formula[]) is defined to be

abs (\{c ∧ ( \begin{matrix}∃\overline{var(B_{1})}(B_{1} = H_{j_{1}}θ ∧ c_{1}θ) \\ ∧ ⋯ ∧ \\ ∃\overline{var(B_{m})}(B_{m} = H_{j_{m}}θ ∧ c_{m}θ) \end{matrix} ) : c_{i} ∈ conc(abs formula[j_{i}]), 1 ≤ i ≤ m\})

where θ renames away from B_{1}, …, B_{m}.

A Non-CLP(R) Example

Consider the following CLP program involving boolean constraints (over {0, 1}):

  p(X, Y) :- (X xor Y) = 1, q(X, Y).
  q(W, Z) :- r(W, Z).
  r(U, V) :- (U ⇒ V) = 1.

Ψ_{1} = ( \begin{matrix}[(X xor Y) = 1]_{⋆} \\ [X^{↑} = W^{↑} ∧ Y^{↑} = Z^{↓}]_{2} \end{matrix} ) Ψ_{2} = ([W^{↑} = U^{↑} ∧ Z^{↑} = V^{↓}]_{3}) Ψ_{3} = ([(U^{↑} ⇒ V^{↓}) = 1]_{⋆})

where xor denotes exclusive-or and ⇒ denotes implication. Using an abstract domain in which variables are mapped to either 1, 0 or ⊤, the unfolding engine generates the following clusters (after simplification and removal of redundancy):

( \begin{matrix}[W^{↑} = U^{↑} ∧ Z^{↑} = V^{↓}]◯_{R}_{⋆} \\ [W^{↑} = ⊤ ∧ Z^{↑} = ⊤]_{⋆} \end{matrix} ) ( \begin{matrix}[(X xor Y) = 1]_{⋆} \\ [X^{↑} = W^{↓} ∧ Y^{↑} = Z^{↓}]◯_{R}_{2} \\ [X^{↑} = U^{↓} ∧ Y^{↑} = V^{↓}]_{3} \\ [X^{↑} = ⊤ ∧ Y^{↑} = ⊤]_{⋆} \end{matrix} ) ( \begin{matrix}[X^{↑} = 0 ∧ Y^{↑} = 1] \\ [X^{↑} = W^{↓} ∧ Y^{↑} = Z^{↓}]◯_{R}_{2} \end{matrix} )

Note that the first group in the third cluster is an approximate group. We remark that the appearance of the rule “q(W, Z) :- r(W, Z).” is intended to be suggestive of some intermediate chain of computation that separates p and r. A key idea behind the unfolding engine (and the residual groups in particular) is that it allows information from very different parts of a program to propagate to points where they can interact with each other to improve the accuracy of the analysis.