ON THE LEAST COMPLETE EXTENSION OF A COMPLETE SUBSEMILATTICE

ROBERTO GIACOBAZZI AND FRANCESCO RANZATO

Abstract. For a complete sublattice X of a complete lattice C, we consider the problem of the existence of the least complete meet subsemilattice of C having as least complete extension (i.e. the least complete sublattice of C containing it) X. We argue that this problem is not trivial, and we provide two results that, under certain conditions on C and X, give a positive answer to it.

1. Introduction

For a complete lattice C, let Sub(C) be the complete lattice of complete sublattices of C (containing both the top ⊤_{C} = ∧∅ and the bottom ⊥_{C} = ∨∅), ordered with respect to set inclusion, and let Sub_{∧}(C) be the complete lattice of complete meet subsemilattices of C (containing the top ⊤_{C} = ∧∅), ordered with respect to set inclusion. It is well known that Sub_{∧}(C) is dually isomorphic to the complete lattice uco(C) of all upper closure operators on C, ordered pointwise (cf. [6]). Closure operators play a key rôle in the theory of semantic approximation of programming languages by abstract interpretation: In fact, it is shown in [1] that the lattice of abstract interpretations, or equivalently the lattice of the semantics derivable by abstraction, for an arbitrary program whose data-objects have a complete lattice structure C, is isomorphic to the lattice uco(C). One facility offered by this result is that it is possible to define operators on uco(C) that systematically refine a given semantics, thus getting more concrete (precise) information about the program behavior (cf. [2]). One such operator is the disjunctive completion, that refines a given semantics so that it can express the logical disjunction of properties. From the lattice-theoretic viewpoint, disjunctive completion corresponds to the map providing for any X ∈ Sub_{∧}(C) its least complete extension ℧(X), i.e. the least complete sublattice ℧(X) ∈ Sub(C) of C containing X. A natural question that arises in the abstract interpretation setting is whether it is possible to define the “inverse” operation to disjunctive completion, namely an operation which, starting from any program semantics ρ, gives as result the most abstract semantics η whose disjunctive completion is exactly the same as that of ρ. Such an operation is useful for efficient implementations of the disjunctive completion in a program analysis system (cf. [4]). In lattice-theoretical terms, this would be equivalent to define an operation providing for any complete sublattice X ∈ Sub(C) the least complete meet subsemilattice Ω(X) ∈ Sub_{∧}(C) of C such that ℧(Ω(X)) = ℧(X) holds (whenever this happens, we call Ω(X) the least basis of X). It is worth noting that similar motivations from abstract interpretation theory led in [3] to prove some properties of pseudocomplementation for uco(C). Note that the above problem is not trivial: Also for a simple finite lattice L like that depicted below, least bases cannot exist (for instance, the least basis of L does not exist).

1991 Mathematics Subject Classification. 06A12, 06A15, 06A23.

Key words and phrases. Complete subsemilattice, least complete extension, closure operator.

[figure: •; •; •; •; •; •; •; •; •]

We provide two results assuring the existence of such a least basis. We show that for a dual-algebraic completely distributive lattice C, there exists the least basis of any complete sublattice of C. Moreover, we prove that there exists the least basis of any finite sublattice of a distributive (complete) lattice. Of course, these results can be dualized for complete join subsemilattices.

2. The Results

Let C be a complete lattice. For any X ∈ Sub_{∧}(C), define ℧(X) = ∩{Y ∈ Sub(C) | X ⊆ Y }, i.e. ℧(X) is the least complete sublattice of C containing X. For X ∈ Sub(C), we say that Y ∈ Sub_{∧}(C) is the least basis of X if ℧(Y) = X, and for any Z ∈ Sub_{∧}(C), ℧(Z) = X implies Y ⊆ Z. Obviously, if such Y exists then it is unique. For a complete lattice C, we denote by JI(C) the set of its (completely) join-irreducible elements, i.e. JI(C) = {x ∈ C | ∀S ⊆ C. x = ∨S ⇒ x ∈ S}.

Lemma 2.1 ([5]). Let C be a dual-algebraic complete lattice.

(i) JI(C) is join-generating, i.e. C = {∨S | S ⊆ JI(C)}. (ii) If X ∈ Sub(C) then X is dual-algebraic.

We can now give the results assuring the existence of the least basis.

Theorem 2.2. (a) If C is a dual-algebraic completely distributive lattice, then for any X ∈ Sub(C), {∧S | S ⊆ JI(X)} is the least basis of X.

(b) If C is a distributive complete lattice, then for any finite X ∈ Sub(C), {∧S | S ⊆ JI(X)} is the least basis of X.

Proof. (a) Let X ∈ Sub(C). By Lemma 2.1 (ii), X is dual-algebraic and completely distributive. Thus, by Lemma 2.1 (i), X = {∨S | S ⊆ JI(X)}. Observe that, by complete distributivity of C, if Y ∈ Sub_{∧}(C) then ℧(Y) = {∨S | S ⊆ Y }. Therefore, if ℧(Y) = X then JI(X) ⊆ Y. Hence, {∧S | S ⊆ JI(X)} actually is the least basis of X.

(b) Analogous to (a), since, by finiteness, X is still join-generated by JI(X) and for any Y ∈ Sub_{∧}(C), ℧(Y) = {∨S | S ⊆ Y } still holds.

It is worth noting that the hypotheses of Theorem 2.2 (a) are tight. For distributivity it is enough to consider the lattice L in the Introduction. On the other hand, the complete lattice given by the unit interval [0, 1] of real numbers, which is not dual-algebraic but completely distributive, does not admit the least basis.

Acknowledgments

Comments from the anonymous referee are gratefully acknowledged.

References

[1] P. Cousot and R. Cousot. Systematic design of program analysis frameworks. In Conf. Record of the 6th ACM Symp. on Principles of Programming Languages, pages 269–282. ACM Press, New York, 1979.

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

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

[4] R. Giacobazzi, and F. Ranzato. Optimal domains for disjunctive abstract interpretation. To appear in Sci. Comput. Program., 1998.

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

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

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

  E-mail address: giaco@di.unipi.it

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

  E-mail address: franz@math.unipd.it