Algebra Universalis, 36 (1996) 405-412 0002-5240/96/030405-08$01.50 + 0.20/0 \begin{matrix}c \\ ◯ \end{matrix}1996 Birkhäuser Verlag, Basel

Weak relative pseudo-complements of closure operators

R. Giacobazzi, C. Palamidessi and F. Ranzato

Abstract. We define the notion of weak relative pseudo-complement on meet semi-lattices, and we show that it is strictly weaker than relative pseudo-complementation, but stronger than pseudo-complementation. Our main result is that if a complete lattice L is meet-continuous, then every closure operator on L admits weak relative pseudo-complements with respect to continuous closure operators on L.

1. Introduction

Closure operators have been widely used in various fields of theoretical computer science, like semantics of declarative languages and program analysis. In particular, Cousot and Cousot proved in [3] 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 lattice structure L, is isomorphic to the lattice uco(L) of the upper closure operators on L. One facility offered by this result is that the meet operation in uco(L) can be applied to compose semantics, thus getting more concrete (precise) information about the program behavior. A natural question that arises in this setting is whether it is possible to define the inverse operation, namely an operation which, starting from two semantics ρ and η for the same program, with ρ more abstract than η, gives as result the most abstract semantics φ whose composition with ρ is exactly η. Such an operation would be useful to isolate properties of ρ which are not shared by η. In terms of closure operators this amounts to define an operation analogous to the relative pseudo-complement, the only difference is that we require φ to be the maximum of the set of closure operators whose meet with ρ is equal to η, instead than smaller than or equal to η. It is easy to see that if the relative pseudocomplement of ρ w.r.t. η exists, then it is the intended element. The converse is not true.

Presented by E. T. Schmidt

Received April 24, 1995; accepted in final form March 4, 1996.

We define the notion described above as a partial operation (which we call weak relative pseudo-complement) on arbitrary meet semi-lattices. We investigate conditions on L under which pairs of elements in uco(L) admit the weak relative pseudocomplement. In particular, we are interested in the case in which L is a complete lattice (in which case also uco(L) is a complete lattice). Our main result is that the weak relative pseudo-complement of a closure operator ρ w.r.t. η, for η continuous, always exists when L is a meet-continuous complete lattice (i.e., when in L the meet preserves the join of chains). In [2], this result is applied to static program analysis.

Note that the pseudo-complement is a particular case of weak relative pseudocomplement, hence the meet-continuity of L also guarantees that uco(L) is pseudocomplemented. On the other hand, the meet-continuity of L is much less restrictive than the condition under which uco(L) is relatively pseudo-complemented. In fact, in a complete lattice, relative pseudo-complementation is equivalent to complete meetdistributivity ([1]), and complete meet-distributivity in uco(L) is equivalent to distributivity ([6]). Now, for uco(L) to be distributive, it is necessary and sufficient that L is a complete well-ordered chain ([4]). This condition is also necessary and sufficient for uco(L) to be complemented ([7]).

2. Weak relative pseudo-complement

Before defining our notion of weak relative pseudo-complement, we first recall some basic notions and terminology. We refer to [1, 5] for all the notions recalled in the paper.

Let L = ⟨L, ⪯, ∧, ∨, ⊤, ⊥⟩ be a complete lattice, where L is a set, ⪯ is the partial ordering relation, ∧ is the meet, ∨ is the join, ⊤ is the top element and ⊥ is the bottom element. The complete lattice L is completely meet-distributive if for each x ∈ L and Y ⊆ L, x ∧ ⋁ Y = ⋁_{y∈Y} (x ∧ y) holds. Given x, y ∈ L, the relative pseudo-complement of x w.r.t. y, if it exists, is the (unique) element x ∗ y ∈ L such that x ∧ x ∗ y ⪯ y, and for each z ∈ L, if x ∧ z ⪯ y then z ⪯ x ∗ y. If x ∗ y exists for every x, y ∈ L, then L is relatively pseudo-complemented. It is well known that this property holds iff L is completely meet-distributive. The element x ∗ ⊥, if it exists, is called the pseudo-complement of x, and it is denoted by x^{∗}. If x^{∗} exists for every x ∈ L, then L is pseudo-complemented. Obviously, (relative) pseudo-complementation is definable for a mere meet semi-lattice.

