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
Advertisements

, ,

  1. Leave a comment

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s

%d bloggers like this: