SourceForge.net LogoThe Eiffel Compiler / Interpreter (tecomp)

doc/papers/proof/complete lattice

Complete lattices and closure systems

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
 

Emacs suffix

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

- Introduction

- Definition of a complete lattice

- Closures

- Closure systems

- Closure maps

- Closures via ascending monotonic functions

- Some important closure systems

- Predicates

- Some facts about relations

- Closures with relations

- Definition of a closure system

- Verification of the closure system

- Closure of sets and elements

- Closures with functions

- Emacs suffix


ip-location