MAX-PLANCK-INSTITUT FÜR

INFORMATIK

An Abstract Interpretation Algorithm

for Residuating Logic Programs

Michael Hanus

MPI–I–92–217 April 1992

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

Im Stadtwald W 6600 Saarbrücken

Germany Author’s Address

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

michael@mpi-sb.mpg.de

Abstract

Residuation is an operational mechanism for the integration of functions into logic programming languages. The residuation principle delays the evaluation of functions during the unification process until the arguments are sufficiently instantiated. This has the advantage that the deterministic nature of functions is preserved but the disadvantage of incompleteness: if the variables in a delayed function call are not instantiated by the logic program, this function can never be evaluated and some answers which are logical consequences of the program are lost. In order to detect such situations at compile time, we present an abstract interpretation algorithm for this kind of programs. The algorithm approximates the possible residuations and instantiation states of variables during program execution. If the algorithm computes an empty residuation set for a goal, then it is ensured that the concrete execution of the goal does not end with a nonempty set of residuations which cannot be evaluated due to insufficient instantiation of argument variables.

Keywords

Logic Programming, Functional Logic Programming, Residuation, Abstract Interpretation

1 Introduction

Many proposals for the integration of functional and logic programming languages have been made during recent years (see [DL86] for a collection). From an operational point of view these proposals can be partitioned into two classes: approaches with a complete operational semantics and a nondeterministic search (narrowing) for solving equations with functional expressions (EQLOG [GM86], SLOG [Fri85], K-LEAF [BGL^{+}87], BABEL [MR92], ALF [Han90], among others), and approaches which try to avoid nondeterministic computations for functional expressions by reducing functional expressions only if the arguments are sufficiently instantiated (Funlog [SY86], Le Fun [AKLN87], LIFE [AK90], NUE-Prolog [Nai91], among others). The former approaches are complete under some well-defined conditions (e.g., canonicity of the axioms), i.e., they compute all answers which can be logically inferred from the given program. The price for this completeness is an increased search space since there may be several incomparable unifiers of two terms if these terms contain unevaluated functional expressions. The latter approaches try to avoid this nondeterminism in the unification process. In these approaches a term is reduced to normal form before it is unified with another term, i.e., functional expressions are evaluated (if possible) before unification. If a function cannot be evaluated because the arguments are not sufficiently instantiated, the unification cannot proceed. Instead of causing a failure, the evaluation of the function is delayed until the arguments will be instantiated. This mechanism is called residuation in Le Fun [AKLN87] and extended to constraint logic programming in [Smo91]. For instance, consider the following program (we write residuating logic programs in the usual Prolog syntax [CM87] but it is allowed to use arbitrary evaluable functions in terms):

   q :- p(X,Y,5), pick(X,Y).
   p(A,B,A+B).
   pick(2,3).

together with the goal “?- q”. After applying the first clause to the goal, the literals p(X,Y,5) and p(A,B,A+B) are unified. This binds A to X and B to Y, but the unification of X+Y and 5 is not successful since the arguments of the function call X+Y are not instantiated to numbers. Hence this unification causes the generation of the residuation X+Y=5 which will be proved (or disproved) if X and Y will be bound to ground terms. We proceed by proving the literal pick(X,Y) which binds X and Y to 2 and 3, respectively. As a consequence, the instantiated residuation 2+3=5 can be verified and therefore the entire goal has been proved.

The residuation principle seems to be preferable to the narrowing approaches since it preserves the deterministic nature of functions. However, it fails to compute all answers if functions are used in a logic programming manner. For instance, consider the function append for concatenating two lists. In a functional language with pattern-matching it can be defined by the following equations (we use the Prolog notation for lists):

   append([],   L) = L
   append([E|R],L) = [E|append(R,L)]

From a logic programming point of view we can compute the last element E of a given list L by solving the equation append(_,[E]) = L. Since the first argument of the left-hand side of this equation will never be instantiated, residuation fails to compute the last element with this

Current goal:  Current residuation:

   rev([a,b,c],R)  ∅
   a(LE1,[E1]) = [a,b,c], rev(LE1,LR1) ∅
   rev(LE1,LR1)                         a(LE1,[E1]) = [a,b,c]
   a(LE2,[E2]) = LE1, rev(LE2,LR2)      a(LE1,[E1]) = [a,b,c]
   rev(LE2,LR2)                         a(LE1,[E1]) = [a,b,c], a(LE2,[E2]) = LE1
   a(LE3,[E3]) = LE2, rev(LE3,LR3)      a(LE1,[E1]) = [a,b,c], a(LE2,[E2]) = LE1

⋯

Figure 1: Infinite derivation with the residuation principle (a(⋯) denotes append(⋯))

equation whereas narrowing computes the unique value for E [Han91]. Similarly, we can specify by the equation append(LE,[_]) = L a list LE which is the result of deleting the last element in the list L. Combining the specification of the last element and the rest of a list, we define the reversing of a list by the following clauses:

   rev([],[]).
   rev(L, [E|LR]) :- append(LE,[E]) = L, rev(LE,LR).

Now consider the goal “?- rev([a,b,c],R)”. Since the arguments of the calls to the function append are never instantiated to ground terms, the residuation principle cannot verify the corresponding residuation. Hence the answer R=[c,b,a] is not computed and there is an infinite derivation path using the residuation principle and applying the second clause infinitely many times (see Figure 1).^{1} On the other hand a functional-logic language based on the narrowing principle can solve this goal and has a finite search space [Han91]. Therefore we should use narrowing instead of residuation in this example.

The last example raises the important question whether it is possible to detect the cases where the (more efficient) residuation principle is able to compute all answers. If this would be possible we can avoid the nondeterministic and hence expensive narrowing principle in many cases and replace it by computations based on the residuation principle without loosing any answers. A simple criterion to the completeness of residuation is the groundness of all residuating variables: if at the end of a computation all variables occurring in residual function calls are bound to ground terms, then all residuations can be evaluated and hence the answer substitution does not depend on an unsolved residuation. Since the satisfaction of this criterion depends on the data flow during program execution, an exact answer is recursively undecidable. Therefore we present an approximation to this answer by applying an abstract interpretation technique to this kind of programs. Previous approaches for abstract interpretation of logic programs (see, for instance, [AH87, Bru91, Nil90]) depends on SLD-resolution as the operational semantics. Hence we cannot directly apply these frameworks to our case. However it is possible to develop a similar technique by considering unsolved residuations as part of the current substitution.

1A residual function call is only evaluated if all arguments are ground terms [AKLN87]. If we weaken this condition to “a residual function call is evaluated if the arguments are sufficiently instantiated” (as in [Nai91]), then we can also verify residuations like append([],[E])=[a]. In this case the answer to the goal “?- rev([a,b,c],R).” can be computed by incremental verification of residuations, but there is also an infinite derivation path using the second clause infinitely many times.

In the next section we give a detailed description of the operational semantics considered in this paper. The abstract domain and the abstract interpretation algorithm for reasoning about residuating programs is presented in Section 3. Finally, the correctness of our method is proved in Section 4.

2 The residuation principle

The residuation principle tries to avoid nondeterministic computations by delaying function calls until the arguments are sufficiently instantiated. The difference between residuating logic programs and ordinary logic programs shows up in the unification procedure: if a call to a defined function f(t_{1}, …, t_{n}) should be unified with a term t, the function call is evaluated if all arguments t_{1}, …, t_{n} are bound to ground terms and the unification proceeds with the evaluated term, otherwise the unification immediately succeeds and the residuation f(t_{1}, …, t_{n}) = t is added. If all variables in t_{1}, …, t_{n} will be bound to ground terms in the further computation process, the residuation f(t_{1}, …, t_{n}) = t will be immediately verified by evaluating the left-hand side and comparing the result with the right-hand side.

In residuating logic programs terms are built from variables, constructors and (defined) functions. Constructors (denoted by a, b, c, d) are used to compose data structures, while defined functions (denoted by f, g, h) are operations on these data structures. A constructor term is a term which does not contain functions, and a non-constructor term is a term containing at least one function call. A ground term is a term containing no variables. With this concept of terms that may contain function calls we adopt all standard notions of logic programming [Llo87] like clause, logic program, substitution etc.

We do not require any formalism for the specification of functions, i.e., they may be defined by equations or in a completely different language (external or predefined functions). However, the following conditions must be satisfied in order to reason about residuating logic programs:

1. A function call can be evaluated if all arguments are ground terms.

2. The result of the evaluation is a ground constructor term (containing only constructors) or an error message (i.e., the computation cannot proceed because of type errors, division by zero etc.).

The unification algorithm for residuating logic programs is described in Figure 2 by a set of transformation rules on term equations E in the style of Martelli and Montanari [MM82].^{2} In order to unify two terms t and t′, we transform the equation t = t′ until no more rules are applicable. In this case we yield the result fail or an equation set of the form

x_{1} = t_{1}, …, x_{k} = t_{k}, s_{1} = s′_{1}, …, s_{m} = s′_{m}

2There is one peculiarity in the unification algorithm in the presence of defined functions. If a variable X occurs in a term t inside a function call, then we cannot deduce the failure of the unification problem X = t due to the occur check. For instance, if id is the identity function, then the equation X = id(X) is valid for any value of X and hence we cannot deduce a failure. But in this case X cannot be further instantiated to a ground term and therefore the residuation X = id(X) will never be verified or disproved. Hence a failure is generated also in this case.

Clash:  \frac{c(t_{1}, …, t_{n}) = d(t′_{1}, …, t′_{m}), E}{fail} if c ≠ d or m ≠ n
Decompose:  \frac{c(t_{1}, …, t_{n}) = c(t′_{1}, …, t′_{n}), E}{t_{1} = t′_{1}, …, t_{n} = t′_{n}, E}
Delete:  \frac{X = X, E}{E}
Occur check: \frac{X = t, E}{fail}  if t ≠ X and X occurs in t

Instantiate:

\frac{X = t, E}{X = t, σ(E)}

if X occurs in E but not in t and σ = {X ↦ t}

Commute:  \frac{t = X, E}{X = t, E}  if t is not a variable

Evaluate-l: \frac{f(t_{1}, …, t_{n}) = t, E}{t′ = t, E} if t_{1}, …, t_{n} are ground and f(t_{1}, …, t_{n})

is evaluated to t′

Evaluate-r: \frac{t = f(t_{1}, …, t_{n}), E}{t = t′, E} if t_{1}, …, t_{n} are ground and f(t_{1}, …, t_{n})

is evaluated to t′

Figure 2: Unification algorithm for residuating logic programs

where each variable x_{i} does not occur in t_{j}, s_{j} or s′_{j}, and s_{i} or s′_{i} are unevaluable function calls (i = 1, …, m). In the latter case s_{i} = s′_{i} is called “residual equation” or simply “residuation” and we interpret the substitution/residuation pair ⟨σ, ρ⟩ with

σ = {x_{1} ↦ t_{1}, …, x_{k} ↦ t_{k}}
ρ = {s_{1} = s′_{1}, …, s_{m} = s′_{m}}

as the result of the unification. In the following we consider the elements s_{i} = s′_{i} of the residuation ρ as multisets {s_{i}, s′_{i}} in order to abstract from the “left” or “right” side of a residual equation (which is irrelevant in this context), i.e., we identify the residual equations s_{i} = s′_{i} and s′_{i} = s_{i}. In the entire computation σ is part of the answer substitution and ρ will be added to unifications in subsequent resolution steps. By giving priority to the evaluate rules we obtain the operational semantics of Le Fun [AKLN87] where residuations are immediately verified if all argument terms are ground.

The operational semantics of residuating logic programs considered in this paper is similar to Prolog’s operational semantics (SLD-resolution with leftmost selection rule) but with the difference that the standard unification is replaced by the unification described above. Hence the concrete domain of computation C is not simply the set of all substitutions but a set of substitution/residuation pairs, i.e.,

C = {⟨σ, ρ⟩ | σ is a substition, ρ is a set of residuations}

where a residuation is an equation (multiset) r = r′ and r or r′ is a function call. Since ground function calls are evaluated during unification, we assume in the following that all elements ⟨σ, ρ⟩ of the concrete domain C do not contain function calls with ground terms in the residuation part ρ. As an example consider the following residuating logic program:

   q :- p(X,Y,5), 1 = W-V, X = V*W, Y = V+W, pick(V,W).
   p(A,B,A+B).
   pick(1,2).

If the initial goal is q, then the following elements of the concrete domain are computed during the processing of the first clause:

Before “p(X,Y,5)”: ⟨∅, ∅⟩
After “p(X,Y,5)”: ⟨∅, {5 = X+Y}⟩

         After “1 = W-V”:  ⟨∅, {5 = X+Y, 1 = W-V}⟩
         After “X = V*W”:  ⟨{X ↦ V*W}, {5 = (V*W)+Y, 1 = W-V}⟩
         After “Y = V+W”:  ⟨{X ↦ V*W, Y ↦ V+W}, {5 = (V*W)+(V+W), 1 = W-V}⟩
         After “pick(V,W)”: ⟨{X ↦ 1*2, Y ↦ 1+2, V ↦ 1, W ↦ 2}, ∅⟩

At the clause end the residuation set is empty since all functions could be evaluated. Hence the initial goal is proved to be true.

3 Abstract interpretation of residuating logic programs

In this section we present a method for checking whether the residuation part of the answer to a goal is empty, i.e., whether the residuation principle is complete w.r.t. a given program and goal. Since this problem is recursively undecidable in general, we present an approximation to it based on a compile-time analysis of the program. If this approximation yields a positive answer, then it is ensured that all residuations can be solved at run time. In the following we present the abstract domain and the motivation for it. The relation to the concrete domain and the correctness of the abstract interpretation algorithm is discussed in Section 4 in more detail. We assume familiarity with basic ideas of abstract interpretation techniques [AH87].

3.1 Abstract domain

There has been done a lot of work concerning the compile-time derivation of run-time properties of logic programs (see, for instance, the collection [AH87]). Since we have abstracted the different operational behaviour of residuating logic programs into an additional component to the concrete domain, we can use the well-known frameworks (e.g., [Bru91, Nil90]) in a similar way. The heart of an abstract interpretation procedure is an abstract domain which approximates subsets of the concrete domain by finite representations. An element of the abstract domain describes common properties of a subset of the concrete domain. The properties must be chosen so that they contain relevant propositions about the interesting run-time properties. So what are the abstract properties in our case?

We are interested in unevaluated residuations at run time (second component of the concrete domain). A residuation can be verified if the function call in it can be evaluated. Since a function call can be evaluated if all arguments are ground, we need some information about the variables in it and the instantiation state of these variables in order to decide the emptiness of the residuation set. Hence our abstract domain contains information about the following properties:

Potential residuations: Residuations are generated by the unification of terms. For instance, if variable X is bound to A+B and variable Y is bound to 2 at run time, the unification of X and Y generates the residuation A+B=2. Hence, in order to state properties of all residuations which may occur at run time, we must know all potential function calls in the bindings of a variable. Moreover, we must also know the variables in this function call in order to decide whether or not this function call can be evaluated. Therefore our abstract domain contains elements of the form “X with +|{A,B}” meaning: variable X may be bound to a term containing a call to function + which can be evaluated if A and B are ground.

Dependencies between variables: Function calls can be evaluated if all variables in it are bound to ground terms. Hence we must have some information about the dependencies between variables. For instance, consider the goal

   ?- A+B = C,  C*2 = 6,  A = 1,  B = 2.

During unification of C*2 and 6 the first term cannot be evaluated since C is not ground. But the groundness of C depends on the groundness of A and B. Thus we can deduce that the function call C*2 can be evaluated if A and B are bound to ground terms. Hence our abstract domain contains the element “C if {A,B}”. In general, “X if V ” means that variable X is bound to a ground term if all variables in V are bound to ground terms.

Sharing between variables: The potential residuations can be copied between different variables

in the unification process. For instance, consider the goal

   ?- Z = c(X),  Y = f(A),  X = Y, . . .

After the unification of X and Y the variable Z contains the function call f(A). In order to manage correctly the potential residuations, we must store the information that Z and X share a term. Hence our abstract domain contains the element {X,Z} representing the sharing between X and Z.

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

Element: Meaning:

X if V

X is ground if all variables in the variable set V are ground

X with f|_{V} X may be bound to a term containing a call to f which can be evaluated if all

variables in V are ground

 f

there may be an unevaluated function call to f depending on arbitrary variables

{X,Y}

X and Y may share a term

Obviously, A is finite if the set of variables and function symbols is finite. Since we use only program variables and functions occurring in the program in the abstract domain, A is finite in case of a finite program. For convenience we simply write “X” instead of “X if ∅”. Hence an element “X” in an abstraction means that variable X is bound to a ground term if it does not contain any function call.

Given an abstraction A, a variable X is called function-free in A if A does not contain elements of the form “X with f|_{V} ” and “f”. In the subset of the concrete domain corresponding to A a function-free variable can only be interpreted as a term without unevaluable function calls (compare Section 4).

To present a simple description of the abstract interpretation algorithm, we will sometimes generate abstractions containing redundant information. The following normalization rules eliminate some redundancies in abstractions:

Normalization rules for abstractions:

A ∪ {Z, X if V ∪ {Z}} ⟶ A ∪ {Z, X if V } if Z is function-free in A
A ∪ {Z, X with f|_{V ∪{Z}}} ⟶ A ∪ {Z, X with f|_{V} } if Z is function-free in A
A ∪ {X with f|_{∅}}  ⟶ A
A ∪ {X if V_{1}, X if V_{2}} ⟶ A ∪ {X if V_{1}} if V_{1} ⊆ V_{2}
A ∪ {X, {X, Y }}  ⟶ A ∪ {X}

The additional condition in the first two rules ensures that Z is bound to a ground term containing no unevaluable function calls. We call an abstraction A normalized if none of these normalization rules is applicable to A. Later we will see that the normalization rules are invariant w.r.t. the concrete substitutions/residuations corresponding to abstractions. Therefore we can assume that we compute only with normalized abstractions in the abstract interpretation algorithm.

In order to keep the abstract interpretation algorithm simple, we assume that predicate calls and clause heads have the form p(X_{1}, …, X_{n}) where all X_{i} are distinct (similarly to the example in [Bru91]). All other literals in the clause bodies and goals have the form X = Y, X = c(Y_{1}, …, Y_{n}) or X = f(Y_{1}, …, Y_{n}). It is easy to see that every residuating logic program can be transformed into a flat residuating logic program satisfying the above restrictions without changing the answer behaviour. For instance, the residuating logic program

   q(T) :- p(X,Y,72), X = V-W, Y = V+W, pick(V,W).
   p(A,B,A*B).
   pick(9,3).

can be transformed into the following equivalent flat program:

   q(T) :- Z = 72,  p(X,Y,Z), X = V-W, Y = V+W, pick(V,W).
   p(A,B,C) :- C = A*B.
   pick(A,B) :- A = 9,  B = 3.

In the following we assume that all programs are in the required form.

3.2 The abstract interpretation algorithm

The abstract interpretation algorithm is based on several operations on the abstract domain. The first operation restricts an abstraction A to a set of variables W. It will be used in a predicate call to omit the information about variables not passed from the predicate call to the applied clause:

call restrict(⊥, W) = ⊥

call restrict(A, W) = {X ∈ A | X ∈ W }
∪ {X with f|_{V} ∈ A | {X} ∪ V ⊆ W }
∪ {f | f ∈ A or X with f|_{V} ∈ A with X ∈ W, V ⊈ W }
∪ {{X, Y } ∈ A | X, Y ∈ W }

The restriction operation for predicate calls transforms an abstraction element X with f|_{V} into the element f if the dependent variables are not contained in W, i.e., it is noted that there may be an unevaluated function call to f but the possible dependencies are too complex for the abstract analysis. Similarly, an abstraction element of the form X if V is passed to the clause only if V = ∅.^{3}

A similar operation is needed at the clause end to forget the abstract information about local clause variables. Hence we define:

exit restrict(⊥, W) = ⊥
exit restrict(A, W) = {X if V ∈ A | {X} ∪ V ⊆ W }
∪ {X with f|_{V} ∈ A | {X} ∪ V ⊆ W }
∪ {f | f ∈ A or X with f|_{V} ∈ A with {X} ∪ V ⊈ W }
∪ {{X, Y } ∈ A | X, Y ∈ W }

The restriction operation for clause exits transforms an abstraction element X with f|_{V} into the element f if one of the involved variables is not contained in W, i.e., it is noted that there may be an unevaluated function call to f which depends on local variables at the end of the clause.

The following operation computes the remaining abstract information of a predicate call restriction call restrict(A, W) in order to combine it after a predicate call:

rest(⊥, W) = ⊥
rest(A, W) = {X if V ∈ A | X ∉ W or V ≠ ∅}
∪ {X with f|_{V} ∈ A | X ∉ W }
∪ {{X, Y } ∈ A | X ∉ W or Y ∉ W }

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

⊥ ⊔ A = A
A ⊔ ⊥ = A
A_{1} ⊔ A_{2} = {X if V_{1} ∪ V_{2} | X if V_{1} ∈ A_{1}, X if V_{2} ∈ A_{2}}
∪ {X with f|_{V} | X with f|_{V} ∈ A_{1} or X with f|_{V} ∈ A_{2}}
∪ {f | f ∈ A_{1} or f ∈ A_{2}}
∪ {{X, Y } | {X, Y } ∈ A_{1} or {X, Y } ∈ A_{2}}

Now we are able to define the abstract unification algorithm for the abstract interpretation of equations occurring in clause bodies or goals. Abstract unification is a function amgu(α, t_{1}, t_{2}) which takes an element of the abstract domain α ∈ A and two terms t_{1}, t_{2} as input and produces another abstract domain element as the result. Because of our restrictions on goal equations, the following definition is sufficient:^{4}

3I conjecture that it is also possible to pass abstraction elements X if V to the clause if {X} ∪ V ⊆ W, but I could not prove the correctness of the abstract interpretation algorithm for this extension.

amgu(⊥, t_{1}, t_{2})  = ⊥
amgu(A, X, X)  = A
amgu(A, X, Y)  = closure(A ∪ {X if {Y }, Y if {X}, {X, Y }}) if X ≠ Y
amgu(A, X, c(Y_{1}, …, Y_{n})) = closure(A ∪ {X if {Y_{1}, …, Y_{n}}, Y_{1} if {X}, …, Y_{n} if {X},
{X, Y_{1}}, …, {X, Y_{n}}})
amgu(A, X, f(Y_{1}, …, Y_{n})) = closure(A ∪ {X if {Y_{1}, …, Y_{n}}, X with f|_{{Y_{1},...,Y_{n}}}})

In this definition and in the rest of this paper closure(A) denotes the least set A′ containing A which is closed under the following rules for transitivity and distribution of sharing information:

{X, Y } ∈ A′, {Y, Z} ∈ A′ ⟹ {X, Z} ∈ A′
{X, Y } ∈ A′, X with f|_{V} ∈ A′ ⟹ Y with f|_{V} ∈ A′

Now we can present the algorithm for the abstract interpretation of a residuating logic program in flat form. It is specified as a function ai(α, L) which takes an abstract domain element α and a goal literal L and yields a new abstract domain element as result. Clearly, ai(⊥, L) =⊥ and ai(A, t = t′) = amgu(A, t, t′). The interesting case is the abstract interpretation of a predicate call ai(A, p(X_{1}, …, X_{n})) which is computed by the following steps:

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

A_{0} = ⟨replace all X_{i} by Z_{i} in A_{call}⟩

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

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

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

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

4For simplicity we omit the occur check in the abstract unification.

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

3.3 An example

The following example is the flat form of a Le Fun program presented in [AKLN87]:

   q(Z) :- p(X,Y,Z), X = V-W, Y = V+W, pick(V,W).
   p(A,B,C) :- C = A*B.
   pick(A,B) :- A = 9,  B = 3.

The abstract interpretation algorithm computes the following abstractions w.r.t. the initial goal q(T) and the initial abstraction ∅ (specifying the set of all substitutions without unevaluated function calls):

ai(∅, q(T)):

      ai(∅, p(X,Y,Z)):

                    ai(∅, C = A*B) = {C if {A,B}, C with *|{A,B}}
      ai(∅, p(X,Y,Z)) = {Z if {X,Y}, Z with *|{X,Y}} =: A_{1}

      ai(A_{1}, X = V-W) = {Z if {X,Y}, X if {V,W}, Z with *|{X,Y}, X with -|{V,W}} =: A_{2}

      ai(A_{2}, Y = V+W) = {Z if {X,Y}, X if {V,W}, Y if {V,W},

                        Z with *|{X,Y}, X with -|{V,W}, Y with +|{V,W}} =: A_{3}

      ai(A_{3}, pick(V,W)):

ai(∅, A = 9) = {A} ai({A}, B = 3) = {A, B}

      ai(A_{3}, pick(V,W)) = {V, W, Z if {X,Y}, X if {V,W}, Y if {V,W},

                          Z with *|{X,Y}, X with -|{V,W}, Y with +|{V,W}}

⟶^{normalize} {V, W, Z, X, Y}

ai(∅, q(T)) = {T} Hence the computed success abstraction is {T} meaning that after a successful computation of the goal q(T) the variable T is bound to a ground term and the residuation set is empty, i.e., the residuation principle allows to compute a fully evaluated answer. Similarly, the completeness of the residuation principle can be proved by our algorithm for all other residuating logic programs presented in [AKLN87].

4 Correctness of the abstract interpretation algorithm

In this section we will prove the correctness of the presented abstract interpretation algorithm. Firstly, we relate the abstract domain to the concrete domain by defining a concretisation function. Then we will prove that the abstract operations defined in the previous section are correct w.r.t. the corresponding operations on the concrete domain. Finally, we obtain the correctness of our algorithm by simply applying Bruynooghe’s framework [Bru91].

4.1 Relating abstractions to concrete values

To relate the computed abstract properties of the program to the concrete run-time behaviour, we have to define a concretisation function γ:A → 2^{C} which maps an abstraction into a subset of the concrete domain. The most difficult point in the definition of γ is the correct interpretation of an abstraction “X if V ”. The intuitive meaning is “the interpretation of X is ground if all interpretations of V are ground”. To be more precise, “X if V ” describes a dependency between the instantiation of X and the instantiation of the variables in V, i.e., we could define:

(*) If Xif V ∈ A and ⟨σ, ρ⟩ ∈ γ(A), then var(σ(X)) ⊆ var(σ(V)).

(var(ξ) denotes the set of all variables occurring in the syntactic construction ξ) Such a definition seems to justify the generation of the abstractions “X if {Y}” and “Y if {X}” in the abstract unification algorithm if X is unified with Y. But this interpretation is not true if X or Y are bound to terms containing unevaluated residuations. E.g., if X is bound to f(B) and Y is bound to c(A) during program execution, then the computation of the literal X=Y yields the substitution/residuation pair ⟨∅, {f(B)=c(A)}⟩. Thus the variables contained in the bindings of X and Y are not identical after the unification step. Therefore we must weaken (*) to the condition that only the variables of σ(X) occurring outside function calls are contained in the variables of σ(V) w.r.t. to the residuation ρ.

To give a precise description of the condition, we need the following definitions. By lvar(t) we denote the set of all variables occurring outside function calls in the term t (in subsequent proofs we say “l-variable” for variables belonging to this set):

lvar(X) = {X}
lvar(c(t_{1}, …, t_{n})) = lvar(t_{1}) ∪ ⋯ ∪ lvar(t_{n})
lvar(f(t_{1}, …, t_{n})) = ∅

The extension of a set of variables V w.r.t. to the residuation ρ is defined by

var_{ρ}(V) = V ∪ \{lvar(e) | f(\overline{t}) = e ∈ ρ with var(\overline{t}) ⊆ V \}

(where \overline{t} denotes the argument sequence t_{1}, …, t_{n}). Note that var_{ρ}(∅) = ∅ if ρ does not contain unevaluated ground residual function calls (which do not occur in our concrete domain) and for an empty residuation we have var_{∅}(V) = V. The intuition of this definition is that we add to a set of variables V all these variables which will be ground during the computation process if all variables in V are ground. For instance, if ρ = {f(X)=c(Y), f(X)=c(Z)}, then var_{ρ}({X}) = {X, Y, Z}. We extend the function var_{ρ} to terms by

var_{ρ}(t) = var_{ρ}(var(t))

and to finite sets of terms by

var_{ρ}({t_{1}, …, t_{k}}) = var_{ρ}(var({t_{1}, …, t_{k}}))

Since we are interested in the property whether a function call occurring in a term can be completely evaluated, it is sufficient to look at the main function calls and not at function calls which occur inside other function calls (this is due to the fact that a unification between a function call and another term does not bind any variables in this call). Therefore we say a term t occurs directly in a term t′ if t occurs in t′ outside a function call. For instance, the term X + (Y ∗ 2) occurs directly in the term c(X + (Y ∗ 2)) but the subterm (Y ∗ 2) is not a direct occurrence.

Now we are able to define the semantics of abstractions by the concretisation function γ:A → 2^{C} (where \overline{t} denotes the argument sequence t_{1}, …, t_{n}):

γ(⊥) = ∅
γ(A) = {⟨σ, ρ⟩ ∈ C | 1. X if V ∈ A ⇒ lvar(σ(X)) ⊆ var_{ρ}(σ(V))
2. f(\overline{t}) occurs directly in σ(X) or ρ with var(\overline{t}) ≠ ∅
⇒ f ∈ A or var(\overline{t}) ⊆ var(σ(V)) for some X with f|_{V} ∈ A

3. lvar(σ(X)) ∩ lvar(σ(Y)) ≠ ∅ for variables X ≠ Y ⇒ {X, Y } ∈ A }

In the following we say a substitution/residuation pair ⟨σ, ρ⟩ satisfies the variable condition X if V ∈ A if condition 1 holds. Similarly, we say an occurrence f(\overline{t}) in σ(X) or ρ is covered by A if condition 2 holds.

Condition 1 implies for X if V ∈ A that all l-variables of the current instantiation of X are ground if all variables in V are instantiated to ground terms. Condition 2 ensures that all unevaluated function calls in variable bindings and in residuations are contained in A. Since we are interested in potential residuations, it is sufficient to look at function calls which occur directly in some variable binding (and not at function calls nested in other function calls). Hence the sharing information is also restricted to lvar instead of var (condition 3). Note that for an unevaluated function call in the residuation part it is sufficient that there is an arbitrary variable X which cover this function call whereas for an unevaluated function call in the binding of a variable X there must be an abstraction element X with f|_{V} with the same variable. This is necessary for passing the correct information about potential residuations in case of a predicate call (compare call restriction operation).

From this interpretation it is clear that an abstraction without elements of the form “X with f|_{V} ” or “f” can only be interpreted as a fully evaluated pair ⟨σ, ρ⟩ if ρ = ∅ and σ does not contain unevaluable function calls. This argument has been used to state the completeness of the example in Section 3.3.

Due to this semantics of abstractions it can be proved that the normalization rules defined on abstractions in Section 3.1 are invariant w.r.t. the concrete interpretation. The following lemma justifies the application of the normalization rules.

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

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

1. Let A = A_{0} ∪ {Z, X if V ∪ {Z}}, A′ = A_{0} ∪ {Z, X if V } and Z be function-free in A_{0}. Since the only difference between A and A′ is the transformation of “X if V ∪ {Z}” into “X if V ”, we have to show lvar(σ(X)) ⊆ var_{ρ}(σ(V)). Since ⟨σ, ρ⟩ ∈ γ(A), lvar(σ(Z)) = ∅ and lvar(σ(X)) ⊆ var_{ρ}(σ(V ∪ {Z})). σ(Z) is a ground term because Z is function-free in A_{0}. Hence lvar(σ(X)) ⊆ var_{ρ}(σ(V ∪ {Z})) = var_{ρ}(σ(V)).

2. Let A = A_{0} ∪{Z, X with f|_{V ∪{Z}}}, A′ = A_{0} ∪{Z, X with f|_{V} } and Z be function-free in A_{0}. Since only the abstraction element X with f|_{V ∪{Z}} is affected by this transformation, we have to show: if f(\overline{t}) occurs directly in σ(X) or ρ with var(\overline{t}) ≠ ∅ and var(\overline{t}) ⊆ var(σ(V ∪ \{Z\})), then var(\overline{t}) ⊆ var(σ(V)). Since ⟨σ, ρ⟩ ∈ γ(A), var(σ(Z)) = lvar(σ(Z)) = ∅ (as in the previous case). Hence var(\overline{t}) ⊆ var(σ(V ∪ \{Z\})) = var(σ(V)).

3. Let A = A′ ∪ {X with f|_{∅}}. If the abstraction element X with f|_{∅} was a relevant condition for ⟨σ, ρ⟩ ∈ γ(A), then f(\overline{t}) occurs directly in σ(X) or ρ with var(\overline{t}) ⊆ ∅. Hence f(\overline{t}) is a ground function call which need not be covered by A′.

4. Let A = A_{0} ∪{X if V_{1}, X if V_{2}}, A′ = A_{0} ∪{X if V_{1}} and V_{1} ⊆ V_{2}. Obviously, ⟨σ, ρ⟩ ∈ γ(A′) since the variable condition X if V_{2} is omitted in A′.

5. Let A = A_{0} ∪ {X, {X, Y }} and A′ = A_{0} ∪ {X}. If the abstraction element {X, Y } was a relevant condition for ⟨σ, ρ⟩ ∈ γ(A), then lvar(σ(X)) ∩ lvar(σ(Y)) ≠ ∅. But this case cannot occur since lvar(σ(X)) = ∅.

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

1. Let A = A_{0} ∪ {Z, X if V ∪ {Z}} and A′ = A_{0} ∪ {Z, X if V }. Since ⟨σ, ρ⟩ ∈ γ(A′), lvar(σ(X)) ⊆ var_{ρ}(σ(V)) ⊆ var_{ρ}(σ(V ∪ {Z})). Hence ⟨σ, ρ⟩ ∈ γ(A) because “X if V ∪ {Z}” is the only altered abstraction element.

2. Let A = A_{0} ∪ {Z, X with f|_{V ∪{Z}}} and A′ = A_{0} ∪ {Z, X with f|_{V} }. Similarly to the first case.

3. Let A = A′ ∪ {X with f|_{∅}}. This case is trivial since A contains the additional abstraction element “X with f|_{∅}”.

4. Let A = A_{0} ∪ {X if V_{1}, X if V_{2}}, A′ = A_{0} ∪ {X if V_{1}} and V_{1} ⊆ V_{2}. We have to show lvar(σ(X)) ⊆ var_{ρ}(σ(V_{2})). But this is trival because ⟨σ, ρ⟩ ∈ γ(A′) implies lvar(σ(X)) ⊆ var_{ρ}(σ(V_{1})) ⊆ var_{ρ}(σ(V_{2})).

5. Let A = A_{0} ∪ {X, {X, Y }} and A′ = A_{0} ∪ {X}. This case is trivial since A contains the additional abstraction element “{X, Y }”.

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

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

(a) ⊥⊑ α for all α ∈ A
(b) A ⊑ A′ ⟺ 1. X if V′ ∈ A′ ⇒ ∃V ⊆ V′ with X if V ∈ A
2. X with f|_{V} ∈ A ⇒ X with f|_{V} ∈ A′
3. f ∈ A ⇒ f ∈ A′
4. {X, Y } ∈ A ⇒ {X, Y } ∈ A′

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

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

Proof: If A_{1} =⊥ or A_{2} =⊥, then obviously A_{1} ⊔ A_{2} is a least upper bound of A_{1} and A_{2}. Therefore we assume A_{1} ≠⊥ and A_{2} ≠⊥.

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

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

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

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

Proof: Let A ⊑ A′ and ⟨σ, ρ⟩ ∈ γ(A). (the case A =⊥ is trivial). We have to show ⟨σ, ρ⟩ ∈ γ(A′).

Let X if V′ ∈ A′. Since A ⊑ A′, there is a set V ⊆ V′ with X if V ∈ A. Since ⟨σ, ρ⟩ ∈ γ(A), lvar(σ(X)) ⊆ var_{ρ}(σ(V)) ⊆ var_{ρ}(σ(V′)). Hence ⟨σ, ρ⟩ satisfies X if V′.

If f(\overline{t}) occurs directly in σ(X) or ρ with var(\overline{t}) ≠ ∅, then f ∈ A or var(\overline{t}) ⊆ var(σ(V)) for some X with f|_{V} ∈ A. These abstraction elements are also contained in A′ in both cases (by definition of ⊑).

If lvar(σ(X))∩lvar(σ(Y)) ≠ ∅ for variables X ≠ Y, then {X, Y } ∈ A. This implies {X, Y } ∈ A′ by definition of ⊑.

It is also not difficult to show that all abstract operations defined in Section 3.2 (restriction, remainder, abstract unification etc.) are monotone. As an example we show the monotonicity of the restriction operation for clause entries.

Lemma 4.4 The abstract operation call restrict is monotone.

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

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

1. X if V ∈ A′_{2}: By definition of call restrict, V = ∅, X ∈ A_{2} and X ∈ W. Since A_{1} ⊑ A_{2}, X ∈ A_{1} which immediately implies X ∈ A′_{1}.

2. X with f|_{V} ∈ A′_{1}: By definition of call restrict, X with f|_{V} ∈ A_{1} and {X} ∪ V ⊆ W. This implies X with f|_{V} ∈ A_{2} and thus X with f|_{V} ∈ A′_{2}.

3. f ∈ A′_{1}: By definition of call restrict, either f ∈ A_{1} which implies f ∈ A_{2} and f ∈ A′_{2}, or X with f|_{V} ∈ A_{1} with X ∈ W and V ⊈ W. The latter case implies X with f|_{V} ∈ A_{2} and f ∈ A′_{2}.

4. {X, Y } ∈ A′_{1}: By definition of call restrict, {X, Y } ∈ A_{1} and X, Y ∈ W. Hence {X, Y } ∈ A_{2} and therefore {X, Y } ∈ A′_{2}.

4.2 Correctness of abstract operations

Following the framework presented in [Bru91], the correctness of the abstract interpretation algorithm can be proved by showing the correctness of each basic operation of the algorithm (like abstract unification, clause entry and clause exit). Correctness means in this context that all concrete computations, i.e., the results of the concrete clause entry, clause exit and unification (cf. Section 2), are subsumed by the abstractions computed by the corresponding abstract operations. In this section we will prove the correctness of each of these operations. In the following we use standard notions and notations from term rewriting [DJ90]. For instance, a position π in a term t is a sequence of natural numbers denoting the path from the root symbol to this term position, and t|_{π} denotes the subterm of t at position π.

First we prove that the abstract unification operation covers all possible concrete unifiers. For this purpose we need several propositions. A unifier of two terms containing function calls does not make these terms identical (due to the residuations), but the following lemma states a relationship between the variables of the unified terms.

Lemma 4.5 If t_{1} and t_{2} are terms and ⟨σ, ρ⟩ is a unifier computed by the rules of Figure 2, then lvar(σ(t_{1})) ⊆ var_{ρ}(σ(t_{2})).

Proof: We prove the lemma by analysing different subterms of σ(t_{1}) and σ(t_{2}) which contain variables of lvar(σ(t_{1})). Let σ(t_{1})|_{π} be a subterm of σ(t_{1}) which is not inside a function call so that σ(t_{1})|_{π} and σ(t_{2})|_{π} have different root symbols and π is minimal with this property. If σ(t_{1})|_{π} is a function call, then the variables in this subterm do not count for lvar(σ(t_{1})). If σ(t_{1})|_{π} is not a function call, then σ(t_{2})|_{π} must be a function call (otherwise these subterms have identical root symbols after successful unification) and σ(t_{2})|_{π} can be evaluated to σ(t_{1})|_{π} (in this case σ(t_{1})|_{π} is a ground term) or σ(t_{1})|_{π} = σ(t_{2})|_{π} ∈ ρ. In the latter case lvar(σ(t_{1})|_{π}) ⊆ var_{ρ}(σ(t_{2})|_{π}) by definition of var_{ρ}.

Next we want to characterize the effect of a substitution with respect to the extension var_{ρ} of a variable set.

Lemma 4.6 If X ∈ var_{ρ}(t) and σ is a substitution, then lvar(σ(X)) ⊆ var_{σ(ρ)}(σ(t)).

Proof: Since var_{ρ}(t) = var(t) ∪ \{lvar(e) | f(\overline{t}) = e ∈ ρ with var(\overline{t}) ⊆ var(t)\}, there are two cases if X ∈ var_{ρ}(t):

1. X ∈ var(t): Then lvar(σ(X)) ⊆ var(σ(X)) ⊆ var(σ(t)) ⊆ var_{σ(ρ)}(σ(t)).

2. X ∈ lvar(e) for some f(\overline{t}) = e ∈ ρ with var(\overline{t}) ⊆ var(t): Then var(σ(\overline{t})) ⊆ var(σ(t)). Hence lvar(σ(X)) ⊆ lvar(σ(e)) ⊆ var_{σ(ρ)}(σ(t)).

The following lemma extends the previous lemma to terms:

Lemma 4.7 If t_{1} and t_{2} are terms with lvar(t_{1}) ⊆ var_{ρ}(t_{2}) and σ is a substitution, then lvar(σ(t_{1})) ⊆ var_{σ(ρ)}(σ(t_{2})).

Proof: Let X ∈ lvar(σ(t_{1})). Then there is a variable Y ∈ lvar(t_{1}) with X ∈ lvar(σ(Y)). Condition lvar(t_{1}) ⊆ var_{ρ}(t_{2}) implies Y ∈ var_{ρ}(t_{2}). By the previous lemma, lvar(σ(Y)) ⊆ var_{σ(ρ)}(σ(t_{2})). Therefore X ∈ var_{σ(ρ)}(σ(t_{2})).

Now we are able to prove the correctness of the abstract unification operation. Correctness means that abstract unification is consistent with concrete unification in the following sense:

If ⟨σ, ρ⟩ ∈ γ(A) is the current substitution/residuation pair during program execution and the execution of the literal t_{1} = t_{2} yields the new substitution/residuation pair ⟨σ′ ∘ σ, ρ′⟩, then this new substitution/residuation pair is covered by the abstraction computed by abstract unification, i.e., ⟨σ′ ∘ σ, ρ′⟩ ∈ γ(amgu(A, t_{1}, t_{2})).

Execution of the literal t_{1} = t_{2} means applying the rules of Figure 2 to the equations ρ ∪ {σ(t_{1}) = σ(t_{2})\}. In order to simplify the proof, we state a result for the unifier ⟨\overline{σ}, \overline{ρ}⟩ of the single equation \{σ(t_{1}) = σ(t_{2})\}, i.e., we show ⟨\overline{σ} ∘ σ, \overline{ρ} ∪ \overline{σ}(ρ)⟩ ∈ γ(amgu(A, t_{1}, t_{2})). The difference between ⟨\overline{σ}∘σ, \overline{ρ}∪\overline{σ}(ρ)⟩ and ⟨σ′ ∘σ, ρ′⟩ is that some variables in \overline{σ}(ρ) are bound to ground terms by ⟨σ′ ∘σ, ρ′⟩ (since the original computation considers also the residuations in ρ which may be evaluated to ground constructor terms and thus binds variables of the other side of the equation) and ρ′ may contain less residuations than \overline{ρ}∪\overline{σ}(ρ). But this difference causes no problem since ⟨\overline{σ}∘σ, \overline{ρ}∪\overline{σ}(ρ)⟩ ∈ γ(A′) implies ⟨σ′ ∘ σ, ρ′⟩ ∈ γ(A′). This can be seen by the following two obvious propositions:

Proposition 4.8 If A is an abstraction, ⟨σ, ρ⟩ ∈ γ(A) and σ′ a substitution which maps all variables X with σ(X) ≠ X into ground constructor terms, then ⟨σ′ ∘ σ, σ′(ρ)⟩ ∈ γ(A).

Proposition 4.9 If A is an abstraction, ⟨σ, ρ⟩ ∈ γ(A) and ρ′ ⊆ ρ where the residuations from ρ − ρ′ do not contain variables, then ⟨σ, ρ′⟩ ∈ γ(A).

Due to this argument we prove in the following correctness theorems all results w.r.t. unifiers which do not consider the current residuation ρ. The following theorem states the correctness of the abstract unification in this sense.

Theorem 4.10 (Correctness of abstract unification) Let X be a variable, t be a term of the form t = Y, t = c(Y_{1}, …, Y_{n}) or t = f(Y_{1}, …, Y_{n}) and A be an abstraction. Then for all ⟨σ, ρ⟩ ∈ γ(A) and all unifiers ⟨σ′, ρ′⟩ for σ(X) and σ(t) computed by the rules of Figure 2, ⟨σ′ ∘ σ, ρ′ ∪ σ′(ρ)⟩ ∈ γ(amgu(A, X, t)).

Proof: Let A, ⟨σ, ρ⟩ and ⟨σ′, ρ′⟩ be given as described above. We prove the theorem for each of the three cases for t. Let t = Y (≠ X, otherwise the theorem is trivially true). Then

A′ := amgu(A, X, Y) = closure(A ∪ {X if {Y }, Y if {X}, {X, Y }})

We have to show: ⟨σ′ ∘ σ, ρ′ ∪ σ′(ρ)⟩ ∈ γ(A′).

1. X if {Y } ∈ A′: Since ⟨σ′, ρ′⟩ is a unifier for σ(X) and σ(Y), Lemma 4.5 yields

lvar(σ′(σ(X))) ⊆ var_{ρ′}(σ′(σ(Y))) ⊆ var_{ρ′∪σ′(ρ)}(σ′(σ(Y))).

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

3. Z if V ∈ A′ ∩ A: Since ⟨σ, ρ⟩ ∈ γ(A), lvar(σ(Z)) ⊆ var_{ρ}(σ(V)). The straightforward extension of Lemma 4.7 to sets of terms yields

lvar(σ′(σ(Z))) ⊆ var_{σ′(ρ)}(σ′(σ(V))) ⊆ var_{ρ′∪σ′(ρ)}(σ′(σ(V))).

Hence all variable conditions of A′ are satisfied by ⟨σ′ ∘ σ, ρ′ ∪ σ′(ρ)⟩.

4. f(\overline{t}) occurs directly in σ′(σ(Z)) with var(\overline{t}) ≠ ∅ (for an arbitrary variable Z):

First we assume that f(\overline{t}) occurs in a position also present in σ(Z), i.e., there is a position π with σ′(σ(Z))|_{π} = f(\overline{t}), σ(Z)|_{π} = f(\overline{s}) and σ′(\overline{s}) = \overline{t}. Since ⟨σ, ρ⟩ ∈ γ(A) and f(\overline{s}) occurs directly in σ(Z), f ∈ A (which implies f ∈ A′) or var(\overline{s}) ⊆ var(σ(V)) for some Z with f|_{V} ∈ A. The latter case implies var(\overline{t}) = var(σ′(\overline{s})) ⊆ var(σ′(σ(V))) for Z with f|_{V} ∈ A′. Otherwise we assume that f(\overline{t}) occurs directly in σ′(σ(Z)) but not in σ(Z), i.e., there is a position π with σ′(σ(Z))|_{π} = f(\overline{t}) but σ(Z)|_{π} is undefined or a variable. In this case σ(Z) must contain a variable which is instantiated by the unifier ⟨σ′, ρ′⟩ to a non-constructor term. Since a unifier computed by the rules of Figure 2 binds only l-variables in σ(X) and σ(Y) to non-constructor terms, σ(Z) must share a l-variable with σ(X) or σ(Y) (for simplicity we consider only the case for σ(X) in the following), i.e., {Z, X} ∈ A and σ′(σ(X)) have also a direct occurrence of the subterm f(\overline{t}). Since new function calls are not created by the rules of Figure 2, there must exist a subterm f(\overline{s}) of an instantiated variable σ(Z′) with σ′(\overline{s}) = \overline{t}. Moreover, σ(Z′) and σ(X) (or σ(Y)) share a l-variable (which contains the function call f(\overline{t}) in σ′). Hence, because of ⟨σ, ρ⟩ ∈ γ(A), {Z′, X}(or {Z′, Y }) ∈ A and f ∈ A (which immediately implies f ∈ A′) or var(\overline{s}) ⊆ var(σ(V)) for some Z′ with f|_{V} ∈ A. In the latter case we have X with f|_{V} ∈ A′ and also Z with f|_{V} ∈ A′ (since A′ is closed under the distribution of sharing information) where var(\overline{t}) = var(σ′(\overline{s})) ⊆ var(σ′(σ(V))). Hence the occurrence of f(\overline{t}) in σ′(σ(Z)) is covered by A′.

5. f(\overline{t}) occurs directly in σ′(ρ) ∪ ρ′ with var(\overline{t}) ≠ ∅ but does not occur directly in σ′(σ(Z)) for any variable Z:

• f(\overline{t}) belongs to σ′(ρ): Since f(\overline{t}) does not occur in σ′(σ(Z)) for any Z, this function call is not contained in the image of σ′ and therefore there exists a residual function call f(\overline{s}) in ρ with σ′(\overline{s}) = \overline{t}. Since var(\overline{s}) ≠ ∅ and ⟨σ, ρ⟩ ∈ γ(A), f ∈ A or var(\overline{s}) ⊆ var(σ(V)) for some Z with f|_{V} ∈ A. Thus f ∈ A′ or var(\overline{t}) = var(σ′(\overline{s})) ⊆ var(σ′(σ(V))) for Z with f|_{V} ∈ A′.

• f(\overline{t}) belongs to ρ′: Since ρ′ is generated during unification of σ(X) and σ(Y), there is a subterm f(\overline{s}) of σ(X) or σ(Y) with σ′(\overline{s}) = \overline{t}, i.e., f(\overline{t}) occurs in σ′(σ(X)) or σ′(σ(Y)) which contradicts our assumption. Thus this case cannot occur.

Therefore every residual function call in σ′(ρ) ∪ ρ′ is covered by A′.

6. lvar(σ′(σ(Z))) ∩ lvar(σ′(σ(Z′))) ≠ ∅ for variables Z ≠ Z′:

If lvar(σ(Z)) ∩ lvar(σ(Z′)) ≠ ∅, then {Z, Z′} ∈ A and thus {Z, Z′} ∈ A′. Otherwise we assume lvar(σ(Z)) ∩ lvar(σ(Z′)) = ∅. Since σ′ instantiates only l-variables of σ(X) and σ(Y) to non-ground terms, σ(Z), σ(Z′) and σ(X), σ(Y) must share l-variables. Hence (in the worst case) {Z, X}, {Z′, Y } ∈ A which implies by definition of A′ (closure property) {Z, Z′} ∈ A′.

Altogether we have shown that ⟨σ′ ∘ σ, ρ′ ∪ σ′(ρ)⟩ ∈ γ(A′) for the case t = Y. Next we consider the case t = c(Y_{1}, …, Y_{n}). Then

\begin{aligned}A := amgu(A, X, c(Y_{1}, …, Y_{n})) & = & closure(A ∪ \{X if \{Y_{1}, …, Y_{n}\}, Y_{1} if \{X\}, …, Y_{n} if \{X\}, \\ & & \{X, Y_{1}\}, …, \{X, Y_{n}\}\}) \end{aligned}

1. X if {Y_{1}, …, Y_{n}} ∈ A′: Since ⟨σ′, ρ′⟩ is a unifier for σ(X) and σ(t), Lemma 4.5 yields

lvar(σ′(σ(X))) ⊆ var_{ρ′}(σ′(σ(t))) ⊆ var_{ρ′∪σ′(ρ)}(σ′(σ(t))) = var_{ρ′∪σ′(ρ)}(σ′(σ({Y_{1}, …, Y_{n}}))).

2. Y_{i} if {X} ∈ A′: Similarly to the previous case, Lemma 4.5 yields lvar(σ′(σ(t))) ⊆ var_{ρ′∪σ′(ρ)}(σ′(σ(X))). Since lvar(σ′(σ(Y_{i}))) ⊆ lvar(σ′(σ(t))), we obtain

lvar(σ′(σ(Y_{i}))) ⊆ var_{ρ′∪σ′(ρ)}(σ′(σ(X))).

3. Z if V ∈ A′ ∩ A: This is identical to the corresponding case of “t = Y ” (see above). Therefore all variable conditions of A′ are satisfied by ⟨σ′ ∘ σ, ρ′ ∪ σ′(ρ)⟩.

4. f(\overline{t}) occurs directly in σ′(σ(Z)) or in the residuation σ′(ρ)∪ρ′ with var(\overline{t}) ≠ ∅: This is similar to the corresponding cases of “t = Y ” with the difference that sometimes we have to replace “Y ” by “some Y_{i}” in the proof.

5. lvar(σ′(σ(Z))) ∩ lvar(σ′(σ(Z′))) ≠ ∅ for variables Z ≠ Z′: Let lvar(σ(Z)) ∩ lvar(σ(Z′)) = ∅ (otherwise we proceed as in case “t = Y ”). Since σ′ instantiates only l-variables of σ(X) and σ(c(Y_{1}, …, Y_{n})) to non-ground terms, σ(Z) and σ(Z′) must share l-variables with σ(X) and σ(c(Y_{1}, …, Y_{n})). By ⟨σ, ρ⟩ ∈ γ(A) and the closure property of A′ we obtain {Z, Z′} ∈ A′.

Hence we have proved the theorem for the case t = c(Y_{1}, …, Y_{n}). Next we consider the case t = f(Y_{1}, …, Y_{n}). Then

A := amgu(A, X, f(Y_{1}, …, Y_{n})) = closure(A ∪ {X if {Y_{1}, …, Y_{n}}, X with f|_{{Y_{1},...,Y_{n}}}})

1. X if {Y_{1}, …, Y_{n}} ∈ A′:

If σ(t) is a ground term, then the function call σ(t) evaluates to a ground term which is unified with σ(X), i.e., all l-variables of σ(X) are bound to ground terms. Hence lvar(σ′(σ(X))) = ∅. If σ(t) is not a ground term, then the function call σ(t) delays or is bound to σ(X), i.e., there are the following two cases:

• If σ(X) is not a variable, then σ′ = ∅ and ρ′ = {σ(X) = σ(t)}. Hence lvar(σ′(σ(X))) = lvar(σ(X)) ⊆ var_{ρ′}(σ(t)) ⊆ var_{ρ′∪ρ}(σ(t)) = var_{ρ′∪σ′(ρ)}(σ′(σ({Y_{1}, …, Y_{n}}))).

• If σ(X) is a variable, then σ′ = {σ(X) ↦ σ(t)} and ρ′ = ∅. Hence lvar(σ′(σ(X))) = lvar(σ(t)) = ∅ ⊆ var_{ρ′∪σ′(ρ)}(σ′(σ({Y_{1}, …, Y_{n}}))).

2. Z if V ∈ A′ ∩ A: This is identical to the corresponding case of “t = Y ” (see above).

3. f(\overline{t}) occurs directly in σ′(σ(Z)) or in the residuation σ′(ρ) ∪ ρ′ with var(\overline{t}) ≠ ∅: We assume that f(\overline{t}) is a “new” residual function call introduced by this unification, i.e., f(\overline{t}) = σ′(σ(f(Y_{1}, …, Y_{n}))) (otherwise we proceed as in case “t = Y ”). But this function call is covered by A′ since X with f|_{\{Y_{1},...,Y_{n}\}} ∈ A′, var(\overline{t}) = var(σ′(σ(\{Y_{1}, …, Y_{n}\}))) and the closure property of A′.

4. lvar(σ′(σ(Z))) ∩ lvar(σ′(σ(Z′))) ≠ ∅ for variables Z ≠ Z′: Let lvar(σ(Z)) ∩ lvar(σ(Z′)) = ∅ (otherwise we proceed as in case “t = Y ”). Then σ(X) must be a variable and thus σ′ = {σ(X) ↦ σ(t)}. Therefore σ′ may only delete occurrences of σ(X) from the l-variables but does not add new l-variables in any term, i.e., lvar(σ′(σ(Z))) ∩ lvar(σ′(σ(Z′))) = ∅. By this contradiction we infer that this case cannot occur.

