# Introduction

Complete lattices are important because of their connection to closure

systems. Closure systems arise in many cases.

Some examples:

1. Graphs: If we have a graph we often use the phrase “All the nodes reachable

from a specific node”. A set of nodes of a graph which contains all reachable

nodes is a closed set and the collection of all such sets is a closure system.

2. Grammars: If we define a formal language e.g. via a context free grammar we

define a set of terminals, a set of nonterminals, a start symbol and a set of

production rules. We define a sentential form to be a string of grammar

symbols which can be produced from the start symbol by using zero or more

production rules. The language of a grammar are all the string of terminal

symbols which can be produced from the start symbol. It turns out that a set

of strings of grammar symbols which contain all producible strings from any of

the strings within the set is a closed set and the collection of all such sets

is a closure system.

3. Transitive closures: For any relation we can define a transitive and a

reflexive transitive closure. The set of all transitive (or reflexive

transitive) relations are closure systems as well. We often use the wording:

“We have a relation r and define the relation rtrans to be the least

transitive relation which contains r”.

Many more examples can be found. But these three should be sufficient to see

the importance of closure system.

Closure systems are best studied within the abstract setting of a complete

lattice. A complete lattice is a minimal structure with sufficient properties

to define the basic structures of closure systems and give a lot of proofs.

# Definition of a complete lattice

A complete lattice is a lattice where each set of elements has an infimum and

a supremum.

deferred class COMPLETE_LATTICE inherit LATTICE end

feature -- Lattice operations and axioms * (a,b:CURRENT): CURRENT deferred end + (a,b:CURRENT): CURRENT deferred end <= (a,b:CURRENT): BOOLEAN ensure Result = (a=a*b) end = (a,b:CURRENT): BOOLEAN deferred end all(a,b,c:CURRENT) deferred ensure a=b => a~b a*b = b*a a+b = b+a a*b*c = a*(b*c) a+b+c = a+(b+c) a = a*(a+b) a = a+(a*b) end end

feature -- Definitions for set of elements <= (a:CURRENT, p:CURRENT?): ghost BOOLEAN ensure Result = all(x) x in p => a<=x end <= (p:CURRENT?, a:CURRENT): ghost BOOLEAN ensure Result = all(x) x in p => x<=a end low_set(p:CURRENT?): ghost CURRENT? ensure Result = {x: x<=p} end up_set(p:CURRENT?): ghost CURRENT? ensure Result = {x: p<=x} end is_minimum(a:CURRENT, p:CURRENT?): ghost BOOLEAN ensure Result = (a in p and a<=p) end is_maximum(a:CURRENT, p:CURRENT?): ghost BOOLEAN ensure Result = (a in p and p<=a) end is_infimum(a:CURRENT, p:CURRENT?): ghost BOOLEAN ensure Result = a.is_maximum(p.low_set) end is_supremum(a:CURRENT, p:CURRENT?): ghost BOOLEAN ensure Result = a.is_minimum(p.up_set) end end

feature -- Supremum and infimum infimum(p:CURRENT?): CURRENT deferred end supremum(p:CURRENT?): CURRENT deferred end 0: CURRENT ensure Result = (0:CURRENT?).supremum end 1: CURRENT ensure Result = (0:CURRENT?).infimum end all(p:CURRENT?) deferred ensure p.infimum.is_infimum(p) p.supremum.is_supremum(p) end end

# Closures

## Closure systems

A closure system is a set of elements of the complete lattice which is closed

under arbitrary meet operations. I.e. the meet “a*b” of any two elements “a”

and “b” of the closure system is in the closure system and also the infimum of

each subset of the closure system (a meet of arbitrary elements of the closure

system) is an element of the closure system. Since the second condition

(arbitrary meets) implies the first one (any meets of two elements) we use the

stronger to define a closure system.

feature is_closure_system(p:CURRENT?): ghost BOOLEAN -- Is the set `p' a closure system, i.e. is `p' closed under -- arbitrary meet operations? ensure Result = all(q:CURRENT?) q<=p => q.infimum in p end end

Being a closure system is a rather abstract property of a set. In specific

closure systems the elements of a closure system can be sets which are closed

with respect to a certain property, i.e. a closure system can be a set of

sets. But within the context of the module “complete_lattice” a closure system

is just a set of elements. Even in this abstract setting we can prove some

important facts about closure systems.

A closure system must contain the top element.

all(p:CURRENT?) require r1: p.is_closure_system check c1: 0:CURRENT? <= p -- the empty set is a subset of any set c2: (0:CURRENT?).infimum in p -- c1, def "is_closure_system" ensure 1 in p -- def "1", c2 end

In the following we define a closure operation and show that a closure

operation maps any element “a” to the least element of a closure system which

is above “a”.

For any element “a” we can define the set {x:a<=x} to represent the set of all

elements above “a”. Let “p” be a closure system. Then “p*{x:a<=x}” is the set

of all elements of “p” which are above “a” (the “*” operator on sets is

intersection). This set is clearly a subset of “p”. Therefore the infimum of

this set is in “p”. We define the closure operation as

feature closed(a:CURRENT, p:CURRENT?): ghost CURRENT -- The closure of `a' with respect to the set `p'. ensure Result = (p * {x:a<=x}).infimum end end

The function “closed” can be applied to any set “p”. In general “closed” is

ascending and monotonic in its first argument. If the set “p” is a closure

system the function is idempotent as well.

First we prove that “closed” is ascending in its first argument, i.e. it

always selects a greater equal element.

feature closed_ascending: all(a:CURRENT, p:CURRENT?) check c1: a = {x:a<=x}.infimum -- general law c2: all(p,q:CURRENT?) p<=q => q.infimum<=p.infimum -- general law: infimum reverses order c3: {x:a<=x}.infimum <= (p*{x:a<=x}).infimum -- c2 c4: a <= (p*{x:a<=x}).infimum -- c1, c3 ensure a <= a.closed(p) -- c4, def "closed" end end

Next we prove that “closed” is monotonic in its first argument, i.e. a

“greater” element gets a “greater” closure.

feature closed_monotonic: all(a,b:CURRENT, p:CURRENT?) require r1: a<=b check c1: {x:b<=x} <= {x:a<=x} -- r1, transitivity "<=" c2: all(p,q,r:CURRENT?) q<=r => p*q<=p*r -- general law c3: p*{x:b<=x} <= p*{x:a<=x} -- c1,c2 c4: (p*{x:a<=x}).infimum <= (p*{x:b<=x}).infimum -- c3, infimum reverses order ensure a.closed(p) <= b.closed(p) -- c4, def "closed" end end

For more properties of “closed” we need to exploit the fact that the second

argument is a closure system. We can prove that the function “closed” always

selects one element of a closure system.

feature closed_selects: all(a:CURRENT, p:CURRENT?) require r1: p.is_closure_system check c1: p*{x:a<=x} <= p -- trivial c2: (p*{x:a<=x}).infimum in p -- c1, r1, def "is_closure_system" ensure a.closed(p) in p end end

Next we see that any element of a closure system is mapped to itself.

feature closed_maps_p2p: all(a:CURRENT, p:CURRENT?) require r1: p.is_closure_system r2: a in p check c1: a <= a.closed(p) -- closed_ascending c2: a in {x:a<=x} -- trivial c3: a in p*{x:a<=x} -- r2,c2 c4: (p*{x:a<=x}).infimum <= a -- c3, infimum in low_set c5: a.closed(p) <= a -- c4, def "closed" ensure a.closed(p) = a -- c1,c5 end end

The last two assertions are sufficient to show that the closure operation is

idempotent.