DEFINITION 2..1. Let L = ⟨L, ⪯, ∧⟩ be a meet semi-lattice, and let x, y ∈ L with y ⪯ x. The weak relative pseudo-complement of x w.r.t. y, if it exists, is the (unique) element wr(x, y) ∈ L such that (i) x ∧ wr(x, y) = y,

(ii) for each z ∈ L, if x ∧ z = y then z ⪯ wr(x, y).

If wr(x, y) exists for every x, y ∈ L such that y ⪯ x, then L is weakly relatively pseudo-complemented. □

The reason why we require y ⪯ x, in the definition of wr(x, y), is that for y ⪯̸ x Condition (i) would never be satisfied.

In the context of Definition 2..1, note that for y ⪯ x Condition (i) could equivalently be rewritten as x ∧ wr(x, y) ⪯ y; the difference with the notion of relative pseudo-complement (within the case y ⪯ x) is only that in Condition (ii) we require x ∧ z = y instead of x ∧ z ⪯ y. It is easy to see that for y ⪯ x, if x ∗ y exists then wr(x, y) = x ∗ y (hence in that case, if L is a complete lattice then wr(x, y) can be defined as the join of all the elements z satisfying the premise of Condition (ii)). The converse is not true. For instance the following lattice is weakly relatively pseudocomplemented, but a ∗ d does not exist (while wr(a, d) = b.)

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

Concerning the relation with the pseudo-complement, we have that if wr(x, ⊥) exists, then it coincides with x^{∗}. However, a pseudo-complemented lattice may not be weakly relatively pseudo-complemented. For instance, the following lattice is pseudocomplemented, but wr(b, e) does not exist.

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

3. Weak relative pseudo-complements of closure operators

In this section, we study the conditions for the existence of weak relative pseudocomplements of closure operators. An (upper) closure operator on L is a mapping ρ : L → L such that x ⪯ ρ(x), ρ(ρ(x)) = ρ(x), and for every x, y ∈ L, if x ⪯ y then ρ(x) ⪯ ρ(y) (obviously, this notion can be given in general for posets). As usual, we say that ρ is continuous if for every chain C ⊆ L, ρ(⋁ C) = ⋁_{x∈C} ρ(x) holds. A closure operator ρ is uniquely determined by the set of its fixpoints, which coincides with its image ρ(L). A set X ⊆ L is the set of fixpoints of some closure operator iff X contains ⊤ and it is meet-closed, i.e. for any Y ⊆ X, with Y ≠ ∅, ⋀ Y ∈ X holds.

Let uco(L) be the set of all closure operators on L. We will denote by uco(L) the complete lattice ⟨uco(L), ⊑, ⊓, ⊔, ℧, ι⟩ where ρ ⊑ η iff for each x ∈ L, ρ(x) ⪯ η(x), (⊓_{i∈I}ρ_{i})(x) = ⋀_{i∈I} ρ_{i}(x), (⊔_{i∈I}ρ_{i})(x) = x iff for each i ∈ I, ρ_{i}(x) = x, and ℧(x) = ⊤ and ι(x) = x. Note that ρ ⊑ η iff η(L) ⊆ ρ(L). Note also that the set of fixpoints of ⊓_{i∈I}ρ_{i} is the smallest meet-closed set which contains all the fixpoints of each ρ_{i}, and that the set of fixpoints of ⊔_{i∈I}ρ_{i} is the intersection of all the sets of fixpoints of the ρ_{i}’s, i.e. (⊔_{i∈I}ρ_{i})(L) = ⋂_{i∈I} ρ_{i}(L).

We recall that a complete lattice L is meet-continuous if for any chain C ⊆ L, and for each element x ∈ L, x ∧ ⋁ C = ⋁_{y∈C}(x ∧ y) holds. It is worth noting that meet-continuity is strictly weaker than complete meet-distributivity. For instance, any finite lattice is meet-continuous, but not necessarily completely meet-distributive (i.e. distributive). Also an infinite lattice can be meet-continuous without being completely meet-distributive: consider, for instance, the ordinal sum of an ω-chain and a finite non-distributive lattice.

The following theorem expresses the main result of this paper. We prove that if L is a meet-continuous complete lattice, then uco(L) admits weak relative pseudocomplements w.r.t. continuous closure operators. In the proof, ordinal numbers will be denoted by greek letters α, β, . . ..

THEOREM 3..1. If L is a complete, meet-continuous lattice then for every ρ, η ∈ uco(L) such that η ⊑ ρ and η is continuous, there exists wr(ρ, η).

Proof. For ρ, η ∈ uco(L) such that η ⊑ ρ and η is continuous, let P_{ρη} = {φ ∈ uco(L) : ρ ⊓ φ = η}, and define ρ̄ = ⊔P_{ρη}. Notice that ρ̄(L) = ⋂{φ(L) : φ ∈ P_{ρη}}. We prove that ρ̄ = wr(ρ, η). Clearly φ ⊑ ρ̄ for every φ ∈ P_{ρη}. Furthermore, η ⊑ ρ ⊓ ρ̄ holds, because P_{ρη} contains η. Hence, we have only to show that ρ ⊓ ρ̄ ⊑ η, which amounts to prove that η(L) ⊆ (ρ ⊓ ρ̄)(L).

Assume that there exists x̄ ∈ η(L) such that x̄ ∉ (ρ ⊓ ρ̄)(L). We show that for each ordinal α we are able to construct a strictly increasing chain {x_{β}}_{β≤α} in η(L). Since the cardinality of this chain is |α|, this leads to a contradiction when |α| > |η(L)|.

More precisely, we prove by transfinite induction on α that it is possible to construct in η(L) two sets {x_{β}}_{β≤α}, with x_{0} = x̄, and {y_{β}}_{β<α}, such that:

(i) {x_{β}}_{β≤α} is a strictly increasing chain in η(L) \ (ρ ⊓ ρ̄)(L),
(ii) ∀β < α. y_{β} ∈ ρ(L),
(iii) x_{0} = x_{α} ∧ (⋀_{β<α} y_{β}), and
(iv) ∀β, γ. β ≤ γ < α ⇒ x_{β} ≺ y_{γ}.

Let us consider the three cases α = 0, α successor ordinal, and α limit ordinal.

(α = 0) Define x_{0} = x̄. Then x_{0} ∈ η(L) \ (ρ ⊓ ρ̄)(L) by definition, thus (i) is satisfied. Conditions (ii), (iii) and (iv) are vacuously satisfied.

(α + 1) By the induction hypothesis (i), x_{α} ∉ ρ̄(L), hence there exists a closure operator φ ∈ P_{ρη} such that x_{α} ∉ φ(L). Also, again by the induction hypothesis (i), x_{α} ∉ ρ(L) and x_{α} ∈ η(L). By the latter and the fact that ρ ⊓ φ = η, we derive x_{α} ∈ (ρ⊓φ)(L). Therefore, there must exist x ∈ φ(L)\ρ(L) and y ∈ ρ(L)\φ(L) such that x_{α} = x ∧ y. Define x_{α+1} = x and y_{α} = y, and observe that (ii) and (iv) are satisfied. We prove now (iii). By the induction hypothesis (iii), we have x_{0} = x_{α} ∧ (⋀_{β<α} y_{β}), hence we derive x_{0} = x_{α+1} ∧ y_{α} ∧ (⋀_{β<α} y_{β}) = x_{α+1} ∧ (⋀_{β<α+1} y_{β}). Concerning (i), observe that x_{α} ⪯ x_{α+1}, and x_{α} ≠ x_{α+1}, since x_{α} ∉ φ(L) while x_{α+1} ∈ φ(L). Furthermore, x_{α+1} ∈ η(L) since φ(L) ⊆ η(L). Finally, note that the term ⋀_{β<α+1} y_{β} in (iii) is an element of ρ(L), being ρ(L) meet-closed. Since ρ(L) ⊆ (ρ ⊓ ρ̄)(L), and (ρ ⊓ ρ̄)(L) is meet-closed, we deduce that x_{α+1} cannot belong to (ρ ⊓ ρ̄)(L), otherwise also x_{0} would.

