Compositional Optimization of Disjunctive Abstract Interpretations

Roberto Giacobazzi^{⋆} Francesco Ranzato^{⋆⋆}

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

                              giaco@di.unipi.it

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

                         franz@hilbert.math.unipd.it

Abstract. We define the inverse operation for disjunctive completion, introducing the notion of least disjunctive basis for an abstract domain D: this is the most abstract domain inducing the same disjunctive completion as D. We show that the least disjunctive basis exists in most cases, and study its properties in relation with reduced product of abstract interpretations. The resulting framework is powerful enough to be applied to arbitrary abstract domains for analysis, providing advanced algebraic methods for domain manipulation and optimization. These notions are applied to abstract domains for analysis of functional and logic programming languages.

1 Introduction

It is widely acknowledged that most program properties need relational abstract domains to be attacked by abstract interpretation ([18, 24]). The Cousot and Cousot functional combination by reduced power ([8]), and Nielson’s tensor product ([25]) were the first systematic methods to induce relational analyses by combining abstract domains. Cousot and Cousot showed in [9] that a relational analysis can be induced by combining reduced product (denoted ⊓) and disjunctive completion (denoted ℧) of abstract domains. If D_{1} and D_{2} are abstract domains, a corresponding domain for relational analysis can always be defined as ℧(D_{1} ⊓ D_{2}). In this construction, reduced product is attribute independent (viz. the information obtainable from the combination of analyses is essentially the same as the one obtainable by performing the analyses separately), while disjunctive completion introduces relational information by exploiting sets of attribute independent abstract properties. Disjunctive completion is therefore fundamental to implement relational analyses.

Disjunctive completion was originally introduced to exploit disjunctive program properties, notably to prove that merge-over-all-paths (MOP) data-flow analysis can be always expressed in fixpoint form ([8]). This notion was also considered in Nielson’s approach to abstract interpretation using domain theory ([24]), and applied in data-flow analysis of functional and logic languages, e.g., to express disjunctive information in Jensen’s strictness logic ([17]), in Cousot and Cousot comportment analysis ([10]), and in analysis of ground-dependencies ([12]).

A natural question is: can we invert a process of “domain refinement”? Namely, can we reconstruct the “least basis” which induces a given domain by composition or completion? Recently, [5] attacked the problem of inverting reduced product, introducing the notion of complementation in abstract interpretation. Complementation provides an important tool for abstract domain decomposition into attribute independent factors. In this paper, we consider the inverse for the remaining fundamental operation of disjunctive completion, denoted Ω. We introduce the notion of least disjunctive basis for an abstract domain, and study its properties in relation with reduced product. The interest in this operation is twofold: (1) theoretically, least disjunctive bases contain the least amount of information which characterizes a given disjunctive property; and (2) practically, least disjunctive bases are minimal (viz. non-redundant), providing useful space saving techniques to implement disjunctive completions and relational analyses. In particular, the disjunctive completion of the least disjunctive basis involves the least number of reduction tests in domain implementation (e.g. by powerset construction), as most redundant information has been removed from the source. This operation can be combined with complementation, in order to characterize optimal (viz. most abstract) decompositions for complex relational abstract domains. The resulting framework is powerful enough to be applied to arbitrary abstract domains for analysis, providing advanced algebraic methods for domain manipulation and optimization.

The main achievements of the paper can be summarized as follows.

• Under weak hypotheses, an abstract domain D can be associated with a unique least disjunctive basis, which is the most abstract domain inducing the same disjunctive completion as D.

• Least disjunctive bases distribute compositionally with respect to the reduced product, and enjoy remarkable algebraic properties.

• We apply the above results to domains for analysis of functional and logic programming languages. In particular, we show that: ∘ The Cousot and Cousot lattice of basic comportments ([10]) is not the least disjunctive basis of the lattice for disjunctive comportment analysis ([10]). ∘ The Marriott and Søndergaard domain Def ([19]) is the least disjunctive basis inducing the domain for disjunctive ground-dependency analysis of logic programs. This shows that Def , which is strictly less expensive than Pos ([6, 19]), always induces the same disjunctive ground-dependency analysis, i.e., Ω(Pos) = Def .

Throughout the paper, we assume familiarity with lattice theory (e.g. see [3, 14]), in particular closure operators (see [20, 28]), and abstract interpretation ([7, 8]).

2 Abstract Interpretation and Closure Operators

The standard Cousot and Cousot theory of abstract interpretation is based on the notion of Galois connection ([7, 8]). In this section, we briefly introduce some notation and recall some well known notions.

If C and D are posets and α : C → D, γ : D → C are monotonic functions such that ∀c ∈ C . c ≤_{C} γ(α(c)) and ∀d ∈ D. α(γ(d)) ≤_{D} d, then we call the quadruple (γ, D, C , α) a Galois connection (G.c.) between C and D. If in addition ∀d ∈ D. α(γ(d)) = d, then (γ, D, C , α) is a Galois insertion (G.i.) of D in C . In the setting of abstract interpretation, C and D 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. D is called an abstraction (or abstract interpretation) of C , and C a concretization of D. Further, D is a proper abstraction of C if γ ∘ α ≠ λx.x. Galois insertions characterize “ideal” abstractions, as any abstract object is the abstraction of a concrete one. In this case, the concretization and abstraction mappings are 1-1 and onto, respectively. Any G.c. can 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.

Let ⟨L, ≤, ∧, ∨, ⊤, ⊥⟩ be a complete lattice. An (upper) closure operator on L is an operator ρ : L → L monotonic, idempotent and extensive (viz. ∀x ∈ L. x ≤ ρ(x)). Each closure operator ρ is uniquely determined by the set of its fixpoints, which is its image ρ(L). A set X ⊆ L is the set of fixpoints of a closure operator iff X is a Moore-family of L, i.e. ⊤ ∈ X and X is meet-closed (viz. for any non-empty Y ⊆ X , ∧Y ∈ X ). For any X ⊆ L, we denote by M(X ) the Moore-closure of X , i.e. the least subset of L containing X which is a Moore-family of L. ρ(L) is a complete lattice with respect to the order of L, but, in general, it is not a complete sublattice of L, since the lub in ρ(L) might be different from that in L. Indeed, ρ(L) is a complete sublattice of L iff ρ is additive, i.e. for all X ⊆ L, ρ(∨X ) = ∨ρ(X ). In the following, we will often denote a closure operator by the set of its fixpoints. We denote by ⟨uco(L), ⊑, ⊓, ⊔, λx.⊤, λx.x⟩ the complete lattice of all upper closure operators on the complete lattice L, with top element λx.⊤ and bottom element λx.x, where for every ρ, η ∈ uco(L), {ρ_{i}}_{i∈I} ⊆ uco(L) and x ∈ L: ρ ⊑ η iff ∀x ∈ L. ρ(x) ≤ η(x), or equivalently ρ ⊑ η iff η(L) ⊆ ρ(L); (⊓_{i∈I} ρ_{i})(x) = ∧_{i∈I} ρ_{i}(x); (⊔_{i∈I} ρ_{i})(x) = x ⇔ ∀i ∈ I . ρ_{i}(x) = x. A lower closure operator φ : L → L is monotonic, idempotent and reductive (viz. ∀x ∈ L. φ(x) ≤ x). The complete lattice of all lower closure operators on the complete lattice L is denoted by lco(L). Its lattice-theoretic properties can all be derived by duality from those above for uco(L).

The lattice of abstract interpretations. A key point in Cousot and Cousot abstract interpretation theory is the equivalence between the Galois insertion and closure operator approach to the design of abstract domains. Actually, an abstract domain is just a “computer representation” of its logical meaning, namely its image in the concrete domain. In fact, using a different but lattice-theoretic isomorphic domain changes nothing in the abstract reasoning. The logical meaning of an abstract domain is exactly captured by the associated closure operator on the concrete domain. More formally, on one hand, if (γ, D, C , α) is a G.i. then the closure associated with D is the operator ρ_{D} = γ ∘ α on C . On the other hand, if ρ is a closure on C and ι : ρ(C ) → D is an isomorphism of complete lattices (with inverse ι^{−1}) then (ι^{−1}, D, C , ι ∘ ρ) is a G.i.. The complete lattice of all abstract interpretations (identified up to isomorphism) of a domain C is therefore isomorphic to uco(C ). By the above equivalence, it is not restrictive to use the closure operator approach to reason about abstract properties up to isomorphic representations of abstract domains. Thus, in the rest of the paper, we will feel free to use most of the times this approach, and whenever we will say that D is an abstraction of C , we will mean that D is isomorphic to ρ_{D}(C ) (denoted by D ≅ ρ_{D}(C )), for some closure ρ_{D} ∈ uco(C ). In this approach, the order relation on uco(C ) corresponds to the order by means of which abstract domains are compared with regard to their precision. More formally, if ρ_{i} ∈ uco(C ) and D_{i} ≅ ρ_{i}(C ) (i = 1, 2), D_{1} is more precise than D_{2} iff ρ_{1} ⊑ ρ_{2} (i.e. ρ_{2}(C ) ⊆ ρ_{1}(C )). Therefore, to compare domains with regard to their precision, we will only speak about abstractions between them, and use ⊑ to relate both closure operators and domains (⊏ denotes strict ordering). Further, we will often use the equality symbol = instead of ≅. In view of this equivalence, the lub and glb on uco(C ) get a clear meaning. Suppose {ρ_{i}}_{i∈I} ⊆ uco(C ) and D_{i} ≅ ρ_{i}(C ) for each i ∈ I . Any domain D isomorphic to the lub (⊔_{i∈I} ρ_{i})(C ) is the most concrete among the domains which are abstractions of all the D_{i}’s. The interpretation of the glb operation on uco(C ) is twofold. Firstly, any domain D isomorphic to the glb (⊓_{i∈I} ρ_{i})(C ) is (isomorphic to) the well known reduced product ([8]) of all the domains D_{i}. Also, the glb D, and hence the reduced product, is the most abstract among the domains (abstracting C ) which are more concrete than every D_{i}. Thus, we will denote the reduced product of abstract domains by the glb symbol ⊓.

Complementation in abstract interpretation. Complementation ([5]) corresponds to the inverse operation for reduced product, namely an operation which starting from any two domains C ⊑ D, gives as result the (unique) most abstract domain C ∼D, whose reduced product with D is exactly C (i.e., (C ∼D) ⊓ D = C ). If C is a meet-continuous complete lattice (i.e., for any chain Y ⊆ C and x ∈ C , x ∧ (∨Y ) = ∨_{y∈Y} (x ∧ y)) and C ⊑ D then C ∼D always exists, and can be defined as C ∼D = ⊔{ρ ∈ uco(C ) | (ρ_{D} ⊓ ρ)(C ) = C } (cf. [5]).

3 Disjunctive Completions by Closures

In this section, we formulate by closure operators the standard Cousot and Cousot definition of disjunctive completion of an abstract domain ([8]), and introduce some basic properties. Let C be any complete lattice, and consider its lattice of abstract interpretations uco(C ).