feature closed_idempotent: all(a:CURRENT, p:CURRENT?) require r1: p.is_closure_system check c1: a.closed(p) in p -- r1, closed_selects ensure a.closed(p).closed(p) = a.closed(p) -- c1, closed_maps_p2p end end

In the last step we can convince ourselves that “a.closed(p)” selects the least

element of the closure system “p” which is above “a”.

feature closed_selects_least: all(a,b:CURRENT, p:CURRENT?) require r1: p.is_closure_system check c1: a.closed(p) in {x:a<=x} -- closed_ascending c2: a.closed(p) in p -- closed_selects c3: a.closed(p) in p*{x:a<=x} -- c1,c2 c4: all(b) require r2: b in p r3: b in {x:a<=x} check c5: b.closed(p)=b -- closed_maps_p2p c6: a<=b -- r3 c7: a.closed(p)<=b.closed(p) -- closed_monotonic ensure a.closed(p) <= b -- c5,c7 end ensure a.closed(p).is_minimum(p*{x:a<=x}) -- c3,c4 end end

## Closure maps

In the previous chapter we defined a closure operation via a closure

system. The reverse is possible and equally powerful. We can define properties

for a closure map and can define a closure system as the range of a closure

map.

feature is_closure_map(f:CURRENT->CURRENT): ghost BOOLEAN ensure Result = ( f.is_total and f.is_ascending and f.is_monotonic and f.is_idempotent ) end end

The function “x->x.closed(p)” is a closure map provided that “p” is a closure

system. It is total in its first argument, it is ascending, monotonic and

idempotent as proved in the previous chapter.

Now we want to prove that any function which satisfies the above properties

defines uniquely a closure system.

feature closure_system_via_map: all(f:CURRENT->CURRENT) require r1: f.is_closure_map check c0: all(p:CURRENT?) require r2: p <= f.range check c1: p.infimum <= f[p.infimum] -- r1, f.is_ascending c2: p.image(f) = p -- r2, f.is_idempotent c3: all(x) require r3: x<=p check c4: f[x]<=p.image(f) -- f.is_monotonic ensure f[x]<=p -- c4,c2 end c5: f[p.infimum]<=p -- c3, infimum in low_set c6: f[p.infimum]<=p.infimum -- c5, p.infimum is maximum -- of low_set c7: f[p.infimum] = p.infimum -- c1,c6 c8: some(x) f[x] = p.infimum -- c7, witness p.infimum ensure p.infimum in f.range -- c8 end ensure f.range.is_closure_system -- c0, def "is_closure_system" end end

The concept of a closure system and a closure map is equivalent. Each closure

system defines a closure map via the function “closed” and each closure map

defines a closure system by its range.

## Closures via ascending monotonic functions

A closure map is a total function which is ascending, monotonic and

idempotent. The range of a closure map is a closure system.

A total function which is ascending and monotonic is not yet a closure map. But

we can construct a closure system from a total ascending and monotonic

function.

We are within the context of a complete lattice. Therefore any total ascending

function “f” must have fixpoints. A complete lattice has a top element “1” and

since the top element is the maximum of all elements it has to be a fixpoint

of f, i.e. f[1]=1. We can prove that the set of all fixpoints “f.fixpoints” is

a closure system. In order to prove this we have to show that the infimum of

any subset of fixpoints is again a fixpoint.

feature fixpoint_lemma: all(f:CURRENT->CURRENT, p:CURRENT?) require r1: f.is_total r2: f.is_ascending r3: f.is_monotonic r4: p = f.fixpoints check c0: all(q:CURRENT?) require r5: q<=p check c1: q.image(f) = q -- r4,r5 c2: q.infimum <= q -- def "infimum" c3: f[q.infimum] <= q.image(f) -- c2,r3 c4: f[q.infimum] <= q -- c1,c3 c5: f[q.infimum] <= q.infimum -- c4, def "infimum" c6: q.infimum <= f[q.infimum] -- r2 c7: f[q.infimum] = q.infimum -- c5,c6 ensure q.infimum in p -- c7 end ensure p.is_closure_system -- c0 end end