(α limit ordinal) Define x_{α} = ⋁_{β<α} x_{β}. Conditions (ii) and (iv) are trivially satisfied by the corresponding induction hypothesis. Consider now (iii). By the induction hypothesis (iii), we have that, for any β < α, x_{0} = x_{β} ∧ (⋀_{γ<β} y_{γ}) holds. Hence, we derive x_{0} = ⋁_{β<α}(x_{β} ∧ (⋀_{γ<β} y_{γ})). By the induction hypothesis (iv), for β ≤ γ < α, x_{β} ⪯ y_{γ} holds. Therefore, we have x_{0} = ⋁_{β<α}(x_{β}∧(⋀_{β≤γ<α} y_{γ})∧(⋀_{γ<β} y_{γ})) = ⋁_{β<α}(x_{β}∧(⋀_{γ<α} y_{γ})), from which we get, by meet-continuity, x_{0} = (⋁_{β<α} x_{β}) ∧ (⋀_{γ<α} y_{γ}) = x_{α} ∧ (⋀_{γ<α} y_{γ}). Finally, we show (i). Since all the elements of {x_{β}}_{β<α} are distinct, also x_{α} is strictly greater than x_{β}, for any β < α. Furthermore, x_{α} ∈ η(L): in fact η(x_{α}) = η(⋁_{β<α} x_{β}) = (by continuity of η) = ⋁_{β<α} η(x_{β}) = (since, by the induction hypothesis (i), x_{β} ∈ η(L), i.e. η(x_{β}) = x_{β}) = ⋁_{β<α} x_{β} = x_{α}. The proof that x_{α} ∉ (ρ ⊓ ρ̄)(L) is like in the case of α successor ordinal. □

In the above theorem, the meet-continuity of L and the continuity of η play a fundamental role. The following example shows that if η is not continuous, then wr(ρ, η) might not exist, even if L is meet-continuous.

EXAMPLE 3..2. Consider the complete, meet-continuous lattice L obtained as direct product of the two elements chain {0, 1} and the (ω+1)-chain IN^{ω} = {0, 1, …, ω}. Consider the closure operators ρ and η such that ρ(L) = {⟨1, x⟩ : x ∈ IN^{ω}}, and η(L) = L \ {⟨0, ω⟩}. Clearly, η is not continuous. For any k ∈ IN, consider the closure operator ρ_{k} such that ρ_{k}(L) = {⟨0, n⟩ : n ∈ IN, k ≤ n} ∪ {⟨1, ω⟩}, and observe that for each k, ρ ⊓ ρ_{k} = η. Define ρ̂ = ⊔_{k∈IN}ρ_{k}, and observe that wr(ρ, η), if it exists, must be greater than or equal to ρ̂. But ρ̂(L) = {⊤}, and therefore ρ ⊓ ρ̂ = ρ, which is strictly greater than η. □

Vice-versa, if L is not meet-continuous, then wr(ρ, η) might not exist, even if η is continuous.

EXAMPLE 3..3. Consider the lattice L defined as in the previous example, but with the element ⟨0, ω⟩ removed. In this case, L is not meet-continuous. The same lattice is used in [8, page 16] as an example of a distributive complete lattice which is not pseudo-complemented. To see that uco(L) is not weakly relatively pseudocomplemented just define ρ, the ρ_{k}’s, and ρ̂ as in the previous example, and observe that for any k, we have ρ ⊓ ρ_{k} = ι, but ρ ⊓ ρ̂ = ρ, namely wr(ρ, ι) does not exist. □

