To appear on Theory and Practice of Logic Programming  1

Decomposing Non-Redundant Sharing by Complementation

ENEA ZAFFANELLA

Department of Mathematics, University of Parma, Italy (e-mail: zaffanella@cs.unipr.it)

PATRICIA M. HILL∗

School of Computing, University of Leeds, Leeds, U.K. (e-mail: hill@comp.leeds.ac.uk)

ROBERTO BAGNARA†

Department of Mathematics, University of Parma, Italy (e-mail: bagnara@cs.unipr.it)

Abstract

Complementation, the inverse of the reduced product operation, is a technique for systematically finding minimal decompositions of abstract domains. Filé and Ranzato advanced the state of the art by introducing a simple method for computing a complement. As an application, they considered the extraction by complementation of the pair-sharing domain PS from the Jacobs and Langen’s set-sharing domain SH . However, since the result of this operation was still SH , they concluded that PS was too abstract for this. Here, we show that the source of this result lies not with PS but with SH and, more precisely, with the redundant information contained in SH with respect to ground-dependencies and pair-sharing. In fact, a proper decomposition is obtained if the non-redundant version of SH , PSD, is substituted for SH . To establish the results for PSD, we define a general schema for subdomains of SH that includes PSD and Def as special cases. This sheds new light on the structure of PSD and exposes a natural though unexpected connection between Def and PSD. Moreover, we substantiate the claim that complementation alone is not sufficient to obtain truly minimal decompositions of domains. The right solution to this problem is to first remove redundancies by computing the quotient of the domain with respect to the observable behavior, and only then decompose it by complementation.

Keywords: Abstract Interpretation, Domain Decomposition, Complementation, Sharing Analysis.

1 Introduction

Complementation (Cortesi, Filé, Giacobazzi, Palamidessi and Ranzato 1997), which is the inverse of the well-known reduced product operation (Cousot and Cousot 1979), can systematically obtain minimal decompositions of complex abstract domains. It has been argued that these decompositions would be useful in finding

∗ This work was partly supported by EPSRC under grant GR/M05645. † The work of the first and third authors has been partly supported by MURST project “Certi-

ficazione automatica di programmi mediante interpretazione astratta.”

space saving representations for domains and to simplify domain verification problems.

In (Filé and Ranzato 1996), Filé and Ranzato presented a new method for computing the complement, which is simpler than the original proposal by Cortesi et al. (Cortesi, Filé, Giacobazzi, Palamidessi and Ranzato 1995, Cortesi et al. 1997) because it has the advantage that, in order to compute the complement, only a relatively small number of elements (namely the meet-irreducible elements of the reference domain) need be considered. As an application of this method, the authors considered the Jacobs and Langen’s sharing domain (Jacobs and Langen 1992), SH , for representing properties of variables such as groundness and sharing. This domain captures the property of set-sharing. Filé and Ranzato illustrated their method by minimally decomposing SH into three components; using the words of the authors (Filé and Ranzato 1996, Section 1):

“[…] each representing one of the elementary properties that coexist in the elements of Sharing, and that are as follows: (i) the ground-dependency information; (ii) the pairsharing information, or equivalently variable independence; (iii) the set-sharing information, without variable independence and ground-dependency.”

However, this decomposition did not use the usual domain PS for pair-sharing. Filé and Ranzato observed that the complement of the pair-sharing domain PS with respect to SH is again SH and concluded that PS was too abstract to be extracted from SH by means of complementation. Thus, in order to obtain their non-trivial decomposition of SH , they used a different (and somewhat unnatural) definition for an alternative pair-sharing domain, called PS′. The nature of PS′ and its connection with PS is examined more carefully in Section 6.

We noticed that the reason why Filé and Ranzato obtained this result was not to be found in the definition of PS, which accurately represents the property of pair-sharing, but in the use of the domain SH to capture the property of pairsharing. In (Bagnara, Hill and Zaffanella 1997, Bagnara, Hill and Zaffanella 2001), it was observed that, for most (if not all) applications, the property of interest is not set-sharing but pair-sharing. Moreover, it was shown that, for groundness and pairsharing, SH includes redundant elements. By defining an upper closure operator ρ that removed this redundancy, a much smaller domain PSD, which was denoted SH^{ρ} in (Bagnara et al. 1997), was found that captured pair-sharing and groundness with the same precision as SH . We show here that using the method given in (Filé and Ranzato 1996), but with this domain instead of SH as the reference domain, a proper decomposition can be obtained even when considering the natural definition of the pair-sharing domain PS. Moreover, we show that PS is exactly one of the components obtained by complementation of PSD. Thus the problem exposed by Filé and Ranzato was, in fact, due to the “information preserving” property of complementation, as any factorization obtained in this way is such that the reduced product of the factors gives back the original domain. In particular, any factorization of SH has to encode the redundant information identified in (Bagnara et al. 1997, Bagnara et al. 2001). We will show that such a problem disappears when PSD is used as the reference domain.

Although the primary purpose of this work is to clarify the decomposition of the domain PSD, the formulation is sufficiently general to apply to other properties that are captured by SH . The domain Pos of positive Boolean functions and its subdomain Def , the domain of definite Boolean functions, are normally used for capturing groundness (Armstrong, Marriott, Schachte and Søndergaard 1998). Each Boolean variable has the value true if the program variable it corresponds to is definitely bound to a ground term. However, the domain Pos is isomorphic to SH via the mapping from formulas in Pos to the set of complements of their models (Codish and Søndergaard 1998). This means that any general result regarding the structure of SH is equally applicable to Pos and its subdomains.

To establish the results for PSD, we define a general schema for subdomains of SH that includes PSD and Def as special cases. This sheds new light on the structure of the domain PSD, which is smaller but significantly more involved than SH .^{1} Of course, as we have used the more general schematic approach, we can immediately derive (where applicable) corresponding results for Def and Pos. Moreover, an interesting consequence of this work is the discovery of a natural connection between the abstract domains Def and PSD. The results confirm that PSD is, in fact, the “appropriate” abstraction of the set-sharing domain SH that has to be considered when groundness and pair-sharing are the properties of interest.

The paper, which is an extended version of (Zaffanella, Hill and Bagnara 1999), is structured as follows: In Section 2 we briefly recall the required notions and notations, even though we assume general acquaintance with the topics of lattice theory, abstract interpretation, sharing analysis and groundness analysis. Section 3 introduces the SH domain and several abstractions of it. The meet-irreducible elements of an important family of abstractions of SH are identified in Section 4. This is required in order to apply, in Section 5, the method of Filé and Ranzato to this family. In Section 6 we present some final remarks and we explain what is, in our opinion, the lesson to be learned from this and other related work. Section 7 concludes.

2 Preliminaries

For any set S, ℘(S) denotes the power set of S and # S is the cardinality of S.

A preorder ‘⪯’ over a set P is a binary relation that is reflexive and transitive. If ‘⪯’ is also antisymmetric, then it is called partial order. A set P equipped with a partial order ‘⪯’ is said to be partially ordered and sometimes written ⟨P, ⪯⟩. Partially ordered sets are also called posets.

A poset ⟨P, ⪯⟩ is totally ordered with respect to ‘⪯’ if, for each x, y ∈ P, either x ⪯ y or y ⪯ x. A subset S of a poset ⟨P, ⪯⟩ is a chain if it is totally ordered with respect to ‘⪯’.

Given a poset ⟨P, ⪯⟩ and S ⊆ P, y ∈ P is an upper bound for S if and only if x ⪯ y for each x ∈ S. An upper bound y for S is a least upper bound (or lub) of S if and only if, for every upper bound y′ for S, y ⪯ y′. The lub, when it exists,

1 For the well acquainted with the matter: SH is a powerset and hence it is dual-atomistic; this is not the case for PSD.

is unique. In this case we write y = lub S. Lower bounds and greatest lower bounds (or glb) are defined dually.

A poset ⟨L, ⪯⟩ such that, for each x, y ∈ L, both lub{x, y} and glb{x, y} exist, is called a lattice. In this case, lub and glb are also called, respectively, the join and the meet operations of the lattice. A complete lattice is a lattice ⟨L, ⪯⟩ such that every subset of L has both a least upper bound and a greatest lower bound. The top element of a complete lattice L, denoted by ⊤, is such that ⊤ ∈ L and ∀x ∈ L : x ⪯ ⊤. The bottom element of L, denoted by ⊥, is defined dually.

As an alternative definition, a lattice is an algebra ⟨L, ∧, ∨⟩ such that ∧ and ∨ are two binary operations over L that are commutative, associative, idempotent, and satisfy the following absorption laws, for each x, y ∈ L: x ∧ (x ∨ y) = x and x ∨ (x ∧ y) = x.

The two definitions of lattice are equivalent. This can be seen by defining:

x ⪯ y ⟺^{def} x ∧ y = x ⟺^{def} x ∨ y = y

and

glb{x, y} =^{def} x ∧ y,
lub{x, y} =^{def} x ∨ y.

The existence of an isomorphism between the two lattices L_{1} and L_{2} is denoted by L_{1} ≡ L_{2}.

A monotone and idempotent self-map ρ: P → P over a poset ⟨P, ⪯⟩ is called a closure operator (or upper closure operator) if it is also extensive, namely

∀x ∈ P : x ⪯ ρ(x).

Each upper closure operator ρ over a complete lattice C is uniquely determined by the set of its fixpoints, that is, by its image

ρ(C) =^{def} { ρ(x) | x ∈ C }.

We will often denote upper closure operators by their images. The set of all upper closure operators over a complete lattice C, denoted by uco(C), forms a complete lattice ordered as follows: if ρ_{1}, ρ_{2} ∈ uco(P), ρ_{1} ⊑ ρ_{2} if and only if ρ_{2}(C) ⊆ ρ_{1}(C). The reduced product of two elements ρ_{1} and ρ_{2} of uco(C) is denoted by ρ_{1} ⊓ ρ_{2} and defined as

ρ_{1} ⊓ ρ_{2} =^{def} glb{ρ_{1}, ρ_{2}}.

For a more detailed introduction to closure operators, the reader is referred to (Gierz, Hofmann, Keimel, Lawson, Mislove and Scott 1980).

A complete lattice C is meet-continuous if for any chain Y ⊆ C and each x ∈ C,

x ∧ (⋁ Y ) = ⋁_{y∈Y} (x ∧ y).

Most domains for abstract interpretation (Cortesi et al. 1997) and, in particular, all the domains considered in this paper are meet-continuous.

Assume that C is a meet-continuous lattice. Then the inverse of the reduced product operation, called weak relative pseudo-complement, is well defined and given as follows. Let ρ, ρ_{1} ∈ uco(C) be such that ρ ⊑ ρ_{1}. Then

ρ ∼ ρ_{1} =^{def} lub{ ρ_{2} ∈ uco(C) | ρ_{1} ⊓ ρ_{2} = ρ }.

Given ρ ∈ uco(C), the weak pseudo-complement (or, by an abuse of terminology now customary in the field of Abstract Interpretation, simply complement) of ρ is denoted by id_{C} ∼ ρ, where id_{C} is the identity over C. Let D_{i} =^{def} ρ_{D_{i}}(C) with ρ_{D_{i}} ∈ uco(C) for i = 1, …, n. Then { D_{i} | 1 ≤ i ≤ n } is a decomposition for C if C = D_{1} ⊓ ⋯ ⊓ D_{n}. The decomposition is also called minimal if, for each k ∈ ℕ with 1 ≤ k ≤ n and each E_{k} ∈ uco(C), D_{k} ⊏ E_{k} implies

C ⊏ D_{1} ⊓ ⋯ ⊓ D_{k−1} ⊓ E_{k} ⊓ D_{k+1} ⊓ ⋯ ⊓ D_{n}.

Assume now that C is a complete lattice. If X ⊆ C, then Moore(X) denotes the Moore completion of X, namely,

Moore(X) =^{def} { ⋀ Y | Y ⊆ X } .

We say that C is meet-generated by X if C = Moore(X). An element x ∈ C is meet-irreducible if

∀y, z ∈ C : ((x = y ∧ z) ⟹ (x = y or x = z)).

The set of meet-irreducible elements of a complete lattice C is denoted by MI(C). Note that ⊤ ∈ MI(C). An element x ∈ C is a dual-atom if x ≠ ⊤ and, for each y ∈ C, x ≤ y < ⊤ implies x = y. The set of dual-atoms is denoted by dAtoms(C). Note that dAtoms(C) ⊂ MI(C). The domain C is dual-atomistic if C = Moore(dAtoms(C)). Thus, if C is dual-atomistic, MI(C) = {⊤} ∪ dAtoms(C). The following result holds (Filé and Ranzato 1996, Theorem 4.1).

Theorem 1 If C is meet-generated by MI(C) then uco(C) is pseudo-complemented and for any ρ ∈ uco(C)

id_{C} ∼ ρ = Moore(MI(C) \ ρ(C)).

Another interesting result is the following (Filé and Ranzato 1996, Corollary 4.5).

Theorem 2 If C is dual-atomistic then uco(C) is pseudo-complemented and for any ρ ∈ uco(C)

id_{C} ∼ ρ = Moore(dAtoms(C) \ ρ(C)).

Let Vars be a denumerable set of variables. For any syntactic object o, vars(o) denotes the set of variables occurring in o. Let T_{Vars} be the set of first-order terms over Vars. If x ∈ Vars and t ∈ T_{Vars} \ {x}, then x ↦ t is called a binding. A substitution is a total function σ: Vars → T_{Vars} that is the identity almost everywhere. Substitutions are denoted by the set of their bindings, thus a substitution σ is identified with the (finite) set

{ x ↦ σ(x) | x ≠ σ(x) }.

If t ∈ T_{Vars}, we write tσ to denote σ(t). A substitution σ is idempotent if, for all t ∈ T_{Vars}, we have tσσ = tσ. The set of all idempotent substitutions is denoted by Subst.

It should be stressed that this restriction to idempotent substitutions is provided for presentation purposes only. In particular, it allows for a straight comparison of our work with respect to other works appeared in the literature. However, the results proved in this paper do not rely on the idempotency of substitutions and are therefore applicable also when considering substitutions in rational solved form (Colmerauer 1982, Colmerauer 1984). Indeed, we have proved in (Hill, Bagnara and Zaffanella 1998) that the usual abstract operations defined on the domain SH , approximating concrete unification over finite trees, also provide a correct approximation of concrete unification over a domain of rational trees.

3 The Sharing Domains

In order to provide a concrete meaning to the elements of the set-sharing domain of D. Jacobs and A. Langen (Jacobs and Langen 1989, Langen 1990, Jacobs and Langen 1992), a knowledge of the finite set VI ⊂ Vars of variables of interest is required. For example, in the Ph.D. thesis of Langen (Langen 1990) this set is implicitly defined, for each clause being analyzed, as the finite set of variables occurring in that clause. A clearer approach has been introduced in (Cortesi, Filé and Winsborough 1994, Cortesi, Filé and Winsborough 1998) and also adopted in (Bagnara et al. 1997, Bagnara et al. 2001, Cortesi and Filé 1999), where the set of variables of interest is given explicitly as a component of the abstract domain. During the analysis process, this set is elastic. That is, it expands (e.g., when solving clause’s bodies) and contracts (e.g., when abstract descriptions are projected onto the variables occurring in clause’s heads). This technique has two advantages: first, a clear and unambiguous description of those semantic operators that modify the set of variables of interest is provided; second, the definition of the abstract domain is completely independent from the particular program being analyzed. However, since at any given time the set of variables of interest is fixed, we can simplify the presentation by consistently denoting this set by VI . Therefore, in this paper all the abstract domains defined are restricted to a fixed set of variables of interest VI of finite cardinality n; this set is not included explicitly in the representation of the domain elements; also, when considering abstract semantic operators having some arguments in Subst, such as the abstract mgu, the considered substitutions are always taken to have variables in VI . We would like to emphasize that this is done for ease of presentation only: the complete definition of both the domains and the semantic operators can be immediately derived from those given, e.g., in (Bagnara et al. 1997, Bagnara et al. 2001). Note that other solutions are possible; we refer the interested reader to (Cortesi, Filé and Winsborough 1996, Section 7) and (Scozzari 2001, Section 10), where this problem is discussed in the context of groundness analysis.

3.1 The Set-sharing Domain SH

Definition 1 (The set-sharing domain SH .) The domain SH is given by

SH =^{def} ℘(SG),

where the set of sharing-groups SG is given by

SG =^{def} ℘(VI ) \ {∅}.

SH is partially ordered by set inclusion so that the lub is given by set union and the glb by set intersection.

Note that, as we are adopting the upper closure operator approach to abstract interpretation, all the domains we define here are ordered by subset inclusion. As usual in the field of abstract interpretation, this ordering provides a formalization of precision where the less precise domain elements are those occurring higher in the partial order. Thus, more precise elements contain less sharing groups.

Since SH is a power set, SH is dual-atomistic and

dAtoms(SH ) = { SG \ {S} | S ∈ SG }.

In all the examples in this paper, the elements of SH are written in a simplified notation, omitting the inner braces. For instance, the set

{{x}, {x, y}, {x, z}, {x, y, z}}

would be written simply as

{x, xy, xz, xyz}.

Example 1 Suppose VI = {x, y, z}. Then the seven dual-atoms of SH are:

\begin{matrix}s_{1} & = \{ y, z, xy, xz, yz, xyz\}, \\ s_{2} & = \{x, z, xy, xz, yz, xyz\}, \\ s_{3} & = \{x, y, xy, xz, yz, xyz\}, \end{matrix} \}  these lack a singleton;

\begin{matrix}s_{4} & = \{x, y, z, xz, yz, xyz\}, \\ s_{5} & = \{x, y, z, xy, yz, xyz\}, \\ s_{6} & = \{x, y, z, xy, xz, xyz\}, \end{matrix} \}  these lack a pair;

s_{7} = {x, y, z, xy, xz, yz  },  this lacks VI .

The meet-irreducible elements of SH are s_{1}, …, s_{7}, and the top element SG.

Definition 2 (Operations over SH .) The function bin: SH × SH → SH , called binary union, is given, for each sh_{1}, sh_{2} ∈ SH , by

bin(sh_{1}, sh_{2}) =^{def} { S_{1} ∪ S_{2} | S_{1} ∈ sh_{1}, S_{2} ∈ sh_{2} }.

The star-union function (·)^{⋆}: SH → SH is given, for each sh ∈ SH , by

sh^{⋆} =^{def} { S ∈ SG | ∃sh′ ⊆ sh . S = ⋃ sh′ }.

The j-self-union function (·)^{j}: SH → SH is given, for each j ≥ 1 and sh ∈ SH , by