Definition 3.1 The disjunctive completion operator is the map ℧_{C} : uco(C ) → uco(C ) defined as: ℧_{C} (ρ) = ⊔{η ∈ uco(C ) | η ⊑ ρ, η is additive}, for any ρ ∈ uco(C ). □

Lemma 3.2 For any ρ ∈ uco(C ), ℧_{C} (ρ) is additive.

℧_{C} (ρ) is called the disjunctive completion of ρ ∈ uco(C ) in C . In other terms, for a domain D abstracting C , ℧_{C} (D) is the most abstract domain which is a concretization of D and (isomorphic to) a complete sublattice of C (or, equivalently, join-closed). It is worth noting that for any domain D its disjunctive completion ℧_{C} (D) contains a denotation ⊥_{C} for the bottom element of C , since ∅ ⊆ D and ⊥_{C} = ∨_{C} ∅. It is evident that the above definition corresponds exactly to the standard definition of disjunctive completion given by means of Galois connections (cf. [8, 9, 10, 12]). This notion is also comprehensive for other forms of disjunctive completions: e.g., disjunctive and order-ideal completions (e.g. [17]) are equivalent (see [10]). Moreover, whenever D satisfies the ascending chain condition, disjunctive, Scott-closed ideal and anti-chain completions are equivalent (see [10]).

Proposition 3.3 ℧_{C} ∈ lco(uco(C )).

The meaning of the above proposition is clear: the disjunctive completion is a domain refinement (viz., a monotonic and reductive mapping in uco(C )). Moreover, no refinement can be obtained by disjunctive completion of a domain which is already disjunctively completed (viz., ℧_{C} is idempotent). Being a lower closure operator, ℧_{C} is uniquely determined by its set of fixpoints, namely its image ℧_{C} (uco(C )) = {ρ ∈ uco(C ) | ρ is additive}, which is precisely the set of all disjunctive abstract interpretations of C . The following result is an immediate consequence of Proposition 3.3, and characterizes the compositionality of the disjunctive completion with respect to the reduced product of abstract domains.

Proposition 3.4 If C ⊑ D, E then ℧_{C} (D ⊓ E) = ℧_{C} (℧_{C} (D) ⊓ ℧_{C} (E)).

It is worth noting that the disjunctive completion of an abstract domain depends on the fixed concrete domain. If C ⊑ D ⊑ E, then ℧_{C} (E) is in general different from ℧_{D}(E). Indeed, they coincide when D is disjunctive.

Proposition 3.5 If C ⊑ D ⊑ E then ℧_{C} (E) ⊑ ℧_{D}(E), and if, in addition, ℧_{C} (D) = D then ℧_{C} (E) = ℧_{D}(E).

Next example shows this phenomenon.^{1}

Example 3.6 Consider the usual lattices D and E for sign analysis of an integer variable ([8]), depicted below. The concrete domain is ⟨℘(ZZ), ⊆⟩, and concretization and abstraction maps are the most natural. Evidently, E is an abstraction of D.

[figure: •; •; •; •; •; •; •; −; −0; ⊥; 0; ⊤; 0+; +; D; •; •; •; •; ⊤; −; +; ⊥; E = ℧_{D}(E); •; •; •; •; •; ⊤; {−, +}; −; +; ⊥; ℧_{C} (E)]

Clearly, D is not a disjunctive abstract interpretation of the concrete domain C = ℘(ZZ), since γ(−) ∪ γ(+) ⊂ γ(− ∨ +) = γ(⊤). In this case, ℧_{C} (E) does not coincide with ℧_{D}(E). In fact, the disjunctive completion of E with respect to D, viz. ℧_{D}(E), is E itself, while the disjunctive completion with respect to C , viz. ℧_{C} (E), is the lattice depicted above. □

4 Optimizing Disjunctive Completions

Our goal is to answer to the following question:

Given a domain D abstracting C , under what hypotheses does exist the least abstraction of C having the same disjunctive completion of D in C ?

1 Throughout the paper, if X and Y are sets then we write X ⊂ Y to denote that X is a proper subset of Y , and X \ Y to denote their set-difference.

In the following, we positively answer the question above. Firstly, we need two preliminary definitions formally stating by closure operators this question.

Definition 4.1 Given a complete lattice C , ρ ∈ uco(C ) is disjunctively optimizable if ℧_{C} (⊔{η ∈ uco(C ) | ℧_{C} (η) = ℧_{C} (ρ)}) = ℧_{C} (ρ). □

In the following, for any ρ ∈ uco(C ), the closure ⊔{η ∈ uco(C ) | ℧_{C} (η) = ℧_{C} (ρ)} is denoted by Ω_{C} (ρ).

Definition 4.2 Assume that C ⊑ D, and the corresponding ρ_{D} ∈ uco(C ) is disjunctively optimizable. The least disjunctive basis for D in C is the complete lattice Ω_{C} (D) given by the set of fixpoints of Ω_{C} (ρ_{D}) in C . □

Ω_{C} (D) is therefore the most abstract domain such that ℧_{C} (Ω_{C} (D)) = ℧_{C} (D). Being Ω_{C} (D) = (Ω_{C} (ρ_{D}))(C ), the above definition implies that Ω_{C} (D) is a subset of C . Obviously, any other lattice isomorphic to Ω_{C} (D) can be considered in all respects as the least disjunctive basis.

The following proposition provides an alternative characterization for the operator Ω_{C} .

Proposition 4.3 ρ ∈ uco(C ) is disjunctively optimizable iff there exists a unique element Ω_{C} (ρ) ∈ uco(C ) such that:

(i) ℧_{C} (Ω_{C} (ρ)) = ℧_{C} (ρ); (ii) ∀η ∈ uco(C ). ℧_{C} (η) = ℧_{C} (ρ) ⇒ η ⊑ Ω_{C} (ρ).

Below, we state two theorems, one orthogonal to the other, for the existence of the least disjunctive basis. The first guarantees the existence of the least disjunctive basis for finite abstract domains.

Theorem 4.4 If D ∈ uco(C ) is finite then it is disjunctively optimizable.

It is important to note that most of the abstract domains used as basis of a static analysis are finite, and hence, by the above result, disjunctively optimizable. For functional languages, these comprise the abstract domains for standard strictness analysis ([4, 21, 22]), and for its generalization of comportment analysis ([10]). For logic languages, ground-dependency analysis, supposedly the most known analysis, involves traditionally finite abstract domains ([1, 6, 16, 19]); in Section 7, we will determine the least disjunctive basis for one of these abstract domains.

Next theorem provides a condition on the concrete domain in order that every of its abstractions is disjunctively optimizable.

Theorem 4.5 If C is dual-algebraic^{2} then each D ∈ uco(C ) is disjunctively optimizable.

2 If C is a complete lattice then the subset of the dual-compacts of C is defined as dK (C ) = {x ∈ C | ∀S ⊆ C . (x ≥ ∧S) ⇒ (∃T ⊆ S. T finite & x ≥ ∧T )}. C is dual-algebraic if for any x ∈ C , x = ∧{z ∈ dK (C ) | z ≥ x}.

The class of (dual-)algebraic lattices is well known from denotational semantics. It is worth noting that this class is wide enough for practical purposes: in fact, any well-founded domain, i.e. any lattice satisfying the descending chain condition, is dual-algebraic, as well as any collecting domain, i.e. any powerset ℘(X ), for some set X , ordered with the subset or supset relation. The latter case includes the standard concrete domains for collecting semantics in functional and logic programming (e.g. [2, 23]). Complete lattices which are join-continuous and that satisfy the ascending chain condition are also dual-algebraic.

Dual-algebraicity plays a fundamental rôle in Theorem 4.5. In general, if C is not dual-algebraic, then it might exist ρ ∈ uco(C ) non-disjunctively optimizable.

Example 4.6 Let L be the complete lattice {⟨m, n⟩ | m ∈ {0, 1}, n ∈ IN} ∪ {⊥}, where the ordering relation is determined by the Hasse diagram below.

[figure: ⊥; ⟨1, 3⟩; ⟨0, 1⟩; ⟨1, 2⟩; ⟨0, 0⟩; ⟨1, 1⟩; ⟨1, 0⟩; L; ⋮; ⋮; •; •; •; •; •; •; •; ⊥; ⟨1, 3⟩; ⟨0, 1⟩; ⟨1, 2⟩; ⟨0, 0⟩; ⟨1, 1⟩; ⟨1, 0⟩; ⟨0, ω⟩; L_{ω}; ⋮; ⋮; •; •; •; •; •; •; •; •]

L is not dual-algebraic: in fact, it is simple to verify that dK (L) = {⟨1, 0⟩} ∪ {⟨0, n⟩}_{n∈IN}, and if n > 0 then ⟨1, n⟩ < ∧{z ∈ dK (L) | z ≥ ⟨1, n⟩}. For any k ∈ IN, consider the closure ρ_{k} = {⟨1, n⟩}_{n∈IN} ∪ {⟨0, n⟩}_{k≤n} ∪ {⊥}. It is clear that for any k ∈ IN, ℧_{L}(ρ_{k}) = L, and (⊔_{k∈IN}ρ_{k})(L) = {⟨1, n⟩}_{n∈IN} ∪ {⊥} = (℧_{L}(⊔_{k∈IN}ρ_{k}))(L). If, by contradiction, Ω_{L}(L) exists, then ⊔_{k∈IN}ρ_{k} ⊑ Ω_{L}(L). But, since ℧_{L} is monotonic, we should have ℧_{L}(⊔_{k∈IN}ρ_{k}) ⊑ ℧_{L}(Ω_{L}(L)) = L, i.e. we should obtain the contradiction L ⊆ {⟨1, n⟩}_{n∈IN} ∪ {⊥}. If we consider the lattice L_{ω} depicted above, and obtained from L by adding the element ⟨0, ω⟩, it is possible to check that L_{ω} is dual-algebraic (although it does not satisfy the descending chain condition). In this case, Ω_{L_{ω}}(L_{ω}) exists, and it is {⟨1, n⟩}_{n∈IN} ∪ {⊥} ∪ {⟨0, ω⟩}. Indeed, for any n ∈ IN, the lacking element ⟨0, n⟩ is obtained by disjunctive completion of L_{ω} as ⟨0, ω⟩ ∨ ⟨1, n + 2⟩. Evidently, this is the least closure whose disjunctive completion is L_{ω}. □

From now on, whenever we will speak about least disjunctive bases we will suppose that the conditions for their existence hold.

Example 4.7 Consider the domain D of Example 3.6. It is immediate to check that its disjunctive completion ℧_{C} (D) (with respect to C = ℘(ZZ)) is the lattice depicted below.

[figure: ⊥; −; 0; +; −0; 0+; {−, +}; ⊤; ℧_{C} (D); •; •; •; •; •; •; •; •; •; •; •; •; •; ⊤; −; 0; +; ⊥; Ω_{C} (D)]

By Theorem 4.4 or Theorem 4.5, its least disjunctive basis Ω_{C} (D) (in C ) exists. Indeed, it is easy to verify that Ω_{C} (D) is the lattice depicted above, which is a proper abstraction of D. □

It is worth noting that the least disjunctive basis operator depends on the fixed concrete domain of reference (an example will be given at the end of Section 7), unless disjunctive abstract interpretations are considered.

Proposition 4.8 If C ⊑ D ⊑ E and ℧_{C} (D) = D then Ω_{C} (E) = Ω_{D}(E).

Join-irreducible elements^{3} play an important rôle in the computation of the least disjunctive basis. In fact, the least disjunctive basis of an abstract domain D which is disjunctive, is precisely the Moore-closure of the set JI_{D} of the join-irreducible elements of D.

Theorem 4.9 If C ⊑ D and ℧_{C} (D) = D then Ω_{C} (D) = M(JI_{D}).^{4}

Obviously, since ℧_{C} (C ) = C , the least disjunctive basis of every concrete domain is just the Moore-closure of its join-irreducible elements. Theorem 4.9 has another interesting consequence.

Corollary 4.10 If C ⊑ D then Ω_{C} (D)(= Ω_{C} (℧_{C} (D)))= M(JI_{℧C (D)} ).

In other terms, the least disjunctive basis of an abstract domain D can always be computed by means of the method of the join-irreducible elements, computing the Moore-closure of the join-irreducible elements of the disjunctive completion of D. Obviously, this is always theoretically possible, but hardly feasible, because of the (usually exponential) size of ℧_{C} (D). Indeed, when ℧_{C} (D) is finite and isomorphic to a powerset, |Ω_{C} (D)| = log(|℧_{C} (D)|) + k, where k is a constant.

5 Algebraic Properties and Compositionality

In this section, we study the algebraic properties of the least disjunctive basis with respect to disjunctive completion and reduced product of abstract interpretations.

Proposition 5.1 Assume that C ⊑ D, E, ⊤ is the most abstract interpretation of C , and Ω_{C} (D), Ω_{C} (E) exist. Then,

(a) D ⊑ Ω_{C} (D);

(b) Ω_{C} (Ω_{C} (D)) = Ω_{C} (D);

(c) Ω_{C} (⊤) = ⊤;

(d) Ω_{C} (℧_{C} (D)) = Ω_{C} (D);

3 An element x of a complete lattice L is (completely) join-irreducible if ∀Y ⊆ L. (x =

∨Y ⇒ x ∈ Y ). JI_{L} denotes the set of join-irreducible elements of L. Note that ⊥_{L} ∉ JI_{L}. 4 Note that this result does not hold if the least disjunctive basis Ω_{C} (D) does not exist.

For instance, in Example 4.6, JI_{L} = {⟨1, n⟩}_{n∈IN\{0}}, but, M(JI_{L}) = {⟨1, n⟩}_{n∈IN} ∪ {⊥} is not the least disjunctive basis for L, as shown in that example.

(e) Ω_{C} (D) = Ω_{C} (E) ⇒ Ω_{C} (D ⊔ E) = Ω_{C} (D);

(f) ℧_{C} (D) = ℧_{C} (E) ⇔ Ω_{C} (D) = Ω_{C} (E);

(g) ℧_{C} (D ⊓ E) = ℧_{C} (Ω_{C} (D) ⊓ Ω_{C} (E)).

Combining points (f) and (g) above, we get an interesting form of compositionality of the least disjunctive basis operator with respect to the reduced product of abstract domains.

Corollary 5.2 Ω_{C} (D ⊓ E) = Ω_{C} (Ω_{C} (D) ⊓ Ω_{C} (E)).

The following is a simple example exploiting the above result on compositionality.

Example 5.3 Suppose that the domain D of Example 3.6 has been incrementally designed by reduced product of the domains E and F given below (the concrete domain is C = ℘(ZZ)).

[figure: • • • + 0+⊤ E; •; •; •; •; •; ⊤; −0; −; 0; ⊥; F; •; •; •; •; •; •; −; ⊥; 0; ⊤; 0+; +; Ω_{C} (E) ⊓ Ω_{C} (F )]

By Corollary 5.2, we can compositionally compute the least disjunctive basis Ω_{C} (D) (in Example 4.7) of D from the least disjunctive bases Ω_{C} (E) and Ω_{C} (F ) of its factors. Indeed, the domain Ω_{C} (E) ⊓ Ω_{C} (F ), which is depicted above, is a proper abstraction of the starting domain D = E ⊓ F , and therefore the task of computing the least disjunctive basis of Ω_{C} (E) ⊓ Ω_{C} (F ) is more simple. □

Domain decomposition by complementation ([5]) and least disjunctive bases can be combined to exploit this form of compositionality of the least disjunctive basis operator. Indeed, complementation provides binary decompositions of abstract domains, and therefore least disjunctive bases can be computed compositionally.

It is important to remark that the least disjunctive basis operator is neither monotonic nor anti-monotonic (hence it is not a closure), as shown below.

Example 5.4 Consider the abstract domains D of Example 3.6 and E of Example 5.3, where D ⊑ E (the concrete domain is C = ℘(ZZ)). The least disjunctive basis Ω_{C} (D) is in Example 4.7, while it is simple to check that Ω_{C} (E) = E. This proves that the least disjunctive basis operator is neither monotonic nor anti-monotonic, since Ω_{C} (D) and Ω_{C} (E) are incomparable abstractions of C . □

