The Eiffel Compiler / Interpreter (tecomp)

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.

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

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

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.

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.

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.

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

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

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

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

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

Local Variables: mode: outline coding: iso-latin-1 outline-regexp: "=\\(=\\)*" End: