A Logical Model for Relational Abstract Domains

ROBERTO GIACOBAZZI and FRANCESCA SCOZZARI Università di Pisa

In this article we introduce the notion of Heyting completion in abstract interpretation. We prove that Heyting completion provides a model for Cousot’s reduced cardinal power of abstract domains and that it supplies a logical basis to specify relational domains for program analysis and abstract interpretation. We study the algebraic properties of Heyting completion in relation with other well-known domain transformers, like reduced product and disjunctive completion. This provides a uniform algebraic setting where complex abstract domains can be specified by simple logic formulas, or as solutions of recursive abstract domain equations, involving few basic operations for domain construction, all characterized by a clean logical interpretation. We apply our framework to characterize directionality and condensing in downward closed analysis of (constraint) logic programs.

Categories and Subject Descriptors: D.3.4 [Programming Languages]: Processors—optimization; F.3.2 [Logics and Meanings of Programs]: Semantics of Programming Languages— program analysis; F.4.1 [Mathematical Logic and Formal Languages]: Mathematical Logic

General Terms: Languages, Theory Additional Key Words and Phrases: Abstract interpretation, closure operators, condensing analysis, constraint logic programming, directional types, domains, Heyting completion, intuitionistic logic, reduced cardinal power, static analysis

1. INTRODUCTION

Abstract interpretation has been introduced in 1977 by Patrick and Radhia Cousot as a general theory for specifying and then validating program analyses [Cousot and Cousot 1977]. In recent years, this theory has increasingly gained popularity as a theory for approximating the semantics of generic discrete dynamic systems, and it has been applied in many different areas of computer science (cf. Cousot [1996]). The idea of abstract interpretation is that the analysis of a system, e.g., a program, can be obtained as an approximation of its formal semantics. The (concrete) semantics of a programming language is traditionally specified by a concrete domain C of objects and a semantic function ⟦·⟧ : P rogram → C, associating with

A preliminary version of this article appeared in Proceedings of the 9th International Symposium on Programming Languages, Implementations, Logics, and Programs (PLILP ’97 ), Southampton UK. Authors’ addresses: R. Giacobazzi, Università di Pisa, Dipartimento di Informatica, Corso Italia 40, 56125 Pisa, Italy; email: giaco@di.unipi.it; F. Scozzari, Università di Pisa, Dipartimento di Informatica, Corso Italia 40, 56125 Pisa, Italy; email: scozzari@di.unipi.it. Permission to make digital/hard copy of all or part of this material without fee is granted provided that the copies are not made or distributed for profit or commercial advantage, the ACM copyright/server notice, the title of the publication, and its date appear, and notice is given that copying is by permission of the Association for Computing Machinery, Inc. (ACM). To copy otherwise, to republish, to post on servers, or to redistribute to lists requires prior specific permission and/or a fee.

2 · Giacobazzi and Scozzari

each (well-formed) program P ∈ P rogram its semantics ⟦P ⟧ ∈ C. According to the classical Cousot and Cousot [1977] framework, an abstract interpretation is defined as a nonstandard (approximated) program semantics, which is obtained from the standard (or concrete) one by substituting the concrete domain C of computation and its semantics ⟦·⟧ with, respectively, an abstract domain A and an abstract semantics ⟦·⟧^{♯}.

One of the most fundamental facts of abstract interpretation is that most properties of the abstract semantics ⟨A, ⟦·⟧^{♯}⟩, like precision, completeness, and compositionality, where ⟦·⟧^{♯} may involve complex operators, fixpoints etc., all depend on the notion of abstraction, which is precisely and uniquely specified by the chosen domain of properties A (cf. Cousot and Cousot [1979]). Central in the construction of an abstract interpretation is therefore the notion of domain. A domain of properties is a set of mathematical objects which represent the properties about the dynamic system we are interested in. The notion of approximation is encoded in domains by a suitable partial order, and both C and A are assumed to be complete lattices with respect to this order. The orderings on the concrete and abstract domains describe the relative precision of domain values, somehow in a dual fashion with respect to the standard domains for denotational semantics—the top element representing no information. Therefore, a ∈ A approximates c ∈ C if a represents some concrete object c̃ ∈ C such that c ≤ c̃. Consider for instance the concrete lattice of sets of integers ℘(ℤ), whose points are traditionally used to represent the set of possible values of integer variables at a given program point. The following simple complete lattice N at is an abstract domain which provides information to detect whether an integer variable is a strictly positive number. In this case, the elements: ℤ, ≥ 0, and > 0 represent the corresponding sets of integers:

• • • ℤ ≥ 0 > 0

Because of the key role of domains in abstract interpretation, any formal method to compare or transform abstract interpretations is inherently based on corresponding methods to compare and transform abstract domains: modifying domains corresponds to modify abstract interpretations. The foundation of a theory of domains for abstract interpretation was fixed by Cousot and Cousot [1979], and later expanded by Giacobazzi and Ranzato [1997b]. A number of operations have been designed to systematically construct new abstract domains from given ones, by refinement [Cortesi et al. 1994; Cousot and Cousot 1979; 1994; Filé and Ranzato 1994; Giacobazzi and Ranzato 1998; 1997a; Jensen 1992; Nielson 1985], simplification [Giacobazzi and Ranzato 1997a], decomposition [Cortesi et al. 1997], and compression [Giacobazzi and Ranzato 1996], and some of them have been included as tools for design aid in modern systems for program analysis, like in GAIA [Cortesi et al. 1994], PLAI [Codish et al. 1995], and System Z [Yi and Harrison 1993], providing high-level facilities to tune program analysis in accuracy and costs. Most of these operations arise from the common logical operations on program properties. A typical example is reduced product [Cousot and Cousot 1979], which is, among these operations, the most common and widely used one (e.g., see Click

ACM Transactions on Programming Languages and Systems, To appear.

A logical model for relational abstract domains · 3

and Cooper [1995], Codish et al. [1995], Muthukumar and Hermenegildo [1991], and Sundararajan and Conery [1992]). Reduced product corresponds to cartesian product of domains, where tuples having equivalent meaning, namely representing the same concrete property, are identified, viz., reduced. Consider for instance the domains N at and N eg depicted below. The reduced product of the two domains is a new richer domain, denoted by N at ⊓ N eg, which includes both the given domains and is closed under intersection. Intersection plays the role of conjunction of properties. For instance, the new object 0 denotes the conjunctive property for a program variable of being simultaneously both nonnegative (≥ 0) and nonpositive (≤ 0). From the domain point of view, the reduced product of two domains corresponds to the simplest (most abstract) domain which is more precise than the two given domains, i.e., which derives at least the same properties, as follows:

\begin{matrix}^{• • • ℤ ≥ 0 > 0} & ^{• • • ℤ ≤ 0 < 0} & [figure: •; •; •; •; •; •; •; 0; < 0; > 0; ∅; ≤ 0; ≥ 0; ℤ] \\ N at & N eg & N at ⊓ N eg \end{matrix}

Another well-known operation for domain transformation, which has a clean logical interpretation, is disjunctive completion, also introduced in Cousot and Cousot [1979]. The disjunctive completion of a domain is the most abstract domain able to represent the concrete disjunction of its objects. This operation has been widely used in static program analysis (e.g., see Cousot and Cousot [1994; 1992], Filé and Ranzato [1998], and Jensen [1992]) to improve precision in case of multiple branches in approximated computations, and more recently in analysis of reactive systems and abstract model checking [Dams et al. 1997]. From a logical point of view, disjunctive completion upgrades a domain with disjunctive information: the disjunctive completion of a given domain X is the least domain which includes X and is closed under possibly infinite disjunctions. In the case of our example, where the disjunction on the concrete lattice ℘(ℤ) is simply set union, the disjunctive completion of the domain N at ⊓ N eg is obtained by adding the only missing disjunctive point ≠ 0, which is obtained as union of < 0 and > 0 and which represents the disjunctive property for a program variable of being either positive or negative, as follows:

[figure: •; •; •; •; •; •; •; 0; < 0; > 0; ∅; ≤ 0; ≥ 0; ℤ; •; •; •; •; •; •; •; •; 0; < 0; > 0; ∅; ≤ 0; ≥ 0; ℤ; ≠ 0]
N at ⊓ N eg  Disjunctive completion

The Problem. The success of reduced product and disjunctive completion in systematic design of domains, for instance in program analysis, stems from their clean

ACM Transactions on Programming Languages and Systems, To appear.

logical interpretation, respectively as conjunction and disjunction of domain’s properties. Unfortunately, there are operations for domain construction and transformation for which a corresponding logical interpretation is not known. These include, among the others, the basic operations for transforming a domain to include some sort of relational information about its objects. The very first example of domain constructor for this purpose is Cousot’s reduced cardinal power, introduced together with reduced product and disjunctive completion in their POPL’79 paper [Cousot and Cousot 1979]. In reduced cardinal power, monotone functions are used to represent relational information between properties of programs. A given domain is upgraded by first including all monotone functions between its objects (which corresponds to the lattice-theoretic notion of cardinal power [Birkhoff 1967]) and then by identifying (viz., reducing) those functions that represent the same relational property between domain’s objects. The relational information supplied by reduced cardinal power is particularly important in program analysis, e.g., for transforming programs in such a way that they can be efficiently executed on parallel computers, and in comparative semantics, where similar relational information has been used to design compositional semantics for logic programs in Giacobazzi and Ranzato [1995]. In particular in program analysis, the possibility to tune the analysis in independent attribute and relational mode is probably one of the most attractive features of the abstract interpretation technology. The efficient but less precise independent attribute analysis method assigns properties to program objects, independently from the properties of other objects. In analysis, this is often insufficient for accurately detecting important program properties, like variable aliasing. This method is generalized by the more precise but costly relational one, which exploits at each program point the relations between the properties of program objects (cf. Jones and Muchnick [1981]), e.g., to express input/output relations. Although the relational information supplied by reduced cardinal power is clearly fundamental for most analyses, this domain constructor is rarely applied in the literature. To the best of our knowledge, the first use of reduced cardinal power after Cousot’s original definition, has been considered about 20 years later in Giacobazzi and Ranzato [1995]. This is quite surprising because, as we prove in this article, most well-known domains for relational program analysis can be specified in this way. We believe that this failure is mostly due to the lack of a clean logical interpretation for this operation, which makes it difficult to understand the meaning of the objects in the reduced cardinal power of domains.

The Idea: Implications to Model Reduced Cardinal Power. Relational information in domains is traditionally used to express relations between properties of program’s objects (e.g., variables) at different program points. The idea of this article originates by observing that, in order to exploit the relational information gathered at different program points, we need some objects in the domain which represent the implicational relation φ → ψ: given two properties φ and ψ, the property φ → ψ encodes the fact that whenever φ holds, then ψ holds too.

In the case of abstract interpretation, the properties of interest about the execution of a program are approximated by the objects of the abstract domain. The idea is therefore to enhance a given abstract domain of basic properties to include the space of all above implications built from every pair of its elements: for

ACM Transactions on Programming Languages and Systems, To appear.

any pair of objects a and b in a domain A, a relational object, called implication and denoted by a → b, is included in the enhancement of A, in such a way that the conjunction of a and a → b is still approximated by b. In general, there are many possible choices for a concrete object c such that the above modus ponens law holds, i.e., a ∧ c ≤ b. In order to have a unique best representative object to express the above relational information, we are interested in those lattices where there exists a most abstract object, yet satisfying the modus ponens law. These are well-known lattices called Heyting algebras, which are precisely the models of intuitionistic logic [Birkhoff 1967; van Dalen 1994].^{1} Intuitionistic logic is the weakest framework where relational information can be exploited by implicational objects. We can think of φ → ψ as an automatic method for transforming proofs of φ into proofs of ψ: if we are able to prove φ at given program point, then we are able to prove ψ too. The general idea of interpreting implications as functions mapping proofs into proofs goes back to Heyting [Girard et al. 1989] and gives semantics to a logic weaker than classical logic, which is known as intuitionistic (constructive) logic. In this new logic, neither proofs by contradiction nor proofs by cases are allowed. The basic idea of intuitionistic logic is to model the notion of “provable sentence.” For instance, the implicational relation φ → φ is interpreted as the identity function, which associates with each proof of φ the same proof. It is easy to imagine that there always exists a proof constructor which simply returns the input proof, for every formula φ. Therefore φ → φ is always a true sentence, i.e., it is a tautology: φ → φ = ⊤. What makes intuitionistic logic weaker than classical logic is the treatment of negation: ¬φ means that φ is not provable. It denotes the implication φ → ⊥, where ⊥ represents a sentence with no possible proof. The intuitive meaning of φ → ⊥ is a method for transforming proofs of φ in proofs of an unprovable sentence. As a consequence, the well-known tautology of classical logic φ ∨ ¬φ does not hold anymore, because in general we might not be able to exhibit a proof of either φ or ¬φ, for some sentence φ. We lose therefore the tautology of classical logic φ → ψ = ¬φ ∨ ψ, since the formula on the right-hand side does not provide a constructive method to obtain a proof of ψ from a proof of φ. The notion of negation is therefore weaker in intuitionistic logic than in classical logic. While φ ∧ (φ → ⊥) = ⊥ always holds (it is a sort of consistency statement: we cannot prove both φ and its contrary), it is not in general true that φ ∨ (φ → ⊥) = ⊤, i.e., in some cases we are not able to prove neither φ nor its contrary. When this latter equality holds, the whole system boils down to classical logic. Consider the domain N at described above. We are in the case of classical logic, because the concrete domain is the Boolean algebra ℘(ℤ). In this case the sets of integers ≠ 0 represents the implication ≥ 0 →> 0, which, according to the law p → q = ¬p ∨ q, is ¬ ≥ 0 ∪ > 0.

[figure: •; •; •; •; ℤ; ≥ 0; > 0; ≠ 0]

1Some authors use the term Brouwerian lattice [Birkhoff 1967] or frame [Vickers 1989] to denote some algebras which are slightly different from Heyting algebras. But, in case of complete lattices, all the definitions become equivalent.

ACM Transactions on Programming Languages and Systems, To appear.

Clearly, Heyting algebras include, among others, Boolean algebras which are the models of classical logic [Birkhoff 1967]. As an example of non-Boolean Heyting algebras, consider the lattice depicted below. Note that ≥ 0 →> 0 cannot be described in terms of disjunction and complementation. In particular, the complement ¬ ≥ 0, namely an object d such that d∧ ≥ 0 = ∅ and d∨ ≥ 0 = ℤ, does not exist . However, being an Heyting algebra, ≥ 0 →> 0 still exists, and it is ≠ 0.

[figure: •; •; •; •; •; ℤ; ≥ 0; > 0; ≠ 0; ∅]

Contribution of this Work. In this article we introduce a new operation for abstract domain refinement, called Heyting completion, and we prove that it provides a precise and clean logical model for reduced cardinal power of domains. The Heyting completion of a domain A corresponds to enhance A with all the above-mentioned implicational objects. Heyting algebras provide here a weak enough generalization of classical implication, and therefore negation, which can be the right basis for giving a comprehensive logical account on a variety of relational information in abstract domains. We show that this fact is true, by proving that Heyting completion provides a logical characterization for a generalization of Cousot’s reduced cardinal power of abstract domains. In particular we prove that the reduced cardinal power of a domain A with respect to a domain B is precisely the Heyting completion of A with respect to B, i.e., the most abstract domain containing a → b with a ∈ A and b ∈ B. Therefore, the domains obtained by reduced cardinal power of any domain with respect to itself gets an immediate and clean logical interpretation as the collection of all intuitionistic formulas built, without nested implication, in the fragment ∧, → of propositional logic. One might think that this result is expected, because Heyting algebras are the models of untyped λ-calculus, and reduced cardinal power of domains is a space of functions. On the contrary, this is quite surprising, because the structure of domains in standard abstract interpretation theory is rather different from domains in standard denotational semantics. As the reader can check from Theorem 5.3, the structure of abstract domains is fully used in the proof. This result has both practical and theoretical consequences in abstract interpretation and static program analysis. Theoretically we establish a strong analogy between well-known domains for relational program analysis and Heyting algebras, which are models of intuitionistic logic and untyped λ-calculus. Practically, we make applicable to reduced cardinal power relevant results in intuitionistic logic, which may be particularly helpful to both characterize the least amount of information which is necessary to construct the reduced cardinal power of domains and provide the domain designer with a number of tools for specifying complex domains from simpler basic ones, directly in terms of the logical properties that their objects have to satisfy. In particular we study the algebraic properties of Heyting completion in relation with the remaining operators introduced in Cousot and Cousot [1979], i.e., reduced product and disjunctive completion. The result is that all the operations introduced in Cousot and Cousot [1979] for systematic domain design can be embedded into an algebra of domain operations, all charac-

ACM Transactions on Programming Languages and Systems, To appear.

terized by a clean logical interpretation, where abstract domains can be specified by simple logic formulas. In this algebraic setting, we study the solutions of implicational domain equations, i.e., equations between abstract domains involving Heyting completion as basic domain constructor. A new family of abstract domains for analysis is introduced as solutions of these equations. These domains are closed under implication construction and represent somehow an upper bound on how much implicational information can be derived systematically from a given domain. We prove that they define precisely the family of abstract domains for which the abstraction function α satisfies one postulate of quantifiers in universal algebra: α(α(a) ∧ b) = α(a) ∧ α(b), for all concrete objects a and b. This result has interesting practical consequences in downward closed domains for analysis of (constraint) logic programs, where conjunction models abstract unification of constraints. Logic programming is a high-level language having a simple declarative semantics, and this is particularly helpful to show practical applications of our theory. We prove that the solutions of these domain equations characterize the domains which are condensing [Langen 1990], i.e., such that the analysis of a goal can be derived from a goal-independent analysis with the same precision as the one obtainable for the same goal in a goal-driven way. Moreover we apply Heyting completion as domain refinement to generalize directional type inference in logic programming. Type inference is general enough to include relevant examples of analyses in logic programs. We prove that the same construction by Heyting completion surfaces most of the well-known applications of type inference, from groundness [Armstrong et al. 1994] to more structured directional types [Aiken and Lakshman 1994; Bronsard et al. 1992]. This approach to directionality by systematic domain refinement has the advantage of being independent from specific applications. It is worth noting that our results, although applied in the context of logic programming, are obtained in the standard theory of abstract interpretation and are therefore independent from the choice of particular programming languages.

Structure of the Article. After some preliminary definitions in Section 2, we define the notion of Heyting completion in abstract interpretation in Section 3. In Section 4 we study the main algebraic and logic properties of Heyting completion with respect to other well-known operations for transforming domains. The main results are in Sections 5 and 7. In Section 5 we prove the equivalence between a generalization of reduced cardinal power and Heyting completion of abstract domains. In Section 7 we characterize the family of domains closed under Heyting completion, and we study the properties of solutions of recursive domain equations involving Heyting and disjunctive completion as basic domain constructors. The application of our operator to directional types, ground dependencies, and condensation in logic program analysis is in Sections 6 and 8. The article ends by addressing related works in Section 9 and further research directions in Section 10.

2. PRELIMINARIES

Throughout the article we assume familiarity with lattice theory (e.g., see Birkhoff [1967] and Davey and Priestley [1990]), closure operators (see Cousot [1978] and Morgado [1960]), and abstract interpretation (see Cousot and Cousot [1977; 1979]).

ACM Transactions on Programming Languages and Systems, To appear.

2.1 Notation and Basic Notions

Let A, B, and C be sets. The powerset of A is denoted by ℘(A). If X ⊆ A, \overline{X} is the set-theoretic complement of X in A. If A is a poset, we usually denote by ≤_{A} the corresponding partial order. The dual of a poset A is denoted by A^{op}. If A is a poset with bottom ⊥ then an element a ∈ A is an atom if a covers ⊥, i.e., a ≠ ⊥ and for all x ∈ A, ⊥ < x ≤ a implies x = a. At(A) denotes the set of atoms in A. A complete lattice A with partial ordering ≤_{A}, least upper bound (lub) ∨_{A}, greatest lower bound (glb) ∧_{A}, least element ⊥_{A}, and greatest element ⊤_{A} is denoted ⟨A, ≤_{A}, ∨_{A}, ∧_{A}, ⊤_{A}, ⊥_{A}⟩. Note that, being A complete, the lub and glb operations are defined on ℘(A) and return an element of A. A complete lattice A is atomic if every element x ∈ A different from ⊥ is the lub of the atoms which precede x, i.e., x = ⋁{a ∈ At(A) | a ≤ x}. Dualatoms and dual-atomicity are defined by duality. If A is a poset and I ⊆ A then ↓ I = {x ∈ A | ∃y ∈ I. x ≤_{A} y}. For x ∈ A, ↓ x is a shorthand for ↓ {x}. ℘^{↓}(A) denotes the set of ideals of A, where I ⊆ A is an ideal if I =↓I. ℘^{↓}(A) is a complete lattice with respect to set-theoretic inclusion, where the join is set union, and the meet is set intersection. We write f : A ⟼ B to mean that f is a total function from A to B. f : A ⟼^{m} B denotes that f is a monotone function. If C ⊆ A then f(C) = {f(x) | x ∈ C}. By g ∘ f we denote the composition λx.g(f(x)). Let ⟨A, ≤_{A}, ∨_{A}, ∧_{A}, ⊤_{A}, ⊥_{A}⟩ and ⟨B, ≤_{B}, ∨_{B}, ∧_{B}, ⊤_{B}, ⊥_{B}⟩ be complete lattices. A function f : A ⟼ B is (co-)additive, denoted f : A ⟼^{a(ca)} B, if for any C ⊆ A, f(∨_{A}C) = ∨_{B}f(C) (f(∧_{A}C) = ∧_{B}f(C)). f is (co-)continuous when the above statement on (co-)additivity holds for chains C only. Ord denotes the proper class of ordinals, where ω ∈ Ord is the first limit ordinal.

2.2 Abstract Interpretation, Galois Connections and Closure Operators

The standard Cousot and Cousot [1977] theory of abstract interpretation is based on the notion of Galois connection. If C and A are posets and α : C ⟼^{m} A, γ : A ⟼^{m} C are such that ∀c ∈ C. c ≤_{C} γ(α(c)) and ∀a ∈ A. α(γ(a)) ≤_{A} a, then we call the quadruple ⟨C, α, A, γ⟩ a Galois connection (G.c.) between C and A. In the setting of abstract interpretation, C and A are called, respectively, concrete and abstract domain, and they are assumed to be complete lattices. If in addition ∀a ∈ A. α(γ(a)) = a, then ⟨C, α, A, γ⟩ is a Galois insertion (G.i.) of A in C. Any G.c. ⟨C, α, A, γ⟩ can be lifted to a G.i. by identifying (in an equivalence class) those objects in A having the same image (meaning) in C. This process is known as reduction of the abstract domain, and the result is an abstract domain containing no redundant objects; namely, different abstract objects denoting the same concrete ones are collapsed into a single object. A reduction of a G.c. ⟨C, α, A, γ⟩ is the G.i. ⟨C, α, α(C), γ⟩. In the following we will always consider abstract domains which are parts of a G.i. If ⟨C, α, α(C), γ⟩ is a G.i. then α(C) is isomorphic to γ(α(C)), and ⟨C, γ ∘ α, γ(α(C)), id⟩ is also a G.i. This allows us to consider only G.i.’s of type ⟨C, ρ, ρ(C), id⟩ with ρ : C ⟼ C: The abstraction function and the abstract domain uniquely determinate each other. Hence, to specify a G.i. ⟨C, ρ, A, id⟩, it suffices to give either the abstraction function ρ (and the abstract domain will be ρ(C)) or an abstract domain A ⊆ C (and the abstraction function is the unique function ρ : C ⟼ C such that ⟨C, ρ, ρ(C), id⟩ is a G.i. and ρ(C) = A).

ACM Transactions on Programming Languages and Systems, To appear.

Cousot and Cousot [1979] observed that an often more practical way of reasoning about abstract domains in abstract interpretation is by closure operators. A function ρ : L ⟼ L is a closure operator on a complete lattice L if it is monotone, idempotent (i.e., ∀x ∈ L. ρ(ρ(x)) = ρ(x)), and extensive (i.e., ∀x ∈ L. x ≤_{L} ρ(x)). The equivalence between G.i. and closure operators is well known (cf. Birkhoff [1967]). In view of this equivalence, abstract domains can be studied independently from the representation chosen for their abstract objects. In the following we briefly recall the relation between G.i. and closure operators. In the rest of the article L is a complete lattice ⟨L, ≤_{L}, ∨_{L}, ∧_{L}, ⊤_{L}, ⊥_{L}⟩ playing the role of the concrete domain. The following result from Cousot and Cousot [1979] will be essential to move from one representation of domains into another.

Theorem 2.1 [Cousot and Cousot 1979]. Let A ⊆ L be a complete lattice and ρ : L ⟼ L. Then the following properties are equivalent.

—⟨L, ρ, A, id⟩ is a G.i.; —ρ is a closure operator such that ρ(L) = A.

We identify with uco(L), the set of all upper closure operators on L, the so-called lattice of abstract interpretations of L (cf. Cousot and Cousot [1977, Section 7] and [1979, Section 8]), i.e., the complete lattice of all possible abstract domains (modulo isomorphic representation of their objects) of the concrete domain L. Thus, in the rest of the article, we often abuse notation and consider an abstract domain and the corresponding closure as the same object, and whenever we say that A is an abstraction of L, we mean that A is isomorphic to ρ(L), for some closure ρ ∈ uco(L). When closures are used to denote abstract domains, they will be denoted as sets, with Latin capital letters. Recall that ρ(L) is a Moore-family of L, i.e., a complete meet-sublattice of L (⊤_{L} ∈ ρ(L), and ρ(L) is completely meet-closed, i.e., for any nonempty Y ⊆ ρ(L), ⋀_{L} Y ∈ ρ(L)). Moreover, any Moore-family of L is the image of some closure operator on L. Note that ρ(L) is not, in general, a complete sublattice of L, since the join in ρ(L) might be different from ∨_{L}. ρ(L) is a complete sublattice of L if and only if ρ is additive. For any X ⊆ L, we denote by ⋏(X) = { ⋀_{L} I | I ⊆ L } the Moore-closure of X, i.e., the least Moore-family of L containing X.

The lattice of abstract interpretations inherits all the relevant algebraic properties of the lattice of all closure operations [Morgado 1960; Ward 1942]. Ward [1942, Theorem 4.2] proved that 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 we have

—ρ ⊑ η if and only if ∀x ∈ L. ρ(x) ≤_{L} η(x), or, equivalently, ρ ⊑ η if and only if