6 Functional Programming: Optimizing Comportment Analysis

In this section, we apply the theory of the least disjunctive basis to the comportment analysis, designed by Cousot and Cousot in [10] to generalize Mycroft’s strictness

truth  γ^{β→β}(top) = D^{β→β}
strictness γ^{β→β}(str) = {f | f (⊥) = ⊥}
totality  γ^{β→β}(tot) = {f | ∀x ∈ D^{β} \ {⊥}. f (x) ≠ ⊥}
identity  γ^{β→β}(ide) = {f | ∀x ∈ D^{β}. f (x) = ⊥ ⇔ x = ⊥}
divergence γ^{β→β}(div) = {f | ∀x ∈ D^{β}. f (x) = ⊥}
convergence γ^{β→β}(con) = {f | ∀x ∈ D^{β}. f (x) ≠ ⊥}
falsity  γ^{β→β}(∅) = ∅

Table 1: Basic comportment analysis B_{C}.

and termination analysis ([21, 22]), Wadler and Hughes’ projection analysis ([27]), and Hunt’s PER analysis ([15]). The comportment analysis applies to higher order monomorphically typed lazy functional programming languages.

To illustrate Cousot and Cousot’s comportment analysis, we consider abstract interpretation of a simply typed lambda calculus with basic types β. Denote D^{τ} the domain of values of a type τ, and by ⊥ its bottom element. For simplicity, we will consider abstractions of function basic types β → β (i.e., elements in D^{β→β} = D^{β} → D^{β}, the lattice of monotonic functions from D^{β} to D^{β} ordered pointwise). The abstract domain B_{C} below represents the lattice of basic comportment analysis, ordered with respect to the approximation order, for function basic types β → β.

The meaning of basic comportments in B_{C} is given in Table 1, in terms of a concretization function γ^{β→β} mapping basic comportments into ⟨℘(D^{β→β}), ⊆⟩, which is the concrete domain of the collecting semantics.

As proved by Cousot and Cousot in [10], more precise comportment properties for higher-order functional languages can be characterized by disjunctive completion of the lattice B_{C} of basic comportment analysis. In this case, the meaning of sets Ψ of basic comportments is given by a concretization γ^{℘} such that γ^{℘}(Ψ) = ∪{γ^{β→β}(ψ) | ψ ∈ Ψ}. The lattice C below, ordered by the approximation order, corresponds precisely to this (extended) comportment analysis for function basic types β → β. It is obtained by a powerset completion (e.g. anti-chain) and reduction. The new element abs corresponds here to the set of basic comportments {con, div} and represents absence.

[figure: ∅; con; div; ide; str; tot; top; •; •; •; •; •; •; •]

Basic comportment B_{C}

[figure: ∅; {con}; {div}; {ide, div}; {str}; {top}; abs; {ide}; {tot}; {tot, div}; •; •; •; •; •; •; •; •; •; •]

Comportment C The disjunctive completion of B_{C} is the lattice C above since: (i) γ^{℘}({con, div}) ⊂ γ^{β→β}(con ∨ div), (ii) γ^{℘}({ide, div}) ⊂ γ^{β→β}(ide ∨ div), and (iii) γ^{℘}({tot, div}) ⊂ γ^{β→β}(tot ∨ div), while for any other Ψ ⊆ B_{C}, γ^{℘}(Ψ) = γ^{β→β}(∨Ψ). For instance, for any basic type β, the identity map λx^{β}.x^{β} is such that λx^{β}.x^{β} ∈ γ^{β→β}(con ∨ div) = γ^{β→β}(top) = D^{β→β}, whilst λx^{β}.x^{β} ∉ γ^{℘}({con, div}) = γ^{β→β}(con) ∪ γ^{β→β}(div).

To find out the least disjunctive basis of B_{C} in ℘(D^{β→β}), viz. the least disjunctive basis for the lattice of basic comportment analysis (which, by Theorem 4.4 or Theorem 4.5, exists since B_{C} is a finite lattice or ⟨℘(D^{β→β}), ⊆⟩ is dual-algebraic), we simply apply Corollary 4.10, that is we compute the Moore-closure of the joinirreducible elements of the disjunctive completion C of B_{C}. It is straightforward to verify that the least disjunctive basis Ω_{℘(D^{β→β})}(B_{C}) is the lattice depicted below.

[figure: ∅; con; div; ide; str; top; •; •; •; •; •; •]
The least disjunctive basis Ω_{℘(D^{β→β})}(B_{C})

The least disjunctive basis Ω_{℘(D^{β→β})}(B_{C}) is therefore a proper abstraction of the original basis B_{C} of basic comportments. In fact, the element tot denoting totality does not belong to the least disjunctive basis, since it can be recovered as lub of the elements ide and con representing identity and convergence, respectively.

7 Logic Programming: Optimizing Disjunctive Ground-Dependency Analysis

