Optimal Domains for Disjunctive Abstract Interpretation

Roberto Giacobazzi^{a}  Francesco Ranzato^{b}

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

                             giaco@di.unipi.it

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

                            franz@math.unipd.it

Abstract

In the context of standard abstract interpretation theory, we define the inverse operation to the disjunctive completion of abstract domains, introducing the notion of least disjunctive basis of 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, also in relation with reduced product and complementation of abstract domains. The resulting framework provides advanced algebraic methodologies for abstract domain manipulation and optimization. These notions are applied to well-known abstract domains for static analysis of functional and logic programming languages.

Keywords: abstract interpretation, closure operator, disjunctive abstract domain, least disjunctive basis, functional and logic program analysis.

1 Introduction

Abstract interpretation ([12,13]) is a widely established theory for programming language semantics approximation. Different semantics, at different levels of abstraction, can be derived by abstract interpretation of a given concrete semantics ([8,11,15]). In particular, frameworks for program analysis, type inference and debugging can be specified and derived by abstract interpretation as approximations of the concrete semantics (see [8–10]).

A key rôle in this process of semantics approximation by abstract interpretation is played by abstract domains. Abstract domains provide a domain-like presentation for those semantic properties of the concrete domain of computation that are approximated by abstract interpretation. An abstract domain is assumed to be a

Preprint submitted to Elsevier Science

[figure: ∅; −; 0; +; −0; 0+; ZZ; •; •; •; •; •; •; •; Sign; ∅; −; 0; +; −0; 0+; ≠ 0; ZZ; •; •; •; •; •; •; •; •; Sign^{∨}]

Fig. 1. The abstract domain Sign and its disjunctive completion Sign^{∨}.

complete lattice, where the ordering relation describes the relative precision of domain objects – the top element representing no information. This is the case of the simple domain Sign, depicted in Fig. 1, abstracting sets of integer numbers (i.e. ℘(ZZ)), and which can be used for sign analysis of integer variables (we present a simple example later on). The interpretation of the elements of Sign is the obvious one: For example, the element −0 denotes the set of nonpositive integers. On the other hand, the concrete value {−5, −2} ∈ ℘(ZZ) is abstracted into the element − of Sign, which is the least element in Sign containing all negative numbers. More technically, the relationship between the concrete and the abstract domain is given by Galois connections (or, equivalently, by closure operators). However, for the rest of this section, the reader can simply consider a domain D more abstract than C if C contains all the information of D, i.e. D ⊆ C .

Since the very beginning of abstract interpretation, Cousot and Cousot ([13]) observed the importance of incrementally designing abstract domains. More expressive domains can be obtained by combining simpler ones, or by lifting them by adding new information. The first kind of operators are known as domain combinators, while the latter ones are known as domain completions. Examples of domain combinators are reduced product ([13]), reduced power ([13]), and tensor product ([35]), while domain completions include for instance disjunctive completion ([13]) and Moore-set completion ([23]). Both kinds of operators are devoted to enhance the expressive power of abstract domains, and have been called domain refinements (cf. [18,25]). All these domain operators provide high-level facilities to tune program analysis in accuracy and cost.

Disjunctive completion was originally introduced to exploit disjunctive program properties, notably to prove that merge-over-all-paths data-flow analysis can always be expressed in fixpoint form (cf. [13, Theorem 9.2.0.4]). Disjunctive completion was also considered in Nielson’s approach to abstract interpretation using domain theory ([35]), and applied in program analysis of functional and logic languages, e.g., in Jensen’s strictness logic for functional languages ([28]), in Cousot and Cousot’s comportment analysis of functional languages ([16]), and in ground-dependency analysis of logic languages ([19]). Some forms of disjunctive completion are also included as tools for automatically refining abstract domains, in modern systems for program analysis, like, for instance, in System Z ([39]).

The basic idea of disjunctive completion is simple: Abstract domains are enhanced by adding the information corresponding to the concrete disjunction of their elements, i.e., by adding a denotation for the lub in the concrete domain of the concretization of the abstract values. For instance, in the example above, the concrete disjunction is union of sets of integers. Hence, it is immediate to see that the domain Sign^{∨} depicted in Fig. 1 corresponds exactly to the disjunctive completion of Sign in ⟨℘(ZZ), ⊆⟩. In this example, a unique further element is added to Sign, namely ≠ 0. The symbol ≠ 0 denotes the concrete disjunction of the Sign-elements − and + (viz., ≠ 0 represents {x | x ≠ 0} = {x | x < 0} ∪ {x | x > 0}). In this sense, the abstract value of a program variable x is ≠ 0 if x is known to be either a positive or a negative integer.

As all domain refinements, the disjunctive completion of abstract domains allows to improve the precision of program analysis. As a very simple example, let us consider the sign analysis of the integer variables in the following simple program fragment:

C_{1}: if B then x := −5 else x := 5 fi; C_{2}: y := 3 div x

Assume that the analysis is defined by sequentially following the data flow, and by ignoring the conditional test B. This is specified by the abstract transition rules presented in Fig. 2, where the transitions occur among abstract states of the form ⟨(x, σ_{x} ), (y, σ_{y}), …⟩, where x, y, … are the variables into consideration, while σ_{x} , σ_{y} ∈ Sign are their corresponding abstract values. Here, α : ℘(ZZ) → Sign is the abstraction function, approximating any set of integers into the sign of its elements, as represented in Sign, whereas ∨ is the lub in Sign. The semantics of the conditional command corresponds to a form of merge-over-all-paths data flow analysis: Since the conditional expression is not evaluated, the analysis considers both branches as possible computations. For the program fragment C_{1}; C_{2}, supposing that x and y are undefined before the execution of C_{1}, it is clear that the analysis (with the abstract domain Sign) does not supply any information on the sign of the variables x and y:^{1}

⟨(x, ∅), (y, ∅)⟩ →^{C_{1}} ⟨(x, ZZ), (y, ∅)⟩ →^{C_{2}} ⟨(x, ZZ), (y, ZZ)⟩.

On the other hand, suppose that the same analysis is performed with the refined domain Sign^{∨}. Then, we get a more precise result saying that x and y are both different from zero:

⟨(x, ∅), (y, ∅)⟩ →^{C_{1}} ⟨(x, ≠ 0), (y, ∅)⟩ →^{C_{2}} ⟨(x, ≠ 0), (y, ≠ 0)⟩.

In particular, we can correctly deduce that no error can occur during the execution of C_{2}, provided that x be defined after the execution of C_{1}. This information is not available from the former analysis, because, even if x is defined, the state ⟨(x, ZZ), …⟩ may include the case x = 0 for which 3 div x is undefined.

1 Obviously, we implicitly use the most natural approximation div^{a} in the abstract domain Sign of the operation of division of integers (where, e.g., + div^{a} ZZ = ZZ).

⟨(x, σ_{x} ), (y, σ_{y}), …⟩ →^{x:=n} ⟨(x, α(n)), (y, σ_{y}), …⟩

⟨…, (x, σ_{x} ), …⟩ →^{C_{1}} ⟨…, (x, σ_{x}^{1}), …⟩ ⟨…, (x, σ_{x}^{1}), …⟩ →^{C_{2}} ⟨…, (x, σ_{x}^{2}), …⟩ ⟨…, (x, σ_{x} ), …⟩ →^{C_{1};C_{2}} ⟨…, (x, σ_{x}^{2}), …⟩

C ≡ if B then C_{1} else C_{2} fi

⟨…, (x, σ_{x} ), …⟩ →^{C_{1}} ⟨…, (x, σ_{x}^{1}), …⟩ ⟨…, (x, σ_{x} ), …⟩ →^{C_{2}} ⟨…, (x, σ_{x}^{2}), …⟩

⟨…, (x, σ_{x} ), …⟩ →^{C} ⟨…, (x, σ_{x}^{1} ∨ σ_{x}^{2}), …⟩

Fig. 2. Abstract transition rules.

The disjunctive completion of abstract domains is not only essential to achieve precision in modeling alternative computations. It plays also an important rôle in the design of relational program analyses ([29,35]). Cousot and Cousot suggested in [14] that a relational analysis can be induced by combining reduced product (denoted by ⊓) and disjunctive completion (denoted by ℧) of abstract domains, in the same way as the space of relations can be obtained in standard algebra by combining cartesian product and powerset. Thus, if D_{1} and D_{2} are abstract domains, a corresponding domain for relational analysis can 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 values.

The Problem: Simplifying Abstract Domains for Disjunctive Analysis. A natural question is: “Can we invert a process of abstract domain refinement”? Namely, can we define the “least basis” (that is, the most abstract domain) which induces a given domain by composition or completion? This question has been technically formulated in a very general setting in [25]. Recently, [5] solved positively the problem of inverting the reduced product domain refinement, introducing the notion of domain complementation in abstract interpretation.

In this work, we consider the inverse for the operator of disjunctive completion, namely an operator, denoted by Ω, that, given any domain D (abstracting C ), provides the most abstract domain (if it exists) whose disjunctive completion (in C ) coincides with that of D, viz. ℧(Ω(D)) = ℧(D). Intuitively, Ω and ℧ should work as compression and uncompression operations (w.r.t. disjunction) on abstract domains. In the example above, for instance, it is easy to see that in addition to Sign the domains depicted below all satisfy this condition, namely their disjunctive completion (in ℘(ZZ)) is Sign^{∨}. In this sense, they can all be candidates to be the “compression” of Sign^{∨} with respect to disjunction.

[figure: ∅; −; 0; +; −0; ZZ; •; •; •; •; •; •; ∅; −; +; 0; ≠ 0; ZZ; •; •; •; •; •; •; •; •; •; •; •; ZZ; −; 0; +; ∅; Sign^{b}]

It is simple to note that Sign^{b} is contained in all these domains, as well as in any other abstraction of Sign^{∨} which, by disjunctive completion, returns Sign^{∨} back. Hence, there is no abstract domain that is more abstract than Sign^{b}, and at the same time, induces the same disjunctive completion as Sign^{b}. For instance, the disjunctive completion of Sign^{±}, that is a proper abstraction of Sign^{b}, does not coincide with Sign^{∨}, i.e. ℧(Sign^{±}) = Sign^{≠0} ≠ Sign^{∨}, as depicted below.

[figure: •; •; •; •; ∅; +; −; ZZ; Sign^{±}; •; •; •; •; •; ∅; +; −; ≠ 0; ZZ; ℧(Sign^{±}) = Sign^{≠0}]

In this sense, Sign^{b} is the most abstract domain which, once refined by disjunctive completion, gives Sign^{∨} back.

