Uniform Closures: Order-Theoretically Reconstructing Logic Program Semantics and Abstract Domain Refinements

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

             giaco@di.unipi.it

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

                                                     franz@math.unipd.it

Abstract

The notion of uniform closure operator is introduced, and it is shown how this concept surfaces in two different areas of application of abstract interpretation, notably in semantics design for logic programs and in the theory of abstract domain refinements. In logic programming, uniform closures permit to generalize, from an order-theoretic perspective, the standard hierarchy of declarative semantics. In particular, we show how to reconstruct the modeltheoretic characterization of the well-known s-semantics using pure order-theoretic concepts only. As far as the systematic refinement operators on abstract domains are concerned, we show that uniform closures capture precisely the property of a refinement of being invertible, namely of admitting a related operator that simplifies as much as possible a given abstract domain of input for that refinement. Exploiting the same argument used to reconstruct the ssemantics of logic programming, we yield a precise relationship between refinements and their inverse operators: we demonstrate that they form an adjunction with respect to a conveniently modified complete order among abstract domains.

Keywords: Abstract interpretation, uniform closure, logic program semantics, abstract domain refinement.

1 Introduction

Abstract interpretation [Cousot and Cousot 1977, 1979] is a well-established theory for program analysis specification, which is gradually gaining ground also as a formal basis for the comparative study and the design of programming language semantics at different levels of abstraction [Cousot 1996, 1997a, 1997b; Cousot and Cousot 1992b, 1995; Giacobazzi 1996; Giacobazzi and Ranzato 1996]. Abstract interpretation theory provides the right mathematical tools to relate in a precise way semantic definitions and to systematically design new semantics, e.g. by approximation or refinement of existing ones. In POPL’92, Patrick and Radhia Cousot put the basis for this new range of applications, by studying the abstract interpretation of generic inductive definitions and by relating trace-based, relational, and denotational semantics.

This work shows that some relevant constructions and results known in semantics of logic programming languages can be generalized from an order-theoretic perspective, and then applied in abstract interpretation theory, providing new and unexpected results in both areas. Our research starts by the attempt to reconstruct the standard hierarchy of declarative semantics for logic programs [Falaschi et al. 1989, 1993] in a purely order-theoretic fashion, i.e. independently from the properties peculiar to the objects manipulated by logic programs, namely atoms, clauses and substitutions. Surprisingly, this generalization, which relies strongly on typical abstract interpretation tools like closure operators and Galois connections, while providing the possibility to extend some standard results well-known in the field of logic programming semantics to other programming languages and semantics, also surfaces in other, completely different, applications

[figure: •; •; •; •; •; •; •; −; −0; ∅; 0; ZZ; 0+; +; Sign; •; •; •; •; •; ∅; 0; ZZ; −; +; A^{±0}; •; •; •; •; ∅; ZZ; −; +; A^{±}]

Figure 1: The domain Sign and two its abstractions A^{±0} and A^{±}.

of abstract interpretation theory, that is in the systematic design of abstract domains. In a sense, this is a good example where the traditional theories of programming language semantics and abstract interpretation may both benefit of a cross fertilization.

Within the standard Cousot and Cousot [1977, 1979] framework, (upper) closure operators capture the “essence” of the process of abstraction, namely they play the rôle of approximating operators. Given a concrete domain C , i.e. a complete lattice where the underlying ordering encodes the relation of approximation between objects (the top element represents no information, i.e. the meaning of the order is dual to the standard one used in classical domain theory), a closure operator ρ : C → C is monotone, idempotent and extensive (i.e. c ≤ ρ(c)). The intuition is quite simple. Monotonicity ensures that the abstraction monotonically approximates domain objects, idempotency means that the process of approximation is performed all at once, while extensivity captures precisely the intended meaning of approximation, i.e. an approximation ρ(c) “contains” less information than its source c. By this approach, the complete lattice uco(C ) of all closure operators on C is identified with the so-called lattice of abstract interpretations of C [Cousot and Cousot 1977], i.e. the complete lattice of all possible abstract domains (modulo isomorphic representation of their objects) of the concrete domain C – where the bottom, i.e. the straightforward abstraction, is C itself.

The order-theoretic reconstruction of the hierarchy of logic program semantics leads naturally to the concept of uniform closure, specialized by duality to meet- and join-uniformity, which is the main novel lattice-theoretic notion of the paper. A closure operator ρ on a complete lattice C is meet-uniform when for any nonempty subset Y ⊆ C , if all the elements of Y are mapped by ρ to some c then also the infimum ∧Y is mapped by ρ to c. Let us give a simple example. Consider the classical domain Sign depicted in Figure 1, typically used for sign analysis of integer variables. The abstract domains A^{±0} and A^{±} both depicted in Figure 1 are two proper abstractions of Sign (actually, A^{±} is in turn an abstraction of A^{±0}). These domains correspond to the following closure operators ρ_{A^{±}0} and ρ_{A^{±}} defined over Sign:

ρ_{A^{±0}}(x) = \{ \begin{matrix}ZZ & if x = ZZ, 0+, 0− \\ x & otherwise; \end{matrix}  ρ_{A^{±}}(x) = \{ \begin{matrix}ZZ & if x = ZZ, 0, 0+, 0− \\ x & otherwise. \end{matrix}

It turns out that ρ_{A^{±0}} is not meet-uniform, because {x ∈ Sign | ρ_{A^{±0}}(x) = ZZ} does not contain its infimum 0, while it is immediate to check that ρ_{A^{±}} is meet-uniform, since in this case {x ∈ Sign | ρ_{A^{±}}(x) = ZZ} contains its infimum.

Closure operators are, in general, neither additive nor co-additive (namely, they do not preserve sups or infs), and meet-uniformity is, in general, weaker than co-additivity. For instance, in the example above, although being meet-uniform, ρ_{A^{±}} is not co-additive: ∅ = ρ_{A^{±}}(0 + ∧ −) ≠ ρ_{A^{±}}(0+) ∧ ρ_{A^{±}}(−) = −. We prove that given a meet-uniform closure ρ on C , meet-uniformity provides a systematic way for lifting the complete order of C , yet maintaining a complete lattice structure, and achieving co-additivity for ρ relatively to the lifted complete order. The definition of such lifted partial order is obtained by generalizing a construction by Falaschi et al. [1993], proposed to relate semantic interpretations for logic programs. Their definition is obtained by lifting the Hoare powerdomain preorder between nonground interpretations (i.e. sets of atoms), based on the relation of instantiation between atoms, so that it becomes a partial order (actually,

[figure: •; •; •; •; •; •; •; −; −0; ∅; 0; ZZ; 0+; +]

Figure 2: Sign equipped with the lifted order for ρ_{A^{±}}.

a complete order). The relevant point of this construction is that it allows to keep track both of the degree of instantiation and of set inclusion between interpretations. The generalization of this idea is quite simple. Given a complete lattice C and any operator ρ : C → C , for all x, y ∈ C , x is smaller than y in the lifted order for ρ, whenever ρ(x) is smaller than ρ(y) in the original order of C . This would lead in general to a preorder relation, unless ρ is injective. Thus, when two elements are mapped by ρ to the same value, the original partial order is considered: whenever ρ(x) = ρ(y), if x is smaller than y in the original order of C , then x is smaller than y in the lifted order as well. The link with the notion of meet-uniformity is given by the relevant consequences of this definition when ρ is a meet-uniform closure operator. The approach of Falaschi et al. [1993] can be then reformulated by means of the closure under instantiation over interpretations, which actually results to be meet-uniform. In the simple example above, the lifted order for Sign with respect to the meet-uniform closure ρ_{A^{±}} gives rise to the lattice depicted in Figure 2, where, e.g., + becomes smaller than −0. Moreover, it is easily seen that for this lifted order, the closure ρ_{A^{±}} actually becomes co-additive.

Let us now illustrate more in detail how the general theory of uniform closure operators will be applied in the fields of logic program semantics and abstract domain design.

Order-Theoretic Reconstruction of the s-Semantics of Logic Programs. The declarative s-sema-ntics has been proposed by Falaschi et al. [1989] (for a survey see [Bossi et al. 1994]) as a semantics modeling more adequately than the canonical least Herbrand model semantics [van Emden and Kowalski 1976] the operational behavior of a logic program as defined by SLD-resolution. In particular, stronger soundness and completeness results hold for the s-semantics, and this allows to characterize precisely the key observable operational property of computed answer substitutions. Due to these features, the s-semantics has been widely and successfully applied in the area of semantics-based program transformation and analysis (see, e.g., [Bossi and Cocco 1993; Barbuti et al. 1993; Codish et al. 1994]). One of the key points of this approach is that the denotations (or interpretations) for a logic program are equivalence classes (w.r.t. renaming of variables) of sets of possibly nonground atoms. However, the original model-theoretic view of s-semantics was unsatisfactory, being based on ad hoc notions of s-truth and s-model [Falaschi et al. 1989, Section 4]. These problems have been solved by Falaschi et al. [1993], where a nonground interpretation is defined to be a model whenever the corresponding Herbrand interpretation given by the closure under ground instances is a model in the standard sense. However, as observed by Falaschi et al. [1993], the model intersection property, which allows to associate with each logic program a canonical model, does not hold in general for these latter models. This is basically due to the fact that plain set inclusion does not adequately reflect this intended meaning of nonground interpretations as models, and instantiation between atoms should be also taken into account. We show that the construction proposed by Falaschi et al. [1993] to overcome these problems can be made fully independent from any notion peculiar to logic programming. Actually, we prove that many results given by Falaschi et al. [1993] can be obtained as an instance of a general framework which completely reconstructs their approach using pure order-theoretic concepts only.

Three are the key observations that led to our construction: (i) the semantics involved in [Falaschi et al. 1993] are related each other by abstract interpretation; (ii) the semantics of computed answers is related to that of correct answers by a meet-uniform closure, which is an instance of a generic downward closure later discussed in Sections 3 and 4; (iii) the lifted order induced by the downward closure generalizes exactly the new ordering relation introduced by Falaschi et al. [1993]. Thus, in our order-theoretic approach, the downward closure becomes co-additive with respect to the lifted order, and, as a consequence, this ensures the existence of the least canonical model. Being independent on specific semantic objects, our results are applicable to other semantics for logic programming in the style of s-semantics, and, more in general, to programming language semantics specified as inductive definitions. For instance, as far as logic programming is concerned, it should not be too hard to generalize many results of the model-theoretic compositional semantics of Bossi et al. [1994, Section 5], following the lines of our approach.

It is worth remarking that logic programming is probably the programming paradigm where abstract interpretation ideas have been mostly successful in the study of semantics, as the growing literature on this topic shows (e.g. see [Amato and Levi 1997; Comini and Levi 1994; Comini et al. 1995; Fages and Gori 1996; Giacobazzi 1996; Giacobazzi and Ranzato 1995, 1996]), and therefore our results well fit along this trend.

Order-Theoretic Foundations of Abstract Domain Refinements. The idea of domain refinement is recurrent in abstract interpretation. Relevant examples include the disjunctive completion [Cousot and Cousot 1979, 1994; Filé and Ranzato 1998; Giacobazzi and Ranzato 1998; Jensen 1997] and the reduced product [Cousot and Cousot 1979], to cite the most known ones. The basic idea is that more expressive abstract domains can be obtained by combining simpler ones or by lifting them by systematically adding new information. A systematic treatment of abstract domain refinements has been given in [Filé et al. 1996; Giacobazzi and Ranzato 1997], where a generic refinement is defined to be a lower closure operator – that is, extensivity is replaced by the dual reductivity – on the lattice of abstract interpretations of a given concrete domain. The intuition is still the most natural. Monotonicity of the refinement preserves the relative precision between abstract domains, idempotency ensures that the refinement is performed all at once, and reductivity captures the action of refinement. This kind of operators on abstract domains provide high-level facilities to tune a program analysis in accuracy and cost, and have been included as tools for design aid in modern systems for program analysis, like for instance in System Z [Yi and Harrison 1993], in PLAI [Codish et al. 1995], and in GAIA [Cortesi et al. 1994].

Recently, much attention has been devoted to “invert” abstract domain refinements. For a given refinement ℜ ∈ lco(uco(C )), this corresponds to define an operator which simplifies an abstract domain A of input for ℜ, by returning the domain (if any) which contains the least amount of information required by ℜ to get the same expressiveness obtainable from A. Thus, the inverse operator of ℜ exists on a class IK ⊆ uco(C ) of abstract domains when, for any A ∈ IK, there exists the least common abstraction of all the domains D such that ℜ(D) = ℜ(A). Intuitively, this somehow resembles what the operation of compression does on files. The problem of inverting in the above sense a refinement can be quite hard to solve in a satisfactory way. Moreover, Filé et al. [1996] observed that not all refinements can be inverted on a significant class of abstract domains. The problem of inverting the reduced product and disjunctive completion has been solved, introducing, respectively, the notions of complementation [Cortesi et al. 1997] and least disjunctive basis [Giacobazzi and Ranzato 1998].

We observe here that the the problem of inverting an abstract domain refinement is closely bound to the concept of uniformity. In fact, since the least common abstraction on the lattice of abstract interpretations coincides with the least upper bound operation, it turns out that a refinement ℜ is invertible if and only if ℜ is join-uniform. Using a straightforward extension of the notion of uniformity, it can be stated more precisely that ℜ is invertible on a class IK of abstract domains if and only if ℜ is join-uniform on IK. The situation is therefore dual to that above for logic program semantics, i.e. join-uniformity replaces meet-uniformity, and hence it is possible to lift the complete order between abstract domains with respect to an invertible refinement. We argue that this novel order reflects more adequately than the standard one the relation of precision between abstract domains relatively to a given invertible refinement. Moreover, we demonstrate that an invertible refinement and its inverse operator give rise to an adjunction with respect to the lifted order, and this justifies once more the use of the term “inversion” in this context.

Structure of the Paper. In Section 2, we recall the basic notations and notions of lattice theory and logic programming used in the paper, and we present a succinct overview of abstract interpretation. In Section 3, motivated from the approach in [Falaschi et al. 1993], we introduce the main notion of uniformity, and in Section 4, we study the meet-uniformity for closure operators on complete lattices. In Section 5, we define the lifting of a complete order via a meet-uniform closure operator, and we prove that this process preserves the complete lattice structure and allows the meetuniform closure to become co-additivity. Using the previous results, in Section 6 we define our order-theoretic generalized semantics, which generalizes the results in [Falaschi et al. 1993]. In particular, the order-theoretic generalizations of the notions of model and least model of a logic program are presented, respectively, in Sections 6.1 and 6.2. Section 7 presents the application to the theory of abstract domain refinements. Section 8 concludes, also by sketching some further research directions.

2 Preliminaries

In this section, we briefly introduce the notation used throughout the paper and summarize some definitions and well-known properties concerning closure operators (for more details see [Birkhoff 1967; Morgado 1960; Ward 1942]), abstract interpretation (see [Cousot and Cousot 1977, 1979]), and logic programming (e.g. see [Apt 1990]).

2.1 Basic Notation

Let C and D be sets. The powerset of C is denoted by ℘(C ), and its cardinality by |C |. The set-difference between C and D is denoted by C \ D. If f is a function defined on C and D ⊆ C then f (D) = {f (x) | x ∈ D}. Functions will be sometimes denoted by Church’s lambda notation. By g ∘ f we denote the composition of the functions f and g, i.e. g ∘ f = λx.g(f (x)). The set C equipped with a partial order ≤ is denoted by ⟨C , ≤⟩ or simply by C_{≤}. If C is a poset, we usually denote by ≤_{C} the corresponding partial order. A complete lattice C with partial order ≤, least upper bound (lub) ∨, greatest lower bound (glb) ∧, top element ⊤ = ∧∅ = ∨C , and bottom element ⊥ = ∨∅ = ∧C , is denoted by ⟨C , ≤, ∨, ∧, ⊤, ⊥⟩. When C is a lattice, ∨_{C} , ∧_{C} , ⊤_{C} and ⊥_{C} denote the corresponding basic operators and elements. Often, we will slightly abuse notation by denoting lattices with their poset notation. We use C ≅ D to denote that the ordered structures C and D are isomorphic. A function f : C → D between complete lattices is additive if for any Y ⊆ C , f (∨_{C} Y ) = ∨_{D}f (Y ). Co-additivity is dually defined.

2.2 Closure Operators

An (upper) closure operator (or simply closure) on a poset C_{≤} is an operator ρ : C → C monotone, idempotent and extensive (i.e., ∀x ∈ C . x ≤ ρ(x)). We denote by uco(C ) the set of all closure operators on the poset C . If C is a complete lattice then each closure operator ρ ∈ uco(C ) is uniquely determined by the set of its fixpoints, which is its image ρ(C ). A subset Y ⊆ C is the set of fixpoints of a closure operator iff Y is a Moore-family of C , i.e. Y = {∧X | X ⊆ Y } (where ⊤ = ∧∅ ∈ Y ). In this case, ρ_{Y} = λx. ∧ {y ∈ Y | x ≤ y} is the corresponding closure on C . The set ρ(C ) of fixpoints of ρ ∈ uco(C ) is a complete lattice (with respect to the order ≤ of C ), and more precisely is a complete meet subsemilattice of C (namely, the glb’s in C and ρ(C ) coincide). However, in general, ρ(C ) is not a complete sublattice of C , since the lub in ρ(C ) might be different from that in C : in fact, ρ(C ) is a complete sublattice of C iff ρ is additive. In view of the above equivalence, often, we will find particularly convenient to identify closure operators with their sets of fixpoints, using as notation capital Latin letters; instead, when viewing closures as functions, we will use Greek letters to denote them. In the following, we will keep this soft ambiguity by using both notations, and leave to the reader to distinguish their use as functions or sets, according to the context. We denote by ⟨uco(C ), ⊑, ⊔, ⊓, λx.⊤, λx.x⟩ the complete lattice of all closure operators on the complete lattice C , where for every ρ, η ∈ uco(C ), {ρ_{i}}_{i∈I} ⊆ uco(C ) and x ∈ L:

– ρ ⊑ η iff ∀x ∈ C . ρ(x) ≤ η(x), or equivalently, ρ ⊑ η iff η(C ) ⊆ ρ(L);

– (⊔_{i∈I} ρ_{i})(x) = x ⇔ ∀i ∈ I . ρ_{i}(x) = x;

– (⊓_{i∈I} ρ_{i})(x) = ∧_{i∈I} ρ_{i}(x);

– λx.⊤ is the top element in uco(C ), whereas λx.x is the bottom element.

By uco^{a}(C ) and uco^{ca}(C ), we denote, respectively, the subsets of uco(C ) consisting of all additive and co-additive closures on C . For a closure operator ρ ∈ uco(C ) and Y ⊆ C , the following two properties hold:

(i) ρ(∧ρ(Y )) = ∧ρ(Y );

(ii) ρ(∨Y ) = ρ(∨ρ(Y )).

It is known that the complete lattice uco(C ) is dual-atomic, namely each closure different from the top λx.⊤ is the glb of the set of dual-atoms following it (where a dual-atom is an element covered by the top).

Lower closure operators are dually defined, that is, extensivity is replaced by reductivity: ∀x ∈ C . ρ(x) ≤ x. The set of all lower closure operators on C is denoted by lco(C ). All the properties of lower closure operators can be derived by duality from those above for upper closures (in particular, uco(C ) and lco(C ) are dually isomorphic). Often, upper and lower closures will be called simply closures, and we will leave to the reader to distinguish them according to the context.

2.3 Galois Connections and Abstract Interpretation Basics

If C and A are posets and α : C → A, γ : A → C are monotone functions such that ∀c ∈ C . c ≤_{C} γ(α(c)) and ∀a ∈ A. α(γ(a)) ≤_{A} a, then the quadruple (α, C , A, γ) is a Galois connection (G.c. for short) between C and A. If in addition ∀a ∈ A. α(γ(a)) = a, then (α, C , A, γ) is a Galois insertion (G.i. for short) of A in C . In a G.i. (α, C , A, γ), α is onto and γ is 1-1. We also recall that the above definition of Galois connection is equivalent to that of adjunction: if α : C → A and γ : A → C then (α, C , A, γ) is a G.c. iff ∀c ∈ C .∀a ∈ A. α(c) ≤_{A} a ⇔ c ≤_{C} γ(a). The map α (γ) is called the left-adjoint (right-adjoint) to γ (α). This terminology is justified by the well-known fact that one mapping uniquely determines the other. In particular, when C and A are complete lattices, if α is additive, or γ is co-additive, then it determines a Galois connection, where:

(i) ∀a ∈ A. γ(a) = ∨_{C} {c ∈ C | α(c) ≤_{A} a};

(ii) ∀c ∈ C . α(c) = ∧_{A}{a ∈ A | c ≤_{C} γ(a)}.

For a function f , we denote by f^{r} (f^{l}) the corresponding right-adjoint (left-adjoint) function, whenever it exists.

Within the standard Cousot and Cousot [1977, 1979] abstract interpretation framework, a nonstandard program semantics is obtained from the standard one by substituting its domain of computation, called concrete (and the basic operations on it), with an abstract domain (and corresponding abstract operations). The concrete and abstract domains are complete lattices, where the ordering relations describe the relative precision of the denotations – the top elements representing no information. The concrete domain C and the abstract domain A are related by a Galois connection (α, C , A, γ), where α and γ are called the abstraction and concretization maps, respectively. Also, A is called an abstraction of C . The intuition is that the concretization map gives the concrete value corresponding to an abstract denotation (i.e. its semantics), whereas for a concrete value the abstraction map gives its best (with respect to the ordering of A) abstract approximation. Thus, an abstract value a ∈ A approximates a concrete value c ∈ C if c ≤_{C} γ(a), or equivalently (by adjunction), if α(c) ≤_{A} a. If (α, C , A, γ) is a G.i., each value of the abstract domain is useful in the representation of the concrete domain, because all the elements of A represent distinct members of C , being γ 1-1. It is known that any G.c. may be lifted to a G.i. identifying in an equivalence class those values of the abstract domain with the same concrete meaning. This process is known as reduction of the abstract domain.

It is well-known since [Cousot and Cousot 1979] that abstract domains can be equivalently specified either as Galois insertions or as (sets of fixpoints of) upper closures on the concrete domain. These two approaches are completely equivalent: if ρ ∈ uco(C ) and A ≅ ρ(C ) (with ι : ρ(C ) → A and ι^{−1} : A → ρ(C ) being the isomorphism) then (ι ∘ ρ, C , A, ι^{−1}) is a G.i.; if (α, C , A, γ) is a G.i. then ρ_{A} = γ ∘ α ∈ uco(C ) is the closure associated with A such that ρ_{A}(C ) ≅ A. Actually, an abstract domain A specified by a G.i. (α, C , A, γ) is just a “computer representation” of its logical meaning, namely its image in the concrete domain C , and therefore the essence of A lies with the corresponding closure operator ρ_{A}. By the above equivalence, it is not restrictive, and often more convenient, to use the closure operator approach to reason about abstract domain properties independently from the representation of the objects. Thus, whenever we will introduce closure operators on some complete lattice C , we will be actually doing a step of abstract interpretation on C . Consequently, we will identify uco(C ) with the so-called lattice of abstract interpretations of C (cf. [Cousot and Cousot 1977, Section 7] and [Cousot and Cousot 1979, Section 8]), i.e. the complete lattice of all possible abstract domains (modulo isomorphic representation of their objects) of the concrete domain C . The ordering on uco(C ) corresponds precisely to the standard order used to compare abstract domains with regard to their precision: A_{1} is more precise than A_{2} (or A_{2} is an abstraction of A_{1}) iff A_{1} ⊑ A_{2} in uco(C ). The lub and glb on uco(C ) have therefore the following meaning as operators on domains. Let {A_{i}}_{i∈I} ⊆ uco(C ):

(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 the A_{i}’s; (ii) ⊓_{i∈I} A_{i} is (isomorphic to) the wellknown reduced product (basically cartesian product plus reduction) of all the A_{i}’s, or, equivalently, it is the most abstract among the domains (abstracting C ) which are more concrete than every A_{i}.

2.4 Logic Programming Notation

Throughout the paper, Atom will denote the set of atoms built over a given first-order language L (where Var denotes the set of variables). A syntactic object is termed ground if it does not contain occurrences of variables. The set of all substitutions (built on L) is denoted by Sub. The application of a substitution σ to a syntactic object s is denoted by sσ. A variable renaming is a substitution which is a bijection on Var. A syntactic object t′ is more instantiated than t (denoted t′ ⪯ t) iff there exists σ ∈ Sub such that t′ = tσ. The relation ⪯ is a pre-order on Atom. Syntactic objects t_{1} and t_{2} are equivalent up to renaming, denoted t_{1} ∼ t_{2}, iff t_{1} ⪯ t_{2} and t_{2} ⪯ t_{1}. For the sake of simplicity, we will let a syntactic object to denote its equivalence class by renaming. The quotient Atom_{/∼} becomes partially ordered with respect to ⪯. With abuse of notation, it is still denoted by Atom, and Atom is also called the nonground Herbrand base. The subset of Atom given by ground atoms is denoted by Atom_{∅}, and called the (ground or standard) Herbrand base.

3 Domains of Interpretations and Meet-Uniformity

In this section, we introduce the concept of (meet-)uniform function defined on complete lattices, which provides us the key notion both for order-theoretically reconstructing the model-theoretic semantics of logic programs and for studying abstract domain refinements.

[figure: ⟨℘(Atom), ⊆, ∪, ∩, Atom, ∅⟩; ⟨℘^{↓}(Atom), ⊆, ∪, ∩, Atom, ∅⟩; ⟨℘(Atom_{∅}), ⊆, ∪, ∩, Atom_{∅}, ∅⟩; ⌈·⌉ ∈ uco(℘(Atom)) additive; gr : ℘^{↓}(Atom) → ℘^{↓}(Atom) additive and co-additive]

Figure 3: The hierarchy of domains of interpretations.

Motivations from Logic Programming. We recall some of the notions involved in the construction proposed by Falaschi et al. [1993]. This is obtained by presenting the different logic program semantics as related by abstract interpretation, similarly to the approaches of Comini and Levi [1994] and Giacobazzi [1996]. In the following, let us assume that a fixed first-order language L is given; all the subsequent notions are then given with respect to L.

In [Falaschi et al. 1993], an interpretation is defined as any subset of the nonground Herbrand base Atom. Hence, the domain of interpretations is fixed as the powerset ⟨℘(Atom), ⊆⟩ of the nonground Herbrand base, ordered by subset inclusion.

Next, some syntactic operators on interpretations are defined as follows. Suppose that I ∈ ℘(Atom).

(i) Closure by instantiation: ⌈I ⌉ = {A ∈ Atom | ∃B ∈ I . A ⪯ B};

(ii) Ground elements: ⌊I ⌋ = {A ∈ I | A is ground};

(iii) Ground instances: gr(I ) = ⌊⌈I ⌉⌋ = ⌈I ⌉ ∩ Atom_{∅}.

Using these operators, we now build a hierarchy of the various domains of interpretations introduced by Falaschi et al. [1993]. The operator ⌈·⌉ defines the subset ℘^{↓}(Atom) of ℘(Atom) given by the interpretations closed by instantiation: ℘^{↓}(Atom) = {I ∈ ℘(Atom) | I = ⌈I ⌉}. Moreover, the set of ground Herbrand interpretations ℘(Atom_{∅}) can be in turn defined as the subset of ℘^{↓}(Atom) which is image of the operator gr (or ⌊·⌋): ℘(Atom_{∅}) = {I ∈ ℘^{↓}(Atom) | I = gr(I ) (= ⌊I ⌋)}.

It is immediate to verify that ⌈·⌉ : ℘(Atom) → ℘(Atom) is an additive closure operator. Hence, its set of fixpoints, equipped with the subset ordering, is a complete sublattice of ℘(Atom), namely ⟨℘^{↓}(Atom), ⊆⟩ is a complete lattice, where lub and glb are, respectively, union and intersection. According to the abstract interpretation viewpoint, this means that the domain of interpretations closed by instantiation actually is an abstraction of the basic domain of (nonground) interpretations. This observation makes explicit in the framework of abstract interpretation the intuition that, by considering as domain of interpretations ℘^{↓}(Atom) instead of ℘(Atom), we are actually disregarding some of the information that ℘(Atom) is able to represent.

On the other hand, it is also clear that gr : ℘^{↓}(Atom) → ℘^{↓}(Atom) is additive and coadditive. Therefore, its image ⟨℘(Atom_{∅}), ⊆⟩, equipped with the subset ordering, is a complete sublattice of ⟨℘^{↓}(Atom), ⊆⟩, and hence lub and glb are union and intersection, respectively. It is worth noting that since gr is additive, it is the left-adjoint of the Galois insertion (gr, ℘^{↓}(Atom), ℘(Atom_{∅}), gr^{r}), where the right-adjoint gr^{r} : ℘(Atom_{∅}) → ℘^{↓}(Atom) is defined as gr^{r}(I ) = ∪{J ∈ ℘^{↓}(Atom) | gr(J ) ⊆ I }. Hence, this Galois insertion induces the closure operator cgr = gr^{r} ∘ gr ∈ uco(℘^{↓}(Atom)), and its image ⟨cgr(℘^{↓}(Atom)), ⊆⟩ is a complete lattice isomorphic to ⟨℘(Atom_{∅}), ⊆⟩. Moreover, since right-adjoints are always co-additive and the composition of co-additive functions is co-additive, the co-additivity of gr induces the co-additivity of the corresponding closure cgr. Here again, these remarks say that ℘(Atom_{∅}) is in turn an abstraction of ℘^{↓}(Atom).

Thus, from the perspective of abstract interpretation, we deal with a hierarchy of abstract domains, as depicted by Figure 3.

Order-Theoretic Generalization. From the order-theoretic point of view, we assume that the basic domain of interpretations is merely any complete lattice ⟨C , ≤⟩. In order to generalize the syntactic operators defined above from an order-theoretic perspective, it is necessary to assume that the domain of interpretations is a powerset of a poset, ordered by subset inclusion, namely ⟨C , ≤⟩ = ⟨℘(Q), ⊆⟩, where ⟨Q, ≤_{Q}⟩ is any poset – nevertheless, it should be remarked that this hypothesis will not be necessary for our generalized order-theoretic construction, as we will see later. The generalization is then immediate, since it involves standard and well-known operators used in basic lattice theory. Let G ⊆ Q be fixed (G stands for the ground Herbrand base), and let I ∈ ℘(Q).

(i) ⌈I ⌉ = ↓I = {x ∈ Q | ∃y ∈ I . x ≤_{Q} y};

(ii) ⌊I ⌋ = I ∩ G;

(iii) gr(I ) = ⌊⌈I ⌉⌋ = (↓I ) ∩ G.

It is immediate to note that ↓ ∈ uco(℘(Q)), and, furthermore, it is additive. This closure operator is generally known as the downward closure. Moreover, it is worthwhile to observe that ↓ is not co-additive: in fact, for the lattice L depicted below, we have that ↓({a} ∩ {b}) = ↓∅ = ∅, while ↓{a} ∩ ↓{b} = {⊥}.

[figure: ⊥; b; ⊤; a; •; •; •; •]

As far as ⌊·⌋ : ℘(Q) → ℘(Q) is concerned, it is immediate to note that ⌊·⌋ is both additive and co-additive.

We propose a generalization of the hierarchy of domains of interpretations recalled above which only takes into consideration some of the order-theoretic properties of the functions involved in that construction. In order to mimic the closure by instantiation relating ℘(Atom) and ℘^{↓}(Atom), we assume that a closure operator ρ ∈ uco(C ) is defined on the generalized domain (i.e. any complete lattice) ⟨C , ≤⟩. Thus, the closure ρ formalizes a step of abstraction on the domain C . In contrast with ⌈·⌉ and its immediate generalization ↓ above, we do not require the additivity of ρ. Instead, we focus on a peculiar and somehow hidden order-theoretic property of the downward closure ↓∈uco(℘(P)), which we call meet-uniformity. To the best of our knowledge, this property of functions has not been previously considered in the literature.^{1} Let C be a complete lattice and S be any set.

Definition 3.1 A function f : C → S is meet-uniform if for all x ∈ C and Y ⊆ C , such that Y ≠ ∅,

(∀y ∈ Y . f (y) = f (x)) ⇒ f (∧_{C} Y ) = f (x). □

In other terms, if S is thought of as a lattice, then a mapping f from C to S enjoys the property of meet-uniformity if it is co-additive for any family of elements for which f is constant. Note that the above condition is vacuously satisfied for Y singleton, and therefore, in the following proofs of meet-uniformity, we will assume |Y | > 1. Further, notice that if f is 1-1 then it is trivially meet-uniform. It is also worth noting that in the above definition the complete lattice C can be easily generalized to any algebra equipped with a finitary or infinitary operation which replaces the rôle played by the glb of C . However, this generality does not contribute significantly to our aims. As far as closures are concerned, we denote by uco^{∗}(C ) = {ρ ∈ uco(C ) | ρ is meet-uniform} the set of all meet-uniform closure operators on the complete lattice C .

1The only account we found on a similar property for closure operators is in [Adaricheva and Gorbunov 1990].

The authors introduced in Definition 1.1 the notion of equational closure on a complete lattice L, as a strict meetuniform upper closure operator ρ on L, where, in addition, closed elements distribute in L and ρ(L) is join-generated by the dual-compact elements of L. The lattice-theoretic structure of equational closures is studied by Adaricheva and Gorbunov [1990] in Section 5. However, because meet-uniformity is in general weaker than equationality, their results are not applicable to study the properties of generic meet-uniform closure operators on complete lattices.

As announced above, although not being co-additive, the downward closure is meet-uniform, whenever the poset Q satisfies the ascending chain condition (ACC for short, i.e. it does not contain infinite strictly increasing chains).

Theorem 3.2 If Q satisfies the ACC then ↓ is meet-uniform.

In order to demonstrate this result, we need some notation and a preliminary lemma. The operator max : ℘(Q) → ℘(Q), giving the maximal elements of any subset S of Q, is defined as follows: max(S) = {x ∈ S | ∀y ∈ S. x ≤_{Q} y ⇒ x = y}.

Lemma 3.3 Let Q be a poset.

(i) For any S ∈ ℘(Q), max(S) = max(↓S).

(ii) If Q satisfies the ACC then, for all S ⊆ Q, ↓S = ↓max(S).

(iii) If Q satisfies the ACC then, for all S, T ⊆ Q, ↓S = ↓T ⇔ max(S) = max(T ).

Proof.

(i) (⊆) Let x ∈ max(S) and consider any y ∈ ↓S such that x ≤_{Q} y. Hence, there exists z ∈ S such that y ≤_{Q} z. Thus, x ≤_{Q} z, from which x = z. Therefore, x = y, and x ∈ max(↓S). (⊇) Let x ∈ max(↓ S). If x ∈ S then x ∈ max(↓ S), since S ⊆ ↓ S. Otherwise, x ∈ ↓ S \ S. Thus, there exists y ∈ S such that x <_{Q} y, which is a contradiction.

(ii) (⊇) Because from max(S) ⊆ S one get ↓max(S) ⊆ ↓S. (⊆) Let x ∈ ↓ S. Then, there exists y_{0} ∈ S such that x ≤_{Q} y_{0}. If y_{0} ∈ max(S) then x ∈ ↓max(S). Otherwise, there exists y_{1} ∈ S such that y_{0} ≤_{Q} y_{1} and y_{0} ≠ y_{1}, i.e. y_{0} <_{Q} y_{1}. If y_{1} ∈ max(S) then x ∈ ↓ max(S), otherwise, as before, we pick out another y_{2} ∈ S such that y_{0} <_{Q} y_{1} <_{Q} y_{2}. Iterating this constructive process, we would get an infinite strictly increasing chain, namely, a contradiction. Thus, there exists k ∈ IN such that y_{k} ∈ max(S) and x ≤_{Q} y_{k}, i.e. x ∈ ↓max(S).

(iii) (⇒) max(S) = (by (i)) = max(↓S) = max(↓T ) = (by (i)) = max(T ). (⇐) ↓S = (by (ii)) = ↓max(S) = ↓max(T ) = (by (ii)) = ↓T .

Proof of Theorem 3.2. Consider any family {S_{i}}_{i∈I} ⊆ ℘(A) (where |I | > 1) and T ∈ ℘(A) such that ∀i ∈ I . ↓S_{i} = ↓T . Let us prove that ↓(∩_{i∈I} S_{i}) = ↓T . (⊆) By monotonicity of ↓. (⊇) Let x ∈ ↓T . By Lemma 3.3 (ii), ↓T = ↓max(T ), and therefore, there exists y ∈ max(T ) such that x ≤_{Q} y. By Lemma 3.3 (iii), for all i ∈ I , max(S_{i}) = max(T ), and hence, max(T ) ⊆ S_{i}. Thus, max(T ) ⊆ ∩_{i∈I} S_{i}, and y ∈ ∩_{i∈I} S_{i}, i.e. x ∈ ↓(∩_{i∈I} S_{i}).

It is worth remarking that when Q does not satisfy the ACC, Theorem 3.2 in general does not hold, as the following example shows.

Example 3.4 Consider the poset IN of the natural numbers, equipped with the standard ordering, which does not satisfy the ACC, and the subsets O and E of, respectively, odd and even numbers. Then, ↓O = ↓E = IN, whilst ↓(O ∩ E) = ↓∅ = ∅, i.e. ↓ is not meet-uniform. □

Since Atom, equipped with the partial order of instantiation ⪯, is evidently a poset satisfying the ascending chain condition, as a consequence of Theorem 3.2, we get that the closure by instantiation ⌈·⌉ : ℘(Atom) → ℘(Atom) is meet-uniform. We will see later that meet-uniformity is the key order-theoretic property that allows to generalize the results in [Falaschi et al. 1993]. Then, in our generalized hierarchy, we assume that the first step of abstraction is given by a

[figure: ⟨C , ≤, ∨, ∧, ⊤_{C} , ⊥_{C} ⟩; ⟨ρ(C ), ≤, ∨_{ρ(C )}, ∧, ⊤_{C} , ρ(⊥_{C} )⟩; ⟨g(ρ(C )), ≤, ∨_{g(ρ(C ))}, ∧, ⊤_{C} , g(ρ(⊥_{C} ))⟩; ρ ∈ uco^{∗}(C ); g : ρ(C ) → ρ(C ) co-additive]

Figure 4: The generalized order-theoretic hierarchy of domains.

meet-uniform closure operator ρ ∈ uco^{∗}(C ). The next step consists in generalizing the grounding operator defined on ℘^{↓}(Atom). As observed above, gr and ⌊·⌋ coincide on ℘^{↓}(Atom), and gr : ℘^{↓}(Atom) → ℘^{↓}(Atom) is both additive and co-additive. Our generalization simply considers any co-additive map defined on the image ⟨ρ(C ), ≤⟩, namely any g : ρ(C ) → ρ(C ) which is coadditive. Clearly, being co-additive, g is also monotone. Hence, in this case the key order-theoretic property of the grounding operator relating the domain of interpretations closed by instantiation and the domain of ground interpretations is its co-additivity. As we noted above, this actually is an abstract interpretation step. However, for our purposes, we only need to consider any co-additive map. Also, notice that the image of the co-additive function g, ⟨g(ρ(C )), ≤⟩ is a complete lattice w.r.t. the induced order ≤, where the glb coincides with that of ρ(C ) (which in turn coincides with that in C ), i.e. ⟨g(ρ(C )), ≤⟩ is a Moore-family of both ⟨C , ≤⟩ and ⟨ρ(C ), ≤⟩. Our order-theoretic generalized hierarchy is summarized by Figure 4.

4 Meet-Uniform Closure Operators

In this section, we mainly concentrate on studying the properties of meet-uniform closure operators on complete lattices. In the following, let us assume that ⟨C , ≤⟩ is any complete lattice.

As we noted above, each injective function is meet-uniform. As far as closures are concerned, obviously, the only injective closure is the identity. Thus, injectivity is not relevant to characterize meet-uniformity of closure operators. Moreover, the following remark shows that, for any closure operator, the dual property of join-uniformity is always satisfied.

Remark 4.1 Each ρ ∈ uco(C ) is join-uniform.

Proof. Let Y ⊆ C and x ∈ C such that for any y ∈ Y , ρ(y) = ρ(x). Then, by point (ii) in Section 2.2 and by idempotency, ρ(∨Y ) = ρ(∨ρ(Y )) = ρ(ρ(x)) = ρ(x).

Clearly, the bottom element of uco(C ), i.e. the identity operator, belongs to uco^{∗}(C ). Furthermore, the following result holds.

Theorem 4.2 uco^{∗}(C ) is a Moore-family of uco(C ).

Proof. Clearly, λx.⊤ ∈ uco^{∗}(C ). Then, let us consider {ρ_{i}}_{i∈I} ⊆ uco^{∗}(C ), with |I | > 1. We show that ⊓_{i∈I} ρ_{i} ∈ uco^{∗}(C ). Consider any Y ⊆ C and x ∈ C such that for all y ∈ Y , (⊓_{i∈I} ρ_{i})(y) = (⊓_{i∈I} ρ_{i})(x). If we prove that for any i ∈ I , ρ_{i}(∧Y ) = ρ_{i}(x), the thesis follows, since (⊓_{i∈I} ρ_{i})(∧Y ) = ∧_{i∈I} ρ_{i}(∧Y ) = ∧_{i∈I} ρ_{i}(x) = (⊓_{i∈I} ρ_{i})(x). Thus, consider any j ∈ I and y ∈ Y . Then, y ≤ (⊓_{i∈I} ρ_{i})(y) = (⊓_{i∈I} ρ_{i})(x) = ∧_{i∈I} ρ_{i}(x), and, analogously, x ≤ ∧_{i∈I} ρ_{i}(y). Hence, y ≤ ρ_{j} (x) and x ≤ ρ_{j} (y), from which ρ_{j} (y) = ρ_{j} (x) easily follows. Therefore, for all i ∈ I , ρ_{i}(∧Y ) = ρ_{i}(x).

As a consequence, uco^{∗}(C ) is a complete lattice with respect to the order inherited from uco(C ). The next example shows that, in general, uco^{∗}(C ) is not a complete sublattice of uco(C ).

[figure: •; •; •; •; •; •; •; ρ_{1}; ρ_{2}; ρ_{3}; ρ_{4}; ρ_{5}; ρ_{6}; ρ_{7}; •; •; •; •; •; •; ρ_{1}; ρ_{2}; ρ_{4}; ρ_{5}; ρ_{6}; ρ_{7}]

Figure 5: The lattices uco(L), on the left, and uco^{∗}(L), on the right.

Example 4.3 Consider the finite lattice L depicted in Section 3 (the four-point “rhombus” lattice). The closure operators on L are as follows:

ρ_{1} = {⊤}, ρ_{2} = {⊤, a}, ρ_{3} = {⊤, ⊥}, ρ_{4} = {⊤, b},
ρ_{5} = {⊤, a, ⊥}, ρ_{6} = {⊤, b, ⊥}, ρ_{7} = {⊤, a, b, ⊥},

and therefore uco(L) is the lattice depicted in Figure 5. It is then simple to verify that uco^{∗}(C ) is the lattice depicted in Figure 5. In fact, the only closure which is not meet-uniform is ρ_{3}: ρ_{3}(a) = ρ_{3}(b) = ⊤, whilst ρ_{3}(a ∧ b) = ρ_{3}(⊥) = ⊥. Also, observe that uco^{∗}(L) is not a sublattice of uco(L). □

The example above allows one to draw the following two additional consequences.

(i) The property of dual-atomicity of uco(C ) does not hold anymore for the complete lattice uco^{∗}(C ).

(ii) The functional composition of two meet-uniform closure operators, whenever this is a closure, in general, is not meet-uniform. In fact, for the meet-uniform closures ρ_{5} and ρ_{6} above, one has that ρ_{5} ∘ ρ_{6} = ρ_{6} ∘ ρ_{5} = ρ_{3} is not meet-uniform.

Let S be a set, f : C → S, and consider the corresponding equivalence relation ≈_{f} on C induced by f : x ≈_{f} y ⇔ f (x) = f (y). The following definition assigns a canonical representative to each equivalence class defined by ≈_{f} .

Definition 4.4 For any x ∈ C , define ∇_{f} (x) = ∧[x]_{≈f} (= ∧{y ∈ C | f (y) = f (x)}). □

If f is meet-uniform then it is immediate to observe that this is a good definition, i.e., for any x ∈ C , ∇_{f} (x) ≈_{f} x. Further, it is worth noticing that if f = ρ ∈ uco(C ) then ∇_{ρ}(x) = ∇_{ρ}(ρ(x)). We will use these remarks in the following proofs. The following observation provides an alternative characterization of meet-uniformity. Let ⟨A, ≤_{A}⟩ be a poset.

Proposition 4.5 Let f : C → A be monotone. f is meet-uniform iff for any x ∈ C , ∇_{f} (x) ≈_{f} x.

Proof. (⇒) Obvious. (⇐) Consider any Y ⊆ C (with |Y | > 1) and x ∈ C such that f (y) = f (x), for all y ∈ Y . Obviously, f (∧_{C} Y ) ≤_{A} f (x). On the other hand, by hypothesis, ∇_{f} (x) ≈_{f} x, and therefore f (x) = f (∇_{f} (x)) ≤_{A} f (∧_{C} Y ). Thus, f (∧_{C} Y ) = f (x).

This observation allows us to give the following slight generalization of the notion of meetuniformity. Let f : C → A be monotone and K ⊆ C . Then, we define f to be meet-uniform on K (or K -meet-uniform) when for any x ∈ K , ∇_{f} (x) ≈_{f} x. Thus, by Proposition 4.5, f is meetuniform iff f is meet-uniform on C . In particular, given a complete lattice, we denote by uco_{K}^{∗} (C ) the set of all closures on C which are meet-uniform on K . It is simple to verify that the above Theorem 4.2 admits a straightforward generalization for this notion of K -meet-uniformity, and therefore uco_{K}^{∗} (C ) is a Moore-family of uco(C ). We will see the usefulness of this more general concept of meet-uniformity later in Section 7.

For the downward closure of Section 3, a simple characterization of the canonical representative of Definition 4.4 can be given as follows.

Remark 4.6 If Q satisfies the ACC then, for each I ∈ ℘(Q), ∇_{↓}(I ) = max(I ).

Proof. By Lemma 3.3 (iii), ∇_{↓}(I ) = ∩{J ∈ ℘(Q) | ↓ J = ↓ I } = ∩{J ∈ ℘(Q) | max(J ) = max(I )}. Moreover, since max(max(I )) = max(I ), ∇_{↓}(I ) ⊆ max(I ). On the other hand, if max(J ) = max(I ), then max(I ) ⊆ J , and therefore ∇_{↓}(I ) = max(I ).

We close this section by observing that meet-uniformity can be induced on closure operators by means of Galois connections. By a slight abuse of terminology, a G.c. (α, C , A, γ) is defined to be meet-uniform if the map α is meet-uniform. The next result shows that meet-uniform G.c.’s induce meet-uniform closures.

Proposition 4.7 A G.c. (α, C , A, γ) is meet-uniform iff γ ∘ α ∈ uco^{∗}(C ).

Proof. We only prove the “only if” part, since the other direction is similar. Consider any Y ⊆ C and x ∈ C such that ∀y ∈ Y . γ(α(y)) = γ(α(x)). Then, for all y ∈ Y , α(γ(α(y))) = α(γ(α(x))), and, since α ∘ γ ∘ α = α, we get α(y) = α(x). Hence, α(∧_{C} Y ) = α(x), from which, γ(α(∧_{C} Y )) = γ(α(x)).

5 Lifting Complete Orders via Meet-Uniform Closures

The following key definition is obtained as an obvious generalization of the partial order introduced by Falaschi et al. [1993, Definition 4.1] (see Section 6.2 below). Let ⟨C , ≤_{C} ⟩ and ⟨A, ≤_{A}⟩ be posets, and consider any function f : C → A.

Definition 5.1 The lifting via f of the ordering ≤_{C} is the relation ≤_{C}^{f} on C defined as follows:

x ≤_{C}^{f} y iff f (x) ≤_{A} f (y) & (f (y) ≤_{A} f (x) ⇒ x ≤_{C} y).

□

In the following, we study the consequences of this notion. Firstly, it is straightforward to note that the above definition actually is correct.

Lemma 5.2 ≤_{C}^{f} is a partial order on C .

Let us assume that the function f is monotone. Then, observe that ≤_{C} ⊆ ≤_{C}^{f} , i.e., for all x, y ∈ C , x ≤_{C} y ⇒ x≤_{C}^{f} y. Also, if C is bounded, with top and bottom elements (w.r.t. ≤_{C} ) ⊤ and ⊥, then C is bounded for the lifted order too, where ⊤ and ⊥ are still the top and the bottom w.r.t. ≤_{C}^{f} .

In the following, we will focus on closure operators, because, in our generalized hierarchy of semantics, f will play the rôle of an abstraction map, which is therefore uniquely determined by a closure operator. For the next result, let us assume that ⟨C , ≤⟩ is a mere poset.

Proposition 5.3 If ρ, η ∈ uco(C_{≤}) and η ⊑ ρ, then η ∈ uco(C_{≤^{ρ}}).

Proof. Idempotency of η is clearly preserved. ≤^{ρ}-extensivity of η easily follows from the fact that ≤ ⊆ ≤^{ρ}. We prove monotonicity: x ≤^{ρ} y ⇒ η(x) ≤^{ρ} η(y). First, since η ⊑ ρ, we have that ρ ∘ η = η ∘ ρ = ρ. Thus, from the hypothesis ρ(x) ≤ ρ(y), we get η(ρ(x)) = ρ(η(x)) ≤ ρ(η(y)) = η(ρ(y)). On the other hand, assume now that ρ(η(y)) ≤ ρ(η(x)). Hence, we have that ρ(y) ≤ ρ(x), which, by hypothesis, implies x ≤ y. Then, by ≤-monotonicity of η, we get η(x) ≤ η(y), which concludes the proof.

As an immediate consequence of the above result, we get that if ρ ∈ uco(C_{≤}) then ρ ∈ uco(C_{≤^{ρ}}). Let us now give a simple example of lifting a partial order via a closure operator.

Example 5.4 Consider the lattice ⟨L, ≤⟩ of Example 4.3, and the closures ρ_{2} = {⊤, a} and ρ_{3} = {⊤, ⊥} defined on L. It is easy to verify that lifting ≤ via ρ_{3} changes nothing in the structure of L, i.e. ≤ = ≤^{ρ_{3}}. Instead, lifting ≤ via ρ_{2} gives the chain {⊥ <^{ρ_{2}} a <^{ρ_{2}} b <^{ρ_{2}} ⊤}. □

From now on, let ⟨C , ≤, ∨, ∧, ⊤, ⊥⟩ be a complete lattice. A key property of lifting a complete order via a meet-uniform closure operator is that this step preserves the complete lattice structure.

Theorem 5.5 If ⟨C , ≤⟩ is a complete lattice and ρ ∈ uco^{∗}(C_{≤}) then ⟨C , ≤^{ρ}⟩ is a complete lattice.

The proof of this theorem consists in giving explicit characterizations of lub’s and glb’s for the lifted order. Given a meet-uniform closure ρ ∈ uco^{∗}(C ), recall from Definition 4.4 that for each x ∈ C , ∇_{ρ}(x) = ∧{y ∈ C | ρ(y) = ρ(x)}. Then, for any subset Y ⊆ C , let us give the following definitions:

˙∨Y = ∨({y ∈ Y | ∇_{ρ}(∨Y ) ≤ y} ∪ {∇_{ρ}(∨Y )});

˙∧Y = \{ \begin{matrix}∧\{y ∈ Y | ρ(y) = ρ(x)\} & if ∃x ∈ Y . ∧ ρ(Y ) = ρ(x); \\ ∧ρ(Y ) & otherwise. \end{matrix}

In order to prove that ˙∨ and ˙∧ actually are the lub and glb for the lifted order, we need the following preliminary lemma.

Lemma 5.6 For all Y ⊆ C , ρ( ˙∨Y ) = ρ(∨Y ).

Proof. The following equalities prove the claim:

ρ( ˙∨Y ) = ρ(∨({y ∈ Y | ∇_{ρ}(∨Y ) ≤ y} ∪ {∇_{ρ}(∨Y )}))
(by point (ii) in Section 2.2) = ρ(∨({ρ(y) ∈ Y | ∇_{ρ}(∨Y ) ≤ y} ∪ {ρ(∇_{ρ}(∨Y ))}))
(by meet-uniformity of ρ) = ρ(∨({ρ(y) ∈ Y | ∇_{ρ}(∨Y ) ≤ y} ∪ {ρ(∨Y )}))
(by point (ii) in Section 2.2) = ρ(∨({y ∈ Y | ∇_{ρ}(∨Y ) ≤ y} ∪ {∨Y }))
= ρ(∨Y ).

Theorem 5.7 ˙∨ and ˙∧ are the lub and glb in ⟨C , ≤^{ρ}⟩.

Proof. Let us first prove that ˙∨ is the lub. Consider any Y ⊆ C .

(a) Let us show that if y ∈ Y then y ≤^{ρ} ˙∨Y .

(a_{1}) ρ(y) ≤ ρ( ˙∨Y ): Immediate from Lemma 5.6. (a_{2}) ρ( ˙∨Y ) ≤ ρ(y) ⇒ y ≤ ˙∨Y : Since, from the hypothesis and Lemma 5.6, we get ρ(y) = ρ( ˙∨Y ) = ρ(∨Y ), we also have that ∇_{ρ}(∨Y ) = ∇_{ρ}(ρ(∨Y )) = ∇_{ρ}(ρ(y)) = ∇_{ρ}(y), and this implies y ≤ ˙∨Y .

(b) Assume that there exists u ∈ C such that ∀y ∈ Y . y ≤^{ρ} u. Then, we prove that ˙∨Y ≤^{ρ} u. (b_{1}) ρ( ˙∨Y ) ≤ ρ(u): From the hypothesis follows that ∨ρ(Y ) ≤ ρ(u). Hence, by Lemma 5.6, ρ( ˙∨Y ) = ρ(∨Y ) = ρ(∨ρ(Y )) ≤ ρ(ρ(u)) = ρ(u). (b_{2}) ρ(u) ≤ ρ( ˙∨Y ) ⇒ ˙∨Y ≤ u: By hypothesis and Lemma 5.6, ρ(u) = ρ(∨Y ). First, we verify that ∇_{ρ}(∨Y ) ≤ u: in fact, ∇_{ρ}(∨Y ) = ∇_{ρ}(ρ(∨Y )) = ∇_{ρ}(ρ(u)) = ∇_{ρ}(u) ≤ u. Second, if ∇_{ρ}(∨Y ) ≤ y then y ≤ u: as above, ∇_{ρ}(∨Y ) = ∇_{ρ}(u), and therefore, ∇_{ρ}(u) ≤ y. Thus, ρ(∇_{ρ}(u)) = ρ(u) ≤ ρ(y). Since, by hypothesis, ρ(u) ≤ ρ(y) ⇒ y ≤ u, we get the desired y ≤ u.

Let us now prove that ˙∧ is the glb. Consider any Y ⊆ C . We distinguish between the two mutually exclusive branches of the definition of ˙∧.

(a) There exists x ∈ Y such that ∧ρ(Y ) = ρ(x), and hence, ˙∧Y = ∧{y ∈ Y | ρ(y) = ρ(x)}. Since ρ is meet-uniform, ρ( ˙∧Y ) = ρ(x) = ∧ρ(Y ). We will use this observation during the proof. (a_{1}) ∀y ∈ Y . ˙∧Y ≤^{ρ} y: First, ρ( ˙∧(Y )) = ρ(x) ≤ ρ(y) holds. Second, ρ(y) ≤ ρ( ˙∧Y ) ⇒ ˙∧Y ≤ y holds too, since the premise is equivalent to ρ(y) = ρ(x). (a_{2}) If there exists l ∈ C such that ∀y ∈ Y . l ≤^{ρ} y then l ≤^{ρ} ˙∧Y : first, ρ(l) ≤ ρ( ˙∧Y ), since ρ( ˙∧Y ) = ρ(x), and, from the hypothesis, ρ(l) ≤ ∧ρ(Y ) = ρ(x). Second, the implication ρ( ˙∧Y ) ≤ ρ(l) ⇒ l ≤ ˙∧Y holds, since its premise implies ρ(x) = ρ(l), and, if y ∈ Y is such that ρ(y) = ρ(x) then ρ(y) = ρ(l). By exploiting the hypothesis l ≤^{ρ} y, this implies l ≤ y, which in turn implies l ≤ ˙∧Y .

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

Figure 6: The lattice ⟨C , ≤⟩ on the right, and the poset ⟨C , ≤^{ρ}⟩ on the left.

(b) Assume the other branch, i.e. ∀y ∈ Y . ∧ ρ(Y ) < ρ(y). In this case, ˙∧Y = ∧ρ(Y ). (b_{1}) ∀y ∈ Y . ˙∧Y ≤^{ρ} y: First, ρ( ˙∧Y ) = ρ(∧ρ(Y )) = ∧ρ(Y ) ≤ ρ(y). Second, the implication ρ(y) ≤ ρ( ˙∧Y ) ⇒ ˙∧Y ≤ y, i.e. ρ(y) = ∧ρ(Y ) ⇒ ˙∧Y ≤ y, trivially holds, since, by hypothesis, its premise is never satisfied. (b_{2}) If there exists l ∈ C such that ∀y ∈ Y . l ≤^{ρ} y then l ≤^{ρ} ˙∧Y : first, ρ(l) ≤ ρ( ˙∧Y ) = ∧ρ(Y ), since, by hypothesis, ∀y ∈ Y . ρ(l) ≤ ρ(y). Second, ρ( ˙∧Y ) ≤ ρ(l) ⇒ l ≤ ˙∧Y holds, since it is equivalent to ρ(l) = ∧ρ(Y ) ⇒ l ≤ ∧ρ(Y ), which is true, because l ≤ ρ(l).

Note that the singleton {∇_{ρ}(∨Y )} has been added in the above definition of ˙∨ because if {y ∈ Y | ∇_{ρ}(∨Y ) ≤ y} results to be empty then ∇_{ρ}(∨Y ) is taken as lub, rather than ∨∅ = ⊥. Also, as observed above in all generality, note that ⊤ and ⊥ remain unchanged after the lifting of the ordering: in fact, ˙∨C = ˙∧∅ = ⊤ and ˙∧C = ˙∨∅ = ⊥. As a consequence of Theorem 5.7, we get the following fact, which will be useful in the following sections.

Corollary 5.8 For any Y ⊆ C , ˙∧ρ(Y ) = ∧ρ(Y ).

It is important to remark that the meet-uniformity is the crucial property of the closure ρ that allows to prove Theorem 5.5. In fact, the following example shows that if the closure is not meet-uniform, then, in general, the lifted order does not give rise to a complete lattice.

Example 5.9 Consider the finite lattice ⟨C , ≤⟩, depicted in Figure 6, and consider the closure ρ ∈ uco(C ) defined by ρ(C ) = {⊤, c, d, ⊥}. It is immediate to verify that ρ is not meet-uniform: in fact, ρ(a) = ρ(b) = ⊤, but ρ(a ∧ b) = ρ(⊥) = ⊥. In this case, the lack of meet-uniformity for ρ implies that the lifted poset ⟨C , ≤^{ρ}⟩, depicted in Figure 6, is not a lattice anymore, because, by definition of ≤^{ρ}, d ≤^{ρ} a and c ≤^{ρ} b. □

There is a further remarkable consequence of lifting a complete order ≤ via a meet-uniform closure operator ρ. In fact, by this process, we upgrade the properties enjoyed by ρ whenever considered w.r.t. the lifted complete order ≤^{ρ}: ρ becomes a co-additive closure operator.

Theorem 5.10 If ρ ∈ uco^{∗}(C_{≤}) then ρ ∈ uco^{ca}(C_{≤^{ρ}}).

Proof. By Proposition 5.3, ρ still is a closure operator on ⟨C , ≤^{ρ}⟩. Let us show that it is coadditive. By Corollary 5.8, it is enough to show that for any Y ⊆ C , ρ( ˙∧Y ) = ∧ρ(Y ). We distinguish the two branches of the characterization of ˙∧.

(i) If ˙∧Y = ∧{y ∈ Y | ρ(y) = ρ(x)} for a suitable x ∈ Y such that ρ(x) = ∧ρ(Y ), then ρ( ˙∧Y ) = ρ(x) = ∧ρ(Y ), because ρ is meet-uniform (on C_{≤}). (ii) Otherwise, ˙∧Y = ∧ρ(Y ), and hence, ρ( ˙∧Y ) = ρ(∧ρ(Y )) = ∧ρ(Y ).

6 Generalized Order-Theoretic Semantics

In this section, we show how to exploit the general order-theoretic results of the previous sections in order to define an order-theoretic semantics generalizing the model-theoretic logic program semantics proposed by Falaschi et al. [1993].

6.1 Interpretations as Models

The s-semantics for logic programs has been defined by Falaschi et al. [1989] with the aim of providing a declarative semantic counterpart to the operational observable property given by computed answer substitutions, since this was not possible by means of the standard ground success-set semantics of van Emden and Kowalski [1976]. Let us introduce the following notation: Π denotes the set of predicate symbols of the underlying first-order language L, and X̄ denotes a sequence of distinct variables; moreover, if P is a program and G = b_{1}, ..., b_{n} (n ≥ 0) is a goal, then we write G ⟶^{θ}_{P} □ iff there exists a SLD-refutation of G in P with computed answer substitution θ. Then, the s-semantics S(P) ⊆ Atom of a program P is defined as

S(P) = {p(X̄ )θ | p ∈ Π, θ ∈ Sub, p(X̄ )⟶^{θ}_{P} □}.

It turns out that this semantics is fully abstract with respect to the notion of computed answer substitution (cf. [Falaschi et al. 1989]). Let P_{1} and P_{2} be programs, and define P_{1} and P_{2} to be equivalent for the computed answer substitutions observable when, for any goal G, p(X̄ )⟶^{θ}_{P_{1}} □ iff p(X̄ )⟶^{σ}_{P_{2}} □ and Gθ ∼ Gσ. Then, the full abstraction theorem states that S(P_{1}) = S(P_{2}) if and only if P_{1} and P_{2} are equivalent in that sense. For all the details, properties and consequences of the s-semantics the reader is referred to [Falaschi et al. 1989], since here we recalled its definition for illustrative purposes only.

The s-semantics of any program is therefore defined as a subset of the nonground Herbrand base, namely it is an interpretation. Falaschi et al. [1993] gave a model-theoretic interpretation for sets of nonground atoms, with the obvious goal of making the s-semantics a model as well as any standard ground Herbrand model. Let us recall this notion. Given a standard ground Herbrand interpretation I ∈ ℘(Atom_{∅}) and a definite clause c, the notion of truth of c in I is the standard logical one, i.e. I ⊧ c. On the other hand, given any nonground interpretation I ∈ ℘(Atom), from a model-theoretic viewpoint, the idea is that I is a denotation for the set of its ground instances gr(I ). Accordingly, Falaschi et al. [1993] proposed the following approach: an interpretation I ∈ ℘(Atom) is a model of a program P if all the clauses of P are true (in the standard logical sense) in gr(I ). By this definition, any standard Herbrand model is also a model in the above sense, and therefore this implies that any program has a model. Moreover, it turns out that, for any program P, the s-semantics S(P) is a model of P, and for any ground Herbrand interpretation I ∈ ℘(Atom_{∅}), this new notion of being a model is equivalent to the standard old one.

It is well-known [van Emden and Kowalski 1976] that, for any program P, its set M_{P} of standard Herbrand models is closed by set intersection, and therefore the least Herbrand model exists. Also, the ground Herbrand base Atom_{∅} is a model, i.e. Atom_{∅} ∈ M_{P}. This implies that M_{P} is a Moore-family of ℘(Atom_{∅}), i.e. M_{P} can be thought of as a closure on ℘(Atom_{∅}) such that for any I ∈ ℘(Atom_{∅}), I is a Herbrand model of P iff I is a fixpoint of M_{P}. This observation has been firstly reported by Lassez and Maher [1984]. As a side observation, we note that, in general, this closure operator is not meet-uniform. In fact, consider P = {p ← q, q ← p}, and I = {p}, J = {q} ∈ ℘(Atom_{∅}); it is clear, that M_{P}(I ) = M_{P}(J ) = {p, q}, whilst I ∩J = ∅ ∈ M_{P}.

Order-Theoretic Generalization. In our order-theoretic approach, the above notion of model is formalized naturally as follows. Recall that in the generalized hierarchy of Section 3, the set of ground Herbrand interpretations corresponds to the complete lattice ⟨g(ρ(C )), ≤⟩, where any generalized interpretation x ∈ C is “grounded” to g(ρ(x)). Thus, given any program P,^{2} its set of ground Herbrand models is generalized by a closure operator m_{P} ∈ uco(g(ρ(C ))). Therefore, an interpretation x ∈ C is a (generalized) model of P whenever g(ρ(x)) is a fixpoint of m_{P}, i.e. when g(ρ(x)) is a generalized Herbrand model of P. The set G_{P} of (generalized) models of P is then defined as: G_{P} = {x ∈ C | m_{P}(g(ρ(x))) = g(ρ(x))}.

2It is worth noting that in our order-theoretic reconstruction, we do not need at all to refer to ‘real’ logic programs. Thus, we can think of the set of all programs as a mere set of objects acting as indices.

6.2 Generalizing the Model-Theoretic Semantics

By contrast to standard Herbrand models, Falaschi et al. [1993] observe, by a simple counterexample, that the model intersection property does not hold any longer for the notion of nonground model recalled in Section 6.1. This implies that the least model of a program with respect to set inclusion, in general, does not exist. Of course, in our order-theoretic construction, this counterexample shows that, in general, the set of generalized models G_{P} is not closed by glb (of C ). Falaschi et al. [1993] point out that this phenomenon “can easily be explained by noting that set inclusion does not adequately reflect the property of nonground atoms of being representatives of all their ground instances”. Then, they propose a new partial order on ℘(Atom), as given in the following definition, which allows to restore the desired model intersection property.

Definition 6.1 ([Falaschi et al. 1993, Definition 4.1]) Let I , J ∈ ℘(Atom). Then,

(i) I ⊢ J ⇔ ∀A ∈ I .∃B ∈ J . B ⪯ A;

(ii) I ≤ J ⇔ (I ⊢ J ) & (J ⊢ I ⇒ I ⊆ J ). □

As Falaschi et al. note, clearly, I ⊢ J iff ⌈I ⌉ ⊆ ⌈J ⌉, and therefore:

I ≤ J ⇔ (⌈I ⌉ ⊆ ⌈J ⌉) & (⌈J ⌉ ⊆ ⌈I ⌉ ⇒ I ⊆ J ).  (∗)

By this formulation, this definition gets a clearer meaning. In fact, it says that in order to compare two interpretations I and J we have to look at their respective abstractions in ℘^{↓}(Atom): I is smaller than J if ⌈I ⌉ ⊂ ⌈J ⌉, and, whenever ⌈I ⌉ = ⌈J ⌉, the original subset-ordering, I ⊆ J , is considered.

Falaschi et al. [1993] present a number of important consequences of Definition 6.1. They show that ⟨℘(Atom), ≤⟩ is a complete lattice, and provide an explicit characterization for the corresponding lub. Further, they prove that for any program P, the glb w.r.t. ≤ of its set of nonground models is still a model, thus obtaining the ≤-least nonground model for P, which is also shown to coincide with the standard least Herbrand model. It is important to remark that in order to prove all these results, specific logic programming concepts and tools are heavily used, like clauses, substitutions, instances, Herbrand models, etc. In contrast, our generalized approach involves pure order-theoretic notions only, and no specific logic programming concept.

Order-Theoretic Generalization. By the characterization (∗) above, it is immediate to observe that the ordering given by Definition 6.1 is an instance of the definition of lifted partial order induced by the meet-uniform closure ⌈·⌉ on the domain of nonground interpretations ℘(Atom). By the results of Section 4, in our generalized hierarchy, the hypothesis that the first step of abstraction of C is given by a meet-uniform closure ρ, just allows us to lift the complete order ≤ of C via ρ, then obtaining the lifted complete lattice ⟨C , ≤^{ρ}⟩. Hence, this is precisely the order-theoretic generalization of the corresponding result of Falaschi et al. [1993, Theorem 4.9]. Also, we noted that, in general, the glb (in C ) of a set of models of P, i.e. of a subset of G_{P} = {x ∈ C | m_{P}(g(ρ(x))) = g(ρ(x))}, is not a model of P. Instead, the next theorem shows that the meet-uniformity of the closure ρ is, once again, the crucial property that permits to recover the generalized model-intersection property w.r.t. the lifted complete order ≤^{ρ}.

Theorem 6.2 If ρ ∈ uco^{∗}(C_{≤}) then G_{P} is a Moore-family of ⟨C , ≤^{ρ}⟩.

[figure: ⟨C , ≤, ∨, ∧, ⊤_{C} , ⊥_{C} ⟩; ⟨ρ(C ), ≤, ∨_{ρ(C )}, ∧, ⊤_{C} , ρ(⊥_{C} )⟩; ⟨g(ρ(C )), ≤, ∨_{g(ρ(C ))}, ∧, g(⊤_{C} ), g(ρ(⊥_{C} ))⟩; G_{P} = {x ∈ C | m_{P}(g(ρ(x))) = g(ρ(x))}; ⇝ in general, G_{P} ∉ uco(⟨C , ≤⟩); ⟨C , ≤^{ρ}, ˙∨, ˙∧, ⊤_{C} , ⊥_{C} ⟩; ·; ·; ·; ·; ·; ·; ·; ·; ·; ·; ·; ·; ·; ·; ·; ·; ·; ·; ·; ·; ·; ·; ·; ·; ·; ·; ·; ·; ·; ·; ·; ·; ·; ·; ·; ·; ·; ·; ·; ·; ·; ·; ·; ·; ·; ·; ·; ·; G_{P} ∈ uco(⟨C , ≤^{ρ}⟩); lifting ≤ via ρ; ρ ∈ uco^{∗}(⟨C , ≤⟩); g : ρ(C ) → ρ(C ) co-additive; m_{P} ∈ uco(⟨g(ρ(C )), ≤⟩); ∥; ∥; ⇓]

Figure 7: The overall generalized order-theoretic approach.

Proof. Let {x_{i}}_{i∈I} ⊆ G_{P}. The following equalities hold:

m_{P}(g(ρ( ˙∧_{i∈I} x_{i}))) = (by Theorem 5.10)
m_{P}(g( ˙∧_{i∈I} ρ(x_{i}))) = (by Corollary 5.8)
m_{P}(g(∧_{i∈I} ρ(x_{i}))) = (by ≤-co-additivity of g)
m_{P}(∧_{i∈I} g(ρ(x_{i}))) = (since ∀i ∈ I . x_{i} ∈ G_{P})
m_{P}(∧_{i∈I} m_{P}(g(ρ(x_{i})))) = (since m_{P} ∈ uco(g(ρ(C ))_{≤}) and by (i) in Section 2.2)
∧_{i∈I} m_{P}(g(ρ(x_{i}))) = (since ∀i ∈ I . x_{i} ∈ G_{P})
∧_{i∈I} g(ρ(x_{i})) = (by ≤-co-additivity of g)
g(∧_{i∈I} ρ(x_{i})) = (by Corollary 5.8)
g( ˙∧_{i∈I} ρ(x_{i})) = (by Theorem 5.10)
g(ρ( ˙∧_{i∈I} x_{i})).

This shows that ˙∧_{i∈I} x_{i} ∈ G_{P}, and therefore closes the proof.

As a consequence, for any program P, G_{P} is a complete lattice w.r.t. ≤^{ρ} – this generalizes [Falaschi et al. 1993, Corollary 4.11] – and the ≤^{ρ}-least generalized model is therefore ˙∧G_{P}. The overall scenario is summarized by Figure 7.

By assuming further hypotheses, we are also able to give the generalization in our framework of the fact proved by Falaschi et al. [1993, Theorem 4.15] that the ≤-least model coincides with the ⊆-least Herbrand model. Recall that in our generalized approach, g(ρ(C )) stands for the subset of C of ground Herbrand interpretations, while, for any program P, m_{P} ∈ uco(⟨g(ρ(C )), ≤⟩) is the closure representing the Herbrand models of P. Thus, the set H_{P} of generalized Herbrand models of a program P is just given by H_{P} = {z ∈ g(ρ(C )) | m_{P}(z) = z}. Hence, ∧H_{P} is the order-theoretic counterpart of the ⊆-least Herbrand model, and ˙∧G_{P} = ∧H_{P} states the equality of the two generalized least models. Analogously to the logic programming side, it is straightforward to note that, for any program P, by grounding its set of generalized models, one gets its set of generalized Herbrand models, i.e. H_{P} = {g(ρ(x)) ∈ g(ρ(C )) | x ∈ G_{P}}. The further hypotheses required by the next theorem correspond, on the logic programming side, to the observations that the grounding operator gr : ℘^{↓}(Atom) → ℘^{↓}(Atom) is indeed a (co-additive) lower closure operator, and that for any I ∈ ℘(Atom) and J ∈ ℘^{↓}(Atom), whenever J indeed is ground (i.e. gr(J ) = J ) and I ⊆ J , then I is ground as well.

Theorem 6.3 If g ∈ lco(ρ(C )_{≤}), and, for any x ∈ C and y ∈ ρ(C ), x ≤ g(y) = y implies x ∈ ρ(C ) and g(x) = x, then, for any program P, ˙∧G_{P} = ∧H_{P}.

Proof. First, note that H_{P} = g(ρ(G_{P})). Also, the following equalities hold:

∧H_{P} = (since H_{P} = g(ρ(G_{P})))
∧g(ρ(G_{P})) = (by ∧-co-additivity of g)
g(∧ρ(G_{P})) = (by Corollary 5.8)
g( ˙∧ρ(G_{P})) = (by Theorem 5.10)
g(ρ( ˙∧G_{P})) = (by Theorem 6.2)  (1)
m_{P}(g(ρ( ˙∧G_{P}))).  (2)

Moreover, by the equality (1), g(ρ(∧H_{P})) = g(ρ(g(ρ( ˙∧G_{P})))), and, since g(ρ(C )) ⊆ ρ(C ) and by idempotency of g and ρ, we get

g(ρ(∧H_{P})) = g(ρ( ˙∧G_{P})) = (by (1)) = ∧H_{P}.  (3)

( ˙∧G_{P} ≤^{ρ} ∧H_{P}) The following equalities show that ∧H_{P} ∈ G_{P}:

m_{P}(g(ρ(∧H_{P}))) = (by (1))
m_{P}(g(ρ(g(ρ( ˙∧G_{P}))))) = (by g(ρ(C )) ⊆ ρ(C ) and idempotency of g and ρ)
m_{P}(g(ρ( ˙∧G_{P}))) = (by (2))
∧H_{P} = (by (3))
g(ρ(∧H_{P})).

(∧H_{P} ≤^{ρ} ˙∧G_{P}) We show that if x ∈ G_{P} then ∧H_{P} ≤^{ρ} x.

(i) From x ∈ G_{P}, we get ˙∧G_{P} ≤^{ρ} x, from which, ρ( ˙∧G_{P}) ≤ ρ(x), and, in turn, g(ρ( ˙∧G_{P})) ≤ g(ρ(x)). By the equality (1) above, ∧H_{P} = g(ρ( ˙∧G_{P})), and since ρ(∧H_{P}) = ∧H_{P}, we get, by reductivity of g, ρ(∧H_{P}) ≤ g(ρ(x)) ≤ ρ(x), as desired. (ii) We show that ρ(x) = ρ(∧H_{P}) ⇒ ∧H_{P} ≤ x. From ρ(x) = ρ(∧H_{P}) = ∧H_{P}, we get g(ρ(x)) = g(∧H_{P}) = (since g is a lower closure) = ∧H_{P} = ρ(x). Thus, x ≤ ρ(x) = g(ρ(x)), and by the hypotheses of the theorem, we obtain g(x) = x. Hence, ρ(x) = ρ(g(x)) = (since g(ρ(C )) ⊆ ρ(C )) = g(x), from which, x = ρ(x) = ∧H_{P}.

It is worth noting that it is possible to slightly generalize our hierarchy, and in particular Theorem 6.2. In fact, after the first step of abstraction given by a meet-uniform closure ρ ∈ uco^{∗}(C_{≤}), we can consider an arbitrary finite number of further abstractions given by co-additive functions. This is possible since the composition of co-additive functions is clearly still co-additive. Also, note that by considering the mapping g as the identity, we can deal only with the unique abstraction given by ρ.

7 Uniform Closures and Abstract Domain Refinements

In this section, we show how the novel order-theoretic notion of uniformity finds relevant applications also in abstract interpretation theory, specifically in the area of refinement operators of abstract domains (as far as the precision is concerned).

7.1 Abstract Domain Refinements

In abstract interpretation, a domain refinement is intended as an operator which takes as input a given abstract domain (that is, a closure), and returns as output an enhanced domain, i.e. a more precise domain, by systematically adding new information. A formal treatment of abstract domain refinements has been recently put forward by Filé et al. [1996] and successively sharpened by Giacobazzi and Ranzato [1997], generalizing most of the well-known domain refinements, like reduced product and disjunctive completion [Cousot and Cousot 1979]. In the following, we assume that ⟨C , ≤⟩ is the complete lattice that plays the rôle of the concrete domain of reference. As recalled in Section 2.3, the lattice of abstract interpretations of a given concrete domain C is isomorphic to the complete lattice uco(C ) of all upper closure operators on C . As recalled

• • • −0 ZZA^{−}  • • • + 0+ ZZA^{+}

Figure 8: The abstract domains A^{−} and A^{+}.

in the Introduction, an abstract domain refinement is defined as an operator ℜ : uco(C ) → uco(C ) on the lattice uco(C ) of abstractions of C , which is monotone and reductive (i.e., ℜ(A) ⊑ A). Idempotency is an additional reasonable requirement, ensuring that the refinement of an abstract domain is performed all at once. Thus, a refinement is a lower closure operator on the complete lattice uco(C ), i.e. any mapping in lco(uco(C )), and therefore, some properties of domain refinements can be derived by duality from those of abstract domains, which are upper closure operators. Among them, (i) the image of ℜ coincides with the set of refined abstract domains: ℜ(uco(C )) = {A ∈ uco(C ) | ℜ(A) = A}, and (ii) the set ⟨lco(uco(C )), ⊑⟩ of all the refinements is a complete lattice (by a slight abuse of notation, we always use the symbol ⊑ for any order between closures), where ℜ_{1} ⊑ ℜ_{2} iff for any A ∈ uco(C ), ℜ_{1}(A) ⊑_{uco(C )} ℜ_{2}(A) iff the set of domains refined by ℜ_{1} is contained in the set of those refined by ℜ_{2}. Thus, analogously to the case of abstract domains, the complete ordering ⊑ between refinements can be interpreted as a relation of precision, where ℜ_{1} is more precise than ℜ_{2} iff ℜ_{1} ⊑ ℜ_{2}. For more details and properties on abstract domain refinements, we refer to [Giacobazzi and Ranzato 1997].

Example 7.1 Reduced product^{3} is the simplest and probably most familiar example of abstract domain refinement. It has been successfully applied in many works on program analysis, for instance in [Codish et al. 1995; Granger 1988; Muthukumar and Hermenegildo 1991; Sundararajan and Conery 1992]. As recalled in Section 2.3, the reduced product corresponds to the glb in the complete lattice of (upper) closure operators. The terminology reduced product of abstract domains stems from the fact that it can be represented by means of the standard cartesian product, where equivalent tuples of objects are identified, i.e. reduced (more details are given, e.g., in [Cousot and Cousot 1992a]). For example, consider the abstract domains A^{−} and A^{+} in Figure 8, which are abstractions of the complete lattice ⟨℘(ZZ), ⊆⟩ (with the most obvious meaning of their elements), and are typically used for sign analysis of integer variables. It is easily seen that, up to isomorphic representation of domain’s objects, the reduced product A^{−} ⊓ A^{+} is the abstract domain Sign of Figure 1. Observe that Sign has two new elements with respect to A^{−} and A^{+}, i.e. 0 and ∅, which are obtained by combining, by set intersection in ℘(ZZ), the corresponding sets of integers, respectively, −0 with 0+, and − with +. Here, reduction is necessary only for identifying distinct pairs of elements denoting the empty set of integers: the pairs ⟨−, +⟩, ⟨−0, +⟩ and ⟨−, 0+⟩ all denote ∅. By fixing one of the arguments of reduced product, one obviously gets a refinement. Let C be the concrete domain and A ∈ uco(C ) be any fixed abstract domain. Then, the reduced product refinement with respect to A is the lower closure operator ℜ_{⊓A} = λX . (A ⊓ X ) ∈ lco(uco(C )). □

7.2 Inverting Refinements

Filé et al. [1996] motivated and introduced the notion of inverse of an abstract domain refinement. For a given refinement ℜ ∈ lco(uco(C )) and an abstract domain A ∈ uco(C ), the optimal basis of A for ℜ, when it exists, is a domain D ∈ uco(C ) such that ℜ(D) = ℜ(A), and for any B ∈ uco(C ), ℜ(B) = ℜ(A) implies B ⊑ D. Clearly, if an optimal basis D exists, then this domain is unique. Thus, we will refer to the existence of the optimal basis. In other terms, whenever the optimal basis of A for ℜ exists, this is the most abstract domain having the same refinement (for ℜ) as

3For simplicity of notation, we consider the reduced product as a binary operator.

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

Figure 9: The abstract domains Sign^{≠0}, A_{1} and A_{2}.

A. Given a class IK ⊆ uco(C ) of abstract domains, if any A ∈ IK admits the optimal basis, the mapping ℜ^{−} : IK → uco(C ) providing the optimal basis is called the inverse of ℜ on IK. Thus, the inverse ℜ^{−} does exist on IK iff there exists the optimal basis for ℜ of any domain in IK. The intuition is that the refined domain ℜ(A) can be systematically reconstructed by applying the refinement ℜ to the more abstract, and therefore simpler, domain ℜ^{−}(A). Therefore, roughly speaking, ℜ^{−} is the operator providing the simplest abstract domains of input for the refinement ℜ.

The notion of abstract domain refinement can be slightly generalized, by allowing the possibility of having as domain of definition of a refinement any subset Q of uco(C ) (see [Giacobazzi and Ranzato 1997] for all the details). In this case, the inverse of a refinement ℜ : Q → uco(C ) could exist for some subset IK of Q and it should take values over Q, i.e. ℜ^{−} : IK → Q. An example of this kind of partial refinement is provided by the negative completion refinement (cf. [Filé et al. 1996; Giacobazzi and Ranzato 1997]). Let the concrete domain C be a complete Boolean algebra. The negative completion ℜ_{¬} is then defined on the sublattice uco^{a}(C ) of uco(C ) of additive closures (also called disjunctive abstract domains), and it upgrades a given abstract domain by adding denotations for the lattice-theoretic complements of its elements. It is easy to verify that if A ∈ uco^{a}(C ) then ¬A = {¬a ∈ C | a ∈ A} ∈ uco^{a}(C ). Thus, ℜ_{¬} lifts a given disjunctive abstract domain A to the most abstract domain containing both A and ¬A, i.e. ℜ_{¬} : uco^{a}(C ) → uco(C ) maps A to the reduced product ℜ_{¬}(A) = A ⊓ ¬A. Although, given A ∈ uco^{a}(C ), ℜ_{¬}(A), in general, does not belong to uco^{a}(C ) (cf. [Giacobazzi and Ranzato 1997]), it turns out that ℜ_{¬} is monotone, reductive and idempotent, and therefore is a refinement in the generalized framework of Giacobazzi and Ranzato [1997]. In general, optimal bases do not always exist, and the negative completion provides a meaningful example of a refinement which is not invertible on any really significant class of abstract domains, as first noted by Filé et al. [1996]. Let us consider the disjunctive abstract domains Sign^{≠0}, A_{1} and A_{2} depicted in Figure 9, for sign analysis of integer variables, with their obvious meanings as additive closures on ⟨℘(ZZ), ⊆⟩ (which obviously is a complete Boolean algebra). It turns out that the the optimal basis of Sign^{≠0} for ℜ_{¬} does not exist. In fact, ℜ_{¬}(A_{1}) = ℜ_{¬}(A_{2}) = ℜ(Sign^{≠0}) = Sign^{≠0}, while for the least common abstraction A_{1} ⊔ A_{2} = {ZZ, 0, ∅}, ℜ_{¬}(A_{1} ⊔ A_{2}) = {ZZ, ≠ 0, ∅}, and hence this implies that Sign^{≠0} does not admit the optimal basis for ℜ_{¬}. Since in this example the concrete domain is a complete Boolean algebra, and Sign^{≠0} enjoys all most important lattice-theoretic properties, this means that ℜ_{¬} is not invertible on any significant class of abstract domains.

7.3 Invertibility as Join-Uniformity

As the attentive reader might have already guessed, it turns out that join-uniformity captures exactly the concept of invertible domain refinement. Recalling by duality from Section 4 the notion of K -join-uniformity, one can state the following immediate result, whose prime importance stems from the striking connection between two notions came out from very different questions.

Theorem 7.2 Given IK ⊆ uco(C ), a refinement ℜ : uco(C ) → uco(C ) is invertible on IK iff ℜ is join-uniform on IK.

Moreover, given a refinement ℜ : uco(C ) → uco(C ) which is invertible on IK, the canonical representative of Definition 4.4 of an abstract domain A ∈ IK for ℜ is ∇_{ℜ}(A) = ⊔{D ∈ uco(C ) | ℜ(D) = ℜ(A)}, and therefore it is exactly the optimal basis of A, i.e. ∇_{ℜ}(A) = ℜ^{−}(A). In other words, the canonical representative operator ∇_{ℜ} is the inverse of ℜ. Hence, following the notation of Section 4, we have that lco_{IK}^{∗}(uco(C )) denotes the set of abstract domain refinements invertible on IK ⊆ uco(C ). By duality from the observations and results of Section 4, we can then derive the following properties of invertible refinements:

(i) Invertible refinements on some IK give rise to a complete lattice ⟨lco_{IK}^{∗}(uco(C )), ⊑⟩, which, in particular, is a complete join subsemilattice, i.e. a dual-Moore-family, of lco(uco(C )), with top and bottom elements λX . X (the identity refinement) and λX . C (the full refinement), respectively;

(ii) The lattice of invertible refinements is not dual-atomic;

(iii) Invertibility is not preserved by composition.

By property (i), the space of refinements that are invertible on some fixed IK is itself the set of fixpoints of a lower closure operator ψ^{∗} ∈ lco(lco(uco(C ))), defined as follows: for any ℜ ∈ lco(uco(C )), ψ^{∗}(ℜ) = ⊔{ℑ ∈ lco(uco(C )) | ℑ ⊑ ℜ, ℑ is invertible on IK}. This operator transforms any, possibly noninvertible on IK, refinement ℜ ∈ lco(uco(C )), into the weakest refinement (with respect to the order ⊑ between refinements explained in Section 7.1) which is both invertible on IK and more precise than ℜ.

Let us now see an important example of an invertible abstract domain refinement.

Example 7.3 Disjunctive completion was originally introduced by Cousot and Cousot [1979] to prove that merge-over-all-paths data-flow analyses can be always expressed in least fixpoint form. It has been then considered in Nielson’s [1984] approach to abstract interpretation using domain theory, and applied in program analysis, e.g., in Cousot and Cousot’s [1994] comportment analysis, in Deutsch’s [1992] alias analysis, in Jensen’s [1997] disjunctive strictness logic, and in analysis of logic program groundness-dependencies [Filé and Ranzato 1998]. The disjunctive completion enhances an abstract domain as little as possible so that it becomes disjunctive, i.e. an additive closure. It should be evident that isjunctive abstract domains are practically very useful, since their lub’s are as precise as possible. Following the general approach of Giacobazzi and Ranzato [1998], given a concrete domain C , the disjunctive completion ℜ_{∨} : uco(C ) → uco(C ) is defined as ℜ_{∨}(A) = ⊔{D ∈ uco^{a}(C ) | D ⊑ A}, for any A ∈ uco(C ). It is immediate to observe that ℜ_{∨} actually is a lower closure, and hence correctly defines an abstract domain refinement. Whenever the concrete domain is completely distributive, the disjunctive completion of an abstract domain can be characterized by various equivalent powerset constructions [Cousot and Cousot 1994; Filé and Ranzato 1998]. As a simple example, if Sign is the abstraction of ⟨℘(ZZ), ⊆⟩ of Figure 1, its disjunctive completion ℜ_{∪}(Sign) is the domain Sign^{≠0} considered above and depicted in Figure 9, which contains the concrete lub (i.e. set union) of any subset of Sign, and in particular it contains a new object ≠ 0 = − ∪ 0, denoting nonzero integers. The inverse of disjunctive completion should therefore be an operation which returns (when possible) the most abstract domain whose disjunctive completion is a given disjunctive abstract domain. Giacobazzi and Ranzato [1998] introduced the notion of least disjunctive basis for an abstract domain, that turns out to be an instance of the concept of optimal basis, and hence allows to define the inverse of the disjunctive completion refinement. Giacobazzi and Ranzato [1998, Theorems 4.10 and 4.11] give two results of existence of the least disjunctive basis, which can be read in the terminology of this paper as follows:

(i) If C is a dual-algebraic completely distributive lattice then ℜ_{∨} is invertible on all uco(C );

(ii) If C is distributive then ℜ_{∨} is invertible on {A ∈ uco(C ) | |A| < ℵ_{0}}.

It is not hard to verify that the optimal basis ℜ_{∪}^{−}(Sign) of Sign is the abstract domain A^{±0} of Figure 1. □

From what has been discussed above, it would be natural to think that the inverse of an abstract domain refinement can be formalized as an operator of simplification, somehow dual to a refinement. Intuitively, an abstract domain simplification should be an operator that for a given domain of input, returns a more abstract domain, that is, it should be an extensive operator on the lattice of abstract interpretations. Moreover, as well as for refinements, a simplification operator should monotonically transform abstract domains, and perform simplifications all at once. In this sense, while refinements are lower closures, their inverses should generally be upper closures. Instead, we will see that when a given refinement ℜ ∈ lco(uco(C )), possibly under some hypotheses on C , is invertible on all uco(C ), the inverse operator ℜ^{−} is not necessarily an upper closure. More in general, when ℜ is invertible on IK ⊆ uco(C ), the inverse ℜ^{−} : IK → uco(C ) is not necessarily monotone. In fact, we can only prove the following general result for join-uniform functions, where f^{ı} is just the dual canonical representative operator of Definition 4.4.

Proposition 7.4 Let L be a complete lattice and f : L → L be monotone and join-uniform on K ⊆ L. Then, f^{ı} : K → L defined as f^{ı}(x) = ∨{y ∈ L | f (y) = f (x)} is extensive and idempotent (i.e., if f^{ı}(x) ∈ K then f^{ı}(f^{ı}(x)) = f^{ı}(x)).

Proof. Extensivity is obvious by definition. Moreover, by join-uniformity, we have that for any x ∈ K such that f^{ı}(x) ∈ K , f^{ı}(f^{ı}(x)) = ∨{y ∈ L | f (y) = f (f^{ı}(x))} = ∨{y ∈ L | f (y) = f (x)} = f^{ı}(x), proving idempotency.

In general, monotonicity of an inverse operator may fail. This is the case of the disjunctive completion, as shown by the following example taken from [Giacobazzi and Ranzato 1998, Example 5.3].

Example 7.5 Consider the abstract domains Sign, A^{+} and A^{±}, all already introduced above. Observe that ℜ_{∪}^{−}(A^{+}) = A^{+}, while ℜ_{∪}^{−}(Sign) = A^{±0}. This shows that the inverse operator of the disjunctive completion refinement is neither monotone nor antimonotone, since A^{+} and A^{±0} are incomparable abstractions of ℘(ZZ). □

By Proposition 7.4, given a lower closure η ∈ lco^{∗}(L) which is join-uniform (on all L), and its associated generalized inverse η^{ı} : L → L, we have that, for any x ∈ L, η(η^{ı}(x)) = η(x) ≤ x and η^{ı}(η(x)) = η^{ı}(x) ≥ x, but the pair η and η^{ı} does not constitute in general a Galois connection, due to the lack of monotonicity of η^{ı}. Clearly, if η^{ı} is monotone, then it is the right-adjoint of η. In this sense, our notion of inverting a refinement does not correspond to the inversion as right-adjoint of the refinement. On the other hand, it is well-known how pervasive the notion of adjunction is in theoretical computer science, and very often the existence of an adjunction is considered as a weak form of inversion (see, e.g., the paradigmatic case of the weak inverse in Hoare’s logic, cf. [Hoare et al. 1987]). Thus, in the following, we will focus on the inversion of a refinement in the sense of adjunctions.

Proposition 7.6 Let L be a complete lattice and f : L → L be a monotone join-uniform operator (where f^{ı} is its generalized inverse). The following statements are equivalent:

(i) f is additive;

(ii) f^{ı} is monotone;

(iii) f^{ı} = f^{r}.

Proof. We prove the following implications.

(i) ⇒ (ii) Let x, y ∈ L such that x ≤ y. Then, by monotonicity of f , f (x) ≤ f (y). Moreover, if for some z ∈ L, f (z) = f (x) then, by additivity, f (z ∨ y) = f (z) ∨ f (y) = f (y). Hence, we have that f^{ı}(x) = ∨{z ∈ L | f (z) = f (x)} ≤ f^{ı}(y) = ∨{u ∈ L | f (u) = f (y)}.

(ii) ⇒ (iii) Both f and f^{ı} are monotone, and, for any x ∈ L, f (f^{ı}(x)) ≤ x and f^{ı}(f (x)) ≥ x. Then, f and f^{ı} constitute a Galois connection on L, and therefore, f^{ı} is the right-adjoint of f .

(iii) ⇒ (i) Because in any adjunction the right-adjoint of a function exists if and only if this function is additive.

The following result shows that, whenever a lower closure admits the right-adjoint, this is always an upper closure, and, therefore, if an abstract domain refinement admits the right-adjoint, this is a simplification operator. Conversely, by duality, the left-adjoint of a simplification operator, when it exists, is always a refinement.

Proposition 7.7 Let L be a complete lattice.

(i) If ρ ∈ lco(L) admits the right-adjoint ρ^{r}, then ρ^{r} ∈ uco(L).

(ii) If ρ ∈ uco(L) admits the left-adjoint ρ^{l}, then ρ^{l} ∈ lco(L).

Proof. We only prove (i), because (ii) follows by duality. As recalled in Section 2.3, in an adjunction on a complete lattice, the left-adjoint is additive and the right-adjoint is co-additive. Thus, let ρ ∈ lco(L) be an additive lower closure that forms an adjunction on L with ρ^{r}. We prove that ρ^{r} is an upper closure. Monotonicity follows by adjunction. Let x ∈ L. Extensivity follows because from ρ(x) ≤ x, we get ρ^{r}(x) ≥ x. Let us now turn to idempotency. By (i) in Section 2.3, we get ρ^{r}(ρ^{r}(x)) ≥ ρ^{r}(x). Thus, let us prove that ρ^{r}(ρ^{r}(x)) ≤ ρ^{r}(x). By definition, ρ^{r}(ρ^{r}(x)) = ∨_{L}{y ∈ L | ρ(y) ≤ ρ^{r}(x)}. Let z ∈ {y ∈ L | ρ(y) ≤ ρ^{r}(x)}. Then, by monotonicity, idempotency, and additivity of ρ, we obtain:

ρ(z) ≤ ρ(∨_{L}{y ∈ L | ρ(y) ≤ x})
= ∨_{L}{ρ(y) ∈ L | ρ(y) ≤ x}
≤ x.

Hence, ρ(z) ≤ x. Thus, we get z ≤ ρ^{r}(ρ(z)) ≤ ρ^{r}(x), and from z ≤ ρ^{r}(x), we therefore obtain the idempotency.

Thus, by the above result, given an abstract domain refinement ℜ ∈ lco(uco(C )), requiring that ℜ admits an inverse on all uco(C ) which in addition is a simplification, is equivalent to requiring that ℜ is additive. However, additivity for ℜ is a quite stronger requirement than join-uniformity, that corresponds to the invertibility of ℜ on all the space uco(C ). For instance, reduced product and disjunctive completion are relevant examples of refinements, which are not additive but still join-uniform (i.e. invertible) under certain nonrestrictive hypotheses on the concrete domain. The reduced product refinement is a paradigmatic case. It is easy to observe that the reduced product is additive if and only if uco(C ) is completely meet-distributive, i.e. a complete Heyting algebra. This latter condition is equivalent to the weaker (finite) distributivity of uco(C ) (cf. [Morgado 1962]), and this holds if and only if the concrete domain C is a complete chain (cf. [Dwinger 1954]). Obviously, being a complete chain for the concrete domain is not a reasonable hypothesis in semantics and program analysis. On the other hand, the general nonadditivity of the disjunctive completion refinement follows from Example 7.5 and Proposition 7.6.

7.4 Reordering Abstract Domains

We have seen that an invertible abstract domain refinement and its inverse does not constitute, in general, an adjunction. This asymmetry can be overcome by considering the lifted complete order induced on the lattice of abstractions by an invertible (i.e. join-uniform) refinement. In fact, dually to what we have seen in logic program semantics, join-uniformity becomes additivity with respect to the lifted complete order. In this way, for a refinement ℜ which, possibly under some conditions on the concrete domain C , is invertible on all uco(C ), by Proposition 7.6, we have that ℜ^{r} = ℜ^{−}, and, in particular, the inverse ℜ^{−} becomes a simplification operator on the lifted order. This is stated by the following consequence of Theorem 5.10, Proposition 7.6 and Proposition 7.7.

[figure: •; •; •; •; •; •; −0; ∅; 0; ZZ; 0+; +]

Figure 10: The abstract domain D.

Corollary 7.8 Let C be a complete lattice, and let ℜ ∈ lco^{∗}(uco(C )) be a refinement which is invertible on uco(C ). Then, (ℜ, uco(C )_{⊑^{ℜ}}, uco(C )_{⊑^{ℜ}}, ℜ^{−}) is an adjunction.

Although being not additive, both the reduced product refinement of Example 7.1 and the disjunctive completion refinement of Example 7.3 are join-uniform under certain weak hypotheses. The following examples show the meaning of the lifted order on abstract domains in these two cases. First, let us recall that if L is a meet semilattice with bottom, then the pseudocomplement of x ∈ L, if it exists, is the (unique) element x^{∗} ∈ L such that x ∧x^{∗} = ⊥ and ∀y ∈ L. (x ∧y = ⊥) ⇒ (y ≤ x^{∗}). In a complete lattice L, if the pseudocomplement x^{∗} exists then x^{∗} = ∨{y ∈ L | x ∧ y = ⊥}. If every x ∈ L has the pseudocomplement, L is called pseudocomplemented (for more details see e.g. [Birkhoff 1967]).

Example 7.9 Giacobazzi et al. [1996] proved that if C is a meet-continuous lattice,^{4} then for each continuous closure X ∈ uco(C ), ↑ X = {Y ∈ uco(C ) | X ⊑ Y } ⊆ uco(C ) is a pseudocomplemented lattice. In particular, uco(C ) itself, which coincides with ↑C , is pseudocomplemented. By the equivalence between closure operators and abstract domains, this result provided the basis for defining the operation of domain complementation in abstract interpretation [Cortesi et al. 1997]. Complementation is an operation which starting from any two abstract domains A, B ∈ uco(C ) such that A ⊑ B (i.e. B ∈ ↑ A), gives as result the most abstract domain A ∼ B whose reduced product with B is A, i.e. (A ∼ B) ⊓ B = A. Hence, the pseudocomplement of B in ↑ A, when it exists, is denoted by A ∼ B, and called complement of B in A (see [Cortesi et al. 1997] for more details). Although a complement A∼B in uco(C ) is defined for any meet-continuous lattice C , continuous closure A and arbitrary B, in order to get that complementation is the inverse of the reduced product refinement on all the space uco(C ), we assume the more restrictive hypothesis that the concrete domain C satisfies the ACC. This condition in fact ensures that A ∼ B exists for any pair A, B ∈ uco(C ) such that A ⊑ B, because C and any closure on C are, respectively, meetcontinuous and continuous. Notice that C may well be thought of as a meaningful abstraction of the actual concrete domain, and in this case, the ACC is not a severe requirement for an abstract domain used in program analysis. It is easy to observe that complementation is the inverse of the reduced product refinement. In fact, for any A ∈ uco(C ), the refinement ℜ_{⊓A} = λX .(A ⊓ X ) ∈ lco(uco(C )) is join-uniform on all uco(C ), because, for any X ∈ uco(C ), A ⊓ X satisfies the ACC, and therefore ↑ (A ⊓ X ) is pseudocomplemented. Moreover, it turns out that the inverse of ℜ_{⊓A} is ℜ_{⊓A}^{−} = λX .(A ⊓ X )∼A, since, for any X ∈ uco(C ), ⊔{Y ∈ uco(C ) | A ⊓ Y = A ⊓ X } is just the complement of A in A ⊓ X . Thus, by Corollary 7.8, reduced product and complementation form an adjunction relatively to the lifted complete order on abstract domains, and ℜ_{⊓A}^{−} is a simplification operator (namely, an upper closure) in the reordered complete lattice of abstract domains ⟨uco(C ), ⊑^{(ℜ⊓A)}⟩. The lifted order between abstract domains induced by some ℜ_{⊓A} allows to give a correct interpretation to its inverse ℜ_{⊓A}^{−}. Consider for instance the abstract domains A^{+} of Figure 8, A_{2} of Figure 9, already considered above, and the abstract domain D of Figure 10. It turns out that ℜ_{⊓A^{+}}^{−} is not monotone with respect to the standard ordering ⊑ which relates abstract domains in terms of their relative precision. In fact, we have that D ⊑ A_{2} ⊑ A^{+}, whilst ℜ_{⊓A^{+}}^{−}(D) = D ∼ A^{+} = {ZZ, −0} is not comparable with ℜ_{⊓A^{+}}^{−}(A_{2}) = A_{2} ∼ A^{+} = {ZZ, 0}, with respect to ⊑. Instead, ℜ_{⊓A^{+}}^{−} becomes monotone with respect to the lifted order ⊑^{(ℜ⊓A_{+} )}, and therefore the optimal bases ℜ_{⊓A^{+}}^{−}(D) and ℜ_{⊓A^{+}}^{−}(A_{2}) are comparable: ℜ_{⊓A^{+}}^{−}(D) ⊑^{(ℜ⊓A_{+} )} ℜ_{⊓A^{+}}^{−}(A_{2}). This relationship reflects the relative power of the domain ℜ_{⊓A^{+}}^{−}(D) = {ZZ, −0} with respect to ℜ_{⊓A^{+}}^{−}(A_{2}) = {ZZ, 0}: when composed with A^{+}, the first resulting in a more precise domain than the latter. □

4A complete lattice C is meet-continuous if for any chain Y ⊆ C and x ∈ C , x ∧ (∨Y ) = ∨_{y∈Y} (x ∧ y) (cf.

[Gierz et al. 1980]).

As observed in the example above, the lifted complete order on abstract domains reflects precisely the relative precision of abstract domains with respect to a given invertible refinement operator: A is more precise than B, in the lifted order for an invertible refinement ℜ, if ℜ(A) is more precise than ℜ(B) in the standard sense, and, whenever they are the same (i.e. ℜ(A) = ℜ(B)), then A is more precise than B in the standard sense.

Example 7.10 Analogously to the above example of reduced product and complementation, the disjunctive completion refinement and its inverse, the least disjunctive basis (cf. Example 7.3), form an adjunction with respect to the lifted order. Thus, because when C is a dual-algebraic completely distributive lattice, ℜ_{∨} is invertible on all uco(C ) (cf. Example 7.3), we get the adjunction (ℜ_{∨}, uco(C )_{⊑^{ℜ∨}} , uco(C )_{⊑^{ℜ∨}} , ℜ_{∨}^{−}). Here again, the inverse ℜ_{∨}^{−} can be interpreted as a simplification operator with respect to ⊑^{ℜ_{∨}}. Now, for the abstract domains Sign and A^{+} considered in Example 7.5, it turns out that ℜ_{∪}^{−}(Sign) ⊑^{ℜ_{∪}} ℜ_{∪}^{−}(A^{+}): in fact, when ℜ_{∪}^{−}(Sign) is refined by the disjunctive completion, provides a more concrete domain than ℜ_{∪}^{−}(A^{+}) does. □

8 Conclusion

In this work, we have introduced the order-theoretic notion of uniform closure operator on complete lattices, and shown that this is the right key property for generalizing the standard hierarchy of declarative semantics for logic programming and to develop a general theory for domain refinement and simplification in abstract interpretation. These results have shown an unexpected relationship between two apparently different fields of application of abstract interpretation. On the one hand, meet-uniformity and abstract interpretation provide the right framework for reordering semantic interpretations of logic programs, keeping into account the relative precision of the models of a program specified at different levels of abstraction in the hierarchy of semantics. On the other hand, the dual property of join-uniformity applied to abstract domain refinements yields the precise characterization of the concept of invertibility for a refinement, and moreover it has been proved that refinements and their inverses constitute an adjunction relatively to a reordered space of abstract domains. Both reordered spaces are based on the same lifted partial order induced by uniformity of the involved closures.

The notion of uniformity might be fruitfully exploited in other areas of application of abstract interpretation, such as in hierarchies of inductive definitions for specifying (non necessarily logic) program semantics and type systems. Inductive definitions are fundamental in mathematical logic and theoretical computer science to provide rule-based presentations of inductively defined sets, or equivalently in the definition of sets generated by closure conditions. In semantics, this is the case for the set of execution traces of a transition system, or more in general, in rulebased specification methods for semantics, e.g. in Plotkin’s [1981] structural operational semantics SOS. As shown by Cousot and Cousot [1992b] and Cousot [1997b], hierarchies of semantics and type systems can be specified as inductive definitions, and related with each other by abstract interpretation. We believe that the order-theoretic reconstruction of the model-theoretic semantics of logic programming presented in the paper can be further generalized by considering, instead of logic programs, generic inductive definitions. The relationship between logic programs and inductive definitions is well-known: while logic programs are finite sets of untyped Horn-clauses, inductive definitions may be given as possibly infinite sets of possibly typed clauses or rules. An account of this analogy can be found in [Bol and Groote 1996]. As observed in Section 6.1, we put no constraint on the structure of programs. In particular, they can be possibly infinite sets of possibly typed clauses, i.e. arbitrary sets of rules. The essential point in our construction is that the space of all models of a program P is a closure m_{P}, and this is just the case of models of inductive definitions (cf. [Aczel 1977]). Thus, in view of our approach, the model-theoretic reconstruction of the semantics of logic programs of Falaschi et al. [1993] might be fully generalized to hierarchies of inductive definitions, and therefore applied to more general rule-based presentations of semantics or type systems related by abstract interpretation.

Acknowledgments

This work was begun while the authors were visiting the LIX, Laboratoire d’Informatique, École Polytechnique, in Paris. They thank the LIX, and in particular Radhia Cousot, for the kind hospitality. The work of Roberto Giacobazzi has been partly supported by the EEC Human Capital and Mobility individual grant “Semantic Definitions, Abstract Interpretation and Constraint Reasoning”, no. ERBCHBICT930822.

References

Aczel, P. 1977. An introduction to inductive definitions. In Handbook of Mathematical Logic, J. Barwise,

Ed. North-Holland, Amsterdam, 739–782. Adaricheva, K. and Gorbunov, V. 1990. Equational closure operator and forbidden semidistributive

lattices. Siberian Math. J. 30, 6, 831–849. Amato, G. and Levi, G. 1997. Properties of the lattice of observables in logic programming. In Pro-

ceedings of the Italian-Portuguese-Spanish Joint Conference on Declarative Programming, (APPIA-GULP-PRODE ’97 ). 175–187.

Apt, K. R. 1990. Introduction to logic programming. In Handbook of Theoretical Computer Science, J. van Leeuwen, Ed. Vol. B: Formal Models and Semantics. Elsevier, Amsterdam, and The MIT Press, Cambridge, Mass., 495–574.

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. Birkhoff, G. 1967. Lattice Theory. AMS Colloquium Publication, 3rd edition. AMS, Providence, R.I. Bol, R. and Groote, J. F. 1996. The meaning of negative premises in transition system specification. J.

ACM 43, 5, 863–914. Bossi, A. and Cocco, N. 1993. Basic transformation operations for logic programs which preserve com-

puted answer substitutions. J. Logic Program. 16, 47–87. Bossi, A., Gabbrielli, M., Levi, G., and Martelli, M. 1994. The s-semantics approach: theory and

applications. J. Logic Program. 19-20, 149–197. Bossi, A., Gabbrielli, M., Levi, G., and Meo, M. 1994. A compositional semantics for logic programs.

Theor. Comput. Sci. 122, 1-2, 3–47. Codish, M., Dams, D., and Yardeni, E. 1994. Bottom-up abstract interpretation of logic programs.

Theor. Comput. Sci. 124, 1, 93–126. 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.

Comini, M. and Levi, G. 1994. An algebraic theory of observables. In Proceedings of the 1994 International Logic Programming Symposium (ILPS ’94 ), M. Bruynooghe, Ed. The MIT Press, Cambridge, Mass., 172–186.

Comini, M., Levi, G., and Meo, M. 1995. Compositionality of SLD-derivations and their abstractions. In Proceedings of the 1995 International Symposium on Logic Programming (ILPS ’95 ), J. Lloyd, Ed. The MIT Press, Cambridge, Mass.

Cortesi, A., Filé, G., Giacobazzi, R., Palamidessi, C., and Ranzato, F. 1997. Complementation in

abstract interpretation. ACM Trans. Program. Lang. Syst. 19, 1, 7–47. 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. 1996. Abstract interpretation. ACM Comp. Surv. 28, 2, 324–328.

Cousot, P. 1997a. Constructive design of a hierarchy of semantics of a transition system by abstract interpretation. In Proceedings of the 13th International Symposium on Mathematical Foundations of Programming Semantics (MFPS ’97 ), S. Brookes and M. Mislove, Eds. Electronic Notes in Theoretical Computer Science, vol. 6. Elsevier, Amsterdam.

Cousot, P. 1997b. Types as abstract interpretations. In Conference Record of the 24th ACM Symposium

on Principles of Programming Languages (POPL ’97 ). ACM Press, New York, 316–331. 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. 1992a. Abstract interpretation and application to logic programs. J. Logic

Program. 13, 2-3, 103–179. Cousot, P. and Cousot, R. 1992b. Inductive definitions, semantics and abstract interpretation. In Con-

ference Record of the 19th ACM Symposium on Principles of Programming Languages (POPL ’92 ). ACM Press, New York, 83–94.

Cousot, P. and Cousot, R. 1994. Higher-order abstract interpretation (and application to comportment 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.

Cousot, P. and Cousot, R. 1995. Compositional and inductive semantic definitions in fixpoint, equational, constraint, closure-condition, rule-based and game-theoretic form. In Proceedings of the 7th International Conference on Computer Aided Verification (CAV ’95 ), P. Wolper, Ed. Lecture Notes in Computer Science, vol. 939. Springer-Verlag, Berlin, 293–308.

Deutsch, A. 1992. Operational models of programming languages and representations of relations on regular languages with application to the static determination of dynamic aliasing properties of data. Ph.D. thesis, University of Paris VI, Paris, France.

Dwinger, P. 1954. On the closure operators of a complete lattice. Indagat. Math. 16, 560–563. van Emden, M. H. and Kowalski, R. A. 1976. The semantics of predicate logic as a programming

language. J. ACM 23, 4, 733–742. Fages, F. and Gori, R. 1996. A hierarchy of semantics for normal constraint logic programs. In Proceed-

ings of the 5th International Conference on Algebraic and Logic Programming (ALP ’96 ), M. Hanus and M. Rodríguez-Artalejo, Eds. Lecture Notes in Computer Science. Springer-Verlag, Berlin, 77–91.

Falaschi, M., Levi, G., Martelli, M., and Palamidessi, C. 1989. Declarative modeling of the operational

behavior of logic languages. Theor. Comput. Sci. 69, 3, 289–318. Falaschi, M., Levi, G., Martelli, M., and Palamidessi, C. 1993. A model-theoretic reconstruction of the

operational semantics of logic programs. Inf. Comput. 103, 1, 86–113. 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. 1998. The powerset operator on abstract interpretations. To appear in Theor.

Comput. Sci. Giacobazzi, R. 1996. “Optimal” collecting semantics for analysis in a hierarchy of logic program se-

mantics. In Proceedings of the 13th International Symposium on Theoretical Aspects of Computer Science (STACS ’96 ), C. Puech, Ed. Lecture Notes in Computer Science, vol. 1046. Springer-Verlag, Berlin, 503–514.

Giacobazzi, R., Palamidessi, C., and Ranzato, F. 1996. Weak relative pseudo-complements of closure

operators. Algebra Universalis 36, 3, 405–412. 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. Complementing logic program semantics. In Proceedings of the 5th International Conference on Algebraic and Logic Programming (ALP ’96 ), M. Hanus and M. Rodríguez-Artalejo, Eds. Lecture Notes in Computer Science. Springer-Verlag, Berlin, 238–253.

Giacobazzi, R. and Ranzato, F. 1997. 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. Optimal domains for disjunctive abstract interpretation. To

appear in Sci. Comput. Program. Gierz, G., Hofmann, K. H., Keimel, K., Lawson, J. D., Mislove, M., and Scott, D. S. 1980. A Com-

pendium of Continuous Lattices. Springer-Verlag, Berlin. Granger, P. 1988. Combinations of semantic analyses. In Proceedings of the 2nd French-Soviet Workshop

on Methods of Compilation and Program Construction, Informatika ’88, P. Deransart, Ed. INRIA, Rocquencourt, France, 71–88.

Hoare, C. A. R., Hayes, I. J., Jifeng, H., Morgan, C. C., Roscoe, A. W., Sanders, J. W., Sorensen, I. H.,

Spivey, J. M., and Sufrin, B. A. 1987. Laws of programming. Comm. ACM 30, 8, 672–686. Jensen, T. 1997. Disjunctive program analysis for algebraic data types. ACM Trans. Program. Lang.

Syst. 19, 5, 751–803. Lassez, J. and Maher, M. 1984. Closures and fairness in the semantics of programming logic. Theor.

Comput. Sci. 29, 167–184. Morgado, J. 1960. Some results on the closure operators of partially ordered sets. Portugal. Math. 19, 2,

101–139. Morgado, J. 1962. On complete congruences of complete lattices. Portugal. Math. 21, 1, 11–25. Muthukumar, K. and Hermenegildo, M. 1991. Combined determination of sharing and freeness of pro-

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

Nielson, F. 1984. Abstract interpretation using domain theory. Ph.D. thesis CST-31/84, University of

Edinburgh, Edinburgh, Scotland. Plotkin, G. 1981. A structural approach to operational semantics. Tech. Rep. DAIMI FN-19, Computer

Science Dept., Aarhus University, Aarhus, Denmark. 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.

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.