η(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.

It is also known that, for any complete lattice L, uco(L) is dual-atomic, where the dual-atoms are all and only those closures φ_{x} = {⊤, x}, for any x ∈ L \ {⊤}, i.e., if y ≤ x then φ_{x}(y) = x, otherwise φ_{x}(y) = ⊤. We call any φ_{x} simply atomic

ACM Transactions on Programming Languages and Systems, To appear.

closure. All domains in the lattice of abstract interpretations are partially ordered by the ordering on uco(L), which corresponds precisely to the standard order used to compare domains with regard to their precision: A_{1} is more precise than A_{2} (or A_{2} is an abstraction of A_{1}) if and only if A_{1} ⊑ A_{2} in uco(L), which holds if and only if A_{2} ⊆ A_{1}. The top closure λx.⊤ is the top domain {⊤}, which contains no information about L. The bottom closure λx.x is the bottom domain L which is the most precise approximation of L. The lub and glb on uco(L) have therefore the following meaning as operators on domains. Suppose {A_{i}}_{i∈I} ⊆ uco(L): (i) ⊔_{i∈I}A_{i} is the most concrete among the domains which are abstractions of all the A_{i}’s, i.e., ⊔_{i∈I}A_{i} is the least common abstraction of all A_{i}’s; (ii) ⊓_{i∈I}A_{i} is (isomorphic to) the well-known reduced product (basically cartesian product plus reduction) of all the A_{i}’s, or, equivalently, it is the most abstract among the domains (abstracting L) which are more concrete than every A_{i}.

3. DOMAIN REFINEMENT BY COMPLEMENTS

The notions of domain refinement, and its dual operations of domain simplification and domain compression, have been introduced in Filé et al. [1996] and Giacobazzi and Ranzato [1997b] as a generalization of most well-known operations for transforming domains. Intuitively a refinement is any operator performing an action of refinement with respect to the standard ordering of precision, e.g., by adding information to domains; while simplificators and compressors perform the dual action of “taking out” information from domains. The refinement ℜ(A) of a domain A is a new domain which includes more information than A, i.e., ℜ(A) ⊑ A. Moreover a refinement respects the order of precision among domains—if we have more information then we add more information. Therefore a refinement is a reductive and monotone operator on uco(L). Relevant examples of these operators include Cousot and Cousot’s reduced product discussed above [Cousot and Cousot 1979], disjunctive completion [Cousot and Cousot 1979; 1994; 1992; Filé and Ranzato 1998; Jensen 1992], and reduced cardinal power [Cousot and Cousot 1979]; Nielson’s tensor product [Nielson 1985]; Giacobazzi and Ranzato’s dual-Moore-set completion [Giacobazzi and Ranzato 1995], and complete extension [Giacobazzi and Ranzato 1997a], and the open product and pattern completion of Cortesi et al. [1994].

In this section we gradually move from complementation in complete lattices to implication in abstract interpretation. In particular we introduce a new operation for domain refinement by complements. This provides a simple way to determine complementary information in abstract interpretation. As we will see later, this information is fundamental to enhance domains to represent relational information and to supply a logical interpretation of Cousot’s reduced cardinal power of domains.

3.1 Complementary Information in Domains

Given two domain objects a and b, we are interested in characterizing an object c such that, when combined with a, the result is approximated by b, i.e., a ∧ c ≤ b. The following example shows how this operation works on a simple domain for sign analysis.

Example 3.1.1. Consider the following lattice Sign, which is an abstract inter-

ACM Transactions on Programming Languages and Systems, To appear.

pretation of ℘(ℤ), and one of its strict abstractions A, both depicted below. The objects in Sign and A have the obvious meaning as fixpoints of closures on ℘(ℤ). Here − ∈ Sign represents the necessary complementary information which, when combined with + ∈ A, gives ∅ as result.

\begin{matrix}[figure: •; •; •; •; •; ℤ; ≠0; −; +; ∅] & • • • • ℤ ≠0 + ∅ \\ Sign & A \end{matrix}

A simple refinement introducing negative information in domains has been firstly studied in Filé et al. [1996]. This refinement is based on the notion of complement [Birkhoff 1967], viz. a^{∗} is a complement for a in L if a∧_{L}a^{∗} = ⊥_{L} and a∨_{L}a^{∗} = ⊤_{L}. When the complement exists unique for an element a, it summarizes the common information shared by all the elements c such that c ∧_{L} a = ⊥_{L}. However, the previous example shows that the requirement of complementation that a∨_{L}a^{∗} = ⊤_{L} is too strong to enhance the simple domain of signs A (note that − is not the complement for + in Sign). In order to characterize complementary information, we need at least to include those points for which a∧_{L} a^{∗} = ⊥_{L} holds, namely those elements a^{∗} which do not share anything but the bottom with a. We weaken the definition of complementation in two ways. First, by relaxing that a∨_{L}a^{∗} = ⊤_{L}, the above observation boils down to the well-known notion of pseudocomplement, which, when it exists, is unique; indeed a → ⊥_{L} = ⋁_{L} { c | a ∧_{L} c = ⊥_{L} }.^{2} Second, we relativize this notion by considering the pseudocomplement of a relatively to b which, if it exists, is the unique element a → b ∈ L such that for any x ∈ L: a ∧_{L} x ≤_{L} b if and only if x ≤_{L} a → b. Relative pseudocomplements, when they exist, are uniquely given by a → b = ⋁_{L} { c | a ∧_{L} c ≤_{L} b }. In other words, the pseudocomplement of a relative to b exists (and it is given by the above formula) if and only if a ∧_{L} (⋁_{L} { c | a ∧_{L} c ≤_{L} b }) ≤_{L} b. It is worth noting that a → b = ⋁_{L} { c | a ∧_{L} c ≤_{L} b } is always defined in any complete lattice, for every pair of elements a and b. This holds even if L is not relative pseudocomplemented, i.e., when a → b may fail to be the relative pseudocomplement of a and b. Because of this, in the following, when no hypotheses on L are assumed, we denote by a → b simply the object ⋁_{L} { c | a ∧_{L} c ≤_{L} b }. The following properties are straightforward by definition.

Proposition 3.1.2. Let a, b ∈ L.

a → ⊤_{L} = ⊤_{L}  (1)
⊤_{L} → a = a  (2)
⊥_{L} → a = ⊤_{L}  (3)
a ∧ b → a = ⊤_{L}  (4)
a → a ∨ b = ⊤_{L}  (5)

2Note, that while pseudocomplements, when they exist, are always unique, in general we may have infinitely many complements in complemented lattices [Birkhoff 1967].

ACM Transactions on Programming Languages and Systems, To appear.

We extend implication between objects to implication between sets in the obvious way.

Definition 3.1.3. For any A, B ⊆ L, A⟶B = { a → b ∈ L | a ∈ A, b ∈ B }.

The following property is immediate by definition.

Proposition 3.1.4. Let L be a complete lattice. λX, Y.X ⟶Y : ℘(L) ⟼ ℘(L) is argumentwise additive in ⟨℘(L), ⊆⟩.

It is worth noting that in the above definition we do not require any further hypothesis on the structure of L, apart of being a complete lattice. As observed above, although a → b = ⋁_{L} { c | a ∧_{L} c ≤_{L} b } always exists unique in complete lattices, it may in general fail to be the pseudocomplement of a relative to b. The following example shows this phenomenon in a simple lattice combining sign and overflow analysis.

Example 3.1.5. Consider the following simple lattice L for sign and overflow analysis of integer variables, which is an abstract interpretation of the standard lattice for interval analysis in Cousot and Cousot [1977]. In this example, m ∈ ℕ is a constant, playing the role of maxint.

[figure: •; •; •; •; •; •; •; •; ℤ; 0; [−m,−1]; [1,+m]; ∅; [−m,0]; [0,+m]; [−m,+m]]

Note that L is neither distributive, nor pseudocomplemented. If N is the domain depicted below, which is a strict abstraction of L, although being defined, 0 → ∅ = 0 → [1, +m] = [−m, +m] is neither the pseudocomplement of 0 nor the pseudocomplement of 0 relative to [1, +m].

\begin{matrix}[figure: •; •; •; •; ℤ; 0; [1,+m]; ∅] & [figure: •; •; •; •; •; •; ℤ; 0; [1,+m]; ∅; [−m,0]; [−m,+m]] \\ N & N ⟶N \end{matrix}

In the case of [1, +m] → 0 = [1, +m] → ∅ instead, we obtain precisely the relative pseudocomplement which is indeed [−m, 0]. Note that when an object a → b is not the relative pseudocomplement, it still provides an approximation for the information which is complementary to a. In this case, the complementary information for 0, which should be given by the union of the intervals [−m, −1] ∪ [1, +m], is approximated by their convex hull 0 → ∅ = [−m, +m].

ACM Transactions on Programming Languages and Systems, To appear.

[figure: \begin{aligned}(i). & a → a & = ⊤ & (ii). & a ∧ ⊥ & = ⊥ \\ (iii). & (a → b) ∧ b & = b & (iv). & a ∧ (a → b) & = a ∧ b \\ (v). & a → (b ∧ c) & = (a → b) ∧ (a → c) & (vi). & (a ∨ b) → c & = (a → c) ∧ (b → c) \end{aligned}]

Fig. 1. Axioms for Heyting algebras.

3.2 Intuitionistic Implication

Considering the implication a → b as a domain object becomes particularly interesting in case it is properly a relative pseudocomplement, i.e., a ∧ (a → b) ≤ b. Lattices where this always happens, for every pair of objects, are called Heyting algebras. Heyting algebras play a central role in our construction, as they correspond to the models of propositional intuitionistic logic. In fact, meet, join, and relative pseudocomplement of Heyting algebras correspond precisely to conjunction, disjunction, and intuitionistic implication of intuitionistic logic (see Birkhoff [1967]). In this section we recall the notion of Heyting algebra and some of its properties that will be frequently used in the rest of the article.

A complete lattice L is a complete Heyting algebra (cHa) if it is relatively pseudocomplemented, i.e., the pseudocomplement of a relative to b (a → b) exists for every a, b ∈ L. A different (but equivalent) definition of (cHa) is the following: for each X ⊆ L and y ∈ L, y ∧_{L} (⋁_{L} X) = ⋁_{L} { y ∧_{L} x | x ∈ X }, which is the (complete) ∧-distributivity law. From a logical point of view, a complete lattice L is a cHa if we can define an (infix) binary operation → which satisfies, for every a, b, c ∈ L, the equalities in Figure 1. The following proposition recalls some key properties of cHa’s [van Dalen 1994].

Proposition 3.2.1. Let L be a cHa, {b_{i}}_{i∈I} ⊆ L, and a, b, c ∈ L.

(a ∧ b) → c = a → (b → c)  (6)
a → ⋀_{i∈I} b_{i} = ⋀_{i∈I}(a → b_{i})  (7)

Proof of (6). See van Dalen [1994].

Proof of (7). Let a ∈ L and {b_{i}}_{i∈I} ⊆ L. By definition, for any i ∈ I, a ∧ (a → b_{i}) ≤ b_{i}. Therefore we have ⋀_{i∈I}(a ∧ (a → b_{i})) ≤ ⋀_{i∈I} b_{i}. However we have that ⋀_{i∈I}(a ∧ (a → b_{i})) = a ∧ ⋀_{i∈I}(a → b_{i}). Therefore ⋀_{i∈I}(a → b_{i}) ≤ a → ⋀_{i∈I} b_{i}. The other inequality holds because ∀k ∈ I. ⋀_{i∈I} b_{i} ≤ b_{k} implies that ∀k ∈ I. a → ⋀_{i∈I} b_{i} ≤ a → b_{k}. Therefore a → ⋀_{i∈I} b_{i} ≤ ⋀_{k∈I}(a → b_{k}).

3.3 Heyting Completion in Abstract Interpretation

In this section we introduce the notion of Heyting completion which formalizes, in a unique operation on domains, the ideas described above. We extend ⟶ to become a binary domain transformation: given two abstract domains X and Y, this is obtained precisely by the least Moore family (viz. the most abstract domain) containing X ⟶Y.

Definition 3.3.1. Let L be a complete lattice and A, B ∈ uco(L). The Heyting

ACM Transactions on Programming Languages and Systems, To appear.

completion of A with respect to B is ⋏(A⟶B), and it is denoted by A⟶^{⋏}B.

Note that the Heyting completion is defined for every complete lattice. Even if the concrete lattice is not a cHa, ⟶ still captures some complementary information, as shown in Example 3.1.5.

Theorem 3.3.2. Let A ∈ uco(L). λX, Y. X ⟶^{⋏}Y is argumentwise monotonic on uco(L) and λX. A⟶^{⋏}X is reductive on uco(L).

Proof. Monotonicity follows from ⋏ and⟶monotonicity in Proposition 3.1.4. Reductivity in its second argument holds by Eq. (2): for any y ∈ Y, y = ⊤_{L} → y. Since A is a Moore-family, then ⊤_{L} ∈ A and therefore Y ⊆ A → Y ⊆ ⋏(A → Y) =

A⟶^{⋏}Y.

In the following, given an abstract domain X, X ⟶^{⋏}X is called the Heyting completion of X. This is a unary operation which is, by Theorem 3.3.2, monotone and reductive on uco(L). Therefore, the operation of Heyting completion λX. X ⟶^{⋏}X : uco(L) ⟼ uco(L) is a domain refinement in the sense of Filé et al.

[1996] and Giacobazzi and Ranzato [1997b]. Note that, while it is monotonic and reductive, in general it is not idempotent, as shown in next example.

Example 3.3.3. Consider the abstract domain A for sign analysis depicted below, whose concrete domain is ℘(ℤ) and whose objects have an obvious meaning as elements in ℘(ℤ). Note that A⟶A is strictly included in A⟶^{⋏}A, which is strictly included in (A⟶^{⋏}A)⟶^{⋏}(A⟶^{⋏}A).

\begin{matrix}[figure: •; •; •; •; < 0; > 0; ∅; ℤ] & [figure: •; •; •; •; •; •; < 0; > 0; ∅; ≤ 0; ≥ 0; ℤ] \\ A & A⟶A \end{matrix}

\begin{matrix}[figure: •; •; •; •; •; •; •; 0; < 0; > 0; ∅; ≤ 0; ≥ 0; ℤ] & [figure: •; •; •; •; •; •; •; •; 0; < 0; > 0; ∅; ≤ 0; ≥ 0; ℤ; ≠ 0] \\ A⟶^{⋏}A & (A⟶^{⋏}A)⟶^{⋏}(A⟶^{⋏}A) \end{matrix}

4. ALGEBRAIC PROPERTIES

In this section we show some basic algebraic properties of Heyting completion with respect to other operations for domain manipulation. To this aim, we embed the lattice of abstract domains uco(L) into an algebra with primitive operators for domain refinement. In particular, we consider the meet operation (⊓) of closure

ACM Transactions on Programming Languages and Systems, To appear.

operators, which is (isomorphic to) the well-known reduced product [Cousot and Cousot 1979] of abstract domains, the operation for disjunctive completion (⋎) [Cousot and Cousot 1979; 1994; Giacobazzi and Ranzato 1996], and the above Heyting completion of abstract domains. As we will see, in most cases, the algebraic properties Heyting completion are direct consequences of analogous logical properties of intuitionistic implication.

4.1 Heyting Completion and Reduced Product

Reduced product was introduced in Cousot and Cousot [1979] as the basic operation for combining domains by including conjunction of domain objects in the refined domain. The following properties hold on generic complete lattices.

Proposition 4.1.1. Let L be a complete lattice, and A, B, C ∈ uco(L).

a. A⟶^{⋏}{⊤_{L}} = {⊤_{L}}

b. {⊤_{L}}⟶^{⋏}A = A

c. {⊤_{L}, x}⟶^{⋏}A = A if x ∈ L and x ≤_{L} ⊥_{A}

d. (A⟶^{⋏}C) ⊓ (B ⟶^{⋏}C) = ⋏((A ∪ B)⟶C)^{3}

Proof.

a. By Eq. (1), ∀a ∈ A. a → ⊤_{L} = ⊤_{L}.

b. By Eq. (2), ∀a ∈ A. ⊤_{L} → a = a.

c. By Eq. (4), ∀a ∈ A. x → a = (x ∧ a) → a = ⊤_{L}.

d. By definition of ⊓, we have to prove that

⋏((A⟶^{⋏}C) ∪ (B ⟶^{⋏}C)) = ⋏((A ∪ B)⟶C).

By Lemma 3.1.4 (A ∪ B)⟶C = (A⟶C) ∪ (B ⟶C) ⊆ A⟶^{⋏}C ∪ B ⟶^{⋏}C,

and therefore ⋏((A ∪ B)⟶C) ⊆ ⋏((A⟶^{⋏}C) ∪ (B ⟶^{⋏}C)). By monotonicity A⟶C ⊆ (A ∪ B)⟶C, and therefore, A⟶^{⋏}C ⊆ ⋏((A ∪ B)⟶C). Similarly,

B ⟶^{⋏}C ⊆ ⋏((A ∪ B)⟶C) and (A⟶^{⋏}C) ∪ (B ⟶^{⋏}C) ⊆ ⋏((A ∪ B)⟶C). By

monotonicity and idempotency of ⋏ we conclude the proof.

Complete Heyting algebras play a central role in our construction, as they correspond precisely to the models of propositional intuitionistic logic. Let L be a cHa. From a logical point of view, the Heyting completion of a domain is the collection of all intuitionistic formulas built with the ∧ and → connectives, without nested implication. Hence, A⟶^{⋏}A is the most abstract domain containing all the intuitionistic implications a → b for a, b ∈ A. The following results are consequences of the basic logical properties of implication in cHa.

Proposition 4.1.2. Let L be a cHa and A, B_{i}, C ∈ uco(L) with i ∈ I.

a. A⟶^{⋏}⨅_{i∈I} B_{i} = ⨅_{i∈I}(A⟶^{⋏}B_{i})

b. (A ⊓ B)⟶^{⋏}C = A⟶^{⋏}(B ⟶^{⋏}C)

c. A⟶^{⋏}⋏(X) = ⨅_{x∈X} A⟶^{⋏}{⊤_{L}, x} if X ⊆ L.

3Note that A ∪ B may not be, in general, a Moore-family, and A ⊓ B = ⋏(A ∪ B).

ACM Transactions on Programming Languages and Systems, To appear.

Proof.

a. A⟶^{⋏}⨅_{i∈I} B_{i} ⊇ ⨅_{i∈I}(A⟶^{⋏}B_{i}) is straightforward by monotonicity of⟶^{⋏}and reduced product. Assume that x ∈ A⟶⨅_{i∈I} B_{i}. x has the form a → ⋀_{j∈J} b_{j} where b_{j} ∈ ∪_{i∈I}B_{i}. By Eq. (7): a → (⋀_{j∈J} b_{j}) = ⋀_{j∈J}(a → b_{j}). We show that for each j ∈ J, a → b_{j} ∈ ⨅_{i∈I}(A⟶^{⋏}B_{i}). Since b_{j} ∈ ∪_{i∈I}B_{i}, there exists B_{k}, k ∈ I, such that b_{j} ∈ B_{k}. It follows that a → b_{j} ∈ A⟶^{⋏}B_{k} and thus a → b_{j} ∈ ⨅_{i∈I}(A⟶^{⋏}B_{i}). The result follows from the fact that ⨅_{i∈I}(A⟶^{⋏}B_{i}) is a Moore family, and therefore ⋀_{j∈J}(a → b_{j}) ∈ ⨅_{i∈I}(A⟶^{⋏}B_{i}).

b. From Eq. (7), it follows that

a → ( ⋀_{j∈J}(b_{j} → c_{j})) = ⋀_{j∈J}(a → (b_{j} → c_{j})) = ⋀_{j∈J}((a ∧ b_{j}) → c_{j})

which proves that A⟶^{⋏}(B ⟶^{⋏}C) ⊆ (A ⊓ B)⟶^{⋏}C.

For the other inclusion, by Eq. (6), it follows

⋀_{i∈I,j∈J}(a_{i} ∧ b_{j}) → c = (⋀_{i∈I}(a_{i}) ∧ ⋀_{j∈J}(b_{j})) → c = ⋀_{i∈I}(a_{i}) → ( ⋀_{j∈J}(b_{j}) → c).

c. One inclusion is straightforward by ⟶^{⋏} and ⊓ monotonicity, and because,

for any x ∈ X: ⋏(X) ⊑ {⊤_{L}, x}. We prove A⟶^{⋏}⋏(X) ⊆ ⊓_{x∈X}A⟶^{⋏}{⊤_{L}, x}.

Let x ∈ A⟶⋏(X). Then x has the form a → ⋀_{i∈I} b_{i} for some set I, a ∈ A and {b_{i}}_{i∈I} ⊆ X. By Eq. (7), a → ⋀_{i∈I} b_{i} = ⋀_{i∈I}(a → b_{i}), and by definition

a → b_{i} ∈ A⟶^{⋏}{⊤_{L}, b_{i}} for any i ∈ I.

As observed above, any abstract interpretation A of a concrete domain L, i.e., A ∈ uco(L), can be always decomposed into atomic domains of the form {⊤_{L}, x} for x ∈ A. In order to use the above result for decomposing the Heyting completion into the completion of simpler domains, we consider lattices generated by some suitable strict subsets of their points. Let L be a complete lattice, and A ∈ uco(L). We say that A is generated by the set B ⊆ A if A = ⋏(B). Hence, by (c) in Proposition 4.1.2, Heyting completion can be constructed from atomic domains, i.e., closures of the form { ⊤_{L}, x }, by considering only the elements x in a generating set X. This is particularly important for domains generated by meet-irreducible elements. An element x of a complete lattice L is completely meet-irreducible if ∀Y ⊆ L. x = ⋀_{L} Y ⇒ x ∈ Y. MIrr(L) denotes the set of completely meetirreducible elements of L (⊤_{L} ∉ MIrr(L)). Most domains in semantics are generated by their meet-irreducible elements. They include algebraic [Birkhoff 1967; Davey and Priestley 1990] and collecting domains of the form ℘(S) for some set S, which are typical domains in collecting semantics and analysis (e.g., see Cousot and Cousot [1994], Jones and Søndergaard [1987], and Mycroft and Nielson [1983]). In the case of algebraic domains, the set of meet-irreducible elements is the least set generating the domain (cf. Birkhoff [1967]). It is therefore immediate by (c) in Proposition 4.1.2 that, if B ∈ uco(L) is algebraic and L is cHa, then the following statement holds:

A⟶^{⋏}B = ⨅_{x∈MIrr(B)} A⟶^{⋏}{⊤_{L}, x}  (8)

This result can be improved by noting that the implications with meet-irreducible elements of L on the right side are always reduced, i.e., if b ∈ MIrr(L)∩B then a → b ∈ B. Therefore, we can get rid of them in our decomposition. The following result characterizes the new information added to B, by A⟶^{⋏}B, in terms of the meetirreducible elements in B. Note that, in general, it does not hold that MIrr(B) = MIrr(L) ∩ B, but MIrr(B) ⊇ MIrr(L) ∩ B.

Proposition 4.1.3. If L is cHa and B ∈ uco(L) is algebraic, then

A⟶^{⋏}B = B ⊓ ( ⨅_{x∈MIrr(B)\MIrr(L)} A⟶^{⋏}{⊤_{L}, x}) .

Proof. We show that for every a ∈ A and b ∈ MIrr(L) ∩ B it holds a → b = b or a → b = ⊤. The result then follows by Eq. (8). Let a ∈ A and b ∈ MIrr(L) ∩ B. If a ≤ b then a → b = ⊤. Suppose a ≰ b. Then we have

a ∧ a → b ≤ b ⇒ (a ∧ a → b) ∨ b = b
⇒ (a ∨ b) ∧ (a → b ∨ b) = b
⇒ (a ∨ b) ∧ a → b = b.

Since b ∈ MIrr(L), then either b = a ∨ b or b = a → b holds. By hypothesis, a ≰ b. Therefore b = a → b.

4.2 Heyting Completion and Disjunctive Completion

In this section we study the relation between Heyting and disjunctive completion in abstract interpretation. Disjunctive completion was introduced in Cousot and Cousot [1979] to express merge over all paths data-flow analysis in fixpoint form. The idea is to lift a given abstract domain A to the most abstract domain which includes A and which is a complete (join-) sublattice of L, viz. no approximation is induced in the disjunctive completed domain by considering the join (i.e., disjunction) of abstract objects. The disjunctive completion of A is defined as the most abstract domain which is an additive closure and includes A (cf. Cousot and Cousot [1979] and Giacobazzi and Ranzato [1996]): ⋎(A) = ⊔{ X ∈ uco(L) | X ⊑ A and X is additive }. A domain A is disjunctive if ⋎(A) = A. The following result specifies the disjunctive completion of an abstract domain A when the concrete domain is either completely distributive or a cHa with A finite.

Proposition 4.2.1. If L is completely distributive or L is a cHa and A is finite, then ⋎(A) = { ⋁_{L} X |X ⊆ A}.

Proof. If L is completely distributive, the result is immediate. Assume L to be a cHa and A to be finite. Therefore ⋎(A) is finite too. Thus we only need to prove that for each X, Y ⊆ A, (⋁_{L} X) ∧ (⋁_{L} Y) ∈ ⋎(A). Being X and Y finite, the thesis follows by L distributivity.

The next result follows immediately from the logical properties of intuitionistic implication, and it specifies the relation between Heyting and disjunctive completion.

Proposition 4.2.2. If L is completely distributive or L is a cHa and A is finite,

then ⋎(A)⟶^{⋏}B = A⟶^{⋏}B.

ACM Transactions on Programming Languages and Systems, To appear.

Proof. Assume L to be completely distributive or L to be a cHa and A to be finite. Let a ∈ ⋎(A)⟶B. By Proposition 4.2.1, there exists X ⊆ A such that a = ⋁_{L} X → b. If L is a cHa and A is finite, then X is finite too, and the result follows by L distributivity; otherwise, because if L is complete distributive then ⋁_{L} X → b = ⋀_{x∈X} x → b from which follows the thesis.

The inverse operation to disjunctive completion, which is called least disjunctive basis, was introduced in Giacobazzi and Ranzato [1996] to characterize the least amount of information which is necessary to construct a given domain by disjunctive completion. Given an abstract domain A, the idea is to find the most abstract domain X (when it exists) such that ⋎(A) = ⋎(X). This domain, denoted Ω(A), is such that A ⊑ Ω(A). Giacobazzi and Ranzato [1996] proved that Ω(A) exists under some hypotheses, e.g., when L or A are finite, or when L^{op} is a completely distributive algebraic lattice. In this case, if JIrr(A) denotes the set of points in A which are completely join irreducible in L, i.e., JIrr(A) = { x ∈ A | ∀Y ⊆ A. x = ⋁_{L} Y ⇒ x ∈ Y }, then Ω(A) = ⋏(JIrr(A)). The following result, which is a consequence of Proposition 4.2.2, specifies the relation between Heyting completion and the least disjunctive bases operation.

Corollary 4.2.3. If L^{op} is a completely distributive algebraic lattice or L is a cHa and A is finite, then A⟶^{⋏}B = Ω(A)⟶^{⋏}B.

This result specifies that A⟶^{⋏}B can be obtained by considering the more abstract, and hence less expensive, domain Ω(A). This provides a systematic method to simplify the construction of Heyting completions of abstract domains, because the implicational objects generated by combining disjunctive objects in A, i.e., those objects x → b where x ∈ A is such that there exists C ⊆ A and x = ⋁_{L} C, can be fully reconstructed by conjunction of relative pseudocomplements of the form c → b, with c ∈ C. Here, the least disjunctive basis plays the role of the least domain generating A by disjunctive completion. By combining the above result with Proposition 4.1.3 we obtain the following result:

A⟶^{⋏}B = B ⊓ ( ⨅_{x∈MIrr(B)\MIrr(L)} Ω(A)⟶^{⋏}{⊤_{L}, x})

This result may be useful to implement Heyting completion of abstract domains, from the most abstract domains as arguments. Note that the implementation of the Heyting completion A⟶^{⋏}B involving the least disjunctive basis of A and an atomic decomposition of B requires a lower number of reductions to identify pairs a → b having the same meaning. The following corollary is immediate by the above observations and can be applied in any cHa to represent the Heyting completion of any finite domain.

Corollary 4.2.4. If L is collecting or L is a cHa and A is finite, then

A⟶^{⋏}A = ⋏(A ∪ (JIrr(A)⟶(MIrr(A) \ MIrr(L)))).

It is known that it is always possible to represent any complete lattice in terms of the set of its join and meet-irreducible elements, and this yields the so-called

ACM Transactions on Programming Languages and Systems, To appear.

concept representation of lattices. According to this reconstruction of lattices (cf. Davey and Priestley [1990]), a complete lattice L is always isomorphic to the collection of all pairs (A, B) such that A ⊆ JIrr(L), B ⊆ MIrr(L), and B = { m ∈ MIrr(L) | ∀j ∈ A. j ≤_{L} m } and A = { j ∈ JIrr(L) | ∀m ∈ B. m ≤_{L} j }, ordered by set inclusion: (A_{0}, B_{0}) ≤ (A_{1}, B_{1}) if A_{0} ⊆ A_{1}, or equivalently B_{1} ⊆ B_{0}. Because JIrr(L) and MIrr(L) can be logarithmic in the size of L, this representation can be very efficient for finite lattices. Moreover, as shown in Freese et al. [1995], most known representations for lattices, e.g., by representing the ≤-relation, can be transformed into a concept representation in O(n^{5/2}), with n = |L|. Therefore, in view of the above results, the theory of concept lattices can be particularly helpful to provide efficient representation for finite domains and their Heyting completion. In order to represent the domain A⟶^{⋏}A it is therefore sufficient to consider pairs in the concept representation of A, i.e., elements in JIrr(A)⟶MIrr(A) \ MIrr(L). This representation is particularly efficient when A = ℘(S), for some set S, and A is a disjunctive domain. In this case an upper bound to the number of elements in A⟶A is not |A|^{2}, but 2|A|, because |Ω(A)| = log(|A|), A = ⋏({ S \ { x } | x ∈ S }), and |{ S \ { x } | x ∈ S }| = log(|A|).

5. REDUCED CARDINAL POWER AND HEYTING COMPLETION

Reduced cardinal power has been introduced by Cousot and Cousot [1979] in the very last section of their POPL’79 paper. The idea is that, given a pair of abstract domains A and B, a new, and more concrete domain can be systematically derived by considering the lattice of all monotone mappings from A to B, which is known in lattice theory as the cardinal power with base B and exponent A. The following result is the main result in Cousot and Cousot [1979, Section 10.2].

Theorem 5.1 [Cousot and Cousot 1979]. Let X be a set, and assume that

(℘(X), α_{A}, A, γ_{A}) and (℘(X), α_{B}, B, γ_{B}) to be G.i.’s. Then (℘(X), α, A ⟼^{m} B, γ)

is a G.c. with α = λP. λx. α_{B}(P ∩ γ_{A}(x)).

The reduced cardinal power with base B and exponent A, denoted B^{A}, is the domain A ⟼^{m} B, reduced with respect to concretization (cf. Cousot and Cousot [1979]). Monotone functions are considered equivalent, and therefore reduced, if they represent the same function between the objects of A and B. It is worth noting that the definition given by Cousot and Cousot [1979] strongly depends on the Boolean structure of the complete lattice of assertions, which is always isomorphic to ℘(X), for some set X, and on the properties of set intersection, which is conjunction of assertions in the early definition of Cousot and Cousot [1979]. Given any set P ⊆ X, the function λx. α_{B}(P ∩ γ_{A}(x)) ∈ B^{A} represents, on the base abstract domain B, the way P changes when put in conjunction with objects in the exponent abstract domain A. This construction has been generalized in Giacobazzi and Ranzato [1995], where the weaker hypotheses of cHa on the concrete domain is considered for the existence of reduced cardinal power of domains. We follow this latter more general presentation, and we call dependencies the objects in the reduced cardinal power of domains. If A = ρ_{A}(L) and B = ρ_{B}(L) for ρ_{A}, ρ_{B} ∈ uco(L), a dependency is specified by the function λx ∈ A. ρ_{B}(d ∧_{L} x) : A ⟼ B, with d ∈ L. The set of all such dependencies is the reduced cardinal power B^{A} = { λx ∈ A. ρ_{B}(d ∧_{L} x) | d ∈ L }. The next result extends Theorem 5.1

ACM Transactions on Programming Languages and Systems, To appear.

above to cHa’s and proves that B^{A} refines B.

Theorem 5.2 [Giacobazzi and Ranzato 1998]. Let L be a cHa, A = ρ_{A}(L), and B = ρ_{B}(L) for ρ_{A}, ρ_{B} ∈ uco(L). Then ⟨L, α⃗, B^{A}, γ⃗⟩ is a G.i. where α⃗ = λd ∈ L. (λx ∈ A. ρ_{B}(d ∧_{L} x)). Moreover B^{A} ⊑ B.

The following representation result for dependencies is the main result of this section, and it specifies that reduced cardinal power^{4} is equivalent to Heyting completion. This result proves a strong link between two apparently unrelated domain refinements, namely between domain refinement by reduced cardinal power and domain completion by relative pseudocomplements.

Theorem 5.3. If L is a cHa and A, B ∈ uco(L), then B^{A} = A⟶^{⋏}B.

In order to prove this result we need some additional lemmata to give a representation, in terms of relative pseudocomplements, for dependencies in B^{A}. In the following, given any X ∈ uco(L), we denote by ρ_{X} the corresponding closure operator.

Lemma 5.4. Let L be a cHa and A, B ∈ uco(L). Then, for any d ∈ L we have

λx ∈ A. ρ_{B}(d ∧ x) = λx ∈ A. ρ_{B}( ⋀_{a∈A}(a → ρ_{B}(d ∧_{L} a)) ∧_{L} x).

Proof. It is sufficient to prove that for any d ∈ L, x ∈ A we have

ρ_{B}(d ∧ x) = ρ_{B}( ⋀_{a∈A}(a → ρ_{B}(d ∧_{L} a)) ∧ x).

For any x ∈ A we have, by extensivity of ρ_{B},

∀a ∈ A. d ∧ a ≤ ρ_{B}(d ∧ a)  ⇒ [ by definition of → ]
∀a ∈ A. d ≤ a → ρ_{B}(d ∧ a)  ⇒
d ≤ ⋀_{a∈A}(a → ρ_{B}(d ∧_{L} a))  ⇒ [ left monotony of ∧ ]
d ∧ x ≤ ⋀_{a∈A}(a → ρ_{B}(d ∧_{L} a)) ∧ x  ⇒ [ monotony of ρ_{B} ]
ρ_{B}(d ∧ x) ≤ ρ_{B}(⋀_{a∈A}(a → ρ_{B}(d ∧_{L} a)) ∧ x).

For the other part we have, for any x ∈ A,

⋀_{a∈A}(a → ρ_{B}(d ∧_{L} a)) ≤ x → ρ_{B}(d ∧ x)  ⇒
⋀_{a∈A}(a → ρ_{B}(d ∧_{L} a)) ∧ x ≤ (x → ρ_{B}(d ∧ x)) ∧ x ≤ ρ_{B}(d ∧ x) ⇒
ρ_{B}(⋀_{a∈A}(a → ρ_{B}(d ∧_{L} a)) ∧ x) ≤ ρ_{B}(d ∧ x).

Lemma 5.5. Let L be a cHa and A, B ∈ uco(L). For any d ∈ L we have

γ⃗(λx ∈ A. ρ_{B}(d ∧_{L} x)) = ⋀_{a∈A}(a → ρ_{B}(d ∧_{L} a)).

Proof. Let b = ⋀_{a∈A}(a → ρ_{B}(d ∧_{L} a)). By Lemma 5.4 λx ∈ A. ρ_{B}(d ∧_{L} x) = λx ∈ A. ρ_{B}(b ∧_{L} x). Now we prove that b is the most abstract object with this

4In the following we call reduced cardinal power the generalization of Cousot’s reduced cardinal power made in Giacobazzi and Ranzato [1995].

ACM Transactions on Programming Languages and Systems, To appear.

property. Let f ∈ L be such that λx ∈ A. ρ_{B}(d ∧_{L} x) = λx ∈ A. ρ_{B}(f ∧_{L} x). Then

∀x ∈ A. f ∧ x ≤ ρ_{B}(f ∧ x)  ⇒ [ because ρ_{B}(d ∧ x) = ρ_{B}(f ∧ x) ]
∀x ∈ A. f ∧ x ≤ ρ_{B}(d ∧ x)  ⇒
∀x ∈ A. f ≤ x → ρ_{B}(d ∧ x)  ⇒
f ≤ ⋀_{a∈A}(a → ρ_{B}(d ∧_{L} a)) = b.

We are now in the position to give the proof of Theorem 5.3.

Proof of Theorem 5.3. Let A, B ∈ uco(L). By Lemma 5.5 we know that

B^{A} = { ⋀_{a∈A}(a → ρ_{B}(d ∧_{L} a)) | d ∈ L }.

Hence B^{A} ⊆ A⟶^{⋏}B. We prove that A⟶^{⋏}B ⊆ B^{A}. Let a → b ∈ A⟶B. We show that a → b = ⋀_{x∈A}(x → ρ_{B}(a → b ∧_{L} x)), which implies, by Lemma 5.5, that a → b ∈ B^{A}. By Lemma 5.5, for any d ∈ L, d ≤ ⋀_{x∈A}(x → ρ_{B}(d ∧_{L} x)) (since d ≤ γ⃗(α⃗(d))). Thus a → b ≤ ⋀_{x∈A}(x → ρ_{B}(a → b ∧_{L} x)). For the other part, for any a ∈ A, b ∈ B we have

a → b ∧ a ≤ b  ⇒ [ because ρ_{B} is monotone and b ∈ B ]
ρ_{B}(a → b ∧ a) ≤ b  ⇒ [ because → is right-monotone ]
a → ρ_{B}(a → b ∧ a) ≤ a → b.

Hence, because a ∈ A, we have that for any b ∈ B

⋀_{x∈A}(x → ρ_{B}(a → b ∧_{L} x)) ≤ a → ρ_{B}(a → b ∧ a) ≤ a → b.

6. APPLICATIONS I: DIRECTIONALITY IN LOGIC PROGRAM ANALYSIS

In this section we apply Heyting completion to systematic design of domains for relational analysis in logic programming. In particular we prove that Heyting completion surfaces most domains and applications aimed to detect directional information in type and groundness analysis.

We fix a first-order language L, with variables ranging in V. The set of terms and idempotent substitutions, viz. mappings from V to terms in L, are denoted respectively T_{L} and Sub. Objects in T_{L} and Sub are partially ordered by instantiation: a ≤ b if and only if ∃θ ∈ Sub. a = bθ. For any syntactic object s, var(s) denotes the set of its variables.

6.1 Directionality in Type Inference

In this section we consider the problem of inferring types in logic programs by abstract interpretation. Given a domain for (basic) type analysis, we show that its Heyting completion captures precisely the notion of directionality among types and, more in general, how this construction surfaces directionality in any property closed under instantiation. In this case, Heyting completion supplies a domain for type inference, including the same relational information between types as traditionally obtained in standard directional type checking by verification methods (e.g., see Aiken and Lakshman [1994]).

The operational semantics of a logic program P, viz. a finite set of Horn clauses in L, is defined by SLD-resolution (cf. Apt [1990]). If G is a goal, viz. a conjunction

ACM Transactions on Programming Languages and Systems, To appear.

of atoms in L, then we write G ⟶^{ϑ}_{P}^{∗} □ if and only if ϑ ∈ Sub is a computed answer substitution for G in P. As usual (cf. Aiken and Lakshman [1994]) a type is a set of terms closed under substitution . Hence, the concrete domain in which we interpret types is ℘^{↓}(T_{L}). An (abstract) domain of types T is therefore any abstraction of ℘^{↓}(T_{L}), i.e., any element in uco(℘^{↓}(T_{L})).

A type for a predicate p of arity n is an n-tuple of types. In the following, for the sake of simplicity, we assume that all predicates in the program have the same arity n, and abuse T_{L} to denote n-tuples of terms. A directional type for a predicate p has the form ⟨I, O⟩ where I and O are types for p. The type I is the “input” type, and type O is the “output” type of p. A predicate p has type ⟨I, O⟩ in a program P (denoted p ∈ ⟨I, O⟩) if for any goal p(t̄), t̄ ∈ I ⇒ θ(t̄) ∈ O for any answer substitution θ (cf. Aiken and Lakshman [1994]). The next result relates the Heyting completion refinement to the notion of directional type. The idea is to prove that an implicational type τ_{1} → τ_{2} ∈ T ⟶^{⋏}T models exactly the above notion of directional type ⟨τ_{1}, τ_{2}⟩.

Theorem 6.1.1. Let P be a program, T be a domain of types, τ_{1}, τ_{2} ∈ T , and p be a predicate. Then the following equivalence holds.

(∀θ. p(X̄) ⟶^{θ}_{P}^{∗} □ ⇒ X̄θ ∈ τ_{1} → τ_{2}) ⇔ (∀t̄∈ τ_{1}.∀σ. p(t̄) ⟶^{σ}_{P}^{∗} □ ⇒ t̄σ ∈ τ_{2})

Proof. Assume that

∀θ. p(X̄) ⟶^{θ}_{P}^{∗} □ ⇒ X̄θ ∈ τ_{1} → τ_{2}.  (9)

We prove that

∀t̄∈ τ_{1}.∀σ. p(t̄) ⟶^{σ}_{P}^{∗} □ ⇒ t̄σ ∈ τ_{2}.  (10)

Let t̄ ∈ τ_{1} and σ ∈ Sub such that p(t̄) ⟶^{σ}_{P}^{∗} □. Let X̄ be new variables, not contained in t̄σ. Let α such that t̄σ = X̄α (it exists since X̄ are new variables). By definition of ⟶_{P}^{∗}, there exists a substitution β such that α ≤ β and p(X̄) ⟶^{β}_{P}^{∗} □. By (9), X̄β ∈ τ_{1} → τ_{2}. Since t̄ ∈ τ_{1} and τ_{1} is closed under instantiation, it follows that t̄σ ∈ τ_{1}. Moreover t̄σ = X̄α ≤ X̄β. Therefore, from X̄β ∈ τ_{1} → τ_{2}, it follows that t̄σ ∈ τ_{2}.

For the other direction, assume (10), and let θ ∈ Sub such that p(X̄) ⟶^{θ}_{P}^{∗} □. In order to prove that X̄θ ∈ τ_{1} → τ_{2}, we have to show that for every instance t̄ of X̄θ such that t̄ ∈ τ_{1}, then t̄ ∈ τ_{2}. From p(X̄) ⟶^{θ}_{P}^{∗} □ it follows that p(t̄) ⟶^{ϵ}_{P}^{∗} □. Therefore, by (10), t̄∈ τ_{2}.

Corollary 6.1.2. In the hypothesis of Theorem 6.1.1, p has type τ_{1} → τ_{2} in

T ⟶^{⋏}T if and only if p ∈ ⟨τ_{1}, τ_{2}⟩.

Clearly, the domain T ⟶^{⋏}T is still closed under instantiation. Directional types in T ⟶^{⋏}T , that satisfy the theorem above, can be obtained by abstract interpretation, with abstract domain T ⟶^{⋏}T , by means of any bottom-up/top-down analyzer which is able to approximate correct or even computed answer substitutions (e.g., see Barbuti et al. [1993] and Bruynooghe [1991]).

Example 6.1.3. Consider the program P = { p(X, X)., r(2, Y) : −p(2, Y). } and the following simple domain of basic types T , where symbols I (integer) and B (Boolean) have the obvious meaning as fixpoints of a closure operator on ℘^{↓}(T_{L}).

ACM Transactions on Programming Languages and Systems, To appear.

[figure: •; (⊥, ⊥); •; (I, I); •; (I, B); •; (B, I); •; (B, B); •; (I, ⊤); •; (⊤, I); •; (⊤, B); •; (B, ⊤); •; (⊤, ⊤)]

A standard type inference which can be obtained from the above domain of types T returns the following type patterns: { p(⊤, ⊤), r(I, ⊤) }. Although correct, this result is not satisfactory. This is due to the fact that the domain T is not able to represent the property that both arguments of the predicate p have the same type. Instead, this information can be expressed in the refined domain T ⟶^{⋏}T . Since the concrete domain is ℘^{↓}(T_{L}), it is easy to prove that we have an explicit definition for the element a → b, i.e., a → b = { t ∈ T_{L} | ∀t′ ≤ t. t′ ∈ a ⇒ t′ ∈ b }. For example (I, ⊤) → (I, I) = { t | ∀t′ ≤ t. t′ ∈ (I, ⊤) ⇒ t′ ∈ (I, I) }, which intuitively denotes the set of pairs of terms such that, for any instance, whenever the first term of the instance is an integer, then the second term of the instance is an integer too. In the domain T ⟶^{⋏}T , we can express the missing property in terms of suitable conjunctions of directional types. Let us denote by p(τ, τ) the conjunction ⋀_{(τ_{1}, τ_{2})∈T} p(τ_{1}, τ_{2}) → p(τ_{1} ∩ τ_{2}, τ_{1} ∩ τ_{2}), i.e., p(I, ⊤) → p(I, I) ∧ p(⊤, I) → p(I, I) ∧ p(B, ⊤) → p(B, B) ∧ p(⊤, B) → p(B, B) ∧ p(I, B) → p(⊥, ⊥) ∧ p(B, I) → p(⊥, ⊥). The implicational objects in p(τ, τ) force both arguments of p to have the same type, by assigning them the common (most precise) type, which is precisely type intersection. By abstract interpretation in the refined domain T ⟶^{⋏}T , we therefore obtain the more precise type patterns: { p(τ, τ), r(I, I) }.

6.2 The Essence of Directionality: From Types to Groundness

Giacobazzi and Ranzato [1995] proved that the abstract domain Def [Armstrong et al. 1994], of propositional formulas whose models are closed under intersection, is the reduced cardinal power of a simpler domain for pure groundness introduced by Jones and Søndergaard’s [1987]. Def is a well-known domain for ground dependency analysis which is able to characterize both pure groundness, i.e., whether a variable is instantiated to ground terms during program execution, and the relations between the groundness of different program variables, providing in this sense another clear example of relational analysis.

Let V ar ⊆ V be a finite set, representing the set of interesting variables. Def is traditionally presented as the set of (classic) propositional formulas built on V ar with connectives ∧ and →, whose models are closed under set-intersection. The interpretation of the connectives is the classical one: ϕ ≤ ψ if and only if ψ is a logical consequence of ϕ. We say that I ⊆ V ar is a model for ϕ, denoted I ⊧ ϕ, if ϕ is true in the interpretation which assigns true to all the variables in I and false to the other ones [Armstrong et al. 1994]. For the sake of simplicity we write θ grounds ϕ to denote { x ∈ V ar | var(xθ) = ∅ } ⊧ ϕ, for θ ∈ Sub. Because logic programs compute substitutions, the concrete domain

ACM Transactions on Programming Languages and Systems, To appear.

we consider is ℘^{↓}(Sub), which is completely distributive, and therefore a cHa. Def is an abstraction of ℘^{↓}(Sub), and the concretization function is γ_{Def}(ϕ) = { θ ∈ Sub | ∀σ ≤ θ. σ grounds ϕ } (cf. Cortesi et al. [1996]). G is the standard domain for pure groundness analysis introduced by Jones and Søndergaard [1987], which is a strict abstraction of Def, including formulas on V ar with the only connective ∧. G is (isomorphic to) the complete lattice ⟨℘(V ar), ⊇⟩, and it is well known that it enjoys a Galois insertion ⟨℘^{↓}(Sub), γ_{V ar}, G, α_{V ar}⟩, where for any V ⊆ V ar, γ_{V ar}(V) = { θ ∈ Sub | ∀v ∈ V. θ grounds v }. As usual, we identify Def and G with the corresponding closures on ℘^{↓}(Sub): γ_{Def}(Def) and γ_{Def}(G). By applying Theorem 5.3 and a result in Giacobazzi and Ranzato [1995], we immediately obtain a characterization of Def in terms of Heyting completion.

Corollary 6.2.1. Def = G ⟶^{⋏}G.

Proof. In Giacobazzi and Ranzato [1995] it has been proven that Def = G^{G}. The thesis follows by Theorem 5.3.

In view of the observations in Section 6.1, pure groundness G can be viewed as some basic type definition, and ground dependency in Def can be interpreted as directional type inference. The key point here, as well as in directional types, is that the concrete domain is some lattice of ideals, i.e., sets of objects closed under instantiation, which are in general non-Boolean cHa. It is worth noting that a different concrete domain would completely change the interpretation of directionality. Consider the Boolean concrete domain ℘(Sub). If V ar = {x, y} we have the following domain G ⟶^{⋏}G, which differs from the analogous completion Def on the non-Boolean lattice ℘^{↓}(Sub).

\begin{matrix}[figure: •; •; •; •; x; y; x∧y; true] & [figure: •; •; •; •; •; •; •; x↔y; x; y; x∧y; y→x; x→y; true] & [figure: •; •; •; •; •; •; •; (x∧y)∨(¬x∧¬y); x; y; x∧y; ¬y∨x; ¬x∨y; true] \\ G & Def in ℘^{↓}(Sub) & G ⟶^{⋏}G in ℘(Sub) \end{matrix}

While G ⟶^{⋏}G is no longer able to express ground dependencies, it is now able to express negative groundness information. This is because intuitionistic implication is replaced by the classical one. This is a consequence of the peculiar nature of the concrete (collecting) domain, which is a Boolean lattice. In this case, the relative pseudocomplements introduced by Heyting completion provide negation of properties. This is because, in Boolean lattices, a → b = ¬a ∨ b and, for instance ¬x∨y = \overline{γ_{Def}(x)}∪γ_{Def}(y), while this is not the case in complete Heyting algebras. For instance, the empty substitution belongs to ¬x∨y, but it provides no groundness information. Clearly, because the set-theoretic complement of a set closed under instantiation is not, in general, closed under instantiation, then G ⟶^{⋏}G above is not an abstraction of ℘^{↓}(Sub). In this sense, when the concrete domain is ℘(Sub), the analysis obtained from G ⟶^{⋏}G cannot be regarded as a type inference.

ACM Transactions on Programming Languages and Systems, To appear.

7. IMPLICATIONAL DOMAIN EQUATIONS

In the previous sections we have given a logical interpretation to a generalization of Cousot’s reduced cardinal power of domains in terms of Heyting completion. We are now in the position where all the operators defined in Cousot and Cousot [1979], i.e., reduced product, disjunctive completion, and reduced cardinal power, have a clean logical interpretation. In this section we consider these operators, together with the lattice of abstract interpretations, as an algebra of domains A = ⟨uco(L), ⊓, ⋎,⟶^{⋏}⟩, involving conjunctive information by reduced product, disjunctive information by disjunctive completion, and relational information by Heyting completion.

It is natural at this point to ask “What is the structure of domains that can be systematically built with the basic operators defined in Cousot and Cousot [1979], i.e., out of the above algebra A?” In particular, which domains can be specified as solutions of simple domain equations on A using Heyting completion? For instance, the examples in Section 6 have shown that well-known domains for logic program analysis can be constructed by combining the operators in A, and the results in Section 4 may help in simplifying complex formulas involving these operators. As usual in domain theory, the most interesting case is the one of recursive domain equations. The presence of recursion leads us to get a constructive definition for domains which are closed under a suitable combination of properties involving disjunction, conjunction, and implication. Clearly, by definition of abstract domains, i.e., Moore families, any domain is closed by conjunction. Therefore the above equations make sense when they combine disjunctive and Heyting completion. Let A ∈ uco(L) be a given abstract domain of basic properties. We want to design a domain which refines A and is closed under some combination of ⨅, ⋎, and ⟶^{⋏}. Since Heyting completion is the only nonidempotent operator, equations which do not contain Heyting completion always have trivial solutions. For instance, it is immediate to observe that the most abstract solution of X = A ⊓ X is the domain A itself and that the most abstract solution of X = A ⊓ ⋎(X) is ⋎(A), because ⋎ is idempotent. The ultimate goal is therefore to construct domains which are closed with respect to Heyting completion, i.e., which are a fixpoint of the Heyting completion operator.

Given a domain A, we are interested in the most abstract abstract domain X which is more concrete than A, and it is closed under ⟶^{⋏}. This domain can be obtained as the greatest (most abstract) solution of the following recursive domain equation:

X = A ⊓ (X ⟶^{⋏}X)  (11)

We are also interested in the family of domains closed with respect to both Heyting and disjunctive completion. This corresponds to find the greatest (most abstract) solution of the following domain equation:

X = A ⊓ (X ⟶^{⋏}X) ⊓ ⋎(X)  (12)

Therefore, we study recursive domain equations X = F (X), where the right-hand side F (X) is for either A ⊓ (X ⟶^{⋏}X) or A ⊓ (X ⟶^{⋏}X) ⊓ ⋎(X). By Theorem 3.3.2, ⟶^{⋏} is monotone. Moreover, both reduced product and disjunctive completion are monotone operators on uco(L). Therefore X = F (X) has always a greatest

ACM Transactions on Programming Languages and Systems, To appear.

(most abstract) and least (most concrete) solution. Note that the least fixpoint of λX. F (X) is L, which is of little interest being the identity closure λx.x. Therefore, we are mostly interested in the greatest fixpoint of λX. F (X) in uco(L), which exists and can be constructively obtained as the limit of the following transfinite sequence of domains {F_{α}}_{α∈Ord}, all approximating the greatest solution from above:

F_{0} = ⊤
F_{α+1} = F (F_{α})
F_{β} = ⨅_{γ<β} F_{γ} if β is a limit ordinal

Clearly, all refinements built in this way are idempotent for the Heyting completion refinement. The following two sections are devoted to study the solutions of the above equations.

7.1 Heyting Completion Closed Domains

In this section we study the solutions to Eq. (11). The most abstract solution is the greatest fixpoint of λX. A ⊓ (X ⟶^{⋏}X) in uco(L), which can be constructively obtained as the limit of the following transfinite sequence of domains \{A\overrightarrow{α}\}_{α∈Ord}:

A\overrightarrow{0} = ⊤
A\overrightarrow{1} = A
A\overrightarrow{α+1} = A ⊓ A\overrightarrow{α} ⟶^{⋏}A\overrightarrow{α}
A\overrightarrow{β} = ⨅_{γ<β} A\overrightarrow{γ} if β is a limit ordinal

Equation (11) can be presented in different but equivalent ways, as shown in the following theorem.

Theorem 7.1.1. The following equations have the same greatest solution:

—X = A ⊓ (X ⟶^{⋏}X)

—Y = A ⊓ (Y ⟶^{⋏}A)

—Z = Z ⟶^{⋏}A

Proof. Let λX. A ⊓ (X ⟶^{⋏}X), λY. A ⊓ (Y ⟶^{⋏}A) and λZ. Z ⟶^{⋏}A be the re-

finement operators associated to the equations. Let \{X\overrightarrow{α}\}_{α∈Ord}, \{Y\overrightarrow{α}\}_{α∈Ord}, and \{Z\overrightarrow{α}\}_{α∈Ord} be the corresponding sequences of domains built from each operator.

First note that X\overrightarrow{0} = Y\overrightarrow{0} = Z\overrightarrow{0} = ⊤ and for α ≥ 1 it holds that X\overrightarrow{α} ⊑ A, Y\overrightarrow{α} ⊑ A, and Z\overrightarrow{α} ⊑ A. It immediately follows that for each α ∈ Ord we have Y\overrightarrow{α} = Z\overrightarrow{α}. Now we prove by transfinite induction that for each α ∈ Ord we have X\overrightarrow{α} = Y\overrightarrow{α}.

α = 0. X\overrightarrow{0} = Y\overrightarrow{0} = ⊤.

α = 1. X\overrightarrow{1} = Y\overrightarrow{1} = A.

α = 2. X\overrightarrow{2} = Y\overrightarrow{2} = A⟶^{⋏}A.

ACM Transactions on Programming Languages and Systems, To appear.

α = β + 2, β ≠ 0.

X\overrightarrow{α} = A ⊓ (X\overrightarrow{β+1} ⟶^{⋏}X\overrightarrow{β+1})  [ β ≥ 1 ]
= X\overrightarrow{β+1} ⟶^{⋏}X\overrightarrow{β+1}  [ by inductive hypothesis ]

= Y\overrightarrow{β+1} ⟶^{⋏}Y\overrightarrow{β+1}

= Y\overrightarrow{β+1} ⟶^{⋏}(A ⊓ (Y\overrightarrow{β} ⟶^{⋏}A)) [ β ≥ 1 ]
= Y\overrightarrow{β+1} ⟶^{⋏}(Y\overrightarrow{β} ⟶^{⋏}A)  [ by (b) in Prop. 4.1.2 ]
= (Y\overrightarrow{β+1} ⊓ Y\overrightarrow{β})⟶^{⋏}A  [ by monotonicity ]

= Y\overrightarrow{β+1} ⟶^{⋏}A

= Y\overrightarrow{β+2} = Y\overrightarrow{α}

α = β + 1, β limit ordinal.

X\overrightarrow{α} = A ⊓ (X\overrightarrow{β} ⟶^{⋏}X\overrightarrow{β})  [ β ≥ 1 ]
= X\overrightarrow{β} ⟶^{⋏}X\overrightarrow{β}  [ by inductive hypothesis ]

= Y\overrightarrow{β} ⟶^{⋏}Y\overrightarrow{β}

= Y\overrightarrow{β} ⟶^{⋏}⨅_{γ<β} Y\overrightarrow{γ}  [ by (a) in Prop. 4.1.2 ]
= ⨅_{γ<β} Y\overrightarrow{β} ⟶^{⋏}Y\overrightarrow{γ}  [ since γ < β ]
= ⨅_{γ<β} (Y\overrightarrow{β} ⊓ Y\overrightarrow{γ})⟶^{⋏}Y\overrightarrow{γ} [ by (b) in Prop. 4.1.2 ]
= ⨅_{γ<β} Y\overrightarrow{β} ⟶^{⋏}(Y\overrightarrow{γ} ⟶^{⋏}Y\overrightarrow{γ}) [ by inductive hypothesis ]
= ⨅_{γ<β} Y\overrightarrow{β} ⟶^{⋏}(Y\overrightarrow{γ} ⟶^{⋏}A) [ by (b) in Prop. 4.1.2 ]
= ⨅_{γ<β} (Y\overrightarrow{β} ⊓ Y\overrightarrow{γ})⟶^{⋏}A  [ since γ < β ]

= ⨅_{γ<β} Y\overrightarrow{β} ⟶^{⋏}A

= Y\overrightarrow{β} ⟶^{⋏}A  [ β ≥ 1 ]

= A ⊓ (Y\overrightarrow{β} ⟶^{⋏}A)

= Y\overrightarrow{α}

α limit ordinal. Trivial by inductive hypothesis.

The following result characterizes the most abstract solution of Eq. (11). Recall that Heyting algebras are defined in terms of three basic operations: meet, join, and relative pseudocomplement. Because any abstract interpretation is always a meet-sublattice of the concrete domain (cf. Cousot and Cousot [1979]), when L is a cHa, X ⊆ L is a solution for Eq. (11) if and only if the abstract operation of relative pseudocomplementation is precisely the restriction of the concrete one to the elements of X. Hence, when X is a solution of the above recursive domain equation, then X is always a cHa, where only the join operator may differ from the concrete one. Moreover we also characterize the solution of Eq. (11) in terms of its achieved precision. It turns out that the most abstract solution of Eq. (11) is the most abstract domain which includes A, and it is complete for a suitable set of functions. Recall that an abstract domain A, associated with a closure operator ρ_{A} ∈ uco(L), is complete for a function f : L ⟼ L if ρ_{A} ∘ f ∘ ρ_{A} = ρ_{A} ∘ f (see Cousot and Cousot [1979], Giacobazzi and Ranzato [1997a], and Mycroft [1993]). A domain is complete for a family of functions {f_{i}}_{i∈I} if it is complete for all of them.

Theorem 7.1.2. Let L be a cHa, X, A ∈ uco(L), and X ⊑ A. Then the following are equivalent:

a. X is a solution of Eq. (11);

ACM Transactions on Programming Languages and Systems, To appear.

b. X is a subalgebra of L with respect to the relative pseudocomplement; c. X is complete for {λx. c ∧ x}_{c∈X}; d. ρ_{X}(ρ_{X}(a) ∧ b) = ρ_{X}(a) ∧ ρ_{X}(b) for any a, b ∈ L.

Proof. a ⇒ b. Assume that X is a solution of Eq. (11). We have to prove that X is relatively pseudocomplemented and that the relative pseudocomplements computed in X are exactly the relative pseudocomplements in L; that is, for any a, b ∈ X there exists a ⇝ b ∈ X such that ∀c ∈ X. a ∧ c ≤ b ⇔ c ≤ a ⇝ b and a ⇝ b = a → b. This is equivalent to proving that ∀a, b ∈ X. a → b ∈ X and ∀c ∈ X. a ∧ c ≤ b ⇔ c ≤ a → b. Since X is a solution of Eq. (11), X = X ⟶^{⋏}X; therefore a → b ∈ X. By definition of →, it holds that ∀c ∈ L. a ∧ c ≤ b ⇔ c ≤ a → b. The thesis follows because X ⊆ L.

b ⇒ c. Assume that for any a, b ∈ X: a → b ∈ X. We prove that ρ_{X} is complete for the set of functions {λx. c ∧ x}_{c∈X}, namely that for any x ∈ L and c ∈ X, ρ_{X}(c ∧ ρ_{X}(x)) = ρ_{X}(c ∧ x). Let x ∈ L and c ∈ X be fixed. It is obvious that ρ_{X}(c ∧ x) ≤ ρ_{X}(c ∧ ρ_{X}(x)). By hypothesis, c → ρ_{X}(c ∧ x) ∈ X. Moreover, by extensivity, c ∧ x ≤ ρ_{X}(c ∧ x). Therefore, L being a cHa, x ≤ c → ρ_{X}(c ∧ x). By monotonicity and idempotence we have that ρ_{X}(x) ≤ ρ_{X}(c → ρ_{X}(c ∧ x)) = c → ρ_{X}(c ∧ x). Therefore we conclude with the following inequalities:

ρ_{X}(c ∧ ρ_{X}(x)) = ρ_{X}(ρ_{X}(c) ∧ ρ_{X}(x))
= ρ_{X}(c) ∧ ρ_{X}(x)
≤ ρ_{X}(c) ∧ (c → ρ_{X}(c ∧ x))
≤ ρ_{X}(c ∧ x).

c ⇒ a. Assume that X be complete for the set of functions {λx. c ∧ x}_{c∈X}. We prove that for any a, b ∈ X, a → b ∈ X, i.e., ρ_{X}(a → b) = a → b. By extensivity, ρ_{X}(a → b) ≥ a → b. Moreover, L being a cHa, we have that a ∧ a → b ≤ b. By hypothesis, X is complete for the function λx. a ∧ x : L ⟼ L. Therefore we have the following inequalities:

a ∧ ρ_{X}(a → b) ≤ ρ_{X}(a ∧ ρ_{X}(a → b))
= ρ_{X}(a ∧ a → b)
≤ ρ_{X}(b)
= b.

Therefore a ∧ ρ_{X}(a → b) ≤ b which implies that ρ_{X}(a → b) ≤ a → b.

c ⇔ d. Straightforwardly by definition of completeness.

By Theorem 7.1.2, the greatest solution of Eq. (11) is therefore the greatest (i.e., most abstract) domain which contains A and is complete for the set of functions {λx. c∧x}_{c∈X}. Completeness represents the key notion to characterize the solutions of Eq. (11). Completeness here means that no loss of precision is accumulated by abstracting the conjunction of abstract objects with respect to what can be achieved by abstracting only one of its arguments. The notion of least complete extension of a domain has been recently introduced by Giacobazzi and Ranzato [1997a] and Giacobazzi et al. [1998a], where the authors proved that there always exists the (unique) most abstract domain which contains a given domain A and is complete

ACM Transactions on Programming Languages and Systems, To appear.

for any given continuous function f. In this sense, Point (c) in Theorem 7.1.2 can be viewed as an instance of these more general results.

Example 7.1.3. P os is definitely the most widely known and used domain for groundness analysis of logic programs (cf. Armstrong et al. [1994]). P os is traditionally presented as the set of (classic) propositional formulas built on V ar and the constant true, by using the connectives ∧, ∨, →, and ordered by logical implication. P os is an abstraction of ℘^{↓}(Sub) and γ_{P os}(ϕ) = { θ ∈ Sub | ∀σ ≤ θ. σ grounds ϕ } (cf. Cortesi et al. [1996]). With respect to Def, disjunction of variables are allowed in P os. In this sense, P os is strictly more expressive than Def, i.e., Def ⊂ P os.

Consider the simple domain G for groundness analysis defined in Section 6.2. It is proved in Scozzari [1997] that P os = (G ⟶^{⋏}G)⟶^{⋏}G and P os⟶^{⋏}P os = P os. Therefore the domain P os is the greatest solution to the equation: X = G ⊓ (X ⟶^{⋏}X). By exploiting our characterization of Theorem 7.1.2, it turns out that P os is the most abstract domain which is complete for the family of functions {λx. c ∧ x}_{c∈P os}. Recall that the meet operation in P os is precisely abstract unification. Therefore P os represents the most abstract domain where abstract unification is complete, provided that at least one of the arguments belongs to P os.

By Theorem 7.1.2, it is clear that the greatest solution of Eq. (11) is a cHa. The meet and implication operations of the greatest solution are exactly the restriction of the corresponding ones on the concrete domain. Since the greatest solution may fail to be disjunctive, the join in the abstract domain can be different from the concrete one. For the case of groundness analysis, this is coherent with a result by Filé and Ranzato [1994], proving that P os is not disjunctive domain, i.e., P os ≠ ⋎(P os).

It is worth noting that the operator associated with the Eq. (11), λX. A ⊓ (X ⟶^{⋏}X) is not, in general, co-continuous in uco(L), as shown by the following example. Hence ω may not in general be the least closure ordinal for the sequence \{A\overrightarrow{α}\}_{α∈Ord}, i.e., it may well happen that A\overrightarrow{ω} ⊂ A\overrightarrow{ω+1}.

Example 7.1.4. Consider the following complete lattice L = ℕ ∪ {ω, ⊤, c} depicted below, and the family of its abstractions A_{i} ∈ uco(L), such that for any i ∈ ℕ, A_{i} = { n ∈ ℕ | n ≤ i } ∪ {⊤}.

[figure: •; •; •; •; •; •; ω; n; 1; 0; c; ⊤]

{A_{i}}_{i∈ℕ} is a chain, and for any i ∈ ℕ, A_{i} = A_{i} ⟶^{⋏}A_{i}, but ⊓_{i∈ℕ}A_{i} = ℕ ∪ {ω} is not implication closed, since c = 0 → ω ∈ (⊓_{i∈ℕ}A_{i})⟶^{⋏}(⊓_{i∈ℕ}A_{i}). Note that L above is not a cHa. However, unfortunately, it is not co-continuous even if the concrete domain is a Boolean algebra. It is sufficient to consider L = ⟨℘(ω), ω, ∅, ∩, ∪, ⊆⟩, and the chain of domains A_{i} = ⋏(∪_{1≤j≤i}{ ∅, ω, ω \ { i }, { i } }) ∈ uco(℘(ω)), for i ≥ 1. Note that ⊓_{i≥1}A_{i} = ⋏(∪_{i≥1}A_{i}) and { 0 }, ∅ ∈ ⊓_{i≥1}A_{i}, but being ∩-irreducible,

{ 0 } → ∅ = ω \ { 0 } ∉ ⊓_{i≥1}(A_{i} ⟶^{⋏}A_{i}).

ACM Transactions on Programming Languages and Systems, To appear.

Clearly, co-continuity is ensured when L is a finite domain, because uco(L) is finite too, or when uco(L) satisfies the descending chain condition, i.e., it does not contains infinite descending chains. Because uco(L) is a domain of functions, both of these conditions are far too restrictive for a concrete domain in most applications of abstract interpretation, e.g., in static program analysis. However, co-continuity is maintained when the descending chain condition holds on the concrete domain L, as proved by the next result. Note that the operator we want to prove co-continuous is defined on uco(L) and that our condition, in general, does not imply that uco(L) enjoys the descending chain property.

Lemma 7.1.5. Let L be a complete lattice which enjoys the descending chain property and { B_{i} }_{i∈I} ⊆ uco(L) be a chain. Then ⊓_{i∈I}B_{i} = ⋃_{i∈I} B_{i}.

Proof. We know that ⊓_{i∈I}B_{i} = ⋏(⋃_{i∈I} B_{i}). Therefore we have only to prove that ⋃_{i∈I} B_{i} is closed under (possibly infinite) ∧. Let { b_{j} }_{j∈J} ⊆ ⋃_{i∈I} B_{i}. By the descending chain condition, there exists a finite J′ ⊆ J such that ⋀_{j∈J} b_{j} = ⋀_{j∈J′} b_{j} and an index k ∈ I such that ∀j ∈ J′. b_{j} ∈ B_{k} (because J′ is finite). Since B_{k} is in uco(L), it follows that ⋀_{j∈J′} b_{j} ∈ B_{k} and thus ⋀_{j∈J′} b_{j} ∈ ⋃_{i∈I} B_{i}.

Theorem 7.1.6. If L enjoys the descending chain property, λX. A ⊓ (X ⟶^{⋏}X) is co-continuous in uco(L).

Proof. Let { B_{i} }_{i∈I} be a chain in uco(L) and F = λX. A ⊓ (X ⟶^{⋏}X). We have to prove that F (⊓_{i∈I}B_{i}) = ⊓_{i∈I}F (B_{i}). By Lemma 7.1.5 this is equivalent to proving that F (⋃_{i∈I} B_{i}) = ⋃_{i∈I} F (B_{i}). The direction F (⋃_{i∈I} B_{i}) ⊇ ⋃_{i∈I} F (B_{i}) trivially holds. For the other direction, let f ∈ F (⋃_{i∈I} B_{i}). By definition of F, there exist a ∈ A, b_{j}, c_{j} ∈ ⋃_{i∈I} B_{i} for j ∈ J, such that f = a ∧ ⋀_{j∈J}(b_{j} → c_{j}). From the descending chain property, there exists a finite J′ ⊆ J such that ⋀_{j∈J}(b_{j} → c_{j}) = ⋀_{j∈J′}(b_{j} → c_{j}). Let k ∈ I be such that ∀j ∈ J′. b_{j}, c_{j} ∈ B_{k} (such an index exists

since J′ is finite). Hence ⋀_{j∈J′}(b_{j} → c_{j}) ∈ B_{k} ⟶^{⋏}B_{k}. Since f = a∧⋀_{j∈J′}(b_{j} → c_{j})

it follows that f ∈ F (B_{k}) and thus f ∈ ⋃_{i∈I} F (B_{i}).

It is therefore immediate that, under the condition in Theorem 7.1.6, ω is the least closure ordinal, i.e., A\overrightarrow{ω} is the greatest solution of Eq. (11).

7.2 Heyting and Disjunctive Closed Domains

In this section we study the family of domains which are solutions to the equation X = A ⊓ (X ⟶^{⋏}X) ⊓ ⋎(X). This equation characterizes all domains which are closed with respect to both Heyting and disjunctive completion. The following result is an immediate extension of Theorem 7.1.2 to the case of disjunctive solutions.

Theorem 7.2.1. Let L be a cHa, X, A ∈ uco(L), and X ⊑ A. The following statements are equivalent:

—X is a solution of Eq. (12); —X is a solution of Eq. (11) and is disjunctive; —X is a complete Heyting subalgebra of L.

Corollary 7.2.2. If B is a solution of Eq. (12) then B is a solution of Eq. (11).

ACM Transactions on Programming Languages and Systems, To appear.

As before for Eq. (11), also Eq. (12) can be presented in different, but equivalent, ways. The following result is straightforward from monotonicity of all involved operators.

Theorem 7.2.3. The following equations have the same greatest fixpoint:

—X = A ⊓ (X ⟶^{⋏}X) ⊓ ⋎(X)

—Y = A ⊓ ⋎(Y ⟶^{⋏}Y)

—Z = ⋎(A ⊓ (Z ⟶^{⋏}Z))

Example 7.2.4. We keep on Example 7.1.3 and consider the equation

X = G ⊓ (X ⟶^{⋏}X) ⊓ ⋎(X).

Since it has been proven in Scozzari [1997] that ⋎(P os) = ⋎(P os)⟶^{⋏}⋎(P os), it follows that ⋎(P os) is the greatest solution of the above equation.

It is worth noting that Z = Z ⟶^{⋏}A in Theorem 7.1.1 cannot be directly extended by applying disjunctive completion, i.e., by considering the equation X = ⋎(X ⟶^{⋏}A), to obtain the same solutions as Eq. (12) does. The next example shows this phenomenon.

Example 7.2.5. Consider the simple lattice L depicted below and one of its abstractions A. The greatest solution of the equation X = ⋎(X ⟶^{⋏}A) is the domain B, while the greatest solution of the equation X = A ⊓ (X ⟶^{⋏}X) ⊓ ⋎(X) is the domain L itself. Note that while B is still disjunctive, it is not closed by Heyting completion.

\begin{matrix}[figure: •; •; •; •; ℤ; −; +; ∅] & • • ℤ + & • • • ℤ + ∅ \\ L & A & B \end{matrix}

The next result gives a characterization of both generic and most abstract solutions to Eq. (11), under the additional hypothesis that L is a collecting domain and ⊥_{L} ∈ A. Under these hypotheses, Eq’s. (11) and (12) both have the same solutions.

Theorem 7.2.6. Let L = ℘(S) for some set S and A ∈ uco(L), with ⊥_{L} ∈ A.

—A = A⟶^{⋏}A if and only if A is disjunctive and complemented, i.e., A = ⋎(A)

and A⟶^{⋏}{⊤_{L}, ⊥_{L}} ⊆ A;

—⋎(A ⊓ (A⟶^{⋏}{⊤_{L}, ⊥_{L}})) is the most abstract solution for (11) and (12).

Proof. Let A = A⟶^{⋏}A. By monotonicity, A = A⟶^{⋏}A ⊑ A⟶^{⋏}{⊤, ⊥_{L}}. Hence A⟶^{⋏}{⊤_{L}, ⊥_{L}} ⊆ A. We now prove that A is disjunctive. Let { a_{i} }_{i∈I} ⊆ A for some set I. Since A is complemented, then ∀i ∈ I. a_{i} → ⊥_{L} ∈ A. Thus being

ACM Transactions on Programming Languages and Systems, To appear.

A ∈ uco(L), ⋀_{i∈I} (a_{i} → ⊥_{L}) ∈ A. But also ⋀_{i∈I} (a_{i} → ⊥_{L}) → ⊥_{L} ∈ A because A is complemented. Moreover

⋀_{i∈I} (a_{i} → ⊥_{L}) → ⊥_{L} = ¬(⋀_{i∈I} (a_{i} → ⊥_{L})) ∨ ⊥_{L}

= ⋁_{i∈I} (¬(¬a_{i} ∨ ⊥_{L})) ∨ ⊥_{L} = ⋁_{i∈I} ((a_{i} ∧ ¬⊥_{L}) ∨ ⊥_{L}) = ⋁_{i∈I} (a_{i} ∧ ⊤_{L}) = ⋁_{i∈I} a_{i}.

Thus A is closed under (possibly) infinite concrete disjunctions and ⊥_{L} ∈ A. By Proposition 4.2.1 it is a disjunctive domain or equivalently an additive closure.

Now assume A to be complemented and disjunctive. Clearly A ⊆ A⟶A by Theorem 3.3.2, and therefore A = ⋏(A) ⊆ A⟶^{⋏}A. Let a → b ∈ A⟶A. Since L is a Boolean algebra, it holds a → b = ¬a ∨ b = (a → ⊥_{L}) ∨ b. Hence a → b ∈ A because A is complemented and disjunctive. Thus A⟶A ⊆ A, and therefore

A = A⟶^{⋏}A.

Let S be a solution to Eq. (11), i.e., S ⊑ A and S = S ⟶^{⋏}S. We first prove that

S ⊑ ⋎(A ⊓ (A⟶^{⋏}{⊤, ⊥_{L}})).

Note that ⊥_{L} ∈ S, since ⊥_{L} ∈ A ⊆ S. Hence, by the previous point, S = ⋎(S). Moreover, S = S ⟶^{⋏}S ⊑ S ⟶^{⋏}{⊤, ⊥_{L}}. It follows that S = S ⊓ S ⟶^{⋏}{⊤, ⊥_{L}} and S = ⋎(S) = ⋎(S ⊓ S ⟶^{⋏}{⊤, ⊥_{L}}). Since S ⊑ A, by monotonicity, it holds that

S = ⋎(S ⊓ S ⟶^{⋏}{⊤, ⊥_{L}}) ⊑ ⋎(A ⊓ (A⟶^{⋏}{⊤, ⊥_{L}})).

Now we prove that ⋎(A ⊓ A⟶^{⋏}{⊤, ⊥_{L}}) is a solution to Eq. (11). Clearly ⋎(A ⊓ A⟶^{⋏}{⊤, ⊥_{L}}) ⊑ A, and it is trivially disjunctive by construction. Hence we have only to show that it is complemented. Let a ∈ ⋎(A ⊓ A⟶^{⋏}{⊤, ⊥_{L}}). We prove that a → ⊥_{L} ∈ ⋎(A ⊓ A⟶^{⋏}{⊤, ⊥_{L}}). By definition of reduced product, a = ⋁_{i∈I} a_{i} ∧ b_{i} with a_{i} ∈ A and b_{i} ∈ A⟶^{⋏}{⊤, ⊥_{L}}, for some set I. Because L is a Boolean algebra, we have

a → ⊥_{L} = (⋁_{i∈I} a_{i} ∧ b_{i}) → ⊥_{L}
= ¬(⋁_{i∈I} a_{i} ∧ b_{i}) ∨ ⊥_{L}
= (⋀_{i∈I} ¬(a_{i} ∧ b_{i})) ∨ ⊥_{L}
= ⋀_{i∈I}(¬(a_{i} ∧ b_{i}) ∨ ⊥_{L})
= ⋀_{i∈I}(¬a_{i} ∨ ¬b_{i}).

With ⋎(A ⊓ A⟶^{⋏}{⊤, ⊥_{L}}) being a Moore family, we have only to prove that, for

each i ∈ I, ¬a_{i}∨¬b_{i} ∈ ⋎(A ⊓ A⟶^{⋏}{⊤, ⊥_{L}}). Since a_{i} ∈ A and b_{i} ∈ A⟶^{⋏}{⊤, ⊥_{L}},

it follows that ¬a_{i} ∈ A⟶^{⋏}{⊤, ⊥_{L}} and ¬b_{i} ∈ A, because a Boolean algebra is uniquely complemented. Hence ¬a_{i}, ¬b_{i} ∈ A ⊓ A⟶^{⋏}{⊤, ⊥_{L}} and ¬a_{i} ∨ ¬b_{i} ∈

⋎(A ⊓ A⟶^{⋏}{⊤, ⊥_{L}}).

Moreover, ⋎(A ⊓ A⟶^{⋏}{⊤, ⊥_{L}}) being disjunctive, by Theorem 7.2.1, it is the most abstract solution of Eq. (12).

We conclude this section by observing that, from a purely algebraic point of view, the solutions of Eq. (11), and therefore those of Eq. (12), have relevant properties that provide a strong link between abstraction functions and algebraic quantifiers. The above results, together with Point (d) in Theorem 7.1.2, show that the solutions of Eq. (11) are all and only those closures ρ ∈ uco(L) that satisfy the pos-

ACM Transactions on Programming Languages and Systems, To appear.

tulate ρ(ρ(x) ∧ y) = ρ(x) ∧ ρ(y) of quantifiers in universal algebra [Halmos 1962]. This apparently useless observation has instead relevant applications in program analysis. In the case of logic program analysis, for instance, this fact implies that goal-directed and goal-independent analyses are equivalent in precision. The next section provides a domain-theoretic characterization of this phenomenon, which is known in logic program analysis as condensation.

8. APPLICATIONS II: CONDENSATION IN LOGIC PROGRAM ANALYSIS

In this section we prove that, for downward closed properties, the domains which are solutions of the recursive domain equation X = A ⊓ X ⟶^{⋏}X all satisfy the relevant property of being condensing (see Langen [1990] and Marriott and Søndergaard [1993]), and under additional nonrestrictive hypotheses, condensing domains are all and only the solutions of X = A ⊓ X ⟶^{⋏}X. This property gives computational relevance in static program analysis to the results in Section 7 and shows a surprising link between Cousot’s reduced cardinal power of domains and condensation.

The definition of condensation for a domain X ∈ uco(L) can be given with respect to a generic abstract function f^{♯} : X ⟼ X. The following definition is due to Marriott and Søndergaard [1993] and formalizes, for downward closed domains, an idea due to Langen [1990].

Definition 8.1. A domain X ∈ uco(L) is condensing for f^{♯} : X ⟼ X if for any x, y ∈ X: x ∧ f^{♯}(y) = f^{♯}(x ∧ y).

The above property of being condensing is relevant in particular in analysis of downward closed properties, e.g., type inference and groundness of (constraint) logic programs. This is because in this case ∧ plays the role of (abstract) unification of constraints [Langen 1990; Marriott and Søndergaard 1993].

It is well known that, in general, goal-independent analyses of logic programs, like those obtainable with generic bottom-up/top-down analyzers [Barbuti et al. 1993; Bruynooghe 1991; Codish et al. 1994], are less precise than goal-directed ones (cf. Marriott and Søndergaard [1993]). This is because goal-independent analysis can be thought to be an analysis for all possible initial states, while in goal-directed analysis, a given query with a fixed initial state is executed in the abstract domain. In this latter case the result may be refined by knowing in advance the initial calls. More formally, if true represents the top (weakest) constraint, representing any initial store, then, by Definition 8.1, for any constraint c we have c ∧ f^{♯}(true) = f^{♯}(c). The idea here is that computing the semantics of a query with initial constraint c, i.e., f^{♯}(c), is the same as unifying c with the result of the semantics of the same query in the most general environment true, which is f^{♯}(true). This encodes the typical way we derive the analysis of a query in an initial state from a goal-independent analysis: we filter out, by unification, those computations which do not satisfy the given initial state (cf. Barbuti et al. [1993]). Unfortunately, for most domains, this information cannot be derived with the same precision as that obtainable in goal-directed analysis, in particular c ∧ f^{♯}(true) ≥ f^{♯}(c). However, as observed in Langen [1990] and Jacobs and Langen [1992], under the hypothesis that the abstract domain is condensing, no loss of precision is accumulated in deriving information about specific calls from goal-independent analyses.

Consider a simple constraint logic programming (clp) language (cf. Jaffar and

ACM Transactions on Programming Languages and Systems, To appear.

Lassez [1987]). We consider here a ccp-like presentation of clp: processes interact with each other by monotonically refining a common store, which is represented by a set of constraints [Saraswat et al. 1991]. For simplicity we do not consider here any synchronization mechanism, like blocking-ask; therefore processes are only allowed to tell constraints to a global store. Because of this restriction, our language boils down to a standard (nondeterministic) clp language. The syntax of programs is as follows, where P are programs and A are clp-agents:

\begin{aligned}P & ::= & ε | p(x̄) ← A | P.P \\ A & ::= & c | A ∧ A | ∑_{i=1}^{n} A_{i} | p(x̄) \end{aligned}

We abuse by considering programs as (finite) sets of predicate or process declarations, and we assume that each process can be declared in at most one clause of the form p(x̄) ← A. Also, we assume here that Store is a poset of constraints (i.e., a constraint system), ordered by logical implication, including equational constraints. This is a weak enough condition to include most constraint systems developed in the literature (e.g., see Saraswat et al. [1991]). The semantic domain is ℘^{↓}(Store), which is a cHa. We consider therefore downward closed properties only. The (forward) semantics ⟦⟨p(x̄), {c}⟩⟧_{P} of a process p, executed with initial store c ∈ Store in a program P, is defined as usual as the fixpoint of the following recursive function S : ℘^{↓}(Store) ⟼ ℘^{↓}(Store), where for any σ ∈ ℘^{↓}(Store) we have

\begin{aligned}S_{P,c}(σ) & = & ↓ c ∧ σ \\ S_{P,A_{1}∧A_{2}}(σ) & = & S_{P,A_{1}}(σ) ∧ S_{P,A_{2}}(σ) \\ S_{P,∑_{i=1}^{n} A_{i}}(σ) & = & ⋁_{i=1}^{n} S_{P,A_{i}}(σ) \\ S_{P,p(x̄)}(σ) & = & S_{P,A}(σ ∧ x̄ = ȳ) if p(ȳ) ← A << P. \end{aligned}

Note that parameter passing is performed, as usual in logic programming, by telling an equation to the global store, which makes formal and actual parameters matching. In this definition << selects a clause from P whose variables are renamed apart from the rest of the computation.

The following result, which is a consequence of Theorem 7.1.2, states that it is always possible to systematically design a condensing domain for a given basic downward closed property of interest A ∈ uco(℘^{↓}(Store)), by solving the recursive domain equation X = A ⊓ X ⟶^{⋏}X. In order to prove this statement, we consider the following abstract semantics of processes. The abstract semantics is associated with an abstract domain X ∈ uco(℘^{↓}(Store)), such that for any σ ∈ X we have

\begin{aligned}S_{P,c}^{X}(σ) & = & ρ_{X}(S_{P,c}(σ)) \\ S_{P,A_{1}∧A_{2}}(σ) & = & S_{P,A_{1}}^{X}(σ) ∧ S_{P,A_{2}}^{X}(σ) \\ S_{P,∑_{i=1}^{n} A_{i}}(σ) & = & ρ_{X}(⋁_{i=1}^{n} S_{P,A_{i}}^{X}(σ)) \\ S_{P,p(x̄)}^{X}(σ) & = & S_{P,A}^{X}(σ ∧ ρ_{X}(↓ x̄ = ȳ)) if p(ȳ) ← A << P. \end{aligned}

In this case, for any process p(x̄), abstract initial store σ ∈ X, and program P, we define ⟦⟨p(x̄), σ⟩⟧_{P}^{X} = fix(S_{P,p(x̄)}^{X}(σ)). Note that, in each equation above, S^{X} is recursively defined as the best correct approximation of S in X.

Theorem 8.2. Let P be a program, A, X ∈ uco(℘^{↓}(Store)), and p(x̄) be a process. If X = A ⊓ X ⟶^{⋏}X then X is condensing for λσ ∈ X. ⟦⟨p(x̄), σ⟩⟧_{P}^{X}.

Proof. Let X be a solution of the recursive domain equation X = A⊓X ⟶^{⋏}X. Let ψ, φ ∈ X ⊆ ℘^{↓}(Store). Because X is a cHa by Theorem 7.1.2, then it is sufficient to prove, by induction on the recursive calls to the function S^{X} in the definition of ⟦⟨p(x̄), ψ ∧ φ⟩⟧_{P}^{X}, that S^{X} is condensing; i.e., S^{X}(ψ ∧ φ) = ψ ∧ S^{X}(φ).

—Consider S_{P,c}^{X}. By Point (d) in Theorem 7.1.2 we have

S_{P,c}^{X}(ψ ∧ φ) = ρ_{X}(S_{P,c}(ψ ∧ φ))
= ρ_{X}(↓ c ∧ ψ ∧ φ)
= ρ_{X}(↓ c) ∧ ψ ∧ φ
= ψ ∧ ρ_{X}(↓ c ∧ φ)
= ψ ∧ S_{P,c}^{X}(φ).

—Consider S_{P,A_{1}∧A_{2}}^{X}. By Point (d) in Theorem 7.1.2 and inductive hypothesis we have

S_{P,A_{1}∧A_{2}}^{X}(ψ ∧ φ) = S_{P,A_{1}}^{X}(ψ ∧ φ) ∧ S_{P,A_{2}}^{X}(ψ ∧ φ)
= ψ ∧ S_{P,A_{1}}^{X}(φ) ∧ S_{P,A_{2}}^{X}(φ)
= ψ ∧ S_{P,A_{1}∧A_{2}}^{X}(φ).

—Consider S_{P,∑_{i=1}^{n} A_{i}}^{X}. Because X is a cHa by Theorem 7.1.2, then X is a completely meet-distributive lattice. By inductive hypothesis and Point (d) in Theorem 7.1.2 we have

S_{P,∑_{i=1}^{n} A_{i}}^{X}(ψ ∧ φ) = ρ_{X}(⋁_{i=1}^{n} S_{P,A_{i}}^{X}(ψ ∧ φ))
= ρ_{X}(⋁_{i=1}^{n} ψ ∧ S_{P,A_{i}}^{X}(φ))
= ρ_{X}(ψ ∧ ⋁_{i=1}^{n} S_{P,A_{i}}^{X}(φ))
= ψ ∧ ρ_{X}(⋁_{i=1}^{n} S_{P,A_{i}}^{X}(φ))
= ψ ∧ S_{P,∑_{i=1}^{n} A_{i}}^{X}(φ).

—Consider S_{P,p(x̄)}. The thesis follows immediately by definition and inductive hypothesis.

In order to prove the converse of Theorem 8.2, i.e., that condensing domains are solutions of Eq. (11), we need some additional hypotheses. Next result, together with Theorem 8.2, provides a constructive characterization of condensing domains which are at least as precise as a given domain A, as all and only those domains which are solutions of a recursive domain equation of the form X = A ⊓ X ⟶^{⋏}X.

Theorem 8.3. Let P be a program, A, X ∈ uco(℘^{↓}(Store)), and p(x̄) be a process. Assume that for any x, y ∈ X there exist {c_{1}, … c_{n}} ⊆ Store, n < ω, such that the following conditions hold:

—⋁_{i=1}^{n} ↓ c_{i} ≤ x → y —ρ_{X}(⋁_{i=1}^{n} ↓ c_{i}) = ρ_{X}(x → y)

If X is condensing for λσ ∈ X. ⟦⟨p(x̄), σ⟩⟧_{P}^{X} and X ⊑ A then X = A ⊓ X ⟶^{⋏}X.

Proof. Let X be condensing. By Theorem 7.1.2, we have to prove that for any a, b ∈ X we have ρ(a → b) = a → b. Suppose, by contradiction, that there exist a, b ∈ X such that ρ(a → b) > a → b. By hypothesis there exists {c_{1}, … c_{n}} ⊆

ACM Transactions on Programming Languages and Systems, To appear.

Store, n < ω such that the above conditions hold. Consider the program P = { p : − ∑_{i=1}^{n} c_{i} }. Then, by hypothesis, we have

a ∧ ⟦⟨p, ⊤⟩⟧_{P}^{X} = a ∧ ρ_{X}(⋁_{i=1}^{n} ρ_{X}(↓ c_{i}))
= a ∧ ρ_{X}(⋁_{i=1}^{n} ↓ c_{i})
= a ∧ ρ_{X}(a → b)
> a ∧ b
= ρ_{X}(a ∧ a → b)
≥ ρ_{X}(a ∧ ⋁_{i=1}^{n} ↓ c_{i})
= ρ_{X}(⋁_{i=1}^{n} a∧ ↓ c_{i})
= ρ_{X}(⋁_{i=1}^{n} ρ_{X}(a∧ ↓ c_{i}))
= ρ_{X}(⋁_{i=1}^{n} S_{P,c_{i}}^{X}(a))
= ⟦⟨p, a⟩⟧_{P}^{X}.

Therefore X would not be condensing, which is a contradiction.

The hypothesis in Theorem 8.3 is not restrictive for most well-known downward closed domains in logic program analysis. Conditions (1) and (2) say that any implicational object x → y always approximates a finite disjunction of basic stores. This allows us, in Theorem 8.3, to construct, for any implicational object x → y, a (finite) program having that object in the abstract semantics. The idea is that, in order to prove the converse of Theorem 8.2, any implicational object has to be the semantics of some well-defined program. The following characterization result of condensing is therefore immediate by Theorems 8.2 and 8.3.

Corollary 8.4. Under the hypothesis of Theorem 8.3, X is condensing for

λσ ∈ X. ⟦⟨p(x̄), σ⟩⟧_{P}^{X} and X ⊑ A if and only if X = A ⊓ X ⟶^{⋏}X.

As observed in Example 7.1.3 (see Scozzari [1997]), P os is the greatest solution of the recursive domain equation X = G ⊓ X ⟶^{⋏}X. This confirms, in view of Theorem 8.2, a result by Marriott and Søndergaard [1993], which was derived from some results in Langen [1990], saying that P os is condensing. Moreover it is immediate to prove that P os satisfies the hypothesis of Theorem 8.3. Therefore, we can conclude that P os is the most abstract domain, including G, which is condensing for our simple clp-language. This statement strengthens the result in Marriott and Søndergaard [1993] and proves that being disjunctive is not a necessary condition for being condensing. In fact we observe that, although P os is not disjunctive, i.e., P os ≠ ⋎(P os) (cf. Filé and Ranzato [1994]), it is still a condensing domain. The key point in the treatment of disjunction in Theorems 8.2 and 8.3 is that the concrete domain and the solutions of the recursive domain equation X = A ⊓ X ⟶^{⋏}X are always cHa, i.e., these domains are completely meet-distributive. Therefore, even if they are not disjunctive, still no loss of precision is accumulated by distributing the glb (abstract unification) over nondeterministic computations, which are modeled by abstract disjunction.

As observed above, condensing domains are fundamental in order to apply goalindependent analysis to logic and constraint-based languages, yet providing the same precision as in a goal-directed one [Langen 1990; Marriott and Søndergaard 1993]. Because of this key property, condensation is known to be an important property of domains for logic program analysis. Clearly, by our results, the same property of condensation holds for any downward closed domain which is a solution

ACM Transactions on Programming Languages and Systems, To appear.

of Eq. (11), including those for directional type inference in Section 6. The following example shows this phenomenon for a simple domain for directional type inference.

Example 8.5. Consider the domain of basic types T defined in Example 6.1.3 and the simple program P = { p(X, Y) : −X = Y. }. We fix the variables X and Y as variables of interest for the predicate p(X, Y) and consider the abstract constraint p(I, ⊤) whose concretization is the set of all constraints where X is an integer.

⟦⟨p(X, Y), p(I, ⊤)⟩⟧_{P}^{T} = S_{P,p(X,Y)}^{T}(p(I, ⊤))
= S_{P,{ X=Y }}^{T}(p(I, ⊤))
= ρ_{T} (S_{P,{ X=Y }}(p(I, ⊤)))
= ρ_{T} (↓ { X = Y } ∧ p(I, ⊤))
= p(I, I)
⟦⟨p(X, Y), p(⊤, ⊤)⟩⟧_{P}^{T} = S_{P,p(X,Y)}^{T}(p(⊤, ⊤))
= S_{P,{ X=Y }}^{T}(p(⊤, ⊤))
= ρ_{T} (S_{P,{ X=Y }}(p(⊤, ⊤)))
= ρ_{T} (↓ { X = Y } ∧ p(⊤, ⊤))
= ρ_{T} (↓ { X = Y })
= p(⊤, ⊤)

In this case p(I, ⊤)∧⟦⟨p(X, Y), p(⊤, ⊤)⟩⟧_{P}^{T} = p(I, ⊤)∧p(⊤, ⊤) = p(I, ⊤) is different from ⟦⟨p(X, Y), p(I, ⊤)⟩⟧_{P}^{T} = p(I, I). This proves that the abstract domain T is not condensing. By Theorem 8.2, a condensing domain for directional type inference can be systematically designed by solving the recursive domain equation

X = T ⊓ X ⟶^{⋏}X.

9. RELATED WORKS

In the very last section of Cousot and Cousot [1979], the authors introduced the notion of reduced cardinal power, as a domain of monotone functions between two given abstract domains. In Cousot and Cousot [1979, Theorem 10.2.0.1] the authors observed that the concretization of objects in the reduced cardinal power can be expressed by classical implication. This was mainly a consequence of the structure of the underlying concrete domain, which was assumed to be a complete Boolean algebra. This construction was reconsidered and generalized in Giacobazzi and Ranzato [1998], where the authors observed that the weaker hypothesis of cHa is sufficient to ensure the existence of reduced cardinal power of abstract domains. Although in Cousot and Cousot [1979] the authors already observed that functions in reduced cardinal power represent classical implications, none of these papers gave a full logical characterization for the operation of reduced cardinal power in the most general case of cHa. This is a limitation of the above approaches, because in most cases, e.g., those considered in Sections 6 and 8, the concrete domain is not a Boolean algebra. Moreover, as observed in Section 6.2, Boolean algebras may provide the wrong basis to characterize directionality in terms of reduced cardinal power. In addition, none of these papers relate reduced cardinal power with other known operations for domain manipulation, and none of them considered the case of domain equations involving reduced cardinal power and other refinements as basic operators. This is particularly important in abstract interpretation because the

ACM Transactions on Programming Languages and Systems, To appear.

design of a domain is usually the combination of several refinements, and in this process, a clean logical interpretation for all these operations and their interaction makes proofs and technical development more easy to understand. The idea of domain refinement by (classical) complements was introduced in Filé et al. [1996], and later used in Giacobazzi and Ranzato [1997b], to show that there exist refinements that are not invertible, i.e., for which it is not possible to define an inverse operation which returns the (unique) most abstract domain which has the same refinement as the refinement of a given input domain. None of these works, however, generalized the idea to intuitionistic implications. Nielson’s tensor product [Nielson 1985] is also known as a basic operator for relational analyses construction. The tensor product ⊗ is a binary operation on domains such that A⊗B = (A ⟼^{a} B^{op})^{op}. The relation between reduced cardinal power and Nielson’s tensor product has been studied in Giacobazzi and Ranzato [1998], where, under suitable hypothesis, it is proven that A ⟼^{a} B = B^{A}. Therefore, by Theorem 5.3, under these conditions, it is possible to give a logical interpretation of tensor product in terms of intuitionistic implication. Recently, the relation between completeness in abstract interpretation and logical implication has been studied in [Giacobazzi et al. 1998b]. This result relies upon a generalization of our construction from intuitionistic to linear implication.

On the side of domains for program analysis, it would be impossible to give here a full and comprehensive account on all domains for relational program analysis, which include some functionalities which can be provided by reduced cardinal power. These include, among the others, the domains proposed in Aiken and Lakshman [1994], Armstrong et al. [1994], Bronsard et al. [1992], Dart [1991], Giacobazzi and Ranzato [1995], Codish and Demoen [1994], and Yi and Harrison [1993]. However, to the best of our knowledge, the first explicit use of reduced cardinal power to design domains in abstract interpretation, after its original definition in Cousot and Cousot [1979], is in Giacobazzi and Ranzato [1995], where the authors derive the domain Def for ground dependency analysis and a compositional semantics for logic programs as the reduced cardinal power of corresponding abstractions for groundness and noncompositional semantics, respectively. An interesting example on a practical way for implementing domains which can be derived by reduced cardinal power has been recently proposed in logic program analysis, by Codish and Demoen [1994]. In this article the authors used the directional information obtainable for groundness analysis in P os (also called P rop [Armstrong et al. 1994]) to efficiently implement a variety of type inference algorithms by abstract compilation. In Section 6 we have shown that both P os and directional types can be obtained by Heyting completion. Because Heyting completion captures precisely the common structure which surfaces directionality in all these applications, it seems natural to think that the approach in Codish and Demoen [1994] can be used to derive prototype implementations of reduced cardinal power of any domain which is downward closed. In Scozzari [1997] Heyting completion has been applied to groundness analysis in logic programming. These results extend those sketched in Section 6.2 and characterize a variety of abstract domains for groundness analysis in terms of Heyting completion. The use of (recursive) domain equations for specifying domains in static analysis was already considered in Benton [1992a]. In his PhD thesis, Benton used recursive domain equations to extend a simply typed lazy functional language to include algebraic data-types. The author proposes a method where abstract

ACM Transactions on Programming Languages and Systems, To appear.

domains for analysis of algebraic data-types are constructed as solutions of a recursive domain equation associated with a given type. This construction is similar to what we propose here for characterizing domains by Heyting completion (e.g., see the characterization of P os in Section 6 and that of condensing in Section 8). However, these two methods differ on the way equations are defined. In our case, domain equations are not derived from any concrete data-type definition, but they are instead specified in terms of a combination of suitable domain refinements. Domain refinements may in fact be not related with any concrete data-type used in the considered programming language. In principle, a domain refinement is just an operation to enhance an input domain by including new information, which can be either derived by some concrete data-type, or be just part of the concrete domain of computation (see Giacobazzi and Ranzato [1997b]). This makes our approach applicable to derive domains for any (possibly untyped) programming language. As a matter of fact, in the case of Heyting completion considered here, the greatest solution to Eq. (11) does not strictly reflect any concrete data-type, but instead it specifies the least amount of information that a domain has to contain in order to both include a basic domain of properties and allow that these properties can be propagated on domain’s objects by conjunction (see Theorem 7.1.2). For instance, in logic programming, the solution of the above domain equation amounts to finding the most abstract domain which is condensing and includes a given domain of basic properties.

10. CONCLUSIONS AND FUTURE WORK

The main contribution of this work, beside the logical characterization of Cousot’s reduced cardinal power in terms of Heyting completion, is to supply a logical interpretation for the algebra of operators introduced in Cousot and Cousot [1979] for manipulating abstract domains. Domains can no longer be specified only in terms of their elements, but they can also be specified in terms of the property they have to meet, e.g., domains can be specified in equational form, as domains in denotational semantics. Heyting completion is, in this construction, the basic step to build relational domains and analyses. This made it possible to give a clean logical characterization of important properties of domains for program analysis, like condensing and directionality. Although this use of Heyting completion in domain refinement provides a better understanding for a number of properties of domains, the equivalence between reduced cardinal power and Heyting completion opens interesting problems that still deserve further investigation. Our result in fact makes explicit a strong link between domains traditionally used in program analysis and nonstandard type inference. The idea is that the domain A, in the domain equation X = A ⊓ X ⟶^{⋏}X, may represent some sort of basic type information which can be unrelated to any concrete data-type. The solution of the above domain equation therefore specifies a domain of nonstandard types, where product and function types still have the meaning, respectively, as conjunction and implication, similarly to the standard semantics of typed λ-calculus. It seems therefore natural to associate with each abstract domain, obtained as solution of the above domain equation, e.g., P os for ground dependency in logic programming (see Example 7.1.3), a corresponding domain of nonstandard types, and with each abstract interpretation based on that domain, a corresponding nonstandard type inference

ACM Transactions on Programming Languages and Systems, To appear.

algorithm, which can be used to derive static program analysis information. The idea of using type information in static program analysis was first considered in Jensens’s [1995] and Benton’s [1992b] strictness logic and later used by Hankin and Le Metayer [1994]. In these works, the authors proved that some relevant properties of data-structures during program execution can be inferred by a simple type system, in a kind of proof-theoretic approach to program analysis. However, this approach is different from what we are looking for. As observed above in Section 9, the type inference based program analysis in Benton [1992a] is always derived by abstracting the definition of concrete types for the considered programming language. Because of this, nowadays, the use of these so-called type inference based methods for static analysis is mostly restricted to functional languages. We believe instead that any abstract interpretation, for any programming language, whose domains are solutions of the above domain equation, may be joint with a type inference system, which can be in general completely unrelated to any concrete data-type, but still provides correct information about program’s data-flow. In this sense, the relation between types and solutions of Eq. (11) can be further investigated in order to let nonstandard type inference be applicable in the analysis of other programming languages, including logic and constraint-based languages.

REFERENCES Aiken, A. and Lakshman, T. 1994. Directional type checking of logic programs. In Proceedings of

the 1st International Static Analysis Symposium (SAS ’94 ), B. L. Charlier, Ed. Lecture Notes in Computer Science, vol. 864. Springer-Verlag, Berlin, 43–60.

Apt, K. 1990. Introduction to logic programming. In Handbook of Theoretical Computer Science,

J. van Leeuwen, Ed. Vol. B, Formal Models and Semantics. Elsevier, Amsterdam, 495–574. Armstrong, T., Marriott, K., Schachte, P., and Søndergaard, H. 1994. Boolean functions

for dependency analysis: Algebraic properties and efficient representation. In Proceedings of the 1st International Static Analysis Symposium (SAS ’94 ), B. Le Charlier, Ed. Lecture Notes in Computer Science, vol. 864. Springer-Verlag, Berlin, 266–280.

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

Benton, P. 1992a. Strictness analysis of lazy functional programs. Ph.D. thesis, University of

Cambridge, Cambridge, U.K. Benton, P. 1992b. Strictness logic and polymorphic invariance. In Proceedings of the 2nd Inter-

national Symposium on Logical Foundation of Computer Science, A. Nerode and M. Taitslin, Eds. Lecture Notes in Computer Science, vol. 620. Springer-Verlag, Berlin, 33–44.

Birkhoff, G. 1967. Lattice Theory. AMS Colloquium Publication, 3rd edition. AMS, Providence,

R.I. Bronsard, F., Lakshman, T., and Reddy, U. 1992. A framework of directionality for proving

termination of logic programs. In Proceedings of the 1992 Joint International Conference and Symposium on Logic Programming. MIT Press, Cambridge, Mass., 321–335.

Bruynooghe, M. 1991. A practical framework for the abstract interpretation of logic programs.

J. Logic Programm. 10, 91–124. Click, C. and Cooper, K. D. 1995. Combining analyses, combining optimizations. ACM Trans.

Program. Lang. Syst. 17, 2, 181–196. Codish, M., Dams, D., and Yardeni, E. 1994. Bottom-up abstract interpretation of logic pro-

grams. Theor. Comput. Sci. 124, 1, 93–126. Codish, M. and Demoen, B. 1994. Deriving type dependencies for logic programs using multi-

ple incarnations of prop. In Proceedings of the 1st International Static Analysis Symposium

ACM Transactions on Programming Languages and Systems, To appear.

(SAS ’94 ), B. L. Charlier, Ed. Lecture Notes in Computer Science, vol. 864. Springer-Verlag, Berlin, 281–297.

Codish, M., Mulkers, A., Bruynooghe, M., García de la Banda, M., and Hermenegildo, M. 1995. Improving abstract interpretations by combining domains. ACM Trans. Program. Lang. Syst. 17, 1, 28–44.

Cortesi, A., Filé, G., Giacobazzi, R., Palamidessi, C., and Ranzato, F. 1997. Complemen-

tation in abstract interpretation. ACM Trans. Program. Lang. Syst. 19, 1, 7–47. Cortesi, A., Filé, G., and Winsborough, W. 1996. Optimal groundness analysis using propo-

sitional logic. J. Logic Program. 27, 2, 137–167. Cortesi, A., Le Charlier, B., and Van Hentenryck, P. 1994. Combinations of abstract domains

for logic programming. In Conference Record of the 21st ACM Symposium on Principles of Programming Languages (POPL ’94 ). ACM Press, New York, 227–239.

Cousot, P. 1978. Méthodes itératives de construction et d’approximation de points fixes d’opérateurs monotones sur un treillis, analyse sémantique des programmes. Ph.D. thesis, Université Scientifique et Médicale de Grenoble, Grenoble, France.

Cousot, P. 1996. Abstract interpretation. ACM Comput. Surv. 28, 2, 324–328. Cousot, P. and Cousot, R. 1977. Abstract interpretation: A unified lattice model for static

analysis of programs by construction or approximation of fixpoints. In Conference Record of the 4th ACM Symposium on Principles of Programming Languages (POPL ’77 ). ACM Press, New York, 238–252.

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

Cousot, P. and Cousot, R. 1992. Abstract interpretation and application to logic programs. J.

Logic Program. 13, 2-3, 103–179. Cousot, P. and Cousot, R. 1994. Higher-order abstract interpretation (and application to com-

portment analysis generalizing strictness, termination, projection and per analysis of functional languages). In Proceedings of the IEEE International Conference on Computer Languages (ICCL ’94 ). IEEE Computer Society Press, Los Alamitos, Calif., 95–112.

Dams, D., Gerth, R., and Grumberg, O. 1997. Abstract interpretation of reactive systems.

ACM Trans. Program. Lang. Syst. 19, 2, 253–291. Dart, P. 1991. On derived dependencies and connected databases. J. Logic Program. 11, 2,

163–188. Davey, B. A. and Priestley, H. A. 1990. Introduction to Lattices and Order. Cambridge

University Press, Cambridge, U.K. Filé, G., Giacobazzi, R., and Ranzato, F. 1996. A unifying view of abstract domain design.

ACM Comput. Surv. 28, 2, 333–336. Filé, G. and Ranzato, F. 1994. Improving abstract interpretations by systematic lifting to the

powerset. In Proceedings of the 1994 International Logic Programming Symposium (ILPS ’94 ), M. Bruynooghe, Ed. The MIT Press, Cambridge, Mass., 655–669.

Filé, G. and Ranzato, F. 1998. The powerset operator on abstract interpretations. To appear

in Theor. Comput. Sci.. Preliminary version in Filé and Ranzato [1994]. Freese, R., Jezek, J., and Nation, J. 1995. Free lattices. Mathematical surveys and monographs,

vol. 42. AMS, Providence, R.I. Giacobazzi, R. and Ranzato, F. 1995. Functional dependencies and Moore-set completions of

abstract interpretations and semantics. In Proceedings of the 1995 International Symposium on Logic Programming (ILPS ’95 ), J. Lloyd, Ed. The MIT Press, Cambridge, Mass., 321–335.

Giacobazzi, R. and Ranzato, F. 1996. Compositional optimization of disjunctive abstract interpretations. In Proc. of the 1996 European Symposium on Programming, H. Nielson, Ed. Lecture Notes in Computer Science, vol. 1058. Springer-Verlag, Berlin, 141–155.

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

Giacobazzi, R. and Ranzato, F. 1997b. Refining and compressing abstract domains. In Proceedings of the 24th International Colloquium on Automata, Languages and Programming (ICALP ’97 ), P. Degano, R. Gorrieri, and A. Marchetti-Spaccamela, Eds. Lecture Notes in Computer Science, vol. 1256. Springer-Verlag, Berlin, 771–781.

Giacobazzi, R. and Ranzato, F. 1998. The reduced relative power operation of abstract domains.

To appear in Theor. Comput. Sci.. Preliminary version in Giacobazzi and Ranzato [1995]. Giacobazzi, R., Ranzato, F., and Scozzari, F. 1998b. Building complete abstract interpreta-

tions in a linear logic-based setting. In Proceedings of Fifth International Static Analysis Symposium (SAS’98), G. Levi, Ed. Lecture Notes in Computer Science. Springer-Verlag, Berlin. To appear.

Giacobazzi, R., Ranzato, F., and Scozzari, F. 1998a. Complete abstract interpretations made constructive. In Proceedings of the 23rd International Symposium on Mathematical Foundations of Computer Science (MFCS ’98 ), J. Gruska and J. Zlatuska, Eds. Lecture Notes in Computer Science, vol. 1450. Springer-Verlag, Berlin, 366–377.

Girard, J.-Y., Lafont, Y., and Taylor, P. 1989. Proofs and Types. Cambridge University

Press, Cambridge, U.K. Halmos, P. 1962. Algebraic Logic. Chelsea Publ. Co., New York. Hankin, C. and Metayer, D. L. 1994. Deriving algorithms from type inference systems: Appli-

cations to strictness analysis. In Conference Record of the 21st ACM Symposium on Principles of Programming Languages (POPL ’94 ). ACM Press, New York, 202–212.

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

parallelism. J. Logic Program. 13, 2-3, 154–165. Jaffar, J. and Lassez, J.-L. 1987. Constraint Logic Programming. In Conference Record of

the ACM Symposium on Principles of Programming Languages (POPL ’87 ). ACM Press, New York, 111–119.

Jensen, T. 1995. Conjunctive type systems and abstract interpretation of higher-order functional

languages. J. Logic Comput. 5, 4, 397–421. Jensen, T. P. 1992. Disjunctive strictness analysis. In Proceedings of the 7th IEEE Symposium

on Logic in Computer Science (LICS ’92). IEEE Computer Society Press, Los Alamitos, Calif., 174–185.

Jones, N. D. and Muchnick, S. S. 1981. Complexity of flow analysis, inductive assertion synthesis and a language due to dijkstra. In Program Flow Analysis: Theory and Applications, S. S. Muchnick and N. D. Jones, Eds. Prentice-Hall, Upper Saddle River, N.J., 380–393.

Jones, N. D. and Søndergaard, H. 1987. A semantics-based framework for the abstract interpretation of Prolog. In Abstract Interpretation of Declarative Languages, S. Abramsky and C. Hankin, Eds. Ellis Horwood Ltd, Chichester, UK, 123–142.

Langen, A. 1990. Static analysis for independent And-parallelism in logic programs. Ph.D. thesis,

Univ. of Southern California, Los Angeles, Calif. Marriott, K. and Søndergaard, H. 1993. Precise and efficient groundness analysis for logic

programs. ACM Lett. Program. Lang. Syst. 2, 1-4, 181–196. Morgado, J. 1960. Some results on the closure operators of partially ordered sets. Portugaliæ-

Mathematica 19, 2, 101–139. Muthukumar, K. and Hermenegildo, M. 1991. Combined determination of sharing and freeness

of program variables through abstract interpretation. In Proceedings of the 8th International Conference on Logic Programming (ICLP ’91 ), K. Furukawa, Ed. The MIT Press, Cambridge, Mass., 49–63.

Mycroft, A. 1993. Completeness and predicate-based abstract interpretation. In Proceedings of the ACM Symposium on Partial Evaluation and Program Manipulation (PEPM ’93 ). ACM Press, New York, 179–185.

Mycroft, A. and Nielson, F. 1983. Strong abstract interpretation using power domains. In Proceedings of the 10th International Colloquium on Automata, Languages and Programming (ICALP ’83 ), J. Díaz, Ed. Lecture Notes in Computer Science, vol. 154. Springer-Verlag, Berlin, 536–547.

ACM Transactions on Programming Languages and Systems, To appear.

Nielson, F. 1985. Tensor products generalize the relational data flow analysis method. In Proceedings of the 4th Hungarian Computer Science Conference, M. Arató, I. Kátai, and L. Varga, Eds. 211–225.

Saraswat, V., Rinard, V. A., and Panangaden, P. 1991. Semantic foundations of concurrent constraint programming. In Conference Record of the 18th ACM Symposium on Principles of Programming Languages (POPL ’91 ). ACM Press, New York, 333–353.

Scozzari, F. 1997. Logical optimality of groundness analysis. In Proceedings of the 4th International Static Analysis Symposium (SAS ’97 ), P. Van Hentenryck, Ed. Lecture Notes in Computer Science, vol. 1302. Springer-Verlag, Berlin, 83–97.

Sundararajan, R. and Conery, J. 1992. An abstract interpretation scheme for groundness, freeness, and sharing analysis of logic programs. In Proceedings of the 12th Conference on Foundations of Software Technology and Theoretical Computer Science (FST&TCS ’92 ), R. Shyamasundar, Ed. Lecture Notes in Computer Science, vol. 652. Springer-Verlag, Berlin, 203–216.

van Dalen, D. 1994. Logic and Structure. 3rd ed. Springer-Verlag, Berlin. Vickers, S. 1989. Topology via Logic. Cambridge University Press, Cambridge, U.K. Ward, M. 1942. The closure operators of a lattice. Ann. Math. 43, 2, 191–196. Yi, K. and Harrison, W. L. 1993. Automatic generation and management of interprocedural

program analyses. In Conference Record of the 20th ACM Symposium on Principles of Programming Languages (POPL ’93 ). ACM Press, New York, 246–259.

Received January 1998; accepted May 1998