Deriving Abstract Semantics for Forward Analysis of Normal Logic Programs

The problem of forward abstract interpretation of {\em normal} logic programs has not been formally addressed in the literature although negation as failure is dealt with through the built-in predicate ! in the way it is implemented in Prolog. This paper proposes a solution to this problem by deriving two generic fixed-point abstract semantics $F^b and $F^\diamond for forward abstract interpretation of {\em normal} logic programs. $F^b$ is intended for inferring data descriptions for edges in the program graph where an edge denotes the possibility that the control of execution transfers from its source program point to its destination program point. $F^\diamond$ is derived from $F^b$ and is intended for inferring data descriptions for textual program points.


Introduction
Abstract interpretation [7] is a program analysis methodology for statically deriving run-time properties of programs. The derived program properties are then used by other program processors such as compilers, partial evaluators, etc. Program analyses are viewed as program executions over non-standard data domains. Cousot and Cousot first laid solid mathematical foundations for abstract interpretation [7,8]. The idea is to define a collecting semantics for a program which associates with each program point the set of the storage states that are obtained whenever the execution reaches the point. Then an approximation of the collecting semantics is calculated by simulating over a non-standard data domain the computation of the collecting semantics over the standard data domain. The standard data domain is called the concrete domain and the non-standard domain is called the abstract domain.
There has been recently much research into abstract interpretation of logic programs [9]. Abstract interpretation has been used in both forward and backward analyses of logic programs. A forward analysis [3] approximates the set of substitutions that might occur at a program point given a program and a set of goal descriptions. A backward analysis [2,6,28,29] approximates the set of the atoms that are logical consequences of a program [42]. A number of generic abstract semantics, often called frameworks, schemes [3,18,30], have been proposed for forward abstract interpretation of logic programs. These generic abstract semantics have been specialised for the detection of determinacy [10], data dependency analyses [5,11,14,15,32,33], mode inference [4,5,11,26,32,41], program transformation [37], type inference [4,13,16,26], termination proof [43], etc. However, these generic abstract semantics have been developed for forward abstract interpretation of definite logic programs. The problem of forward abstract interpretation of normal logic programs has not been formally addressed in the literature although negation as failure is dealt with in practice through the built-in predicate ! in the way it is implemented in Prolog. This paper proposes a solution to this problem by deriving two generic fixed-point abstract semantics F ♭ P and F ⋄ P for forward abstract interpretation of normal logic programs without relying on any capability of dealing with the built-in predicate !.
Existing generic abstract semantics in the literature are optimisation-oriented and they are used to infer data descriptions for textual program points. However, there are some applications such as debugging where it is helpful to infer data descriptions for edges p← •q in the program graph where p← •q denotes that the control of execution may transfers from program point q to program point p. F ♭ P is intended for these applications. F ⋄ P is derived from F ♭ P and is intended for inferring data descriptions for textual program points.
The way in which F ♭ P and F ⋄ P are derived is conventional. F ♭ P is based on a fixed-point collecting semantics that associates a set of substitutions with each edge p← •q in the program graph. The set of substitutions associated with p← •q includes all the substitutions at program point p whenever the control of execution transfers from program point q to program point p. The collecting semantics is obtained through two approximations. The operational semantics SLDNF-resolution via the left-to-right computation rule is first approximated by a transition system. The transition system is then approximated by the collecting semantics. Obtained from the collecting semantics by a further approximation is F ♭ P that can then be specialised to perform various analyses under certain sufficient conditions. F ⋄ P is derived from F ♭ P through one more approximation and it can be specialised to perform various analyses under the same sufficient conditions as F ♭ P . This paper makes two contributions. Firstly, F ♭ P and F ⋄ P can be used to perform forward abstract interpretation of normal logic programs while the existing generic abstract semantics in the literature can only be used to perform forward abstract interpretation of definite logic programs. A common practice in analysing logic programs with negation as failure is to extend an existing generic abstract semantics with capability of dealing with the built-in predicate ! and then analyse negation as failure in the way it is implemented in Prolog. However, the built-in predicate ! is not a part of the language of normal logic programs. The derivation of F ♭ P and F ⋄ P does not resort to any capability of dealing with any built-in predicate. Secondly, F ♭ P is easier to specialise for inferring data descriptions for edges in the program graph than the existing generic abstract semantics in the literature.
The remainder of this paper is organised as follows. Section 2 briefly recalls on mathematical foundations for abstract interpretation and some terminology in logic program, and introduces some notations used later in this paper. Section 3 reformulates SLDNF in order to facilitate the derivation of the collecting semantics. Section 4 derives the collecting semantics from the operational semantics. Section 5 derives F ♭ P from the collecting semantics through a further approximation, and gives the sufficient conditions for F ♭ P to safely approximate the collecting semantics, and analyses its worst case complexity. Section 6 derives F ⋄ P from F ♭ P through one more approximation, and analyses its worst case complexity. In section 7, we show how F ♭ Let < D, ⊑> be a complete lattice and f ∈ D → D. x ∈ D is a fixed-point of f if x = f (x).
x is the least fixed-point, denoted by lfpf , of f if x ⊑ y for each fixed-point y of f . lfpf = f ↑ β for some ordinal β [40] where if β is a successor ordinal

Abstract Interpretation
We now formalise the notion of abstract interpretation according to the ideas given by [7]. The idea of having an element in an abstract domain <D,⊑ > as description of a element in a concrete domain < D, ⊑> is formalised by a monotonic function fromD to D, called a concretisation function.
We say that an element d in D is approximated by an elementd inD if d⊑ γ(d). There might well be a number of elements that approximate d. If γ ∈D → D and γ ′ ∈D →D are concretisation functions then γ · γ ′ ∈D → D is a concretisation function.
The notion of approximation can also be formalised by means of an abstraction function from the concrete domain to the abstract domain, or a Galois connection between the abstract domain and the concrete domain or a relation between the concrete and the abstract domains [27].
A fixed-point interpretation of a program is the least fixed-point of a function associated with the program on a semantic domain, often a complete lattice. The following theorem shows how the least fixed-point of a monotonic function on one complete lattice can be approximated by the least fixed-point of another monotonic function on another complete lattice.

Logic programming
We assume that the reader is familiar with the terminology in logic programming [24]. Let L be a first order language with function symbol set Σ and predicate symbol set Π which is disjoint from Σ. Let VAR be a denumerable set of variables and V ⊆ VAR. TERM(Σ, V) denotes the set of terms that can be built from Σ and V. ATOM(Π, Σ, V) denotes the set of atoms constructible from Π, Σ and V. The negation of an atom A is denoted as ¬A. A literal is either an atom or the negation of an atom. Let θ and σ be substitutions. σ • θ denotes the composition of σ and θ. dom(θ) denotes the domain of θ. Define Sub def = {θ | θ is a substitution}. An expression is a term, an atom, a literal, a clause, a goal etc. The set of variables in an expression E is denoted as vars(E). For an expression E and a substitution θ, Eθ denotes the instance of E under θ. An expression E ′ is an instance of another expression E if E ′ ≡ Eθ for some substitution θ where A ≡ B denotes that A is syntactically identical to B. Let θ be a substitution and V ⊆ VAR.
Two substitutions σ and θ are equivalent modulo renaming if there are two renamings δ and ρ such that σ = θ•δ and θ = σ •ρ. We write σ ∼ = θ to denote that σ and θ are equivalent modulo renaming. We will not distinguish those substitutions that are equivalent modulo renaming. ∼ = is naturally extended to expressions. Let E 1 and E 2 be two expressions. E 1 ∼ = E 2 if there are two renamings δ and ρ such that E 1 = E 2 δ and E 2 = E 1 ρ.
An equation is a formula of the form l = r where l and r are terms or atoms. The set of equations is denoted as Eq. Let E ∈ ℘(Eq). E is in solved form if, for each equation l = r in E, l is a variable and l does not occur in the right hand side of any equation in E. There is a natural bijection between substitutions and the sets of equations in solved form. Therefore, we sometimes write a substitution as a set of equations in solved form. The unification of a set of equations is decidable and the most general unifiers for a set of equations are equivalent modulo renaming. Let mgu be the function from ℘(Eq) to {fail} ∪ (VAR → TERM(Σ, VAR)) that, given a set of equations E, either returns a most general unifier for E if E is unifiable or returns fail otherwise. mgu({l = r}) is sometimes written as mgu(l, r).
A normal clause is a formula of the form H ← L 1 , L 2 , · · · , L n where H is an atom, L i for each 1 ≤ i ≤ n is a literal. H is called the head of the clause and L 1 , L 2 , · · · , L n the body of the clause. A normal goal is a formula of the form ← L 1 , L 2 , · · · , L n with L i for each 1 ≤ i ≤ n being a literal. A normal program is a set {C ı | ı ∈ ℵ C } of normal clauses where ℵ C is a finite set of distinct natural numbers. Let m[ı] denote the number of the literals in the body of clause C ı . We write C ı as H ı ← L (ı,1) , L (ı,2) , · · · , L (ı,m[ı]) .
A query to a program is a goal that initiates the execution of that program. There might be infinite number of possible queries that a program is intended to respond to. For the time being, we denote the set of all possible queries as {G k Θ k | k ∈ ℵ G } where ℵ G is a finite set of distinct natural numbers such that ℵ G ∩ ℵ C = ∅. G k for each k ∈ ℵ G is a normal goal and Θ k is a set of substitutions θ k . Each G k θ k with θ k ∈ Θ k is a query. Let m[k] be the number of literals in G k . We write G k as ← L (k,1) , L (k,2) , · · · , L (k,m[k]) .
Let ℵ def = ℵ C ∪ ℵ G . Let P i refer to C i for i ∈ ℵ C and to refer to G i for i ∈ ℵ G and define V i def = vars(P i ). Let i ∈ ℵ. We designate P i with m[i] + 1 program points, point (i, j) immediately before We denote by N P the set of all program points designated with P i for all i ∈ ℵ. Let p = (i, j) be a program point. p [1] = i denotes the index to the clause or the query to which p belongs. p [2] = j denotes the position of p in the clause or the query. So, p = (p [1], p [2]). We define two partial functions λp.p + and λp.p over the set of all the program points. p + = (p [1], p[2] + 1) is defined for each p such that p [2] ≤ m[p [1]] and p = (p [1], p[2] − 1) is defined for each p satisfying 2 ≤ p [2] ≤ m[p [1]] + 1. p + is the program point to the right of p if p + exists and p is the program point to the left of p if p exists.
Let p ∈ N P . B p denotes the atom in literal L p . If L p is positive then L p ≡ B p . If L p is negative then L p ≡ ¬B p .
Example 2.2 The following normal logic program will be used in several examples in this paper. The meaning of member(X, L) is that X is a member of list L. The meaning of dif f (X, L, K) is that either X is a member of list L or X is a member of list K but X is not both a member of L and a member of K.
Suppose that the set of queries is described by

Operational semantics
The operational semantics we consider is the SLDNF-resolution via the left to right computation rule. We shall not mention the computation rule explicitly. When the set of all the descendant goals of a set of queries is to be computed, it is necessary to resolve the current goal with every clause whose head unifies with the selected atom in the current goal. Therefore, the selection rule for choosing a particular clause to resolve with the current goal is not of interest. [9] uses general SLD-resolution as operational semantics of definite logic programs and does not take the computation rule into account. This usually leads to less precise analyses [16].

SLDNF
We now briefly recall on SLDNF-resolution (SLDNF in short). The renamed literals will be written in the form Lρ where L is a literal in a clause or a query and ρ a renaming used in standardisation apart [1]. First consider SLD-resolution (SLD in short) for definite logic programs where every literal is positive. For a query and a definite program, SLD works by repeatedly resolving the current goal, initially the query, with a clause in the program. In one resolution step, SLD nondeterministically selects a clause in the program, renames the clause so that it does not have any common variable with the current goal, and derives a new goal by replacing the leftmost literal in the current goal with the body of the renamed clause and applying to the resultant the most general unifier of the head of the renamed clause and the leftmost literal.
If SLD has derived an empty goal, it has successfully computed a computed answer substitution to the query. The computed answer substitution is the restriction, to the variables in the query, of the composition of the most general unifiers in the derivation from the query to the empty goal.
With SLD, only positive information can be derived from a program. SLDNF uses the negation as failure rule to derive negative information. SLDNF deals with positive literals in the same way as SLD. Suppose that the leftmost literal in the current goal is negative. SLDNF first recursively invokes itself with the leftmost literal as the query of the recursive invocation. If the recursive invocation fails then SLDNF removes the leftmost literal from the current goal and continues with the resultant as the new current goal. Otherwise, according to the rule for the weak safe uses of negation as failure [24], SLDNF either backtracks if the computed answer substitution returned by the recursive invocation is a renaming or otherwise flounders.
Let the current goal be where ρ j is the renaming used to rename clause C ij . If L (ij ,k) ≡ ¬B (ij ,k) then SLDNF recursively invokes itself with ← B (ij ,k) τ (j,k) as the query of the recursive invocation.
in the program and a renaming ρ j+1 such that and B (ij ,k) ρ j τ (j,k) and H ij+1 ρ j+1 unify, then the new current goal becomes and Suppose that there is a sub-refutation of 1) with the composition of the most general unifiers used in the sub-refutation being θ. Then the next current goal immediately after the sub-refutation is

VSLDNF
We now propose a variant of SLDNF (VSLDNF in abbreviation) as the operational semantics. VSLDNF is equivalent to SLDNF in the sense that, given the same goal and the same program, VSLDNF reaches a program point iff SLDNF reaches the same program point, and the instantiation of the variables in the clause of the program point by VSLDNF is equivalent (modulo renaming) to that by SLDNF. We now formulate VSLDNF and then establish the equivalence between SLDNF and VSLDNF. Let the current goal be If L (ij ,k) ≡ ¬B (ij ,k) then VSLDNF recursively invokes itself with ← B (ij ,k) σ (j,k) being the query of the recursive invocation. Let L (ij ,k) ≡ B (ij ,k) . The derivation is suspended and a sub-derivation is started as follows. If there is a clause C ij+1 ≡ H ij+1 ← L (ij+1,1) , L (ij+1,2) , · · · , L (ij+1,m[ij+1]) in the program and a renaming ψ j+1 such that and B (ij ,k) σ (j,k) ψ j+1 and H ij+1 unify then the next current goal becomes We call the step to derive a new goal from the current goal and a clause in the program procedure-entry.
Lemma 3.1 VSLDNF is equivalent to SLDNF in the sense that, given the same goal and the same program, VSLDNF reaches a program point iff SLDNF reaches the same program point, and the instantiation of the variables in the clause of the program point by VSLDNF is equivalent (modulo renaming) to that by SLDNF.
VSLDNF performs a procedure-exit step and derives the following from (G1).
This finishes a sub-refutation of (G1). VSLDNF performs a procedure-exit step and derives the following from (G0).
where, letting φ 1 = ∅, This finishes a refutation of (G0). So, σ (0,2) = {X/2} is a computed answer substitution of ← dif f (X, [2,1], [3,1]). 2 VSLDNF differs from SLDNF in several ways. Firstly, a goal in VSLDNF is a part of a clause or a query, in particular, it is a tail of a clause or a query. This helps to approximate VSLDNF as a transition system later. Secondly, when VSLDNF derives a new goal from the current goal and a clause, it renames the leftmost literal in the goal instead of the clause. This is to ensure that the domain of the substitution that will be applied to the body of the clause contains variables in the clause instead of their renamed counterparts. Thirdly, when a sub-refutation is finished, an extra renaming and an extra unification are needed for VSLDNF to calculate the substitution immediately after the sub-refutation whilst these extra operations are not needed in SLDNF. Note that VSLDNF is only used in formulating the collecting semantics.

Program graph
Let p, q ∈ N P , and q be the most recent program point that VSLDNF has reached. There are several possibilities that VSLDNF will reach p next. If q is the exit point of a clause then the only way that VSLDNF can reach p immediately is to perform a procedure-exit. This can happen only if L p is positive and that program clause has been used to resolve with L p . If q is not the exit point of a clause then VSLDNF may reach p immediately either by performing a procedure-entry or by applying the negation as failure rule. VSLDNF may reach p immediately by applying negation as failure rule if L q ≡ ¬B q ∧ q = p . VSLDNF may reach p immediately by performing a procedure-entry either directly when L q is positive or indirectly when L q is negative. Note that if q is the exit point of a query then VSLDNF has succeeded and will not visit any more program points. In order to facilitate further presentation, we assume that VSLDNF starts at a dummy program point (0, 0) ∈ N P from where it can reach entry points of goal clauses by doing nothing. Therefore, there are four ways that VSLDNF will reach p immediately after it has reached q. We use a graph < N + P , E P >, called program graph, to represent the relation among program points p, q that "VSLDNF will possibly visit p immediately after it has visited q. The set N + P of nodes in the program graph is N P ∪ {(0, 0)} and each edge p← •q in E P in the program graph denotes that VSLDNF will possibly visit p immediately after it has visited q. Formally, E P is inductively defined as follows.
P is the collection of edges from dummy program point (0, 0) to the entry points of queries. Edges in E 1 P correspond to procedure-entries, edges in E 2 P to procedure-exits, and edges in E 3 P to the negation as failure rule.
There are 23 edges in the program graph for the program. 2

Collecting semantics
In this section, we present the fixed-point collecting semantics for normal programs. The collecting semantics of normal program P is lfpF ♯ P where F ♯ P is defined below. lfpF ♯ P associates a set of substitutions with each edge p← •q ∈ E P . Sub-section 4.1 uses a transition system to approximate VSLDNF. A state in this transition system corresponds to a goal in VSLDNF. The set of states derivable from a set of initial states by the transition system is then characterised as the least fixed-point lfpF P of a function F P mapping a set of states into another set of states. Therefore, the set of goals derivable from a set of initial goals by VSLDNF is approximated by lfpF P . Sub-section 4.2 derives the fixed-point collecting semantic function F ♯ P from F P and proves that lfpF ♯ P is a safe approximation of lfpF P . Let A, B be atoms, and θ, ω ∈ Sub. Define Although there are infinite number of renamings ρ satisfying vars(Aθρ) ∩ vars(Bω) = ∅ in equation 9, only one renaming must be considered when computing unif y(A, θ, B, ω) because unif y(A, θ, B, ω) for one renaming is equivalent (modulo renaming) to unif y(A, θ, B, ω) for another renaming accoding to lemma 10.2.

Approximating VSLDNF by a transition system
We now devise a transition system to approximate VSLDNF. A state in the transition system corresponds to a goal in VSLDNF. The transition system approximates VSLDNF in the sense that, if a goal is derivable from an initial goal by VSLDNF then the state corresponding to the goal is derivable from the state corresponding to the initial goal by the transition system while the reverse is not necessarily true.
A state in the transition system is a stack that is a sequence of stack items. The empty stack is denoted as $. A stack item is of the form p← •q, θ where p← •q ∈ E P and θ ∈ Sub. The meaning of p← •q, θ is that the control of execution transfers from q to p with θ being the substitution at p. The set S ♯ of all possible stack items is therefore The set S of all possible stacks is the set of all possible sequences of stack items from S ♯ . S can be inductively defined as follows.
• $ ∈ S; and The set S 0 ⊆ S of initial states is determined by the set of queries in VSLDNF.
The set of final states is The set of descendant states of the set S 0 of initial states is obtained by applying the transition rules in figure 1. Rule (0) says that every final state is stable. Rule (1a) corresponds to direct procedure-entry and rule (1b) to indirect procedure-entry. Rule (2) corresponds to procedure-exit and rule (3) deals with negative literals.
Rule (3) causes the inaccuracy of the transition system. When the transition system reaches a state corresponding to a goal with its leftmost literal being negative, the transition system may apply either rule (1b) or rule (3). Applying rule (1b), it will go to a state corresponding to a goal after performing a procedure-entry indirectly. The application of rule (1b) is to enable information to propagate forward so as to ensure that the transition system safely approximates VSLDNF. Applying rule (3), it will go to a state corresponding to the goal as if the recursive The set of descendant states of a set S 0 of initial states is therefore the least fixed-point of function F P that is defined as follows.
The domain D of F P is ℘(S). < D, ⊆> is a complete lattice and F P is monotonic on < D, ⊆>.
Rule (0) of the transition system is not embodied in F P . Since F P is a monotonic function on < D, ⊆>, we have F P ↑ k ⊆ F P ↑ (k + 1) for any k ≥ 0. Therefore, any final state will be in lfpF P if it is derivable from an initial state by the transition system.

Collecting semantics
lfpF P is a set of states. A state is a stack that corresponds to a goal. The collecting semantics lfpF ♯ P first abstracts away the sequential relation between stack items of a stack and then classifies the stack items according to edges p← •q. lfpF ♯ P associates each p← •q in E P with the set of substitutions θ such that p← •q, θ is a stack item in S ♯ . Each edge p← •q ∈ E P will be assocaited with a member from ℘(Sub). < ℘(Sub), ⊆, ∅, Sub, ∩, ∪ > is a complete lattics. Therefore, the domain D ♯ of the collecting semantics is the Cartesian product of the same component domain ℘(Sub) for as many times as the number of edges p← The approximation of a set of stacks by a vector of sets of substitutions is modeled by the following monotonic function γ ♯ ∈ D ♯ → D.
Let A, B be atoms, and Θ, Ω be sets of substitutions. Define The fixed-point collecting semantics is defined in the following.
The collecting semantics lfpF ♯ P is a safe approximation of the operational semantics and can be used as a basis for program analysis because any safe approximation of this collecting semantics is a safe approximation of the operational semantics. [lfpF ♯ P ] p← •q contains all the substitutions whenever the control of execution transfers from program point q to program point p. [lfpF ♯ P ] p← •q is usually an infinite set of substitutions and is therefore not computable in finite time. In order to obtain useful information about the possible substitutions when the control of execution transfers from program point q to program point p, further approximations are needed. This section derives the generic abstract semantics F ♭ P from F ♯ P .

Abstract domains
The collecting semantics lfpF ♯ P associates with each edge p← •q a set of substitutions which is a superset of the set of the substitutions whenever the control of execution transfers from q to p. When program is analysed by means of abstract interpretation, the set of substitutions associated with p← •q is approximated by an abstract substitution associated with p← •q. For edge p← •q, only values of the variables in V p [1] are of interest and, for edge p ′ ← •q ′ , only values of the variables in V p ′ [1] are of interest. The abstract substitions for p← •q and p ′ ← •q ′ are from different domains when p ′ [1] = p [1]. We will simply call a domain for abstract substitutions an abstract domain. We find it convenient to parameterise abstract domains with finite sets of variables instead of having a single abstract domain for all abstract substitutions associated with different edges or constructing abstract domains for different edges in different ways. Let ASub V denote the domain for abstract substitutions for describing values of variables in V. Then [lfpF ♯ P ] p← •q is represented by a member of ASub V p [1] . We require that, for any finite V ⊆ VAR, The domain D ♭ of F ♭ P is constructed in the same manner as the domain D ♯ of F ♯ P was constructed. Each member X ♭ in D ♭ is a vector that is indexed by edges p← •q in E P . X ♭ p← •q is an element from ASub V p [1] . Let X ♭ ∈ D ♭ and Y ♭ ∈ D ♭ . Define The concretisation function γ ♭ is defined in terms of γ Vi . For every p← •q ∈ E P and X ♭ ∈ D ♭ , The monotonicity of γ ♭ ∈ D ♭ → D ♯ follows immediately from equation 21 and C2.

