Functional Dependencies and Moore-Set Completions of Abstract Interpretations and Semantics

Roberto Giacobazzi Dipartimento di Informatica Università di Pisa Corso Italia 40, 56125 Pisa, Italy

giaco@di.unipi.it

Francesco Ranzato Dipartimento di Matematica Pura ed Applicata Università di Padova Via Belzoni 7, 35131 Padova, Italy

franz@hilbert.math.unipd.it

Abstract

We introduce the notion of functional dependencies of abstract interpretations relatively to a binary operator of composition. Functional dependencies are obtained by a functional composition of abstract domains, and provide a systematic approach to construct new abstract domains. In particular, we study the case of autodependencies, namely monotone operators on a given abstract domain. Under suitable hypotheses, this corresponds to a Moore-set completion of the abstract domain, providing a compact lattice-theoretic representation for dependencies. We prove that the abstract domain Def for ground-dependency analysis of logic programs can be systematically derived by autodependencies of a more abstract (and simple) domain for pure groundness analysis. Furthermore, we show that functional dependencies can be applied in collecting semantics design by abstract interpretation to systematically derive compositional semantics for logic programs.

1 Introduction

Functional dependencies belong to the standard Cousot and Cousot’s theory of abstract interpretation, and have been firstly introduced in [11] as domain combination for attribute dependent (or relational) analyses. In [11] the domain of functional dependencies corresponds precisely to the domain of monotone mappings between two abstract domains. Cousot and Cousot proved that this domain enjoys a Galois insertion under suitable hypotheses, like reduction with respect to concretization.

In this paper we exploit the definition of functional dependency in [11] by extending this notion to the functional composition of abstract domains relatively to a given concrete binary operator of composition, and apply it to data-flow analysis and semantics of logic programs. Our construction is general and can be applied to any abstract interpretation in the standard framework of Cousot and Cousot. The idea is to study the domain of monotone mappings between abstract domains which encode the data-dependencies between the corresponding abstractions via a concrete operator of composition. In particular, we prove that simple algebraic properties of the underlying operator of composition naturally induce relevant lattice-theoretic properties of the corresponding domain of functional dependencies. This is particularly significative in the case of autodependencies, i.e., the domain of monotone operators on a given abstract domain. In this case, the space of autodependencies can be associated with some well known space of functions, like closure operators, enjoying remarkable lattice-theoretic properties. We introduce the Moore-set completion for an abstract domain, and prove that, under suitable hypotheses, the space of autodependencies of an abstract domain corresponds precisely to its (dual-) Moore-set completion. The Moore-set completion provides a different and alternative information with respect to well known techniques for disjunctive completion of abstract domains, like down-set (order ideal) and anti-chain completion ([12, 14]). The Moore-set completion corresponds indeed to upgrade a given abstract domain with its autodependencies relatively to a lower bound concrete operator of composition.

Domain composition by functional dependencies provides a uniform approach to study the relational information in data-flow analysis and semantics design by abstract interpretation. In data-flow analysis, new and possibly more precise abstract domains can be derived by functional composition of simpler (abstract) domains. The relation between the Moore-set completion of an abstract domain and the space of its autodependencies is here a key point in order to give an alternative representation for dependencies in abstract domains. In particular, we prove in Subsection 5.1 that the well known domain Def of definite propositional formulae ([15]) for grounddependency analysis of logic programs ([24]), is actually isomorphic to the functional autodependencies of the more simple domain Ground (denoted G) for pure groundness analysis ([23, 24]), relatively to the operator of intersection of order ideals of substitutions. Also, Def is isomorphic to the dual-Moore-set completion of G. In semantics, abstract interpretation provides a systematic way to derive semantics at different levels of abstraction ([13, 21]). Functional composition can therefore be interpreted as a basic operator for semantic composition, providing a systematic method to design new more descriptive semantics for programming languages. In Subsection 5.2, we show that a compositional semantics for logic programs, with respect to the union of sets of clauses (i.e. programs), can be systematically derived by abstract interpretation from a more concrete semantics of SLD-traces. The compositional semantics corresponds to the functional autodependencies of a very abstract (non-compositional) semantics for computed answer substitutions ([17]), relatively to an operator of trace-unfolding. This provides an alternative characterization of the semantics in [6], and introduces a framework for the definition of new compositional semantics for logic programs. This approach has several advantages with respect to previous techniques (e.g., the approach in [6]). In particular, it can be applied to arbitrary semantics, provided that they can be derived by abstract interpretation from a more concrete (operational) one. This is the case (see [21]) for the semantics of call patterns ([19]), computed answer substitutions ([17]), Clark ([17]) and Herbrand ([27]), and other semantics for logic programs. This approach is general and independent from specific semantic representations (e.g., by means of atoms, clauses, etc.), and therefore it can be universally applied to design compositional semantics with respect to arbitrary observable properties.

Throughout the paper, we will assume familiarity with the standard notions of lattice theory ([5]) and abstract interpretation ([10, 11]).

2 Preliminaries

If A is a poset and I ⊆ A then ↓ I = {x ∈ A | ∃y ∈ I . x ≤_{A} y}. For x ∈ A, ↓ x is a shorthand for ↓ {x}. ℘^{↓}(A) denotes the set of order ideals of A, where I ⊆ A is an order ideal if I =↓ I . ℘^{↓}(A) is a complete lattice with respect to set-theoretic inclusion. If A is a poset with bottom element ⊥ then an element a ∈ A is an atom if a ≠ ⊥ and for all x ∈ A, ⊥ < x ≤ a implies x = a. A lattice is atomistic if every element different from ⊥ is the join of the atoms which precede it. The complete lattice of total (monotone, continuous) functions from the complete lattice A into the complete lattice B equipped with the functional pointwise order (i.e., f ⊑ g iff ∀x ∈ A. f (x) ≤_{B} g(x)) is denoted A → B (A→^{m}B, A→^{c}B). Let ⟨A, ≤, ∧, ∨, ⊤, ⊥⟩ be a complete lattice (sometimes simply denoted A_{≤}). An upper (lower) closure operator on A is a map ρ : A → A monotone, idempotent and extensive (reductive), i.e., for every x ∈ A, x ≤ ρ(x) (ρ(x) ≤ x). Any (upper or lower) closure operator ρ is uniquely determined by the set of its fixpoints, which is its image ρ(A) = fp(ρ). We denote uco(A) (lco(A)) the set of all upper (lower) closure operators on A. uco(A) and lco(A) are complete lattices with respect to the pointwise ordering. If ρ ∈ uco(A) (ρ ∈ lco(A)) then ρ(A) is a (dual-)Moore-set, i.e. a subset of A which contains ⊤ (⊥) and it is closed with respect to the glb (lub). If A and D are posets and α : D → A, γ : A → D are monotone maps such that ∀x ∈ D. x ≤_{D} γ(α(x)) and ∀y ∈ A. α(γ(y)) ≤_{A} y, then we call the quadruple (D, α, A, γ) a Galois connection (G.c.) between D and A. If in addition ∀y ∈ A. α(γ(y)) = y, then we call (D, α, A, γ) a Galois insertion (G.i.) of A in D. In the setting of abstract interpretation, D and A are called, respectively, the concrete and the abstract domain, and they are assumed to be complete lattices, whereas α and γ are called the abstraction and the concretization maps, respectively. Also, A is called an abstract interpretation (or abstraction) of D. If (D, α, A, γ) is a G.i., then the concretization and abstraction mappings, γ and α, are 1-1 and onto, respectively. Moreover, any G.c. may be lifted to a G.i. identifying in an equivalence class those values of the abstract domain with the same concrete meaning. This process is known as reduction of the abstract domain.

In the following, Σ, Π and Var will respectively denote a set of function symbols, a set of predicate symbols and a denumerable set of variables defining a first-order language L. The set of terms, atoms and Horn clauses over L are denoted Term, Atom and Clause, respectively. Term_{∅} and Atom_{∅} denote the corresponding sets of ground objects. The set of (definite) logic programs is denoted Program. Sequences of objects with the same type (variables, atoms, etc.) are sometimes denoted s̄. Concatenation of sequences is denoted ::. The empty sequence is Λ, while a | s̄ denotes a sequence with first element a. If A is a set of syntactic objects then inst(A) and ground(A) denote respectively the set of instances and ground instances of elements in A. We restrict our interest to idempotent substitutions ranging in Sub, unless explicitly stated otherwise. A syntactic object t is more general than t′ (denoted t′ ≤ t) iff there exists a substitution θ such that t′ = tθ. Syntactic objects t_{1} and t_{2} are equivalent up to renaming, denoted t_{1} ∼ t_{2}, iff t_{1} ≤ t_{2} and t_{2} ≤ t_{1}. Term_{/∼}, Atom_{/∼}, Clause_{/∼} and Sub_{/∼} are complete lattices with respect to ≤. With abuse of notation, they will be often denoted Term, Atom, Clause and Sub. Since all the definitions in the paper are independent on syntactic variable names, we will let a syntactic object to denote its equivalence class by renaming. For a syntactic object s and a set of (equivalence classes by renaming) of objects I , we denote by ⟨c_{1}, …, c_{n}⟩ <<_{s} I (n ≥ 0), that c_{1}, …, c_{n} are representatives of elements of I renamed apart from s and from each other.

3 Functional dependencies of abstract interpretations

In this section we study the functional dependencies between abstract domains relatively to a fixed basic operator of composition for concrete denotations. The basic underlying structure is called semantic structure, and it is defined as a complete lattice together with the binary operator of composition. This name is justified by its use in the semantic definition of logic programming, as shown later in Section 5.

Definition 3.1 A semantic structure is a pair ⟨D_{≤}, ⊙⟩, where D_{≤} is a complete lattice and ⊙ : D × D → D is a monotone binary operator on D. □

We consider functional dependencies relatively to a fixed semantic structure ⟨D_{≤}, ⊙⟩, namely we consider the domain of functional dependencies of denotations in D relatively to the basic composition operator ⊙.

Definition 3.2 Let ⟨D_{≤}, ⊙⟩ be a semantic structure, γ_{1} : D_{1} → D be a monotonic function between complete lattices and (D, α_{2}, D_{2}, γ_{2}) be a Galois connection. The domain of functional dependencies from D_{1} into D_{2} relatively to ⊙ is the set of functions {λx.α_{2}(d ⊙ γ_{1}(x)) ∈ D_{1} → D_{2} | d ∈ D}, partially ordered by the pointwise functional ordering relation, and denoted by D_{1}→^{⊙}D_{2}. □

It is worth noting that |D_{1}→^{⊙}D_{2}| ≤ |D|. Moreover, in the following we will often assume that γ_{1} belongs to a Galois connection, i.e. (D, α_{1}, D_{1}, γ_{1}) is a G.c.. In this case we call D_{1} and D_{2} the domain and range abstract interpretations.

The above definition of functional dependencies generalizes the original proposal of Cousot and Cousot in [11]. A functional dependency is here associated with any concrete denotation d ∈ D, and it is a mapping which associates with any abstract value x ∈ D_{1} an element of D_{2} which corresponds to the composition of d and x via ⊙. Therefore, a functional dependency in D_{1}→^{⊙}D_{2}, for a concrete object d ∈ D, encodes how d reacts when composed with any object described by the domain abstract interpretation D_{1}, with respect to the range abstract interpretation D_{2}.

Clearly, each functional dependency λx.α_{2}(d ⊙ γ_{1}(x)) is a monotone mapping, i.e., D_{1}→^{⊙}D_{2} ⊆ D_{1}→^{m}D_{2}. The poset of functional dependencies D_{1}→^{⊙}D_{2} is indeed a complete lattice, where the lub coincides with that of D_{1}→^{m}D_{2}, whenever ⊙ is left-additive.

Proposition 3.3 If ⊙ is left-additive then D_{1}→^{⊙}D_{2} is a complete join-sublattice of D_{1}→^{m}D_{2}.

In general, the lattice of monotone mappings D_{1}→^{m}D_{2} cannot be viewed as an abstract interpretation of D, unless ⊙ is left-additive, as specified below.

Theorem 3.4 If ⊙ is left-additive then (D, α, D_{1}→^{m}D_{2}, γ) is a Galois connection, where for any d ∈ D, α(d) = λx ∈ D_{1}.α_{2}(d ⊙ γ_{1}(x)).

It is now simple to associate with (D, α, D_{1}→^{m}D_{2}, γ) a corresponding Galois insertion by reducing the abstract domain D_{1}→^{m}D_{2}.

Corollary 3.5 Under the hypotheses of Theorem 3.4, D_{1}→^{⊙}D_{2} is isomorphic to (D_{1}→^{m}D_{2})_{/≡_{γ}}, where f ≡_{γ} g iff γ(f ) = γ(g), for any f , g ∈ D_{1}→^{m}D_{2}.

In view of the above basic results, in the rest of the paper we will take for granted the following assumption.

Assumption 3.6 In any semantic structure ⟨D_{≤}, ⊙⟩, ⊙ is left-additive. □

Example 3.7 Consider the following two abstract domains Sign and Parity for sign and parity analysis of an integer variable ([10, 11]).

[figure: ⊥_{s}; +; ⊤_{s}; −; •; •; •; •; ⊥_{p}; o; ⊤_{p}; e; •; •; •; •]