In this section, we apply the theory of the least disjunctive basis to Pos, a well known relational domain of propositional formulae for ground-dependency analysis of (constraint) logic programs ([1, 6, 19]). The disjunctive completion of Pos has been recently studied by Filé and Ranzato in [12], where it has been shown that it is strictly more precise than Pos itself. In a sense, this was a surprising result, since the fact that Pos is closed under logical disjunction should lead to an opposite conclusion. Therefore, static analyses based on the disjunctive completion of Pos are more precise. We show that the least disjunctive basis for the disjunctive completion of Pos is the domain Def , which is a proper abstraction of Pos. Def is a domain of propositional formulae already existing in literature, introduced by Dart in [11] for groundness analysis in deductive databases, and used by Marriott and Søndergaard in [19] for ground-dependency analysis of logic programs. Recently, Armstrong et al. in [1] investigated various representations for the formulae in Pos and Def , and they experimentally compared the resulting precision and efficiency of these different static analyses. They showed that analyses using Pos achieve a higher precision than those using Def , although there is an additional cost relatively small. However, this additional cost becomes relevant when lifting Pos and Def to the powerset, due to the combinatorial explosion of the disjunctive completion. In view of the work in [1], the results of this section gain an important and significative practical impact: the disjunctive ground-dependency analysis of logic programs can be always obtained by disjunctive completion of Def , without losing precision and at a lower cost with respect to the disjunctive completion of Pos. Moreover, this completes the understanding of the problem, since it is the best that one can do in this direction.

The domains Pos and Def . Let Var be a countable set of variables, and let VI be any (non-empty) finite subset of Var containing the variables of interest. As usual, variables are denoted by x, y, z, u, . . .. We assume that the concrete domain of computation of a given logic program is the powerset ℘(Sub) of idempotent substitutions, ordered with set-theoretic inclusion. Every substitution σ ∈ Sub is an idempotent function mapping each x ∈ Var to a term σ(x) built on the variables in Var, such that σ(x) ≠ x for a finite number of variables x. A substitution σ is typically specified by listing its non-trivial bindings, viz. σ = {x/σ(x) | σ(x) ≠ x}.

Pos is the finite lattice (indeed Boolean lattice) of positive Boolean functions on VI , where a Boolean function f is positive if f (true,…, true) = true. Obviously, the order of Pos is given by the logical consequence ⊧, and, lub and glb on Pos are given by logical disjunction and conjunction, respectively. Def is the finite lattice of positive Boolean functions on VI whose models are closed under intersection. Formulae in Def are called definite. For more details about Pos and Def see [1, 19]. It is well known that Boolean functions can be represented by means of propositional formulae. Thus, in the following, we will use propositional formulae over VI to represent Boolean functions in Pos and Def . Below, Pos and Def are depicted for VI = {x, y}.

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

The domains Pos and Def for VI ={x, y}

As observed in [1], Def is a meet-sublattice of Pos. Further, the top Boolean function true is in Def . Hence, Def is a Moore-family of Pos, namely, being (the set of fixpoints of) a closure operator on Pos, it is an abstract interpretation of Pos. The abstraction and concretization maps between Pos, Def and ℘(Sub) are well known, and can be found, e.g., in [6, 19]. For instance, assuming VI ={x, y, z, u}, the formula x ∧ (y ↔ z) is an element of Pos (and Def ) that represents the substitutions σ such that for any instance σ′ of σ: (i) the term σ′(x) is ground; (ii) σ′(y) is ground iff also σ′(z) is ground. In particular,^{5} σ_{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)).

5 By a, b, c, …, we denote ground terms.

The least disjunctive basis of Pos is Def . Filé and Ranzato showed in [12] that ℧_{℘(Sub)}(Pos) ⊏ Pos, i.e. there is a strict improvement in precision lifting Pos to its disjunctive completion. For example, by considering as variables of interest VI = {x, y}, the logical disjunction (x → y) ∨ (y → x) in Pos does not represent the concrete disjunction of the two formulae x → y and y → x, i.e. the union of their concretizations. In fact, γ(x → y) ∪ γ(y → x) ⊂ γ((x → y) ∨ (y → x)) = γ(true): σ = {x/v, y/w} is such that σ ∈ γ((x → y) ∨ (y → x)) \ γ(x → y) ∪ γ(y → x).

Sets of positive formulae for which logical (i.e., in Pos) and concrete (i.e., in ℘(Sub)) disjunctions coincide have been characterized as follows (cf. [13]).

Theorem 7.1 ([13]) If ∅ ≠ Φ ⊆ Pos then

∪{γ(f ) | f ∈ Φ} = γ(∨Φ) ⇔ ∀g ∈ Def . ((g ⊧ ∨Φ) ⇒ (∃f ∈ Φ. g ⊧ f )).

By Theorem 7.1, the disjunctive completion of Pos (after reduction), for VI = {x, y}, is the lattice depicted below.

[figure: ∅ = false; x ∧ y; x; x ↔ y; y; {x, x ↔ y}; {y, x ↔ y}; y → x; x → y; {x, x ↔ y, y}; {y, y → x}; x ∨ y; {x, x → y}; {y → x, x → y}; true; •; •; •; •; •; •; •; •; •; •; •; •; •; •; •]

℧_{℘(Sub)}(Pos) for VI = {x, y}

By Theorem 4.4 or Theorem 4.5, Ω_{℘(Sub)}(Pos) exists, since Pos is a finite lattice or ⟨℘(Sub), ⊆⟩ is dual-algebraic. The complexity of the simple case of two variables shows how difficult is the application of the method of join irreducible elements of Corollary 4.10 to compute the least disjunctive basis of Pos. The main result of this section can however be proved directly on the definition of Def and Pos.

Theorem 7.2 Ω_{℘(Sub)}(Pos) = Def .

Indeed, it is simple to verify on the previous diagrams for the case of two variables VI = {x, y}, that Def is the least abstraction of Pos having the same disjunctive completion. This particular case is also verifiable by applying Corollary 4.10: in fact, Def is precisely the Moore-closure of the join-irreducible elements of ℧_{℘(Sub)}(Pos). Moreover, Ω_{℘(Sub)}(Pos) = Def , while Ω_{Pos}(Pos) = M(JI_{Pos}), and for the case VI = {x, y}, the Moore-closure of the join-irreducible elements of Pos clearly does not coincide with Def (for instance, y → x ∈ Def \ M(JI_{Pos})). This proves the dependency of the least disjunctive basis operator on the concrete domain of reference, as postulated in Section 4.