5.2
The Generic Abstract Semantics F ♭ P F ♭ P is derived from F ♯ P as follows. A set Θ ∈ ℘(Sub) of substitutions is replaced by an abstract substitution θ ♭ in ASub V where V is a set of variables whose values are of interest. unif y ♯ applied to two sets of substitutions described by θ ♭ ∈ ASub U and σ ♭ ∈ ASub V respectively is replaced by an operator unif y U ,V applied to θ ♭ and σ ♭ . ∪ in the definition of [F ♯ P ] p← •q is replaced by ⊔ V p [1] . Let θ ♭ k ∈ ASub V k be the least abstract substitution such that Θ k ⊆ γ V k (θ ♭ k ) for each k ∈ ℵ G . Note that θ ♭ k instead of Θ k is given before the program is analysed. Let ǫ Vi ∈ ASub Vi , called an abstract identity substitution in [3], be the least abstract substitution such that ǫ ∈ γ Vi (ǫ Vi ) for each i ∈ ℵ C . F ♭ P is defined as follows.
for any finite U, V ⊆ VAR, any θ ♭ ∈ ASub U , any σ ♭ ∈ ASub V , and any atoms A and B such that vars(A) ⊆ U and vars(B) ⊆ V.

Complexity of F ♭ P
The cost of computing lfpF ♭ P is affected by the characteristics of P , the abstract domain, abstract substitutions θ ♭ k where k ∈ ℵ G , and the algorithm for least fixed-point computation. Using O'Keefe's algorithm for least fixed-point computation [36], the worst case cost of computing lfpF ♭ P is proportional to the product of the number of operations in F ♭ P and the maximum height dmax of ASub Vi for i ∈ ℵ. Since ⊔ is much less costly than unif y in most cases, we measure the worst case number of occurrences of unif y in F ♭ P . Let S be a set and define #S be the number of members in S. Let P is the set of edges whose ending points lie in N  P . Let pmax be the maximum number of predecessors that a program point has. By equations 22 and 25, unif y does not occur in equations for edges in E 0 P ∪ E 3 P . By equation 23, unif y occurs at most pmax times in the equation for an edge in E 1 P . So, unif y occurs at most #E 1 P * pmax times in the equations for edges in E 1 P . By equation 24, unif y occurs at most pmax 2 times in the equation for an edge in E 2 P . So, unif y occurs at most #E 2 P * pmax 2 times in the equations for edges in E 2 P . Since #E 2 P ≤ #E 1 P and #E 1 P ≤ #ℵ C * pmax, the worst case number of occurrences of unif y in F ♭ P is O(#ℵ C * pmax 3 ). Therefore, the worst case cost of computing lfpF ♭ P is The Generic Abstract Semantics F ⋄ P A further approximation may be made of F ♭ P so as to reduce the complexity of program analyses. lfpF ♭ P is a vector indexed by edges in the program graph for P . lfpF ♭ P associates with each program point with several abstract substitutions, each for one edge ending at the program point. This results in fine analyses for applications such as program debugging. However, there are some applications where such fine analyses are not beneficial with respect to their costs and one abstract substitution for each program point is a better choice. F ⋄ P fulfills such purposes and is derived from F ♭ P by one more approximation. The domain of F ⋄ P is D ⋄ and each X ⋄ ∈ D ⋄ is a vector indexed by program points. D ⋄ is constructed from ASub V in a similar manner as is and define The approximation through collapsing the abstract substitutions associated with all the edges ending at a common program point is characterised by the following concretization function.
It follows immediately from equation 31 that γ ⋄ ∈ D ⋄ → D ♭ is monotonic. We now construct a monotonic function Lemma 6.1 lfpF ♭ P ⊑ ♭ γ ⋄ (lfpF ⋄ P ). Proof: See p.35 lfpF ⋄ P associates each program point with an abstract substitution. The simultaneous recurrence equations for F ⋄ P are simpler than those for F ♭ P and hence the computation of lfpF ⋄ P is less costly than that of lfpF ♭ P . F ⋄ P is a generalisation of Nilsson's generic abstract semantics for definite logic programs [34]. Specifically, if P does not have negative literals then lfpF ⋄ P is equal to that in [34]. Nilsson later [35] presented a generic abstract semantics that is based on a collecting semantics that associates with each program point a set of pairs of goal structures. A goal structure is very similar to a stack in our term.
Each program point in P corresponds to an equation of F ⋄ P . By equations 32 and 35, unif y does not occur in equations for points in N 0 P ∪ N 3 P . unif y occurs at most pmax times in an equation for a point in N 1 P ∪ N 2 P according to equations 33 and 34. The worst case number of occurrences of unif y in F ⋄ P is O(#N P * pmax) since #N 1 P + #N 2 P ≤ #N P . Therefore, the worst case cost of computing lfpF ⋄ P is O(dmax * #N P * pmax) F ⋄ P ( a generalisation of the generic abstract semantic in [34] ) may also be used to obtain abstract substitutions for edges. We prefer F ♭ P to F ⋄ P for such analyses since F ♭ P is easier to specialise than F ⋄ P . In order to specialise F ⋄ P (or the generic abstract semantics in [35]) for such an analysis, in addition to the work required to specialise F ♭ P for the same analysis, one needs to do • keeping information about program points in abstract substitutions, an abstract substitution for F ⋄ P is a set of pairs of a program point and an abstract substitution for F ♭ P ; • replacing unif y by unif y which, for each member of θ ⋄ × σ ⋄ , discards point information and calls unif y.
This amounts to requiring the analysis design who specialises F ⋄ P to undo approximation γ ⋄ . A call to unif y may cause unif y to be called as many times as pmax 2 . So, the worst case complexity of F ⋄ P is no less than that of F ♭ P for the same analysis.
We have so far developed the generic abstract semantics lfpF ♭ P and lfpF ⋄ P for forward abstract interpretation of normal logic programs. lfpF ♭ P obtains an abstract substitution for each edge in E P while lfpF ⋄ P obtains an abstract substitution for each program point in N P . In order to specialise either of these generic abstract semantics to perform a particular analysis, it is sufficient to design ASub, γ, ǫ,unif y and ⊔ such that they satisfy C1-C4.

Example
We now illustrate how F ♭ P and F ⋄ P can be specialised to perform a particular analysis through groundness analysis -a simplified version of mode analysis.
In groundness analysis, we are interested in knowing which variables will be definitely instantatiated to ground terms. Therefore, a set of substitutions is approximated naturally by a set of variables. ASub V = ℘(V). The partial order on ASub V induced by ⊆ on ℘(Sub) is ⊇. < ℘(V), ⊇, V, ∅, ∪, ∩ > is a complete lattice.
The approximation of a set of substitutions by a set of variables is modeled by the following concretisation function γ V ∈ ℘(V) → ℘(Sub).
Note that E 0 is written as a set of equations in solved form.

Related work and Discussion
There has been much research into abstract interpretation of logic programs. For a comprehensive survey, see [9]. A number of generic abstract semantics have been brought about for abstract interpretation of logic programs [3,18,29,30]. Abstract interpretation has been used in both forward and backward analyses of logic programs. A forward analysis [3] approximates the set of substitutions that might occur at each program points given a program and a set of goal descriptions. A backward analysis [2,6,28,29] approximates the set of the atoms that are logical consequences of a program [42]. However, the problem of forward abstract interpretation of normal logic programs has not been formally addressed in the literature although negation as failure is dealt with through the built-in predicate ! in the way it is implemented in Prolog. We have proposed a simple solution to the problem. We now review previous work and discuss about the solution.

Approaches to forward abstract interpretation of logic programs
There are three approaches to forward abstract interpretation of logic programs. A bottomup forward abstract interpreter mimics a bottom-up evaluation strategy. A top-down forward abstract interpreter mimics a top-down evaluation strategy. Top-down forward abstract interpreters can be further divided into two sub-classes according to whether or not the underlying top-down evaluation strategy uses memoisation. A fixed-point forward abstract interpreter computes the least fixed-point of a system of simultaneous recurrence equations.

Bottom-up forward abstract interpretation
The abstract interpreter based on Alexander Templates (AT) [18] simulates the bottom-up evaluation based on AT [38]. Given a program and a goal, AT first transforms the program and the goal and then evaluates the transformed program and the transformed goal in a bottomup manner. Given a program and a goal description, the AT-based abstract interpreter first transforms the program and the query description in the same way as AT does and then mimics the evaluation phase of AT by replacing standard unification with an abstract one.

Top-down forward abstract interpretation without memoisation
A top-down forward abstract interpreter without memoisation [3,31,44,46] approximately executes a goal description by mimicing the underlying the top-down evaluation strategy. As an example, we take the top-down forward abstract interpreter in [3].
Given a goal description that is a pair of an atom and an abstract substitution, the topdown forward abstract interpreter in [3] constructs an abstract AND-OR graph to approximate the set of all the intermediate proof trees that may be constructed by SLDNF under the leftto-right computation rule for all the goals satisfying the goal description. In other words, any intermediate proof tree for any goal satisfying the goal description can be obtained by unraveling the abstract AND-OR graph. An AND-node is a clause head and its child OR-nodes are the atoms in the body of the clause. Every OR-node is adorned with one abstract substitution to the left, called abstract call substitution, and with another to the right, called abstract success substitution. The abstract success substitution of an OR-node is the abstract call substitution of its right sibling.
The initial abstract AND-OR graph has one OR-node that is the atom in the goal description and is adorned to the left with the abstract substitution in the goal description. Suppose that the abstract AND-OR graph has been partly constructed. Consider an ORnode A with abstract call substitution β. The abstract interpreter computes the abstract success substitution of OR-node A as follows. For each clause C i ≡ H i ← B (i,1) , · · · , B (i,m[i]) such that H i may match with Aθ for some θ satisfying β, the abstract interpreter adds to OR-node A a child AND-node H i that has m[i] child OR-nodes B (i,1) , · · · , B (i,m[i]) and computes the abstract call substitution β i in of OR-node B (i,1) -the first child OR-node of AND-node H i . β i in approximates the set of the most general unifiers of H i and Aθ for all θ satisfying β. The abstract interpreter extends OR-node B (i,1) by recursively applying the same process and extends OR-node B (i,j+1) in the same way after it has computed the abstract success substitution of OR-node B (i,j) . Eventually, it will have computed the abstract success substitution β i out of OR-node B (i,m[i]) . After computing β i out for each clause such that H i may match with Aθ for some θ satisfying β, the abstract interpreter computes the abstract success substitution β ′ of OR-node A and β ′ approximates from above the set of the most general unifiers of Aθ and H i η for all the θ satisfying β and all the η satisfying β i out . Since there are recursive calls, [3] introduces a fixed-point component to the abstract interpretation process. Suppose that an OR-node A with abstract call substitution β were to be extended. If A has an ancestor OR-node A ′ with abstract call substitution β ′ such that A is a variant of A and β is a variant of β ′ , the abstract interpreter adorns OR-node A to the right with the infimum abstract substitution and proceeds until the abstract success substitution of OR-node A ′ is computed. The abstract interpreter then repeatedly recomputes the part of the AND-OR graph starting from the abstract success substitution of OR-node A to the abstract success substitution of OR-node A ′ by using the abstract success substitution for OR-node A ′ as the abstract success substitution for OR-node A. This fixed-point process finishes when there is no more increase in the abstract success substitution of OR-node A ′ . The same fixed-point component is also used to limit the sizes of abstract AND-OR graphs. [31,44,46] differ from [3] only in dealing with recursive calls. [31] and [46] make use of a memo table and [44] uses stream predicates.

Top-down forward abstract interpretation with memoisation
An abstract interpreter based on an evaluation strategy with memoisation mimics the underlying evaluation strategy with memoisation by replacing concrete substitutions with abstract substitutions and the concrete unification with an abstract unification. For an introduction to evaluation strategies with memoisation, see [45].
The abstract interpreter based on OLDT resolution [19,20,21] mimics the OLDT resolution [39]. The left-to-right computation rule is used in OLDT resolution. Given a goal that is a pair of a sequence of atoms and a substitution, OLDT resolution [39] constructs an OLDT structure for the goal. An OLDT structure consists of a search tree, a solution table and an association. An entry of the solution table has a key and a solution list. The key is an atom and the solution list is a list of atoms that are instances of the key. Each node of the search tree is a pair of a goal and a substitution and each edge of the search tree is labeled with a substitution. The association is a group of pointers between the nodes of the search tree and the entries of the solution table.
Initially, the search tree has one node that is the pair of the sequence of atoms and the substitution, and both the solution table and the association are empty. OLDT resolution extends the OLDT structure as follows until it cannot be further extended. Suppose that the OLDT structure has been partly constructed. Consider a node < (A, R), σ > in the search tree where A is an atom, R a sequence of atoms and σ a substitution. If there is an entry in the solution table with a key that is a variant of Aσ then < (A, R), σ > is called a lookup node. Otherwise, it is called a solution node. OLDT resolution extends the OLDT structure by extending its lookup nodes and its leaf solution nodes. If < (A, R), σ > is a leaf solution node then OLDT resolution first adds into the solution table an entry whose key is Aσ and whose solution list is an empty list that will be filled in later. OLDT resolution then, for each clause such that H i and Aσ unify with θ being the most general unifier, adds < (B (i,1) , · · · , B (i,m[i]) , R), σ • θ > as a child node to node < (A, R), σ > and labels the edge from node < (A, R), σ > to node < (B (i,1) , · · · , B (i,m[i]) , R), σ • θ > with θ. These child nodes will then be extended by the same process. If < (A, R), σ > is a lookup node then, OLDT resolution first adds < R, σ • θ > as a child node to < (A, R), σ > and labels the edge from < (A, R), σ > to < R, σ • θ > with θ for each solution Aσθ in the solution list for key Aσ, and then adds to the association a pointer from lookup node < (A, R), σ > to the tail of the solution list for key Aσ. This pointer will be used to add more child nodes to lookup node < (A, R), σ > because at the moment lookup node < (A, R), σ > is first extended, some solutions for Aσ might be unavailable from the solution list and will show up later. When a unit clause is resolved with a leaf solution node < (A, R), σ >, the unit clause completes a sub-refutation for Aσ and may also completes sub-refutations for the leftmost atoms of other nodes along the path from < (A, R), σ > up to the root of the search tree. Whenever a unit clause is resolved with a leaf solution node, OLDT resolution updates the solution lists for those keys that corresponds to completed sub-resolutions. After the solution list for a key is updated, OLDT resolution expands those lookup nodes that have pointers pointing to the solution list accordingly.
The abstract interpreter mimics OLDT resolution closely by constructing an abstract OLDT structure for a goal description that is a pair of a sequence of atoms and an abstract substitution. The nodes of the abstract OLDT structure are pairs of a sequence of atoms and an abstract substitution instead of a concrete substitution and the edges of the abstract OLDT structure are now labeled with abstract substitutions instead of concrete substitutions. The key of a solution table entry is now a pair of an atom and an abstract substitution and so is each solution in the solution list for the key. The abstract interpreter mimics OLDT by replacing the concrete unification function with an abstract unification function and the concrete composition function for concrete substitutions with an abstract composition function for abstract substitutions.

Fixed-point forward abstract interpretation
Given a program and a set of goal descriptions that are abstract atoms, [30] derives a system of concrete simultaneous recurrence equations whose least solution approximates the set of all the input atoms and the set of all the output atoms that occur in an intermediate proof tree derivable from the program and any goal satisfying one of the goal descriptions. The system of concrete simultaneous recurrence equations is approximated from above by a system of abstract simultaneous recurrence equations with each concrete operation being replaced by an abstract operation. Abstract interpretation is done by computing the least fixed-point of the system of abstract simultaneous equations.
Given a program and a set of goal descriptions each of which is a pair of a goal and an abstract substitution, [34] derives a system of concrete simultaneous recurrence equations whose least solution gives each program point a superset of the set of all the possible substitutions at the program point during the satisfaction of any goal satisfying one of these goal descriptions. A system of abstract simultaneous recurrence equations is derived to approximate from above the system of concrete simultaneous recurrence equations in the same manner as in [30]. Abstract interpretation is accomplished by computing in an abstract domain the least fixed-point of the system of abstract simultaneous recurrence equations.
[34] collects a set of substitutions for every program point. [30] collects the set of input atoms and the set of output atoms. Collecting the set of input atoms corresponds to collecting a set of substitutions for the entry point of each clause, applying each substitution in the set to the head of the clause to obtain a set of atoms for the clause and then lumping together the sets of atoms for all the clauses as well as the given set of input atoms. Similarly, collecting the set of output atoms corresponds to collecting a set of substitutions for the exit point of each clause, applying each substitution in the set to the head of the clause to get a set of output atoms for the clause and lumping together the sets of output atoms for all the clauses. [30] uses the idea of a trace to summarise the execution of a query. When making abstraction, the sets of call substitutions of different calls to the same predicate are lumped together in a single set input. Similarly, the set of success substitutions are lumped together in the set output.
In [17], contexts are recorded only at the entry of each program clause. [17] is also a generic procedure, their core semantics is augmented with application dependent auxiliary functions that are similar to abstract operations in [3]. These auxiliary functions operate on abstract domains consisting of appropriate approximations of the collecting semantics. They distinguish between different call instances. However, there is only one instance of every clause, so substitutions originating from different call instances are lumped together.

The Negation as Failure
The treatment of negation as failure in F ♭ P and F ⋄ P is simple. The transition system F P approximates VSLDNF (an equivalent of SLDNF) by assuming that a negative literal always succeeds while it may fail. This approximation introduces noises into F ♭ P and F ⋄ P . However, it is difficult within the provisions of abstract interpretation to improve on this simple solution.
Let (¬A)σ be selected by SLDNF where ¬A is a negative literal in the body of a clause in the program and σ be a substitution. During abstract interpretation, σ is not known and possible values for σ are described by an abstract substitution σ ♭ ∈ ASub V , often called the abstract call substitution for (¬A). Since σ ♭ usually describes an infinite set of substitutions, it may well be the case that Aσ succeeds for some σ ∈ γ V (σ ♭ ) and fails for other σ ∈ γ V (σ ♭ ). We take σ ♭ as the abstract success substitution for ¬A by simply assuming that Aσ fails for all σ ∈ γ V (σ ♭ ) (¬Aσ succeeds). An improvement needs making the abstract success substitution for ¬A stronger, that is, replacing σ ♭ with another abstract substitution η ♭ ∈ ASub V such that η ♭ ⊑ V σ ♭ . Let us assume that γ V (σ ♭ )\γ V (η) = ∅ for otherwise η ♭ is no stronger than σ ♭ . By safeness requirement for negation as failure and safeness requirement for abstract interpretation, it is necessary to be able to infer ∀θ ∈ γ V (σ ♭ )\γ V (η). ǫ is a computed answer f or P ∪ {← Aθ} To infer 36, we need to under-estimate success and over-estimate failure in order to make the analysis safe. However, abstract interpreters over-estimate success and under-estimate failure.
Note that the word approximation in abstract interpretation means approximation from above. An abstract interpreter over-estimates success by means of an abstract unification function which approximates the normal unification function from above, that is, over-estimates the success of the normal unification function. To infer 36, we must use a unification function which approximates the normal unification function from below. Such a unification function should succeed only if the normal unification function succeeds. Of course, we could use a unification function which always fails. But, this does not achieve any improvement since such a unification function will make Aσ always fail. Since an abstract domain for an analysis is much simpler than the concrete domain, some information about a set of substitutions is lost when the set of substitutions is approximated by an abstract substitution. It is difficult to design a unification function which approximates the normal unification function from below based on abstract substitutions because abstract substitutions are inaccurate descriptions of sets of substitutions while such a unification function, we believe, needs accurate descriptions of sets of substitutions.

Summary
We have presented and justified a simple solution to the problem of forward abstract interpretation of normal logic programs and derived generic abstract semantics lfpF ♭ P and lfpF ⋄ P of normal logic programs. The solution is simple and it amounts to replacing the negation as failure rule with an unconditional derivation rule. lfpF ♭ P and lfpF ⋄ P can be specialised for various analyses. An analysis can be thought of as a series of approximations of the operational semantics as shown below. An arrow from A to B reads as "A is approximated by B".

SLDNF VSLDNF
To specialise either lfpF ♭ P or lfpF ⋄ P for an analysis, one has to find out the corresponding abstract domain and corresponding concretisation function, to provide a function for computing abstract identity substitutions, a function for computing the least upper bounds, and a function for computing abstract unifications. The abstract domain and the concretisation function must satisfy C1-C2, the function for computing abstract identity substitutions must satisfy C3, and the function for computing abstract unifications must satisfy C4.
We deal with negation as failure by approximating SLDNF with a transition system. The way negation as failure is dealt with may be generalised to deal with built-in predicate !. Although, we have not dealt with other built-in predicates, we believe that the generic abstract semantics can be augmented to deal with these built-in predicates in the way they are dealt with in [3]. Proof: Let aρ ≡ a ′ and φρ ≡ φ ′ . If a ′ φ ′ and bψ unify then there is a substitution θ such that a ′ φ ′ θ ≡ bφθ. We have vars(a ′ ) ∩ dom(ψ) = ∅ and rang(ψ) ∩ dom(φ ′ ) = ∅ and vars(b) ∩ dom(φ ′ ) = ∅. Hence, a ′ ψφ ′ θ ≡ bψφ ′ θ. Therefore, aρ and b unify.
The following equation results from equation 42 and the definition of ρ 3 .
The following equation results from equation 45 and the definition of ρ 4 .
. By corollary 10.3, Aρ A and B unify, and We also have rang(ρ 1 Lemma 10.5 Let θ 1 and θ 2 be two substitutions and Va set of variables.
Lemma 10.6 Let E 1 and E 2 be two sets of equations, and θ 1 and θ 2 be two substitutions. If Proof: See [5] Proof of lemma 3.1 (p.8): VSLDNF and SLDNF deals with negative literals in the same manner. Therefore, it remains to prove for the cases where the leftmost literals are positive. The proof has two parts. The first part corresponds to procedure-entry and the second part to procedure-exit.