An Engine for Logic Program Analysis

Nevin Heintze  Joxan Jaffar
School of Computer Science  IBM T.J. Watson Research Center
Carnegie Mellon University  PO Box 740
Pittsburgh, PA 15213-3890  Yorktown Heights, NY 10598
nch@cs.cmu.edu  joxan@watson.ibm.com

Abstract

Most logic program analyzers employ a standard approach based on abstract interpretation. At the core of these is a generic algorithm or “engine” which is parameterized by an abstract domain. This standard engine is essentially a fixpoint computation over the abstract semantic equations of a program. This paper presents a new engine which is based on unfolding of semantic equations. A main advantage of the unfolding engine is a uniform treatment of structural information in a program. In particular, reasoning about partially instantiated structures, an area where traditional algorithms have been weak, is greatly enhanced. The main result of this paper shows that our engine is uniformly more accurate than the standard engine in the following sense: given an abstract domain, the output of our engine, for any program, is more accurate than that of the standard engine.

1 Introduction

Most algorithms for logic program analysis are based on abstract interpretation, and essentially consist of two components: an abstract domain (and implementations of its associated functions) and an implementation of an iterative fixpoint computation. The focus of these algorithms is in the design of the abstract domain. In general, more sophisticated domains give better analysis.

Consider the simple abstract domain whose formulas map program variables into either ground or any. For example, the formula [X ↦ ground, Y ↦ any] represents substitutions which ground X (and may or may not ground Y). For the first program below, this domain can be used to deduce that Y is ground, but not that X is ground.

          ?- eq(X, Y), r(Y).
          eq(U, U).
          r(a).

                                                          ?- p(f(X, b)).
                                                          p(U) ← q(U).
                                                          q(f(a, V)).
                                                           ?- p(Y), r(Y, X).
                                                           p(U) ← q(U).
                                                           q(f(a, V)).
                                                           r(f(W1, W2), W1).

To overcome this problem, domains have been developed in which information about the aliasing and sharing behavior of variables is maintained; see [3, 12, 7, 9, 11] for example. These dependency-based approaches improve the accuracy of the analysis and, for the first program, they infer that both X and Y are ground. They are, however, rather weak in reasoning about partially instantiated structures. For example, in the second program, the dependency-based approaches cannot infer that X is ground since this requires reasoning about the structure of the terms to which U can be bound.

A different approach, that of set constraints [5], has been shown to be useful for reasoning about structural information. The basic idea here is to reason about the program variables as sets of possible values, as opposed to one set of substitutions. While the target application has been type analysis, this approach can be used for groundness analysis. For the second program, it can infer that X is ground. The weakness of using set constraints, however, is that intervariable dependencies are not represented. For example in the first and third programs, it cannot be inferred that X is ground. Thus the dependency-based and set constraint approaches have different advantages and disadvantages, and hence are not directly comparable. This paper focuses on the fixpoint computation aspect of program analysis, rather than the domain. Whereas domains vary widely from one algorithm to another, the fixpoint computation aspects are similar. (Often algorithms differ because ad hoc approximations are introduced for efficiency reasons.) In fact, it possible to speak of a generic algorithm or “engine” which encompasses the essence of these fixpoint computations.

This paper presents a new engine which can reason about structural information in a uniform manner (as in the set constraint approach), and can also reason about dependencies between variables (as in the standard algorithms). The third program above, for example, can be analyzed by the new unfolding engine. The underlying iteration technique is based upon the use of unfold transformations. While the standard engine iterates over fixed semantic equations, the unfolding engine iterates over dynamically changing equations. The main result shows that the unfolding engine is uniformly more accurate than the standard engine in the sense that, given an abstract domain, the output of the unfolding engine, for any program, is more accurate than that of the standard engine.

2 Semantic Equations

The starting point for our engine is an equational representation of a program’s operational semantics. While such representations are well understood, the purpose of this section is to provide the specific formulation required for the rest of this paper. We introduce our semantic equations by means of an example. Consider the append program:

1.  append(nil, W, W).
2.  append(X.Xs,Y,X.Zs)←append(Xs,Y,Zs).

The formulation of semantic equations presented here serves to represent, for each rule, the computed answer substitutions obtained from executing the body of that rule. Specifically, introduce variables Ψ_{1} and Ψ_{2} to represent the sets corresponding to rules 1 and 2 respectively. Now construct the equations:

Ψ_{1} = {mgu()}|_{V_{1}}

Ψ_{2} = \{mgu (body = \overline{γ(head_{1})}) : γ ∈ Ψ_{1}\}|_{V_{2}} ⋃ \{mgu (body = \overline{γ(head_{2})}) : γ ∈ Ψ_{2}\}|_{V_{2}}

where head_{1} and head_{2} denote the head atoms of rules 1 and 2 respectively, body denotes the body atom of rule 2, and V_{1} and V_{2} denote the variables in rules 1 and 2 respectively. The function mgu^{1} maps a set of equations to its most general unifier^{2}. The function |_{V} restricts the domain of a set of substitutions to the variables V. Finally, \overline{t} denotes the renaming of the variables in t into new variables. Intuitively, a semantic equation Ψ_{i} = ⋯ provides a definition for the variables in the i^{th} rule.

A model of such equations is a mapping from each Ψ_{i} to a set of substitutions such that each equation is satisfied. For example

\begin{matrix}Ψ_{1} = \{(W ↦ W)\}, \\ Ψ_{2} = \{ \begin{matrix}( \begin{matrix}Xs ↦ nil \\ Y ↦ W \\ Zs ↦ W \end{matrix} ) , ( \begin{matrix}Xs ↦ X.nil \\ Y ↦ W \\ Zs ↦ X.W \end{matrix} ) \\ ( \begin{matrix}Xs ↦ X.X′.nil \\ Y ↦ W \\ Zs ↦ X.X′.W \end{matrix} ) , ⋯ \end{matrix} \} \end{matrix}

where X′, ⋯ are new variables, is a model of the above equations for the append program. It is in fact the least such model^{3} (up to renaming of new variables). It coincides exactly with the program’s meaning in the sense that the set for Ψ_{i} consists of the computed answer substitutions obtained when the body of the i^{th} rule is executed as a goal.