Next we want to prove that the abstract operations performed at the entry of a clause are correct w.r.t. the concrete semantics. Hence we must show something like:

If P is a predicate call with abstraction A, ⟨σ, ρ⟩ ∈ γ(A), L:- L1, …, L_{k} is a variant of a clause and ⟨σ′, ρ′⟩ is a unifier for σ(P) and L, then ⟨σ′ ∘ σ, ρ′ ∪ σ′(ρ)⟩ ∈ γ(A_{0}) where A_{0} is the abstraction computed for the clause L:- L1, …, L_{k} by the abstract interpretation algorithm ai.

However, this statement is too strong and not true in general since A_{0} contains only properties of variables occurring in the clause L:- L_{1}, …, L_{k}. Bruynooghe [Bru91] has shown that it is sufficient to prove that the call substitution restricted to the clause variables is contained in the computed call abstraction. Hence in our case it is sufficient that ⟨σ′ ∘ σ|_{W} , ρ′⟩ ∈ γ(A_{0}) where W is the set of all clause variables and the restriction of a substitution ϕ to a variable set V is defined by

ϕ|_{V} := {X ↦ t ∈ ϕ | X ∈ V }

Strictly speaking we have omitted the “old” residuation σ′(ρ) while applying the clause, but later we will see that this omitted residuation set is also covered by the computed success abstraction (compare Theorem 4.14). The difference of this simplification in comparison to the “real” computation is that some residuations of σ′(ρ) may be evaluated during the concrete clause application. But this difference makes no problem due to Propositions 4.8 and 4.9.

Theorem 4.11 (Correctness of clause entry) Let P = p(X_{1}, …, X_{n}) be a predicate call with abstraction A and ⟨σ, ρ⟩ ∈ γ(A). Let p(Z_{1}, …, Z_{n}) :- L_{1}, …, L_{k} be a (renamed) clause, ⟨σ′, ρ′⟩ be a unifier for σ(P) and p(Z_{1}, …, Z_{n}) computed by the rules of Figure 2, and A_{0} be the abstraction computed by algorithm ai. Then ⟨σ′ ∘σ|_{W} , ρ′⟩ ∈ γ(A_{0}) with W = var(p(Z_{1}, …, Z_{n}) :- L_{1}, …, L_{k}).

Proof: σ′ = {Z_{1} ↦ σ(X_{1}), …, Z_{n} ↦ σ(X_{n})} and ρ′ = ∅ is a unifier computed for σ(P) and p(Z_{1}, …, Z_{n}) (all other unifiers are renamings of this). Since all Z ∈ W are new variables, σ(Z) = Z and thus σ′ ∘ σ|_{W} = σ′. Hence we have to show: ⟨σ′, ∅⟩ ∈ γ(A_{0}).

1. X if V ∈ A_{0}: By definition of call restrict and ai, V = ∅, X = Z_{i} for some i ∈ {1, …, n} and X_{i} ∈ A. Since ⟨σ, ρ⟩ ∈ γ(A), lvar(σ′(Z_{i})) = lvar(σ(X_{i})) = ∅. Hence all variable conditions of A_{0} are satisfied by ⟨σ′, ∅⟩.

2. f(\overline{t}) occurs directly in σ′(X) with var(\overline{t}) ≠ ∅: Then X = Z_{i} for some i ∈ \{1, …, n\} and therefore f(\overline{t}) occurs directly in σ(X_{i}). Since ⟨σ, ρ⟩ ∈ γ(A), f ∈ A (which immediately implies f ∈ A_{0}) or var(\overline{t}) ⊆ var(σ(V)) for some X_{i} with f|_{V} ∈ A. Now consider the latter case. If V ⊈ {X_{1}, …, X_{n}}, then f ∈ A_{0} by definition of call restrict. Otherwise, if V ⊆ {X_{1}, …, X_{n}}, Z_{i} with f|_{σ_{xz}(V)} ∈ A_{0} (where the substitution σ_{xz} renames each X_{j} into Z_{j}). Since σ_{xz}(V) ⊆ \{Z_{1}, …, Z_{n}\}, var(\overline{t}) ⊆ var(σ(V)) = var(σ′(σ_{xz}(V))).

3. Since the residuation part is empty, there are no function calls in this part.

4. lvar(σ′(X)) ∩ lvar(σ′(Y)) ≠ ∅ for variables X ≠ Y: Then X = Z_{i} and Y = Z_{j} for some i ≠ j. σ′(Z_{i}) = σ(X_{i}) and σ′(Z_{j}) = σ(X_{j}) implies lvar(σ(X_{i})) ∩ lvar(σ(X_{j})) ≠ ∅. Since ⟨σ, ρ⟩ ∈ γ(A), {X_{i}, X_{j}} ∈ A and hence {Z_{i}, Z_{j}} ∈ A_{0}.

To prove a similar theorem for the correctness of the abstract operations performed at clause exit, we need two propositions about the flow of residuation abstractions in the abstract interpretation of predicates. The first proposition states that a residuation abstraction of the form “f” will never be deleted during abstract interpretation:

Proposition 4.12 Let P be a predicate call with abstraction A, f ∈ A and ai(A, P) ≠⊥. Then f ∈ ai(A, P).

Proof: By induction on the computation steps of the abstract interpretation algorithm (cf. Section 4.3), it is straightforward to show that this proposition holds since an abstraction element “f” is passed through abstract unification (amgu), from predicate calls to clause entries (call restrict) and from clause exits to predicate calls (exit restrict and rest). Hence “f” is present in all abstractions different from ⊥ during the entire abstract interpretation of ai(A, P).

The next proposition states that a residuation abstraction of the form “X with f|_{V} ” will only be deleted during abstract interpretation if all variables are provable bound to ground terms:

Proposition 4.13 Let P be a predicate call with abstraction A, X with f|_{V} ∈ A and A′ := ai(A, P) ≠⊥. Then f ∈ A′ or V = V_{1} ∪ V_{2} with X with f|_{V_{1}} ∈ A′ and all variables Z ∈ V_{2} are bound to ground terms in all concrete interpretations corresponding to A′.

Proof: This proposition holds similarly to the previous proposition. Note that an abstraction element X with f|_{V} is never deleted but only transformed into f (by call restrict or exit restrict) or some variables in V are deleted by the normalization rules. In the latter case the conditions in the normalization rules ensure that these deleted variables are bound to ground terms in the corresponding concrete interpretations (see proof of Lemma 4.1).

Now we are prepared to prove the correctness of the abstract clause exit operations, i.e., we show that each substitution/residuation pair which may occur at the end of a clause applied to a predicate call is covered by the abstract interpretation algorithm.

Theorem 4.14 (Correctness of clause exit) Let P = p(X_{1}, …, X_{n}) be a predicate call with abstraction A_{in} and ⟨σ_{in}, ρ_{in}⟩ ∈ γ(A_{in}). Let A = ai(A_{in}, P) = closure(A_{success} ∪ rest(A_{in}, {X_{1}, …, X_{n}})) be the abstraction after the predicate call computed by the abstract interpretation algorithm ai. Let L:- L_{1}, …, L_{k} be a (renamed) clause for P, and A_{k} be the abstraction computed for the clause end in ai. Let ⟨σ_{k}, ρ_{k}⟩ ∈ γ(A_{k}) and σ be a substitution on the variables from σ_{in}(P) so that σ(σ_{in}(P)) = σ_{k}(L). Then ⟨σ ∘ σ_{in}, ρ_{k} ∪ σ(ρ_{in})⟩ ∈ γ(A).

In a concrete computation the substitution/residuation pair ⟨σ_{k}, ρ_{k}⟩ after the clause application is an extension of σ_{in} (i.e., σ_{k}(L) = σ(σ_{in}(P)), as required) and an extension of ρ_{in} (i.e., ρ_{k} = ρ∪σ(ρ_{in}) for some ρ where some of the residuations can be evaluated). Since we have omitted the residuation ρ_{in} in the corresponding clause entry (compare Theorem 4.11), we prove in this theorem that this was correct. Proof: Let L = p(Z_{1}, …, Z_{n}), σ_{zx} = {Z_{1} ↦ X_{1}, …, Z_{n} ↦ X_{n}} be the renaming of each variable Z_{i} into X_{i}, and σ_{xz} = {X_{1} ↦ Z_{1}, …, X_{n} ↦ Z_{n}} the inverse of σ_{zx}. Note that σ_{k}(Z_{i}) = σ(σ_{in}(X_{i})) for i = 1, …, n. We have to show: ⟨σ ∘ σ_{in}, ρ_{k} ∪ σ(ρ_{in})⟩ ∈ γ(A).

1. X if V ∈ A: Hence there are two cases:

• X if V ∈ rest(A_{in}, {X_{1}, …, X_{n}}): Then lvar(σ_{in}(X)) ⊆ var_{ρ_{in}}(σ_{in}(V)) since X if V ∈ A_{in} and ⟨σ_{in}, ρ_{in}⟩ ∈ γ(A_{in}). Lemma 4.7 yields lvar(σ(σ_{in}(X))) ⊆ var_{σ(ρ_{in})}(σ(σ_{in}(V))) ⊆ var_{ρ_{k}∪σ(ρ_{in})}(σ(σ_{in}(V))).

• X if V ∈ A_{success}: Since A_{exit} ⊑ A_{success}, there is a set V′ ⊆ V with X if V′ ∈ A_{exit}. By definition of A_{exit}, σ_{xz}(X) if σ_{xz}(V′) ∈ A_{k} and {σ_{xz}(X)} ∪ σ_{xz}(V′) ⊆ {Z_{1}, …, Z_{n}}. ⟨σ_{k}, ρ_{k}⟩ ∈ γ(A_{k}) implies lvar(σ_{k}(σ_{xz}(X))) ⊆ var_{ρ_{k}}(σ_{k}(σ_{xz}(V′))) and hence (since σ(σ_{in}(P)) = σ_{k}(L)) lvar(σ(σ_{in}(X))) ⊆ var_{ρ_{k}}(σ(σ_{in}(V′))). Therefore lvar(σ(σ_{in}(X))) ⊆ var_{ρ_{k}}(σ(σ_{in}(V))) ⊆ var_{ρ_{k}∪σ(ρ_{in})}(σ(σ_{in}(V))).