The problem of finding a canonical subset of objects which, by means of a given operation, represent a given algebraic structure, is typical in lattice theory, and in particular in representation theory ([4,26]). We restrict here this investigation to specific algebraic structures, namely abstract domains for program analysis, and we introduce the notion of least disjunctive basis for them. The interest in this operation is twofold. Theoretically, least disjunctive bases contain the least amount of information which characterizes a given disjunctive property. This information must surely be included in any domain which is intended to meet a given disjunctive completion. On the practical side, least disjunctive bases are minimal (viz. nonredundant), providing useful space saving techniques to implement disjunctive completion of abstract domains, for instance for 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 a powerset construction), as most of the redundant information has been already removed from the source. Further, the least disjunctive basis operator can also 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 methodologies for domain manipulation and optimization.

Structure of the Paper. In Section 2, we introduce the basic notations and notions of abstract interpretation (and, in particular, on closure operators) used throughout the paper. The disjunctive completion operator on abstract domains is presented and discussed in Section 3, together with a number of related results. The disjunctive completion is first given in its most general form, i.e. when the concrete domain is an arbitrary complete lattice. Then, under the standard hypothesis of distributivity of the concrete domain, we give the usual powerset-like characterization of the disjunctive completion. In the latter case, additional properties of the disjunctive completion operator are proved. In Section 4, we introduce the notion of least disjunctive basis of a domain D, which is the most abstract domain inducing the same disjunctive completion as D, and we prove that, under certain reasonable hypotheses, least disjunctive bases exist. Particular emphasis is given to the least disjunctive basis of domains abstracting distributive lattices: Whenever the disjunctive completion of an abstract domain D can be expressed in the powerset-like form, its least disjunctive basis can be explicitly defined by using the join-irreducible elements of D. We study in Section 5 the algebraic properties of disjunctive completion and least disjunctive basis of abstract domains, also in relation with reduced product and complementation. In the same section, we also show that least disjunctive bases distribute compositionally with respect to the reduced product, and we give a domain-theoretic characterization of the redundant disjunctive information of an abstract domain, as the information which is not in its least disjunctive basis. These properties are all proved in the most general setting, where no hypothesis on the structure of the involved domains is assumed.

We apply the above results to abstract domains for analysis of functional (Section 6) and logic (Section 7) programming languages. The main achievements are as follows.

– The comportment domain has been introduced by Cousot and Cousot ([16]) for the analysis of higher-order functional programs. This abstract domain has been defined as disjunctive completion of a more simple basic comportment domain. We show that this definition might be sharpened, since we prove that the least disjunctive basis of the comportment domain is strictly more abstract than the basic comportment domain. Moreover, by combining domain complementation and least disjunctive basis, we introduce in Section 6 the notion of local optimization of abstract domains. This is obtained by removing from abstract domains only portions of their redundant disjunctive information. This is applied to the comportment domain in order to design new abstract domains for strictness and termination analysis.

– We show that the Marriott and Søndergaard domain Def (viz. the lattice of positive Boolean functions whose models are closed under intersection, cf. [30]) is the least disjunctive basis inducing the domain for disjunctive ground-dependency analysis of logic programs ([19]). This shows that Def , which is strictly more abstract, and therefore less expensive than Pos (viz. the lattice of positive Boolean functions, cf. [6,30]), always induces the same disjunctive ground-dependency analysis as Pos does, and in particular Ω(Pos) = Def .

The paper ends by addressing related literature and future work in Section 8.

2 Closure Operators and Abstract Interpretation

After introducing the mathematical notation used in the paper, in this section we present a brief overview of the basic notions on closure operators and abstract interpretation (in particular, complementation of abstract domains, cf. [5]). For more details about lattice theory, and in particular closure operators, the reader is referred to [4,26,31,38], while for abstract interpretation to [12,13].

2.1 Mathematical Notation

Let C and D be sets. The set-difference between C and D is denoted by C \ D, while C ⊂ D denotes proper inclusion. The powerset of D is denoted by ℘(D), and its cardinality by |D|. If f is a function defined on C and D ⊆ C then f (D) = {f (x) | x ∈ D}. By g ∘ f we denote the composition of the functions f and g, i.e. ∀x. (g ∘ f )(x) = g(f (x)). The set D equipped with a partial order ≤ is denoted by ⟨D, ≤⟩. By x < y we denote strict ordering. If D is a poset, we usually denote by ≤_{D} the corresponding partial order. If D is a poset and I ⊆ D then ↓ I = {x ∈ D | ∃y ∈ I . x ≤_{D} y}. For x ∈ D, ↓ x is a shorthand for ↓ {x}. By D^{op} we denote the dual-poset of D. A complete lattice D with partial ordering ≤, greatest lower bound (glb) ∧, least upper bound (lub) ∨, greatest element ⊤ = ∧∅ = ∨D, and least element ⊥ = ∨∅ = ∧D, is denoted ⟨D, ≤, ∧, ∨, ⊤, ⊥⟩. In a complete lattice D, a subset S ⊆ D is directed if every finite subset of S has an upper bound in S, while S is co-directed if it is directed in D^{op}. When D is a lattice, ∧_{D}, ∨_{D}, ⊤_{D} and ⊥_{D} denote the corresponding basic operators and elements. We use C ≅ D to denote that the ordered structures C and D are isomorphic. In the following, we will often abuse notation by denoting lattices with their poset notation.

2.2 Galois Connections and Closure Operators

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 we call (γ, D, C , α) a Galois insertion (G.i.) of D in C . We also recall that the above definition of G.c. is equivalent to that of adjunction: (γ, D, C , α) is an adjunction if ∀c ∈ C .∀d ∈ D. α(c) ≤_{D} d ⇔ c ≤_{C} γ(d). Abstract interpretations are traditionally specified in terms of Galois insertions: 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 concretization maps, respectively. Also, D is called an abstraction (or abstract interpretation) of C , and C a concretization of D. Furthermore, if C is not an abstraction of D, then we say that D is a strict abstraction of C . Galois insertions characterize “perfect” 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. may be lifted to a G.i. identifying in an equivalence class those values of the abstract domain with the same concrete meaning. This process is known as reduction of the abstract domain.

An (upper) closure operator, or simply a closure, on a poset ⟨L, ≤⟩ is an operator ρ : L → L monotonic, idempotent and extensive (viz. ∀x ∈ L. x ≤ ρ(x)). The set of all closure operators on L is denoted by uco(L). If ⟨L, ≤, ∧, ∨, ⊤, ⊥⟩ is a complete lattice then 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 is meet-closed (viz. for any Y ⊆ X , ∧Y ∈ X , where, in particular, ⊤ = ∧∅ ∈ X ). In this case, ρ_{X} = ∧{x ∈ X | y ≤ x} will denote the corresponding closure operator on L. For any X ⊆ L, M(X ) = {∧S | S ⊆ X } is the Moore-closure of X in L, i.e. the least subset of L containing X which is a Moore-family of L. The set of fixpoints ρ(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 ). The subset of uco(L) given by the additive closures will be denoted by uco^{a}(L). In view of the above equivalence, in the following a closure operator ρ will often denote the set of its fixpoints ρ(L). Being a set, the set of fixpoints of a closure is often denoted with capital Latin letters. Denoting closures by sets will be particularly convenient when closure operators will denote abstract domains. However, viewing closures as functions is also important in abstract interpretation, because they define the abstraction function. Hence, in the following, we will keep this soft ambiguity by using both notations, and leave to the reader to distinguish their use as functions or sets, according to the context. If L is a complete lattice then ⟨uco(L), ⊑, ⊓, ⊔, λx.⊤, λx.x⟩ is a complete lattice, 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;

– λx.⊤ is the top element, whereas λx.x is the bottom element.

For a closure operator ρ ∈ uco(L) and Y ⊆ L, the following two properties hold:

(i) ρ(∧ρ(Y )) = ∧ρ(Y ); (ii) ρ(∨Y ) = ρ(∨ρ(Y )).

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).

2.3 The Lattice of Abstract Interpretations