With this we a have third method to get a closure of an arbitrary element “a”

of a complete lattice. If we have a total, ascending and monotonic function

“f”, then

a.closed(f.fixpoints)

returns the least fixpoint with is greater equal “a”. The already proved

assertion “closed_selects_least” and the fact that “f.fixpoints” is a closure

system for a total, ascending and monotonic function guarantees this.

feature all(a:CURRENT, f:CURRENT->CURRENT) require r1: f.is_total r2: f.is_ascending r3: f.is_monotonic check c1: f.fixpoints.is_closure_system -- fixpoint_lemma ensure a.closed(f.fixpoints).is_minimum(f.fixpoints*{x:a<=x}) -- c1, closed_selects_least end end -- Note: f.fixpoints*{x:a<=x} is the set of fixpoints of f above a.

# Some important closure systems

## Predicates

The type PREDICATE[G] is a complete lattice. Each predicate defines a set. And

each set of sets has an infimum (the intersection of all sets) and an supremum

(the union of all sets).

-- module: predicate immutable class PREDICATE[G] inherit BOOLEAN_LATTICE redefine <= end COMPLETE_LATTICE redefine <=, 0, 1 end end feature -- all usual lattice and boolean lattice features ... -- see article "Predicates as sets" end feature -- Infimum and supremum infimum(pp:CURRENT?): CURRENT -- The intersection of all sets in `pp'. ensure Result = {x:G: all(p) p in pp => x in p} end supremum(pp:CURRENT?): CURRENT -- The union of all sets in `pp'. ensure Result = {x:G: some(p) p in pp and x in p} end end

In this framework it is possible to define closed sets.

## Some facts about relations

The type [G,G]? is a shorthand for PREDICATE[G,G] which is a shorthand for

PREDICATE[ [G,G] ] i.e. the set of tuples [G,G]. I.e. [G,G]? is an

endorelation over G.

If we have a set s:G? and a relation r:[G,G]? we sometimes want to define the

set which contains “s” and all elements which are reachable from “s” via the

relation “r”.

Some functions on relations.

feature -- Functions of relations domain(r:[G,G]?): ghost G? -- The domain of the relation `r'. ensure Result = {x:G: some(y:G) [x,y] in r} end range(r:[G,G]?): ghost G? -- The range of the relation `r'. ensure Result = {x:G: some(y:G) [x,y] in r} end image(p:G?, r:[G,G]?): ghost G? -- The image of the set `p' under the relation `r' ensure Result = {y:G: some(x:G) x in p and [x,y] in r} end preimage(p:G?, r:[G,G]?): ghost G? -- The preimage of the set `p' under the relation `r' ensure Result = {x:G: some(y:G) y in p and [x,y] in r} end all(r:[G,G]?, p:G?) ensure p.image(r) <= r.range -- def "image", "range" p.preimage(r) <= r.domain -- def "preimage", "domain" end end

The functions “p:G?->p.image(r)” and “p:G?->p.preimage(r)” are monotonic. We

give a proof for the first one. The proof for the second is similar.

feature all(r:[G,G]?) check c1: all(p,q:G?) require r1: p<=q check c2: all(b:G) require r2: b in p.image(r) check c3: some(a:G) a in p and [a,b] in r c4: all(a:G) require r3: a in p r4: [a,b] in r check c5: a in q -- r3,r1 c6: some(a:G) a in q and [a,b] in r -- c5, r4 ensure b in q.image(r) end ensure b in q.image(r) -- c3,c4 end ensure p.image(r) <= q.image(r) -- c2 end ensure (p:G? -> p.image(r)).is_monotonic -- c1 end end

## Closures with relations

### Definition of a closure system

We can use a relation to define a closure system.

