A General Framework for Semantics-based Bottom-up Abstract Interpretation of Logic Programs ^{∗}

Roberto Barbuti , Roberto Giacobazzi , Giorgio Levi Dipartimento di Informatica Università di Pisa Corso Italia 40, 56125 Pisa

{barbuti,giaco,levi}@di.unipi.it

in ACM Transactions on Programming Languages and Systems Vol 15, January 1993

Abstract

The theory of abstract interpretation provides a formal framework to develop advanced dataflow analysis tools. The idea is to define a non-standard semantics which is able to compute, in finite time, an approximated model of the program. In this paper we define an abstract interpretation framework based on a fixpoint approach to the semantics. This leads to the definition, by means of a suitable set of operators, of an abstract fixpoint characterization of a π-model associated with the program. Thus, we obtain a specializable abstract framework for bottom-up abstract interpretations of definite logic programs. The specialization of the framework is shown on two examples, namely ground dependence analysis and depth-k analysis.

Categories and Subject Descriptors: D.2.2 [Software Engineering]: Tools and Techniques; D.2.4 [Software Engineering]: Program Verification; D.3.1 [Programming Languages]: Formal Definitions and Theory - semantics; F.3.2 [Logic and Meaning of Programs]: Semantics of Programming Languages; I.2.3 [Artificial Intelligence]: Deduction and Theorem Proving - logic programming.

Keywords: Abstract interpretation, logic programming, program analysis.

1 Introduction

An abstract interpretation [13, 14] of a program is an approximation of its standard semantics on an abstract simpler, generally finite, domain. Its goal is to collect static (compile-time) information about the run-time behavior of a program (data-flow analysis), to be used by compilers (for error detection, code optimization [9, 11, 20, 36]) and, in general, by program manipulation systems [27]. An introduction to the subject of abstract interpretation in the field of logic and functional languages can be found in [1]. Abstract interpretation is inherently semantics sensitive. However, in many cases the result is an ad-hoc algorithm (see for example [8]). Alternatively, the abstract interpretation is explicitly based on a formal semantics definition.

∗This work has been supported by “Progetto Finalizzato Sistemi Informatici e Calcolo Parallelo” of C.N.R.

under grant n. 9100880.PF69 and by the Esprit Basic Research Action 3012 - Compulog.

The last approach (semantics-based abstract interpretation) is closer to the original approach [13] in which a specific semantics (collecting semantics) was defined in order to make possible the static dataflow analysis. Different semantics definition styles lead to different approaches to program analysis. In the case of logic programs, there exist mainly two approaches, namely top-down analysis and bottom-up analysis [46]. The most popular approach is the top-down one, which propagates the information in the same direction as SLD-resolution does. In this class we can find top-down ad-hoc algorithms, frameworks based on an operational semantics, and frameworks based on a denotational semantics [8, 9, 19, 43, 48, 46, 58, 35]. The bottom-up approach propagates the information as in the computation of the least fixpoint of the immediate consequences operator T_{P} [39, 60]. The idea of bottom-up analysis was first introduced in [45]. [48] uses a bottom-up analysis to reason about top-down computations. The main difference between the top-down and the bottom-up approach is related to goal dependence. In particular, the top-down analysis starts with a particular goal and it is able to determine call pattern information [46], that is information about specific procedure calls. On the other side, the bottom-up approach determines an approximation of the success set which is goal independent. As discussed in [46], there are applications for which each of the two approaches is the most adequate. In this paper we show that the area of applicability of the bottom-up approach can be extended with respect to the cases devised in [46].

The semantics definition underlying the bottom-up approach is related to the computation of the least fixpoint of the immediate consequences operator on Herbrand interpretations. However, the standard T_{P} operator, whose least fixpoint is the least Herbrand model, being defined on ground atoms only, does not allow to model correctly the concept of logical variable which is essential in describing properties like modes and aliasing [37, 45]. In [22, 23, 24] a model-theoretic and a fixpoint semantics is defined which capture (non-ground) computed answer substitutions. The corresponding immediate consequences operator operates on a domain composed of ground and non-ground atoms. This concrete semantics is used as the basis for our abstract interpretation framework. This semantics is both simpler than the denotational one and more typical for logic programming. Moreover, since it is able to deal with logical variables, allows to extend the scope of the bottom-up approach to problems like mode and aliasing analysis. Since the result is an abstraction of the least fixpoint, we obtain an approximation of the program success patterns. In the last part of the paper we discuss the use of success patterns to compute call patterns. The abstract interpretation framework is composed of two levels. A core level, shared by all the applications, defines an abstract T_{P} expressed in terms of a suitable set of abstract operators. These operators essentially play the role of similar ones in [9, 48, 35]. The specialization level defines the abstract operators for each specific application. The standard semantics can be viewed as a specialization of the abstract one. If the definitions of the abstract operators satisfy some properties, then the correctness of the specific analysis is guaranteed.

The paper is organized as follows. In the first part, the main concepts and results on the fixpoint semantics [23] are presented, together with a presentation of the abstract interpretation notions. Section 3 defines the abstract fixpoint semantics based on a suitable set of abstract operators. Section 4 introduces two specific applications, namely ground dependence and depth-k analysis. In section 5 the relation between our framework and other proposals on the same subject is discussed. Finally, in section 6 further extensions and applications of the general framework are presented.

2 Logic Programs and Abstract Interpretation