More formally, let P be a logic program whose rules are R_{1}, ⋯, R_{N}. Let H_{i} denote the head atom of R_{i}, and let V_{i} denote var(R_{i}), the variables in R_{i}. Now, for each rule R_{i} of the form H ← B_{1},…, B_{m}, construct an equation Ψ_{i} =

⋃_{j_{1},···,j_{m}} \{mgu ( \begin{matrix}B_{1} =\overline{γ_{1}(H_{j_{1}})} \\ ⋯ \\ B_{m} =\overline{γ_{m}(H_{j_{m}})} \end{matrix} ) : \begin{matrix}γ_{k} ∈ Ψ_{j_{k}} \\ 1 ≤ k ≤ m \end{matrix} \}|_{V_{i}}

where the sequence j_{1}, ⋯, j_{m} ranges over all possible m-tuples of indices such that (a suitably renamed version of) H_{j_{k}} unifies with B_{k}, 1 ≤ k ≤ m. Note that the variable renaming above is such that the expressions \overline{γ_{k}(H_{j_{k}})} are variable disjoint, and further, their variables do not appear in B_{1}, ⋯, B_{m}.

Before considering more examples, consider abbreviating expressions on the rhs (right hand side) of semantic equations of the form

\{mgu (s_{1} =\overline{γ_{1}(t_{1})}, ⋯, s_{m} =\overline{γ_{m}(t_{m})}) : \begin{matrix}γ_{k} ∈ Ψ_{j_{k}} \\ 1 ≤ k ≤ m \end{matrix} \}|_{V}

by ([s_{1} = t_{1}]_{j_{1}} , ⋯, [s_{m} = t_{m}]_{j_{m}})_{V}. Such an expression is called a cluster. For example, the equations for the append program can be written as follows. Note that the rhs of the first equation is an empty cluster, and the rhs of the second equation contains two clusters.

1There can be different definitions; we assume any fixed one.

2mgu(◯̸) is the identity substitution.

3Models are ordered componentwise: model_{1} ≤ model_{2} iff model_{1}(Ψ_{i}) ⊆ model_{2}(Ψ_{i}) for each variable Ψ_{i}.

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

Ψ_{2} = ([append(Xs, Y, Zs) = append(nil, W, W)]_{1})_{V_{2}} ∪

([append(Xs, Y, Zs) = append(X.Xs, Y, X.Zs)]_{2})_{V_{2}}

In general, expressions such as [s = t]_{i} contained in clusters are called groups, and the individual equations contained in groups are called group equations. (Note that group equations are not pure equations; thus [s = t]_{i} is different from [t = s]_{i}.) The subscript i indicates the rule i, and is called the dependency of the group. Consider below another example program and its semantic equations, illustrating clusters of more than one group. Note that we have omitted the subscripts on groups and clusters since these values are obvious from the context (for example, the dependency of the first group is 1 because the variables on the rhs appear only in rule 1, and the subscript of the first cluster is {X, Y } because the cluster appears in the equation for rule 1).

1.  p(f(X)) ← p(X), q(X), r(Y).
2.  p(a).
3.  q(W).
4.  r(b).

\begin{matrix}Ψ_{1} = ( \begin{matrix}[p(X) = p(f(X))] \\ [q(X) = q(W)] \\ [r(Y) = r(b)] \end{matrix} ) ⋃ ( \begin{matrix}[p(X) = p(a)] \\ [q(X) = q(W)] \\ [r(Y) = r(b)] \end{matrix} ) \\ Ψ_{2} = Ψ_{3} = Ψ_{4} = () \end{matrix}

In the least model, Ψ_{1} is {(X ↦ a, Y ↦ b), (X ↦ f(a), Y ↦ b), (X ↦ f(f(a)), Y ↦ b), ⋯}.

We finally remark that the semantics 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; we defer an illustration of this to the appendix. Neither formulation presents any new concepts; rather, they are necessary preliminary definitions.

In what follows, the term semantic equations shall mean either the equations corresponding to bottomup or top-down program execution. Our engine can be applied in either case.

3 Unfolding Semantic Equations

A key idea behind our engine is the substitution of one cluster into another. Such a substitution step may generate a new cluster. The engine is essentially an exhaustive application of this step. We now elaborate.

Consider a group G whose dependency i is a fact, that is, rule i has no body. Since the equation for rule i is of the form Ψ_{i} = (), any model of the semantic equations must map Ψ_{i} to the singleton set consisting of the identity substitution. Hence G has a fixed interpretation in any model, and can be thought of as representing a fixed set of substitutions. Call such groups G terminal. A group is in substitution form if the lhs (left hand side) of each equation therein is a variable; a cluster is in substitution form if each of its groups is in substitution form. We illustrate informally how such clusters are used as substitutions by returning to the append example. Recall the semantic equations for append, which we can simplify (by rewriting equations between predicates p(s̃) = p(t̃)^{4} into s̃ = t̃) to become:

\begin{aligned}Ψ_{1} & = & () \\ Ψ_{2} & = & ([ \begin{matrix}Xs = nil \\ Y = W \\ Zs = W \end{matrix} ]) ∪ ([ \begin{matrix}Xs = X.Xs \\ Y = Y \\ Zs = X.Zs \end{matrix} ]) \end{aligned}

Denote the two clusters in the equation for Ψ_{2} by C_{1} and C_{2} respectively. C_{1} contains a terminal group G_{1} which represents the substitution (Xs ↦ nil, Y ↦ W, Zs ↦ W). C_{2} contains a group G_{2} which is nonterminal. By substituting C_{1} into C_{2}, we obtain the new cluster:

([ \begin{matrix}Xs & = & X.nil \\ Y & = & W \\ Zs & = & X.W \end{matrix} ]) (3.1)

which can be added to the equation for Ψ_{2} so that the rhs of Ψ_{2} becomes:

\begin{aligned}( \\ [ & \begin{matrix}Xs=nil \\ Y =W \\ Zs=W \end{matrix} & ] \\ & & ) \end{aligned} ∪ \begin{aligned}( \\ [ & \begin{matrix}Xs=X.Xs \\ Y =Y \\ Zs=X.Zs \end{matrix} & ] \\ & & ) \end{aligned} ∪ \begin{aligned}( \\ [ & \begin{matrix}Xs=X.nil \\ Y =W \\ Zs=X.W \end{matrix} & ] \\ & & ) \end{aligned}

The correctness of a substitution step follows from the fact that it is essentially an “unfolding” operation using the definition of Xs, Y, and Zs. That is, the new expression (3.1) is subsumed by C_{2} in the following sense: in all models I of the original equations, I((3.1)) ⊆ I(C_{2}). Hence the original and new equations are equivalent.

However, the new equation is more explicit in the sense that it displays more elements of the set Ψ_{2} (as terminal groups). Clearly the process of unfolding of equations can be repeated indefinitely to obtain new clusters ([Xs = X.X′.nil, Y = W, Zs = X.X′.W]), ⋯, etc. Note that each such cluster represents an answer substitution for the body of the second rule of append. To obtain a terminating analysis algorithm, this process of adding new clusters must be curtailed by using a notion of approximation.

4The symbol ∼ groups terms into a sequence; for example, s_{1}, ⋯, s_{n} may be abbreviated s̃ and equations s_{1} = t_{1}, ⋯, s_{n} = t_{n} abbreviated s̃ = t̃.

Consider approximating the new groups constructed during the substitution step. Each such group is terminal and hence defines a fixed set of substitutions. Hence any traditional means for approximating substitution sets can be employed (see, for example, [8]). We present one formalization as follows.

Definition 1 An abstract domain D is a set of abstract formulas together with (a) an abstraction function abs which takes a set of variables and a set of substitutions and returns an abstract formula, and (b) a concretization function conc which takes an abstract formula and returns a set of substitutions satisfying conc(abs_{V}(Θ)) ⊇ Θ for all Θ and variables V. (Typically, some further algebraic conditions are specified, but these will not concern us here.) The definition of abs and conc induces a notion of abstract unification^{5} which is the mapping D-unify_{V}(s, t, A) = abs_{V}(\{mgu(s = tθ) : θ ∈ \overline{conc(A)}\}) where s, t are terms, A ∈ D, and the overline operator in \overline{conc(A)} renames the range of substitutions in conc(A) to avoid name clashes.

Example 1 [11] Let D_{prop} consist of all propositional formulas over certain variables, whose purpose is to describe propositional relationships between groundness of variables. Let abs and conc be described informally as follows. Define that a basic proposition (a variable) X is true in a substitution θ if θ grounds X; the proposition X ∨ Y is true in θ if θ grounds either X or Y; similarly for X ∧ Y, X ⟷ Y, X ∧ Y ⟷ Z, etc. Now define conc(A) to be {θ : A is true in θ}, and define abs_{V}(Θ) to be the weakest proposition A such that var(A) ⊆ V and A is true for all θ ∈ Θ. For instance, the equation X = f(a, Y) can be approximated wrt variables {X, Y } by the formula X ⟷ Y; similarly Xs = X.nil, Y = W, Zs = X.W wrt {Xs, Y, Zs} by (Xs ∧ Y ⟷ Zs).

We return now to the the append example. Using the above abstract domain D_{prop}, we can obtain a terminating unfolding process in a straightforward way: approximate any new groups G constructed during the unfolding step by abs_{V}(G). Specifically, the first unfolding step yields the equation Ψ_{2} =

\begin{aligned}( \\ [ & \begin{matrix}Xs=nil \\ Y =W \\ Zs=W \end{matrix} & ] \\ & & ) \end{aligned} ∪ \begin{aligned}( \\ [ & \begin{matrix}Xs=X.Xs \\ Y =Y \\ Zs=X.Zs \end{matrix} & ] \\ & & ) \end{aligned} ∪ ([Xs ∧ Y ⟷ Zs])

The algorithm outlined so far is not very accurate because the substitution step, when approximated, loses a significant amount of structural information. In fact, when a group G_{1} is substituted into a group G_{2}, the resulting cluster loses all information about these two groups except for that contained in the Dapproximation. A key observation of this paper is that the group G_{2} can in fact be retained. Specifically, we define that the substitution of G_{1} into G_{2}, which originally yielded a single group [Xs ∧ Y ⟷ Zs], now yields two groups:

( [ Xs ∧ Y ⟷ Zs ] [ \begin{matrix}Xs & = & X.Xs \\ Y & = & Y \\ Zs & = & X.Zs \end{matrix} ]◯_{R} )

In other words, the group G_{2} remains after the substitution, and is then pronounced a residual group (marked with ◯_{R}). It is these residual groups which provide our engine with the ability to reason about structures.

4 The Engine

We begin with some definitions, some of which were informally discussed above. Let VAR denote a denumerable set of variables, and let P be a logic program constructed from functors Σ and variables VAR. Let the rules in P be R_{1}, ⋯, R_{N} (N ≥ 1) with variables V_{1}, ⋯, V_{N} respectively. We assume that the sets V_{i} are mutually disjoint.

An exact group is of the form [s_{1} = t_{1}, ⋯, s_{n} = t_{n}]_{k} where the s_{i} and t_{i} are terms constructed from Σ and VAR. Such a group is terminal if R_{k} is a fact. Some exact groups may be marked residual during execution of the engine. An approximate group is defined wrt a given abstract domain D; it is simply of the form [A] where A ∈ D. 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. In the previous section, the semantic equations for a program P were defined. Our engine starts with these equations and modifies them during its execution. 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 and Ψ_{k} is a distinguished variable representing substitutions on V_{k}.

5For pragmatic reasons, some analysis algorithms do not implement D-unify exactly, but instead use a conservative approximation.