A key point in Cousot and Cousot’s abstract interpretation theory is the equivalence between the Galois insertion and closure operator approach to the design of abstract domains (cf. [13]). 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 the 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. It turns out that these two characterizations are one the inverse of the other. 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 this approach, and whenever we will say that D is an abstraction of C , we will mean that D is isomorphic to ρ_{D}(C ) (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 ([13]) 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 ⊓.

2.4 Complementation in Abstract Interpretation

The notion of domain complementation in abstract interpretation has been introduced in [5], and further studied in [21]. This operation provides a systematic method for decomposing abstract domains into simpler factors.

Complementation corresponds to the inverse of the reduced product (cf. [18]), that is, an operation which, starting from any two domains C ⊑ D, gives as result the most abstract domain C ∼ D, whose reduced product with D is exactly C (i.e., (C ∼ D) ⊓ D = C ). By the above equivalence between closure operators and abstract domains, this notion of complementation corresponds precisely to pseudocomplementation for ρ_{D} in uco(C ). We recall the well known lattice-theoretic notion of pseudocomplementation ([4]).

Definition 2.1 Let L be a meet-semilattice with bottom. The pseudocomplement of x ∈ L, if it exists, is the (unique) element x^{∗} ∈ L such that x ∧ x^{∗} = ⊥ and ∀y ∈ L. (x ∧ y = ⊥) ⇒ (y ≤ x^{∗}). If every x ∈ L has the pseudocomplement, L is called pseudocomplemented. □

In a complete lattice L, if the pseudocomplement x^{∗} exists then

x^{∗} = ∨{y ∈ L | x ∧ y = ⊥}.

Giacobazzi et al. solved positively in [22] the problem of pseudocomplementation for closure operators. Recall that a complete lattice C is meet-continuous if for any chain Y ⊆ C and x ∈ C , x ∧ (∨Y ) = ∨_{y∈Y} (x ∧ y) ([4,26]). The following result is recalled from [22].

Theorem 2.2 ([22]) If C is meet-continuous then uco(C ) is pseudocomplemented.

This result has been first applied in abstract interpretation in [5]. In particular, whenever C is meet-continuous, the complement C ∼D of a domain D with respect to C exists, and it is defined as:

C ∼D = ⊔{E ∈ uco(C ) | D ⊓ E = C }.

Meet-continuity is a sufficiently weak hypothesis to include most domains used in practice. For instance, it includes (see [26]) complete Heyting algebras, completely distributive, algebraic, complete Boolean and continuous lattices. Cortesi et al. observed in [5] that most of the abstract domains for program analysis are meetcontinuous. This is also the case of domains for denotational semantics, as proved in [24], where complementation has been fruitfully applied to “decompose” semantics of programming languages.

Assume that C ⊑ D, E and let ⊤ be the most abstract interpretation of C (i.e. the top closure λx.⊤). The following are some basic algebraic properties of complementation ([5]):

(a) D ⊑ C ∼(C ∼D);
(b) (D ⊑ E) ⇒ (C ∼E) ⊑ (C ∼D);
(c) (C ∼D) = C ∼(C ∼(C ∼D));
(d) C ∼⊤ = C and C ∼C = ⊤.

Complementation is important for abstract domain decompositions. If C ⊑ D then ⟨C ∼D, D⟩ is a (conjunctive binary) decomposition for C , namely C can be reconstructed by reduced product of its factors. The advantage of domain decomposition is twofold: (1) it provides more compact representations for complex domains, enhancing space saving techniques, and (2) it simplifies verification problems for complex domains, by decomposing them into simpler problems for their factors. We show how complementation actually works by a simple example.

Example 2.3 Consider the lattice Sign for sign analysis of an integer variable presented in Fig. 1 of Section 1. Recall that the concrete domain is ⟨℘(ZZ), ⊆⟩, while concretization and abstraction maps are the most natural. The (more abstract) lattice of positive values Sign^{+} can be “subtracted” from Sign by complementation (viz., Sign ∼Sign^{+}), yielding the lattice of negative values Sign^{−}.

• • • + 0+ ZZ Sign^{+}  • • • −0 ZZ Sign^{−} = Sign ∼Sign^{+}

⟨Sign^{+}, Sign^{−}⟩ is therefore a decomposition for Sign (i.e., Sign = Sign^{+} ⊓ Sign^{−}). In particular, 0 and ∅, which are not in Sign^{+} ∪ Sign^{−}, can be both reconstructed by reduced product from Sign^{+} and Sign^{−}. □

3 Disjunctive Completion by Closures

In this section, we reformulate using closure operators the standard Cousot and Cousot definition of disjunctive completion of an abstract domain ([13]), and study some of its algebraic properties, that will be useful later to characterize the inverse of disjunctive completion. Closure operators provide here the right high-level setting, where properties of abstract domains and operators for domain refinement can be studied independently from the representation of domain objects.

In view of their peculiar structure as Moore-families (cf. Sections 2.2 and 2.3), abstract domains support a precise interpretation for the glb operation, which abusively will be also called conjunction in the following. This is not in general the case for the dual operation of lub, also called disjunction. In technical terms, this means that if C is a complete lattice (the concrete domain), and ρ ∈ uco(C ) (the abstract domain), then for any X ⊆ ρ(C ), ρ(∧_{C} X ) = ∧_{C} X (by property (i) in Section 2.2), whilst ∨_{C} X ≤ ρ(∨_{C} X ). Hence, while abstract conjunction (i.e., λX .ρ(∧_{C} X )) always coincides (up to object names) with concrete conjunction (i.e., λX .∧_{C} X ), abstract disjunction (i.e., λX .ρ(∨_{C} X )) may cause a loss of information in the abstract domain. Disjunctive completion is therefore intended as a domain enhancement, which modifies a given abstract domain so that disjunction becomes precise.

Lemma 3.1 If ρ ∈ uco(C ) then (∀X ⊆ ρ(C ). ρ(∨_{C} X ) = ∨_{C} X ) ⇔ ρ ∈ uco^{a}(C ).

Proof. (⇒) Consider any Y ⊆ C . Then, we have that ρ(∨_{C} Y ) = (by property (ii) in Section 2.2) = ρ(∨_{C} ρ(Y )) = (by hypothesis) = ∨_{C} ρ(Y ). (⇐) If X ⊆ ρ(C ) then, by hypothesis, ρ(∨_{C} X ) = ∨_{C} ρ(X ), but since ρ(C ) is the set of fixpoints of ρ, we get ρ(∨_{C} X ) = ∨_{C} X . □

This lemma says that disjunction in an abstract domain is precise (in the sense above, as conjunction is) iff its associated closure operator is additive. Moreover, as recalled in Section 2.2, this is equivalent to the fact that the image of the closure is a complete sublattice of the concrete domain. These remarks justify the following technical definition of disjunctive completion by closure operators.

Let C be any complete lattice, and consider its lattice of abstract interpretations uco(C ). An additive extension of a closure ρ ∈ uco(C ) is any element belonging to the set {η ∈ uco^{a}(C ) | η ⊑ ρ}.

Lemma 3.2 If {ρ_{i}}_{i∈I} ⊆ uco^{a}(C ) then ⊔_{i∈I} ρ_{i} ∈ uco^{a}(C ).

Proof. Using the results recalled in Section 2.2, it is sufficient to verify that ∩_{i∈I} ρ_{i}(C ) is a complete sublattice of C . But this is evidently true, since, by hypothesis, each ρ_{i}(C ) is a complete sublattice of C . □

By this result, it is then natural to give the following definition.

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

Thus, the disjunctive completion operator maps any given abstract domain D, to the least common abstraction of the domains more precise than D and for which disjunction is precise. The correctness of this definition is therefore immediate by Lemma 3.2.

Proposition 3.4 For any ρ ∈ uco(C ), ℧_{C} (ρ) ∈ uco^{a}(C ).

℧_{C} (ρ) is called the disjunctive completion (in C ) of ρ ∈ uco(C ). Since ℧_{C} (ρ) is the greatest additive closure operator which is less than or equal to ρ, it is clear that our Definition 3.3 is equivalent to the original Cousot and Cousot definition in [13, Lemma 9.2.0.3]. It is worth noting that for any ρ ∈ uco(C ), ⊥_{C} ∈ ℧_{C} (ρ), because any additive closure is strict, namely ρ(⊥_{C} ) = ρ(∨_{C} ∅) = ∨_{C} ∅ = ⊥_{C} . In the following, we will apply the operator ℧ both to Moore-families and closure operators, being these two notions equivalent in view of our applications (cf. Sections 2.2 and 2.3). For the operator ℧_{C} , the following obvious result holds.

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

The meaning of the above proposition is clear: The disjunctive completion is a domain refinement, as defined in [18]. This means that ℧_{C} is a monotonic and reductive operator on uco(C ), and 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^{a}(C ), which is precisely the set of all disjunctive abstract interpretations of C . The following result is a straight consequence of Proposition 3.5, and characterizes the compositionality of the disjunctive completion with respect to the reduced product of abstract domains.

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

Proof. This follows by the dual of property (ii) in Section 2.2, since, by Proposition 3.5, ℧_{C} is a lower closure operator on uco(C ). □

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 whenever D is disjunctive. In order to show this fact, we need the following technical lemma on closure operators, that can be found, e.g., in [7, Theorem 4.2.0.4.7].

Lemma 3.7 ([7]) Let C be a complete lattice and η ∈ uco(C ). Then, uco(η(C )) ≅ {ρ ∈ uco(C ) | η ⊑ ρ}.

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

Proof. We reason on the associated closure operators; thus, the assumption is that ρ_{D}, ρ_{E} ∈ uco(C ) and ρ_{D} ⊑ ρ_{E}. By the isomorphism of Lemma 3.7, ρ_{E} can also be viewed as a closure operator on D. Therefore, ℧_{C} (E) = ℧_{C} (ρ_{E}) = ⊔{η ∈ uco^{a}(C ) | η ⊑ ρ_{E}}, while ℧_{D}(E) = ℧_{D}(ρ_{E}) = ⊔{μ ∈ uco^{a}(D) | μ ⊑ ρ_{E}}. Moreover, by Lemma 3.7, ℧_{D}(ρ_{E}) = ⊔{μ ∈ uco(C ) | ρ_{D} ⊑ μ ⊑ ρ_{E}, μ is additive on D}. Let us use the following notation: S_{C}^{E} = {η ∈ uco^{a}(C ) | η ⊑ ρ_{E}} and S_{D}^{E} = {μ ∈ uco(C ) | ρ_{D} ⊑ μ ⊑ ρ_{E}, μ is additive on D}. Now, if μ ∈ S_{D}^{E} then ℧_{C} (μ) ∈ S_{C}^{E}, because ℧_{C} (μ) ⊑ μ ⊑ ρ_{E} and ℧_{C} (μ) is additive on C . Therefore, we get that ℧_{C} (E) ⊑ ℧_{D}(E). Suppose now that D is disjunctive (on C ), i.e. ℧_{C} (D) = D. If μ ∈ uco(C ) is such that ρ_{D} ⊑ μ and μ is additive on D, then μ is additive on C : In fact, μ(C ) ⊆ ρ_{D}(C ) = D, and since, by hypothesis, D is a complete sublattice of C , also μ(C ) is a complete sublattice of C . Therefore, we have that S_{D}^{E} ⊆ S_{C}^{E}, i.e. ℧_{C} (E) = ℧_{D}(E). □

The following simple example shows this fact.

Example 3.9 Consider the lattice Sign of Example 2.3, and the lattice Sign^{±} depicted below. Evidently, Sign^{±} is an abstraction of Sign.

[figure: •; •; •; •; ZZ; −; +; ∅; Sign^{±} = ℧_{Sign}(Sign^{±}); •; •; •; •; •; ZZ; ≠ 0; −; +; ∅; ℧_{C} (Sign^{±})]

Clearly, Sign is not a disjunctive abstract interpretation of the concrete domain C = ℘(ZZ), since the lub of − and + is not precise. In this case, ℧_{C} (Sign^{±}) does not coincide with ℧_{Sign}(Sign^{±}). In fact, the disjunctive completion of Sign^{±} with respect to Sign, viz. ℧_{Sign}(Sign^{±}), is Sign^{±} itself, while the disjunctive completion with respect to C , viz. ℧_{C} (Sign^{±}), is the lattice depicted above. □

3.1 Powerset-Like Construction of the Disjunctive Completion

Definition 3.3 above gives an implicit account of the disjunctive completion, by defining it, for a domain D abstracting C , as the most abstract domain which is both more concrete than D, and, at the same time, a complete sublattice of C . In this section, we specialize the discussion to the case of concrete domains satisfying some hypothesis of distributivity. This gives the possibility to introduce an explicit definition of the disjunctive completion of an abstract domain using a powerset-like construction, analogous to the standard ones (cf. [14,16,19]). We recall below the standard definitions involving the finite and infinite distributivity laws for lattices (see e.g. [4,26]).

Definition 3.10 A complete lattice C is distributive (d), or completely distributive (cd), if for any {x_{i,k} | i ∈ I , k ∈ K (i)} ⊆ C and x, y, z ∈ C , the following identities respectively hold:

(d) x ∧ (y ∨ z) = (x ∧ y) ∨ (x ∧ z),
(cd) ⋀_{i∈I} ⋁_{k∈K (i)} x_{i,k} = ⋁_{f ∈K I} ⋀_{i∈I} x_{i,f (i)},

where for any i ∈ I , K (i) is a set of indices, and K^{I} is the set of all functions f from I to ∪_{i∈I} K (i) such that ∀i ∈ I . f (i) ∈ K (i). □

Obviously, (cd) ⇒ (d). For concrete domains that are completely distributive, the following result yields a powerset-like characterization of the disjunctive completion of an abstract domain.

Proposition 3.11 If C is a completely distributive lattice then, for any ρ ∈ uco(C ),

℧_{C} (ρ) = {∨S | S ⊆ ρ(C )}.

Proof. Let us call d_{C}^{ρ} = {∨S | S ⊆ ρ(C )}. In order to show that d_{C}^{ρ} ∈ uco^{a}(C ), we have to verify that M(d_{C}^{ρ}) = d_{C}^{ρ} and that ⟨d_{C}^{ρ} , ≤⟩ is join-closed. If X ⊆ d_{C}^{ρ} then we can write X = {∨S_{i}}_{i∈I} , with S_{i} = {z_{i,k}}_{k∈K (i)} ⊆ ρ(C ), for suitable sets of indices I and, for each i ∈ I , K (i). By this expression, it is clear that, by complete distributivity of C , we have that ∧X ∈ d_{C}^{ρ}. Moreover, it is also clear that ∨X = ∨{∨_{k∈K (i)}z_{i,k} | i ∈ I } = ∨{z_{i,k} | i ∈ I , k ∈ K (i)} belongs to d_{C}^{ρ}, proving that d_{C}^{ρ} is join-closed (i.e. a complete sublattice of C ). Moreover, by definition, ρ(C ) ⊆ d_{C}^{ρ}, hence showing that d_{C}^{ρ} is an additive extension of ρ. In order to conclude, we verify that if η is an additive extension of ρ then d_{C}^{ρ} ⊆ η(C ): If ∨S ∈ d_{C}^{ρ}, for some S ⊆ ρ(C ), then S ⊆ η(C ), and then ∨S ∈ η. □

The following example shows that without the hypothesis of complete distributivity of the concrete domain, in general, the above characterization is no longer true.

Example 3.12 Consider the finite lattice C depicted below.

[figure: ⊥; c; d; e; b; a; ⊤; •; •; •; •; •; •; •]

Consider also the closure ρ ∈ uco(C ) given by ρ(C ) = {⊤, b, c, d, ⊥}. It is easy to verify that the least additive extension of ρ is ℧_{C} (ρ) = C , whereas {∨S | S ⊆ ρ(C )} = C \ {e}, and this latter is not even a closure. □

In Proposition 3.11, for finite abstract domains, we can weaken the hypothesis on the concrete domain, requiring (finite) distributivity only.

Corollary 3.13 If C is a distributive complete lattice and ρ ∈ uco(C ) is finite (i.e., |ρ(C )| < ω), then ℧_{C} (ρ) = {∨S | S ⊆ ρ(C )}.

Proof. Observe in the proof of Proposition 3.11 that for a finite ρ, d_{C}^{ρ} is finite too. Then, by an easy inspection of that proof, we see that finite distributivity of C is sufficient. □

Proposition 3.11 does require the same hypothesis on the concrete domain as the usual standard powerset construction of the disjunctive completion ([14,19]) does. In this case, the above characterization actually gives rise to the standard powerset completion of an abstract domain written by a closure-like expression. Thus, whenever the concrete domain is completely distributive the disjunctive completion by closures (Definition 3.3) coincides with the standard powerset completion. Moreover, we have also observed in Corollary 3.13 that for finite abstract domains it is enough to consider the weaker hypothesis of (finite) distributivity for the concrete domain. However, it is worthwhile to remark that Definition 3.3 of disjunctive completion of an abstract domain is of wider applicability than the standard powerset definition. In fact, Example 3.12 shows that whenever the concrete domain is not (completely) distributive, in general, the standard powerset definition is not applicable, while, in contrast, Definition 3.3 is always applicable to any domain.

We close this section by giving an alternative, but equivalent, presentation for the disjunctive completion operator. We characterize the disjunctive completion of an abstract domain as a function, instead of a set. This may be sometimes more practical, in particular when abstract domains are defined by Galois connections, in order to identify explicitly the abstraction map corresponding to the disjunctive completion. In addition to complete distributivity, this result requires that the concrete domain is join-generated by a suitable subset of points, namely its joinirreducible elements (see [2,4,26]). In Section 4, join-irreducible elements will play a rôle also in characterizing the inverse operation to disjunctive completion.

Definition 3.14 Let C be a complete lattice and x ∈ C . x is (completely) joinirreducible if for any S ⊆ C , x = ∨S implies x ∈ S. The set of join-irreducible elements of C is denoted by JI (C ). □

The following lemma characterizing join-irreducible elements in completely distributive lattices is standard in lattice theory (cf.[2,26]).

Lemma 3.15 ([2]) Let C be a completely distributive lattice. Then, x ∈ JI (C ) iff for any S ⊆ C , x ≤ ∨S implies x ≤ s for some s ∈ S.

Let us recall that if C is a complete lattice and S ⊆ C then C is join-generated by S if for all x ∈ C , x = ∨(↓x ∩ S) (cf. [4,26]). We now prove the announced explicit functional characterization of the disjunctive completion operator.

Proposition 3.16 If C is completely distributive and join-generated by JI (C ), and ρ ∈ uco(C ), then

℧_{C} (ρ) = λx. ∨ {ρ(y) | y ∈ ↓x ∩ JI (C )}.

Proof. Let us define d_{C}^{ρ} = λx. ∨ {ρ(y) | y ∈ ↓x ∩ JI (C )}. We first prove that d_{C}^{ρ} ∈ uco^{a}(C ). Monotonicity of d_{C}^{ρ} is immediate, being ρ monotone. By hypothesis, if x ∈ C then x = ∨{y ∈ JI (C ) | y ≤ x}. Hence, since ρ is extensive, we have x ≤ ∨{ρ(y) | y ∈ ↓x ∩ JI (C )} = d_{C}^{ρ} (x), proving extensivity of d_{C}^{ρ}. We now prove that d_{C}^{ρ} is idempotent. For any x ∈ C , by Lemma 3.15, we have that

d_{C}^{ρ} (d_{C}^{ρ} (x)) = ∨{ρ(y) | y ∈ JI (C ), y ≤ ∨{ρ(z) | z ∈ JI (C ), z ≤ x}}
= ∨{ρ(y) | y ∈ JI (C ), y ≤ ρ(z), z ∈ JI (C ), z ≤ x}.

By monotonicity and idempotency of ρ, ρ(y) ≤ ρ(z) for any y ∈ JI (C ) such that y ≤ ρ(z) for some z ∈↓ x ∩ JI (C ). This implies that ∨{ρ(y) | y ∈ JI (C ), y ≤ ρ(z), z ∈ ↓ x ∩ JI (C )} ≤ ∨ρ(↓ x ∩ JI (C )), namely d_{C}^{ρ} (d_{C}^{ρ} (x)) ≤ d_{C}^{ρ} (x). Since we have already proved that d_{C}^{ρ} is extensive, this implies that d_{C}^{ρ} is idempotent. The following equalities prove that d_{C}^{ρ} is additive. For any S ⊆ C :

d_{C}^{ρ} (∨S) = ∨{ρ(y) | y ∈ JI (C ), y ≤ ∨S}
= ∨{ρ(y) | y ∈ JI (C ), s ∈ S, y ≤ s} (by Lemma 3.15)
= ⋁_{s∈S}(∨{ρ(y) | y ∈ JI (C ), y ≤ s})
= ∨d_{C}^{ρ} (S).

We observe that using the idempotency of ρ, for any x ∈ C , we get d_{C}^{ρ} (ρ(x)) = ∨{ρ(y) | y ≤ ρ(x), y ∈ JI (C )} ≤ ρ(x). This clearly implies that d_{C}^{ρ} (ρ(x)) = ρ(x), and therefore d_{C}^{ρ} ⊑ ρ. Consider now any η ∈ uco^{a}(C ) such that η ⊑ ρ. In order to conclude the proof, we have to demonstrate that η ⊑ d_{C}^{ρ}. Being η additive, for any x ∈ C , η(d_{C}^{ρ} (x)) = ∨{η(ρ(y)) | y ∈ ↓x ∩ JI (C )}. Because η ⊑ ρ, for any x ∈ C , η(ρ(x)) = ρ(x), and therefore η(d_{C}^{ρ} (x)) = d_{C}^{ρ} (x). This clearly means that η ⊑ d_{C}^{ρ}, as desired. □

4 Least Disjunctive Basis of Abstract Domains

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 ?

In the following, we positively answer this question. 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 lub of all closures having the same disjunctive completion as ρ, namely ⊔{η ∈ uco(C ) | ℧_{C} (η) = ℧_{C} (ρ)}, is denoted by Λ_{C} (ρ). It is worth noting that by monotonicity of ℧_{C} (cf. Proposition 3.5), for any ρ ∈ uco(C ), ℧_{C} (ρ) ⊑ ℧_{C} (Λ_{C} (ρ)) always holds. Hence, ρ ∈ uco(C ) is disjunctively optimizable if the converse holds.

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

If D is disjunctively optimizable then we also say that its least disjunctive basis exists, and in this case, we denote it by Ω_{C} (D). Ω_{C} (D) is therefore the most abstract domain such that ℧_{C} (Ω_{C} (D)) = ℧_{C} (D) holds. 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 result provides an alternative characterization for the least disjunctive basis.

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

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

Proof. (⇒) Define ρ̂ = Ω_{C} (ρ) = ⊔{η ∈ uco(C ) | ℧_{C} (η) = ℧_{C} (ρ)}. Condition (i) is satisfied by hypothesis. Moreover, if η ∈ uco(C ) is such that ℧_{C} (η) = ℧_{C} (ρ), then, clearly, η ⊑ ρ̂, so that (ii) is satisfied. Also, ρ̂ is the unique element in uco(C ) satisfying (i) and (ii): if ψ ∈ uco(C ) is another such an element different from ρ̂ then, by (i), ψ ⊑ ρ̂, while, by (ii), ρ̂ ⊑ ψ. (⇐) It is sufficient to verify that Λ_{C} (ρ) = ρ̂. This is evidently true, by conditions (i) and (ii) on ρ̂. □

The following simple example illustrates how the notion of least disjunctive basis actually works.

Example 4.4 Consider the domain Sign and its disjunctive completion (with respect to C = ℘(ZZ)) ℧_{C} (Sign) = Sign^{∨} both depicted in Fig. 1 of Section 1.

[figure: •; •; •; •; •; ZZ; −; 0; +; ∅; Λ_{C} (Sign) = Ω_{C} (Sign)]

It is easy to verify that the least common abstraction of all the domains having as disjunctive completion ℧_{C} (Sign), namely Λ_{C} (Sign), is the lattice depicted above. In this case, since ℧_{C} (Λ_{C} (Sign)) = ℧_{C} (Sign), the least disjunctive basis of Sign (in C = ℘(ZZ)) exists, and therefore it is Ω_{C} (Sign) = Λ_{C} (Sign). □

However, the least disjunctive basis of an abstract domain does not always exist, as the following example shows.

Example 4.5 Let C 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⟩; ⋮; ⋮; •; •; •; •; •; •; •]

For any k ∈ IN, consider the closure ρ_{k} = {⟨1, n⟩}_{n∈IN} ∪ {⟨0, n⟩}_{k≤n} ∪ {⊥}. It is clear that for any k ∈ IN, ℧_{C} (ρ_{k}) = C , and (⊔_{k∈IN}ρ_{k})(C ) = {⟨1, n⟩}_{n∈IN} ∪ {⊥} = (℧_{C} (⊔_{k∈IN}ρ_{k}))(C ). If, by contradiction, Ω_{C} (C ) exists, then ⊔_{k∈IN}ρ_{k} ⊑ Ω_{C} (C ). But, since ℧_{C} is monotonic, we should have ℧_{C} (⊔_{k∈IN}ρ_{k}) ⊑ ℧_{C} (Ω_{C} (C )) = C , i.e. we should obtain the contradiction C ⊆ {⟨1, n⟩}_{n∈IN} ∪ {⊥}. □

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 any (possibly infinite) abstract domain, provided that the concrete domain is completely distributive and co-algebraic. The second, instead, guarantees the existence of the least disjunctive basis for finite abstract domains, when the concrete domain is (finitely) distributive.

4.1 The Infinite Case

In this section, we prove that every (possibly infinite) abstraction of a co-algebraic completely distributive concrete domain is disjunctively optimizable. In order to do this, we need some technical results on algebraic complete lattices, also involving the notion of join-irreducibility. Firstly, let us recall the lattice-theoretic definition of co-algebraicity (see, e.g., [26]).