The following are easy consequences of Theorem 3..1.

COROLLARY 3..4. If L is meet-continuous then uco(L) is pseudo-complemented.

COROLLARY 3..5. If L does not have infinite ascending chains, then for any ρ, η ∈ uco(L), with η ⊑ ρ, there exists wr(ρ, η).

One might, at this point, raise the question whether uco(L) satisfies the Stone identity (namely, for every ρ ∈ uco(L), ρ^{∗} ⊔ ρ^{∗∗} = ℧), in case the conditions for it to be pseudo-complemented hold. Next example answers this question negatively.

EXAMPLE 3..6. Let L be the following lattice:

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

Consider the closure operator ρ on L for which ρ(L) = {⊤, a, b, ⊥}. It is clear that ρ^{∗}(L) = {⊤, c, d, ⊥} and ρ^{∗∗} = ρ. Thus, the Stone identity does not hold since (ρ^{∗} ⊔ ρ^{∗∗})(L) = {⊤, ⊥}. □

We conclude by observing that the hypothesis of meet-continuity of L could be weaken. Given a complete lattice L = ⟨L, ⪯, ∧, ∨, ⊤, ⊥⟩, and η ∈ uco(L), the structure η(L) = ⟨η(L), ⪯, ∧⟩ is a complete meet-sublattice of L. Furthermore, η(L) is indeed a complete lattice, but, in general, not a complete sublattice of L, because the join in η(L) may be different from ∨. However, it is easy to show that if η is continuous, then the join of chains in η(L) is the same as in L. Thus, in the hypotheses of Theorem 3..1, one could replace the condition of meet-continuity of L (used in the limit ordinal case) with the condition of meet-continuity of η(L). The present formulation of the theorem can then be retrieved as a consequence, by observing that if L is meet-continuous and η ∈ uco(L) is continuous, then η(L) is meet-continuous (an analogous result is proved in [5] for algebraic complete lattices).

Acknowledgments

We would like to thank Gilberto Filé who contributed to arouse our interest in studying pseudo-complements of closure operators.

REFERENCES

[1] Birkhoff, G., Lattice Theory. AMS Colloquium Publications vol. XXV, 3rd edition, 1967.

[2] Cortesi, A., Filé, G., Giacobazzi, R., Palamidessi, C. and Ranzato, F., Complementation in abstract interpretation. In A. Mycroft, ed., Proc. of the 2nd Static Analysis Symposium, Lecture Notes in Computer Science 983, pp. 100–117. Springer-Verlag, 1995.

[3] Cousot, P. and Cousot, R., Systematic design of program analysis frameworks. In Conference Record of the 6th ACM Symposium on Principles of Programming Languages, pp. 269–282. ACM Press, 1979.

[4] Dwinger, P., On the closure operators of a complete lattice. Indagationes Math., 16(1954), 560–563.

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

[6] Morgado, J., On complete congruences of complete lattices. Portugal. Math., 21(1)(1962), 11–25.

[7] Morgado, J., Note on complemented closure operators of complete lattices. Portugal. Math., 21(3)(1962), 135–142.

[8] Varlet, J., Contribution à l’étude des treillis pseudo-complémentés et des treillis de Stone. Mémoires de la Société Royale des Sciences de Liège, 5eme série, 8(4), 71 pages, 1963.

R. Giacobazzi

Dipartimento di Informatica, Università di Pisa Corso Italia 40, I-56125 Pisa, Italy e-mail: giaco@di.unipi.it

C. Palamidessi

Dipartimento di Informatica, Università di Genova Via Dodecaneso 35, I-16146 Genova, Italy e-mail: catuscia@disi.unige.it

F. Ranzato

Dipartimento di Matematica Pura ed Applicata Università di Padova Via Belzoni 7, 35131 Padova, Italy e-mail: franz@math.unipd.it