feature is_closed(p:G?, r:[G,G]?): ghost BOOLEAN -- Is the set `p' closed with respect to the relation `r'? ensure Result = all(a,b:G) a in p => [a,b] in r => b in p end closure_system(r:[G,G]?): ghost G?? -- The closure system generated from the relation `r'. ensure Result = {p:G?: p.is_closed(r)} end

The predicate “p.is_closed(r)” says that whenever there is an element “a” in

“p” and there is an element “b” such that “[a,b] in r”, then “b” is in “p” as

well. We call such a set “p” a set closed with respect to the relation “r”.

### Verification of the closure system

It is easy to verify that “p.is_closed(r)” is equivalent “p.image(r)<=p”

all(p:G?, r:[G,G]?) require r1: p.image(r) <= p check c0: all(a,b:G) require r2: a in p r3: [a,b] in r check c1: some(x:G) x in p and [x,b] in r -- r2,r3 c2: b in p.image(r) -- c1, def "image" ensure b in p -- c2,r1 end ensure p.is_closed(r) -- c0 end all(p:G?, r:[G,G]?) require r1: p.is_closed(r) check c0: all(y:G) require r2: y in p.image(r) check c1: some(x:G) x in p and [x,y] in r -- r2 c2: all(x:G) x in p and [x,y] in r => y in p -- r1 ensure y in p -- c1,c2 end ensure p.image(r) <= p -- c0 end end

We define for any relation “r” the function “p:G?->p+p.image(r)”. This

function adds to each set “p” the set of all elements which can be reached in

one step using the relation “r”. If we can add nothing more, i.e. “p.image(r)”

is already a subset of “p”, then we have reached a fixpoint of the function.

It is evident that this function is total and ascending. The monotonicity can

be verified by using the monotonicity of “image”.

feature all(r:[G,G]?, f:G?->G?) require r1: f = (p->p+p.image(r)) check c1: all(p,q:G?) require r2: p<=q check c2: p.image(r) <= q.image(r) -- "image" is monotonic ensure f[p]<=f[q] -- r2,c2 end ensure f.is_total -- evident from definition f.is_ascending -- evident from definition f.is_monotonic -- c1 end end

The fixpoints of “p->p+p.image(r)” form a closure system which is the same as

the result of the above define function “r.closure_system”.

feature all(r:[G,G]?, f:G?->G?) require r1: f = (p->p+p.image(r)) check c1: f.fixpoints = {p:G?: p.image(r)<=p} -- evident c2: {p:G?: p.image(r)<=p} = {p:G?, p.is_closed(r)} -- see above proof that p.image(r)<=p and p.is_closed(r) -- are equivalent c3: {p:G?: p.is_closed(r)} = r.closure_system -- def "closure_system" ensure f.fixpoints = r.closure_system -- c1,c2,c3 end end

### Closure of sets and elements

Since any relation defines uniquely a closure system, we can close any set of

elements (even singleton sets) with respect to any relation using the

following functions.

feature closed(p:G?, r:[G,G]?): ghost G? -- The set `p' closed with respect to the relation `r'. ensure Result = p.closed(r.closure_system) end closed(a:G, r:[G,G]?): ghost G? -- The set {a} closed with respect to the relation `r'. ensure Result = {a}.closed(r) -- {a} is a shorthand for {x:G: x~a} end end

Note that each of these functions returns the least set which is closed under

the relation “r”.

## Closures with functions

Since functions are relations we can use functions as well to close sets. A

function f:G->G defines the relation

feature relation(f:G->G): ghost [G,G]? -- The relation defined by the function `f'. ensure Result = {a,b: a in f.domain and b~f[a]} end closed(p:G?, f:G->G): ghost G? -- The set `p' closed under the function `f'. ensure Result = p.closed(f.relation) end closed(a:G, f:G->G): ghost G? -- The set {a} closed under the function `f'. ensure Result = {a}.closed(f.relation) end end