sh^{j} =^{def} { S ∈ SG | ∃sh′ ⊆ sh . (# sh′ ≤ j, S = ⋃ sh′) }.

The extraction of the relevant component of an element of SH with respect to a subset of VI is encoded by the function rel: ℘(VI ) × SH → SH given, for each V ⊆ VI and each sh ∈ SH , by

rel(V, sh) =^{def} { S ∈ sh | S ∩ V ≠ ∅ }.

The function amgu captures the effects of a binding x ↦ t on an element of SH . Let sh ∈ SH , v_{x} = {x}, v_{t} = vars(t), and v_{xt} = v_{x} ∪ v_{t}. Then

amgu(sh, x ↦ t) =^{def} (sh \ (rel(v_{xt}, sh)) ∪ bin(rel(v_{x}, sh)^{⋆}, rel(v_{t}, sh)^{⋆}).

We also define the extension amgu: SH × Subst → SH by

amgu(sh, ∅) =^{def} sh,
amgu(sh, {x ↦ t} ∪ σ) =^{def} amgu(amgu(sh, x ↦ t), σ \ {x ↦ t}).

The function proj: SH ×℘(VI ) → SH that projects an element of SH onto a subset V ⊆ VI of the variables of interest is given, for each sh ∈ SH , by

proj(sh, V) =^{def} { S ∩ V | S ∈ sh, S ∩ V ≠ ∅ } ∪ { {x} | x ∈ VI \ V }.

Together with lub, the functions proj and amgu are the key operations that make the abstract domain SH suitable for computing static approximations of the substitutions generated by the execution of logic programs. These operators can be combined with simpler ones (e.g., consistent renaming of variables) so as to provide a complete definition of the abstract semantics. Also note that these three operators have been proved to be the optimal approximations of the corresponding concrete operators (Cortesi and Filé 1999). The j-self-union operator defined above is new. We show later when it may safely replace the star-union operator. Note that, letting j = 1, 2, and n, we have sh^{1} = sh, sh^{2} = bin(sh, sh), and, as # VI = n, sh^{n} = sh^{⋆}.

3.2 The Tuple-Sharing Domains

To provide a general characterization of domains such as the groundness and pairsharing domains contained in SH , we first identify the sets of elements that have the same cardinality.

Definition 3 (Tuples of cardinality k.) For each k ∈ ℕ with 1 ≤ k ≤ n, the overloaded functions tuples_{k}: SG → SH and tuples_{k}: SH → SH are defined as

tuples_{k}(S) =^{def} { T ∈ ℘(S) | # T = k },
tuples_{k}(sh) =^{def} ⋃{ tuples_{k}(S′) | S′ ∈ sh }.

In particular, if S ∈ SG and sh ∈ SH , let

pairs(S) =^{def} tuples_{2}(S),
pairs(sh) =^{def} tuples_{2}(sh).

The usual domains that represent groundness and pair-sharing information will be shown to be special cases of the following more general domain.

Definition 4 (The tuple-sharing domains TS_{k}.) For each k ∈ ℕ such that 1 ≤ k ≤ n, the function ρ_{_{TS}_{k}}: SH → SH is defined as

ρ_{_{TS}_{k}}(sh) =^{def} { S ∈ SG | tuples_{k}(S) ⊆ tuples_{k}(sh) }

and, as ρ_{_{TS}_{k}} ∈ uco(SH ), it induces the lattice

TS_{k} =^{def} ρ_{_{TS}_{k}}(SH ).

Note that ρ_{_{TS}_{k}}(tuples_{k}(sh)) = ρ_{_{TS}_{k}}(sh) and that there is a one to one correspondence between TS_{k} and ℘(tuples_{k}(VI )). The isomorphism is given by the functions tuples_{k}: TS_{k} → ℘(tuples_{k}(VI )) and ρ_{_{TS}_{k}}: ℘(tuples_{k}(VI )) → TS_{k}. Thus the domain TS_{k} is the smallest domain that can represent properties characterized by sets of variables of cardinality k. We now consider the tuple-sharing domains for the cases when k = 1, 2, and n.

Definition 5 (The groundness domain Con.) The upper closure operator ρ_{Con} : SH → SH and the corresponding domain Con are defined as

ρ_{Con} =^{def} ρ_{_{TS}_{1}},
Con =^{def} TS_{1}(SH ) = ρ_{Con}(SH ).

This domain, which represents groundness information, is isomorphic to a domain of conjunctions of Boolean variables. The isomorphism tuples_{1} maps each element of Con to the set of variables that are possibly non-ground. From the domain tuples_{1}(Con), by set complementation, we obtain the classical domain G (Jones and Søndergaard 1987) for representing the set of variables that are definitely ground (so that we have TS_{1} =^{def} Con ≡ G).

Definition 6 (The pair-sharing domain PS.) The upper closure operator ρ_{PS} : SH → SH and the corresponding domain PS are defined as

ρ_{PS} =^{def} ρ_{_{TS}_{2}},
PS =^{def} TS_{2}(SH ) = ρ_{PS}(SH ).

This domain represents pair-sharing information and the isomorphism tuples_{2} maps each element of PS to the set of pairs of variables that may be bound to terms that share a common variable. The domain for representing variable independence can be obtained by set complementation.

Finally, in the case when k = n we have a domain consisting of just two elements:

TS_{n} = {SG, SG \ {VI }}.

Note that the bottom of TS_{n} differs from the top element SG only in that it lacks the sharing group VI . There is no intuitive reading for the information encoded by this element: it describes all but those substitutions σ ∈ Subst such that ⋂{ vars(xσ) | x ∈ VI } ≠ ∅.

Just as for SH , the domain TS_{k} (where 1 ≤ k ≤ n) is dual-atomistic and:

dAtoms(TS_{k}) = { (SG \ { U ∈ SG | T ⊆ U }) | T ∈ tuples_{k}(VI ) }.

Thus we have

dAtoms(Con) = { (SG \ { U ∈ SG | x ∈ U }) | x ∈ VI },
dAtoms(PS) = { (SG \ { U ∈ SG | x, y ∈ U }) | x, y ∈ VI , x ≠ y }.

Example 2 Consider Example 1. Then the dual-atoms of Con are

r_{1} = s_{1} ∩ s_{4} ∩ s_{5} ∩ s_{7} = { y, z,  yz},
r_{2} = s_{2} ∩ s_{4} ∩ s_{6} ∩ s_{7} = {x, z, xz },
r_{3} = s_{3} ∩ s_{5} ∩ s_{6} ∩ s_{7} = {x, y, xy  };

the dual-atoms of PS are

m_{1} = s_{4} ∩ s_{7} = {x, y, z, xz, yz},
m_{2} = s_{5} ∩ s_{7} = {x, y, z, xy, yz},
m_{3} = s_{6} ∩ s_{7} = {x, y, z, xy, xz }.

It can be seen from the dual-atoms that, for each j = 1, …, n, where j ≠ k, the precision of the information encoded by domains TS_{j} and TS_{k} is not comparable. Also, we note that, if j < k, then ρ{TS \atop j}(TS_{k}) = \{SG\} and ρ_{_{TS}_{k}}(TS_{j}) = TS_{j}.

3.3 The Tuple-Sharing Dependency Domains

We now need to define domains that capture the propagation of groundness and pair-sharing; in particular, the dependency of these properties on the further instantiation of the variables. In the same way as with TS_{k} for Con and PS, we first define a general subdomain TSD_{k} of SH . This must be safe with respect to the tuple-sharing property represented by TS_{k} when performing the usual abstract operations. This was the motivation behind the introduction in (Bagnara et al. 1997, Bagnara et al. 2001) of the pair-sharing dependency domain PSD. We now generalize this for tuple-sharing.

Definition 7 The tuple-sharing dependency domain (TSD_{k}.) For each k where 1 ≤ k ≤ n, the function ρ_{_{TSD}_{k}}: SH → SH is defined as

ρ_{_{TSD}_{k}}(sh)

=^{def} { S ∈ SG | ∀T ⊆ S : # T < k ⟹ S = ⋃{ U ∈ sh | T ⊆ U ⊆ S } },

and, as ρ_{_{TSD}_{k}} ∈ uco(SH ), it induces the tuple-sharing dependency lattice

TSD_{k} =^{def} ρ_{_{TSD}_{k}}(SH ).

It follows from the definitions that the domains TSD_{k} form a strict chain.

Proposition 1 For j, k ∈ ℕ with 1 ≤ j < k ≤ n, we have TSD_{j} ⊂ TSD_{k}.

Moreover, TSD_{k} is not less precise than TS_{k}.

Proposition 2 For k ∈ ℕ with 1 ≤ k ≤ n, we have TS_{k} ⊆ TSD_{k}. Furthermore, if n > 1 then TS_{k} ⊂ TSD_{k}.

As an immediate consequence of Propositions 1 and 2 we have that that TSD_{k} is not less precise than TS_{1} ⊓ ⋯ ⊓ TS_{k}.

Corollary 1 For j, k ∈ ℕ with 1 ≤ j ≤ k ≤ n, we have TS_{j} ⊆ TSD_{k}.

It also follows from the definitions that, for the TSD_{k} domain, the star-union operator can be replaced by the k-self-union operator.

Proposition 3 For 1 ≤ k ≤ n, we have ρ_{_{TSD}_{k}}(sh^{k}) = sh^{⋆}.

We now instantiate the tuple-sharing dependency domains for the cases when k = 1, 2, and n.

Definition 8 (The ground dependency domain Def .) The domain Def is induced by the upper closure operator ρ_{Def} : SH → SH . They are defined as

ρ_{Def} =^{def} ρ_{_{TSD}_{1}},
Def =^{def} TSD_{1} = ρ_{Def} (SH ).

By Proposition 3, we have, for all sh ∈ SH , ρ_{_{TSD}_{1}}(sh) = sh^{⋆} so that TSD_{1} is a representation of the domain Def used for capturing groundness. It also provides evidence for the fact that the computation of the star-union is not needed for the elements in Def .

Definition 9 (The pair-sharing dependency domain PSD.) The upper closure operator ρ_{PSD} : SH → SH and the corresponding domain PSD are defined as

ρ_{PSD} =^{def} ρ_{_{TSD}_{2}},
PSD =^{def} TSD_{2} = ρ_{PSD}(SH ).

Then, it follows from (Bagnara et al. 1997, Theorem 7) that PSD corresponds to the domain SH^{ρ} defined for capturing pair-sharing. By Proposition 3 we have, for all sh ∈ SH , that ρ_{PSD}(sh^{2}) = sh^{⋆}, so that, for elements in PSD, the starunion operator sh^{⋆} can be replaced by the 2-self-union sh^{2} = bin(sh, sh) without any loss of precision. This was also proved in (Bagnara et al. 1997, Theorem 11). Furthermore, Corollary 1 confirms the observation made in (Bagnara et al. 1997) that PSD also captures groundness.

Finally, letting k = n, we observe that TSD_{n} = SH . Figure 1 summarizes the relations between the tuple-sharing and the tuple-sharing dependency domains.

As already discussed at the start of this section, the set of variables of interest VI is fixed and, to simplify the notation, omitted. In (Bagnara et al. 1997, Bagnara et al. 2001) the domains SS and SS^{ρ} (corresponding to SH and PSD, respectively) are instead obtained by explicitly adding to each domain element a new component, representing the set of variables of interest. It is shown that SS^{ρ} is as good as SS for both representing and propagating pair-sharing and it is also proved that any weaker domain does not satisfy these properties, so that SS^{ρ} is the quotient (Cortesi et al. 1994, Cortesi et al. 1998) of SS with respect to the pair-sharing property PS.

We now generalize and strengthen the results in (Bagnara et al. 1997, Bagnara et al. 2001) and show that, for each k ∈ {1, …, n}, TSD_{k} is the quotient of SH with respect to the reduced product TS_{1} ⊓ ⋯ ⊓ TS_{k}. These results are proved at the end of this section.

Theorem 3 Let sh_{1}, sh_{2} ∈ SH and 1 ≤ k ≤ n. If ρ_{_{TSD}_{k}}(sh_{1}) = ρ_{_{TSD}_{k}}(sh_{2}) then, for each

TS_{1} = Con _{TS_{2}} = PS  _{TS_{3}}  _{TS_{n−1}}  _{TS_{n}} ⨅_{i=1}^{2}_{TS_{i}} TSD_{1} = Def  ⨅_{i=1}^{3}_{TS_{i}} TSD_{2} = PSD _{TSD_{3}}  ⨅_{i=1}^{n−1}_{TS_{i}}_{TSD_{n−1}} TSD_{n} = ⨅_{i=1}^{n} TS_{i} = SH

Fig. 1. The set-sharing domain SH and some of its abstractions.

σ ∈ Subst, each sh′ ∈ SH , and each V ∈ ℘(VI ),

ρ_{_{TSD}_{k}}(amgu(sh_{1}, σ)) = ρ_{_{TSD}_{k}}(amgu(sh_{2}, σ)),
ρ_{_{TSD}_{k}}(sh′ ∪ sh_{1}) = ρ_{_{TSD}_{k}}(sh′ ∪ sh_{2}),
ρ_{_{TSD}_{k}}(proj(sh_{1}, V)) = ρ_{_{TSD}_{k}}(proj(sh_{2}, V)).

Theorem 4 Let 1 ≤ k ≤ n For each sh_{1}, sh_{2} ∈ SH , ρ_{_{TSD}_{k}}(sh_{1}) ≠ ρ_{_{TSD}_{k}}(sh_{2}) implies

∃σ ∈ Subst, ∃j ∈ \{1, …, k\} . ρ{TS \atop j}(amgu(sh_{1}, σ)) ≠ ρ{TS \atop j}(amgu(sh_{2}, σ)).

3.4 Proofs of Theorems 3 and 4

In what follows we use the fact that ρ_{_{TSD}_{k}} is an upper closure operator so that, for each sh_{1}, sh_{2} ∈ SH ,

sh_{1} ⊆ ρ_{_{TSD}_{k}}(sh_{2}) ⟺ ρ_{_{TSD}_{k}}(sh_{1}) ⊆ ρ_{_{TSD}_{k}}(sh_{2}).  (1)

In particular, since (·)^{⋆} = ρ_{_{TSD}_{1}}, we have

sh_{1} ⊆ sh_{2}^{⋆} ⟺ sh_{1}^{⋆} ⊆ sh_{2}^{⋆}.  (2)

Lemma 1 For each sh ∈ SH and each V ∈ ℘(VI ),

ρ_{_{TSD}_{k}}(sh) \ rel(V, ρ_{_{TSD}_{k}}(sh)) = ρ_{_{TSD}_{k}}(sh \ rel(V, sh)).

Proof By Definition 7,

S ∈ ρ_{_{TSD}_{k}}(sh \ rel(V, sh))

⟺ ∀T ⊆ S : (# T < k ⟹ S = ⋃{ U ∈ sh \ rel(V, sh) | T ⊆ U ⊆ S })

⟺ ∀T ⊆ S : (# T < k ⟹ S = ⋃{ U ∈ sh | T ⊆ U ⊆ S })
∧ S ∩ V = ∅
⟺ S ∈ ρ_{_{TSD}_{k}}(sh) \ rel(V, ρ_{_{TSD}_{k}}(sh)).

Lemma 2 For each sh_{1}, sh_{2} ∈ SH , each V ∈ ℘(VI ) and each k ∈ ℕ with 1 < k ≤ n,

ρ_{_{TSD}_{k}}(sh_{1}) ⊆ ρ_{_{TSD}_{k}}(sh_{2}) ⟹ rel(V, sh_{1})^{⋆} ⊆ rel(V, sh_{2})^{⋆}.

Proof We prove that

sh_{1} ⊆ ρ_{_{TSD}_{k}}(sh_{2}) ⟹ rel(V, sh_{1}) ⊆ rel(V, sh_{2})^{⋆}.

The result then follows from Eqs. (1) and (2).

Suppose S ∈ rel(V, sh_{1}). Then, S ∈ sh_{1} and V ∩ S ≠ ∅. By the hypothesis, S ∈ ρ_{_{TSD}_{k}}(sh_{2}). Let x ∈ V ∩ S. Then, by Definition 7, we have

S = ⋃{ U ∈ sh_{2} | {x} ⊆ U ⊆ S }
= ⋃{ U ∈ rel(V, sh_{2}) | {x} ⊆ U ⊆ S }.

Thus S ∈ rel(V, sh_{2})^{⋆}.

Lemma 3 For each sh_{1}, sh_{2} ∈ SH , each σ ∈ Subst and each k ∈ ℕ with 1 ≤ k ≤ n,

ρ_{_{TSD}_{k}}(sh_{1}) = ρ_{_{TSD}_{k}}(sh_{2}) ⟹ ρ_{_{TSD}_{k}}(amgu(sh_{1}, σ)) = ρ_{_{TSD}_{k}}(amgu(sh_{2}, σ)).

Proof If σ = ∅, the statement is obvious from the definition of amgu. In the other cases, the proof is by induction on the size of σ. The inductive step, when σ has more than one binding, is straightforward. For the base case, when σ = {x ↦ t}, we have to show that

sh_{1} ⊆ ρ_{_{TSD}_{k}}(sh_{2}) ⟹ amgu(sh_{1}, {x ↦ t}) ⊆ ρ_{_{TSD}_{k}}(amgu(sh_{2}, {x ↦ t})).

The result then follows from Eq. (1).

Let v_{x} =^{def} {x}, v_{t} =^{def} vars(t), and v_{xt} =^{def} v_{x} ∪ v_{t}. Suppose

S ∈ amgu(sh_{1}, {x ↦ t}).

Then, by definition of amgu,

S ∈ (sh_{1} \ rel(v_{x} ∪ v_{t}, sh_{1})) ∪ bin(rel(v_{x}, sh_{1})^{⋆}, rel(v_{t}, sh_{1})^{⋆}).

There are two cases:

1. S ∈ sh_{1} \ rel(v_{x} ∪ v_{t}, sh_{1}). Then, by hypothesis, S ∈ ρ_{_{TSD}_{k}}(sh_{2}). Hence we have S ∈ ρ_{_{TSD}_{k}}(sh_{2}) \ rel(v_{x} ∪ v_{t}, ρ_{_{TSD}_{k}}(sh_{2})). Thus, by Lemma 1,

S ∈ ρ_{_{TSD}_{k}}(sh_{2} \ rel(v_{x} ∪ v_{t}, sh_{2})).

2. S ∈ bin(rel(v_{x}, sh_{1})^{⋆}, rel(v_{t}, sh_{1})^{⋆}). Then we must have S = T ∪ R where T ∈ rel(v_{x}, sh_{1})^{⋆} and R ∈ rel(v_{t}, sh_{1})^{⋆}.

The proof here splits into two branches, 2a and 2b, depending on whether k > 1 or k = 1.

2a. We first assume that k > 1. Then, by Lemma 2 we have that T ∈ rel(v_{x}, sh_{2})^{⋆} and R ∈ rel(v_{t}, sh_{2})^{⋆}. Hence,

S ∈ bin(rel(v_{x}, sh_{2})^{⋆}, rel(v_{t}, sh_{2})^{⋆}).

Combining case 1 and case 2a we obtain

S ∈ ρ_{_{TSD}_{k}}(sh_{2} \ rel(v_{x} ∪ v_{t}, sh_{2})) ∪ bin(rel(v_{x}, sh_{2})^{⋆}, rel(v_{t}, sh_{2})^{⋆}).

Hence as ρ_{_{TSD}_{k}} is extensive and monotonic

S ∈ ρ_{_{TSD}_{k}}((sh_{2} \ rel(v_{x} ∪ v_{t}, sh_{2})) ∪ bin(rel(v_{x}, sh_{2})^{⋆}, rel(v_{t}, sh_{2})^{⋆})),

and hence, when k > 1, S ∈ ρ_{_{TSD}_{k}}(amgu(sh_{2}, {x ↦ t})).

2b. Secondly suppose that k = 1. In this case, we have, by Proposition 3:

ρ_{_{TSD}_{1}}(sh_{2}) = sh_{2}^{⋆}

and that

ρ_{_{TSD}_{1}}(amgu(sh_{2}, {x ↦ t})) = amgu(sh_{2}, {x ↦ t})^{⋆}.

Thus, by the hypothesis,

S ∈ bin(rel(v_{x}, sh_{2}^{⋆})^{⋆}, rel(v_{t}, sh_{2}^{⋆})^{⋆}),
= bin(rel(v_{x}, sh_{2}^{⋆}), rel(v_{t}, sh_{2}^{⋆})).

Therefore we can write

S = T ∪ T_{x} ∪ R ∪ R_{t}

where

T ∪ T_{x} ∈ rel(v_{x}, sh_{2}^{⋆}),
R ∪ R_{t} ∈ rel(v_{t}, sh_{2}^{⋆}),
T , R ∈ (sh_{2} \ rel(v_{xt}, sh_{2}))^{⋆},
T_{x} ∈ rel(v_{x}, sh_{2})^{⋆} \ ∅,
R_{t} ∈ rel(v_{t}, sh_{2})^{⋆} \ ∅.

Thus

S ∈ ((sh_{2} \ rel(v_{xt}, sh_{2})) ∪ bin(rel(v_{x}, sh_{2})^{⋆}, rel(v_{t}, sh_{2})^{⋆}))^{⋆}
= amgu(sh_{2}, {x ↦ t})^{⋆}.

Combining case 1 and case 2b for k = 1, the result follows immediately by the monotonicity and extensivity of (·)^{⋆}.

Lemma 4 For each sh_{1}, sh_{2} ∈ SH ,

ρ_{_{TSD}_{k}}(sh_{1} ∪ sh_{2}) = ρ_{_{TSD}_{k}}(ρ_{_{TSD}_{k}}(sh_{1}) ∪ ρ_{_{TSD}_{k}}(sh_{2})).

Proof This is a classical property of upper closure operators (Gierz et al. 1980).

Lemma 5 For each sh_{1}, sh_{2} ∈ SH and each V ⊆ VI ,

ρ_{_{TSD}_{k}}(sh_{1}) = ρ_{_{TSD}_{k}}(sh_{2}) ⟹ ρ_{_{TSD}_{k}}(proj(sh_{1}, V)) = ρ_{_{TSD}_{k}}(proj(sh_{2}, V)).

Proof We show that

sh_{1} ⊆ ρ_{_{TSD}_{k}}(sh_{2}) ⟹ proj(sh_{1}, V) ⊆ ρ_{_{TSD}_{k}}(proj(sh_{2}, V)).

The result then follows from Eq. (1).

Suppose sh_{1} ⊆ ρ_{_{TSD}_{k}}(sh_{2}) and S ∈ proj(sh_{1}, V). Then, as proj is monotonic, we have S ∈ proj(ρ_{_{TSD}_{k}}(sh_{2}), V ). We distinguish two cases.

1. There exists x ∈ V such that S = {x}. Then S ∈ proj(sh_{2}, V) and hence, by Definition 7, S ∈ ρ_{_{TSD}_{k}}(proj(sh_{2}, V)).

2. Otherwise, by definition of proj and Definition 7, there exists S′ ∈ ρ_{_{TSD}_{k}}(sh_{2}) such that S = S′ ∩ V and

∀T ⊆ S′ : (# T < k ⟹ S = ⋃{ U ∈ sh_{2} | T ⊆ U ⊆ S′ } ∩ V ).

Hence

∀T ⊆ S : (# T < k ⟹ S = ⋃{ U ∈ proj(sh_{2}, V) | T ⊆ U ⊆ S }),

and thus S ∈ ρ_{_{TSD}_{k}}(proj(sh_{2}, V)).

Proof of Theorem 3. Statements 1, 2 and 3 follow from Lemmas 3, 4 and 5, respectively.

The following lemma is also proved in (Bagnara et al. 1997, Bagnara et al. 2001) but we include it here for completeness.

Lemma 6 Let σ =^{def} {x_{1} ↦ t_{1}, …, x_{n} ↦ t_{n}}, where, for each i = 1, …, n, t_{i} is a ground term. Then, for all sh ∈ SH we have

amgu(sh, σ) = sh \ rel({x_{1}, …, x_{n}}, sh).

Proof If n = 0, so that σ = ∅, the statement can be easily verified after having observed that rel(∅, sh) = ∅. Otherwise, if n > 0, we proceed by induction on n. For the base case, let n = 1. Then

amgu(sh, x_{1} ↦ t_{1}) = sh \ rel({x_{1}}, sh) ∪ bin(rel({x_{1}}, sh)^{⋆}, rel(∅, sh)^{⋆})
= sh \ rel({x_{1}}, sh).

For the inductive step, let n > 1 and let

σ′ =^{def} {x_{1} ↦ t_{1}, …, x_{n−1} ↦ t_{n−1}}.

By definition of amgu we have

amgu(sh, σ) = amgu(sh, {x_{n} ↦ t_{n}} ∪ σ′)
= amgu(amgu(sh, {x_{n} ↦ t_{n}}), σ′)
= amgu(sh \ rel({x_{n}}, sh), σ′)
= (sh \ rel({x_{n}}, sh)) \ rel({x_{1}, …, x_{n−1}}, sh \ rel({x_{n}}, sh))

= sh \ (rel({x_{n}}, sh) ∪ rel({x_{1}, …, x_{n−1}}, sh \ rel({x_{n}}, sh)))

= sh \ rel({x_{1}, …, x_{n}}, sh).

Proof of Theorem 4. We assume that S ∈ ρ_{_{TSD}_{k}}(sh_{1}) \ ρ_{_{TSD}_{k}}(sh_{2}). (If such an S does not exist we simply swap sh_{1} and sh_{2}.)

Let C denote a ground term and let

σ =^{def} { x ↦ C | x ∈ VI \ S }.

Then, by Lemma 6, for i = 1, 2, we define amgu(sh_{i}, σ) =^{def} sh_{i}^{S} where

sh_{1}^{S} =^{def} { T ⊆ S | T ∈ sh_{1} },
sh_{2}^{S} =^{def} { T ⊂ S | T ∈ sh_{2} }.

Now, if # S = j and j ≤ k, then we have S ∈ sh_{1} \ sh_{2}. Hence S ∈ sh_{1}^{S} \ sh_{2}^{S} and we can easily observe that S ∈ ρ{TS \atop j}(sh_{1}^{S}) but S ∉ ρ{TS \atop j}(sh_{2}^{S}).

On the other hand, if # S = j and j > k, then by Definition 7 there exists T with # T < k such that

S = ⋃{ U ∈ sh_{1}^{S} | T ⊆ U }

but

S ⊃ ⋃{ U ∈ sh_{2}^{S} | T ⊆ U } =^{def} S′.

Let x ∈ S \ S′. We have h =^{def} #(T ∪ {x}) ≤ k and thus we can observe that T ∪ {x} ∈ ρ_{_{TS}_{h}}(sh_{1}^{S}) but T ∪ {x} ∉ ρ_{_{TS}_{h}}(sh_{2}^{S}).

4 The Meet-Irreducible Elements

In Section 5, we will use the method of Filé and Ranzato (Filé and Ranzato 1996) to decompose the dependency domains TSD_{k}. In preparation for this, in this section, we identify the meet-irreducible elements for the domains and state some general results.

We have already observed that TS_{k} and TSD_{n} = SH are dual-atomistic. However, TSD_{k}, for k < n, is not dual-atomistic and we need to identify the meetirreducible elements. In fact, the set of dual-atoms for TSD_{k} is

dAtoms(TSD_{k}) = { SG \ {S} | S ∈ SG, # S ≤ k }.

Note that # dAtoms(TSD_{k}) = ∑_{j=1}^{k} \binom{n}{j}. Specializing this for k = 1 and k = 2, respectively, we have

dAtoms(Def ) = { SG \ {{x}} | x ∈ VI },
dAtoms(PSD) = { SG \ {S} | S ∈ pairs(VI ) } ∪ dAtoms(Def ),

and we have # dAtoms(Def ) = n and # dAtoms(PSD) = n(n + 1)/2. We present as an example of this the dual-atoms for Def and PSD when n = 3.

Example 3 Consider Example 1. Then the 3 dual-atoms for Def are s_{1}, s_{2}, s_{3} and the 6 dualatoms for PSD are s_{1}, …, s_{6}. Note that these are not all the meet-irreducible elements since sets that do not contain the sharing group xyz such as {x} and ⊥ = ρ_{Def} (⊥) = ∅ cannot be obtained by the meet (which is set intersection) of a set of dual-atoms. Thus, unlike Con and PS, neither Def nor PSD are dual-atomistic.

Consider next the set M_{k} of the meet-irreducible elements of TSD_{k} that are neither the top element SG nor dual-atoms. M_{k} has an element for each sharing group S ∈ SG such that # S > k and each tuple T ⊂ S with # T = k. Such an element is obtained from SG by removing all the sharing groups U such that T ⊆ U ⊆ S. Formally, for 1 ≤ k ≤ n,

M_{k} =^{def} { SG \ { U ∈ SG | T ⊆ U ⊆ S } | T, S ∈ SG, T ⊂ S, # T = k }.

Note that, as there are \binom{n}{k} possible choices for T and 2^{n−k} − 1 possible choices for S, we have # M_{k} = \binom{n}{k}(2^{n−k} − 1) and # MI(TSD_{k}) = ∑_{j=0}^{k−1} \binom{n}{j} + \binom{n}{k}2^{n−k}.

We now show that we have identified precisely all the meet-irreducible elements of TSD_{k}.

Theorem 5 If k ∈ ℕ with 1 ≤ k ≤ n, then

MI(TSD_{k}) = {SG} ∪ dAtoms(TSD_{k}) ∪ M_{k}.

The proof of this theorem is included at the end of this section. Here, we illustrate the result for the case when n = 3.

Example 4 Consider again Example 3. First, consider the domain Def . The meet-irreducible elements which are not dual-atoms, besides SG, are the following (see Figure 2):

q_{1} = { y, z, xz, yz, xyz} ⊂ s_{1},
q_{2} = { y, z, xy, yz, xyz} ⊂ s_{1}, r_{1} = { y, z, yz} ⊂ q_{1} ∩ q_{2},
q_{3} = {x, z, xz, yz, xyz} ⊂ s_{2},
q_{4} = {x, z, xy, xz, xyz} ⊂ s_{2},  r_{2} = {x, z, xz } ⊂ q_{3} ∩ q_{4},
q_{5} = {x, y, xy, yz, xyz} ⊂ s_{3},
q_{6} = {x, y, xy, xz, xyz} ⊂ s_{3},  r_{3} = {x, y, xy  } ⊂ q_{5} ∩ q_{6}.

Next, consider the domain PSD. The only meet-irreducible elements that are not dual-atoms, beside SG, are the following (see Figure 3):

m_{1} = {x, y, z, xz, yz  } ⊂ s_{4}
m_{2} = {x, y, z, xy, yz  } ⊂ s_{5}
m_{3} = {x, y, z, xy, xz  } ⊂ s_{6}.

Each of these lack a pair and none contains the sharing group xyz.

Looking at Examples 2 and 4, it can be seen that all the dual-atoms of the domains Con and PS are meet-irreducible elements of the domains Def and PSD, respectively. Indeed, the following general result shows that the dual-atoms of the domain TS_{k} are meet-irreducible elements for the domain TSD_{k}.

Corollary 2 Let k ∈ ℕ with 1 ≤ k ≤ n. Then

dAtoms(TS_{k}) = { sh ∈ MI(TSD_{k}) | VI ∉ sh }.

For the decomposition, we need to identify which meet-irreducible elements of TSD_{k} are in TS_{j}. Using Corollaries 1 and 2 we have the following result.

\begin{matrix}x, y, z \\ xy, xz, yz \\ xyz \end{matrix} ; SG  \begin{matrix}^{\begin{matrix}y, z \\ xy, xz, yz \\ xyz \end{matrix} s_{1}} & \begin{matrix}^{\begin{matrix}y, z \\ xz, yz \\ xyz \end{matrix} q_{1}} & ^{\begin{matrix}y, z \\ yz \end{matrix} r_{1}} \\ \begin{matrix}y, z \\ xy, yz \\ xyz \end{matrix} & q_{2} \end{matrix} \\ \begin{matrix}x, z \\ xy, xz, yz \\ xyz \end{matrix} s_{2} & \begin{matrix}^{\begin{matrix}x, z \\ xz, yz \\ xyz \end{matrix} q_{3}} & ^{\begin{matrix}x, z \\ xz \end{matrix}  r_{2}} \\ \begin{matrix}x, z \\ xy, xz \\ xyz \end{matrix} & q_{4} \end{matrix} \\ _{\begin{matrix}x, y \\ xy, xz, yz \\ xyz \end{matrix} s_{3}} & \begin{matrix}_{\begin{matrix}x, y \\ xy, yz \\ xyz \end{matrix} q_{5}} & _{\begin{matrix}x, y \\ xy \end{matrix}  r_{3}} \\ \begin{matrix}x, y \\ xy, xz \\ xyz \end{matrix} & q_{6} \end{matrix} \end{matrix}

Fig. 2. The meet-irreducible elements of Def for n = 3, with dual-atoms emphasized.

Corollary 3 If j, k ∈ ℕ with 1 ≤ j < k ≤ n, then MI(TSD_{k}) ∩ TS_{j} = {SG}.

By combining Proposition 1 with Theorem 5 we can identify the meet-irreducible elements of TSD_{k} that are in TSD_{j}, where j < k.

Corollary 4 If j, k ∈ ℕ with 1 ≤ j < k ≤ n, then

MI(TSD_{k}) ∩ TSD_{j} = dAtoms(TSD_{j}).

4.1 Proof of Theorem 5

Proof of Theorem 5. We prove the two inclusions separately.

1. MI(TSD_{k}) ⊇ {SG} ∪ dAtoms(TSD_{k}) ∪ M_{k}. Let m be in the right-hand side. If m ∈ {SG} ∪ dAtoms(TSD_{k}) there is nothing to prove. Therefore we assume m ∈ M_{k}. We need to prove that if

\begin{matrix}x, y, z \\ xy, xz, yz \\ xyz \end{matrix} ; SG  ^{\begin{matrix}y, z \\ xy, xz, yz \\ xyz \end{matrix} s_{1}}^{\begin{matrix}x, z \\ xy, xz, yz \\ xyz \end{matrix} s_{2}}^{\begin{matrix}x, y \\ xy, xz, yz \\ xyz \end{matrix} s_{3}}_{_{\begin{matrix}x, y, z \\ xz, yz \\ xyz \end{matrix} s_{4}}  _{\begin{matrix}x, y, z \\ xz, yz \end{matrix} m_{1}}}_{_{\begin{matrix}x, y, z \\ xy, yz \\ xyz \end{matrix} s_{5}}  _{\begin{matrix}x, y, z \\ xy, yz \end{matrix} m_{2}}}_{_{\begin{matrix}x, y, z \\ xy, xz \\ xyz \end{matrix}  s_{6}}  _{\begin{matrix}x, y, z \\ xy, xz \end{matrix}  m_{3}}}

Fig. 3. The meet-irreducible elements of PSD for n = 3, with dual-atoms emphasized.

sh_{1}, sh_{2} ∈ TSD_{k} and

m = sh_{1} ∧ sh_{2} =^{def} sh_{1} ∩ sh_{2}

then m = sh_{1} or m = sh_{2}. Obviously, we have m ⊆ sh_{1} and m ⊆ sh_{2}. Moreover, by definition of M_{k}, there exist T, S ∈ SG where # T = k and T ⊂ S such that

m = SG \ { U ∈ SG | T ⊆ U ⊆ S }.

Since S ∉ m, we have S ∉ sh_{1} or S ∉ sh_{2}. Let us consider the first case (the other is symmetric). Then, applying the definition of TSD_{k}, there is a T′ ⊂ S with # T′ < k such that

⋃{ U′ ∈ sh_{1} | T′ ⊆ U′ ⊆ S } ≠ S.

Since # T′ < # T, there exists x such that x ∈ T \ T′. Thus T′ ⊂ S \ {x} and S \{x} ∈ m. Hence, as m ⊆ sh_{1}, we have S \{x} ∈ sh_{1}. Consider an arbitrary U ∈ SG where T ⊆ U ⊆ S. Then x ∈ U. Thus, since S = (S \ {x}) ∪ U and S ∉ sh_{1}, U ∉ sh_{1}. Thus, as this is true for all such U, sh_{1} ⊆ m.

2. MI(TSD_{k}) ⊆ {SG} ∪ dAtoms(TSD_{k}) ∪ M_{k}. Let sh ∈ TSD_{k}. We need to show that sh is the meet of elements in the righthand side. If sh = SG then there is nothing to prove. Suppose sh ≠ SG. For each S ∈ SG such that S ∉ sh, we will show there is an element m_{S} in the right-hand side such that S ∉ m_{S} and sh ⊆ m_{S}. Then sh = ⋂{ m_{S} | S ∉ sh }. There are two cases. 2a. # S ≤ k; Let m_{S} = SG \ {S}. Then m_{S} ∈ dAtoms(TSD_{k}) and sh ⊆ m_{S}. 2b. # S > k; in this case, applying the definition of TSD_{k}, there must exist a

set T′ ⊂ S with # T′ < k such that

⋃{ U′ ∈ sh | T′ ⊂ U′ ⊆ S } ⊂ S.

However, since T′ ⊂ S, we have S = ⋃{ T′ ∪ {x} | x ∈ S \ T′ }. Thus, for some x ∈ S \ T′, if U is such that T′ ∪ {x} ⊆ U ⊆ S then U ∉ sh. Choose T ∈ SG so that T′ ∪ {x} ⊆ T and # T = k and let m_{S} = SG \ { U ∈ SG |

T ⊆ U ⊆ S }. Then m_{S} ∈ M_{k}, S ∉ m_{S}, and sh ⊆ m_{S}.

5 The Decomposition of the Domains

5.1 Removing the Tuple-Sharing Domains

We first consider the decomposition of TSD_{k} with respect to TS_{j}. It follows from Theorem 1 and Corollaries 1 and 3 that, for 1 ≤ j < k ≤ n, we have

TSD_{k} ∼ TS_{j} = Moore(MI(TSD_{k}) \ ρ{TS \atop j}(TSD_{k}))
= Moore(MI(TSD_{k}) \ TS_{j})
= TSD_{k}.  (3)

Since SH = TSD_{n}, we have, using Eq. (3) and setting k = n, that, if j < n,

SH ∼ TS_{j} = SH .  (4)

Thus, in general, TS_{j} is too abstract to be removed from SH by means of complementation. (Note that here it is required j < n, because we have SH ∼ TS_{n} ≠ SH .) In particular, letting j = 1, 2 (assuming n > 2) in Eq. (4), we have

SH ∼ PS = SH ∼ Con = SH ,  (5)

showing that Con and PS are too abstract to be removed from SH by means of complementation. Also, by Eq. (3), letting j = 1 and k = 2 it follows that the complement of Con in PSD is PSD.

Now consider decomposing TSD_{k} using TS_{k}. It follows from Theorem 1, Proposition 2 and Corollary 2 that, for 1 ≤ k ≤ n, we have

TSD_{k} ∼ TS_{k} = Moore(MI(TSD_{k}) \ ρ_{_{TS}_{k}}(TSD_{k}))
= Moore(MI(TSD_{k}) \ TS_{k})
= { sh ∈ TSD_{k} | VI ∈ sh }.  (6)

Thus we have

TSD_{k} ∼ (TSD_{k} ∼ TS_{k}) = TS_{k}.  (7)

We have therefore extracted all the domain TS_{k} from TSD_{k}. So by letting k = 1, 2 in Eq. (6), we have found the complements of Con in Def and PS in PSD:

Def ∼ Con = { sh ∈ Def | VI ∈ sh },
PSD ∼ PS = { sh ∈ PSD | VI ∈ sh }.

Thus if we denote the domains induced by these complements as Def^{⊕} and PSD^{⊕}, respectively, we have the following result.

Theorem 6

Def ∼ Con = Def^{⊕},  Def ∼ Def^{⊕} = Con,
PSD ∼ PS = PSD^{⊕},  PSD ∼ PSD^{⊕} = PS.

Moreover, Con and Def^{⊕} form a minimal decomposition for Def and, similarly, PS and PSD^{⊕} form a minimal decomposition for PSD.

5.2 Removing the Dependency Domains

First we note that, by Theorem 5, Proposition 1, and Corollary 4, the complement of TSD_{j} in TSD_{k}, where 1 ≤ j < k ≤ n, is given as follows:

TSD_{k} ∼ TSD_{j} = Moore(MI(TSD_{k}) \ ρ_{_{TSD}_{j}}(TSD_{k}))
= Moore(MI(TSD_{k}) \ TSD_{j})
= { sh ∈ TSD_{k} | ∀S ∈ SG : # S ≤ j ⟹ S ∈ sh }.  (8)

It therefore follows from Eq. (8) and setting k = n that the complement of ρ_{_{TSD}_{j}} in SH for j < n is:

SH ∼ TSD_{j} = { sh ∈ SH | ∀S ∈ SG : # S ≤ j ⟹ S ∈ sh }  (9)

=^{def} SH _{j}^{+}.

In particular, in Eq. (9) when j = 1, we have the following result for Def , also proved in (Filé and Ranzato 1996, Lemma 5.4):

SH ∼ Def = { sh ∈ SH | ∀x ∈ VI : {x} ∈ sh }
=^{def} SH +_{Def} .

Also, in Eq. (9) when j = 2, we have the following result for PSD:

SH ∼ PSD = { sh ∈ SH | ∀S ∈ SG : # S ≤ 2 ⟹ S ∈ sh }
=^{def} SH +_{PSD}.

Def^{−}  _{TS_{2}} = PS  PSD^{‡}_{PSD_{+}} TSD_{2} = PSD

Fig. 4. A non-trivial decomposition of PSD.

We next construct the complement of PSD with respect to Def . By Eq. (8),

PSD ∼ Def = { sh ∈ PSD | ∀x ∈ VI : {x} ∈ sh }

=^{def} PSD^{+}.

Then the complement factor Def^{−} =^{def} PSD ∼ PSD^{+} is exactly the same thing as SH ∼ SH +_{Def} so that PSD and SH behave similarly for Def .

5.3 Completing the Decomposition

Just as for SH , the complement of SH +_{Def} using PS (or, more generally, TS_{j} where 1 < j < n) is SH +_{Def} . By Corollary 2 and Theorem 1, as PS is dual-atomistic, the complement of PS in PSD^{+} is given as follows.

Theorem 7

PSD^{‡} =^{def} PSD^{+} ∼ PS
= { sh ∈ PSD | VI ∈ sh, ∀x ∈ VI : {x} ∈ sh },
PSD^{+} ∼ PSD^{‡} = PS.

So, we have extracted all the domain PS from PSD^{+} and we have the following result (see Figure 4).

Corollary 5 Def^{−}, PS, and PSD^{‡} form a minimal decomposition for PSD.

6 Discussion

By studying the sharing domain SH in a more general framework, we have been able to show that the domain PSD has a natural place in a scheme of domains based on SH . Since the well-known domain Def for groundness analysis is an instance of this scheme, we have been able to highlight the close relationship between Def and PSD and the many properties they share. In particular, it was somehow unexpected that these domains could both be obtained as instances of a single parametric construction. As another contribution, we have generalized and strengthened the results in (Cortesi et al. 1994, Cortesi et al. 1998) and (Bagnara et al. 1997, Bagnara et al. 2001) stating that

• Def is the quotient of SH with respect to the groundness domain G ≡ Con; and

• PSD is the quotient of SH with respect to the reduced product Con ⊓ PS of groundness and pair-sharing.

In the view of recent results on abstract domain completeness (Giacobazzi and Ranzato 1997), these points can be restated by saying that Def and PSD are the least fully-complete extensions (lfce’s) of Con and Con ⊓ PS with respect to SH , respectively.

From a theoretical point of view, the quotient of an abstract domain with respect to a property of interest and the least fully-complete extension of this same property with respect to the given abstract domain are not equivalent. While the lfce is defined for any semantics given by means of continuous operators over complete lattices, it is known (Cortesi et al. 1994, Cortesi et al. 1998) that the quotient may not exist. However, it is also known (Giacobazzi, Ranzato and Scozzari 1998b) that when the quotient exists it is exactly the same as the lfce, so that the latter has also been called generalized quotient. In particular, for all the domains considered in this paper, these two approaches to the completeness problem in abstract interpretation are equivalent.

In (Bagnara et al. 1997, Bagnara et al. 2001), we wrote that PSD ∼ PS ≠ PSD. This paper now clarifies that statement. We have provided a minimal decomposition for PSD whose components include Def^{−} and PS. Moreover, we have shown that Def and PSD are not dual-atomistic and we have completely specified their meetirreducible elements. Our starting point was the work of Filé and Ranzato. In (Filé and Ranzato 1996), they noted, as we have, that SH +_{Def} ∼ PS = SH +_{Def} so that nothing of the domain PS could be extracted from SH +_{Def} . They observed that ρ_{PS} maps all dual-atoms that contain the sharing group VI to the top element SG and thus lose all pair-sharing information. To avoid this, they replaced the classical pair-sharing domain PS with the domain PS′ where, for all sh ∈ SH +_{Def} ,

ρ_{PS}′(sh) = ρ_{PS}(sh) \ ({VI } \ sh),

and noted that SH +_{Def} ∼ PS′ = { sh ∈ SH +_{Def} | VI ∈ sh }. To understand the nature of this new domain PS′, we first observe that,

PS′ = PS ⊓ TS_{n}.

This is because TS_{n} = MI(TS_{n}) = {SG \ {VI }, SG}. In addition,

SH +_{Def} ∼ TS_{n} = { sh ∈ SH +_{Def} | VI ∈ sh },

which is precisely the same as SH +_{Def} ∼ PS′. Thus, since SH +_{Def} ∼ PS = SH +_{Def} , it is not surprising that it is precisely the added component TS_{n} that is removed when we compute the complement for SH +_{Def} with respect to PS′.

We would like to point out that, in our opinion, the problems outlined above are not the consequence of the particular domains considered. Rather, they are mainly related to the methodology for decomposing a domain. As shown here, complementation alone is not sufficient to obtain truly minimal decompositions of domains. The reason being that complementation only depends on the domain’s data (that is, the domain elements and the partial order relation modeling their intrinsic precision), while it is completely independent from the domain operators that manipulate that data. In particular, if the concrete domain contains elements that are redundant with respect to its operators (because the observable behavior of these elements is exactly the same in all possible program contexts) then any factorization of the domain obtained by complementation will encode this redundancy. However, the theoretical solution to this problem is well-known (Cortesi et al. 1994, Cortesi et al. 1998, Giacobazzi and Ranzato 1997, Giacobazzi et al. 1998b) and it is straightforward to improve the methodology so as to obtain truly minimal decompositions: first remove all redundancies from the domain (this can be done by computing the quotient of the domain with respect to the observable behavior) and only then decompose it by complementation. This is precisely what is done here.

We conclude our discussion about complementation with a few remarks. It is our opinion that, from a theoretical point of view, complementation is an excellent concept to work with: by allowing the splitting of complex domains into simpler components, avoiding redundancies between them, it really enhances our understanding of the domains themselves.

However, as things stand at present, complementation has never been exploited from a practical point of view. This may be because it is easier to implement a single complex domain than to implement several simpler domains and integrate them together. Note that complementation requires the implementation of a full integration between components (i.e., the reduced product together with its corresponding best approximations of the concrete semantic operators), otherwise precision would be lost and the theoretical results would not apply.

Moreover, complementation appears to have little relevance when trying to design or evaluate better implementations of a known abstract domain. In particular, this reasoning applies to the use of complementation as a tool for obtaining space saving representations for domains. As a notable example, the GER representation for Pos (Bagnara and Schachte 1999) is a well-known domain decomposition that does enable significant memory and time savings with no precision loss. This is not (and could not be) based on complementation. Observe that the complement of G with respect to Pos is Pos itself. This is because of the isomorphisms Pos ≡ SH (Codish and Søndergaard 1998) and G ≡ Con =^{def} TS_{1} so that, by Eq. (5), Pos ∼ G = Pos. It is not difficult to observe that the same phenomenon happens if one considers the groundness equivalence component E, that is, Pos ∼ E = Pos. Intuitively, each element of the domain E defines a partition of the variable of interest VI into groundness equivalence classes. In fact, it can be shown that two variables x, y ∈ VI are ground-equivalent in the abstract element sh ∈ SH ≡ Pos if and only if rel({x}, sh) = rel({y}, sh). In particular, this implies both {x} ∉ sh and {y} ∉ sh. Thus, it can be easily observed that in all the dual-atoms of Pos no variable is ground-equivalent to another variable (because each dual-atom lacks just a single sharing group).

A new domain for pair-sharing analysis has been defined in (Scozzari 2000) as

Sh^{PSh} = PSD^{+} ⊓ A,

where the A component is a strict abstraction of the well-known groundness domain Pos. It can be seen from the definition that Sh^{PSh} is a close relative of PSD. This new domain is obtained, just as in the case for PSD, by a construction that starts from the set-sharing domain SH ≡ Sh and aims at deriving the pair-sharing information encoded by PS ≡ PSh. However, instead of applying the generalized quotient operator used to define PSD, the domain Sh^{PSh} is obtained by applying a new domain-theoretic operator that is based on the concept of optimal semantics (Giacobazzi, Ranzato and Scozzari 1998a).

When comparing Sh^{PSh} and PSD, the key point to note is that Sh^{PSh} is neither an abstraction nor a concretization of the starting domain SH . On the one hand Sh^{PSh} is strictly more precise for computing pair-sharing, since it contains formulas of Pos that are not in the domain SH . On the other hand SH and PSD are strictly more precise for computing groundness, since Sh^{PSh} does not contain all of Def : in particular, it does not contain any of the elements in Con.

While these differences are correctly stated in (Scozzari 2000), the informal discussion goes further. For instance, it is argued in (Scozzari 2000, Section 6.1) that

“in [(Bagnara et al. 2001)] the domain PSD is compared to its proper abstractions only, which is a rather restrictive hypothesis … ”

This hypothesis is not one that was made in (Bagnara et al. 2001) but is a distinctive feature of the generalized quotient approach itself. Moreover, such an observation is not really appropriate because, when devising the PSD domain, the goal was to simplify the starting domain SH without losing precision on the observable PS. This is the objective of the generalized quotient operator and, in such a context, the “rather restrictive hypothesis” is not restrictive at all.

The choice of the generalized quotient can also provide several advantages that have been fully exploited in (Bagnara et al. 2001). Since an implementation for SH was available, the application of this operator resulted in an executable specification of the simpler domain PSD. By just optimizing this executable specification it was possible to arrive at a much more efficient implementation: exponential time and space savings have been achieved by removing the redundant sharing groups from the computed elements and by replacing the star-union operator with the 2-self-union operator. Moreover, the executable specification inherited all the correctness results readily available for that implementation of SH , so that the only new result that had to be proved was the correctness of the optimizations.

These advantages do not hold for the domain Sh^{PSh}. In fact, the definition of a feasible representation for its elements and, a fortiori, the definition of an executable specification of the corresponding abstract operators seem to be open issues.^{2} Most importantly, the required correctness results cannot be inherited from those of SH . All the above reasons indicate that the generalized quotient was a sensible choice when looking for a domain simpler than SH while preserving precision on PS.

Things are different if the goal is to improve the precision of a given analysis with respect to the observable, as was the case in (Scozzari 2000). In this context the generalized quotient would be the wrong choice, since by definition it cannot help, whereas the operator defined in (Scozzari 2000) could be useful.

7 Conclusion

We have addressed the problem of deriving a non-trivial decomposition for abstract domains tracking groundness and sharing information for logic languages by means of complementation. To this end, we have defined a general schema of domains approximating the set-sharing domain of Jacobs and Langen and we have generalized and strengthened known completeness and minimality results. From a methodological point of view, our investigation has shown that, in order to obtain truly minimal decompositions of abstract interpretation domains, complementation should be applied to a reference domain already enjoying a minimality result with respect to the observable property.

Acknowledgment

We recognize the hard work required to review technical papers such as this one and would like to express our real gratitude to the Journal referees for their critical reading and constructive suggestions for preparing this improved version.

References

Armstrong, T., Marriott, K., Schachte, P. and Søndergaard, H. (1998). Two classes of Boolean functions for dependency analysis, Science of Computer Programming 31(1): 3– 45.

Bagnara, R. and Schachte, P. (1999). Factorizing equivalent variable pairs in ROBDD-based implementations of Pos, in A. M. Haeberer (ed.), Proceedings of the “Seventh International Conference on Algebraic Methodology and Software Technology (AMAST’98)”, Vol. 1548 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, Amazonia, Brazil, pp. 471–485.

Bagnara, R., Hill, P. M. and Zaffanella, E. (1997). Set-sharing is redundant for pairsharing, in P. Van Hentenryck (ed.), Static Analysis: Proceedings of the 4th International Symposium, Vol. 1302 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, Paris, France, pp. 53–67.

Bagnara, R., Hill, P. M. and Zaffanella, E. (2001). Set-sharing is redundant for pair-sharing, Theoretical Computer Science. To appear.

2 In (Scozzari 2000), the only representation given for the elements of Sh^{PSh} is constituted by infinite sets of substitutions.

Decomposing Non-Redundant Sharing 29

Codish, M. and Søndergaard, H. (1998). The Boolean logic of set sharing analysis, in C. Palamidessi, H. Glaser and K. Meinke (eds), Principles of Declarative Programming, Vol. 1490 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, Pisa, Italy, pp. 89–100.

Colmerauer, A. (1982). Prolog and infinite trees, in K. L. Clark and S. Å. Tärnlund (eds), Logic Programming, APIC Studies in Data Processing, Vol. 16, Academic Press, New York, pp. 231–251.

Colmerauer, A. (1984). Equations and inequations on finite and infinite trees, Proceedings of the International Conference on Fifth Generation Computer Systems (FGCS’84), ICOT, Tokyo, Japan, pp. 85–99.

Cortesi, A. and Filé, G. (1999). Sharing is optimal, Journal of Logic Programming

38(3): 371–386. Cortesi, A., Filé, G. and Winsborough, W. (1994). The quotient of an abstract inter-

pretation for comparing static analyses, in M. Alpuente, R. Barbuti and I. Ramos (eds), Proceedings of the “1994 Joint Conference on Declarative Programming (GULP-PRODE’94)”, Peñíscola, Spain, pp. 372–397. An extended version has been published as (Cortesi et al. 1998).

Cortesi, A., Filé, G. and Winsborough, W. (1996). Optimal groundness analysis using

propositional logic, Journal of Logic Programming 27(2): 137–167. Cortesi, A., Filé, G. and Winsborough, W. (1998). The quotient of an abstract interpreta-

tion for comparing static analyses, Theoretical Computer Science 202(1&2): 163–192. Cortesi, A., Filé, G., Giacobazzi, R., Palamidessi, C. and Ranzato, F. (1995). Comple-

mentation in abstract interpretation, in A. Mycroft (ed.), Static Analysis: Proceedings of the 2nd International Symposium, Vol. 983 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, Glasgow, UK, pp. 100–117.

Cortesi, A., Filé, G., Giacobazzi, R., Palamidessi, C. and Ranzato, F. (1997). Complementation in abstract interpretation, ACM Transactions on Programming Languages and Systems 19(1): 7–47.

Cousot, P. and Cousot, R. (1979). Systematic design of program analysis frameworks, Proceedings of the Sixth Annual ACM Symposium on Principles of Programming Languages, pp. 269–282.

Filé, G. and Ranzato, F. (1996). Complementation of abstract domains made easy, in M. Maher (ed.), Logic Programming: Proceedings of the Joint International Conference and Symposium on Logic Programming, MIT Press Series in Logic Programming, The MIT Press, Bonn, Germany, pp. 348–362.

Giacobazzi, R. and Ranzato, F. (1997). Completeness in abstract interpretation: a domain perspective, in M. Johnson (ed.), Proceedings of the 6th International Conference on Algebraic Methodology and Software Technology (AMAST’97), Vol. 1349 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, Sydney, Australia, pp. 231–245.

Giacobazzi, R., Ranzato, F. and Scozzari, F. (1998a). Building complete abstract interpre-

tations in a linear logic-based setting, in Levi (1998), pp. 215–229. Giacobazzi, R., Ranzato, F. and Scozzari, F. (1998b). Complete abstract interpretations

made constructive, in J. Gruska and J. Zlatuska (eds), Proceedings of 23rd International Symposium on Mathematical Foundations of Computer Science (MFCS’98), Vol. 1450 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, pp. 366–377.

Gierz, G., Hofmann, K. H., Keimel, K., Lawson, J. D., Mislove, M. and Scott, D. S. (1980).

A Compendium of Continuous Lattices, Springer-Verlag, Berlin. Hill, P. M., Bagnara, R. and Zaffanella, E. (1998). The correctness of set-sharing, in Levi

(1998), pp. 99–114. Jacobs, D. and Langen, A. (1989). Accurate and efficient approximation of variable aliasing

30 E. Zaffanella, P. M. Hill and R. Bagnara

in logic programs, in E. L. Lusk and R. A. Overbeek (eds), Logic Programming: Proceedings of the North American Conference, MIT Press Series in Logic Programming, The MIT Press, Cleveland, Ohio, USA, pp. 154–165.

Jacobs, D. and Langen, A. (1992). Static analysis of logic programs for independent AND

parallelism, Journal of Logic Programming 13(2&3): 291–314. Jones, N. D. and Søndergaard, H. (1987). A semantics-based framework for the abstract

interpretation of Prolog, in S. Abramsky and C. Hankin (eds), Abstract Interpretation of Declarative Languages, Ellis Horwood Ltd, West Sussex, England, chapter 6, pp. 123– 142.

Langen, A. (1990). Advanced Techniques for Approximating Variable Aliasing in Logic Programs, PhD thesis, Computer Science Department, University of Southern California. Printed as Report TR 91-05.

Levi, G. (ed.) (1998). Static Analysis: Proceedings of the 5th International Symposium, Vol.

1503 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, Pisa, Italy. Scozzari, F. (2000). Abstract domains for sharing analysis by optimal semantics, in J. Pals-

berg (ed.), Static Analysis: 7th International Symposium, SAS 2000, Vol. 1824 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, Santa Barbara, CA, USA, pp. 397– 412.

Scozzari, F. (2001). Logical optimality of groundness analysis, Theoretical Computer Sci-

ence. To appear. Zaffanella, E., Hill, P. M. and Bagnara, R. (1999). Decomposing non-redundant sharing by

complementation, in A. Cortesi and G. Filé (eds), Static Analysis: Proceedings of the 6th International Symposium, Vol. 1694 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, Venice, Italy, pp. 69–84.