An exact group is in substitution form if the lhs of each equation therein is a variable. Let G be a group in substitution form, and let X_{1}, ⋯, X_{n} be the variables var(lhs(G)). Now define subs(G) to be the set of all substitutions of the form (X_{1} ↦ t_{1}, ⋯, X_{n} ↦ t_{n}) where X_{i} = t_{i} ∈ G, 1 ≤ i ≤ n. A exact group can be made into substitution form by deleting certain equations: ˆ[E]_{j} =^{def} [X = t : X = t ∈ E and X is a variable ]_{j}. (This overhat operator will be used only in the construction of residual groups.) A cluster is in substitution form if each group therein is either an approximate group, or a terminal group in substitution form, or a residual group (such groups are identified by the engine).

The basic operation of our algorithm is the notion of substituting a cluster in substitution form into a group. What results is a new cluster. First define the composition of an exact group with an approximate group as follows:

[E]_{i} ∘ [A] =^{def} D-unify_{var(s̃)}(s̃, t̃, A)

where E is s̃ = t̃. Similarly define the composition of an exact group [E_{1}] with an exact group [E_{2}] in substitution form as follows:

[E_{1}]_{i} ∘ [E_{2}]_{j} =^{def} [s = tθ : (s = t) ∈ E_{1}, θ ∈ subs(\overline{E_{2}})]_{j}

where \overline{E_{2}} renames all of the head-only^{6} variables in rhs(E_{2}) into new ones. (For example, [X = f(W, Y)]∘ [Y = W], where W is a head-only variable, should not yield [X = f(W, W)], but rather [X = f(W, W′)].)

To embed a notion of approximation into the composition [E_{1}]_{i} ∘ [E_{2}]_{j} of groups, define the “approximate composition” [E_{1}]_{i}⋄[E_{2}]_{j} to consist of two groups. The first group is simply the D-approximation of [E_{1}]_{i} ∘ [E_{2}]_{j}:

[abs_{var(lhs(E_{1}))} (mgu ([E_{1}]_{i} ∘ [E_{2}]_{j}))]

The second group is a subset of [E_{1}]_{i} ∘ [E_{2}]_{j}. It is defined by select([E_{1}]_{i}, [E_{2}]_{j}) =

[s = tθ : \begin{matrix}(s = t) ∈ E_{1}, θ ∈ subs(\overline{E_{2}}) and \\ either t is a variable or |tθ| = |t| \end{matrix} ]_{j}

where |s| is the number of symbols in s. Intuitively, select chooses equations from [E_{1}]_{i} ∘[E_{2}]_{j} in such a way the size of any term therein does not exceed the size of the terms in the original equations [E_{1}]_{i} and [E_{2}]_{j}.

For example, if [E_{1}]_{i} and [E_{2}]_{j} were [X = W_{1}, Y = f(W_{1}), Z = f(W_{2})]_{i} and [W_{1} = g(a), W_{2} = V]_{j} respectively, then [E_{1}]_{i} ∘ [E_{2}]_{j} is [X = g(a), Y = f(g(a)), Z = f(V)]_{j}. However select([E_{1}]_{i}, [E_{2}]_{j}) will contain the first and third equations, but not the second because f(g(a)) is too big. As we see later, it is possible to consider other definitions of select.

We are now in a position to define the main step of our engine.

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:

• Ĝ, and this group is marked as residual;

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