In this section we recall some notions about lattice theory [7], about the semantics of logic programs (as defined in [23]) and about the general theory of abstract interpretation (as defined in [1, 13]. The reader is assumed to be acquainted with the basic concepts of logic programming, an introduction to which can be found in [39].

2.1 Preliminaries

A set S together with a binary relation ≤ which is reflexive, antisymmetric and transitive (a partial-ordering) is called a poset and it is denoted by the pair (S, ≤). s ∈ S is an upper (lower) bound for a subset X ⊆ S iff x ≤ s (s ≤ x) for all x ∈ X. The subset X ⊆ S has a least upper bound (greatest lower bound) (denoted by lub(X) (glb(X))), iff for any other upper (lower) bound x′ of X, lub(X) ≤ x′ (x′ ≤ glb(X)). A poset (S, ≤) is a lattice iff lub(X) and glb(X) exist for every finite (non-empty) subset X ⊆ S. A poset (S, ≤) is a complete lattice iff for each subset X ⊆ S, there exist lub(X) and glb(X).

A set X is directed if every finite subset of X has an upper bound in X, that is if whenever A ⊆ X is finite then for each a ∈ A there exists b ∈ X such that a ≤ b. A function (defined on complete lattices) f : D → D′ is continuous if ∀X ⊆ D directed, f(lub_{D}(X)) = lub_{D′}{f(x) | x ∈ X}. A function f : D → D′ such that ∀X ⊆ D (possibly non-directed), f(lub_{D}(X)) = lub_{D′}{f(x) | x ∈ X} is said to be additive [59]. Obviously, additive functions are continuous.

Let F : S → S be a function defined on a complete lattice S. There exists a least fixpoint of F, x = lfp(F) ∈ S, iff F (x) = x and for all x′ ∈ S such that F (x′) = x′ we have x ≤ x′. Let D be a complete lattice and T : D → D be a monotonic function. The classical result on fixpoints due to Knaster-Tarski states that T has a least fixpoint lfp(T) = glb_{D}{x | T (x) = x} = glb_{D}{x | T (x) ≤ x}.

In the following, given a set S, we denote by |S| the number of elements in S and by S −{s} the set S where the element s has been removed.

A (one sorted) algebra is a pair (S, Op) (the signature) where S represents a set of elements and Op a specified set of operations with a ranking function ρ such that

∀f ∈ Op, f : S ×, ..., × S → S, ⇒ ρ(f) = n.

Operators σ ∈ Op such that ρ(σ) = 0 are usually called constants. Groups and lattices are families of algebras, each one satisfying a specified set of postulates [7].

The most important generalization of the algebraic lattice concept is provided by semilattices. An algebra with a single binary idempotent, commutative and associative operation is called a semilattice [7]. If we denote by ⊔ (join) and ⊓ (meet) the binary operations corresponding to the least upper bound and the greatest lower bound respectively, it follows that any lattice is both a join and a meet-semilattice.

A poset for which every subset has a least upper bound (greatest lower bound) is a complete join (meet) semilattice. Notice that any complete join-semilattice is a complete lattice.

Let X be a set, we denote by 2^{X} the powerset of X. 2^{X} with subset ordering is a complete lattice.

Let (S, Op) and (S′, Op′) be two algebras defined on the same signature (i.e. having the same operators structure). A function

f : S → S′

is an algebraic morphism iff • ∀σ ∈ Op | ρ(σ) = 0 : f(σ) = σ′

• ∀σ ∈ Op | ρ(σ) = n (n > 0), ∀a_{1}, ..., a_{n} ∈ S :

f(σ(a_{1}, ..., a_{n})) = σ′(f(a_{1}), ..., f(a_{n}))

A congruence relation on an algebra (S, Op) is an equivalence relation ≈ on S such that for each operator σ ∈ Op (ρ(σ) = n), and each pair of elements a_{i}, b_{i} ∈ S such that a_{i} ≈ b_{i}, i = 1, ..., n, the following relation holds

σ(a_{1}, ..., a_{n}) ≈ σ(b_{1}, ..., b_{n}).

The quotient algebra (S^{mod}, Op^{mod}) on (S, Op) modulo a congruence relation ≈ (denoted by (S, Op)/_{≈}) is defined as follows:

• S^{mod} = S/_{≈} (the set of equivalence classes on S),

• ∀σ ∈ Op | ρ(σ) = 0 : σ^{mod} = [σ]_{≈},

• ∀σ ∈ Op | ρ(σ) = n (n > 0), ∀a_{1}, ..., a_{n} ∈ S : σ^{mod}([a_{1}]_{≈}, ..., [a_{n}]_{≈}) = [σ(a_{1}, ..., a_{n})]_{≈}

where σ^{mod} denotes elements in Op^{mod} and [a]_{≈} denotes the equivalence class of a with respect to ≈ (i.e. [a]_{≈} = {a′ | a′ ≈ a}).

2.2 A semantics of Logic Programs adequate to Abstract Interpretation

The following results about the semantics of logic programs are defined in [22, 23]. The semantic definition in [22, 23] is closer than the one in [39, 60] to the operational behavior of logic programs, which was shown to require a more complex and appropriate notion of model, in general different from the minimal Herbrand model. The model theoretic and fixpoint semantics in [23] capture possibly non-ground computed answer substitutions. Such a semantic definition is then the right one in order to develop a bottom-up abstract interpretation framework, without requiring to extend the standard semantics with a somewhat artificial collecting semantics. A standard semantics able to characterize the operational behavior of logic languages can therefore be found inside the first order logic semantics (model-theoretic and fixpoint), by considering possibly non-initial models, having a richer information structure, like those giving a representation (usually finite by means of variables) of infinite sets of ground atoms. We have to consider a different notion of program equivalence [40], rich enough to model the useful information for program analysis, i.e. the observable properties of the operational semantics.

The extended Herbrand Universe contains also non-ground terms. Thus, it is possible to define a non-ground success set and to declaratively characterize the ability of logic programs to compute answer substitutions (which are non-ground in general).

Let us consider the set Cons of constructors, with typical elements a, b, c, ... (constructors with 0 arguments Cons_{0}), and f, g, h, ... (constructors with one or more arguments Cons_{n}, n > 0), and a denumerable set V ar of variables. The free Cons-algebra on V ar, T_{Cons}(V ar), is inductively defined as the least family such that:

• ∀c ∈ Cons_{0}, c ∈ T_{Cons}(V ar);

• ∀v ∈ V ar, v ∈ T_{Cons}(V ar);

• ∀t_{1} ∈ T_{Cons(V ar)}, ..., ∀t_{n} ∈ T_{Cons}(V ar), ∀d ∈ Cons_{n}, d(t_{1}, ..., t_{n}) ∈ T_{Cons}(V ar).

Notice that the standard Herbrand Universe is defined as T_{Cons}(∅), that is the set of all ground terms in the language.

We denote by t[x_{1}, ..., x_{n}] a term containing the symbols x_{1}, ..., x_{n} as variables. Moreover, in the following, we denote by ≡ the syntactic equivalence of objects.

The set of substitutions, with typical elements σ, ϑ, ... consists of all the mappings ϑ from V ar into T_{Cons(V ar)}, such that {x ∈ V ar | ϑ(x) ≠ x} is finite. ε denotes the empty substitution.

The application of a substitution ϑ to a term t (denoted tϑ) is defined as the term obtained by replacing each variable x in t by ϑ(x). The composition ϑσ of ϑ and σ is defined as function composition. We recall that the composition is associative and for each term t, t(ϑσ) ≡ (tϑ)σ. A renaming is a substitution ρ for which there exists the inverse ρ^{−1}, such that ρ∘ρ^{−1} = ρ^{−1}∘ρ = ε. A substitution ϑ′ is more general than ϑ (ϑ ≤ ϑ′), iff there exists σ such that ϑ = ϑ′σ.

The notion of unification can be given with respect to a set of equations. An equation is an expression of the form t = u, where t, u ∈ T_{Cons}(V ar). Given a set E of equations, E is unifiable iff there exists ϑ such that ∀(t = u) ∈ E, (tϑ) ≡ (uϑ). We denote by Unif(E) the (possibly empty) set of unifiers of E. We denote by mgu(E) the set {ϑ ∈ Unif(E) | ∀ϑ′ ∈ Unif(E) : ϑ ≤ ϑ′}. It is well known that all the most general unifiers of a set E are equivalent [21, 38].

Consider a program P and the set Cons_{P} of constructors of the first order language underlying P. The extended Herbrand Universe U_{P} is defined as T_{Cons_{P}} (V ar)/ ≈, i.e. the set of equivalence classes with respect to the variance relation ≈ (t_{1} ≈ t_{2} iff ∃ ϑ_{1}, ϑ_{2} | t_{1}ϑ_{1} = t_{2} ∧ t_{2}ϑ_{2} = t_{1}). Together with an added least element, it is a complete lattice with respect to the usual preorder on terms ≤ , such that t_{1} ≤ t_{2} iff ∃ϑ | t_{1} = t_{2}ϑ.

Let P red_{P} be the set of predicate symbols in the program P. An atom is an object of the form p(t_{1}, ..., t_{n}) where t_{1}, ..., t_{n} ∈ T_{Cons_{P}} (V ar) and p is an n-ary predicate symbol (i.e. p ∈ P red_{P}^{n}). We denote the set of atoms as Atoms. In the following, given two atoms A = p(t_{1}, ..., t_{n}) and A′ = p(t′_{1}, ..., t′_{n}), we denote by mgu(A, A′) an element in mgu({t_{i} = t′_{i} | i = 1, ..., n}). We extend this notation to any tuple of atoms.

A clause is a formula of the form

H : − B_{1}, ..., B_{n} with n ≥ 0

where H (the head) and B_{1}, ..., B_{n} (the body) are atoms and : − and “,” denote logic implication and conjunction respectively. The variables are assumed to be universally quantified. If the body is empty, the clause is a unite clause. A goal is a formula B_{1}, ..., B_{n} (denoted by ? − B_{1}, ..., B_{n}), where each B_{i} are atoms. A logic program is a finite set of clauses.

Given a term t ∈ T_{Cons}(V ar), the set of variables occurring in t is denoted by var(t) (in the following, with abuse of notation, we apply the var operator to atoms as well). We extend also the notion of variance ≈ to any syntactic object (i.e. terms, atoms, clauses, etc.).

In the following, an extended notion of interpretation (π-interpretation) is given [24, 26]. π-interpretations are more expressive than Herbrand interpretations because of the use of more syntactic objects (like variables) in the semantic domains.

Analogously to the standard semantics, the Base of π-interpretations B_{P} is defined as Atoms/ ≈. A π-interpretation I is a subset of B_{P} (it represents the set of atoms which are true in I).

Definition 2.1 [24] A π-interpretation I is a π-model for the logic program P iff every clause of P is true in the Herbrand interpretation G(I) (i.e. G(I) is a Herbrand model for P), where G(I) represents the set of ground instances of atoms in I.

In positive logic programs, the operational semantics is a set of possibly non-ground atoms. The notion of π-model is general enough to capture the observable operational behavior of a logic program as a π-model. Moreover, every Herbrand model is still a π-model. However, the model intersection property does not hold in general for π-models, i.e. the information of a π-interpretation I_{1} may be contained in I_{2} without I_{1} being a subset of I_{2}.

Definition 2.2 [24] Let I_{1} and I_{2} be π-interpretations. Let ⪯ be defined as follows

• I_{1} ≤ I_{2} iff ∀A ∈ I_{1}, ∃A′ ∈ I_{2} such that A ≤ A′.

• I_{1} ⪯ I_{2} iff (I_{1} ≤ I_{2}) and (I_{2} ≤ I_{1} implies I_{1} ⊆ I_{2}).

Intuitively, I_{1} ≤ I_{2} means that every atom verified by I_{1} is also verified by I_{2} and I_{1} ⪯ I_{2} means that either I_{2} contains more information than I_{1} or if they have the same information, then I_{1} expresses it by less elements.

Using this extended semantic definition, it is possible to prove [24, 26] that, given a logic program P,

• the set of π-interpretations is a complete lattice with respect to set-inclusion,

• let W be a set of π-models of P, then glb_{⪯}(W) is a π-model for P,

• the set of π-models is a complete lattice with respect to ⪯, where the least model M_{P} is the least Herbrand model.

As we have observed, in the new semantics definition the least Herbrand model is still the least model. However, if we are interested in computed answer substitutions, the least Herbrand model is not satisfactory. Thus, in order to capture such operational behaviors, we have to consider non-minimal π-models.

We introduce now an immediate consequences operator T_{P} on π-interpretations whose least fixpoint is a non-minimal π-model which is able to capture computed answer substitutions.

Definition 2.3 (immediate consequences operator) [22, 23] Given a logic program P, the operator T_{P} on the set of π-interpretations associated with P is defined as follows

T_{P} (I) = { A′ ∈ B_{P} |

∃ C ≡ A : −B_{1}, ..., B_{n} ∈ P

∃ (B′_{1}, ..., B′_{n}) ∈ I

with no variables in common with C and with each other, ∃ϑ = mgu((B_{1}, ..., B_{n}), (B′_{1}, ..., B′_{n})) and A′ = Aϑ }.

This definition is different with respect to the standard T_{P} operator [60]. It derives possibly non-ground atoms by means of a bottom-up inference rule which is based on unification, as in the top-down SLD resolution.

As usual, T_{P} is a continuous function on the complete lattice of π-interpretations ordered by set-inclusion [23]. The following definition gives a fixpoint characterization of the program semantics. In the following we use T_{P} ↑ α as a notation for ∪_{n∈α} T_{P}^{n}(∅), where α is a set of finite ordinals and ω denotes the set of all the finite ordinals.

Definition 2.4 (fixpoint semantics F(P)) [22, 23] For every program P, F(P) = lfp(T_{P}) = T_{P} ↑ ω.

We observe that each π-interpretation I such that T_{P} (I) ⊆ I is a π-model for P. Moreover, F(P) is a π-model as well.

The two most important results which characterize the relation between the new fixpoint semantics and the operational one (the equivalence between fixpoint and operational semantics) are the strong soundness and the strong completeness theorems given below. They show that F(P) is the fully abstract semantics with respect to computed answer substitutions. Previous attempts of defining bottom-up abstract interpretations failed on non-trivial analyses (like mode analysis) since they were based on an immediate consequence operator leading to a fixpoint semantics which did not model computed answer substitutions [45, 46].

In the following G →_{P}^{∗}^{ϑ} □ denotes a refutation for a given goal G, with answer substitution ϑ, while ϑ_{|G} is the restriction of the substitution ϑ to the variables occurring in G, extended as an identity for each variable x ∈ var(G) such that ϑ(x) is undefined.

Theorem 2.1 (Strong Soundness) [22, 23]

Let P be a logic program and let G be a goal ? − B_{1}, ..., B_{n}. Assume that G →_{P}^{∗}^{ϑ} □, then ∃ B′_{1}, ..., B′_{n} ∈ F(P) and ∃ ϑ′ = mgu((B_{1}, ..., B_{n}), (B′_{1}, ..., B′_{n})) such that ϑ′_{|G} = ϑ_{|G}.

Theorem 2.2 (Strong Completeness) [22, 23] Let P be a logic program and let G be a goal ? − B_{1}, ..., B_{n}. If ∃ B′_{1}, ..., B′_{n} ∈ F(P) and

∃ ϑ′ = mgu((B_{1}, ..., B_{n}), (B′_{1}, ..., B′_{n})), then ∃ ϑ such that G →_{P}^{∗}^{ϑ} □ and ϑ′_{|G} = ϑ_{|G}.

2.3 Abstract Interpretation

We now formalize the notion of abstract interpretation according to the ideas given by Cousot and Cousot [13]. Let us consider a concrete domain D_{P} (a set of computational state representations associated with the generic program P) which is a complete lattice with respect to a partial order relation ≤_{D_{P}}, and a state transition function E_{P}, defined on D_{P}. Let us assume the program computational behavior being fully characterized by a solution of the recursive equation x = E_{P} (x). Thus we can state that (D_{P} , ≤_{D_{P}} , E_{P}) defines a standard fixpoint semantics for the program P. Since computations can be infinite, the above definition cannot be used for static program analysis. Therefore we define a non-standard fixpoint semantics based on an abstract (usually finite) domain D_{P}^{♯}, called abstract semantics (D_{P}^{♯} , ≤_{D_{P}}^{♯} , E_{P}^{♯}) to guarantee the effectiveness of the analysis. Obviously, this kind of analysis is less precise than the one given by the complete semantics definition. According to the notation of Mycroft [52], in the following we denote by O^{♯} the abstract analog of any concrete syntactic object O.

The relation between the standard and the abstract semantics was established in [13] by defining a pair of functions α and γ (abstraction and concretization), which form a Galois connection between (D_{P}^{♯} , ≤_{D_{P}}^{♯}) and (D_{P} , ≤_{D_{P}}) [33, 49, 54]. This notion allows us to formally handle the correctness condition on the abstract interpretation framework [5]. Formally, an abstract interpretation scheme [13, 45] is a tuple

⟨(D_{P} , ≤_{D_{P}}) , E_{P} , (D_{P}^{♯} , ≤_{D_{P}}^{♯}) , E_{P}^{♯} , α , γ⟩

such that

1. (D_{P} , ≤_{D_{P}}) and (D_{P}^{♯} , ≤_{D_{P}}^{♯}) are complete lattices, 2. E_{P} : D_{P} → D_{P} and E_{P}^{♯} : D_{P}^{♯} → D_{P}^{♯} are monotonic functions,

3. α : D_{P} → D_{P}^{♯} (abstraction) and γ : D_{P}^{♯} → D_{P} (concretization) are monotonic functions,

4. ∀ d^{♯} ∈ D_{P}^{♯} , α(γ(d^{♯})) ≤_{D_{P}^{♯}} d^{♯},

5. ∀ d ∈ D_{P} , d ≤_{D_{P}} γ(α(d)).

The last three conditions define a Galois connection between the abstract domain and the concrete one. A Galois insertion is a connection where γ is one-to-one (injective) or equivalently when the composition α∘γ is the identity on D_{P}^{♯} [49, 54]. We note that in any Galois connection, α is surjective iff γ is one-to-one [49].

Galois connections give us the formal framework to prove correctness of an abstract interpretation. They define a strong relationship between the concrete domain of computations and the abstract, usually simpler, domain associated with the analysis. Their usefulness was outlined in [13, 14] as a base to develop soundness conditions for semantics-based analysis of flowchart programs.

Galois insertions ensure that the domain D_{P}^{♯} (the abstract domain of computation) does not contain redundant elements. According to conditions 4 and 5, the concretization cannot cause any loss of information, while the abstraction of a concrete object may cause some loss of information [13].

Given a Galois connection ⟨α, γ⟩ on the lattices (D_{P} , ≤_{D_{P}}) and (D_{P}^{♯} , ≤_{D_{P}}^{♯}), the following statements hold [33, 49, 54].

• abstraction and concretization uniquely determine each other,

• γ preserves arbitrary meets, that is ∀ B^{♯} ⊆ D_{P}^{♯} , glb_{≤_{D_{P}}} \{γ(d^{♯}) | d^{♯} ∈ B^{♯}\} = γ(glb_{≤_{D{♯ \atop P}}} B^{♯}),

• α preserves arbitrary joins (i.e. α is additive), that is ∀ B ⊆ D_{P} , lub_{≤_{D{♯ \atop P}}} \{α(d) | d ∈ B\} = α(lub_{≤_{D_{P}}} B).

The program analysis is done by computing a (finite) Kleene sequence

{E_{P}^{♯^{n}}(⊥_{D_{P}^{♯}})}_{n∈{1,...,k}}

of finitely computable approximations of the semantic solution of the recursive equation x = E_{P} (x). The correctness of such an approximation can be given by one of the following correctness conditions [13, 14]:

• ∀ d ∈ D_{P} : α(E_{P} (d)) ≤_{D_{P}^{♯}} E_{P}^{♯} (α(d)),

• ∀ d^{♯} ∈ D_{P}^{♯} : E_{P} (γ(d^{♯})) ≤_{D_{P}} γ(E_{P}^{♯} (d^{♯})).

Proposition 2.3 [13] ∀d ∈ D_{P} : α(E_{P} (d)) ≤_{D_{P}^{♯}} E_{P}^{♯} (α(d)) ⇒ ∀d^{♯} ∈ D_{P}^{♯} : E_{P} (γ(d^{♯})) ≤_{D_{P}} γ(E_{P}^{♯} (d^{♯})).

The viceversa holds iff α is a surjective map (i.e. ⟨α, γ⟩ is a Galois insertion). In the Galois insertion hypothesis, the previous correctness conditions are equivalent.

In the following section we use the previous notions to define an abstract interpretation scheme for logic programs based on a fixpoint characterization of the concrete semantics.

3 Abstract Semantics

In this section we develop, starting from the fixpoint semantics of section 2.2, an abstract semantics scheme for logic programs, which can be specialized to various kinds of bottom-up abstract interpretations. The presentation is organized in two sections. The first one introduces the abstract domains and the associated abstract operators, while the second one describes the fixpoint abstract semantics.

3.1 Basic Notions

“Each method of giving a semantics to programs induces a, possibly different, equivalence relation on programs” [40]. In the standard semantics of logic programs, the observable properties are the computed answer substitutions. As a consequence, the semantics construction (both in the operational and fixpoint case) leads to a denotation (set of atoms), which can then be used to characterize the observable property (i.e. computed answer substitutions), by means of a unification process between goals and atoms in the denotation.

The same situation arises in the abstract semantics case. In order to define an abstract semantics for logic programs we have to consider how to approximate the concrete equivalence relation on logic programs, based on the computed answer substitution. Abstract atoms represent approximations of concrete program denotations, with respect to a given program property. Thus, in order to define a general semantics-based analysis framework, the notion of observable property of the semantics has to be defined. Abstract substitutions will be introduced for this purpose, to have an approximation of observable program properties, that is how variables are instantiated. This will be obtained by means of an abstract unification process of a concrete goal (the current program query) with abstract atoms in an approximated model for the program. This approach is not considered in [37], thus failing in capture the abstract program observable properties (i.e. abstract substitutions). However, the abstract model fails to be captured by a semantics definition based only on the notion of abstract substitution. Thus, in order to define an abstract fixpoint semantics for logic programs, we introduce both the notion of abstract atom and the notion of abstract substitution, corresponding to abstract program denotations and abstract observable properties respectively.

Let P be a definite logic program defined on a first order logic language, based on the ⟨P red, Cons, V ar⟩ alphabet, and T_{Cons}(V ar) be the concrete universe of terms.

The definition of abstract domains for program analysis is often a hard step in the abstract interpretation definition. The systematic approach given in [14] can be applied to logic programming obtaining elegant techniques to define abstract domains. These techniques can always be summarized by a suitable notion of data equivalence [16, 19].

In the following we develop a step-by-step approach to the abstract domain definition. The main problem is what we want to observe from concrete data behavior and how the resulting abstract data are represented in order to have an efficient (concise) data-flow analysis. The abstract domain construction is given in terms of abstract objects which are equivalence classes with respect to an equivalence relation induced by the data-flow observable properties. Thus, in order to suitably define an abstract domain for a given program analysis, three abstraction levels are presented, each one related with a different analysis environment. In the first one, the abstraction is performed on terms in order to summarize all and only those properties which are useful for the term analysis. The second step deals with how abstract terms are collected together (in abstract atoms) and which properties of their union the analysis is interested in. Finally, in the third step the notion of abstract π-interpretation is introduced. It corresponds to choosing which properties we want to observe, collecting together different abstract atoms.

These levels correspond to suitable equivalence notions on the related concrete domains (i.e. the universe of terms, atoms and interpretations). Their structure strongly depends on the kind of analysis we want to perform on the program.

3.1.1 Abstract universe

The abstract domain of terms is a set of abstract terms each one summarizing a specific term property. The properties of terms we want to observe induce an equivalence relation on the concrete set of terms T_{Cons}(V ar). By means of the equivalence relation, denoted by ≈_{t}, the abstract universe is T_{Cons}(V ar)/ ≈_{t}. It is the set of equivalence classes with respect to ≈_{t}. Working with equivalence classes is usually unpractical. Thus we denote by U_{P}^{♯} a set of equivalence classes denotations, t^{♯}, which is isomorphic to the quotient set T_{Cons}(V ar)/ ≈_{t}, by means of an isomorphism χ_{t}.

There are many examples in the literature on a suitable partitioning of the universe of terms, like the modes domain in [48].

Example 3.1 Consider the logic program

p(succ(x)) : −p(x).
p(0).
p(a).

The observable property for the type analysis is the type structure of terms. Given the type specification for terms

• 0 : nat

• succ(x) : \{ \begin{matrix}nat & if x : nat \\ err & otherwise \end{matrix}

• a : char

the equivalence relation for type analysis states that two terms are equivalent if they have the same type structure. In this case succ(succ(0)) ≈_{t} 0. The abstract universe of terms is the set of equivalence classes denotations U_{P}^{♯} = {nat, char, err}. In the abstract universe, terms are then approximated by their type structure. An extension to type polymorphism, by a suitable partitioning of the universe of terms, is presented in [3].

The abstract domain of terms can be a non-flat one. If variables are considered [3] the partial ordering relation ≤ (less instantiated than) on concrete terms (up to renaming) can be abstracted in order to define a partial ordering relation ≤^{♯} on abstract terms too.

3.1.2 Abstract base

The abstract base of atoms Atoms^{♯} represents the set of atoms instantiated over the abstract universe.

Definition 3.1 Atoms^{♯} = {p(t_{1}^{♯}, ..., t_{n}^{♯}) | p ∈ P red_{P}^{n} ∧ (t_{1}^{♯}, ..., t_{n}^{♯}) ∈ U_{P}^{♯^{n}}}.

The problem of how abstract information is represented is central in abstract interpretation. Program analysis often requires to capture the interaction between abstract terms, like sharing and functional dependences [28, 30, 31, 32, 50, 61]. An equivalence relation on abstract atoms ≈_{A} characterizes such properties.

Example 3.2 Let us consider the abstract universe of terms defined with respect to the following equivalence relation t_{1} ≈_{t} t_{2} iff var(t_{1}) = var(t_{2}). In ground dependence analysis (see Section 4 for more details), the observable properties are related with the shared variables between terms. Thus the abstract atoms

p(f(x, y), x) and p(g(x′, y′, z′), f(x′, y′))

characterize the same observable properties, i.e. the groundness of the first argument implies the groundness of the second one. Thus, they are equivalent with respect to the ground dependence notion.

As usual, we denote by B_{P}^{♯} a set of equivalence classes denotations which is isomorphic to Atoms^{♯}/_{≈_{A}}, and by χ_{A} the corresponding isomorphism.

3.1.3 Abstract domain of interpretations

The abstract domain of interpretations defined in terms of the powerset of the abstract base (2^{B_{P}^{♯}} , ⊆) is usually not concise enough to represent abstract information. In some applications, as an example, the analysis returns at most one success pattern per program clause [10] or per predicate symbol [19, 47]. This assumption is reasonable if we assume that in most of the real programs, specific predicate arguments are used with the same mode or type structure. As shown in [18], this technique may lead to a considerable simplification in the analysis complexity.

Example 3.3 Consider an analysis which tries to infer the type of the arguments of a predicate symbol p, for all the atoms belonging to the success set of the following simple logic program P

p(x).
p(0).

The abstract universe of terms is the two element domain {τ, nat}, where τ is a type variable. The domain is ordered by instantiation (i.e. nat ≤_{type} τ).

The analysis of the program results in the type “nat” and “τ” (the type variable τ says that the argument of p can be a term of any type). The information collected in the interpretation {p(nat), p(τ)} is redundant since p(τ) subsumes p(nat).

In order to define the concept of abstract π-interpretation, we consider an algebraic generalization of the standard lattice associated with the concrete semantics.

The idea is to consider the least algebraic structure which captures the notion of composition of interpretations. In the complete lattice of concrete π-interpretations (2^{B_{P}} , ⊆) the composition of interpretations is modeled by set union.

Let us consider the join-semilattice (2^{B_{P}^{♯}} , ∪) with ∅ as identity, and a congruence relation ≈_{I} on the corresponding algebraic system.

Let (2^{B_{P}^{♯}} , ∪)/_{≈_{I}} be the quotient join-semilattice on (2^{B_{P}^{♯}} , ∪), modulo ≈_{I}. As stated in the preliminary section, the abstract join operator is defined in the obvious way as the equivalence class of the interpretation set union, that is

∀I_{1}, I_{2} ∈ 2^{B_{P}^{♯}} , [I_{1}]_{≈_{I}} ∪_{≈_{I}} [I_{2}]_{≈_{I}} = [I_{1} ∪ I_{2}]_{≈_{I}}.

Let (H_{P} , α-⊔) be a domain of denotations I^{♯}, isomorphic to (2^{B_{P}^{♯}} , ∪)/_{≈_{I}} by means a translation map (an isomorphism) χ_{I}, where the abstract union α-⊔ is interpreted in the obvious way as ∪_{≈_{I}}.

Example 3.4 In the previous example, the join of the two types τ and nat would result in τ (because the variable subsumes the type “natural”). The corresponding congruence relation is induced by the preorder ⪯ on interpretations:

∀I_{1}^{♯}, I_{2}^{♯} ∈ 2^{B_{P}^{♯}} . I_{1}^{♯} ⪯ I_{2}^{♯} iff

∀A ∈ I_{1}^{♯}, ∃A′ ∈ I_{2}^{♯} such that A ≤_{type} A′

(where ≤_{type} can be extended on atoms in the obvious way).

The representative elements in each equivalence class are the minimal ones (w.r.t. the number of elements). Thus, since {p(τ), p(nat)} ≈_{I} {p(τ)},

H_{P} = {{p(τ)}, {p(nat)}}.

Obviously, we may be interested in collecting all the type information. In this case, the congruence relation is simply the identity. As a consequence, H_{P} = 2^{B_{P}^{♯}}.

Definition 3.2 An abstract π-interpretation is an element in H_{P}.

Again, the congruence relation depends on the kind of analysis to be performed on the program. The join operator implements the composition of abstract π-interpretations. H_{P} denotes the set of abstract π-interpretations associated with the first-order logic language of the program P. Each abstract π-interpretation represents the set of abstract atoms which contain useful information from the analysis viewpoint. The corresponding join-semilattice

(H_{P} , α-⊔)

represents the least algebraic structure which models the composition of π-interpretations into the abstract framework. The abstract union, α-⊔, gives us the ability of composing abstract π-interpretations, to obtain a new abstract π-interpretation (which contains the information present in both its arguments).

The ordering relation induced by the abstraction process ≤_{α} is naturally defined in terms of the abstract union operator,

∀I_{1}^{♯}, I_{2}^{♯} ∈ H_{P} , I_{1}^{♯} ≤_{α} I_{2}^{♯} iff I_{1}^{♯}α-⊔I_{2}^{♯} = I_{2}^{♯}.

In the following we will assume that H_{P} is a finite set. This assumption will ensure the effectiveness of the analysis.

Proposition 3.1 α-⊔ is idempotent, commutative and associative.

Proof. It follows trivially from the congruence relation properties. □

Proposition 3.2 α-⊔ is monotonic on both its arguments.

Proof. Let us consider two abstract π-interpretations I_{1}^{♯} and I_{2}^{♯} such that I_{1}^{♯} ≤_{α} I_{2}^{♯}. For each I^{♯} ∈ H_{P}, by the commutative and associative property, inherited by the set union

(I^{♯}α-⊔I_{1}^{♯})α-⊔(I^{♯}α-⊔I_{2}^{♯}) = (I^{♯}α-⊔I^{♯})α-⊔(I_{1}^{♯}α-⊔I_{2}^{♯}) = (I^{♯}α-⊔I_{2}^{♯}).

Thus (I^{♯}α-⊔I_{1}^{♯}) ≤_{α} (I^{♯}α-⊔I_{2}^{♯}). □

Proposition 3.3 (H_{P} , ≤_{α}) is a complete lattice.

Proof. (H_{P} , ≤_{α}) is a finite join-semilattice. Since χ_{I}([∅]_{≈_{I}}) ∈ H_{P} and ∀I^{♯} ∈ H_{P}, χ_{I}([∅]_{≈_{I}}) ≤_{α} I^{♯}, and H is a finite domain, (H_{P} , ≤_{α}) is a complete lattice [7]. □

3.1.4 Abstract substitutions

In order to model abstract observable properties we have also to reconsider the substitution notion within the abstract framework. An abstract substitution or α-substitution ϑ^{♯} is a mapping from a finite set of variables into U_{P}^{♯},

ϑ^{♯} : V → U_{P}^{♯}.

An abstract substitution is represented as a tuple of bindings ⟨t_{1}^{♯}/x_{1}, ..., t_{n}^{♯}/x_{n}⟩ where the set of variables {x_{1}, ..., x_{n}} is denoted by Dom(ϑ^{♯}). Notice that abstract substitutions are not required to be idempotent.

Given a finite set V_{n} of variable symbols {x_{1}, ..., x_{n}} such that x_{i} ≠ x_{j} for each i ≠ j, Subst_{V_{n}}^{♯} denotes the set {⟨t_{1}^{♯}/x_{i_{1}}, ..., t_{k}^{♯}/x_{i_{k}}⟩ | t_{1}^{♯}, ..., t_{k}^{♯} ∈ U_{P}^{♯} ∧ {x_{i_{1}}, ..., x_{i_{k}}} ⊆ V_{n}}. Thus, Subst_{V_{n}}^{♯} consists of k-tuples of bindings, k ≤ n, defined on the same set of variables. We extend this notation to the concrete case denoting by Subst_{V_{n}} the set {⟨t_{1}/x_{i_{1}}, ..., t_{k}/x_{i_{k}}⟩ | t_{1}, ..., t_{k} ∈ T_{Cons}(V ar) ∧ {x_{i_{1}}, ..., x_{i_{k}}} ⊆ V_{n}}.

The previous results about abstract atoms can easily be extended to abstract substitutions. In fact, given a finite set of variables V_{n}, Subst_{V_{n}}^{♯} can be viewed as a set of abstract atoms instantiated over the abstract universe of terms, having a different predicate symbol (of arity k), for each V′_{k} ⊆ V_{n}. As a consequence, the results obtained for abstract atoms can be extended in order to handle abstract substitutions too.

We can deal with a finite set of variables because we are using a bottom-up approach. In fact, using this kind of analysis the meaningful substitutions are those dealing with the variables occurring in program clauses (whose number is finite). Obviously, in order to preserve the correctness of the approach, it is necessary to consider the set of variables in the abstract domain as different from the set of variables in the concrete domain. Furthermore, we have to restrict the domain of abstract substitutions to the mappings V → U_{P}^{♯}, where V is the set of variables occurring in the concrete domain and the variables occurring in U_{P}^{♯} (if any) belong to the abstract domain.

An equivalence relation ≈_{S} on abstract substitutions is defined to capture the observable properties of these mappings. This equivalence relation plays the same role as ≈_{A} in the abstract atom case. As in the abstract atom case, we denote by S_{V}^{♯} a domain of denotations isomorphic to Subst_{V_{n}}^{♯}, by means of an isomorphism map χ_{S}.

Once we have chosen a finite set of variables V, let us consider the powerset of (equivalence classes of) abstract substitutions defined on this set of variables, 2^{S_{V}^{♯}}. In analogy to the definition of the set H_{P}, let (Σ_{V} , α-⊔_{Φ}) be a domain isomorphic to the quotient join-semilattice defined on (2^{S_{V}^{♯}} , ∪) modulo a congruence relation ≈_{Φ}, modeling the same observable properties as ≈_{I}. Given a finite set of variables V, we assume that Σ_{V} is a finite set.

Example 3.5 In a type analysis application (see Example 3.3 and 3.4), let

Φ_{1}^{♯} = {⟨τ/x, nat/y⟩, ⟨nat/y⟩} and Φ_{2}^{♯} = {⟨τ/x, τ′/y⟩, ⟨nat/y⟩}

be two sets of abstract substitutions, in 2^{S_{{x,y}}^{♯}}. As shown in the previous example, ⟨τ/x, τ′/y⟩ subsumes ⟨τ/x, nat/y⟩.

In this case we can consider the sets of abstract substitutions Φ_{1}^{♯} and Φ_{2}^{♯} as sets of abstract atoms defined on two different predicate symbols, the first on {x, y} (of arity 2), and the second on {y} (of arity 1). The extension of the congruence relation on abstract π-interpretations to sets of abstract substitutions is straightforward.

In the following Φ^{♯} will denote the elements in Σ_{V}, for a given finite set of variables V. They are called α-sets of abstract substitutions.

In analogy to the case of abstract π-interpretations, the ordering ≤_{Φ} is defined in terms of an abstract set-union operator on Σ_{V},

∀Φ_{1}^{♯}, Φ_{2}^{♯} ∈ Σ_{V} , Φ_{1}^{♯} ≤_{Φ} Φ_{2}^{♯} iff Φ_{1}^{♯}α-⊔_{Φ}Φ_{2}^{♯} = Φ_{2}^{♯}.

The proofs of the following propositions are similar to those given for the abstract atoms case.

Proposition 3.4 α-⊔_{Φ} is monotonic on both its arguments.

Proposition 3.5 Let V be a finite set of variables, (Σ_{V} , ≤_{Φ}) is a complete lattice.

In the following we will denote by ∅ the abstract objects χ_{I}([∅]_{≈_{I}}) and χ_{Φ}([∅]_{≈_{Φ}}).

3.1.5 Galois connection

Since the definition of the abstract domain for the analysis depends on a suitable equivalence on the corresponding concrete domain of computation, we impose some constraints in the equivalence choice, in order to have a systematic approach to the analysis correctness. The first constraint deals with finiteness of the quotient domains, while the second deals with correctness.

The relation between the concrete (infinite) lattice of interpretations (2^{B_{P}} , ⊆) and the corresponding abstract (finite) one (H_{P} , ≤_{α}), and between (2^{Subst_{V}} , ⊆) and (Σ_{V} , ≤_{Φ}) is established by defining two Galois connections, ⟨α, γ⟩ and ⟨α_{Φ}, γ_{Φ}⟩ respectively.

Proposition 3.6 α = λI.χ_{I}([{χ_{A}([p(t_{1}^{♯}, ..., t_{n}^{♯})]_{≈_{A}}) | p(t_{1}, ..., t_{n}) ∈ I ∧ t_{i}^{♯} = χ_{t}([t_{i}]_{≈_{t}})}]_{≈_{I}}) is a join-morphism between the join-semilattices (2^{B_{P}} , ∪) and (H_{P} , α-⊔).

Proof. α is a join-morphism, that is α(I_{1} ∪ I_{2}) = α(I_{1})α-⊔α(I_{2}). This trivially follows from the α-⊔ definition. Notice that α(∅) = χ_{I}([∅]_{≈_{I}}), and, since α corresponds to the definition process for the abstract domain H_{P}, by an abuse of notation, H_{P} = α(2^{B_{P}}), that is α is a surjective map. □

Proposition 3.7 The pair of functions ⟨α, γ⟩ defined as follows

α = λI.χ_{I}([{χ_{A}([p(t_{1}^{♯}, ..., t_{n}^{♯})]_{≈_{A}}) | p(t_{1}, ..., t_{n}) ∈ I ∧ t_{i}^{♯} = χ_{t}([t_{i}]_{≈_{t}})}]_{≈_{I}}),
γ = λI^{♯}. ∪ {I | α(I) ≤_{α} I^{♯}}

is a pair of monotonic functions between (H_{P} , ≤_{α}) and (2^{B_{P}} , ⊆) such that

∀I ∈ 2^{B_{P}} : I ⊆ γ(α(I)).

Proof.

• α is monotonic. Let I_{1} ⊆ I_{2} then, {[p(t_{1}^{♯}, ..., t_{n}^{♯})]_{≈_{A}} | p(t_{1}, ..., t_{n}) ∈ I_{1} ∧ t_{i}^{♯} = χ_{t}([t_{i}]_{≈_{t}})} ⊆ {[p(t_{1}^{♯}, ..., t_{n}^{♯})]_{≈_{A}} | p(t_{1}, ..., t_{n}) ∈ I_{2} ∧ t_{i}^{♯} = χ_{t}([t_{i}]_{≈_{t}})}. Thus α(I_{1})α-⊔α(I_{2}) = α(I_{2}).

• γ is monotonic. Let I_{1}^{♯}α-⊔I_{2}^{♯} = I_{2}^{♯}. Then

γ(I_{1}^{♯}) = ∪{I | α(I)α-⊔I_{1}^{♯} = I_{1}^{♯}}, and γ(I_{2}^{♯}) = ∪{I | α(I)α-⊔I_{2}^{♯} = I_{2}^{♯}}.

The following set-inclusion is straightforward

{I | α(I)α-⊔I_{1}^{♯} = I_{1}^{♯}} ⊆ {I | α(I)α-⊔I_{2}^{♯} = I_{2}^{♯}}

and then the thesis follows.

• Let I ∈ 2^{B_{P}}, then I ⊆ γ(α(I)) holds trivially by definition of γ.

□

The same properties hold for the pair of functions ⟨α_{Φ}, γ_{Φ}⟩,

α_{Φ} = λΦ.χ_{Φ}([\{ χ_{S}([⟨t_{1}^{♯}/x_{1}, ..., t_{n}^{♯}/x_{n}⟩]_{≈_{S}}) | \begin{matrix}⟨t_{1}/x_{1}, ..., t_{n}/x_{n}⟩ ∈ Φ \\ t_{i}^{♯} = χ_{t}([t_{i}]_{≈_{t}}) \end{matrix} \}]_{≈_{Φ}}),

γ_{Φ} = λΦ^{♯}. ∪ {Φ | α_{Φ}(Φ) ≤_{Φ} Φ^{♯}}.

Thus, the specialization of the abstract interpretation scheme requires the definition of the abstract domains of interpretations and substitutions to obtain a corresponding Galois connection between abstract and concrete domains. This can be reduced to proving α(γ(I^{♯})) ≤_{α} I^{♯} and α_{Φ}(γ_{Φ}(Φ^{♯})) ≤_{α} Φ^{♯}. In particular, since α is a surjective map, the previous condition can be reduced to proving [33, 49, 54]

α(γ(I^{♯})) = I^{♯} and α_{Φ}(γ_{Φ}(Φ^{♯})) = Φ^{♯}

that is ⟨α, γ⟩ and ⟨α_{Φ}, γ_{Φ}⟩ are Galois insertions.

In Figure 3.1, the abstract domains design is shown. The horizontal arrows are analysis dependent definitions (the equivalence relation ≈ denoting variance can be viewed as an abstraction process on syntactic terms in atoms and substitutions) while the vertical ones correspond to standard definitions, involving no abstraction.

[figure: T_{Cons}(V ar); Atoms; B_{P}; 2^{B_{P}}; Subst_{V}; S_{V}; 2^{S_{V}}; U_{P}^{♯}; Atoms^{♯}; Subst_{V}^{♯}; B_{P}^{♯}; S_{V}^{♯}; 2^{S_{V}^{♯}}; 2^{B_{P}^{♯}}; Σ_{V}; H_{P}; ≈_{t}; ≈_{A}; ≈_{S}; ≈_{I}; ≈_{Φ}; ≈; ≈]

Figure 3.1. The abstract domains definition

We can specify an abstract fixpoint semantics for logic programs based on the abstract domains ⟨(H_{P} , ≤_{α}), (Σ_{V} , ≤_{Φ})⟩. A suitable set of abstract operators has to be defined in order to develop a general scheme for semantics-based analysis of logic programs.

3.1.6 Abstract operators

In order to pass information from the concrete to the abstract framework we have to define the abstract unification notion. This process takes two n-tuples of abstract and concrete atoms respectively and returns an abstract substitution defined on the variables of the concrete atoms. Since the immediate consequence operator returns the heads of the clauses instantiated by the set of substitutions obtained by unifying the corresponding clause body with atoms in an interpretation, we will consider a cumulative version (collecting sets of abstract substitutions) of the abstract unification process. This approach leads to a cleaner definition of the properties (like correctness) that the abstract operators have to satisfy.

The abstract unifier of a conjunction of concrete atoms into an abstract π-interpretation

α-mgu : B_{P}^{n} × H_{P} → Σ_{V} ∪ {F ail}

takes an n-tuple of concrete atoms and an abstract π-interpretation, and returns an α-set of abstract substitutions which is defined on the set of variables of the concrete atoms. It represents the abstract substitutions returned by α-unifying the concrete atoms with the atoms inside the interpretation. The following axioms have to be satisfied

• ∀B_{1}, ..., B_{n} ∈ B_{P} , α-mgu(B_{1}, ..., B_{n}, ∅) = {F ail}, • ∀I^{♯} ∈ H_{P} , α-mgu(∅, I^{♯}) = ∅.

The notion of α-unification is left unspecified and it is the most important aspect of the specialization process. We only require that ∀Φ^{♯} ∈ Σ_{V} , {F ail} ≤_{Φ} Φ^{♯}. Given an α-set of abstract substitutions Φ^{♯}, we have to define how these substitutions are applied to a concrete atom. The abstract application of a set of abstract substitutions to a concrete atom

α-apply : B_{P} × Σ_{V} → H_{P}

returns an abstract π-interpretation containing the abstract atoms corresponding to the “application” of each abstract substitution represented in Σ_{V}, to the concrete atom. As in the previous case, the axioms are

• ∀A ∈ B_{P} | var(A) ∩ V = ∅, α-apply(A, Φ_{V}^{♯}) = α({A}),

• ∀A ∈ B_{P} , α-apply(A, {F ail}) = ∅.

3.2 Abstract Fixpoint Semantics

We can now define an abstract fixpoint semantics based on the set of abstract operators

{α-⊔, α-mgu, α-apply}.

In the following we list a set of properties that the abstract operators have to satisfy. These properties are related to two different aspects. The first one concerns monotonicity and allows the definition of a monotonic abstract immediate consequence operator. The second one is related to the correctness of each abstract operator as defined in [13], and ensures a correct definition of the abstract interpretation.

• Monotonicity:

– given a n-tuple of concrete atoms (B_{1}, ..., B_{n}) ∈ B_{P}^{n}, for each I_{1}^{♯}, I_{2}^{♯} ∈ H_{P} such that I_{1}^{♯} ≤_{α} I_{2}^{♯} we have

α-mgu((B_{1}, ..., B_{n}), I_{1}^{♯}) ≤_{Φ} α-mgu((B_{1}, ..., B_{n}), I_{2}^{♯}),

– given a set of variables V, and a concrete atom A, for each Φ_{1}^{♯}, Φ_{2}^{♯} ∈ Σ_{V} such that Φ_{1}^{♯} ≤_{Φ} Φ_{2}^{♯} we have

α-apply(A, Φ_{1}^{♯}) ≤_{α} α-apply(A, Φ_{2}^{♯}).

• Correctness:

– for each I ∈ 2^{B_{P}} we have

α_{Φ}(\{ ϑ | \begin{matrix}ϑ = mgu((B_{1}, ..., B_{n}), (B′_{1}, ..., B′_{n}))_{|var(B_{1},...,B_{n})} \\ B′_{1}, ..., B′_{n} ∈ I \end{matrix} \})

≤_{Φ} α-mgu((B_{1}, ..., B_{n}), α(I)),
– for each Φ ∈ 2^{Subst_{V}} we have

α({(Aϑ) | ϑ ∈ Φ}) ≤_{α} α-apply(A, α_{Φ}(Φ)).

These conditions, together with the Galois insertion of the abstract domains into the concrete ones, provide a framework for the definition of a monotonic and correct abstract immediate consequence operator, on which the abstract fixpoints semantics is based.

Let us define the abstract analog of the standard notion of π-model, according to the previous basic concepts.

Definition 3.3 (abstract model-theoretic semantics) Given a logic program P consisting of a set of Horn clauses {C_{1}, ..., C_{m}}, where C_{i} ≡ A_{i} : −B_{i_{1}}, ..., B_{i_{n}}, I^{♯} ∈ H_{P} is an abstract π-model for P iff there exists a concrete π-model I such that α(I) = I^{♯}.

Abstract π-models capture the approximation induced by the abstract interpretation. An abstract π-interpretation is an abstract π-model if and only if it is the approximation of a concrete π-model.

The standard semantics can be viewed as an instance of the abstract scheme (even if the finite domain property is not satisfied), where abstraction is the identity function.

We want now to give a finitely computable characterization of the concrete π-model associated with the fixpoint semantics. Usually the fixpoint semantics of a program is given in terms of the least fixpoint of a monotonic (and continuous) transformation associated with it. We define the transformation in an “incremental way” on the clause structure of the program. Let P be a finite non-empty set of clauses {C_{1}, ..., C_{m}}.

Definition 3.4 Given a program clause C ≡ A : −B_{1}, ..., B_{n} ∈ P (n ≥ 0), let us define an abstract transformation map associated with the clause C,

T_{C}^{♯} : H_{P} → H_{P}

such that

T_{C}^{♯}(I^{♯}) = α-apply(A, α-mgu((B_{1}, ..., B_{n}), I^{♯})).

It is trivial to prove that

Proposition 3.8 If α-mgu and α-apply are well defined operators, T_{C}^{♯} is a well defined map on (H_{P} , ≤_{α}).

The monotonicity of the abstract operators ensures that

Theorem 3.9 T_{C}^{♯} is a monotonic mapping on the finite lattice (H_{P} , ≤_{α}).

Proof. Let us consider a given clause C ≡ A : −B_{1}, ..., B_{n} ∈ P and two abstract πinterpretations I_{1}^{♯} and I_{2}^{♯}, such that I_{1}^{♯} ≤_{α} I_{2}^{♯}. Then, by the monotonic property of α-mgu we have

α-mgu((B_{1}, ..., B_{n}), I_{1}^{♯}) ≤_{Φ} α-mgu((B_{1}, ..., B_{n}), I_{2}^{♯}).

By the monotonicity of α-apply, it follows that T_{C}^{♯}(I_{1}^{♯}) ≤_{α} T_{C}^{♯}(I_{2}^{♯}). □

Following the approach to program compositionality given in [42], the abstract transformation maps can be composed in an algebraic way, such that, for each T_{C_{1}}^{♯}, T_{C_{2}}^{♯}, the composed abstract transformation map is λI^{♯}.(T_{C_{1}}^{♯}(I^{♯})α-⊔T_{C_{2}}^{♯}(I^{♯})). We are now able to define an abstract transformation map, associated with the whole program P, as the composition of all the abstract transformations associated with the clauses in P.

Definition 3.5 Given a logic program P = {C_{1}, ..., C_{m}}, the abstract transformation map associated with the program , T_{P}^{♯} : H_{P} → H_{P}, is defined as

T_{P}^{♯} = λI^{♯}.α- ⊔_{i=1}^{m} T_{C_{i}}^{♯}(I^{♯}).

Corollary 3.10 T_{P}^{♯} is a monotonic mapping on (H_{P} , ≤_{α}).

Proof. It is a trivial consequence of the monotonicity of α-⊔ and T_{C_{i}}^{♯}. □

The general correctness condition on this abstraction scheme is

∀I ∈ 2^{B_{P}} , α(T_{P} (I)) ≤_{α} T_{P}^{♯} (α(I)).

Note that, since T_{P}^{♯} was defined in terms of two abstract operators, α-mgu and α-apply, we can reduce the general correctness condition to two corresponding correctness conditions, given in terms of the abstract most general unifier and the abstract substitution application operators, according to the following theorem.

Theorem 3.11 Let P = {C_{1}, ..., C_{m}} be a logic program with clauses C_{i} of the form A_{1} : −B_{i_{1}}, ..., B_{i_{n}}, for i = 1, ..., m. Assume that α-mgu and α-apply satisfy the monotonicity and the correctness properties, then α(T_{P} (I)) ≤_{α} T_{P}^{♯} (α(I)) for all I ∈ 2^{B_{P}}.

Proof. Let us consider a given concrete π-interpretation I ∈ 2^{B_{P}}. Then, by the definition of T_{P} and since α is a join-morphism, we have

α(T_{P} (I)) = α( ∪_{i=1}^{m} T_{C_{i}}(I)) = α- ⊔_{i=1}^{m} α(T_{C_{i}}(I)).

By α-apply correctness

\begin{aligned}α(T_{C_{i}}(I)) & = & α(\{ (A_{i}ϑ) | \begin{matrix}ϑ = mgu((B_{i_{1}}, ..., B_{i_{n}}), (B′_{1}, ..., B′_{n}))_{|var(B_{i_{1}},...,B_{in})}, \\ B′_{1}, ..., B′_{n} ∈ I \end{matrix} \}) \\ & ≤_{α} & α-apply(A_{i}, Φ^{♯}) where: \end{aligned}

Φ^{♯} ∈ α_{Φ}(\{ ϑ | \begin{matrix}ϑ = mgu((B_{i_{1}}, ..., B_{i_{n}}), (B′_{1}, ..., B′_{n}))_{|var(B_{i_{1}},...,B_{in})}, \\ B′_{1}, ..., B′_{n} ∈ I \end{matrix} \}).

By α-mgu correctness and α-apply monotonicity, α-apply(A_{i}, Φ^{♯}) ≤_{α} α-apply(A_{i}, Φ^{′♯}) where: Φ^{′♯} = α-mgu((B_{i_{1}}, ..., B_{i_{n}}), α(I)). Thus, by the definition α-apply(A_{i}, Φ^{′♯}) = T_{C_{i}}^{♯}(α(I)), that is

α(T_{C_{i}}(I)) ≤_{α} T_{C_{i}}^{♯}(α(I)).

(T_{C_{i}}^{♯} is correct according to the corresponding abstract interpretation notion). Therefore, by α-⊔ monotonicity,

α( ∪_{i=1}^{m} T_{C_{i}}(I)) ≤_{α} α- ⊔_{i=1}^{m} T_{C_{i}}^{♯}(α(I))

and then α(T_{P} (I)) ≤_{α} T_{P}^{♯} (α(I)). □

We can now give the abstract fixpoint semantics. The following results allow to characterize, by a finite fixpoint computation, an approximation of the fixpoint semantics of any logic program P.

Theorem 3.12 Let I^{♯} ∈ H_{P} be an abstract π-interpretation such that T_{P}^{♯} (I^{♯}) ≤_{α} I^{♯}. Then I^{♯} is an abstract π-model for the logic program P.

Proof. Let I^{♯} ∈ H_{P} such that T_{P}^{♯} (I^{♯}) ≤_{α} I^{♯}. By monotonicity of γ

γ(T_{P}^{♯} (I^{♯})) ⊆ γ(I^{♯}).

By correctness, we have T_{P} (γ(I^{♯})) ⊆ γ(T_{P}^{♯} (I^{♯})), and therefore

T_{P} (γ(I^{♯})) ⊆ γ(I^{♯})

that is, there exists γ(I^{♯}) which is a concrete π-model for P. By the Galois insertion we obtain α(γ(I^{♯})) = I^{♯}, i.e. I^{♯} is an abstract π-model for P. □

Let us denote by ℑ^{♯} = {I^{♯} ∈ H_{P} | T_{P}^{♯} (I^{♯}) ≤_{α} I^{♯}}. Thus

ℑ^{♯} ⊆ {I^{♯} ∈ H_{P} | I^{♯} is an abstract π-model of P }.

The following theorem corresponds to the standard one [23] specifying ℑ^{♯} as a finite lattice with respect to ≤_{α}.

Theorem 3.13 ℑ^{♯} is a finite lattice with respect to the ≤_{α} order relation.

Proof. Let us first show that for any finite set of abstract π-models W ⊆ ℑ^{♯}, there exists an abstract π-model I^{′♯} ∈ ℑ^{♯} such that I^{′♯} ≤_{α} I^{♯}, for each I^{♯} ∈ W. Let us consider a finite set of abstract π-models W = {I_{1}^{♯}, ..., I_{k}^{♯}} ⊆ ℑ^{♯}. Then, by definition

α- ⊔_{i=1}^{m} α-apply(A_{i}, α-mgu((B_{i_{1}}, ..., B_{i_{n}}), I_{j}^{♯})) ≤_{α} I_{j}^{♯}, for all j = 1, ..., k.

Let I^{′♯} = glb_{≤_{α}}W = α-⊔{I^{♯} | I^{♯} ≤_{α} I_{j}^{♯}, ∀j = 1, ..., k}. Then, by the α-⊔ associativity, I^{′♯} ≤_{α} I_{j}^{♯}, for all j = 1, ..., k. By the monotonic property of α-mgu and α-apply, we have

α- ⊔_{i=1}^{m} α-apply(A_{i}, α-mgu((B_{i_{1}}, ..., B_{i_{n}}), I^{′♯})) ≤_{α} I_{j}^{♯}, for all j = 1, ..., k.

Thus, by the definition of I^{′♯}, α- ⊔_{i=1}^{m} α-apply(A_{i}, α-mgu((B_{i_{1}}, ..., B_{i_{n}}), I^{′♯})) ≤_{α} I^{′♯}. Therefore,

I^{′♯} ∈ ℑ^{♯}. Finally if W = {I_{1}^{♯}, ..., I_{k}^{♯}} is a finite set of abstract π-models in ℑ^{♯}, \overline{I}^{♯} = glb_{≤_{α}}\{I^{♯} ∈ ℑ^{♯} | I_{j}^{♯} ≤_{α} I^{♯}, ∀j = 1, ..., k\} ∈ ℑ^{♯}, and for each I_{j}^{♯} ∈ W, I_{j}^{♯} ≤_{α} \overline{I}^{♯}. □

A consequence of the previous theorem is that there exists a least element (w.r.t ≤_{α}) in the finite lattice of abstract π-models ℑ^{♯} associated with the program P.

Definition 3.6 (abstract fixpoint semantics) The abstract fixpoint semantics of a logic program P is defined as

F^{♯}(P) = lfp(T_{P}^{♯}).

By definition F^{♯}(P) is an abstract π-model in ℑ^{♯}. The following theorem states that F^{♯} is always finitely computable.

Theorem 3.14 There exists a finite positive number k such that F^{♯}(P) = T_{P}^{♯} ↑ k.

Proof. By the Knaster-Tarski theorem, every monotonic operator T has a least fixpoint denoted by lfp(T).

Therefore lfp(T_{P}^{♯}) = glb_{≤_{α}}{I^{♯} | T_{P}^{♯} (I^{♯}) ≤_{α} I^{♯}} = F^{♯}(P). Moreover, since the associated lattice (H_{P} , ≤_{α}) is finite, there exists a positive number k, such that lfp(T_{P}^{♯}) = T_{P}^{♯} ↑ k. □

This theorem is analogous to the concrete semantics one and gives us a method to compute F^{♯}(P) in a finite time. Since we are dealing with abstract interpretations, we can compute an abstract approximation of the concrete fixpoint semantics in a finite number of steps (the approximated solution of the recursive semantic relation, T_{P} (I) ⊆ I) We have therefore implicitly defined an abstraction scheme for any definite logic program P,

⟨(2^{B_{P}} , ⊆) , T_{P} , (H_{P} , ≤_{α}) , T_{P}^{♯} ⟩.

The abstract immediate consequence operator for a logic program P can be considered as a specialized tool for a particular kind of analysis. The algebraic compositionality of the T_{P}^{♯} definition, allows the algebraic composition of tools defined for different program modules. Moreover, different program analyses can be composed in order to obtain more powerful analysis tools.

Example 3.6 Let us consider a simple ground analysis where abstract terms are denoted by g and ng, representing ground and non-ground terms respectively. Let P be the following logic program

p(x, succ(x)) : −r(x), q(x).
q(x).

provided that the following type declaration P′ is given (in a logic program form)

r(succ(x)) : −r(x).
r(0).

P′ defines a type constraint on the arguments of p. Types are defined as equivalence classes of terms with respect to a given type definition (e.g. nat = {0, succ(0), ...}) see Example 3.3. No type variables are considered. Abstract π-interpretations contain abstract atoms denoting both type and ground information.

A simple type analysis is processed by an instance T^{type} of the abstract immediate consequence operator, where the abstract unification of a concrete term t with a type τ associates types with the variables in var(t): {τ̄_{1}/x_{1}, ..., τ̄_{m}/x_{m}} if ∀ϑ = {t̄_{1}/x_{1}, ..., t̄_{m}/x_{m}} where t̄_{j} ∈ τ̄_{j}, j = 1, ..., m we have tϑ ∈ τ (e.g. α-mgu(r(x), r(nat)) = {nat/x}). This process is extended to tuples, returning consistent set of bindings (i.e. only one type is associated with each variable). The application of an abstract substitution {τ̄_{1}/x_{1}, ..., τ̄_{m}/x_{m}} to a concrete term t returns a type τ such that ∀ϑ = {t̄_{1}/x_{1}, ..., t̄_{m}/x_{m}} where t̄_{j} ∈ τ̄_{j}, j = 1, ..., m we have tϑ ∈ τ.

Ground analysis is processed by an abstract immediate consequence operator denoted T^{G}. The abstract domain of terms for ground analysis is enhanced by considering type information. A “type label” τ is associated with the abstract term g, denoting the set of ground terms having the same type τ (e.g. {0, succ(0), ...} and {a, b, c, ...} are denoted g_{nat} and g_{char} respectively). g and ng denote ground and non-ground terms having an unspecified type. Note that the type label τ is considered by T^{G} as denotation for ground terms of type τ. Thus g_{τ} and τ have the same meaning for T^{G}. Abstract unification of a concrete term t with an abstract one t^{♯} generates bindings on var(t): {g_{τ_{1}}/x_{1}, ..., g_{τ_{m}}/x_{m}} if t^{♯} = g_{τ} or t^{♯} = τ; and ∀ϑ = {t̄_{1}/x_{1}, ..., t̄_{m}/x_{m}} where t̄_{j} ∈ τ̄_{j}, j = 1, ..., m, we have tϑ ∈ τ (a deeper discussion of type inference can be found in [3]). No type labels are returned if the unification is performed with an abstract term g. Type labels are introduced by the α-unification of a concrete term with an abstract term denoting a type structure, processed by T_{P′}^{type} or by T_{P}^{G} in a previous step. (e.g. αmgu(r(x), r(nat)) = {g_{nat}/x}). As before this process is extended to atoms. The application returns ng if the corresponding term is not fully instantiated.

The type analysis on P′ can be combined with the “extended” ground analysis of P

T_{P ∪P′}^{♯} = λI^{♯}.(T_{P′}^{type}(I^{♯})α-⊔T_{P}^{G}(I^{♯}))

returning the following abstract π-model

T_{P ∪P′}^{♯}(∅) = {r(nat), q(ng)}

T_{P ∪P′}^{♯}(T_{P ∪P′}^{♯}(∅)) = {r(nat), q(ng), p(g_{nat}, g_{nat})} (fixpoint).

The correctness of the abstract fixpoint semantics with respect to the concrete one is proved by the following theorem.

Theorem 3.15 Let us consider a monotonic map T_{P}^{♯} which satisfies the previous correctness condition. Then, there exists a finite positive integer k such that

α(T_{P} ↑ ω) ≤_{α} T_{P}^{♯} ↑ k.

Proof. We prove by induction that, for each positive integer n, α(T_{P}^{n}(∅)) ≤_{α} T_{P}^{♯^{n}}(∅).

• The base case is straightforward.

• Assume that α(T_{P}^{(n−1)}(∅)) ≤_{α} T_{P}^{♯^{(n−1)}}(∅). Then, by correctness, α(T_{P}^{n}(∅)) = α(T_{P} (T_{P}^{(n−1)}(∅))) ≤_{α} T_{P}^{♯} (α(T_{P}^{(n−1)}(∅))). By the induction hypothesis α(T_{P}^{(n−1)}(∅)) ≤_{α} T_{P}^{♯^{(n−1)}}(∅). Therefore, by monotonicity α(T_{P}^{n}(∅)) ≤_{α} T_{P}^{♯^{n}}(∅).

Since the abstract domain is finite, there exists a finite positive number k, such that T_{P}^{♯^{n}}(∅) = T_{P}^{♯^{k}}(∅) for each n ≥ k. Then α(T_{P}^{n}(∅)) ≤_{α} T_{P}^{♯^{k}} for each n.

By definition of Galois connection (insertion) over complete lattices, and by abstraction continuity (recall that α is additive and then continuous)

α( ∪_{n≤ω} T_{P}^{n}(∅)) = α − ⊔_{n≤ω} α(T_{P}^{n}(∅)).

By α-⊔ idempotence, we obtain:

α( ∪_{n≤ω} T_{P}^{n}(∅)) ≤_{α} T_{P}^{♯^{k}}(∅).

□

Corollary 3.16 Under the previous hypothesis, α(F(P)) ≤_{α} F^{♯}(P).

Once we have tested (at specialization time) the correctness of abstract unification and abstract application, we have proved the correctness of the associated abstract interpretation. This result points out the relevance of the α-mgu, and α-apply operators in our abstraction scheme. From a semantic viewpoint (see the diagram in Figure 3.2), given a logic program P, the fixpoint semantics ⟨F, (2^{B_{P}} , ⊆)⟩, is approximated by the corresponding abstract fixpoint semantics based on the previous abstraction scheme ⟨F^{♯}, (H_{P} , ≤_{α})⟩.

[figure: P; H_{P}; 2^{B_{P}}; α; γ; F^{♯}(P); F(P); T_{P}^{♯}; T_{P}]

Figure 3.2. Concrete and Abstract Fixpoint Semantics

The meaning of a logic program P is then given according to a non-standard (abstract) semantics (an abstract π-model) which evaluates the program on a non-standard domain (the abstract one). Its correctness with respect to the concrete one is a consequence of the abstract interpretation correctness.

Thus, the abstract interpretation for logic programs consists in computing a finite approximation of the fixpoint semantics of the program. The computed abstract π-model can be used both as a collection of program information (goal independent analysis) and as a collection of abstract program facts, which can be used to analyze success patterns of different queries (goal directed analysis).

The relation between the abstract fixpoint and the concrete operational semantics (computed answer substitutions) is given by the following result.

Theorem 3.17 Let P be a logic program and let G be a goal ? − B_{1}, ..., B_{n}. If G →_{P}^{∗}^{ϑ} □, then α_{Φ}({ϑ_{|G}}) ≤_{Φ} α-mgu((B_{1}, ..., B_{n}), F^{♯}(P)).

Proof. Let us assume G →_{P}^{∗}^{ϑ} □, then there exist B′_{1}, ..., B′_{n} ∈ F(P) and there exists ϑ′ = mgu((B_{1}, ..., B_{n}), (B′_{1}, ..., B′_{n})) such that ϑ_{|G} = ϑ′_{|G} (Strong Soundness). By correctness, α(F(P)) ≤_{α} F^{♯}(P), thus by α-mgu correctness and by monotonicity,

α_{Φ}({ϑ_{|G}}) ≤_{α} α_{Φ}({ϑ | ϑ = mgu((B_{1}, ..., B_{n}), (B′_{1}, ..., B′_{n})) ∧ (B′_{1}, ..., B′_{n}) ∈ F(P)}) ≤_{α} αmgu((B_{1}, ..., B_{n}), α(F(P))) ≤_{α} α-mgu((B_{1}, ..., B_{n}), F^{♯}(P)). □

Example 3.7 The type analysis of the logic program

sum(x, 0, x).

sum(x, s(y), s(z)) : −sum(x, y, z).

returns the abstract π-model {sum(τ, nat, τ)} (since the abstraction of the first clause, sum(τ, nat, τ), subsumes sum(nat, nat, nat)).

Given a goal G : ? − sum(a, x, y), the abstract substitution returned by α-unifying the goal into the abstract π-model is ⟨nat/x, char/y⟩ corresponding to the success pattern of G [3].

4 Applications

In the previous sections we have defined a general scheme which allows us to construct bottomup abstract interpretations for logic programs according to the Cousot’s idea, following the fixpoint approach to the semantics for logic programs. From a pragmatic point of view, the definition of an abstract interpretation corresponds to a specialization process which basically consists of the following steps.

• Defining a suitable abstract universe of terms U_{P}^{♯} by means of a quotient operation with respect to an equivalence relation induced (on terms) by the observable properties of the analysis (like type structure, mode and depth of terms).

• Defining a set of abstract atoms and abstract substitutions on the abstract universe of terms, modulo an equivalence relation. The abstract atoms and substitutions are denotations for the corresponding equivalence classes. Such an equivalence relation is defined in order to capture the observable properties of the relationship between terms (like sharing of variables and functional dependences on terms).

• Defining a congruence relation on the algebraic system associated with the powersets of the abstract base and the set of abstract substitutions, ordered by set-inclusion, which induces a lattice of abstract π-interpretations and α-sets of abstract substitutions respectively. The congruence relation preserves joins (i.e. interpretation and set-substitution composition) and strongly depends on the observable properties of the analysis with respect to sets of abstract atoms and abstract substitutions (like concise model representation, general type/mode structure for each predicate symbol).

• The set of previously defined equivalence relations has to satisfy the following conditions

– the abstract domains of interpretations and substitutions are finite collections of abstract objects,

– ⟨α, γ⟩ and ⟨α_{Φ}, γ_{Φ}⟩ form a pair of Galois insertions of the abstract domains into the concrete ones.

• Defining the abstract transformation map T_{P}^{♯} associated with the program being analyzed, by specializing the abstract operators α-mgu and α-apply. This process takes place by specializing the operators and by testing their monotonicity and correctness.

In this section we present two applications of our abstract interpretation scheme, namely an extension of the classical ground analysis, and an approximation of the success set on a domain of terms whose depth is less than k (depth-k analysis). In particular, an abstract domain for groundness and dependence analyses, based on hypergraph properties, is introduced. The emphasis is not on showing novel applications, but in showing how known relevant applications can be formalized within our framework. Some new applications of the framework are mentioned at the end of Section 4.1.

4.1 Ground Dependence Analysis

Ground analysis has been considered by several authors in a top-down framework [6, 16, 19, 43, 48, 35]. Most of the above papers are concerned with groundness analysis for code optimization. Thus the emphasis is on obtaining information about call patterns.

Our analysis collects goal independent information about success patterns of the program. Given a goal G, by abstract unification with atoms in F^{♯}(P) we obtain information on which arguments will definitely become ground and on ground dependences between the arguments. The underlying analysis is similar to the one in [15], which, however, is not explained in terms of abstract interpretation. In Section 4.1.1 we briefly discuss the use of our analysis to obtain call patterns information.

Let us consider an abstract universe of terms. We want to define it as composed of equivalence classes corresponding to the sets of (definitely) ground and (possibly) non-ground terms. Ground dependence analysis (like sharing analysis [12, 43, 57]) requires variable information for each non-ground concrete term. The equivalence relation ≈_{t} is defined as follows

∀t_{1}, t_{2} ∈ U_{P} : t_{1} ≈_{t} t_{2} iff var(t_{1}) = var(t_{2}).

Each equivalence class can be represented as a set of (abstract) variables (the empty set represents the ground terms class), t^{♯} = var(tρ^{♯}), where ρ^{♯} is a variable renaming which associates with each concrete variable in t an abstract variable in a set of abstract symbols of variables {ς, ζ, η, ...} which are not in V ar.

The observable properties in the abstract atoms are the ground dependences between the

corresponding arguments. If t_{j}^{♯} ⊆ ∪_{r=1}^{k} t_{i_{r}}^{♯} the groundness of the term t_{j} depends on the groundness of t_{i_{1}}, ..., t_{i_{k}}. The equivalence relation ≈_{A} is defined as follows

p(t_{1}^{♯}, ..., t_{n}^{♯}) ≈_{A} p(t_{1}^{′♯}, ..., t_{n}^{′♯}) iff ∀T ⊂ {1, ..., n}, j ∈ {1, ..., n} and j ∉ T,

t_{j}^{♯} ⊆ ∪_{i∈T} t_{i}^{♯} ⟺ t_{j}^{′♯} ⊆ ∪_{i∈T} t_{i}^{′♯}.

Thus two atoms are equivalent iff they have the same ground dependences between the same sets of arguments.

Notice that, once the dependences between the arguments of an atom are discovered, the information on variables (i.e. sharing) becomes useless from the analysis viewpoint. By using sets of variables as terms denotations, dependences are implicitly captured by sharing variables between arguments. Since the ground dependence analysis is an analysis of dependences, a more efficient analysis requires an appropriate data structure to explicitly characterize arguments dependences, avoiding redundant computations on variables (like full unification). As we will see, the unification process on atoms having data dependences can be summarized in a suitable graph notation. Then, the abstract unification can be specialized in a very efficient way, as a simple data dependences calculus, whose principles were introduced by [15, 41].

We propose a new abstract domain of atoms which is isomorphic to the abstract base. Dependence information is represented by means of an hypergraph notation. The resulting analysis is more concise and efficient than the standard one, exploiting explicit dependences. In the following we give the basic definitions of the representation of abstract atoms and abstract substitutions as hypergraphs.

The term representation in any abstract atom needs not to record variable names in list structures. The set {g, ng}, where g and ng represent the equivalence classes of (definitely) ground and (possibly) non-ground terms respectively, is adequate to represent any concrete term.

For each ground term there exists a non-ground term which is greater than it. Thus, g ≤^{♯} ng. Note also that, because of the approximation introduced by abstract interpretation, we can get the ng value for an argument also if it actually results in a ground value. Thus, the value “anything”, instead of ng, could give a better intuition about the abstract domain. By using the value ng we want to stress that ng represents the set of all non-ground terms in the universe. This shows that the abstract domain for groundness can be used as term representation in ground dependence analysis, and it does not need to be ordered by set-inclusion [19, 48]. A more natural ordering relation is, in fact, that based on the usual instantiation relation as given for ≤^{♯}. However, the correctness of the abstract interpretation guarantees that if we get the g value for an argument of an atom, then, in all the possible evaluations, this argument will be ground.

In order to represent dependences, the classical ground information is integrated with a further information on ground dependences among the arguments in the success patterns for each atom. As we said before, a ground dependence of an argument position j on a set of other argument positions J means that if all the arguments whose position is in J are ground, then the argument in position j is ground too. For a concise dependence representation, we introduce a suitable hypergraph notation.

An hypergraph is a pair G = (V, Ψ) where V = {v_{1}, ..., v_{n}} is a (finite) set of nodes and Ψ = {e_{1}, ..., e_{m}} with e_{i} ⊆ V for i = 1, ..., m is the set of hyperarcs. We will consider directed hyperarcs, where for each i = 1, ..., m, e_{i} = ⟨T, H⟩ such that T ⊆ V (the tail), H ∈ V (the head) and T ∩ H = ∅. In the following we denote by E any subset of Ψ. Moreover, we denote by tail(e) and head(e) the tail and the head of any hyperarc e. The “tail” and “head” notions can be extended to deal with sets of hyperarcs. Let E = {e_{1}, ..., e_{n}}, then

T ail(E) = ∪_{i=1}^{n} tail(e_{i}) and Head(E) = ∪_{i=1}^{n} head(e_{i}).

A hyperarc e is satisfied by a set of nodes V′ iff tail(e) ⊆ V′. The graph, associated with the hypergraph G = (V, Ψ) is obtained by reducing each hyperarc: ⟨{s_{1}, ..., s_{m}}, h⟩ ∈ Ψ, in a set of arcs {⟨s_{1}, h⟩..., ⟨s_{m}, h⟩}. In the following we will denote by Π_{G}(v′, v) the set of paths π defining a connection from v′ to v in the graph associated with the hypergraph G.

The hypergraph notation is useful to represent dependence information in a concise way. The abstract base B_{P}^{♯} can be represented as a set of abstract atoms (each one representing an equivalence class with respect to ≈_{A}) of the form

< p, (V_{n}, Ψ) >

where p is an n-ary predicate, V_{n} = {v_{1}^{♯}, ..., v_{n}^{♯}} and v_{i}^{♯} ∈ {g, ng} is a set of indexed nodes representing the mode of the corresponding predicate argument (the index represents the corresponding argument position), and Ψ describes the ground dependences among the non-ground arguments. These dependences are expressed by hyperarcs. Thus, there exists a ground dependence of the j-argument on the i_{1}, ..., i_{k}-ones (or if the i_{1}, ..., i_{k}-arguments have all ground mode then the j-one has ground mode too), iff ⟨{v_{i_{1}}^{♯}, ..., v_{i_{k}}^{♯}}, v_{j}^{♯}⟩ ∈ Ψ.

Proposition 4.1 B_{P}^{♯} ≃ ({p(t_{1}^{♯}, ..., t_{n}^{♯}) | p ∈ P red_{P}^{n} ∧ t_{i}^{♯} ∈ U_{P}^{♯} })/_{≈_{A}}, that is the set of typed (by predicate symbols) hypergraphs is isomorphic (by means of χ_{A}, which is defined below) to the set of equivalence classes of atoms with respect to ≈_{A}, where

χ_{A}([p(t_{1}^{♯}, ..., t_{n}^{♯})]_{≈_{A}}) =< p, ({v_{1}^{♯}, ..., v_{n}^{♯}}, Ψ) >

and

• v_{1}^{♯} = \{ \begin{matrix}g & if t_{i}^{♯} = ∅ \\ ng & otherwise \end{matrix}

• ⟨{v_{i_{1}}^{♯}, ..., v_{i_{k}}^{♯}}, v_{j}^{♯}⟩ ∈ Ψ, iff ∀h ∈ {i_{1}, ..., i_{k}, j}, v_{h}^{♯} = ng, and {i_{1}, ..., i_{k}} is the least set of argument indexes of p(t_{1}^{♯}, ..., t_{n}^{♯}) such that

t_{j}^{♯} ⊆ ∪_{r=1}^{k} t_{i_{r}}^{♯}.

Example 4.1 We choose the least set of indexes in the tail of each hypergraph, in order to avoid redundant hyperarcs. The abstract atom [p({ς, ζ}, {η}, {ς})]_{≈_{A}} is represented by

< p, ({ng_{1}, ng_{2}, ng_{3}}, {⟨{ng_{1}}, ng_{3}⟩}) > instead of < p, ({ng_{1}, ng_{2}, ng_{3}}, {⟨{ng_{1}}, ng_{3}⟩, ⟨{ng_{1}, ng_{2}}, ng_{3}⟩}) >

The same holds for abstract substitutions which can be represented by hypergraphs too. Thus each equivalence class (w.r.t. ≈_{A} or ≈_{S}) can be represented by an “efficient” hypergraph structure.

Given a finite set of (concrete) variables V, an abstract substitution is represented as a pair

< V′, (V, Ψ) >

where V′ ⊆ V is a set of indexed variables and (V, Ψ) is an hypergraph where V is a set of indexed nodes in {g, ng}. The binding v^{♯}/x is represented as an indexed variable x_{i} ∈ V′ and a corresponding (having the same index) node. Hyperarcs are defined as in the abstract atom case.

In order to collect all the success patterns, the congruence relation required to define abstract π-interpretations is simply identity, H_{P} = 2^{B_{P}^{♯}}. However, to make the analysis more concise (and efficient [18]) we can approximate success patterns with their least upper bound, maintaining at most one success pattern per predicate symbol [10]. For this reason, we introduce a merging hypergraph operator which, given a set of hypergraphs, returns the least upper bound hypergraph (the hypergraph more general with respect to the dependence information), containing all and only those dependences which are shared by all the elements in the set.

Hyperarcs allow the ground information to be spread among the arguments in the atoms and substitutions. Given an hypergraph (V, Ψ), the sets of nodes V′ ⊆ V and the node v are connected, denoted V′ ⟶_{c}^{Ψ} v, iff there exists E ⊆ Ψ such that:

• all the hyperarcs in E are satisfied by V′ ∪ Head(E); • ∀v′ ∈ V′ : Π_{(V,E)}(v′, v) ≠ ∅;

• ∀e ∈ E : ∀v̄ ∈ tail(e) : v̄ ∉ V′, ∃v′ ∈ V′ such that Π_{(V,E−{e})}(v′, v̄) ≠ ∅.

Example 4.2 Let us consider the following hypergraph

[figure: G = v_{1} v_{2} v_{3} v_{4} v_{5}; a; b; c; d; e]

Hyperarcs are labeled {a, b, c, d, e}. The node v_{5} is connected with {v_{4}} (through the hyperarcs {d, c, e, a}), {v_{3}} (through the hyperarcs {c, e, a}), {v_{1}, v_{2}} (through the hyperarcs {d, c, e, a}), etc.. .

Note that the definition of connection requires that any node in the tail of an hyperarc which is not in the set of starting nodes V′, can be reached from some starting node, without using the hyperarc itself. This condition avoids considering, in a connection, a hyperarc (e.g. a), such that each non-starting node (e.g. v_{2}) in the tail can only be reached from some starting node (e.g. v_{1}) by means of a path using the hyperarc itself (the hyperarc become “auto-satisfied”). As a consequence {v_{1}} ↛_{c}^{{a,b,c,d,e}} v_{5}.

Given a set of hypergraphs {({v_{1_{1}}^{♯}, ..., v_{1_{n}}^{♯}}, Ψ_{1}), ..., ({v_{m_{1}}^{♯}, ..., v_{m_{n}}^{♯}}, Ψ_{m})}, each one having n nodes, we define a merging operator M returning an hypergraph of n nodes:

(\{lub_{≤^{♯}}(v_{1_{1}}^{♯}, ..., v_{m_{1}}^{♯}), ..., lub_{≤^{♯}}(v_{1_{n}}^{♯}, ..., v_{m_{n}}^{♯})\}, \overline{Ψ})

where

\overline{Ψ} = ∪_{j=1}^{m} \{ ⟨\{v_{j_{i_{1}}}^{♯} , ..., v_{j_{i_{k}}}^{♯} \}, v_{j_{i_{h}}}^{♯} ⟩ ∈ Ψ_{j} | \begin{matrix}∀w ∈ \{1, ..., m\}, w ≠ j : \\ (v_{w_{i_{h}}}^{♯} = g) ∨ \\ (∃T ⊆ \{v_{w_{i_{1}}}^{♯} , ..., v_{w_{i_{k}}}^{♯} \}| T ⟶_{c}^{Ψ_{w}} v_{w_{i_{h}}}^{♯}) \end{matrix} \} .

Note that \overline{Ψ} is obtained as a synthesis of the ground dependences of the hypergraphs. A ground dependence is present in \overline{Ψ} iff it is true in all the hypergraphs.

Example 4.3 The merging of the hypergraphs:

M( [figure: (ng, ng, ng)] , [figure: (g, ng, ng)] ) is [figure: (ng, ng, ng)] .

The resulting nodes are ng, since g ≤^{♯} ng. Moreover, in the second hypergraph, the first argument is ground. Thus, each hyperarc (in the first hypergraph) having the first argument as a head is present in the result. As for the hyperarc ⟨{ng_{1}, ng_{2}}, ng_{3}⟩, since there exists {ng_{2}} ⊆ {ng_{1}, ng_{2}} such that ⟨{ng_{2}}, ng_{3}⟩ is an hyperarc in the second graph (i.e. the third argument is connected with the second one), ⟨{ng_{1}, ng_{2}}, ng_{3}⟩ is present in the result too.

Let us furthermore define an equivalence relation ≈_{I} on sets of abstract atoms.

Definition 4.1 By denoting with I^{♯} ↓ p the set of abstract atoms in I^{♯}, defined on the same predicate symbol p, for each I_{1}^{♯}, I_{2}^{♯} ∈ 2^{B_{P}^{♯}}, I_{1}^{♯} ≈_{I} I_{2}^{♯} iff • ∀p ∈ P red_{P}^{n} , I_{1}^{♯} ↓ p ≠ ∅ ⟺ I_{2}^{♯} ↓ p ≠ ∅ and

• for each p ∈ P red_{P}^{n} such that I_{1}^{♯} ↓ p ≠ ∅ (or equivalently I_{2}^{♯} ↓ p ≠ ∅) M({(V_{n}, Ψ)| < p, (V_{n}, Ψ) >∈ I_{1}^{♯} ↓ p}) = M({(V_{n}, Ψ)| < p, (V_{n}, Ψ) >∈ I_{2}^{♯} ↓ p}).

It is trivial to prove that ≈_{I} is a congruence relation on the join-semilattice (2^{B_{P}^{♯}} , ∪). Let H_{P} be the corresponding quotient algebra. In the following we will represent each equivalence class of abstract interpretations by the set having the least abstract atom occurrences. Since the merging operation has always one hypergraph as result, each π-interpretation contains just one abstract atom for each predicate symbol. This occurrence denotes the ground synthesis of all the abstract atoms belonging to the original set and having the same predicate name. Abstract substitutions will be handled in the same way. The abstract atom

< p, ({ng_{1}, ng_{2}, ng_{3}}, {⟨{ng_{1}}, ng_{2}⟩, ⟨{ng_{3}}, ng_{1}⟩}) >

and the α-substitution

< {x, y, z}, ({ng_{1}, ng_{2}, ng_{3}}, {⟨{ng_{1}}, ng_{2}⟩}) >

are respectively represented as:

[figure: p(ng, ng, ng); (ng/x, ng/y, ng/z)]

Example 4.4 Let us consider the abstract atoms

[figure: p(ng, ng, ng)] and p(ng, g, ng).

Since the second argument of p(ng, g, ng) is ground, the dependence ⟨{ng_{1}}, ng_{2}⟩ in the first abstract atom holds in the second too. The ground dependence ⟨{ng_{3}}, ng_{1}⟩, instead, is not true in p(ng, g, ng). Thus

M( [figure: p(ng, ng, ng)] , p(ng, g, ng)) = { p(ng, ng, ng) }, that is:

{ [figure: p(ng, ng, ng)] , p(ng, g, ng)} ≈_{I} { p(ng, ng, ng) }

Note that I_{1}^{♯} ≤_{α} I_{2}^{♯} (the ordering relation induced by α-⊔) holds iff for each abstract atom A^{♯} ∈ I_{1}^{♯}, there exists A^{′♯} ∈ I_{2}^{♯} such that A^{′♯} is more general (in the sense of ground dependence) than A^{♯}.

Analogously to the previous case, we can extend the congruence relation to the α-substitution framework. As usual, abstract substitutions defined over the same set of variables, are handled as abstract atoms having the same predicate symbol, where the bindings are viewed as the corresponding arguments.

Given a finite set of variables V, and two sets of abstract substitutions defined on V′ ⊆ V, Φ_{1}^{♯}, Φ_{2}^{♯} ∈ 2^{S_{V}^{♯}}, the congruence relation on (2^{S_{V}^{♯}} , ∪) is equivalently defined as in the abstract π-interpretation case.

Definition 4.2 By denoting with Φ^{♯} ↓ V′ the set of abstract atoms defined on the same symbols of variables V′ ⊆ V, for each Φ_{1}^{♯}, Φ_{2}^{♯} ∈ 2^{S_{V}^{♯}}, Φ_{1}^{♯} ≈_{Φ} Φ_{2}^{♯} iff

• ∀V′ ⊆ V, Φ_{1}^{♯} ↓ V′ ≠ ∅ ⟺ Φ_{2}^{♯} ↓ V′ ≠ ∅ and

• for each V′ ⊆ V such that Φ_{1}^{♯} ↓ V′ ≠ ∅ M({(V, Ψ)| < V′, (V, Ψ) >∈ Φ_{1}^{♯} ↓ V′}) = M({(V, Ψ)| < V′, (V, Ψ) >∈ Φ_{2}^{♯} ↓ V′}).

In analogy to the case of abstract atoms we define the ordering relation on sets of abstract substitutions ≤_{Φ}. In order to have a more familiar abstract substitution denotation, we will often denote each abstract substitution ϑ^{♯} =< V′, (V, Ψ) > as a pair < β^{♯}, Ψ_{ϑ} > where β^{♯} denotes the corresponding set of bindings variables/node and Ψ_{ϑ} = Ψ.

Example 4.5 Let V = {x, y, z, u} be a set of variable symbols and

< β_{1}^{♯}, Ψ_{ϑ_{1}} >= [figure: (ng/x, g/y, ng/z, ng/u)] , < β_{2}^{♯}, Ψ_{ϑ_{2}} >= (ng/x,g/y,ng/z,g/u)

two abstract substitutions defined on V. Since

M({< β_{1}^{♯}, Ψ_{ϑ_{1}} >, < β_{2}^{♯}, Ψ_{ϑ_{2}} >}) = [figure: (ng/x, g/y, ng/z, ng/u)] we have

{< β_{1}^{♯}, Ψ_{ϑ_{1}} >, < ϑ_{2}^{♯}, Ψ_{ϑ_{2}} >} ≈_{Φ} { [figure: (ng/x, g/y, ng/z, ng/u)] }.

Given a finite set of variables V, H_{P} and Σ_{V} are finite sets of abstract atoms and abstract substitutions respectively. Moreover it is trivial to prove that

α(γ(I^{♯})) = I^{♯} and α_{Φ}(γ_{Φ}(Φ^{♯})) = Φ^{♯}.

For the α-mgu definition, let us consider the concrete and the abstract atoms, p(t_{1}, ..., t_{n}) and < p, (\{v_{1}^{♯}, ..., v_{n}^{♯}\}, Ψ) > respectively. Let us define an hypergraph (V, \overline{Ψ}) associated with the abstract unification process, such that:

• V = V_{1} ∪ V_{2} where V_{1} = V ar(p(t_{1}, ..., t_{n})) ∪ {⊗} and V_{2} = {v_{i}^{♯} | i = 1, ..., n}.

• The set of hyperarcs \overline{Ψ} is built as follows

– Ψ ⊆ \overline{Ψ}, – [t_{i}]_{≈_{t}} = ∅ ⇒ ∃e, e′ ∈ \overline{Ψ} | e =< \{⊗\}, v_{i}^{♯} > and e′ =< \{v_{i}^{♯}\}, ⊗ >,

– t_{i} = t[x_{1}, ..., x_{k}] ⇒ ∃e ∈ \overline{Ψ}, ∀j = 1, ..., k ∃e′_{j} ∈ \overline{Ψ} | e =< \{x_{1}, ..., x_{k}\}, v_{i}^{♯} > and e′_{j} =< {v_{i}^{♯}}, x_{j} >.

Example 4.6 The hypergraph in Figure 4.1 corresponds to the pair of atoms

p(f(x, y), b, c) and {p(ng, ng, ng) \atop } .

[figure: ng; ng; ng; x; y; ⊗; ⊗]

Figure 4.1. The hypergraph associated with the α-mgu process

The α-unification process works on this hypergraph and consists of the following two steps

1. Ground information propagation. It is an iterative labelling process on the hypergraph which labels nodes in V. The process labels by ∗ any node v in V such that there exists a hyperarc which has v as head and each node in the tail is g, if belonging to V_{2}, ⊗ if belonging to V_{1}, or it is already labeled by ∗. The process halts when no more nodes can be labeled.

2. α-substitution definition. This process takes the labeled hypergraph and returns an abstract substitution Φ^{♯} = {< β^{♯}, Ψ_{ϑ} >}, where β^{♯} is defined on the set of variables of the concrete atom. If the first argument is empty, Φ^{♯} = ∅, if the second argument is empty, then Φ^{♯} = {F ail}. Otherwise, it associates the abstract value g to every variable labeled by ∗, and ng to the other ones. Ψ_{ϑ} represents the ground dependence information associated with the α-substitution. There exists a ground dependence between some nonground argument iff there exists a graph connection among the involved ng-nodes in the hypergraph.

Example 4.7 The abstract substitution resulting from the unification process, under the hypothesis of the previous example, is a ground substitution with no associated ground dependence information, that is: < {g/x, g/y}, ∅ >.

Example 4.8 Let us consider the atoms

p(f(x, y), z, c) and [figure: p(ng, ng, ng)] .

In this case, we note that there is no ground information propagation. The resulting abstract substitution is [figure: ng; ng; ng*; x; y; z; ⊗] ⇒ [figure: (ng/x, ng/y, ng/z)]

Figure 4.2. The hypergraph for the α-mgu computation.

Since each abstract π-interpretation contains at most one abstract atom for each predicate symbol, given a concrete atom A, α-mgu returns at most one abstract substitution corresponding to the α-unification process. Note also that the α-unification process of any pair of atoms cannot fail as long as the related concrete and abstract atoms have the same predicate symbol.

Finally, it is easy to extend the previous abstract unification process to any n-tuple (n ≥ 1) of atoms. In this case, if there exists a shared variable between the concrete atoms, we may have possibly multiple connections between the shared variable and a set of nodes (abstract arguments).

Example 4.9 The hypergraph associated with the α-unification process of the concrete atoms

p(x, y), q(y) and { p(ng, ng) ,q(g)} is

[figure: ng*; ng*; g; x*; y*]

Figure 4.3. The hypergraph for the α-mgu computation.

The resulting abstract substitution is < {g/x, g/y}, ∅ >.

Theorem 4.2 α-mgu satisfies the monotonicity and the correctness properties.

Proof.

1. Monotonicity. Let us consider a given n-tuple of concrete atoms B_{1}, ..., B_{n} ∈ B_{P}, and I_{1}^{♯}, I_{2}^{♯} ∈ H_{P} such that I_{1}^{♯} ≤_{α} I_{2}^{♯}. Thus: for each B_{1}^{♯}, ..., B_{n}^{♯} ∈ I_{1}^{♯} there exist B_{1}^{′♯}, ..., B_{n}^{′♯} ∈ I_{2}^{♯} such that {B_{i}^{♯}} ≤_{α} {B_{i}^{′♯}}, for all i = 1, ..., n.

Thus ϑ_{1}^{♯} = α-mgu((B_{1}, ..., B_{n}), {B_{1}^{♯}, ..., B_{n}^{♯}}) is less general (i.e. it contains more ground information) than ϑ_{2}^{♯} = α-mgu((B_{1}, ..., B_{n}), {B_{1}^{′♯}, ..., B_{n}^{′♯}}). Then {ϑ_{1}^{♯}}α-⊔_{Φ}{ϑ_{2}^{♯}} = {ϑ_{2}^{♯}}.

2. Correctness. We sketch the proof for the α-unification of a single concrete atom with a single abstract one. Let us consider a pair of atoms, A and A′, having the same predicate symbol p. We want to prove that α_{Φ}({mgu(A, A′)_{|var(A)}}) ≤_{Φ} {α-mgu(A, α({A′}))}. Thus: if mgu(A, A′) = F ail, then {F ail} ≤_{Φ} {ϑ^{♯}}, ∀ϑ^{♯} ∈ S_{var(A)}^{♯}.

Let us assume that the two atoms have the following structure,

A ≡ p(t_{1}, ..., t_{n}) and A′ ≡ p(t′_{1}, ..., t′_{n}),

and suppose that α_{Φ}({mgu(A, A′)_{|var(A)}})α-⊔_{Φ}{α-mgu(A, α({A′}))} =< β^{♯}, Ψ >, where < β^{♯}, Ψ >≠ {α-mgu(A, α({A′}))}.

Thus {α-mgu(A, α({A′}))} ≤_{Φ}< β^{♯}, Ψ >. Let

< β^{′♯}, Ψ′ >= {α-mgu(A, α({A′}))},

thus we can have:

• β^{♯} = {..., ng/x_{i}, ...} ∧ β^{′♯} = {..., g/x_{i}, ...} then α_{Φ}({mgu(A, A′)_{|var(A)}}) = {..., ng/x_{i}, ...}. This implies that the two atoms have the form

p(...x_{i}...) and p(...t′_{i}[y_{1}, ..., y_{k}]...).

Moreover if we consider the set of ground dependences (hyperarcs) Ψ′_{y_{1},...,y_{k}}, having the t′_{i}[y_{1}, ..., y_{k}] as head in α({A′}), we can have:

a. Ψ′_{y_{1},...,y_{k}} ≠ ∅. There does not exist any configuration of constants in p(...x_{i}...) which leads t′_{i}[y_{1}, ..., y_{k}] to be ground. Thus the corresponding tails (in the hypergraph) are never labeled by ∗, which is a contradiction since our hypothesis was β^{′♯} = {..., g/x_{i}, ...}.

b. Ψ′_{y_{1},...,y_{k}} = ∅, which is a contradiction since we assumed that β^{′♯} = {..., g/x_{i}, ...} (someone has to set t′_{i}[y_{1}, ..., y_{k}] to ground).

• Let us assume that β^{♯} = β^{′♯} and Ψ ≠ Ψ′. Thus we can distinguish two cases:

a. Ψ has a ground dependence belonging to α_{Φ}({mgu(A, A′)_{|var(A)}}) and not to Ψ′. This case leads to a contradiction since the ground dependence belonging to α_{Φ}({mgu(A, A′)_{|var(A)}}) can be inherited in the result iff its head is g in β^{′♯} (but β^{♯} = {..., ng/x_{i}, ...} ∧ β^{′♯} = {..., g/x_{i}, ...} is not possible), or if its tail is contained in a tail of a ground dependence belonging to Ψ′. But this is a contradiction because by abstracting we do not lose any ground dependence.

b. Let us assume that there exists ⟨{v_{i_{1}}^{♯}, ..., v_{i_{k}}^{♯}}, v_{i_{j}}^{♯}⟩ ∈ Ψ′ such that, the node {ng/x_{i_{j}}} cannot be reached in α_{Φ}({mgu(A, A′)_{|var(A)}}) from the nodes ng/x_{i_{h}}, for all h = 1, ..., k. Thus the two atoms have the form

p(...x_{i_{j}}...) and

p(...t_{i_{j}}[y_{1}, ..., y_{w}]...t_{i_{1}}[u_{i_{1,1}}, ..., u_{i_{1,d_{1}}} ]...t_{i_{k}}[u_{i_{k,1}}, ..., u_{i_{k,d_{k}}}]...)

and there exists at least a h′ ∈ {1, ..., w} such that

y_{h′} ∉ {u_{i_{1,1}}, ..., u_{i_{1,d_{1}}} , ..., u_{i_{k,1}}, ..., u_{i_{k,d_{k}}} }.
Thus α({p(...t_{i_{j}}[y_{1}, ..., y_{w}]...t_{i_{1}}[u_{i_{1,1}}, ..., u_{i_{1,d}}]...t_{i_{k}}[u_{i_{k,1}}, ..., u_{i_{k,d_{k}}}]...)})

does not contain the associated hyperarc ⟨{v_{i_{1}}^{♯}, ..., v_{i_{k}}^{♯}}, v_{i_{j}}^{♯}⟩, which is a contra-

diction, since ⟨{v_{i_{1}}^{♯}, ..., v_{i_{k}}^{♯}}, v_{i_{j}}^{♯}⟩ ∈ Ψ′.

□

α-apply(A, {< β^{♯}, Ψ >}) is the operator that returns the abstract atom obtained by replacing each variable in var(A) ∩ Dom(ϑ^{♯}) with the corresponding abstract term. As in the α-mgu case, an hypergraph (V, \overline{Ψ}) is associated with the α-apply process. Let us consider

α-apply(p(t_{1}, ..., t_{n}), {< V, (V_{ϑ}, Ψ_{ϑ}) >}).

The hypergraph associated with the α-apply process is built as follows

• V = ( ∪_{i=1}^{n} V_{i}) ∪ V_{ϑ} where V_{i} is a set of labeled (with i) variables in var(t_{i}),

• Ψ_{ϑ} ⊆ \overline{Ψ},

• ∀i ∈ {1, ..., n} such that x ∈ var(t_{i}) and x is bound to an abstract value (node) v_{j}^{♯}, ∃ < \{x_{i}\}, v_{j}^{♯} >, < \{v_{j}^{♯}\}, x_{i} >∈ \overline{Ψ} (x is a linked variable).

α − apply(p(t_{1}, ..., t_{n}), Φ^{♯}) = \{ \begin{matrix}∅ & if Φ^{♯} = \{F ail\} \\ < p, (V_{p}, Ψ_{p}) > & otherwise \end{matrix}

where the abstract atom < p, (V_{p}, Ψ_{p}) > results from a labelling process analogous to the one for the α-mgu computation, such that

• V_{p} is the set of nodes v_{i}^{♯} such that

v_{i}^{♯} = \{ \begin{matrix}g & iff V_{i} = ∅ (the term was already ground) \\ & or all the nodes in V_{i} are labeled by ∗ \\ ng & otherwise. \end{matrix}

• < {v_{i_{1}}^{♯}, ..., v_{i_{k}}^{♯}}, v_{j}^{♯} >∈ Ψ_{p} iff {i_{1}, ..., i_{k}} is the least set of indexes such that

– F ree(V_{j}) ⊆ ∪_{r=i_{1}}^{i_{k}} F ree(V_{r}), where F ree(V_{i}) is the set of nodes (variables) which are

not linked with any node in the hypergraph,

– all the linked nodes in V_{j} which are not labeled by ∗ are reachable (by a connection) from some linked nodes in V_{i_{1}}, ..., V_{i_{k}}.

This process is equivalent to consider ground dependences as variable sharing. The resulting abstract atom corresponds to the abstraction of a concrete atom where each variable which is bound to an abstract value (linked variable) is handled as a shared variable according to the corresponding hyperarc.

Example 4.10 Given a concrete atom p(f(x, y), z, c) (where V_{1} = {x, y}, V_{2} = {z} and V_{3} =

∅) and an abstract substitution [figure: (ng/y, ng/z)] , α-apply(p(f(x, y), z, c), { [figure: (ng/y, ng/z)] }) = p(ng, ng, ng) .

[figure: ng; ng; {x; y}_{1}; {z}_{2}]

Figure 4.4. Hypergraph associated with the α-apply computation

Note that the variables y and z are mutually dependent. When this dependence is applied to the whole atom, we have that if the first argument is ground then the second one is ground too, but not viceversa (F ree(V_{1}) = {x}, F ree(V_{2}) = ∅).

Proposition 4.3 α-apply(A, ∅) = α(A).

Proof. Let A ≡ p(t_{1}, ..., t_{n}). The hypergraph associated with the α-apply process has the form

({var(t_{1})_{1}, ..., var(t_{n})_{n}}, ∅).

There are no linked nodes in the hypergraph. Since F ree(V_{i}) = var(t_{i}), the only condition F ree(V_{j}) ⊆ ∪_{i∈T} F ree(V_{i}) for some set of indexes T ⊂ {1, ..., n}, is equivalent to the usual ground dependence condition. This corresponds to the abstraction of the atom as given by α. □

Theorem 4.4 α-apply verifies the monotonicity and the correctness properties.

Proof.

1. Monotonicity. Let us consider two sets of abstract substitutions, {ϑ_{1}^{♯}} and {ϑ_{2}^{♯}}, defined on the same set of variables V, such that {ϑ_{1}^{♯}} ≤_{Φ} {ϑ_{2}^{♯}}. Then, we can have

• V ∩ var(A) = ∅. Thus, {α-apply(A, {ϑ_{1}^{♯}})} = {α-apply(A, {ϑ_{2}^{♯}})} = α({A}).

• V ∩var(A) ≠ ∅. By definition it follows that {α-apply(A, {ϑ_{1}^{♯}})} ≤_{α} {α-apply(A, {ϑ_{2}^{♯}})}.

2. Correctness. By definition, given a set of concrete substitutions defined on the same set of variables V, Φ_{V}, both α({(Aϑ) | ϑ ∈ Φ_{V} }) and {α-apply(A, ϑ^{♯}) | ϑ^{♯} ∈ α_{Φ}(Φ_{V})} are singletons. Thus, if

• V ∩ var(A) = ∅, α-apply is trivially correct, since

α({A}) = {α-apply(A, ϑ^{♯}) | ϑ^{♯} ∈ α_{Φ}(Φ_{V})}.

• V ∩ var(A) ≠ ∅, let us assume that α({(Aϑ) | ϑ ∈ Φ_{V} }) = {A^{′♯}}, and \{α-apply(A, ϑ^{♯}) | ϑ^{♯} ∈ α_{Φ}(Φ_{V})\} = \{\overline{A}^{♯}\}.

Moreover, let us assume that \{A^{′♯}\}α-⊔\{\overline{A}^{♯}\} = \{Ã^{♯}\} and \{\overline{A}^{♯}\} ≠ \{Ã^{♯}\}.

Thus by definition, \{\overline{A}^{♯}\} ≤_{α} \{Ã^{♯}\}. The rest of this proof is analogous to the one given in the previous theorem, by considering abstract atoms instead of abstract substitutions.

□

From an operational viewpoint, it is interesting to consider the ground dependence information associated with the abstract π-model F^{♯}(P). In fact, if we analyze the hypergraphs associated with each atom p, it is possible to establish the ground structure of the success patterns for the program. Then, given a goal G, the abstract substitution resulting from the abstract unification process between the goal and F^{♯}(P) gives us the required ground information about the goal arguments.

Example 4.11 Let us consider the program P:

1. sum(x, 0, x).

2. sum(x, s(y), s(z)) : −sum(x, y, z).

The ground analysis is performed as follows, T_{P}^{♯} = λI^{♯}.(T_{C_{(1)}}^{♯}(I^{♯})α-⊔T_{C_{(2)}}^{♯}(I^{♯})), then

T_{P}^{♯^{1}}(∅) = { [figure: sum(ng, g, ng)] } (fixpoint).

The process converges in 1 step to F^{♯}(P) = { [figure: sum(ng, g, ng)] }.

Let us consider a goal ? − sum(x, y, s(s(0))). The abstract substitution resulting from the abstract unification between the (concrete) goal and the abstract atoms in F^{♯}(P) is

ϑ^{♯} = α-mgu(sum(x, y, s(s(0))), { [figure: sum(ng, g, ng)] })

where ϑ^{♯} = {g/x, g/y}, as shown in Figure 4.5.

[figure: ng*; g; ng*; x*; y*; ⊗]

Figure 4.5. The hypergraph associated with the ϑ^{♯} computation

Example 4.12 Given the logic program P:

1. append(nil, x, x).

2. append(cons(x, y), z, cons(x, u)) : −append(y, z, u).

3. length(nil, 0).

4. length(cons(x, y), s(z)) : −length(y, z). The associated abstract π-model is computed by:

• T_{P}^{♯^{1}}(∅) = { [figure: append(g, ng, ng)] }α-⊔{length(g, g)} =

{ [figure: append(g, ng, ng)] , length(g, g)}.

• T_{P}^{♯^{2}}(∅) = { [figure: append(g, ng, ng)] }α-⊔{ [figure: append(ng, ng, ng)] }α-⊔

{length(g, g)}α-⊔{length(ng, g)}

= { [figure: append(ng, ng, ng)] , length(ng, g)} (fixpoint).

(in fact, there is no ground propagation during the abstract unification between append(y, z, u)

and [figure: append(g, ng, ng)] , so that the resulting abstract substitution is

ϑ^{♯} = [figure: (g/y, ng/z, ng/u)] .

Since

[figure: ng; ng; g; {x y∗}_{1}; {z}_{2}; {x u}_{3}]

Figure 4.6. Hypergraph for the α-apply computation

we have α-apply(append(cons(x, y), z, cons(x, u)), ϑ^{♯}) = [figure: append(ng, ng, ng)] .

The abstract π-model

F^{♯}(P) = {length(ng, g), [figure: append(ng, ng, ng)] },

if compared to the standard one (for the append predicate),

F(P) = {append(cons(x_{1}, ..., x_{n}), z, cons(x_{1}, ..., x_{n}, z)) | n ≥ 0},

results to contain information about the ground dependences between the arguments of the goals.

There are further applications of the ground dependence analysis by means of the same abstract data representation. In [28, 29] the previous dataflow analysis is enhanced by means of labeled hypergraphs. Deterministic dependences [29] can then be exploited simply by adding a suitable set of labels to each hyperarc, without changing the abstraction framework. Moreover, the notion of dependence can also be specialized to capture depth-k ground dependence [28]. This technique is usefully applied to deduce information (i.e. pipeline AND-parallelism) to optimize the performance of AND/OR-parallel executions of logic programs in a massively parallel system [55].

4.1.1 Bottom-up Analysis and Call Patterns

As pointed out before, our groundness analysis determines an approximation of the program success set. In many cases one is interested in determining information about a specific procedure call (call pattern). Let us consider the following program and the related groundness information:

p(x, y, z) : −q(x, y), r(y, z), t(y).

r(x, y) : −s(x, y), t(y).

q(x, x). s(x, x). s(x, y) : −u(x, y). u(x, x). t(a). t(b).

The abstract π-model F^{♯}(P) is

{p(g, g, g), [figure: q(ng, ng)] , r(g, g), [figure: s(ng, ng)] , t(g), [figure: u(ng, ng)] }.

The procedure t has t(g) as success pattern. This means that any call to the procedure t results in a ground answer (if the answer is not the empty substitution). This information has no relation to the way in which t is called in the program clauses. In particular we might be interested in the call patterns in the first two clauses. The information about the procedure call p in a clause C can be obtained by abstractly unifying all the atoms which precede (according to the left-to-right computation rule) p in C with the atoms in the computed abstract π-model.

In the example, to obtain the information on the call of t in the first clause, we have to abstractly unify the goal ? − q(x, y), r(y, z) with atoms in F^{♯}(P). The only abstract unifier is the one with

[figure: q(ng, ng)] , r(g, g),

which binds x, y and z to g. Thus, in this clause the procedure t is always called with a ground argument. This allows several optimizations to be performed in the code of p (for example elimination of backtrack points [20]). In the second clause, the unification of the goal ? − s(x, y) with

[figure: s(ng, ng)]

binds y to ng, thus showing that t can be called with a non-ground argument.

Note that in this example, the call patterns are still goal independent, hence they allow a goal independent code optimization. If one is interested in a goal dependent analysis, a mixed top-down and bottom-up approach can be used. The mixed approach requires the introduction of abstract values in concrete goals and a suitable extension of the abstract unification. This extension is out of the scope of this paper. The approach can anyway informally be discussed on the example. Consider the mixed goal: ? − p(g, y, z) which represents any goal with the first argument ground. We are interested in the goal specific call pattern for t in the body of procedure r, which can be obtained by the following sequence of actions.

• Goal unification with the head of the first clause. This step produces the goal: ? − q(g, y), r(y, z), t(y).

• Abstract unification of q(g, y) with [figure: q(ng, ng)] . This action produces the mixed goal: ? − r(g, z).

• Goal unification with the head of the second clause. This step produces the goal: ? − s(g, y), t(y).

• Abstract unification of s(g, y) with [figure: s(ng, ng)] . This action produces the mixed goal: ? − t(g), which shows that the procedure t is always called with a ground argument whenever the computation starts with a call of procedure p with the first argument ground.

We have then shown that the computed abstract π-model can be used to obtain goal independent call patterns. It can also help in computing goal dependent call patterns. However, the top-down approach, which does not require the computation of the whole model, is definitely better if one is interested in goal dependent information only. Let us finally remark that the above considerations can naturally be extended to other applications.

4.2 Depth-k Abstractions

In this section we define an analysis scheme, based on the Sato & Tamaki’s work [56]. A very similar analysis can be found in [45]. The resulting abstract interpretation finds depth-k abstractions of success patterns for the atoms in the program. We can classify this kind of analysis as a type inference analysis. We can find some interesting applications for program specialization to most specific logic programs, in [44]. Let us consider the function depth : T_{Cons}(V ar) → ω, such that

depth(t) = \{ \begin{matrix}1 & if t is a constant or \\ & a variable \\ max(depth(t_{1}), ..., depth(t_{n})) + 1 & if t = f(t_{1}, ..., t_{n}) \end{matrix}

and let us consider a given positive integer k. The associated equivalence relation is ≈_{t}, such that t_{1} ≈_{t} t_{2} iff t_{1_{|depth−k}} = t_{2_{|depth−k}}, where t_{|depth−k} represents the term which can be obtained by substituting with a fresh variable both each subterm t′ in t, such that depth(t)−depth(t′) = k, and each multiple occurrence of the same variable.

We can define the abstract universe as the image of the map ρ = λt. t_{|depth−k}, U_{P}^{♯} = ρ(T_{Cons}(V ar)).

To specialize our abstraction scheme, we note that the abstract atoms and the abstract substitutions have the same structure as the corresponding concrete one. The congruence relation is the syntactic equality on abstract atoms. The observable properties in the abstract π-model are in fact the depth-k abstraction of all the success patterns for the program. In this case then we have H_{P} = 2^{B_{P}^{♯}}, Σ_{V} = 2^{S_{V}^{♯}}, α-⊔ ≡ ∪ and α-⊔_{Φ} ≡ ∪.

Let us define the α-mgu as the standard mgu operator returning a substitution mapping the set of variables of the concrete atoms to depth-k terms, that is

α-mgu((B_{1}, ..., B_{n}), I^{♯}) = \{ ϑ^{k} | \begin{matrix}ϑ = mgu((B_{1}, ..., B_{n}), (B_{1}^{♯}, ..., B_{n}^{♯}))_{|var(B_{1},...,B_{n})}, \\ ∧ B_{1}^{♯}, ..., B_{n}^{♯} ∈ I^{♯} \end{matrix} \}

where ϑ_{V}^{k} denotes a substitution mapping variables in V to depth-k terms.

It is trivial to prove that α-mgu satisfies the associated correctness and monotonicity properties. Moreover, by defining the α-apply operator as the abstraction of the concrete application, we obtain a corresponding correct abstract operator.

This abstraction allows to find a depth-k approximation of the fixpoint semantics of a given program P.

Example 4.13 Let us consider the logic program for the predicate sum . If k = 2, we obtain

T_{P}^{♯^{1}}(∅) = {sum(x, 0, x)},
T_{P}^{♯^{2}}(∅) = T_{P}^{♯^{1}}(∅) ∪ {sum(x, s(0), s(x))},
T_{P}^{♯^{3}}(∅) = T_{P}^{♯^{2}}(∅) ∪ {sum(x, s(s(x′)), s(s(x)))} (fixpoint).

The depth-2 abstraction of the success patterns associated with the program is

F^{♯}(P) = {sum(x, 0, x), sum(x, s(0), s(x)), sum(x, s(s(x′)), s(s(x)))}.

5 Related work

As already mentioned in the introduction, the idea of T_{P} -based bottom-up abstract interpretation goes back to [45], which considers general programs using as concrete semantics the one defined in [25]. Since this semantics is defined on a ground domain, the resulting abstract analysis is not able to capture computational properties related to the use of logical variables.

[46] solves the above problem by using a non-ground domain for interpretations. However, the resulting semantics, which is the same as the C-semantics in [23], can only model the non-ground logical consequences of a program but not the computed answer substitutions. For example this definition assigns the same meaning to the two programs {p(x)} and {p(x), p(a)}. In the following example we show that the strong soundness and completeness of the underlying concrete semantics [22, 23] allows to obtain better abstract information with respect to the usual Herbrand (ground) model approximation [45] and with respect to the bottom-up semanticsbased analysis framework given in [46].

Example 5.1 Let us consider the logic program

p(f(x)) : −p(x).
p(x) : −q(x).
q(x).
q(a).

For a depth-k analysis (the same holds for general type analysis), the abstract models returned for k = 2 are

• {p(x), q(x)} using the semantics in [46],

• {q(a), p(a), p(f(a)), p(f(f ))} using the standard ground T_{P},

• {q(a), q(x), p(a), p(x), p(f(a)), p(f(f(x)))} in our approach.

For a simple mode analysis, U_{P}^{♯} = {g, ng} and g ≤ ng, in which we are interested in collecting all the success patterns, we obtain

• {p(ng), q(ng)} using the semantics in [46] (the analysis approximates the success patterns by their least upper bound) ,

• {p(g), q(g)} using the standard ground T_{P} (this analysis is not even correct!),

• {p(g), p(ng), q(g), q(ng)} in our approach.

As we can observe, the abstract models we obtain are richer than the ones based on different semantics definitions.

The semantics defined in [23] was used in [4] (an earlier version of our framework) and independently used in [10, 37]. [10] extends our approach with an elegant mechanism to compute call patterns in a bottom-up way, by using program transformations.

In [37] an algebraic framework for the abstract interpretation of logic programs is presented. The main contribution of the paper is the use of the bottom-up framework to give a rigorous formalization of the Bruynooghe’s practical method [8, 9]. The main difference between [37] and our framework is the use of abstract substitutions. The presentation in [37] is given without considering the substitution notion, in terms of domains of tuples of atoms. The notion of refuted answer for a goal replaces the notion of computed answer substitution. This technique can always be “implemented” by composition of the α-mgu and α-apply operators. However, the resulting approach is different from the concrete semantics definition. Since the notion of abstract substitution does not make the resulting abstract semantics more complex, a distinction between

• α-unification: defining how abstract values are spread to concrete variables,

• α-application: defining how the bindings in an abstract substitution affect the resulting abstract atom structure,

allows to capture both the abstract model associated with a given logic program and an abstraction of the program observable properties, i.e. abstract computed answer substitutions.

Our abstract immediate consequences operators can be viewed as instances of a more general operator whose algebraic properties are defined in [17]. This characterization establishes a connection between fixpoint and transitive closure computations, thus allowing algorithms developed in the last area to be considered for bottom-up analysis.

6 Conclusions

In this paper we have developed a specializable scheme for bottom-up abstract interpretation of logic programs, based on a fixpoint characterization of the program success set. The resulting analysis is goal independent, and intrinsically deals with program success patterns. We have shown, on one meaningful application, the use of success patterns in computing (possibly goal dependent) call patterns. The framework can be extended to cope with different language features. One of these features is, of course, negation. However, to handle negation we first need a suitable generalization of the concrete semantics in [23] to general programs. In general, we can apply our framework to those features that can be expressed through a suitable immediate consequences operator. Our present interest is to define a program analysis technique which captures some Prolog peculiarities, as the left-to-right computation rule and the search strategy based on backtracking. The idea is to enhance a given (Prolog) program with a transformation defined in terms of an instance of the cc paradigm so that the standard meaning of the enhanced program reflects the required control information [2]. This approach to Prolog analysis, needs a richer abstract interpretation technique, general enough to handle the constraint logic programming paradigm.

In its present form, the approach can be instantiated to various analyses. The groundness analysis framework can be extended to deal with variable sharing analysis [15, 34, 51, 43, 48, 57]. The idea is to specialize our scheme, by using the same abstract universe of the groundness analysis and a different notion of dependence. Namely, there exists a dependence between some arguments iff the same variable occurs in all of them. The same problem has been considered in [10], where a bottom-up approach, based again on the concrete semantics in [23], is used. An extension of the notion of ground dependence may also be useful to detect cases when pipeline optimizations in AND-Parallelism are applicable. In [28] there is an application of our abstraction scheme able to detect ground dependences among subterms in list structures. This allows to detect that a partial binding generated by a producer may be exploited by a consumer to perform “useful computation”. The notion of “useful partial binding” is defined through a refinement of that of previously defined ground dependence, namely, a partial ground binding in a list structure is useful when it allows the consumer to produce ground bindings on other arguments. Finally, we developed [3] an application of our framework to polymorphic type inference extending the results in [36, 53].

Acknowledgments

The authors are indebted to the anonymous referees for many helpful comments and suggestions on an earlier version of this paper.

References

[1] S. Abramsky and C. Hankin. An Introduction to Abstract Interpretation. In S. Abramsky and C. Hankin, editors, Abstract Interpretation of Declarative Languages, pages 9–31. Ellis Horwood Ltd, 1987.

[2] R. Barbuti, M. Codish, R. Giacobazzi, and G. Levi. Modelling Prolog Control. In Proc. Nineteenth Annual ACM Symp. on Principles of Programming Languages. ACM, 1992.

[3] R. Barbuti and R. Giacobazzi. A Bottom-up Polymorphic Type Inference in Logic Programming. Technical Report TR 27/89, Dipartimento di Informatica, Università di Pisa, 1989.

[4] R. Barbuti, R. Giacobazzi, and G. Levi. A Declarative Abstract Semantics for Logic Programs. In A. Bertoni, C. Böhm, and P. Miglioli, editors, Proc. of the Third Italian Conference on Theoretical Computer Science, pages 84–96. World Scientific, 1989.

[5] R. Barbuti and A. Martelli. A Structured Approach to Semantics Correctness. Science of Computer Programming, 3:279–311, 1983.

[6] R. Barbuti and M. Martelli. Recognizing Non-Floundering Logic Programs and Goals. International Journal on Foundations of Computer Science, 1(2):151–163, 1990.

[7] G. Birkhoff. Lattice Theory. In AMS Colloquium Publication, third ed., 1967.

[8] M. Bruynooghe and G. Janssens. An Instance of Abstract Interpretation Integrating Type and Mode Inferencing. In R. A. Kowalski and K. A. Bowen, editors, Proc. Fifth Int’l Conf. on Logic Programming, pages 669–683. The MIT Press, Cambridge, Mass., 1988.

[9] M. Bruynooghe, G. Janssens, B. Demoen, and A. Callebaut. Abstract Interpretation: Towards the Global Optimization of Prolog Programs. In Proc Fourth IEEE Symp. Logic Programming, pages 192–204. IEEE Comp. Soc. Press, 1987.

[10] M. Codish, D. Dams, and E. Yardeni. Bottom-up Abstract Interpretation of Logic Programs. Technical report, Dept. of Computer Science, The Weizmann Institute, Rehovot, 1990.

[11] M. Corsini and G. Filè. A Complete Framework for the Abstract Interpretation of Logic Programs: Theory and Application. Technical report, Università di Padova, Italy, 1989.

[12] A. Cortesi and G. Filè. Abstract Interpretation of Logic Programs: an Abstract Domain for Groundness, Sharing, Freeness and Compoundness Analysis. In Proc. ACM Symposium on Partial Evaluation and Semantics-based Program Transformation. ACM 1991.

[13] P. Cousot and R. Cousot. Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. In Proc. Fourth ACM Symp. Principles of Programming Languages, pages 238–252, 1977.

[14] P. Cousot and R. Cousot. Systematic Design of Program Analysis Frameworks. In Proc. Sixth ACM Symp. Principles of Programming Languages, pages 269–282, 1979.

[15] P. Dart. On Derived Dependencies and Connected Databases. Technical Report No. 87/13, Dept. of Computer Science, Univ. of Melbourne, 1987.

[16] S. Debray. Efficient Dataflow Analysis of Logic Programs. In Proc. Fifteenth Annual ACM SIGACT-SIGPLAN Symp. on Principles of Programming Languages, pages 260–273, San Diego, 1988.

[17] S. Debray and R. Ramakrishnan. Generalized Horn Clause Programs. Technical report, Dept. of Computer Science, The Univ. of Arizona, Tucson, 1991.

[18] S. Debray. The Mythical Free Lunch (Notes on the Complexity/Precision Tradeoff in Dataflow Analysis of Logic Programs). Technical report, Dept. of Computer Science, The Univ. of Arizona, Tucson, 1991.

[19] S. Debray and D.S. Warren. Automatic Mode Inference for Logic Programs. Journal of Logic Programming, 5:207–230, 1988.

[20] B. Demoen, P. VanRoy, and Y.D. Willems. Improving the Execution Speed of Compiled Prolog with Modes, Clause Selection and Determinism. In H. Ehrig, R. Kowalski, G. Levi, and U. Montanari, editors, Proc. TAPSOFT 1987, volume 250 of Lecture Notes in Computer Science, pages 111–125. Springer-Verlag, Berlin, 1987.

[21] E. Eder. Properties of substitutions and unifications. Journal of Symbolic Computation, 1:31–46, 1985.

[22] M. Falaschi, G. Levi, M. Martelli, and C. Palamidessi. A new Declarative Semantics for Logic Languages. In R. A. Kowalski and K. A. Bowen, editors, Proc. Fifth Int’l Conf. on Logic Programming, pages 993–1005. The MIT Press, Cambridge, Mass., 1988.

[23] M. Falaschi, G. Levi, M. Martelli, and C. Palamidessi. Declarative Modeling of the Operational Behavior of Logic Languages. Theoretical Computer Science, 69(3):289–318, 1989.

[24] M. Falaschi, G. Levi, M. Martelli, and C. Palamidessi. A Model-Theoretic Reconstruction of the Operational Semantics of Logic Programs. Technical Report TR 32/89, Dipartimento di Informatica, Università di Pisa, 1989. To appear in Information and Computation.

[25] M. Fitting. A Kripke-Kleene semantics for logic programs. In Journal of Logic Programming, volume 2, pages 295–312, 1985.

[26] M. Gabbrielli and G. Levi. On the Semantics of Logic Programs. In J. Leach Albert and B. Monien and M. Rodriguez-Artalejo, editors, Proc. of the 18th International Colloquium on Automata, Languages and Programming, volume 510 of Lecture Notes in Computer Science, pages 1–19. Springer-Verlag, Berlin, 1991.

[27] J. Gallagher, M. Codish, and E. Shapiro. Specialization of Prolog and FCP Programs Using Abstract Interpretation. New Generation Computing, 6 (2-3):159–186, 1988.

[28] R. Giacobazzi and L. Ricci. Pipeline Optimizations in AND-Parallelism by Abstract Interpretation. In D. H. D. Warren and P. Szeredi, editors, Proc. Seventh Int’l Conf. on Logic Programming, pages 291–305. The MIT Press, Cambridge, Mass., 1990.

[29] R. Giacobazzi and L. Ricci. Detecting Determinate Computations by a Bottom-up Abstract Interpretation. In B. Krieg-Brückner, editor, ESOP’92, Proceedings, Lecture Notes in Computer Science. Springer-Verlag, Berlin, 1992.

[30] M. Hermenegildo. An Abstract Machine for Restricted AND-Parallel Execution of Logic Programs. In E. Y. Shapiro, editor, Proc. Third Int’l Conf. on Logic Programming, volume 225 of Lecture Notes in Computer Science, pages 25–40. Springer-Verlag, Berlin, 1986.

[31] M. Hermenegildo and R.I. Nasr. Efficient Management of Backtacking in AND-Parallelism. In E. Y. Shapiro, editor, Proc. Third Int’l Conf. on Logic Programming, volume 225 of Lecture Notes in Computer Science, pages 40–55. Springer-Verlag, Berlin, 1986.

[32] M. Hermenegildo and F. Rossi. On the Correctness and Efficiency of Independent And-Parallelism in Logic Programs. In E. Lusk and R. Overbeck, editors, Proc. North American Conf. on Logic Programming’89, pages 369–389. The MIT Press, Cambridge, Mass., 1989.

[33] H. Herrlich and M. Husek. Galois Connections. In A. Melton, editor, Mathematical Foundations of Program Semantics, volume 239 of Lecture Notes in Computer Science, pages 122–134. Springer-Verlag, Berlin, 1985.

[34] D. Jacobs and A. Langen. Accurate and Efficient Approximation of Variable Aliasing in Logic Programs. In E. Lusk and R. Overbeck, editors, Proc. North American Conf. on Logic Programming’89, pages 154–165. The MIT Press, Cambridge, Mass., 1989.

[35] N.D. Jones and H. Søndergaard. A Semantics-based Framework for the Abstract Interpretation of Prolog. In S. Abramsky and C. Hankin, editors, Abstract Interpretation of Declarative Languages, pages 123–142. Ellis Horwood Ltd, 1987.

[36] T. Kanomori and K. Horiuchi. Polymorphic Type Inference in Prolog by Abstract Interpretation. In Logic Programming 87- Tokyo, volume 315 of Lecture Notes in Computer Science, pages 195–214. Springer-Verlag, Berlin, 1988.

[37] R. Kemp and G. Ringwood. An Algebraic Framework for the Abstract Interpretation of Logic Programs. In S. Debray and M. Hermenegildo, editors, Proc. North American Conf. on Logic Programming’90, pages 506–520. The MIT Press, Cambridge, Mass., 1990.

[38] J.-L. Lassez, M. J. Maher, and K. Marriott. Unification Revisited. In J. Minker, editor, Foundations of Deductive Databases and Logic Programming, pages 587–625. Morgan Kaufmann, Los Altos, Ca., 1988.

[39] J.W. Lloyd. Foundations of Logic Programming. Springer-Verlag, Berlin, 1987. Second edition.

[40] M.J. Maher. Equivalences of Logic Programs. In J. Minker, editor, Foundations of Deductive Databases and Logic Programming, pages 627–658. Morgan Kaufmann, Los Altos, Ca., 1988.

[41] M.J. Maher and R. Ramakrishnan. Dèjà Vu in Fixpoints of Logic Programs. In E. Lusk and R. Overbeck, editors, Proc. North American Conf. on Logic Programming’89, pages 963–980. The MIT Press, Cambridge, Mass., 1989.

[42] P. Mancarella and D. Pedreschi. An Algebra of Logic Programs. In R. A. Kowalski and K. A. Bowen, editors, Proc. Fifth Int’l Conf. on Logic Programming, pages 1006–1023. The MIT Press, Cambridge, Mass., 1988.

[43] H. Mannila and E. Ukkonen. Flow Analysis of Prolog Programs. In Proc. 4th IEEE Symp. on Logic Programming, pages 205–214, 1987.

[44] K. Marriott. Finding Explicit Representations for Subsets of the Herbrand Universe. PhD thesis, University of Melbourne, 1988. Technical Report 88/22.

[45] K. Marriott and H. Søndergaard. Bottom-up Abstract Interpretation of Logic Programs. In R. A. Kowalski and K. A. Bowen, editors, Proc. Fifth Int’l Conf. on Logic Programming, pages 733–748. The MIT Press, Cambridge, Mass., 1988.

[46] K. Marriott and H. Søndergaard. Semantics-based Dataflow Analysis of Logic Programs. In G. Ritter, editor, Information Processing 89. North-Holland, 1989.

[47] C. Mellish. Some Global Optimizations for a Prolog Compiler. Journal of Logic Programming, 2:43–66, 1985.

[48] C. Mellish. Abstract Interpretation of Prolog Programs. In S. Abramsky and C. Hankin, editors, Abstract Interpretation of Declarative Languages, pages 181–198. Ellis Horwood Ltd, 1987.

[49] A. Melton, D.A. Schmidt, and G.E. Strecker. Galois Connections and Computer Science Applications. In D. Pitt et al., editor, Category Theory and Computer Programming, volume 240 of Lecture Notes in Computer Science, pages 299–312. Springer-Verlag, Berlin, 1986.

[50] A.O. Mendelzon. Functional Dependencies in Logic Programs. In Proc. of the Eleventh International Conference on Very Large Data Bases, pages 324–330, 1985.

[51] K. Muthukumar and M. Hermenegildo. Determination of Variable Dependence Information through Abstract Interpretation. In E. Lusk and R. Overbeck, editors, Proc. North American Conf. on Logic Programming’89, pages 166–185. The MIT Press, Cambridge, Mass., 1989.

[52] A. Mycroft. Abstract Interpretation and Optimising Transformations for Applicative Programs. PhD thesis, University of Edinburgh, 1981. CST-15/81.

[53] A. Mycroft and R.A. O’Keefe. A Polymorphic Type System for Prolog. Artificial Intelligence, 23:295–307, 1984.

[54] O. Ore. Galois Connections. In Trans. AMS, volume 55, pages 493–513, 1944.

[55] L. Ricci. Compilation of Logic Programs for Massively Parallel Systems. PhD thesis, Universitá di Pisa, Feb. 1990. T.D. 3-90.

[56] T. Sato and H. Tamaki. Enumeration of Success Patterns in Logic Programs. Theoretical Computer Science, 34:227–240, 1984.

[57] H. Søndergaard. An Application of Abstract Interpretation of Logic Programs: Occur Check Reduction. In B. Robinet and R. Wilhelm, editors, Proc. ESOP 86, volume 213 of Lecture Notes in Computer Science, pages 327–338. Springer-Verlag, Berlin, 1986.

[58] H. Søndergaard. Semantics-Based Analysis and Transformation of Logic Programs. PhD thesis, The University of Melbourne, June 1990. Revised version of PhD thesis, University of Copenhagen, December 1989.

[59] J.E. Stoy. Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory. MIT Press, 1977.

[60] M. H. van Emden and R. A. Kowalski. The semantics of predicate logic as a programming language. Journal of the ACM, 23(4):733–742, 1976.

[61] J. Zobel and P. Dart. On Logic Programs, Functional Dependencies, and Types. Technical report, University of Melbourne, 1990.