8 Related Work

To the best of our knowledge, this is the first systematic characterization of least disjunctive bases for disjunctive completion in abstract interpretation. However, the use of join-irreducible elements to represent disjunctive properties is definitely not new, in particular in relation with the work of Nielson. Join-irreducible elements were firstly investigated in the context of abstract interpretation in [24], with the aim of giving an alternative (more concise) representation for the relational (Hoare) powerdomain in analysis of typed functional languages. We extend Nielson’s idea in the definition of our notion of least disjunctive basis. Least disjunctive bases are more general in this sense, since join-irreducible elements can only represent domains which are already disjunctive. The least disjunctive basis operator is applicable to arbitrary abstract interpretations, provided that the hypotheses of Theorem 4.4 or Theorem 4.5 are satisfied. In [24], Nielson investigates also the situation where the abstraction function maps join-irreducibile elements to join-irreducibile elements, defining the notion of expected form for an abstract interpretation, further studied in [26]. This is a related topic, and provides an interesting application of least disjunctive bases. Nielson suggests the use of expected forms in order to simplify the implementation of functionals induced in abstract interpretation of denotational semantics. The aim of expected forms is therefore similar to that of least disjunctive bases, both providing sensible simplifications in abstract interpretation design. In particular, some expected forms defined on collecting semantics, i.e. on some powerset domain, (e.g. for cond in [26]) can be viewed as functionals on the least disjunctive basis of the abstract domain.

Acknowledgments. We would like to thank Patrick Cousot, Gilberto Filé and Harald Søndergaard for many stimulating discussions on the subject of this paper.

References

1. T. Armstrong, K. Marriott, P. Schachte, and H. Søndergaard. Boolean functions for dependency analysis: algebraic properties and efficient representation. In Proc. of SAS ’94, LNCS 864, pp. 266–280, 1994. To appear in Sci. of Comp. Programming.

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

3. G. Birkhoff. Lattice Theory. AMS Colloq. Publ., vol. XXV, 3rd ed., 1967.

4. G.L. Burn, C.L. Hankin, and S. Abramsky. Strictness analysis of higher-order functions. Sci. of Comp. Programming, 7:249–278, 1986.

5. A. Cortesi, G. Filé, R. Giacobazzi, C. Palamidessi, and F. Ranzato. Complementation in abstract interpretation. In Proc. of SAS ’95, LNCS 983, pp. 100–117, 1995.

6. A. Cortesi, G. Filé, and W. Winsborough. Prop revisited: propositional formula as abstract domain for groundness analysis. In Proc. of LICS ’91, pp. 322–327, 1991.

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

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

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

10. 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. of IEEE ICCL ’94, pp. 95–112, 1994.

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

12. G. Filé and F. Ranzato. Improving abstract interpretations by systematic lifting to the powerset. In Proc. of ILPS ’94, pp. 655–669, 1994.

13. G. Filé and F. Ranzato. The powerset operator on abstract interpretations. Tech. Rep., Dip. di Matematica Pura ed Appl., U. di Padova, 1995.

14. G. Gierz, K.H. Hofmann, K. Keimel, J.D. Lawson, M. Mislove, and D.S. Scott. A Compendium of Continuous Lattices. Springer-Verlag, 1980.

15. S. Hunt. PERs generalize projections for strictness analysis. In Proc. of the 1990 Glasgow Funct. Progr. Workshop, pp. 156–168. Springer Workshops in Comp., 1990.

16. D. Jacobs and A. Langen. Static analysis of logic programs for independent ANDparallelism. J. of Logic Programming, 13(2,3):154–165, 1992.

17. T.P. Jensen. Disjunctive strictness analysis. In Proc. of LICS ’92, pp. 174–185. 1992.

18. N.D. Jones and S.S. Muchnick. Complexity of flow analysis, inductive assertion synthesis and a language due to Dijkstra. In Program Flow Analysis: Theory and Applications, pp. 380–393. Prentice-Hall, 1981.

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

20. J. Morgado. Some results on the closure operators of partially ordered sets. Port. Math., 19(2):101–139, 1960.

21. A. Mycroft. The theory and practice of transforming call-by-need into call-by-value. In Proc. of the 4th Int. Symp. on Programming, LNCS 83, pp. 270–281, 1980.

22. A. Mycroft. Abstract interpretation and optimizing transformations for applicative programs. Ph.D. Thesis, Dept. of Computer Science, U. of Edinburgh, CST-15-81, 1981.

23. A. Mycroft and F. Nielson. Strong abstract interpretation using power domains. In Proc. of ICALP ’83, LNCS 154, pp. 536–547, 1983.

24. F. Nielson. Abstract interpretation using domain theory. Ph.D. Thesis, Dept. of Computer Science, U. of Edinburgh, CST-31-84, 1984.

25. F. Nielson. Tensor products generalize the relational data flow analysis method. In Proc. of the 4th Hung. Computer Science Conf., pp. 211–225, 1985.

26. F. Nielson. Expected forms of data flow analysis. In Programs as Data Objects, LNCS 217, pp. 192–205, 1986.

27. P.L. Wadler and R.J.M. Hughes. Projections for strictness analysis. In Proc. of FPCA ’87, LNCS 274, pp. 385–407, 1987.

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