• G ⋄ [E]_{i}, for all exact groups [E]_{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 2 Consider the abstract domain D_{prop} above. The following presents clusters C_{1}, C_{2}, and C_{3} respectively. C_{3} is the result of substituting C_{2} into C_{1}.

([X =f(Y)]) ( \begin{matrix}[ & \begin{matrix}Y =U \\ Y =g(a) \\ Z =b \end{matrix} & ] \\ [Y =V] \end{matrix}) ( \begin{matrix}[X =f(Y)]◯_{R} \\ [X =f(U)] \\ [X] \\ [X =f(V)] \\ [true] \end{matrix} )

Consider C_{3}. The group [X = f(Y)] is residual. The second group [X = f(U)] is obtained from select([X = f(Y)] ∘ [Y = U, Y = g(a), Z = b]). (Note that the equation X = f(g(a)) is omitted by select.) The third group [X] is approximate, and is obtained from abs_{{X}}(mgu([X = f(Y)]∘[Y = U, Y = g(a), Z = b])). It contains the proposition that X is ground. The fourth group [X = f(V)] is obtained from select([X = f(Y)] ∘ [Y = V]). Finally, the fifth group [true] is approximate and is obtained from abs_{{X}}(mgu([X = f(Y)] ∘ [Y = V])).

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 [E]_{j} ∈ C_{1}. Let C_{2} appear in the semantic equation for Ψ_{j}. If substituting C_{2} into C_{1} at [E]_{j} results in a cluster C which 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.

6A head-only variable appears in the head of a rule but not in the body.

The complete engine is presented in figure 1. It is essentially an exhaustive application of the unfolding step just defined. Note that before an unfolding step is performed, it is necessary to perform some straightforward simplification steps which can be described as follows:

• replace a group equation of the form f(s_{1}, ⋯, s_{n}) = f(t_{1}, ⋯, t_{n}) by s_{1} = t_{1}, ⋯, s_{n} = t_{n};

• delete any cluster which contains (a) a group equation of the form f(s̃) = g(t̃) or (b) two group equations of the form X = f(s̃) and X = g(t̃), where f ≠ g;

• replace any group of the form [s_{1} = t_{1}, ⋯, s_{n} = t_{n}], where one of the equations is of the form f(u_{1}, ⋯, u_{k}) = W and W is a head-only variable, by [s_{1} = t_{1}θ, ⋯, s_{n} = t_{n}θ] where θ is the substitution [W ↦ f(W_{1}, ⋯, W_{k})] and the variables W_{1}, ⋯, W_{k} are new variables. (Intuitively, a group such as [f(X) = W, Y = W] does define a substitution though not in substitution form. This simplification step remedies the problem by transforming it to [f(X) = f(W_{1}), Y = f(W_{1})], which in turn can be simplified into [X = W_{1}, Y = f(W_{1})].)

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 substitutions 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 substitutions for each Ψ_{i}. A postprocessing phase may then be applied to extract the specific information sought.

Example 3 Consider the following program and its (simplified) semantic equations:

    main(Y) ← p(f(X)), q(X, Y).
    p(U) ← r(U).
    q(g(W1, W2), W1).
    r(g(a, W3)).
    r(f(V)) ← r(V).

input an arbitrary program P;

obtain the semantic equations for P; repeat

exhaustively apply the basic simplification steps; apply an effective unfolding step if possible;

until no effective unfolding step is possible; delete all residual groups^{7}; output all clusters in substitution form;

Figure 1: The Unfolding Engine

Ψ_{1} = ( \begin{matrix}[f(X) = U] \\ [X = g(W 1, W 2), Y = W 1] \end{matrix} )◯_{1}

Ψ_{2} = ([U = g(a, W 3)])◯_{2} ∪ ([U = f(V)])◯_{3}

Ψ_{3} = Ψ_{4} = ()

Ψ_{5} = ([V = g(a, W 3)])◯_{4} ∪ ([V = f(V)])◯_{5}

These initial semantic equations contain two substitution clusters ◯_{2} and ◯_{4}. The following three unfolding steps can be performed: cluster ◯_{2} can be substituted into ◯_{1} and cluster ◯_{4} can be substituted into ◯_{3} and ◯_{5} to obtain

( \begin{matrix}[f(X) = g(a, W 3)] \\ [X = g(W 1, W 2), Y = W 1] \end{matrix} )◯_{6}

( \begin{matrix}[U = f(V)]◯_{R} \\ [true] \end{matrix} )◯_{7}

( \begin{matrix}[V = f(V)]◯_{R} \\ [true] \end{matrix} )◯_{8}

respectively. Consider the first unfolding step. There is no residual group in ◯_{6} because ˆ[E] = ◯̸ when [E] = [f(X) = U]. Cluster ◯_{6} is (eventually) deleted because it contains the conflicting group equation f(X) = g(a, W 3). The clusters ◯_{7} and ◯_{8} are added to the equations for Ψ_{2} and Ψ_{5} respectively.

Next, the clusters ◯_{7} and ◯_{8} can be used in unfolding steps. We omit the details for ◯_{8} since these steps do not lead to any new clusters. Substituting ◯_{7} into ◯_{1} yields ◯_{9} which can be simplified into ◯_{10} and then added to the equation for Ψ_{1}:

7These groups in fact do contain some structural information.

We choose to delete them because substantial post-processing is required to extract this information, and space reasons forbid further description of this.

( \begin{matrix}[f(X)=f(V)] \\ [true] \\ [ & \begin{matrix}X =g(W 1, W 2) \\ Y =W 1 \end{matrix} & ] \end{matrix} )◯_{9}  ( \begin{matrix}[X =V] \\ [true] \\ [ & \begin{matrix}X =g(W 1, W 2) \\ Y =W 1 \end{matrix} & ] \end{matrix} )◯_{10}

Now, there are two possible substitutions into this new cluster: ◯_{4} into ◯_{10} and ◯_{8} into ◯_{10}, respectively yielding

( \begin{matrix}[X = V]◯_{R} \\ [X = g(a, W 3)] \\ [true] \\ [X = g(W 1, W 2), Y = W 1] \end{matrix} )◯_{11}

( \begin{matrix}[X = V]◯_{R} \\ [X = f(V)] \\ [true] \\ [X = g(W 1, W 2), Y = W 1] \end{matrix} )◯_{12}

The second cluster ◯_{12} is (eventually) deleted since it contains the conflicting equations X = f(V) and X = g(W 1, W 2). The cluster ◯_{11} is added to the equation for Ψ_{1}. At this point the engine terminates, and outputs all clusters in substitution form: ◯_{2}, ◯_{4}, ◯_{7}, ◯_{8}, and ◯_{11}. Of interest is ◯_{11}, corresponding to Ψ_{1}, which represents the fixed collection of substitutions given by mgu(X = g(a, W 3), X = g(W 1, W 2), Y = W 1) conjoined with true. This in turn can be simplified and projected onto {X, Y } to obtain {(X ↦ g(a, t), Y ↦ a) : t is any term} from which we can deduce that Y is ground.

To see need for residual groups in the above example, consider removing the residual group in ◯_{7}. Then the group [f(X) = f(V)] would not be in in ◯_{9}, and consequently the group [X = V] would not be in in ◯_{10}, and consequently the group [X = g(a, W 3)] would not be in ◯_{11}, our output cluster. Hence it cannot be inferred that Y is ground.

One could raise the question as to why the group in ◯_{3}, which gave rise to the residual group in ◯_{7}, could not itself be used for substitution into ◯_{1}. (That is, consider substituting ◯_{3} into ◯_{1}.) Allowing this means that groups which are neither terminal nor residual are allowed to be substituted into other clusters. This means that many more unfolding steps are permitted in general. The following example shows that such substitutions cause loss of information.

Example 4 Consider the domain D_{prop} once again, and let C_{1}, C_{2} and C_{3} respectively be

\begin{aligned}( \\ [ & \begin{matrix}U_{1} =f(X_{1}) \\ f(U_{2})=X_{2} \end{matrix} & ] \\ & & ) \end{aligned} \begin{aligned}( \\ [ & \begin{matrix}X_{1} =f(Y_{1}) \\ X_{2} =f(Y_{2}) \end{matrix} & ] \\ & & ) \end{aligned} \begin{aligned}( \\ [ & \begin{matrix}Y_{1} =f(W) \\ Y_{2} =f(W) \end{matrix} & ] \\ & & ) \end{aligned}

Let the group in C_{3} be the only terminal group. Our engine dictates that C_{3} is first substituted into C_{2} to

obtain ([X_{1} = f(Y_{1}), X_{2} = f(Y_{2})]◯_{R} , [X_{1} ⟷ X_{2}])

which is then substituted into C_{1} to obtain a new cluster C_{4} which is ([U_{1} = f(X_{1})]◯_{R} , [U_{2} = Y_{2}], [U_{1} ⟷ U_{2}]) after simplification. Finally, C_{3} is substituted into C_{4} to obtain a cluster in substitution form containing [U_{1} ⟷ U_{2}]. Assuming that this is the only cluster output for the rule containing U_{1} and U_{2}, it deduced that U_{1} is ground iff U_{2} is ground.

Now suppose that we allow the substitution of C_{2} into C_{1}, obtaining ([U_{1} = f(X_{1})]◯_{R} , [U_{2} = Y_{2}], [true]), and then using C_{3} to substitute into this, we obtain

([U_{1} = f(X_{1})]◯_{R} , [U_{2} = Y_{2}]◯_{R} , [U_{2} = f(W)], [true]).

Since this cluster is substitution form, it is output. Clearly it forbids the inference that U_{1} is ground iff U_{2} is ground. Intuitively, the problem here was that the substitution of C_{2} into C_{1} was performed before the information from C_{3} was used; this information could not be recovered later.

In order to prove correctness of the engine, it is necessary to first define the meaning of semantic equations used by the engine. Now, the meaning of semantic equations containing only exact groups was given above. However approximate groups are generated during the algorithm. We now informally describe the meaning of these more general equations.

Let mgi(θ_{1}, θ_{2}) denote the most general instance of θ_{1} and θ_{2} if it exists, that is, the most general substitution which is an instance of both θ_{1} and θ_{2}. For example, mgi((X ↦ f(W), Y ↦ a), (X ↦ f(g(W)))) is (X ↦ f(g(W′)), Y ↦ a). Next define the function join_{V}(θ_{1}, θ_{2}) to be mgi(\overline{θ_{1}}, \overline{θ_{2}})|_{V} where the overline renaming operator makes the range of θ_{1} and θ_{2} disjoint. For example, join_{V}((X ↦ f(a), Y ↦ W), (X ↦ W)) is mgi((X ↦ f(a), Y ↦ W_{1}), (X ↦ W_{2}))|_{V} where W_{1} and W_{2} are new variables. Finally, extend the join function to apply over sets: join_{V}(Θ_{1}, Θ_{2}) =^{def} {join_{V}(θ_{1}, θ_{2}) : θ_{1} ∈ Θ_{1}, θ_{2} ∈ Θ_{2}}.

An interpretation I for semantic equations is a mapping from each Ψ_{i} variable, 1 ≤ i ≤ N to a set of substitutions I(Ψ_{i}). For groups, I([s̃ = t̃]_{j}) = \{mgu(s̃ = \overline{γ(t̃)}) : γ ∈ I(Ψ_{j})\}, and I([A]) is simply conc(A). For clusters in the equation Ψ_{i}, I ((G_{1}, ⋯, G_{n})) = join_{V_{i}}(I(G_{1}), ⋯, I(G_{n})). As usual, an interpretation I is a model of semantic equations Ψ_{i} = C_{1} ∪ ⋯ ∪ C_{n}, 1 ≤ i ≤ N, if I(Ψ_{i}) = I(C_{1}) ∪ ⋯ ∪ I(C_{n}).

Theorem 1 (Correctness and Termination) Let P be a program and let D be a finite^{8} 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: Let E^{P} denote the semantic equations obtained from the input program P. The first part of the proof establishes that the least model of these equations (denoted lm(E^{P})) corresponds to the collecting semantics at hand. This is tedious but fairly straightforward (see [5] and [4] for proofs of related results).

We next prove that the algorithm constructs a conservative approximation to lm(E^{P}). Let E^{loop} denote the equations obtained from E^{P} after execution of the main repeat-until loop of the unfolding engine. Let E^{no−res} denote the equations obtained by deleting the residual expressions from E^{loop}, and let E^{final} denote the final equations, that is those obtained by selecting only the substitution form clusters from E^{no−res}. Now, the main loop of the algorithm merely serves to add expression to the rhs of equations in E^{P}. Moreover, the original equations in E^{P} do not contain any residual expressions. Therefore, for each equation X = rhs in E^{P}, there will be an equation of the form X = rhs ∪ ⋯ in both E^{loop} and E^{no−res}. Hence both E^{loop} and E^{no−res} approximate E^{P} in the sense that lm(E^{P}) ⊆ lm(E^{loop}) and lm(E^{P}) ⊆ lm(E^{no−res}).

The main part of the correctness proof establishes that the exhaustive application of the unfolding step generates sufficient substitution form clusters that these clusters alone characterize the least model of E^{no−res}. In essence we prove a form of completeness of the unfolding step with respect to the least model. The proof of this requires reasoning about the specific formulation of the unfolding step, and is omitted.

Termination is proved by showing that there are only a finite number of different clusters that can be produced. This is essentially because during an unfolding step, the function select ensures that the size of terms appearing the new cluster are not larger than those appearing in the previous clusters. The main complications are (a) the part of the simplification step which deals with head only variables, since this step can increase the size of terms and introduce new variables, and (b) the renamings of equations during the unfolding step, since this may introduce new variables. A key part of the termination proof is that the number of new variables can be bounded.

5 Variations of the Engine

The main parameter of the engine is the domain used for approximation. We now discuss two other parts of the engine where there is scope for variation. Consider the select function which is used to curtail the growth of group equations. Another reasonable definition of select can be obtained by using a uniform bound on the size of terms, the so-called “depth-k” approximation. The important point is that the use of any select function does not affect correctness. It will, however, affect accuracy and termination. In general, using a smaller or more restrictive function will make the proof of termination easier (and can also enhance efficiency). Using a bigger function, on the other hand, is more accurate, but it complicates the termination proof in general.

Next consider the output of the engine. As defined, this consists of a collection of clusters in substitution form. Such a collection is an explicit definition, for each program rule, of a set of substitutions. However, to maximize the structural information obtained from the engine, residual groups should not be deleted upon termination. This however raises the problem that if clusters contain residual groups, then they are no longer an explicit representation of a set of substitutions. In fact, they represent an undecidable set of equations in general.

Perhaps the best general technique for extracting information from these residual groups is to approximate them by interpreting them as set constraints, and then employing an intersection algorithm for set expressions (see [6] for example). It is important to note that the engine as stated already has much of the analytical power of the set constraint approach to analysis. Indeed the third program in section 1 shows that it is sometimes strictly more accurate. By augmenting the engine output with the residual groups, and applying an intersection algorithm, the engine in fact becomes uniformly more accurate than the set constraint approach to analysis.

6 Comparison with Abstract Interpretation Algorithms

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 which underlies these algorithms, and is at least as accurate as any of them. We can therefore call this idealized engine a standard engine, which we now outline.

8Some 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.

In general each analysis algorithm starts by associating a value from the chosen abstract domain with designated parts of the program. The operation of the algorithm then consists of repeatedly recomputing each value from the values previously computed. For a bottom-up analysis, an informal and simplified outline is:

initialize the array value[1..N]; loop {

for (1 ≤ i ≤ N) { let B̃ denote the body atoms of rule i;

newvalue[i] := ⋃_{H̃} D-unify(B̃, H̃, value[ ])

where H̃ ranges over all sequences of rule heads which (after appropriate renaming) unify with B̃;

} if (newvalue[ ] = value[ ]) break; value[ ] := newvalue[ ];

} output value[ ];

Example 5 The following illustrates each iteration of the standard engine on an example program. The abstract domain used here is D_{prop}. Note that the i^{th} column describes value[ ] after the i iterations of the main loop.

1:      ?- eq(X, Y), p(f(Y, Z)).
2:      p(U) ← q(U).
3:      q(f(S, V)) ← r(S).
4:      r(a).
5:      eq(W, W).

initial 1  2  3  4
value[1] false false false false x ↔ y
value[2] false false false true true
value[3] false false s s s
value[4] false true true true true
value[5] false true true true true

We can similarly specify a standard engine for topdown analysis, but we defer the details to the appendix. Amongst the many papers for which the standard engine applies are [10, 7] (bottom-up) and [1, 3, 9] (top-down).

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

• all terminal groups [E] are initially replaced by abs_{var(lhs(E))}([E]);

• the unfolding step is simplified so that no residual groups are produced (and this can achieved simply by redefining Ĝ = ◯̸).

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 1 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.

An alternative view of the differences between the standard and unfolding engines is as follows. The standard engine implements abstract interpretation by a successive iteration starting from some initial values A_{0} and computing the sequence A_{0} →^{F} A_{1} →^{F} A_{2} →^{F} A_{3} ⋯ where F represents the abstract semantic function at hand and the A_{i} are the successive abstract values being computed. The unfolding engine, on the other hand, uses a changing abstract semantic function and computes A_{0} →^{F_{0}} A_{1} →^{F_{1}} A_{2} →^{F_{2}} A_{3} · · · . Such a change takes place whenever an unfolding step is applied. The important point is that each function F_{i} is at least as accurate as the original function F.

We conclude this section with the realization of some analysis algorithms using our engine. Let unfold(D) denote the algorithm obtained by using the unfolding engine and the abstract domain D; similarly for standard(D). Let D_{sharing} denote the domain described in [7].

Corollary 1 For groundness analysis, unfold(D_{prop})

is uniformly more accurate than [11] ^{9}.

Corollary 2 For sharing analysis, unfold(D_{sharing})

is uniformly more accurate than [7]. (The second example program in section 1 shows that unfold(D_{sharing}) is strictly more accurate.)

7 Conclusion

A new engine for analysis of logic program is presented. Its starting point is a specific formulation of semantic equations of a program. We have illustrated how these equations can model bottom-up and topdown execution. In fact, they can model the usual variations of top-down execution such as those with fixed atom selection rule (for example left-to-right). Using a given abstract domain D, the engine performs unfolding on these equations. Each unfolding is augmented with a notion of approximation, defined in terms of D, to curtail the expansion of terms. The main advantage of our specific technique of unfolding, which uses the key concept of residual groups, is that there is a uniform and accurate treatment of structural information. By formulating the standard analysis engine as a special case of the unfolding engine, we then showed that the unfolding engine is uniformly more accurate than the standard engine.

Yet to be addressed is the issue of efficiency. There are two main parts of the engine in this regard. First is the initial number of clusters in the equations. This number is bounded by the number of sequences of head atoms which match the sequence of body atoms, for each rule. The second part concerns the unfolding step. Though the number of new groups produced by this step is linear in the size of the input clusters, the termination of the engine is based on an exhaustive application of this step. Experience with a prototype implementation of set constraints [4] provides some evidence that these two problems can be overcome. First, the issue of matching body and head atoms in set constraints is essentially the same as in the unfolding engine. Using our set constraint implementation^{10} on reasonable example programs, this issue was not prohibitive. Next consider the issue of unfolding efficiency. In set constraints, there is a notion of substitution which is similar to unfolding in terms of the number of new expressions generated (but whose semantics is very different). The said implementation exploits the crucial fact that the substitution step gives rise to mostly redundant expressions. This experience suggests that the currently planned implementation of the unfolding engine can be engineered to be practical.

Acknowledgments

We thank Michael Maher, Kim Marriott and Roland Yap for their comments.

References

[1] M. Bruynooghe and G. Janssens, “An Instance of Abstract Interpretation integrating Type and Mode Inference”, Proc. 5^{th} Int. Conf. on Logic Programming, MIT Press, pp 669–683, August 1988.

[2] A. Cortesi, G. Filé and W. Winsborough, “Equivalence of Abstract Domains for Groundness Analysis”, Technical Report, Dip. di Matematica Pure é Applicata, Universitá di Padova, 1991.

[3] S. Debray, “Global Optimization of Logic Programs”, Ph.D. Thesis, Department of Computer Science, SUNY at Stony Brook, December 1986.

[4] N. Heintze, “Set Based Program Analysis”, forthcoming Ph.D. thesis, School of Computer Science, Carnegie Mellon University, May 1992 (expected).

[5] N. Heintze and J. Jaffar, “A Finite Presentation Theorem for Approximating Logic Programs”, Proc. 17^{th} ACM-POPL, 1990, pp. 197–209. (A full version of this paper appears as IBM technical report RC 16089 (# 71415), August 1990, 66 pp.)

[6] N. Heintze and J. Jaffar, “A Decision Procedure for a Class of Herbrand Set Constraints”, Proc. 5^{th} IEEE-LICS, June 1990, pp 42 - 51. (A full version of this paper appears as Carnegie Mellon University technical report CMU-CS-91-110, February 1991, 42 pp.)

[7] D. Jacobs and A. Langen, “Accurate and Efficient Approximation of Variable Aliasing in Logic Programs”, Proc. North American Conf. on Logic Programming, 1989, pp 154–165.

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

9By [2], UNFOLD(Dprop ) is uniformly more accurate than a number of other algorithms as well.

10Approximately 3000 lines of Standard ML.

[9] K. Muthukumar and M. Hermenegildo, “Determination of Variable Dependence Information Through Abstract Interpretation”, Proc. North American Conf. on Logic Programming, 1989, pp 166–186.

[10] K. Marriott and H. Søndergaard, “Bottom-Up Abstract Interpretation of Logic Programs” Proc. Fifth International Conf. and Symp. on Logic Programming, 1988, pp 733–748.

[11] K. Marriott and H. Søndergaard and N.D. Jones, “Abstract Interpretation of Logic Programs: The Denotational Approach”, ACM-TOPLAS, to appear. (Also, Proc. Fifth Italian Conf. Logic Programming, 1990, pp 399-425.)

[12] H. Søndergaard, “An Application of Abstract Interpretation of Logic Programs: Occur Check Reduction”, in Proc. ESOP ’86, Saarbrucken, March 86.

Appendix: Top-Down Analysis

Whereas semantic equations for bottom-up analysis collect a set of substitutions for each rule, topdown semantic equations collect information about a number of other “program points”. Typically there is one point corresponding to each rule and one point corresponding to each body atom. The idea is that each point corresponding to a rule is assigned the set of substitutions obtained upon successful execution of the rule body. Similarly, each point corresponding to a body atom is associated with the set of substitutions encountered just before the atom is resolved. Another difference between top-down and bottom-up equations is that execution proceeds from a given initial goal (or set of goals). For technical convenience, it is simplest to distinguish a rule, say main ← A1, ⋯, An, which specifies that the initial goal is ?- A1, ⋯, An.

We omit the details of top-down semantic equations, and instead illustrate them using the program

1.  append(nil, W, W).
2.  append(X.Xs,Y,X.Zs)←append(Xs,Y,Zs)^{4}.
3.  main ← goal^{5}.

where goal is some atom whose variables are denoted by V_{3}, and 1 − 5 denote program points. Variables Ψ_{i} are introduced to collect the substitutions encountered at each point. Ψ_{2} collects the substitutions just after execution of the body atom in the second rule. Ψ_{4} collects those substitutions encountered just before this body atom is called. The top-down equations are:

Ψ_{1} = \{mgu (head_{1} = \overline{γ(body)}) : γ ∈ Ψ_{4}\}|_{V_{1}}

∪ \{mgu (head_{1} = \overline{γ(goal)}) : γ ∈ Ψ_{5}\}|_{V_{1}}

Ψ_{2} = \{mgu ( \begin{matrix}head_{2} = \overline{γ_{1}(body)} \\ body = \overline{γ_{2}(head_{1})} \end{matrix} ) : \begin{matrix}γ_{1} ∈ Ψ_{4} \\ γ_{2} ∈ Ψ_{1} \end{matrix} \}|_{V_{2}}

∪ \{mgu ( \begin{matrix}head_{2} = \overline{γ_{1}(body)} \\ body = \overline{γ_{2}(head_{2})} \end{matrix} ) : \begin{matrix}γ_{1} ∈ Ψ_{4} \\ γ_{2} ∈ Ψ_{2} \end{matrix} \}|_{V_{2}}

∪ \{mgu ( \begin{matrix}head_{2} = \overline{γ_{1}(goal)} \\ body = \overline{γ_{2}(head_{1})} \end{matrix} ) : \begin{matrix}γ_{1} ∈ Ψ_{5} \\ γ_{2} ∈ Ψ_{1} \end{matrix} \}|_{V_{2}}

∪ \{mgu ( \begin{matrix}head_{2} = \overline{γ_{1}(goal)} \\ body = \overline{γ_{2}(head_{2})} \end{matrix} ) : \begin{matrix}γ_{1} ∈ Ψ_{5} \\ γ_{2} ∈ Ψ_{2} \end{matrix} \}|_{V_{2}}

Ψ_{3} = \{mgu (goal = \overline{γ(head_{1})}) : γ ∈ Ψ_{1}\}|_{V_{2}}

∪ \{mgu (goal = \overline{γ(head_{2})}) : γ ∈ Ψ_{2}\}|_{V_{3}}

Ψ_{4} = \{mgu (head_{2} = \overline{γ(body)}) : γ ∈ Ψ_{4}\}|_{V_{2}}

∪ \{mgu (head_{2} = \overline{γ(goal)}) : γ ∈ Ψ_{5}\}|_{V_{2}}

Ψ_{5} = {mgu()}|_{V_{3}}

Finally, we informally outline the standard engine which idealizes the commonly used algorithms for topdown analysis. Let there be n predicates. Let pred(A) map an atom A to the predicate of A. The function D-unify(s, t, A_{1}, A_{2}) returns the abstract unification of s in the context of A_{1} and t in the context of A_{2}.

initialize the arrays value[1..N] and call[1..n] ; loop {

for (1 ≤ i ≤ N) {

let rule i be A ← B̃ where B̃ is B_{1}, ⋯, B_{m};

newvalue[i] :=

⋃_{H̃} D-unify(B̃, H̃, call[pred(A)], value[ ]),

where H̃ ranges over heads which, when suitable renamed, match B̃;

newcall[pred(B_{j})] :=

⋃_{H̃} D-unify ( \begin{matrix}(B_{1}, ⋯, B_{j−1}), H̃, \\ call[pred(A)], value[ ] \end{matrix} ),

where 1 ≤ j ≤ m and H̃ ranges over heads which, when suitably renamed, match B_{1}, ⋯, B_{j−1};

}

if (newvalue[ ] = value[ ] & newcall[ ] = call[ ])

break; value[ ] := newvalue[ ]; call[ ] := newcall[ ];

}
output value[ ] and call[ ];