2. f(\overline{t}) occurs directly in σ(σ_{in}(X_{i})) (for some i ∈ \{1, …, n\}) with var(\overline{t}) ≠ ∅: Then f(\overline{t}) occurs also directly in σ_{k}(Z_{i}) since σ(σ_{in}(P)) = σ_{k}(L). ⟨σ_{k}, ρ_{k}⟩ ∈ γ(A_{k}) implies f ∈ A_{k} (which immediately implies f ∈ A) or var(\overline{t}) ⊆ var(σ_{k}(V)) for some Z_{i} with f|_{V} ∈ A_{k}. In the latter case there are two possibilities: If V ⊈ {Z_{1}, …, Z_{n}}, then f ∈ A_{out} (by definition of exit restrict) and f ∈ A. If V ⊆ {Z_{1}, …, Z_{n}}, then X_{i} with f|_{σ_{zx}(V)} ∈ A_{exit}. This implies X_{i} with f|_{σ_{zx}(V)} ∈ A where var(\overline{t}) ⊆ var(σ_{k}(V)) = var(σ(σ_{in}(σ_{zx}(V))).

3. f(\overline{t}) occurs directly in σ(σ_{in}(X)) with X ∉ \{X_{1}, …, X_{n}\} and var(\overline{t}) ≠ ∅: Hence there is a position π with f(\overline{t}) = σ(σ_{in}(X))|_{π}. We can distinguish two cases:

• π is also a position in σ_{in}(X) and σ_{in}(X)|_{π} = f(\overline{s}) with σ(\overline{s}) = \overline{t}: Since ⟨σ_{in}, ρ_{in}⟩ ∈ γ(A_{in}), f ∈ A_{in} (which implies f ∈ A by Proposition 4.12) or var(\overline{s}) ⊆ var(σ_{in}(V)) for some X with f|_{V} ∈ A_{in}. Since X ∉ {X_{1}, …, X_{n}}, the latter case yields X with f|_{V} ∈ rest(A_{in}, \{X_{1}, …, X_{n}\}) and thus X with f|_{V} ∈ A where var(\overline{t}) = var(σ(\overline{s})) ⊆ var(σ(σ_{in}(V)).

• π is not a position in σ_{in}(X) or σ_{in}(X)|_{π} is a variable: Then σ_{in}(X) contains a variable Z which is instantiated by σ to a term containing the subterm f(\overline{t}). Since σ instantiates only variables occurring in σ_{in}(P), there is a variable X_{i} so that σ_{in}(X_{i}) has a direct occurrence of Z. Hence Z is shared between σ_{in}(X_{i}) and σ_{in}(X) which implies {X_{i}, X} ∈ A_{in}, {X_{i}, X} ∈ rest(A_{in}, {X_{1}, …, X_{n}}), and also {X_{i}, X} ∈ A (since X ∉ \{X_{1}, …, X_{n}\}). Moreover, f(\overline{t}) occurs directly in σ(σ_{in}(X_{i})). Hence we obtain as above f ∈ A or var(\overline{t}) ⊆ var(σ(σ_{in}(V)) for some X_{i} with f|_{V} ∈ A. The latter case implies X with f|_{V} ∈ A since {X_{i}, X} ∈ A and A is closed under the rule for distribution of sharing information.

4. f(\overline{t}) with var(\overline{t}) ≠ ∅ occurs directly in ρ_{k} but not directly in σ(σ_{in}(X)) for all variables X (otherwise proceed as in case 2 or 3): Since ⟨σ_{k}, ρ_{k}⟩ ∈ γ(A_{k}), f ∈ A_{k} (which immediately implies f ∈ A) or var(\overline{t}) ⊆ var(σ_{k}(V)) for some X with f|_{V} ∈ A_{k}. In the latter case there are two possibilities: If {X} ∪ V ⊈ {Z_{1}, …, Z_{n}}, then f ∈ A_{out} (by definition of exit restrict) and hence f ∈ A. If {X}∪V ⊆ {Z_{1}, …, Z_{n}}, then σ_{zx}(X) with f|_{σ_{zx}(V)} ∈ A_{exit}. This implies σ_{zx}(X) with f|_{σ_{zx}(V)} ∈ A where var(\overline{t}) ⊆ var(σ_{k}(V)) = var(σ(σ_{in}(σ_{zx}(V))).

5. f(\overline{t}) with var(\overline{t}) ≠ ∅ occurs directly in σ(ρ_{in}) but not directly in σ(σ_{in}(X)) for all variables X (otherwise proceed as in case 2 or 3): Since f(\overline{t}) does not occur directly in any σ(σ_{in}(X)), f(\overline{s}) occurs directly in ρ_{in} with σ(\overline{s}) = \overline{t}. Since ⟨σ_{in}, ρ_{in}⟩ ∈ γ(A_{in}), f ∈ A_{in} (which implies f ∈ A by Proposition 4.12) or var(\overline{s}) ⊆ var(σ_{in}(V)) for some X with f|_{V} ∈ A_{in}. In the latter case there are three possibilities:

• X ∉ {X_{1}, …, X_{n}}: Then X with f|_{V} ∈ rest(A_{in}, {X_{1}, …, X_{n}}) and hence X with f|_{V} ∈ A where var(\overline{t}) = var(σ(\overline{s})) ⊆ var(σ(σ_{in}(V)).

• X ∈ {X_{1}, …, X_{n}}, V ⊈ {X_{1}, …, X_{n}}: Then f ∈ A_{call} (by definition of call restrict) and f ∈ A (by Proposition 4.12).

• {X} ∪ V ⊆ {X_{1}, …, X_{n}}: Then, by Proposition 4.13, f ∈ A or V = V_{1} ∪ V_{2} with X with f|_{V_{1}} ∈ A and all Z ∈ V_{2} are bound to ground terms by σ ∘ σ_{in}. The latter case implies var(\overline{t}) = var(σ(\overline{s})) ⊆ var(σ(σ_{in}(V)) = var(σ(σ_{in}(V_{1})).

6. lvar(σ(σ_{in}(X)) ∩ lvar(σ(σ_{in}(Y))) ≠ ∅ for variables X ≠ Y. We distinguish the following cases for the variables X and Y:

• X, Y ∈ {X_{1}, …, X_{n}}: Since σ(σ_{in}(P)) = σ_{k}(L), lvar(σ_{k}(σ_{xz}(X)) ∩ lvar(σ_{k}(σ_{xz}(Y)) ≠ ∅ which implies {σ_{xz}(X), σ_{xz}(Y)} ∈ A_{k}. Hence {X, Y } ∈ A_{success} and {X, Y } ∈ A.

• X ∉ {X_{1}, …, X_{n}} (the case Y ∉ {X_{1}, …, X_{n}} is symmetric and therefore omitted) and lvar(σ_{in}(X)) ∩ lvar(σ_{in}(Y)) ≠ ∅: Then {X, Y } ∈ A_{in} which yields {X, Y } ∈ rest(A_{in}, {X_{1}, …, X_{n}}) and {X, Y } ∈ A.

• X ∉ {X_{1}, …, X_{n}} and lvar(σ_{in}(X)) ∩ lvar(σ_{in}(Y)) = ∅:

First suppose Y ∈ {X_{1}, …, X_{n}}. Since σ does only instantiate variables from σ_{in}(P), σ_{in}(X) must share a l-variable with some σ_{in}(X_{i}), and σ(σ_{in}(X_{i})) shares another l-variable with σ(σ_{in}(Y)). Hence {X, X_{i}} ∈ A_{in} which implies {X, X_{i}} ∈ rest(A_{in}, {X_{1}, …, X_{n}}), and {X_{i}, Y } ∈ A_{success} (as in the first case). Both facts imply {X, X_{i}} ∈ A and {X_{i}, Y } ∈ A. Since A is closed under the rule for transitivity of sharing information, {X, Y } ∈ A. Now suppose Y ∉ {X_{1}, …, X_{n}}. Since σ does only instantiate variables from σ_{in}(P), σ_{in}(X) must share a l-variable with some σ_{in}(X_{i}) and σ_{in}(Y) must share a l-variable with some σ_{in}(X_{j}) so that σ(σ_{in}(X_{i})) shares another l-variable with σ(σ_{in}(X_{j})). Hence {X, X_{i}}, {Y, X_{j}} ∈ A_{in} which implies {X, X_{i}}, {Y, X_{j}} ∈ rest(A_{in}, {X_{1}, …, X_{n}}). If

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

Figure 3: OR-node for clause entry

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

Figure 4: AND-node for a clause

i = j, then {X, Y } ∈ A since A is a closed abstraction. If i ≠ j, then {X_{i}, X_{j}} ∈ A_{success} and {X_{i}, X_{j}} ∈ A (as in the first case). But this implies {X, Y } ∈ A by the closure property of A.

4.3 Correctness of the abstract interpretation algorithm

Until now we have proved the local correctness of the basic operations of the abstract interpretation algorithm. We can combine these results into a correctness proof for the whole algorithm by using Bruynooghe’s framework [Bru91]. In his framework the abstract interpretation algorithm generates an abstract AND-OR-tree which represents all concrete computations. To avoid infinite paths, this tree is a rational AND-OR-tree, i.e., if a predicate call is identical to (or a variant of) a predicate call in an ancestor node, then this call node is identified with the ancestor node. The monotonicity property of all abstract operations together with the finite domain avoids an infinite computation in this graph. Next we will give a more detailed description of the abstract interpretation algorithm.

The abstract interpretation procedure generates the abstract AND-OR-graph as follows. In the first step, the root is created. It is marked with the initial goal (w.l.o.g. we assume that the initial goal contains only one literal) and the call abstraction for this goal. Then this initial graph is extended by computing the success abstraction for this goal. The success abstraction A′ of an equation t = t′ with call abstraction A is computed by abstract unification, i.e., A′ = amgu(A, t, t′). To compute the success abstraction A′ of a node with predicate call P and call abstraction A, we distinguish the following cases:

1. There is no ancestor node with the same predicate call and the same call abstraction (up to renaming of variables): First of all, we add an OR-node as shown in Figure 3 (H_{1}, …, H_{m}

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

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

are the heads of all clauses for P). A_{i}^{in} is the call abstraction computed by our abstract operations for the entry of clause H_{i}:- ⋯ (i.e., A_{0} in algorithm ai in Section 3.2). Then for each new clause head H an AND-node is added as shown in Figure 4 where H:- L_{1}, …, L_{k} is the corresponding clause. After copying the call abstraction of the head to the call abstraction of the first body literal (A_{0} = A^{in}) the success abstraction of each literal in the clause body is computed. Then the success abstraction A^{out} of the entire clause is calculated by restricting A_{k} to the head variables (i.e., A^{out} is identical to A_{out} in algorithm ai in Section 3.2). When all success abstractions of all clauses for the predicate call P are computed, they are renamed, combined by the least upper bound operation and then combined with the remainder of the call abstraction of A (compare algorithm ai).

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

In [Bru91] it is shown that this algorithm computes a superset of all concrete proof trees if the abstract operations for built-ins (here: unification), clause entry and clause exit satisfies certain correctness conditions. Theorems 4.10, 4.11 and 4.14 imply exactly these correctness conditions. Hence we can infer the correctness of our abstract interpretation algorithm.

     [figure: A_{0} sum(L0,S0) A_{12}; OR; A_{1} sum(L,S) A_{5}  A_{6} sum(L,S) A_{11}; AND; A_{2} L=[]  A_{3}  S=0 A_{4}; AND; A_{7} L=[E|R] A_{8} S=E+RS A_{9} sum(L,RS) A_{10}]

Figure 6: AND-OR-tree for the abstract interpretation of sum(L0,S0)

4.4 A final example

The following residuating logic program is an example for a recursive procedure which requires the construction of the abstract AND-OR-tree described in the previous section. The following clauses define a predicate sum(L,S) which computes the sum S of a list of numbers L:

   sum([],0).
   sum([E|R],E+RS) :- sum(L,RS).

For instance, the execution of the goal sum([1,3,5],S) yields the answer S=9. The concrete computation is shown in the following table:

Goal:  Current residuation:  Current substitution:

  sum([1,3,5],S) ∅  ∅
  sum([3,5],RS1) {1+RS1=S}  ∅
  sum([5],RS2)  {1+RS1=S, 3+RS2=RS1}  ∅
  sum([],RS3)  {1+RS1=S, 3+RS2=RS1, 5+RS3=RS2} ∅
  ∅  ∅  {RS3↦0, RS2↦5, RS1↦8, S↦9}

We want to show that the residuation principle computes a fully evaluated answer for S for any given list of numbers L. In order to apply our abstract interpretation algorithm, we transform the program into an equivalent flat program:

   sum(L,S) :- L=[], S=0.
   sum(L,S) :- L=[E|R], S=E+RS, sum(L,RS).

The initial goal is sum(L0,S0) with abstraction {L0}, i.e., it is a predicate call with a ground first argument. Our abstract interpretation algorithm applied to this goal and abstraction generates the abstract AND-OR-tree shown in Figure 6. We will see that the tree is finite because the literal sum(L,RS) together with the call abstraction part of A_{9} is a renaming of the root literal sum(L0,S0) together with the call abstraction part of A_{0}. In the following we describe the computation of the abstract interpretation algorithm and the evolving values of the abstractions A_{i}.

• A_{0} = {L0}: The call abstraction of the root literal is the initial abstraction of the goal.

• A_{1} = {L} and A_{6} = {L}: The root is an OR-node with two sons since two clauses can be applied to the literal sum(L0,S0). The entry abstractions for these clauses is computed from A_{0} by call restrict and renaming.

• A_{2} = {L}: The entry abstraction of the clause is also the abstraction for the first predicate call in the clause body.

• A_{3} = {L}: The abstraction A_{2} is not modified by abstract unification since L is already ground.

• A_{4} = {L, S}: S is added to the abstraction by abstract unification since it is bound to a ground term after this unification.

• A_{5} = {L, S}: The exit abstraction of this clause is the exit abstraction of the last body literal restricted to the variables in the clause head.

• A_{7} = {L}: The entry abstraction of the second clause is also the abstraction for the first predicate call in the clause body.

• A_{8} = {L, E, R}: The variables E and R are ground since L is ground. This is computed by the abstract unification algorithm together with the normalization rules.

• A_{9} = {L, E, R, Sif {RS}, Swith+|{RS}}: The function call to + is added to the abstraction. It can not be evaluated until the variable RS is ground.

• A_{10} =⊥: The call abstraction part of A_{9} is {L} (compare definition of call restrict). Hence this predicate call is a renaming of the predicate call at the root and therefore we take the value ⊥ as the success abstraction for this call since the success abstraction of the root call is not yet known. However, if the latter success abstraction is available and different from ⊥, we start a recomputation at this point.

• A_{11} =⊥: The exit abstraction of the second clause is the exit abstraction of the last body literal.

• A_{12} = {L0, S0}: The success abstraction of the root predicate call is the least upper bound of {L0, S0} and ⊥ together with the remainder of A_{0} (which is actually empty). Since the success abstraction of the root call is now available and different from ⊥, we restart the evaluation of the abstraction A_{10}.

• A_{10} = {L, RS, E, R, S}: The new value of A_{10} is computed from the new renamed success abstraction of the root predicate call ({L, RS}) together with the remainder of A_{9} giving {L, RS, E, R, Sif {RS}, Swith+|{RS}}. This abstraction simplified by the normalization rules is the new value of A_{10}.

• A_{11} = {L, S}: The exit abstraction of the second clause is the exit abstraction of the last body literal restricted to the variables in the clause head.

• A_{12} = {L0, S0}: The success abstraction of the root predicate call is the least upper bound of the renamed exit abstractions A_{5} and A_{11} (which are identical) together with the remainder of A_{0} (which is actually empty). Since the success abstraction of the root call is identical to the previous value, we need not restart the evaluation of the abstraction A_{10}. Hence the abstract interpretation algorithm is finished.

Since the abstract interpretation has computed the exit abstraction {L0, S0} for the initial goal, we conclude by the correctness of the abstract interpretation algorithm and the concretisation function γ that variable S0 is bound to a ground term without unevaluable residuations at the end of a successful computation.

5 Conclusions and related work

In this paper we have considered an operational mechanism for the integration of functions into logic programs. This mechanism, called residuation, extends the standard unification algorithm used in SLD-resolutions by delaying unifications between unevaluable function calls and other terms. If all variables of a delayed function call are bound to ground terms, then this function call is evaluated in order to verify the delayed unification. This residuation principle yields a nice operational behaviour for many functional logic programs but has two disadvantages. One problem is that the answer to a query may contain unsolved and complex residuations for which the user cannot easily decide their solvability. A further problem is that the search space of a residuating logic program can be infinite in contrast to the equivalent logic program. This case can occur if the residuation principle generates more and more residuations which are simultaneously not solvable. Hence it is important to check at compile time whether or not this case can occur at run time. Since this is undecidable in general, we have presented an approximation to this problem based on the abstract interpretation of residuating logic programs. Our algorithm manages information about all possible residuations together with their argument variables and the dependencies between different variables in order to compute groundness information. Hence the algorithm is able to infer which residuations can be completely solved at run time.

We can also interpret our algorithm as an attempt to compile functional logic programs from languages with a complete but often complex operational semantics (e.g., EQLOG [GM86], SLOG [Fri85], BABEL [MR92], or ALF [Han90]) into a more efficient execution mechanism without loosing completeness. For this purpose we check a given functional logic program by our algorithm. If the algorithm computes an abstraction containing no potential residuations, then we can safely execute the program with the residuation principle. Otherwise we must apply the nondeterministic narrowing principle to compute all answers. This method can also be applied to individual parts of the program so that some parts are executed using the residuation principle and other parts are executed by narrowing.

Marriott, Søndergaard and Dart [MSD90] have also presented an abstract interpretation algorithm for analysing logic programs with delayed evaluation. The purpose of their work was to check logic programs with negation for floundering, i.e., whether a delayed evaluation of negated subgoals is complete. This is a simpler problem than our analysis of residuating logic programs due to the following reasons:

1. In their context only entire literals can be delayed and not single subterms. Therefore in their framework it is not necessary to analyse the precise structure of the terms.

2. A delayed evaluation of a negated literal cannot bind any goal variables since this literal is evaluated if all arguments are ground. In our context it is important that a delayed evaluation of a residuation can bind variables in order to enable the evaluation of other residuations (see the example in Section 3.3). Therefore we have to manage the dependencies between residuations and their variables in order to analyse the data flow in this case.

3. In our context the terms contain constructors and function calls. The right abstraction of these terms complicates the correctness proofs of our algorithm.

On the other side, we cannot analyse logic programs with delayed negation with our algorithm (for instance, by declaring all negated literals as functions) since we consider the evaluation of a ground function call as an atomic operation. But the evaluation of a negated literal may cause the evaluation of other negated literals and therefore it is not an atomic operation. However, it would be interesting to extend our algorithm to a more detailed analysis of function calls if the functions are specified and evaluated in a particular formalism (for instance, by conditional equations as in ALF [Han90]).

Since we must restrict all abstract information to a finite domain, our algorithm cannot manage all dependencies between residuations and their variables. If a residuation depends only on variables of one clause and these variables are bound to ground terms at the end of the clause, the algorithm detects the solvability of the residuation. But if a residuation depends on local variables from different clauses, then the algorithm cannot manage it and therefore it simply infers the unsolvability of this residuation. It seems to be possible to improve the algorithm at this point by refining the abstract domain (which makes the definition of the concretisation function and the correctness proofs more complex).

Another interesting topic for further research is the question whether it is possible to adapt our proposed method to the abstract interpretation of other logic languages which are not based on SLD-resolution with the leftmost selection rule. Such a method could be applied to analyse the floundering problem of NU-Prolog or to derive run-time properties of the Andorra computation rule [HB88].

References

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

[AK90] H. Aït-Kaci. An Overview of LIFE. In J.W. Schmidt and A.A. Stogny, editors, Proc. Workshop on Next Generation Information System Technology, pp. 42–58. Springer LNCS 504, 1990.

[AKLN87] H. Aït-Kaci, P. Lincoln, and R. Nasr. Le Fun: Logic, equations, and Functions. In Proc. 4th IEEE Internat. Symposium on Logic Programming, pp. 17–23, San Francisco, 1987.

[BGL^{+}87] P.G. Bosco, E. Giovannetti, G. Levi, C. Moiso, and C. Palamidessi. A complete semantic characterization of K-LEAF, a logic language with partial functions. In Proc. 4th IEEE Internat. Symposium on Logic Programming, pp. 318–327, San Francisco, 1987.

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

[CM87] W.F. Clocksin and C.S. Mellish. Programming in Prolog. Springer, third rev. and ext. edition, 1987.

[DJ90] N. Dershowitz and J.-P. Jouannaud. Rewrite Systems. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, Vol. B, pp. 243–320. Elsevier, 1990.

[DL86] D. DeGroot and G. Lindstrom, editors. Logic Programming, Functions, Relations, and Equations. Prentice Hall, 1986.

[Fri85] L. Fribourg. SLOG: A Logic Programming Language Interpreter Based on Clausal Superposition and Rewriting. In Proc. IEEE Internat. Symposium on Logic Programming, pp. 172–184, Boston, 1985.

[GM86] J.A. Goguen and J. Meseguer. Eqlog: Equality, Types, and Generic Modules for Logic Programming. In D. DeGroot and G. Lindstrom, editors, Logic Programming, Functions, Relations, and Equations, pp. 295–363. Prentice Hall, 1986.

[Han90] M. Hanus. Compiling Logic Programs with Equality. In Proc. of the 2nd Int. Workshop on Programming Language Implementation and Logic Programming, pp. 387–401. Springer LNCS 456, 1990.

[Han91] M. Hanus. Efficient Implementation of Narrowing and Rewriting. In Proc. Int. Workshop on Processing Declarative Knowledge, pp. 344–365. Springer LNAI 567, 1991.

[HB88] S. Haridi and P. Brand. Andorra Prolog: An Integration of Prolog and Committed Choice Languages. In Proc. Int. Conf. on Fifth Generation Computer Systems, pp. 745–754, 1988.

[Llo87] J.W. Lloyd. Foundations of Logic Programming. Springer, second, extended edition, 1987.

[MM82] A. Martelli and U. Montanari. An Efficient Unification Algorithm. ACM Transactions on Programming Languages and Systems, Vol. 4, No. 2, pp. 258–282, 1982.

[MR92] J.J. Moreno-Navarro and M. Rodríguez-Artalejo. Logic Programming with Functions and Predicates: The Language BABEL. Journal of Logic Programming, Vol. 12, pp. 191–223, 1992.

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

[Nai91] L. Naish. Adding equations to NU-Prolog. In Proc. of the 3rd Int. Symposium on Programming Language Implementation and Logic Programming, pp. 15–26. Springer LNCS 528, 1991.

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

[Smo91] G. Smolka. Residuation and Guarded Rules for Constraint Logic Programming. Research Report 12, DEC Paris Research Laboratory, 1991.

[SY86] P.A. Subrahmanyam and J.-H. You. FUNLOG: a Computational Model Integrating Logic Programming and Functional Programming. In D. DeGroot and G. Lindstrom, editors, Logic Programming, Functions, Relations, and Equations, pp. 157–198. Prentice Hall, 1986.