Definition 4.6 Let C be a complete lattice and x ∈ C .

(i) x is compact if for any S ⊆ C , x ≤ ∨S implies that there exists T ⊆ S, with T finite, such that x ≤ ∨T . The set of compact elements of C is denoted by K (C ).

(ii) The complete lattice C is algebraic if for any y ∈ C , y = ∨(↓y ∩ K (C )), while it is co-algebraic if C^{op} is algebraic. □

We recall from [26] two technical results on algebraic lattices. The first one gives a characterization of (co-)algebraic lattices (cf. [26, Theorem 4.15, pag. 89]), while the second one provides a representation for the elements of (co-)algebraic lattices using join-irreducible elements (cf. [26, Theorem 4.23, pag. 93]).

Theorem 4.7 ([26]) Assume that C is a complete lattice. C is co-algebraic iff C is isomorphic to a subset of ℘(X ), for some set X , ordered by inclusion and closed under arbitrary unions and intersections of co-directed families (in ⟨℘(X ), ⊆⟩) of sets.

Theorem 4.8 ([26]) If C is a co-algebraic complete lattice, then C is join-gene-rated by JI (C ).

In order to prove the main theorem of this section, we need the following lemma stating that the images of additive closures preserve co-algebraicity of complete lattices.

Lemma 4.9 If ⟨C , ≤⟩ is a co-algebraic complete lattice and ρ ∈ uco^{a}(C ), then ⟨ρ(C ), ≤⟩ is a co-algebraic complete lattice.

Proof. By Theorem 4.7, assume that C_{≤} ≅ S_{⊆}, for some S and X such that S ⊆ ℘(X ), where S is closed under arbitrary unions and co-directed intersections. Hence, also ρ(C ) is isomorphic to a subset of ℘(X ). Suppose that {Y_{i}}_{i∈I} ⊆ ρ(C ), for some set of indices I . Since ρ(C ) is a Moore-family, we have that ∩_{i∈I} Y_{i} ∈ ρ(C ). Moreover, since ρ is an additive closure, by Lemma 3.1, we also have that ∪_{i∈I} Y_{i} ∈ ρ(C ). Thus, being closed under arbitrary unions and intersections, by Theorem 4.7, ρ(C ) is, in particular, co-algebraic. □

We are now in the position to prove the main result of this section.

Theorem 4.10 If C is a co-algebraic completely distributive lattice, then each ρ ∈ uco(C ) is disjunctively optimizable.

Proof. As observed previously, it is enough to prove that ℧_{C} (ρ) ⊆ ℧_{C} (Λ_{C} (ρ)). Since, by Proposition 3.4, ℧_{C} (ρ) is additive, we have, by Lemma 4.9, that ℧_{C} (ρ) (intended as its set of fixpoints) is co-algebraic. Now, consider any x ∈ ℧_{C} (ρ). Since ℧_{C} (ρ) is co-algebraic, by Theorem 4.8, there exists R ⊆ JI (℧_{C} (ρ)) such that x = ∨R (note that the lub of ℧_{C} (ρ) coincides with the lub ∨ of C because ℧_{C} (ρ) is a complete sublattice of C ). If y ∈ R then, by Proposition 3.11, there exists T_{y} ⊆ ρ such that y = ∨T_{y}. Since y is join-irreducible (in ℧_{C} (ρ) where the lub is ∨), this implies that y ∈ T_{y}. Thus, we get R ⊆ ρ. Moreover, if we consider η ∈ uco(C ) such that ℧_{C} (η) = ℧_{C} (ρ) then, by the same reasoning, we get R ⊆ η. Thus, since Λ_{C} (ρ) = ∩{η ∈ uco(C ) | ℧_{C} (η) = ℧_{C} (ρ)}, we have that R ⊆ Λ_{C} (ρ). Therefore, by Proposition 3.11, x = ∨R ∈ ℧_{C} (Λ_{C} (ρ)), which concludes the proof. □

It is worthwhile to remark that any complete lattice isomorphic to a complete ring of sets (i.e., a subset of a powerset ℘(X ), for some set X , closed under arbitrary unions and intersections) is both co-algebraic and completely distributive (see [2,26]). Thus, in particular, the class of co-algebraic completely distributive lattices comprises the well known collecting domains, i.e. any powerset ℘(X ), for some set X , ordered with the subset or supset relation. Therefore, the standard concrete domains for collecting semantics of functional and logic programming (e.g. [3,34]) are included in this class (we will use these concrete domains in our examples in Sections 6 and 7).

4.2 The Finite Case

We now prove a second theorem assuring the existence of the least disjunctive basis for any finite domain abstracting a distributive complete lattice. Thus, the restriction to finite abstract domains allows us to weaken the hypothesis of complete distributivity on the concrete domain considered in Theorem 4.10.

Theorem 4.11 If C is a distributive complete lattice and ρ ∈ uco(C ) is finite, then ρ is disjunctively optimizable.

Proof. First, let us point out that, as usual, we do not distinguish between a closure operator and its set of fixpoints (i.e. its image). Recall the definition Λ_{C} (ρ) = ⊔{η ∈ uco(C ) | ℧_{C} (η) = ℧_{C} (ρ)}. As observed previously, it is enough to prove that ℧_{C} (ρ) ⊆ ℧_{C} (Λ_{C} (ρ)). Assume by contradiction, that there exists x ∈ ℧_{C} (ρ) \ ℧_{C} (Λ_{C} (ρ)). We prove by induction on natural numbers that for any n ∈ IN we are able to build a strictly decreasing chain {x_{j} }_{j ≤n} such that for any j ≤ n, x_{j} ∈ ℧_{C} (ρ) \ ℧_{C} (Λ_{C} (ρ)). (n = 0) By defining x_{0} = x, we have that x_{0} ∈ ℧_{C} (ρ) \ ℧_{C} (Λ_{C} (ρ)). (n + 1) By inductive hypothesis, x_{n} ∉ ℧_{C} (Λ_{C} (ρ)), from which we get x_{n} ∉ Λ_{C} (ρ), viz. x_{n} ∉ ∩{η ∈ uco(C ) | ℧_{C} (η) = ℧_{C} (ρ)}. Therefore, there exists η ∈ uco(C ) such that ℧_{C} (η) = ℧_{C} (ρ) and x_{n} ∉ η. Hence, x_{n} ∈ ℧_{C} (η) \ η. By Corollary 3.13, ℧_{C} (ρ) = ℧_{C} (η) is finite, and therefore, η ⊆ ℧_{C} (η) is finite as well. This implies that, by Corollary 3.13, there exists S ⊆ η such that x_{n} = ∨_{C} S and x_{n} ∉ S. Also, S ⊈ ℧_{C} (Λ_{C} (ρ)), otherwise we would have x_{n} = ∨_{C} S ∈ ℧_{C} (Λ_{C} (ρ)), a contradiction. Thus, there exists y ∈ S \ ℧_{C} (Λ_{C} (ρ)). Define x_{n+1} = y. We have that x_{n+1} ∈ η ⊆ ℧_{C} (η) = ℧_{C} (ρ), and, by construction, x_{n+1} ∉ ℧_{C} (Λ_{C} (ρ)). Moreover, x_{n+1} ≤ x_{n}, and x_{n+1} ≠ x_{n}, because x_{n+1} ∈ S while x_{n} ∉ S. To conclude the proof, note that, as observed above, ℧_{C} (ρ) is finite. This implies that if we build the above strictly decreasing chain of infinite length, we get the desired contradiction. □

It is worthwhile to note that most of the abstract domains used as basis of a static program analysis are finite, and hence for them one can exploit the weaker hypothesis on the concrete domain. In Sections 6 and 7, we will determine the least disjunctive basis of some finite abstract domains used for the analysis of functional and logic languages.

It is important to remark that the least disjunctive basis of a domain D, abstracting C , may well exist even if D and C do not satisfy the hypotheses of one of the two theorems of existence given above (i.e., Theorems 4.10 and 4.11). This is shown by the following example.

Example 4.12 Consider the finite lattice C and the closure ρ ∈ uco(C ) presented in Example 3.12. It is easily seen that C is not distributive, and therefore, for any abstraction of C neither Theorem 4.10 nor Theorem 4.11 are applicable. However, the least disjunctive basis Ω_{C} (C ) of C itself (in C ) exists, and it is actually given by the closure ρ. □

4.3 Least Disjunctive Basis and Join-Irreducible Elements

In case the concrete domain is a co-algebraic completely distributive lattice, from the proof of Theorem 4.10, we can observe that join-irreducible elements play an important rôle in the computation of the least disjunctive basis. Intuitively, they represent information that cannot be further decomposed by disjunction. In particular, join-irreducible elements allow to give an explicit characterization of the least disjunctive basis of an abstract domain D which is disjunctive, as proved below.

Theorem 4.13 Assume that C ⊑ D. If ℧_{C} (D) = D, and C is completely distributive and co-algebraic, or C is distributive and D is finite, then Ω_{C} (D) = M(JI (D)).

Proof. The case C completely distributive and co-algebraic is immediate, by inspection of the proof of Theorem 4.10. Assume C distributive and D finite. Let ρ ∈ uco(C ) be the closure operator associated with D, such that ℧_{C} (ρ) = ρ. We show that Ω_{C} (ρ) = M(JI (ρ)). First, observe that ℧_{C} (M(JI (ρ))) = ℧_{C} (ρ). Under the hypotheses of Theorems 4.11, since ρ = ℧_{C} (ρ) is finite, then, by Theorem 4.7, ℧_{C} (ρ) = {∨S | S ⊆ JI (℧_{C} (ρ))}, i.e. ℧_{C} (ρ) = ℧_{C} (JI (℧_{C} (ρ))). Thus, ℧_{C} (JI (ρ)) = ℧_{C} (ρ), as desired. Next, assume that η ∈ uco(C ) and ℧_{C} (η) = ℧_{C} (ρ). In this case, we want to prove that JI (ρ) ⊆ η. Suppose that x ∈ JI (ρ). Then, x ∈ ρ = ℧_{C} (ρ) = ℧_{C} (η). Note that since ℧_{C} (η) = ρ is finite, η ⊆ ℧_{C} (η) is finite as well. Therefore, by Corollary 3.13, there exists R ⊆ η such that x = ∨R. On the other hand, since η ⊆ ℧_{C} (η) = ℧_{C} (ρ) = ρ, we have that R ⊆ ρ. Hence, being x join-irreducible in ρ, we get x ∈ R ⊆ η. □

It is worth noting that the above result does not hold if the least disjunctive basis Ω_{C} (D) does not exist. For instance, in Example 4.5, JI (C ) = {⟨1, n⟩}_{n∈IN\{0}}, but, M(JI (C )) = {⟨1, n⟩}_{n∈IN} ∪ {⊥} is not the least disjunctive basis for C , as shown in that example. Obviously, since ℧_{C} (C ) = C , the least disjunctive basis of every concrete domain, satisfying the hypotheses above, is just the Moore-closure of its join-irreducible elements. Theorem 4.13 has another interesting consequence.

Corollary 4.14 Assume that C ⊑ D and C is completely distributive and coalgebraic, or C is distributive and D is finite. Then, Ω_{C} (D) = M(JI (℧_{C} (D))).

Proof. Since Ω_{C} (D) = Ω_{C} (℧_{C} (D)) and ℧_{C} (℧_{C} (D)) = ℧_{C} (D). □

In other terms, whenever the hypotheses of Theorems 4.10 and 4.11 are satisfied, the least disjunctive basis of an abstract domain D is always given by the Moore-closure of the join-irreducible elements of the disjunctive completion of D.

Example 4.15 With reference to Fig. 1 in Section 1, consider the abstract domain Sign and its disjunctive completion (w.r.t. C = ℘(ZZ)) ℧_{C} (Sign) = Sign^{∨}. It is clear that JI (℧_{C} (Sign)) = {−, 0, +}. Since the concrete domain C = ℘(ZZ) is a collecting domain, we can apply Corollary 4.14, obtaining the least disjunctive basis Ω_{C} (Sign) = M({−, 0, +}), as already computed in Example 4.4. □

Obviously, computing explicitly the whole disjunctive completion ℧_{C} (D) in order to characterize its join-irreducible elements, although being theoretically possible, is 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. From now on, whenever we will speak about least disjunctive bases, we will not suppose that conditions of Theorems 4.10 and 4.11 are satisfied, but merely we will assume their existence.

In general, 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 5.1 If C ⊑ D ⊑ E and ℧_{C} (D) = D then Ω_{C} (E) = Ω_{D}(E).

Proof. Let us define S_{C}^{E} = {A ∈ uco(C ) | ℧_{C} (A) = ℧_{C} (E)} and S_{D}^{E} = {B ∈ uco(D) | ℧_{D}(B) = ℧_{D}(E)}. Thus, explicitly, we have Ω_{C} (E) = ⊔S_{C}^{E} and Ω_{D}(E) = ⊔S_{D}^{E}. By Proposition 3.5, we have that ℧_{C} (D) ⊑ ℧_{C} (E), and because D = ℧_{C} (D) and ℧_{C} (E) ⊑ Ω_{C} (E), we get D ⊑ Ω_{C} (E) (i.e. Ω_{C} (E) ∈ uco(D)). Moreover, by Proposition 3.8, we have ℧_{D}(Ω_{C} (E)) = ℧_{C} (Ω_{C} (E)) = ℧_{C} (E) = ℧_{D}(E), which implies Ω_{C} (E) ∈ S_{D}^{E}. Thus, we get Ω_{C} (E) ⊑ Ω_{D}(E). To prove the other inclusion, assume that B ∈ S_{D}^{E}. Then, by Proposition 3.8, ℧_{C} (B) = ℧_{D}(B) = ℧_{D}(E) = ℧_{C} (E), i.e. B ∈ S_{C}^{E}. Therefore, Ω_{D}(E) ⊑ Ω_{C} (E). □

Next proposition summarizes the basic algebraic properties of the least disjunctive basis.

Proposition 5.2 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);

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

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

Proof. (a): Obvious from the definition. (b): We have that Ω_{C} (Ω_{C} (D)) = ⊔{A ∈ uco(C ) | ℧_{C} (A) = ℧_{C} (Ω_{C} (D))} = ⊔{A ∈ uco(C ) | ℧_{C} (A) = ℧_{C} (D)} = Ω_{C} (D). (c): By using (a). (d): Since ℧_{C} is idempotent (Proposition 3.5). (e): (⇒) By applying Ω_{C} and by (d); (⇐) By applying ℧_{C} . (f): ℧_{C} (Ω_{C} (D)⊓Ω_{C} (E)) = (Proposition 3.6) = ℧_{C} (℧_{C} (Ω_{C} (D))⊓℧_{C} (Ω_{C} (E))) = ℧_{C} (℧_{C} (D) ⊓ ℧_{C} (E)) = (Proposition 3.6) = ℧_{C} (D ⊓ E). □

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.3 Consider the abstract domains Sign and Sign^{+} of Example 2.3, where Sign ⊑ Sign^{+} (the concrete domain is as usual C = ℘(ZZ)). The least disjunctive basis Ω_{C} (Sign) is in Example 4.4, while it is simple to check that Ω_{C} (Sign^{+}) = Sign^{+}. This proves that the least disjunctive basis operator is neither monotonic nor anti-monotonic, since Ω_{C} (Sign) and Ω_{C} (Sign^{+}) are uncomparable abstractions of C . □

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

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

Domain decomposition by complementation 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. The following is a simple example exploiting the above result on compositionality.

Example 5.5 Consider the abstract domains Sign and Sign^{+} of Example 2.3, and suppose that Sign has been incrementally designed by reduced product of Sign^{+} and of the domain Sign^{−0} given below (the concrete domain is as usual C = ℘(ZZ)).

[figure: •; •; •; •; •; ZZ; −0; −; 0; ∅; Sign^{−0}; •; •; •; •; •; •; −; ∅; 0; ZZ; 0+; +; Ω_{C} (Sign^{+}) ⊓ Ω_{C} (Sign^{−0})]

Exploiting Corollary 5.4, we can compositionally compute the least disjunctive basis Ω_{C} (Sign) (in Example 4.4) of Sign from the least disjunctive bases Ω_{C} (Sign^{+}) and Ω_{C} (Sign^{−0}) of its factors. Indeed, the domain Ω_{C} (Sign^{+}) ⊓ Ω_{C} (Sign^{−0}), depicted above, is a proper abstraction of the starting domain Sign = Sign^{+} ⊓ Sign^{−0}, and therefore the task of computing the least disjunctive basis of Ω_{C} (Sign^{+}) ⊓ Ω_{C} (Sign^{−0}) is more simple. □

Characterizing Disjunctive Redundancies. The notion of least disjunctive basis allows to give a formal definition for the redundant disjunctive information of an abstract domain. Assume that D is an abstract interpretation of C and that Ω_{C} (D) exists. We define the redundant disjunctive information of the abstract domain D as the set D \ Ω_{C} (D) given by the set-theoretic difference between D and its least disjunctive basis Ω_{C} (D). Hence, D\Ω_{C} (D) is precisely the subset of D containing all and only those elements of D which can be systematically constructed by disjunctive completion with basis D.

Exploiting complementation, we can introduce another related interesting concept. We define the abstraction of disjunctive redundancy of D as the domain D ∼Ω_{C} (D), namely the complement of the least disjunctive basis Ω_{C} (D) with respect to D itself. Thus, D ∼Ω_{C} (D) characterizes precisely the most abstract domain (of D, and hence of C ) which composed by reduced product with the least disjunctive basis of D gives D back. Obviously, this definition makes sense whenever the involved least disjunctive basis and complement exist. Roughly speaking, the abstraction of disjunctive redundancy captures the least abstraction of D containing the redundant disjunctive information of D and which recovers the entire domain D when composed by reduced product with the least disjunctive basis of D. We illustrate these notions by our simple running example.

Example 5.6 Consider again Sign and ℧_{C} (Sign) = Sign^{∨} in Fig. 1. From Example 4.4 we know that Sign ⊏ Ω_{C} (Sign), where C = ℘(ZZ). The set of the redundant disjunctive information of Sign is therefore given by {−0, 0+}. In fact, both −0 and 0+ can be reconstructed by the subsets of the least disjunctive basis {−, 0} and {0, +}, respectively. On the other hand, it is easy to verify that the abstraction of disjunctive redundancy of Sign is the domain depicted below.

[figure: •; •; •; •; ZZ; −0; 0+; 0; Sign ∼Ω_{C} (Sign)]

□

6 Functional Programming: Optimizing Comportment Analysis

We apply the theory of the least disjunctive basis to the comportment analysis, designed by Cousot and Cousot in [16] to generalize Mycroft’s strictness and termination analysis ([32,33]), Wadler and Hughes’ projection analysis ([37]), and Hunt’s PER analysis ([27]). 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 β. Let denote

[figure: ∅; con; div; ide; str; tot; top; •; •; •; •; •; •; •]
B_{C}

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

Fig. 3. The abstract domains for basic comportment B_{C} and comportment C.

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  γ^{β→β}(∅)  = ∅

Fig. 4. Basic comportment analysis B_{C}.

D^{τ} the domain of values of a type τ, and ⊥ its bottom element. For simplicity, we will consider abstractions of basic function types β → β (i.e., elements in D^{β→β} = D^{β} → D^{β}, the lattice of continuous functions from D^{β} to D^{β} ordered pointwise). The abstract domain B_{C} depicted in Fig. 3 represents the lattice of basic comportment analysis, ordered with respect to the approximation order, for basic function types β → β. The meaning of basic comportments in B_{C} is given in Fig. 4, in terms of a concretization function γ^{β→β} mapping basic comportments into ⟨℘(D^{β→β}), ⊆⟩, which is the concrete domain of the collecting semantics. It is immediate to observe that B_{C} is precisely the reduced product of the standard Mycroft lattices for strictness (div < str < top, denoted by S) and termination (con < tot < top, denoted by T ) analysis (more precisely, using complementation, B_{C} ∼S = T and B_{C} ∼T = S).

As proved by Cousot and Cousot in [16], 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 order to exploit sets of values, Cousot and Cousot considered a powerset completion of the abstract domain, used

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

to mimic the collecting semantics construction. The corresponding abstract domain for comportments is derived by reduction of the powerset completion of the basic comportment lattice B_{C}, i.e. sets of basic comportments denoting the same object in ℘(D^{β→β}) are identified. Thus, the meaning of sets Ψ of basic comportments is given by a concretization γ^{℘} such that γ^{℘}(Ψ) = ∪{γ^{β→β}(ψ) | ψ ∈ Ψ}. The lattice C in Fig. 3, ordered by the approximation order, corresponds precisely to this (extended) comportment analysis for basic function types β → β. The new element abs corresponds here to the set of basic comportments {con, div} (it represents the property of absence, cf. [16]).

The disjunctive completion of B_{C} is the lattice C in Fig. 3 since:

(i) γ^{℘}({con, div}) ⊂ γ^{β→β}(con ∨ div), (ii) γ^{℘}({ide, div}) ⊂ γ^{β→β}(ide ∨ div), (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.10 or Theorem 4.11, exists since ⟨℘(D^{β→β}), ⊆⟩ is co-algebraic and completely distributive), we simply apply Corollary 4.14, 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 in Fig. 5. The least disjunctive basis Ω_{℘(D^{β→β})}(B_{C}) is therefore a proper abstraction of the original basis B_{C} of basic comportments. The redundant disjunctive information is given by totality tot, which can be recovered as lub of the elements ide and con representing identity and convergence, respectively.

Local Optimization. The least disjunctive basis can be combined with complementation in order to systematically simplify portions of abstract domains. Let C be a concrete domain and let D ⊑ E be abstractions of C . The domain D can be locally simplified by removing the disjunctive information which is not expressible by E. We call this method local optimization. The local optimization of D with respect to E is thus defined as Ω_{C} (D ∼E) ⊓ E. Obviously, this definition makes sense whenever the involved least disjunctive basis and complement exist. As proved by the proposition below, the local optimization of D with respect to E is an abstraction of D. Intuitively, the only disjunctive information which is preserved when moving from D to Ω_{C} (D ∼E) ⊓ E is that directly depending on the information in E. Any other form of disjunctive information is removed. In this sense, all the disjunctive information in D and in E is saved, while the disjunctive information of D which does not directly depend on E is removed. The following proposition also shows that the local optimization of D with respect to E has a more concrete least disjunctive basis than that of D, while it has the same disjunctive completion as D.

Proposition 6.1 Let C ⊑ D ⊑ E. Then,

(a) ℧_{C} (Ω_{C} (D ∼E) ⊓ E) = ℧_{C} (D);

(b) D ⊑ Ω_{C} (D ∼E) ⊓ E ⊑ Ω_{C} (D);

Proof. (a) ℧_{C} (Ω_{C} (D ∼ E) ⊓ E) = (Proposition 3.6) = ℧_{C} (℧_{C} (Ω_{C} (D ∼ E)) ⊓ ℧_{C} (E)) = ℧_{C} (℧_{C} (D ∼ E) ⊓ ℧_{C} (E)) = (Proposition 3.6) = ℧_{C} ((D ∼ E) ⊓ E) = ℧_{C} (D).

(b) Since D ⊑ D ∼ E ⊑ Ω_{C} (D ∼ E), we have that D = D ⊓ E ⊑ Ω_{C} (D ∼ E) ⊓ E. On the other hand, Ω_{C} (D ∼E) ⊓ E ⊑ Ω_{C} (D) follows by (a). □

As an example, we apply local optimization to the comportment domain, which clearly contains too much information with respect to strictness. The lattice C ∼S depicted below captures precisely nonstrictness analysis. In this case, by removing the element {tot, div} we get the least disjunctive basis Ω_{C}(C ∼S). Then, by adding strictness via reduced product we obtain the lattice Ω_{C}(C ∼S)⊓S, which is properly more abstract than C yet containing strictness, termination and basic comportment.

[figure: •; •; •; •; •; {top}; {tot, div}; abs; {tot}; {con}; C ∼S; •; •; •; •; {top}; abs; {tot}; {con}; Ω_{C}(C ∼S); •; •; •; •; •; •; •; •; •; •; ∅; {div}; {ide}; {con}; {str}; abs; {tot}; {top}; Ω_{C}(C ∼S) ⊓ S]

Here, {tot, div} is removed because it can be obtained by disjunctive completion of objects that do not include strictness str: abs ∨ {tot} = {tot, div}. The divergence information in {tot, div} is here inherited from abs, and not directly from any of the elements in S. It is also worth noting that {ide, div} cannot be reconstructed by reduced product from S and Ω_{C}(C ∼S).

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 abstract domain of propositional formulae for ground-dependency analysis of (constraint) logic programs ([1,6,30]). The disjunctive completion of Pos has been studied by Filé and Ranzato in [19], 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. 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 introduced by Dart in [17] for groundness analysis in deductive databases, and used by Marriott and Søndergaard in [30] for grounddependency analysis of logic programs. Armstrong et al. in [1] investigated various representations for the formulae in Pos and Def , and they experimentally compared precision and efficiency of static program analyses using these two domains. They showed that analyses using Pos achieve higher precision than those using Def , although there is a relatively small additional cost. 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 significant practical impact: The disjunctive ground-dependency analysis of logic programs can always be 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.

7.1 The Abstract Domains Pos and Def

Let Var be a countable set of variables, and let VI be any (nonempty) 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. A substitution σ is typically specified by the set of its nontrivial bindings, viz. σ = {x/σ(x) | σ(x) ≠ x}.

Pos is the finite lattice (indeed Boolean lattice) of positive Boolean functions on VI , where a Boolean function is positive if it gives true for the truth assignment where each variable is true. Obviously, the order of Pos is given by logical consequence ⊧, glb is given by logical conjunction, while lub on nonempty sets by logical disjunction (the lub of the empty set yields the bottom ∧VI ). 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 we refer to [1,30]. It is well known that Boolean functions can be represented by means of propositional formulae. Thus, in the following, we will use propositional formulae

[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; •; •; •; •; •; •; •]

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

over VI to represent Boolean functions in Pos and Def . In Fig. 6, Pos and Def are depicted for VI = {x, y}. As observed in [1], Def is a meet subsemilattice 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 [30]. 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,^{2} σ_{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)).

7.2 The Least Disjunctive Basis of Pos is Def

Filé and Ranzato showed in [19] that ℧_{℘(Sub)}(Pos) ⊏ Pos, namely there is a strict improvement in precision by lifting Pos to its disjunctive completion. For example, by considering as variables of interest VI = {x, y}, we have that 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. [20]).

Theorem 7.1 ([20]) 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 in Fig. 7.

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

[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; •; •; •; •; •; •; •; •; •; •; •; •; •; •; •]
Fig. 7. ℧_{℘(Sub)}(Pos) for VI = {x, y}.

By Theorem 4.10, Ω_{℘(Sub)}(Pos) exists, since ⟨℘(Sub), ⊆⟩ is collecting (on the other hand, Theorem 4.11 may be exploited as well). The complexity of the simple case of two variables shows that the application of the method of join-irreducible elements of Corollary 4.14 to compute the least disjunctive basis of Pos can result quite hard. The main result of this section can however be proved directly on the definition of Def and Pos.

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

Proof. We exploit Proposition 4.3. Therefore, let us first show that ℧_{℘(Sub)}(Def ) = ℧_{℘(Sub)}(Pos). Since Pos ⊑ Def , and, by Proposition 3.5, ℧_{℘(Sub)} is monotonic, we have ℧_{℘(Sub)}(Pos) ⊑ ℧_{℘(Sub)}(Def ). Now, consider any f ∈ Pos, and Φ_{f} = {g ∈ Def | g ⊧ f } ⊆ Def . It is known (cf. [1]) that in this case, f = ∨Φ_{f} holds. We want to verify that γ(∨Φ_{f} ) = ∪γ(Φ_{f} ). If h ∈ Def and h ⊧ ∨Φ_{f} = f then h ∈ Φ_{f} , and therefore, by Theorem 7.1, we have that γ(∨Φ_{f} ) = ∪γ(Φ_{f} ). This means that for any f ∈ Pos there exists S ⊆ Def such that γ(f ) = ∪γ(S), and hence ℧_{℘(Sub)}(Def ) ⊑ Pos. Hence, applying the idempotent and monotonic (cf. Proposition 3.5) operator ℧_{℘(Sub)}, we get the other inclusion, ℧_{℘(Sub)}(Def ) ⊑ ℧_{℘(Sub)}(Pos). Now, assume that there exists D abstracting ℘(Sub) such that ℧_{℘(Sub)}(D) = ℧_{℘(Sub)}(Pos). Then, we show that D ⊑ Def . Assume that f ∈ Def . Since Def ⊆ ℧_{℘(Sub)}(Def ) = ℧_{℘(Sub)}(Pos) = ℧_{℘(Sub)}(D), we have that f ∈ ℧_{℘(Sub)}(D). Hence, by Proposition 3.11, there exists S ⊆ D such that γ(f ) = ∪γ(S). Since D ⊆ ℧_{℘(Sub)}(Pos), for any x ∈ S there exists F_{x} ⊆ Pos such that γ(x) = ∪γ(F_{x} ). Hence, there exists Φ ⊆ Pos such that γ(f ) = ∪γ(Φ). Applying the Pos-abstraction map, and exploiting its additivity, we get f = ∨Φ, i.e. γ(∨Φ) = ∪γ(Φ). Thus, by Theorem 7.1, we have that for any g ∈ Def , g ⊧ ∨Φ implies that there exists h ∈ Φ such that g ⊧ h. By using this implication for f = ∨Φ ∈ Def , we get that there exists h ∈ Φ such that ∨Φ ⊧ h, i.e. f = ∨Φ ∈ Φ. Therefore, there exists x ∈ S such that f ∈ F_{x} , and γ(f ) ⊆ γ(x). But, since γ(f ) = ∪γ(S), we have that γ(x) = γ(f ), and thus f = x, from which f ∈ D. □

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.14: 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 also proves that the least disjunctive basis operator depends on the concrete domain of reference, as postulated in Section 5. Finally, note that the redundant disjunctive information of Pos is obviously given by the formula x ∨ y, which can be reconstructed in the disjunctive completion of the least disjunctive basis Def as {x, y}.

8 Related and Further Work

To the best of our knowledge, this is the first systematic characterization of least bases for the disjunctive completion of domains 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 Flemming Nielson. Joinirreducible elements were first investigated in the context of abstract interpretation in [35], 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, provided that the hypotheses of Theorem 4.10 or Theorem 4.11 are satisfied (cf. Theorem 4.13). In [35], Nielson investigates also the situation where the abstraction function maps join-irreducible elements to join-irreducible elements, defining a notion of expected form for an abstract interpretation, further studied in [36]. This could be a related topic, and it should provide 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 [36]), can be viewed as functionals on the least disjunctive basis of the abstract domain.

We conclude by observing that least disjunctive bases could be also applied in semantics of programming languages. Cousot and Cousot proved in [11,15] that many semantics of programming languages can be derived by abstract interpretation from a more concrete (usually operational) semantics. However, collecting semantics are generally defined exploiting a (more abstract) standard semantics, by “collecting” sets of possible output values corresponding to a given set of possible input values (e.g. [34]). This construction can be achieved by a disjunctive completion of the standard semantics, relatively to a more concrete operational semantics. The meaning of the least disjunctive basis should therefore be evident in semantics as well as in analysis: The least disjunctive basis of a collecting semantics is precisely the most abstract (standard) semantics which induces the same collecting semantics, and our results allow to characterize this “optimal” semantics as an abstract interpretation of the operational one. A similar application to semantics has been presented in [24], where complementation, i.e. the inverse of reduced product, has been used to derive new semantics for programming languages.

Acknowledgments

We would like to thank Patrick Cousot, Gilberto Filé and Harald Søndergaard for many stimulating discussions on the subject of this paper. We are also grateful to one anonymous referee for many helpful suggestions.

References

[1] T. Armstrong, K. Marriott, P. Schachte, and H. Søndergaard. Two classes of Boolean functions for dependency analysis. To appear in Sci. Comput. Program. A preliminary version appeared in Proc. SAS ’94, LNCS 864.

[2] R. Balbes and P. Dwinger. Distributive Lattices. University of Missouri Press, Columbia, Missouri, 1974.

[3] R. Barbuti, R. Giacobazzi, and G. Levi. A general framework for semantics-based bottom-up abstract interpretation of logic programs. ACM Trans. Program. Lang. Syst., 15(1):133–181, 1993.

[4] G. Birkhoff. Lattice Theory. AMS Colloquium Publication, Providence, R.I., 3rd edition, 1967.

[5] A. Cortesi, G. Filé, R. Giacobazzi, C. Palamidessi, and F. Ranzato. Complementation in abstract interpretation. ACM Trans. Program. Lang. Syst., 19(1):7–47, 1997.

[6] A. Cortesi, G. Filé, and W. Winsborough. Optimal groundness analysis using propositional logic. J. Logic Program., 27(2):137–167, 1996.

[7] P. Cousot. Méthodes Itératives de Construction et d’Approximation de Points Fixes d’Opérateurs Monotones sur un Treillis, Analyse Sémantique des Programmes. PhD thesis, Université Scientifique et Médicale de Grenoble, 1978.

[8] P. Cousot. Abstract interpretation. ACM Comp. Surv., 28(2):324–328, 1996.

[9] P. Cousot. Program analysis: the abstract interpretation perspective. ACM Comp. Surv., 28(4), 1996.

[10] P. Cousot. Types as abstract interpretations (invited paper). In Conference Record of the 24th ACM Symp. on Principles of Programming Languages (POPL ’97), pages 316–331. ACM Press, New York, 1997.

[11] P. Cousot. Design of semantics by abstract interpretation. Slides of an invited talk at 13th Int. Symp. on Mathematical Foundations of Programming Semantics (MFPS ’97), 1997.

[12] P. Cousot and R. Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Conference Record of the 4th ACM Symp. on Principles of Programming Languages (POPL ’77), pages 238–252. ACM Press, New York, 1977.

[13] P. Cousot and R. Cousot. Systematic design of program analysis frameworks. In Conference Record of the 6th ACM Symp. on Principles of Programming Languages (POPL ’79), pages 269–282. ACM Press, New York, 1979.

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

[15] P. Cousot and R. Cousot. Inductive definitions, semantics and abstract interpretation. In Conference Record of the 19th ACM Symp. on Principles of Programming Languages (POPL ’92), pages 83–94. ACM Press, New York, 1992.

[16] P. Cousot and R. Cousot. Higher-order abstract interpretation (and application to comportment analysis generalizing strictness, termination, projection and PER analysis of functional languages) (invited paper). In Proceedings of the IEEE Int. Conf. on Computer Languages (ICCL ’94), pages 95–112. IEEE Computer Society Press, Los Alamitos, Calif., 1994.

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

[18] G. Filé, R. Giacobazzi, and F. Ranzato. A unifying view of abstract domain design. ACM Comput. Surv., 28(2):333–336, 1996.

[19] G. Filé and F. Ranzato. Improving abstract interpretations by systematic lifting to the powerset. In M. Bruynooghe, editor, Proceedings of the 1994 Int. Logic Programming Symp. (ILPS ’94), pages 655–669. The MIT Press, Cambridge, Mass., 1994.

[20] G. Filé and F. Ranzato. The powerset operator on abstract interpretations. To appear in Theor. Comput. Sci., 1998.

[21] G. Filé and F. Ranzato. Complementation of abstract domains made easy. In M. Maher, editor, Proceedings of the 1996 Joint Int. Conf. and Symp. on Logic Programming (JICSLP ’96), pages 348–362. The MIT Press, Cambridge, Mass., 1996.

[22] R. Giacobazzi, C. Palamidessi, and F. Ranzato. Weak relative pseudo-complements of closure operators. Algebra Universalis, 36(3):405–412, 1996.

[23] R. Giacobazzi and F. Ranzato. Functional dependencies and Moore-set completions of abstract interpretations and semantics. In J. Lloyd, editor, Proceedings of the 1995 Int. Logic Programming Symp. (ILPS ’95), pages 321–335. The MIT Press, Cambridge, Mass., 1995.

[24] R. Giacobazzi and F. Ranzato. Complementing logic program semantics. In M. Hanus and M. Rodríguez Artalejo, editors, Proceedings of the 5th Int. Conf. on Algebraic and Logic Programming (ALP ’96), volume 1139 of Lecture Notes in Computer Science, pages 238–253. Springer-Verlag, Berlin, 1996.

[25] R. Giacobazzi and F. Ranzato. Refining and compressing abstract domains. In P. Degano, R. Gorrieri, and A. Marchetti-Spaccamela, editors, Proceedings of the 24th Int. Colloq. on Automata, Languages and Programming (ICALP ’97), volume 1256 of Lecture Notes in Computer Science, pages 771–781. Springer-Verlag, Berlin, 1997.

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

[27] S. Hunt. PERs generalize projections for strictness analysis. In S. Peyton Jones, G. Hutton, and C. K. Holst, editors, Proceedings of the 1990 Glasgow Functional Programming Workshop, Workshops in Computing, pages 156–168. Springer-Verlag, Berlin, 1990.

[28] T. P. Jensen. Disjunctive strictness analysis. In Proceedings of the 7th IEEE Symp. on Logic in Computer Science (LICS ’92), pages 174–185. IEEE Computer Society Press, Los Alamitos, Calif., 1992.

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

[30] K. Marriott and H. Søndergaard. Precise and efficient groundness analysis for logic programs. ACM Lett. Program. Lang. Syst., 2(1-4):181–196, 1993.

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

[32] A. Mycroft. The theory and practice of transforming call-by-need into call-by-value. In B. Robinet, editor, Proceedings of the 4th Int. Symp. on Programming, volume 83 of Lecture Notes in Computer Science, pages 270–281. Springer-Verlag, Berlin, 1980.

[33] A. Mycroft. Abstract Interpretation and Optimising Transformations for Applicative Programs. PhD thesis, CST-15-81, Univ. of Edinburgh, Scotland, 1981.

[34] A. Mycroft and F. Nielson. Strong abstract interpretation using power domains. In J. Díaz, editor, Proceedings of the 10th Int. Colloq. on Automata, Languages and Programming (ICALP ’83), volume 154 of Lecture Notes in Computer Science, pages 536–547. Springer-Verlag, Berlin, 1983.

[35] F. Nielson. Abstract Interpretation using Domain Theory. PhD thesis, CST-31-84, Univ. of Edinburgh, Scotland, 1984.

[36] F. Nielson. Expected forms of data flow analysis. In H. Ganzinger and N. D. Jones, editors, Programs as Data Objects, volume 217 of Lecture Notes in Computer Science, pages 192–205. Springer-Verlag, Berlin, 1986.

[37] P. Wadler and R. J. M. Hughes. Projections for strictness analysis. In G. Kahn, editor, Proceedings of the Int. Conf. on Functional Programming Languages and Computer Architecture (FPCA ’87), volume 274 of Lecture Notes in Computer Science, pages 385–407. Springer-Verlag, Berlin, 1987.

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

[39] K. Yi and W. L. Harrison III. Automatic generation and management of interprocedural program analyses. In Conference Record of the 20th ACM Symp. on Principles of Programming Languages (POPL ’93), pages 246–259. ACM Press, New York, 1993.