The corresponding G.i.’s are (℘(ZZ)_{⊆}, α_{s}, Sign, γ_{s}), (℘(ZZ)_{⊆}, α_{p}, Parity, γ_{p}), where abstraction and concretization mappings are the most natural. The domain of functional dependencies from Sign into Parity relatively to the glb ∩ of ℘(ZZ) is Sign→^{∩}Parity = {λx.α_{p}(S ∩ γ_{s}(x)) ∈ Sign → Parity | S ∈ ℘(ZZ)}, and, since ∩ is obviously left-additive, by Corollary 3.5, it enjoys a Galois insertion into ℘(ZZ). This lattice consists of twenty elements. It is a very expressive abstract interpretation since it allows to represent several sets of integers which are not representable neither in Sign nor in Parity. For example, this abstract interpretation is able to represent the sets of integers below.

• The null value

λx.α_{p}(\{0\} ∩ γ_{s}(x)) = \{ \begin{matrix}⊤_{s} & ↦ e \\ − & ↦ ⊥_{p} \\ + & ↦ ⊥_{p} \\ ⊥_{s} & ↦ ⊥_{p} \end{matrix} ⟼^{γ} \{0\}

• The positive and even integers

λx.α_{p}(\{x ∈ ZZ | x > 0, x even\}∩γ_{s}(x)) =\{ \begin{matrix}⊤_{s} & ↦ e \\ − & ↦ ⊥_{p} \\ + & ↦ e \\ ⊥_{s} & ↦ ⊥_{p} \end{matrix} ⟼^{γ} \{x ∈ ZZ | x > 0, x even\}

□

4 Autodependencies and Moore-set completions

A relevant case of functional dependencies between abstract interpretations is given by the autodependencies of an abstract domain.

Definition 4.1 Let ⟨D_{≤}, ⊙⟩ be a semantic structure, and (D, α, A, γ) be a Galois connection. The domain of autodependencies of A relatively to ⊙ is A→^{⊙}A. □

Therefore, A→^{⊙}A = {λx.α(d ⊙ γ(x)) ∈ A→^{m}A | d ∈ D}. Corollary 3.5 implies that autodependencies enjoy a Galois insertion into D (whenever ⊙ is left-additive). In the following, we adopt a more concise notation and often denote by Dep_{⊙}(A) the domain of autodependencies A→^{⊙}A. Note that Dep_{⊙}(A) is precisely the set of best correct approximations ([11]) of the family of concrete operators λx.d ⊙x ∈ D→^{m}D, for d ∈ D. Moreover, note that when ⊙ is an idempotent operator (i.e., ∀x. x ⊙x = x) which implements a lower (upper) bound operator on D (i.e., ∀x, y. x ⊙ y ≤ x, y (x, y ≤ x ⊙ y)), then λx.d ⊙ x ∈ lco(D) (λx.d ⊙ x ∈ uco(D)), for any d ∈ D.

The case of autodependencies for an abstract interpretation is important because it is always possible to identify some special cases where Dep_{⊙}(A) corresponds to well known function spaces. In particular, when ⊙ implements an idempotent lower (upper) bound operator on D, we obtain lower (upper) closure operators as denotations for autodependencies, as specified by the following result.

Theorem 4.2 Let (D, α, A, γ) be a G.c. and ⊙ be an idempotent binary operator.

(i) If ⊙ is a lower bound such that for any d, d′ ∈ D, γ(α(d ⊙d′)) ≤ d ⊙γ(α(d′)), then Dep_{⊙}(A) ⊆ lco(A).

(ii) If (D, α, A, γ) is a G.i. and ⊙ is an upper bound such that for any d, d′ ∈ D, d ⊙ γ(α(d′)) ≤ γ(α(d ⊙ d′)), then Dep_{⊙}(A) ⊆ uco(A).

Whenever ⊙ coincides with the glb of D, i.e. ⊙ = ∧, Assumption 3.6 of leftadditivity of ⊙ corresponds to the requirement that D is infinitely inf-distributive. Further, whenever ⊙ = ∨, Assumption 3.6 is obviously always satisfied. We call the dependencies in Dep_{∧}(A) and Dep_{∨}(A), meet-autodependencies and joinautodependencies, respectively. It is possible to show that in such cases the hypotheses for ⊙ in (i) and (ii) of Theorem 4.2 are satisfied.

Corollary 4.3

(i) If D is infinitely inf-distributive then Dep_{∧}(A) is a complete join-sublattice of lco(A).

(ii) If (D, α, A, γ) is a G.i. then Dep_{∨}(A) ⊆ uco(A).

The following is a simple example of meet-autodependencies.

Example 4.4 Consider the domain Sign of Example 3.7. Taking as concrete composition operator the glb ∩ of ℘(ZZ), by Corollary 4.3 (i), we have that Dep_{∩}(Sign) ⊆ lco(Sign). It is possible to verify that Dep_{∩}(Sign) = lco(Sign), and they correspond precisely to the following abstract domain, which includes denotations for possibly null values.

[figure: ⊥; [+]; [−]; [0]; [−0]; [0+]; ⊤; •; •; •; •; •; •; •]

The key point in this example is that Dep_{∩}(Sign) captures the null value [0], which is encoded by the lower closure λx.α({0} ∩ γ(x)), which corresponds to its dual-Moore-set of fixpoints {⊤, ⊥}. This provides the basis to define denotations for sets of non-negative and non-positive values, denoted respectively by [0+] and [−0], and corresponding to the lower closure operators λx.α(I^{+} ∩ γ(x)) and λx.α(I^{−} ∩ γ(x)), where I^{+} and I^{−} are any element in {I ∪ {0} ∈ ℘(ZZ) | I ≠ ∅, ∀x ∈ I . x > 0} and {I ∪ {0} ∈ ℘(ZZ) | I ≠ ∅, ∀x ∈ I . x < 0}, respectively. The set of fixpoints of these closures are, respectively, {⊤, +, ⊥} and {⊤, −, ⊥}, and they represent precisely the sets of non-negative and non-positive integers, respectively. □

We now introduce a powerset completion for abstract interpretations which provides a representation for spaces of functional autodependencies of abstract domains.

Definition 4.5 Let (D, α, A, γ) be a Galois connection. The (dual-)Moore-set completion of A is M(A) (DM(A)), where M(A) = {M ⊆ A | M is a Moore-set} (DM(A) = {M ⊆ A | M is a dual-Moore-set}), ordered by the supset (subset) relation. □

It is well known that M(A) is (isomorphic to) the complete lattice uco(A) of upper closure operators on A, while DM(A) is (isomorphic to) the complete lattice lco(A) of lower closure operators on A ([28]). The following two results relate the dual-Moore-set completion DM(A) to the abstract and concrete domains A and D.

Theorem 4.6 (DM(A), α̂, A, γ̂) is a Galois insertion, where α̂(M ) = ∨_{A}M and γ̂(a) = ↓a, for any M ∈ DM(A) and a ∈ A.

Theorem 4.7 Under the hypotheses of Theorem 4.2 (i), (D, α̃, DM(A), γ̃) is a Galois connection, where for any d ∈ D, α̃(d) = {x ∈ A | α(d ⊙ γ(x)) = x}.

Therefore, the dual-Moore-set completion of an abstract domain is an abstract interpretation (i.e. it enjoys a Galois insertion into the concrete domain), when reduced relatively to the corresponding autodependencies. Autodependencies are then the right way to interpret dual-Moore-set completions. Moreover, by Theorem 4.6, the dual-Moore-set completion is a domain refinement, namely it contains the original domain as an abstract interpretation. Note that the dual-Moore-set completion cannot be compared with the disjunctive completions introduced in [12, 14]. We consider the case of the down-set completion in the following example.

Example 4.8 Consider the domain Sign of Example 3.7. As pointed out in Example 4.4, the dual-Moore-set completion of Sign (viz. lco(Sign)) is exactly Dep_{∩}(Sign). By contrast, the down-set (or order ideal) completion of Sign is the domain ℘^{↓}(Sign) depicted below.

[figure: ⊥; +; ≠ 0; −; ⊤; •; •; •; •; •]

The dual-Moore-set completion of Sign, Dep_{∩}(Sign), does not provide a denotation for non-null values, which instead can be obtained by the down-set completion of Sign, ℘^{↓}(Sign), notably by the order ideal {+, −, ⊥}. This example shows that the dual-Moore-set completion does not correspond to the disjunctive down-set completion. □

The following result shows that the domain A is always an abstract interpretation of its meet-autodependencies Dep_{∧}(A), therefore extending Theorem 4.6 when^{1} Dep_{∧}(A) ⊂ lco(A) (cf. Corollary 4.3 (i)).

Proposition 4.9 If D is infinitely inf-distributive then (Dep_{∧}(A), ᾱ, A, γ̄) is a Galois insertion, where ᾱ(λx.α(d ∧ γ(x))) = ∨_{A}{y ∈ A | α(d ∧ γ(y)) = y} and γ̄(y) = λx.y ∧ x, for any d ∈ D and y ∈ A.

We now give a sufficient condition on abstract interpretations (D, α, A, γ) in order that meet-autodependencies of A and the dual-Moore-set completion of A coincide, i.e. Dep_{∧}(A) = lco(A).

1We write S ⊂ T if S is a proper subset of T.

Definition 4.10 A Galois insertion (D, α, A, γ) is separated if for any x ∈ A, there exists d_{x} ∈ D such that α(d_{x} ) = x, and for each y ∈ A such that x ≰_{A} y, d_{x} ∧ γ(y) = ⊥_{D} holds. □

It is well known ([11]) that in any G.i. (D, α, A, γ), the abstract domain A is isomorphic (by γ) with a (Moore-)set A_{D} ⊆ D. In separated abstract interpretations the elements in A_{D} are all join-irreducible, i.e., for any x ∈ A_{D}, x ≠ ⊥_{D}, and Y ⊆ A_{D}, x = ∨_{D}Y ⇒ x ∈ Y . Intuitively, in separated abstract interpretations each abstract denotation represents some concrete objects which cannot be described through the other denotations. Examples of separated abstract interpretations are the domain Sign of Example 3.7 and the abstract domain G of Subsection 5.1 for pure groundness analysis of logic programs. Note that both Dep_{∩}(Sign) and ℘^{↓}(sign) (cf. Example 4.4 and 4.8) are not separated (take x as [−0] and ≠0 respectively).

Theorem 4.11 If (D, α, A, γ) is a separated Galois insertion and D is infinitely inf-distributive, then Dep_{∧}(A) = lco(A).

When Dep_{∧}(A) = lco(A), the domain of meet-autodependencies enjoys the following lattice-theoretic properties inherited from lco(A): (1) Dep_{∧}(A) is atomistic ([28]);

(2) Dep_{∧}(A) is distributive or complemented or a Boolean algebra iff A is a complete well-ordered chain ([25]); and (3) if A satisfies the descending chain condition then Dep_{∧}(A) is dual-pseudo-complemented ([22]), namely for any x ∈ Dep_{∧}(A), there exists a unique x^{∗} ∈ Dep_{∧}(A) such that x ⊔x^{∗} = ⊤, and if x ⊔y = ⊤ then x^{∗} ⊑ y, for any y ∈ Dep_{∧}(A). Atomicity is an interesting property in abstract interpretation: atoms represent primitive properties, and each (non primitive) property can be generated by collecting primitive ones.

It is possible to see that in the case of join-autodependencies of A, Dep_{∨}(A) is always isomorphic to A.

Proposition 4.12 If (D, α, A, γ) is a Galois insertion then Dep_{∨}(A) ≅ A.

Therefore, we can conclude that while the meet-autodependencies may capture the dual-Moore-set completions, the join-autodependencies does not add any further information to the original domain of abstraction.

5 Applications: data-flow analysis and semantics

In this section, we consider two examples of applications of functional dependencies in the context of data-flow analysis of logic programs and systematic design of semantics for logic programs by abstract interpretation.

5.1 Systematic derivation of ground-dependency analysis

We show that the abstract domain Def , introduced by Dart in [15], and used by Marriott and Søndergaard for ground-dependency analysis in [24], can be systematically derived by meet-autodependencies of the more abstract (and simple) domain for pure groundness analysis G ([23, 24]), relatively to the set-theoretic intersection of order ideals of concrete substitutions.

Consider the following semantic structure for sets of concrete substitutions ⟨℘^{↓}(Sub)_{⊆}, ∩⟩, containing sets of substitutions closed by instantiation, viz. order ideals. The analysis of pure groundness for sets of substitutions in ℘^{↓}(Sub), relatively to a (non-empty) finite set of variables of interest V ⊆ Var, can be obtained by the Galois insertion (℘^{↓}(Sub), α_{g}, ℘(V )_{⊇}, γ_{g}), where for any Θ ∈ ℘^{↓}(Sub) and W ∈ ℘(V ), α_{g}(Θ) = {x ∈ V | ∀σ ∈ Θ. var(σ(x)) = ∅}, while γ_{g}(W ) = {σ ∈ Sub | ∀x ∈ W . var(σ(x)) = ∅}. It is worth noting that γ_{g} is closed by instantiation (i.e., if σ ∈ γ_{g}(W ) and σ′ ≤ σ then σ′ ∈ γ_{g}(W )), and therefore, correctly, γ_{g}(W ) is an order ideal. We denote by G_{V} the abstract domain ℘(V )_{⊇}, which is, clearly, a finite distributive lattice. In the case of two variables, G_{{x,y}} is depicted below.

[figure: {x, y}; {x}; ∅; {y}; •; •; •; •]

It is clear that Boolean functions can be represented by means of propositional formulae ([2, 24]). Recall that a Boolean function f is positive if f (true,…, true) = true. Def_{V} is the finite lattice (with respect to the usual implication partial order) of definite formulae on V , i.e. positive Boolean functions on V whose models are closed under intersection (for more details see [2]). The abstraction and concretization maps between Def and ℘^{↓}(Sub) are well known, and can be found, e.g., in [24]. Also in this case, we remark that the concretization of any definite formula is an order ideal of substitutions. As an example, assuming V = {x, y, z, u}, the formula x ∧ (y ↔ z) is an element of Def_{V} that represents all the substitutions σ such that for any instance σ′ of σ the following conditions hold: the term σ′(x) is ground, and σ′(y) is ground iff σ′(z) is ground. In particular, σ_{1} = {x/a, y/b, z/c} and σ_{2} = {x/a, y/w, z/w, v/u} satisfy this property. Thus, {σ_{1}, σ_{2}} ⊆ γ(x ∧ (y ↔ z)).

Clearly, the domain for groundness analysis G_{V} may be equivalently represented by means of conjunctive propositional formulae on V , by associating any W ∈ G_{V} with the formula ∧W (viz. the conjunction of all the variables in W ).

Def_{V} can be systematically derived by lifting G_{V} to its autodependencies, or, equivalently, by dual-Moore-set completion of G_{V} .

Proposition 5.1 (℘^{↓}(Sub), α_{g}, G_{V} , γ_{g}) is a separated abstract interpretation.

Therefore, by Theorem 4.11, Dep_{∩}(G_{V} ) = lco(G_{V} ) = DM(G_{V} ). The following result provides an alternative lattice-theoretic characterization of Def in terms of meet-autodependencies of groundness (or, alternatively, as dual-Moore-set completion of groundness).

Theorem 5.2 Def_{V} ≅ Dep_{∩}(G_{V} ) = DM(G_{V} ).

For the case of Def_{{x,y}}, we obtain the same lattice structure in Example 4.4.

[figure: x ∧ y; x; y; x ↔ y; x → y; y → x; true; •; •; •; •; •; •; •]

The correspondence between Def -formulae and dual-Moore-sets of G is given by the model-theoretic interpretation of Def -formulae. For V = {x, y} we have: x ∧ y = {{x, y}}, x = {{x}, {x, y}}, y = {{y}, {x, y}}, x ↔ y = {∅, {x, y}}, x → y = {∅, {y}, {x, y}}, y → x = {∅, {x}, {x, y}}, and true = {∅, {x}, {y}, {x, y}}.

It is worth noticing that the operation of conjunction, which usually implements abstract unification in ground-dependency analysis by Def , can be easily implemented by set-intersection on the corresponding dual-Moore-set completion. Furthermore, Def shares the lattice-theoretic properties of lower closures, being atomistic and dual-pseudo-complemented. In particular, by the first property, any element in Def_{V} can be represented as the join of the atoms that imply it. An atom is here a dual-Moore-set {W , V }, where W ∈ ℘(V ). For instance, the dependency x → y can be represented by joining the atomic dual-Moore sets {{y}, {x, y}} and {∅, {x, y}}. This may provide a concise representation for ground-dependencies. It is worth noting that Dep_{∩}(Def ) ≠ Def , namely Def is not dependency closed. In particular, the dependency relation (x → y) → y is precisely x ∨ y ∉ Def .^{2}

5.2 Systematic derivation of compositional semantics

In this subsection we systematically derive compositional semantics for logic programs by composing semantics according to their functional dependencies. In the following, a semantics for logic programs is a pair ⟨C , T ⟩, where C_{⊑} is a complete lattice (the semantic domain) and T : Program → (C →^{c}C ). T (P) is often denoted T_{P}, for P ∈ Program.

As Cousot and Cousot proved in [13], semantics of a programming language can all be derived by abstract interpretation of a more concrete reference semantics. A natural choice for a reference concrete semantics is the operational description of the computational process, which is in logic programming SLD resolution. In the following, we recall some basic results from [21], where a hierarchy of semantics for logic programs has been introduced, based on standard SLD resolution. We fix the Prolog left-to-right selection rule. The operational semantics of a logic program P is defined as execution traces in a labeled transition system defining SLD resolution as follows: SLD = ⟨State, {⟶^{c} | c ∈ P}⟩, where states are goals State = Atom^{∗}, and transitions are labeled with program clauses, ⟶^{c} ⊆ State × State, such that a | b̄⟶^{c}(body :: b̄)ϑ iff c = h ← body is a renamed apart clause in P, and ϑ = mgu(a, h). The transitive closure of ⟶ is denoted ⟶^{c̄}^{∗}, where c̄ ∈ P^{∗}. We denote T_{P}(SLD) the set of (finite) execution traces of SLD, with arbitrary elements π. π_{0} denotes the first element of the trace π. T_{P}(SLD) is inductively defined by the rules:

\frac{s ∈ State}{s ∈ T_{P}(SLD)} \frac{s⟶^{c}π_{0} ∧ π ∈ T_{P}(SLD)}{s⟶^{c}π ∈ T_{P}(SLD)}.

A key point in this construction is that execution traces can be equivalently represented by restricting the interest to AND-compositional execution traces only. Intuitively a set of traces is AND-compositional if the execution trace of any (possibly non-atomic) goal can be reconstructed by composing traces for its atomic subgoals. The inductive definition of the set E of AND-compositional execution traces for atomic goals is given in [21] as in Table 1. Rules 1 and 2 specify a big-step semantics as (positive) inductive definition with universe the set of traces from atomic goals only, denoted T_{P}^{a}(SLD) ⊆ T_{P}(SLD). The first rule specifies an atomic transition from an atomic goal h with clause c. The second rule specifies the AND-compositionality of derivations for a clause c. This is obtained by composing the successful transitions for the first k −1 atoms of the body, with the state (goal) produced from a derivation of the k^{th} atom of the body. The following theorem justifies the interest in AND-compositional traces, relating SLD-traces with AND-compositional ones.

2This observation is due to Roberto Bagnara.

1 \frac{c = h ← b_{1}, ..., b_{n} ∈ P}{h⟶^{c}⟨b_{1}, ..., b_{n}⟩ ∈ E} 2 \frac{c = h ← b_{1}, ..., b_{n} ∈ P ⟨⟨a_{i} ⟶^{c̄i}Λ⟩_{i=1}^{k−1}, a_{k} ⟶^{c̄k}b̄⟩ <<_{c} E (1 ≤ k ≤ n) θ = mgu(⟨b_{1}, ..., b_{k}⟩, ⟨a_{1}, ..., a_{k}⟩)}{(h⟶^{c}⟨b_{1}, ..., b_{n}⟩⟶^{c̄_{1}}...⟶^{c̄k}b̄ :: ⟨b_{k+1}, ..., b_{n}⟩)θ ∈ E}

Table 1: AND-compositional traces

Theorem 5.3 ([21]) Let G = g_{1}, ..., g_{n} be a goal. G⟶^{c̄}^{+}b̄ ∈ T_{P}(SLD) iff there exist ⟨⟨h_{i} ⟶^{c̄i}Λ⟩_{i=1}^{k−1}, h_{k} ⟶^{c̄k}b̄_{k}⟩ <<_{G} E (1 ≤ k ≤ n) s.t. δ = mgu(⟨g_{1}, ..., g_{k}⟩, ⟨h_{1}, ..., h_{k}⟩), c̄ = c̄_{1} :: ... :: c̄_{k}, and b̄ ∼ (b̄_{k} :: ⟨g_{k+1}, ..., g_{n}⟩)δ.

As usual (cf. [1]), a continuous operator φ_{P} on ℘(T_{P}^{a}(SLD)) can be systematically derived by the inductive definition of E in Table 1, such that E = lfp(φ_{P}). In the following, we consider ⟨℘(T_{P}^{a}(SLD))_{⊆}, φ_{P}⟩ as the reference semantics. Elements in ℘(T_{P}^{a}(SLD)) are called trace interpretations. This semantics models AND-compositional execution traces for atomic goals, yet providing a fixpoint operational semantics for logic programs which is equivalent to SLD resolution by Theorem 5.3.

The semantic domain ℘(T_{P}^{a}(SLD)) can be extended to a semantic structure by considering the trace-unfolding as basic binary operator for trace composition.

Definition 5.4 Define ∇ : ℘(T_{P}^{a}(SLD)) × ℘(T_{P}^{a}(SLD)) → ℘(T_{P}^{a}(SLD)) such that for any X , Y ∈ ℘(T_{P}^{a}(SLD)),

X ∇Y = \{ πϑ | \begin{matrix}c = h⟶^{c̄}b_{1}, ..., b_{n} ∈ X , \\ ⟨⟨a_{i} ⟶^{c̄i}Λ⟩_{i=1}^{k−1}, a_{k} ⟶^{c̄k}b̄⟩ <<_{c} Y (1 ≤ k ≤ n) \\ ϑ = mgu(⟨b_{1}, ..., b_{k}⟩, ⟨a_{1}, ..., a_{k}⟩), \\ π = h⟶^{c̄}⟨b_{1}, ..., b_{n}⟩⟶^{c̄_{1}}...⟶^{c̄k}b̄ :: ⟨b_{k+1}, ..., b_{n}⟩ \end{matrix} \} .

□

The trace-unfolding operator above satisfies the following basic algebraic properties.

Proposition 5.5 The operator ∇ is left-additive, i.e. (∪_{i∈I} X_{i})∇X = ∪_{i∈I} (X_{i}∇X ), associative ([16]), and ∅ is a left-annihilator for ∇, i.e. ∅∇X = ∅.

Hence, ⟨℘(T_{P}^{a}(SLD))_{⊆}, ∇⟩ is a semantic structure where the basic Assumption 3.6 is satisfied. In particular, Corollary 3.5 implies that if (℘(T_{P}^{a}(SLD)), α_{1}, D_{1}, γ_{1}) and (℘(T_{P}^{a}(SLD)), α_{2}, D_{2}, γ_{2}) are G.c.’s, then (℘(T_{P}^{a}(SLD)), α, D_{1}→^{∇}D_{2}, γ) is a Galois insertion, where for any trace interpretation I ∈ ℘(T_{P}^{a}(SLD)), α(I ) = λx.α_{2}(I ∇γ_{1}(x)). A trace interpretation is therefore abstracted in D_{1}→^{∇}D_{2} by a function that encodes the transformation by unfolding of traces approximated in D_{1} into traces approximated in D_{2}.

The key point here is that each Galois connection (℘(T_{P}^{a}(SLD)), α, D, γ) actually induces an (abstract) semantics for logic programs ⟨D, α∘φ_{P} ∘γ⟩, which is clearly correct^{3} with respect to the reference semantics ⟨℘(T_{P}^{a}(SLD)), φ_{P}⟩, yet providing the best correct approximation for φ_{P} in D. Therefore, any pair of semantics which can be derived from ⟨℘(T_{P}^{a}(SLD)), φ_{P}⟩ by abstract interpretation, can be functionally composed, yet providing a semantics for logic programs.

3In the sense of abstract interpretation ([10]), i.e. α(lfp(φ_{P} )) ≤_{D} lfp(α∘φ_{P} ∘γ).

The following is a list of some well known semantics for logic programs that can all be derived by abstract interpretation from ⟨℘(T_{P}^{a}(SLD)), φ_{P}⟩. Some of them have been used in [4, 8, 18] for data-flow analysis of logic programs. Each semantics is provided with the corresponding abstraction, hence with a G.c. (indeed insertion). A more complete treatment for semantics derivable by abstract interpretation from a reference semantics is in [9, 21]. In what follows, we denote γ_{x} the unique upper adjoint to α_{x} for x ∈ {s, Call, S, C, H}, and assume X ∈ ℘(T_{P}^{a}(SLD)).

• The sequence abstraction α_{s} is obtained by approximating finite traces by the pair of their initial and final states in a clause-like form. α_{s} : ℘(T_{P}^{a}(SLD)) → ℘(Clause) is such that α_{s}(X ) = {h ← b̄ | h⟶^{c̄}^{∗}b̄ ∈ X }. This abstraction induces a semantics which is equivalent to the semantics for partial answers in [19]. The semantics for call patterns in [19] can also be derived by further approximating partial answers. Recall that an atom a ∈ Atom is a call pattern for a goal G in a program P if G⟶^{c̄}^{∗}a | b̄ ∈ T_{P}(SLD). The corresponding abstraction α_{Call} : ℘(T_{P}^{a}(SLD)) → ℘(BClause) is α_{Call}(X ) = {h ← a | h⟶^{c̄}^{∗}a | b̄ ∈ X }, and induces a semantics which is equivalent to Call = ⟨℘(BClause)_{⊆}, T_{P}^{Call}⟩ (i.e., T_{P}^{Call} = α_{Call} ∘φ_{P} ∘γ_{Call}), where denotations are sets of binary clauses ranging in BClause, representing call patterns for atomic goals, and where by defining Φ = {h ← h | h ∈ Atom}, for each I ∈ ℘(BClause):

T_{P}^{Call}(I ) = \{ (h ← b)ϑ | \begin{matrix}c = h ← b_{1}, ..., b_{n} ∈ P (1 ≤ k ≤ n) \\ ⟨⟨a_{i} ← Λ⟩_{i=1}^{k−1}, ⟨a_{k} ← b⟩⟩ <<_{c} X ∪ Φ \\ ϑ = mgu(⟨b_{1}, ..., b_{k}⟩, ⟨a_{1}, ..., a_{k}⟩) \end{matrix} \} .

• The success abstraction α_{S} : ℘(T_{P}^{a}(SLD)) → ℘(Atom) approximates any finite successful trace with its initial state, while non successful traces are simply ignored: α_{S}(X ) = {h | h⟶^{c̄}^{∗}Λ ∈ X }. Notice that it induces a best correct approximation which is equivalent to the s-semantics ([17]) for computed answers, S = ⟨℘(Atom)_{⊆}, T_{P}^{S}⟩ (i.e., T_{P}^{S} = α_{S}∘φ_{P} ∘γ_{S}), where for each I ∈ ℘(Atom):

T_{P}^{S}(I ) = \{ hϑ | \begin{matrix}c = h ← b_{1}, ..., b_{n} ∈ P \\ ⟨b′_{1}, ..., b′_{n}⟩ <<_{c} I , n ≥ 0 \\ ϑ = mgu(⟨b_{1}, ..., b_{n}⟩, ⟨b′_{1}, ..., b′_{n}⟩) \end{matrix} \} .

• The Clark’s abstraction α_{C} = inst∘α_{S} maps successful traces to the set of instances of their initial states, while non successful traces are ignored. Notice that it induces a best correct approximation which is equivalent to Clark’s semantics for correct answers, C = ⟨inst(℘(Atom))_{⊆}, T_{P}^{C}⟩ (i.e., T_{P}^{C} = α_{C}∘φ_{P} ∘γ_{C}), where for each I ∈ inst(℘(Atom)): T_{P}^{C}(I ) = {hϑ | c = h ← b_{1}, ..., b_{n} ∈ P, ϑ ∈ Sub, b_{1}ϑ, ..., b_{n}ϑ ∈ I }.

• Finally, the Herbrand’s abstraction α_{H} = ground∘α_{S} maps successful traces to the set of ground instances for their initial states, while non-successful traces are ignored. The corresponding semantics is the well known Herbrand’s semantics ([27]), H = ⟨℘(Atom_{∅})_{⊆}, T_{P}^{H} ⟩ (i.e., T_{P}^{H} = α_{H}∘φ_{P} ∘γ_{H}), where for each I ∈ ℘(Atom_{∅}): T_{P}^{H} (I ) = {h ∈ Atom_{∅} | h ← b̄ ∈ ground(P), b̄ ⊆ I }.

Let A and B be semantics. In the following we abuse by letting A→^{∇}B denote both the semantics which corresponds to the functional composition of A and B, and its semantic domain. The following result provides a first semantic interpretation of functional autodependencies for the s-semantics S defined in [17].

Theorem 5.6 S→^{∇}S is isomorphic to ⟨℘(Clause), α_{s} ∘φ_{P} ∘γ_{s}⟩.

The abstraction of a trace interpretation I is an element in S→^{∇}S which encodes the dependency between input successful traces and output successful computations that can be obtained by unfolding traces in I . In particular, the elements in S→^{∇}S (i.e., λx.α_{S}(I ∇γ_{S}(x))) are actually the best correct approximations for the concrete operators λx.I ∇x : ℘(T_{P}^{a}(SLD)) → ℘(T_{P}^{a}(SLD)), for I ∈ ℘(T_{P}^{a}(SLD)). It is well known that λx.I ∇x is a T_{P}-like function ([16]). Hence, the isomorphism above is based on the correspondence between T_{P}-like functions and clauses, the latter encoding the functional dependency between their bodies and heads. It is worth noticing that S→^{∇}S corresponds to the well known compositional semantics of Bossi et al. introduced in [6], specialized for left-to-right selection rule and where each predicate in P is considered open. Denotations in S→^{∇}S are T_{P}-like functions. The main difference with the approach of Brogi and Turini [7] is that in [7] the semantics of a module is a T_{P}-like function, and compositionality is achieved by function composition, while in S→^{∇}S the semantics of a module is the fixpoint iteration of a transformation of T_{P}-like functions. It is straightforward to prove that S→^{∇}S is compositional in the sense of [6], i.e., if S→^{∇}S = ⟨D, T_{P}⟩ and F(P) = lfp(T_{P}) then for any P_{1}, P_{2} ∈ Program, F(P_{1} ∪P_{2}) = F(F(P_{1})∪F(P_{2})). Likewise, it is easy to define the semantics C→^{∇}C and H→^{∇}H, being all compositional in the sense of [6]. Note that H→^{∇}H is the compositional semantics in [20].

An interesting feature of this approach is that, being based on arbitrary Galois connections, it is independent on specific choices for semantic denotations. In particular, we can compose arbitrary semantics, without being constrained to look for corresponding syntactic objects as denotation, like clauses, binary clauses, atoms, etc., which is the case in the standard s-semantics approach. An interesting application of this idea is S→^{∇}Call. This semantics models the functional dependencies between successful computations for predicates and goal-independent call patterns. It is easy to see that denotations in S→^{∇}Call are functions from ℘(Atom) to ℘(BClause). In particular, a trace interpretation I ∈ ℘(T_{P}^{a}(SLD)) is abstracted by α_{s−c} into an object in S→^{∇}Call such that α_{s−c}(I ) = λY ∈ ℘(Atom).T_{αs (I )}^{Call}(Y ). A semantic interpretation for S→^{∇}Call can be obtained in modular logic programming by the following result. We adopt the notation in [8], and say that for a logic program (or module) P, open(P) denotes the set of predicates that occur in the body of a clause in P but are not defined in P. A program Q extends P if Q defines open(P). Let γ_{s−c} be the upper adjoint of α_{s−c}, and T_{P}^{s−c} = α_{s−c}∘φ_{P} ∘γ_{s−c}.

Theorem 5.7 Let P and Q be program modules such that Q extends P, and let G = g_{1}, ..., g_{n} be a goal. If f_{1}, ..., f_{k} ∈ lfp(T_{P}^{s−c}), 1 ≤ k ≤ n and for 1 ≤ i ≤ k − 1, h_{i} <<_{G} f_{i}(lfp(T_{Q}^{S})) and h_{k} ← b_{k} <<_{G} f_{k}(lfp(T_{Q}^{S})) are renamed apart, and ϑ = mgu(⟨h_{1}, ..., h_{k}⟩, ⟨g_{1}, ..., g_{k}⟩), then b_{k}ϑ is a call pattern for G in P ∪ Q.

6 Related works

The most related works are [3, 11, 12, 26]. Cousot and Cousot firstly defined the reduced cardinal power of abstract interpretations in [11]. This construction, relied upon the particular semantics of assertions, was based on functional composition with respect to the meet-operation on assertions, which restricted to additive functions is isomorphic to Nielson’s tensor product of [26]. We generalize those results for arbitrary operators of composition for concrete denotations, allowing the approach to be applicable to semantics of logic programming, where trace-unfolding does not behave like a meet-operation (e.g., it is not commutative). Note, however, that functional dependencies relatively to an operation of composition are included into the relational analysis defined by combination of reduced product and down-set completion ([12]). Recently, Bagnara in [3] has developed an elegant meta-language for domain combination which is based on a subset of a cc language, providing asynchronous interaction of domains. Because of this feature, the composition of abstract domains relies upon (lower) closure operators, which provide the standard semantic interpretation of cc. The use of cc-like expressions to combine domains is therefore equivalent to upgrade a domain with some of its lower closures, and it is in this sense an instance of the general notion of functional dependency, which is however sufficient to give an alternative characterization for Def . The key point here is that a cc language can be too restrictive to express arbitrary dependency relations between different abstract domains relatively to non-meet like operations of composition (e.g., in semantics design).

Acknowledgments

The stimulating discussions with Roberto Bagnara, Patrick Cousot and Enea Zaffanella are gratefully acknowledged. This work was partly done while the authors were visiting the LIX, Laboratoire d’Informatique, École Polytechnique, Paris. They thank LIX , and in particular Radhia Cousot, for the kind hospitality.

References

[1] P. Aczel. An introduction to inductive definitions. In Handbook of Mathematical Logic, pp. 739–782. North-Holland, 1977.

[2] T. Armstrong, K. Marriott, P. Schachte, and H. Søndergaard. Boolean functions for dependency analysis: algebraic properties and efficient representation. In Proc. SAS ’94, LNCS 864, pp. 266–280, 1994.

[3] R. Bagnara. Constraint systems for pattern analysis of constraint logic-based languages. In P. Codognet, editor, Proc. CCP ’95 Workshop, 1995. URL

    http://www.di.unipi.it/∼bagnara/bagnara.html.

[4] R. Barbuti, R. Giacobazzi, and G. Levi. A general framework for semanticsbased bottom-up abstract interpretation of logic programs. ACM TOPLAS, 15(1):133–181, 1993.

[5] G. Birkhoff. Lattice Theory. AMS Colloq. Public. vol. XXV, 3rd ed., 1967.

[6] A. Bossi, M. Gabbrielli, G. Levi, and M.C. Meo. A compositional semantics for logic programs. TCS, 122(1–2):3–47, 1994.

[7] A. Brogi and F. Turini. Fully abstract compositional semantics for an algebra of logic programs. To appear in TCS, 1995.

[8] M. Codish, S. Debray, and R. Giacobazzi. Compositional analysis of modular logic programs. In Proc. ACM POPL ’93, pp. 451–464, 1993.

[9] M. Comini and G. Levi. An algebraic theory of observables. In Proc. ILPS ’94, pp. 172–186, 1994.

[10] P. Cousot and R. Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proc. ACM POPL ’77, pp. 238–252, 1977.

[11] P. Cousot and R. Cousot. Systematic design of program analysis frameworks. In Proc. ACM POPL ’79, pp. 269–282, 1979.

[12] P. Cousot and R. Cousot. Abstract interpretation and application to logic programs. J. of Logic Programming, 13(2,3):103–179, 1992.

[13] P. Cousot and R. Cousot. Inductive definitions, semantics and abstract interpretation. In Proc. ACM POPL ’92, pp. 83–94, 1992.

[14] P. Cousot and R. Cousot. Higher-order abstract interpretation (and application to comportment analysis generalizing strictness, termination, projection and PER analysis of functional languages). In Proc. IEEE ICCL ’94, pp. 95–112, 1994.

[15] P. Dart. On derived dependencies and connected databases. J. of Logic Programming, 11(2):163–188, 1991.

[16] F. Denis and J.-P. Delahaye. Unfolding, procedural and fixpoint semantics of logic programs. In Proc. STACS ’91, LNCS 480, pp. 511–522, 1991.

[17] M. Falaschi, G. Levi, M. Martelli, and C. Palamidessi. Declarative modeling of the operational behavior of logic languages. TCS, 69(3):289–318, 1989.

[18] M. Gabbrielli and R. Giacobazzi. Goal independency and call patterns in the analysis of logic programs. In Proc. ACM SAC ’94, pp. 394–399, 1994.

[19] M. Gabbrielli and M.C. Meo. Fixpoint semantics for partial computed answer substitutions and call patterns. In Proc. ALP ’92, LNCS 632, pp. 84–99, 1992.

[20] H. Gaifman and E. Shapiro. Fully abstract compositional semantics for logic programs. In Proc. ACM POPL ’89, pp. 134–142, 1989.

[21] R. Giacobazzi. On the collecting semantics of logic programs. In Proc. Post-ICLP ’94 Workshop on Verif. and Analysis of Logic Lang., pp. 159–174, 1994.

URL http://www.di.unipi.it/∼giaco/giaco.html.

[22] R. Giacobazzi, C. Palamidessi, and F. Ranzato. Weak relative pseudocomplements of closure operators. Technical Report LIX/RR/95/04, Laboratoire d’Informatique, École Polytechnique, Paris, 1995. URL

http://www.di.unipi.it/∼giaco/giaco.html.

[23] N.D. Jones and H. Søndergaard. A semantics-based framework for the abstract interpretation of PROLOG. In Abstract Interpretation of Declarative Languages, pp. 123–142. Ellis Horwood Ltd., 1987.

[24] K. Marriott and H. Søndergaard. Precise and efficient groundness analysis for logic programs. ACM LOPLAS, 2(1–4):181–196, 1993.

[25] J. Morgado. Note on complemented closure operators of complete lattices. Portugal. Math., 21(3):135–142, 1962.

[26] F. Nielson. Tensor products generalize the relational data flow analysis method. In Proc. 4th Hung. Comp. Science Conf., pp. 211–225, 1985.

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

[28] M. Ward. The closure operators of a lattice. Ann. of Math., 43(2):191–196,