Binary Relations, Endorelations and Transitive Closures

Introduction

Relations are an important vehicle to write specifications. In this article we
study some properties of binary relations. First we start from binary
relations in general with domain, range, composition, images etc.

In the second part we study endorelations i.e. binary relations where the type
of the domain and the range are the same. The most important endorelations are
transitive relations. Transitive relations have a close connection to closure
systems.

All of the presented material in this article is part of the module
`predicate’ because relations are just predicates over tuples i.e. set of
tuples.

Binary relations

A binary relation between the type G and the type H has the type [G,H]?,
i.e. it is a set of tuples, where the first element is an object of type G and
the second element is an object of type G.

In order to express the basic functions and properties we need some generic
types as placeholders for any type.

  feature
      E,F,G,H: ANY
  end

Domain and range

Each relation has a domain (the set of all objects which can serve as a first
component of a pair of the relation) and a range (the set of all objects which
can serve as a second component of a pair of the relation).

  domain(r:[G,H]?): ghost G?
          -- The domain of the relation `r'.
      ensure
          Result = {x:G: some(y:H) [x,y] in r}
      end

  range(r:[G,H]?): ghost G?
          -- The range of the relation `r'.
      ensure
          Result = {y:H: some(x:G) [x,y] in r}
      end

Inverse

For any relation and for each collection of relations we can define a unique
inverse.

  feature
      inverse(r:[G,H]?): [H,G]?
              -- The inverse of the relation `r'.
          ensure
              Result = {y,x: [x,y] in r}
          end

      inverse(rr:[G,H]??): [H,G]??
              -- The collection of all inverse relations of `rr'.
          ensure
              Result = {r: r.inverse in rr}
          end
  end

Note that [G,H]? is a set of tuples and [G,H]?? is a set of set of tuples,
i.e. a set of relations.

The function “inverse” is an involution.

  inverse_involution:
  all(r:[G,H]?)
      check
          r.inverse.inverse
          =
          {y:H,x:G: [x,y] in r}.inverse    -- def "inverse"
          =
          {x:G,y:H: [x,y] in r}           -- def "inverse"
          =
          r
      ensure
          r.inverse.inverse = r
      end

The same applies to any collection of relations.

  inverse_involution:
  all(rr:[G,H]??)
      check
          rr.inverse.inverse
          =
          {r:[H,G]?: r.inverse in rr}.inverse    -- def "inverse"
          =
          {r:[G,H]?: r.inverse.inverse in rr}    -- def "inverse"
          =
          {r:[G,H]?: r in rr}                  -- inverse_involution
          =
          rr
      ensure
          rr.inverse.inverse = rr
      end

Furthermore “inverse” is monotonic.

  
  inverse_monotonic:
  all(r,s:[G,H]?)
      require
          r1: r<=s     -- "<=" is the subset relation,
                       -- i.e. `r' is contained in `s'
      check
          c1: all(x:G,y:H)
              require
                  r2: [x,y] in r.inverse
              check
                  c2: [y,x] in r      -- r2
                  c3: [y,x] in s      -- c2,r1
              ensure
                  [x,y] in s.inverse   -- c3
              end
      ensure
          r.inverse<=s.inverse
      end

For any collection of relations the infimum/supremum commutes with inverse

  invers_commutes_limits:
  all(rr:[G,H]??)
      check
          c1:
          rr.infimum.inverse
          =
          {x:G,y:H: all(r:[G,H]?) r in rr => [x,y] in r}.inverse
          =
          {y:H,x:G: all(r:[G,H]?) r in rr => [x,y] in r}
          =
          {y:H,x:G: all(r:[H,G]?) r in rr.inverse => [y,x] in r}
          =
          rr.inverse.infimum
      ensure
          rr.infimum.inverse = rr.inverse.infimum     -- c1
          rr.supremum.inverse = rr.inverse.supremum   
              -- c1 with "all,=>" replaced by "some,and"
      end

Since “x*y={x,y}.infimum” and “x+y={x,y}.supremum” we get the following laws.

  inverse_commutes_order:
  all(r,s:[G,H]?)
      check
          c1:
          (r*s).invers
          = {r,s}.infimum.inverse               -- def "*"
          = {r,s}.inverse.infimum               -- inverse_commutes_limits
          = {r.inverse,s.inverse}.infimum       -- def "inverse" on collection
          = r.inverse*s.inverse                 -- def "*"

          -- Note: {r,s} is a shorthand for {t:[G,H]?: t=s or t=r}
      ensure
          (r*s).inverse = r.inverse*s.inverse   -- c1
          (r+s).inverse = r.inverse+s.inverse   -- c1 with infimum replaced
                                                --    by supremum
      end

Composition

We can define the composition of two binary relations.

  | (r:[F,G]?, s:[G,H]?): ghost [F,H]?
          -- The relation `r' composed with the relation `s'.
      ensure
          Result = {x:F,z:H: some(y:G) [x,y] in r and [y,z] in s}
      end

The composition is associative

  composition_associative:
  all(r:[E,F]?, s:[F,G]?, t:[G,H]?)
      check
          r|s|t
          =
          {u:E,w:G: some(v:F) [u,v] in r and [v,w] in s} | t
          =
          {u:E,x:H: some(w:G) (some(v:F) [u,v] in r and [v,w] in s) 
                              and [w,x] in t}
          =
          {u:E,x:H: some(v:F,w:G) [u,v] in r and [v,w] in s and [w,x] in t}
          =
          {u:E,x:H: some(v:F) [u,v] in r and 
                              some(w:G) [v,w] in s and [w,x] in t}
          =
          r | {v:F,x:H: some(w:G) [v,w] in s and [w,x] in t}
          =
          r|(s|t)
      ensure
          r|s|t = r|(s|t)
      end

The prove is simple if one remembers the basic laws

  all[G](x:G, e:BOOLEAN) x in {y:G: e} = e[y:=x]

  all[G](e1,e2:BOOLEAN) 
      (some(x:G) e1) and e2 = (some(x:G) e1 and e2)
          -- x does not occur free in e2!

The operation “inverse” distributes over composition.

  inverse_distributes_composition:
  all(r:[F,G]?, s:[G,H]?)
      check
          (r|s).inverse
          =
          {x:F,z:H: some(y:G) [x,y] in r and [y,z] in s}.inverse
          =
          {z:H,x:F: some(y:G) [x,y] in r and [y,z] in s}
          =
          {z:H,x:F: some(y:G) [z,y] in s.inverse and [y,x] in r.inverse}
          =
          s.inverse|r.invers
      ensure
          (r|s).inverse = s.invers|r.inverse
      end

Images and preimages

Unlike a function where each argument is mapped to a unique value, a relation
does not map one element of its domain to only one element of its range. It
maps each element of its domain to a set of elements of the range. We can
define a function “image” which maps each element `x’ to a set of elements. If
`x’ is not in the domain of the relation then set is empty.

In the following we define the image for an element and the image for a set of
elements and the corresponding preimage functions.

  image(x:G, r:[G,H]?): ghost H?
          -- The image of `x' under the relation `r'.
      ensure
          Result = {y:H: [x,y] in r}
      end

  image(p:G?, r:[G,H]?): ghost H?
          -- The image of the set `p' under the relation `r'.
      ensure
          Result = {y:H: some(x:G) x in p and [x,y] in r}
      end

  preimage(y,H, r:[G,H]?): ghost H?
          -- The preimage of `y' under the relation `r'.
      ensure
          Result = y.image(r.inverse)
      end

  preimage(q:H?, r:[G,H]?): ghost H?
          -- The preimage of the set `q' under the relation `r'.
      ensure
          Result = q.image(r.inverse)
      end

The image operator is monotonic in both arguments. First we prove that
“p.image(r)” is monotonic in “p”.

  image_monotonic_in_set:
  all(p,q:G?, r:[G,H]?)
      require
          r1: p<=q
      check
          c1: all(y:H)
              require
                  r2: y in p.image(r)
              check
                  c2: some(x:G) x in p and [x,y] in r   -- r2
                  c3: all(x:G)
                      require
                          r3: x in p
                          r4: [x,y] in r
                      check
                          c4: x in q    -- r3,r1
                      ensure
                          some(x:G) x in q and [x,y] in r  -- c4,r4
                      end
                  c5: some(x:G) x in q and [x,y] in r   -- c2,c3
              ensure
                  y in q.image(r)    -- c5
              end
      ensure
          p.image(r) <= q.image(r)   -- c1
      end

Next we prove that “p.image(r)” is monotonic in “r”.

  image_monotonic_in_relation:
  all(p:G?, r,s:[G,H]?)
      require
          r1: r<=s
      check
          c1: all(y:H)
              require
                  r2: y in p.image(r)
              check
                  c2: some(x:G) x in p and [x,y] in r
                  c3: all(x:G)
                      require
                          r3: x in p
                          r4: [x,y] in r
                      check
                          c4: [x,y] in s   -- r4,r1
                      ensure
                          some(x:G) x in p and [x,y] in s   -- r3,c4
                      end
                  c5: some(x:G) x in p and [x,y] in s   -- c2,c3
              ensure
                  y in p.image(s)   -- c5
              end
      ensure
          p.image(r)<=p.image(s)    -- c1
      end

Next we can see that containment of relations can be decided by containment
of the images.

  all(r,s:[G,G]?)
      require
          r1: all(x:G) x.image(r)<=x.image(s)
      check
          c1: all(x,y:G)
              require
                  r2: [x,y] in r
              check
                  c2: y in x.image(r)   -- r2
                  c3. y in x.image(s)   -- c2,r1
              ensure
                  [x,y] in s            -- c3
              end
      ensure
          r<=s       -- c1
      end

Similar proofs can be done for the preimage operator.

Furthermore any set `p’ in the domain of a relation `r’ mapped through the
image operator and then back through the premage operator results in a
superset of `p’.

  all(r:[G,H]?, p:G?)
      require
          r1: p<=r.domain
      check
          c0: all(x:G)
              require
                  r2: x in p
              check
                  c1: some(y:H) [x,y] in r    -- r1,r2
                  c2: all(y:H)
                      require
                          r3: [x,y] in r
                      ensure
                          some(z:G,y:H) z in p and [z,y] in r and [x,y] in r
                              -- r3,r2, witness [x,y]
                      end

                  c3: some(z:G,y:H) z in p and [z,y] in r and [x,y] in r
                          -- c1,c2
                  c4: some(y:H) y in p.image(r) and [x,y] in r  -- c3
              ensure
                  x in p.image(r).preimage(r)   -- c4
              end
      ensure
          p<=p.image(r).preimage(r)   -- c0
      end

With the same reasoning it is possible to proof the dual law

  all(r:[G,H]?, q:H?)
      require
          q in r.range
      ensure
          q <= q.preimage(r).image(r)  -- proof similar to proof above
      end

Domain/range restrictions of relations

We can restrict the domain or the range of a relation and get a restricted
relation.

  feature
      <: (p:G?, r:[G,H]?): [G,H]?
              -- The relation `r' restricted to the domain `p'
          ensure
              Result = {x:G,y:H: [x,y] in r and x in p}
          end

      <-:(p:G?, r:[G,H]?): [G,H]?
              -- The relation `r' without the domain `p'
          ensure
              Result = (-p)<:r
          end

      :> (r:[G,H]?, q:H?): [G,H]?
              -- The relation `r' restricted to the range `q'
          ensure
              Result = {x:G,y:H: [x,y] in r and y in q}
          end

      <-:(r:[G,H]?, q:H?): [G,H]?
              -- The relation `r' without the range `q'
          ensure
              Result = r:>(-q)
          end
  end

The restriction and substraction of domain or range respectively are
complementary operations which split the relation into two disjoint
complementary subrelations.

  feature
      all(r:[G,H]?, p:G?, q:H?)
          ensure
                  -- proof:  def `<:', def `<-:'
              p<:r + p<-:r = r
              p<:r * p<-:r = 0

              r:>q + r:->q = r
              r:>q * r:->q = 0
          end
  end

Some obvious laws for the domains and ranges of restricted relations.

  feature
      all(r:[G,H]?, p:G?, q:H?)
          ensure
                  -- Proofs: Just expand the definitions of "<:", ":>",
                  --         "domain", "range", "image" and "preimage"
              (p<:r).domain = p
              (p<:r).range  = p.image(r)

              (r:>q).range  = q
              (r:>q).domain = q.preimage(r)
          end
  end

A subrelation `r’ of a relation `s’ remains a subrelation if we substract a
set `p’ from the domain of `s’ which is disjoint from the domain of `r’.

  all(r,s:[G,H]?, p:G?)
      require
          r1: r<=s
          r2: p*r.domain = 0
      check
          all(x:G,y:H)
              require
                  r3: [x,y] in r
              check
                  c1: x in r.domain   -- r3
                  c2: not (x in p)    -- c1,r2
                  c3: [x,y] in s      -- r3,r1
              ensure
                  [x,y] in (p<-:s)    -- c2,c3
              end
      ensure
          r <= p<-:s
      end

The same applies to range substraction.

  all(r,s:[G,H]?, q:H?)
      require
          r1: r<=s
          r2: q*r.range = 0
      check
          all(x:G,y:H)
              require
                  r3: [x,y] in r
              check
                  c1: y in r.range    -- r3
                  c2: not (y in q)    -- c1,r2
                  c3: [x,y] in s      -- r3,r1
              ensure
                  [x,y] in (s:->q)    -- c2,c3
              end
      ensure
          r <= s:->q
      end

Functional relations

A binary relation is functional if for all pairs [x,y] and [x,z] implies that
y is identical to z.

  is_functional(r:[G,H]?): ghost BOOLEAN
          -- Is the relation `r' functional?
      ensure
          Result = all(x:G,y,z:H) [x,y] in r => [x,z] in r => y=z
      end

If a relation is functional, it is possible to convert the relation to a
function.

  feature
       function(r:[G,H]?): ghost G->H
           require
               r.is_functional
           ensure
               Result = (agent(a) 
                            require
                                a in r.domain
                            ensure
                                [a,Result] in r
                            end)
           end
  end

The result of the anonymous function is defined by the property it has to
satisfy. This specification of a function is valid only if it is provable that
there exists an object which satisfies the specification and that the object
is unique. I.e. the following proof is needed.

  all(r:[G,H]?, a:G)
      require
         r1: r.is_functional
         r2: a in r.domain
      ensure
         some(b:H) [a,b] in r                        -- r2
         all(x,y:H) [a,x] in r => [a,y] in r => x=y  -- r1, def "is_functional"
      end

Since the proof requires just to expand the definition of `is_functional’, it
can be done automatically by the system.

If a relation is functional then whenever two images are disjoint, the
corresponding preimages have to be disjoint as well. Here is a detailed proof
of this statement.

  functional_disjoint_preimages:
  all(r:[G,H]?, p,q:H?)
     require
         r1: r.is_functional
         r2: p*q = 0
     check
         all(x:G)
             require
                 r3: x in p.preimage(r)
                 r4: x in q.preimage(r)
             check
                 c1: some(y:H) [x,y] in r and y in p   -- r3
                 c2: some(z:H) [x,z] in r and z in q   -- r4
                 c3: all(y:H)
                     require
                         r5: [x,y] in r
                         r6: y in p
                     check
                         c4: all(z:H)
                             require
                                 r7: [x,z] in r
                                 r8: z in q
                             check
                                 c5: y  = z   -- r1,r5,r7
                                 c6: y /= z   -- r6,r8,r2
                             ensure
                                 False    -- c5,c6
                             end
                     ensure
                         False    -- c2,c4
                     end
             ensure
                 False   -- c1,c3
             end
     ensure
         p.preimage(r)*q.preimage(r) = 0
     end

There is another law for functional relations.

  all(r:[G,H]?, q:H?)
      require
          r.is_functional
          q<=r.range
      ensure
          q = q.preimage(r).image(r)
             -- `<=' true in general (chapter images and preimages)
             -- `>=' proof see below
      end

In general `q<=q.preimage(r).image(r)’ is valid (see chapter about images and
preimages). It remains to be proved that `q’ is a superset in the case of a
functional relation.

  all(r:[G,H]?, q:H?)
      require
          r1: r.is_functional
      check
          c1: all(y:H)
              require
                  r2: y in q.preimage(r).image(r)
              check
                  c2: some(x:G,z:H) z in q and [x,z] in r and [x,y] in r -- r2
                  c3: all(x:G,z:H)
                      require
                          r3: z in q
                          r4: [x,z] in r
                          r5: [x,y] in r
                      check
                          c4: y=z  -- r4,r5,r1
                      ensure
                          y in q   -- r3,c4
                      end
              ensure
                  y in q
              end
      ensure
          q.preimage(r).image(r) <= q   -- c1
      end

Endorelations

A binary relation is an endorelation if the type of the domain is the same as
the type of the range.

Properties of endorelations

The most important properties of endorelations are reflexivity, transitivity
and symmetry. It is easy to define these properties formally.

  is_reflexive(r:[G,G]?): ghost BOOLEAN
         -- Is the relation `r' reflexive?
      ensure
         Result = all(x:G) [x,x] in r
      end

  is_transitive(r:[G,G]?): ghost BOOLEAN
         -- Is the relation `r' transitive?
      ensure
         Result = all(x,y,z:G) [x,y] in r => [y,z] in r => [x,z] in r
      end
  
  is_symmetric(r:[G,G]?): ghost BOOLEAN
         -- Is the relation `r' symmetric?
      ensure
         Result = (r=r.inverse)
      end

Duality

For endorelations we have an important duality principle which states whenever
a relation is reflexive, transitive or symmetric the inverse relation satisfies
the corresponding property.

  er_1:
  all(r:[G,G]?)
      ensure
          r.is_reflexive   => r.inverse.is_reflexive

          r.is_transitive  => r.inverse.is_transitive

          r.is_symmetric   => r.inverse.is_symmetric
      end

The proofs for reflexivity and symmetry are trivial. We spell out a proof for
transitivity.

  all(r:[G,G]?)
      require
          r1: r.is_transitive
      check
          c1: all(x,y,z:G)
              require
                  r2: [x,y] in r.invers
                  r3: [y,z] in r.invers
              check
                  c2: [z,y] in r        -- r3
                  c3: [y,x] in r        -- r2
                  c4: [z,x] in r        -- c2,c3,r1
              ensure
                  [x,z] in r.invers     -- c4
              end
      ensure
          r.invers.is_transitive   -- c1
      end

Transitivity and restricted relations

We claim that any restriction (domain or range) of a transitive relation
results in a transitive relation.

  er_2:
  all(r:[G,G]?, p:G?)
      require
          r1: r.is_transitive
      check
          all(x,y,z)
              require
                  r2: [x,y] in (p<:r)
                  r3: [y,z] in (p<:r)
              check
                  c1: [x,y] in r   -- r2
                  c2: x in p       -- r2
                  c3: [y,z] in r   -- r3
                  c4: [x,z] in r   -- c1,c3,r1
              ensure
                  [x,z] in (p<:r)  -- c4,c2
              end
      ensure
          (p<:r).is_transitive
      end
  er_3:
  all(r:[G,G]?, q:G?)
      require
          r1: r.is_transitive
      check
          all(x,y,z)
              require
                  r2: [x,y] in (r:>q)
                  r3: [y,z] in (r:>q)
              check
                  c1: [x,y] in r   -- r2
                  c2: [y,z] in r   -- r3
                  c3: z in q       -- r3
                  c4: [x,z] in r   -- c1,c2,r1
              ensure
                  [x,z] in (r:>q)  -- c4,c3
              end
      ensure
          (r:>q).is_transitive
      end

Transitivity and images

We call a set `p’ closed under a relation `r’ if it satisfies the following
predicate.

  is_closed(p:G?, r:[G,G]?): ghost BOOLEAN
          -- Is the set `p' closed under the relation `r'?
      ensure
          Result = all(x,y:G) [x,y] in r => x in p => y in p
      end

All images of a transitive relation `r’ are closed under the relation `r’.

  er_4:
  all(p,q:G?, r:[G,G]?)
      require
          r1: r.is_transitive
          r2: q = p.image(r)
      check
          c1: all(y,z:G)
              require
                  r3: [y,z] in r
                  r4: y in q
              check
                  c2: some(x:G) x in p and [x,y] in r  -- r4,r2
                  c3: all(x:G)
                      require
                          r5: x in p
                          r6: [x,y] in r
                      check
                          c4: [x,z] in r    -- r6,r3,r1
                      ensure
                          z in q     -- r5,c4,r2
                      end
              ensure
                  z in q   -- c2,c3
              end
      ensure
          q.is_closed(r)   -- c1
      end

The same applies to the union of a set `p’ with its image under `r’.

  er_4a:
  all(p,q:G?, r:[G,G]?)
      require
          r1: r.is_transitive
          r2: q = p.image(r)
      check
          c1: all(x,y:G)
              require
                  r3: [x,y] in r
                  r4: x in (p+q)
              check
                  c2: x in p or x in q   -- r4
                  c3: x in p => y in q   -- r2
                  c4: x in q => y in q   -- r2,r1,er_4
                  c5: y in q             -- c2,c3,c4
              ensure
                  y in (p+q)    -- c5
              end
      ensure
          (p+q).is_closed(r)    -- c1
      end

Closure systems

The set of all reflexive relations, the set of all symmetric relations and the
set of all transitive relations are closure systems. Recall that a set is a
closure system if arbitrary intersections of elements remain within the set
(for more details please read the article “Complete lattices and closure
systems).

Let us state the properties first.

  er_5:
  all(rr:[G,G]??)
      ensure
         rr={r: r.is_transitive} => rr.is_closure_system  -- proof see below

         rr={r: r.is_reflexive}  => rr.is_closure_system
             -- def "is_closure_system", "infimum", "is_reflexive"

         rr={r: r.is_symmetric}  => rr.is_closure_system
             -- def "is_closure_system", "infimum", "is_symmetric"
      end

The most important closure system is the set of transitive relations. We give
a formal proof that the set of transitive relations form a closure system (the
proof for reflexive and symmetric relations is similar). The proof is spelled
out in detail in the following.

  all(rr:[G,G]??)
      require
          r1: rr = {r: r.is_transitive}
      check
          c1: all(ss:[G,G]??)
              require
                  r2: ss<=rr
              check
                  c2: all(x,y,z:G)
                      require
                          r3: all(r:[G,G]?) r in ss => [x,y] in r
                          r4: all(r:[G,G]?) r in ss => [y,z] in r
                      check
                          c3: all(r:[G,G]?)
                              require
                                  r5: r in ss
                              check
                                  c4: r.is_transitive   -- r5,r2
                                  c5: [x,y] in r        -- r5,r3
                                  c6: [y,z] in r        -- r5,r4
                              ensure
                                  [x,z] in r            -- c4,c5,c6
                              end
                      ensure
                          all(r:[G,G]?) r in ss => [x,z] in r
                      end
                  c7: {x,y:G: all(r:[G,G]?) 
                                       r in ss 
                                       => [x,y] in r}.is_transitive  -- c2
                  c8: s.infimum.is_transitive  -- c7,def "infimum"
              ensure
                  ss.infimum in rr     -- c8,r1
              end
      ensure
          rr.is_closure_system    -- c1, def "is_closure_system"
      end

The proof seems complicated at first glance because it contains all detailed
steps. But it is just an expansion of the definitions of “is_closure_system”,
“infimum”, and “is_transitive”. Since it requires just the expansion of
defintions and some simple algebraic transformations, the proof can be done by
the system automatically.

Transitive closures

Transitive relations with logical implication

The boolean operation `=>’ is transitive. This can be used to create the
transitive relation `{x,y:G: e => e[x;=y]}’ over any type G with the help of a
boolean expression `e’ with one free variable.

  tc_1:
  all(r:[G,G]?, e:BOOLEAN)
      require
          r1: r = {x,y: e => e[x:=y]}
      check
          c1: all(x,y,z:G)
              require
                  r2: [x,y] in r
                  r3: [y,z] in r
              check
                  c2: e       => e[x:=y]   -- r2,r1
                  c3: e[x:=y] => e[x:=z]   -- r3,r1
                  c4: e       => e[x:=z]   -- c2,c3
              ensure
                  [x,z] in r    -- c4,r1
              end
      ensure
          r.is_transitive   -- c1
      end

Inheriting properties via relations and transitive closures

In the article “complete lattices and closure systems” we have given a
definition for the statement that a set `p:G?’ is closed under a relation
`r:[G,G]?’

  p.is_closed(r) = all(x,y) x in p => [x,y] in r => y in p

  -- or equivalent
  p.is_closed(r) = all(x) x in p => (x.image(r)<=p)

This definition says that the relation `r’ inherits the property of an element
`x’ of being in `p’ to all elements in its image.

If we rewrite the definition of `p.is_closed(r)’ slightly we can verify the
following assertion.

  tc_2:
  all(r,rp:[G,G]?, p:G?)
      require
          r1: rp = {x,y: x in p => y in p}
      check
          c1: (r<=rp) = all(x,y:G) [x,y] in r => x in p => y in p
                   -- def "<=", r1
      ensure
          rp.is_transitive           -- r1, tc_1
          p.is_closed(r) = (r<=rp)   -- c1, def "is_closed"
      end

This assertions states that the relation `{x,y: x in p => y in p}’ is a
transitive relation and that the statement `p.is_closed(r)’ is equivalent to
`r’ being a subset of this relation.

From this we can conclude immediately that if `p’ is closed under a relation
`r’ then it is closed under any subset of `r’ as well.

  tc_3:
  all(r,s:[G,G]?, p:G?)
      require
          r1: p.is_closed(r)
          r2: s<=r
      check
          c1: r<={x,y: x in p => y in p}   -- r1, tc_2
          c2: s<={x,y: x in p => y in p}   -- r2,c1
      ensure
          p.is_closed(s)    -- c2, tc_2
      end

This proof is straighforward, because `s’ is a subset of `r’ and the subset
relation is transitive. But we can prove the closedness under the transitive
closure of `r’ which is a superset of `r’ as well.

We claim that if a set `p’ is closed under a relation `r’ then its closed
under the transitive closure `rc’ as well.

  tc_4:
  all(r,rc,rp:[G,G]?, p:G?)
      require
          r1: p.is_closed(r)
          r2: rc = r.closed(is_transitive)
          r3: rp = {x,y: x in p => y in p}
      check
          c1: rp.is_transitive    -- r3, tc_1
          c2: r  <= rp            -- r1, tc_2
          c3: rc <= rp            -- c1,c2,r2
      ensure
          p.is_closed(rc)         -- c3, tc_2
      end

This proof is based on the crucial fact that the transitive closure of a
relation `r’ is the least relation which is transitive and contains `r’. Since
`rp’ is transitive and contains `r’ by `tc_2′, `rc’ must be less or equal
`rp’ which implies that `p’ is closed under the transitive closure as well.

Reachability via a relation

If we have a set `p’ of elements of type G and a relation `r:[G,G]?’ then we
can ask the question which elements can be reached from `p’ via `r’ in zero or
more steps. This set can be calculated via a closure operation as demonstrated
in the paper “Complete lattices and closure systems” by the expression
`pc=p.closed(r)’.

Since `pc’ is calculated via a closure operation it is the least set which
contains `p’ and is closed under the relation `r’.

From tc_4 we can conclude doing the closure operation with `r’ and doing it
with its transitive closure must yield the same result.

  tc_5:
  all(r,rc:[G,G], q,qc:G?)
      require
          r1: rc = r.closed(is_transitive)
          r2: qc = q.closed(r)
      check
          c1: all(p:G?) q<=p => q.is_closed(r) => qc<=q  
                                  -- r2, closure is least set
          c2: qc.is_closed(r)     -- r2
          c3: qc.is_closed(rc)    -- c2, tc_4
          c4: all(p:G?)
              require
                  r3: q<=p
                  r4: q.is_closed(rc)
              check
                  c5: q.is_closed(r)   -- r4, r1, tc_3
              ensure
                  qc<=q                -- r3,c5,c1
              end
          c6: qc = q.closed(rc)        -- c3,c4
      ensure
          q.closed(r) = q.closed(rc)  -- r2,c6
      end

Equivalent expressions for transitive closures

We want to show that the relations

  r.closed(is_transitive)

  {x,y: y in x.image(r).closed(r)}

are equivalent. We proof this by

  tc_6:
  all(r,s,rc:[G,G]?)
      require
          rc = r.closed(is_transitive)
          s  = {x,y: y in x.image(r).closed(r)}
      check
          rc <= s    -- lemma_1 below
          s  <= rc   -- lemma_2 below
      ensure
          rc = s
      end

The following `lemma_1′ proves that `s’ is transitive and includes `r’ and
therefore must be a superset of `rc’.

  lemma_1:
  all(r,s:[G,G]?)
      require
          r1: s  = {x,y: y in x.image(r).closed(r)}
          r2: rc = r.closed(is_transitive)
      check
          c1: all(x,y,z:G)
              require
                  r2: [x,y] in s
                  r3: [y,z] in s
              check
                  c2: y in x.image(r).closed(r)  -- r2
                  c3: z in y.image(r).closed(r)  -- r3
                  c4: z in x.image(r).closed(r)  -- c2,c3,closure is monotonic
              ensure
                  [x,z] in s    -- c4
              end
          c5: s.is_transitive   -- c1
          c6: all(x,y)
              require
                  r4: [x,y] in r
              check
                  c7: y in x.image(r)           -- r4
                  c8: y in x.image(r).closed(r) -- c7, closure is ascending
              ensure
                  [x,y] in s    -- c8
              end
          c9: r<=s   -- c6
      ensure
          rc <= s   -- c5,c9,r2
      end

The following `lemma_2′ shows that a transitive closure `rc’ of a relation `r’
always produces closed images (under the relation `r’) and every image under
`rc’ contains the corresponding image under `r’ and therfore must contain the
corresponding images of `s’ which are least sets by definition.

  lemma_2:
  all(r,s,rc:[G,G]?)
      require
          r1: rc = r.closed(is_transitive)
          r2: s = {x,y: y in x.image(r).closed(r)}
      check
          c0: all(x:G)
              check
                  c1: r<=rc                       -- r1
                  c2: x.image(r) <= x.image(rc)   -- c1, image monotonic
                  c3: x.image(rc).is_closed(rc)   -- r1, er_4
                  c4: x.image(rc).is_closed(r)    -- c3, tc_5
                  c5: x.image(r).closed(r) <= x.image(rc)  -- c2,c4
              ensure
                  x.image(s) <= x.image(rc)   -- c5,r2
              end
      ensure
          s <= rc   -- c0
      end

Equivalent expressions for closed sets

We want to show that the sets

  p.closed(r)

  p + p.image(r.closed(is_transitive))

are equivalent. Proof:

  tc_7:
  all(p,pc:G?, r,rc:[G,G]?)
      require
          pc = p.closed(r)
          rc = r.closed(is_transitive)
      check
          pc <= p + p.image(rc)   -- lemma_1 below
          p + p.image(rc) <= pc   -- lemma_2 below
      ensure
          pc = p + p.image(rc)
      end
  lemma_1:
  all(p,pc:G?, r,rc:[G,G]?)
      require
          r1: pc = p.closed(r)
          r2: rc = r.closed(is_transitive)
      check
          c1: p <= p + p.image(rc)
          c2: p.image(rc).is_closed(r)   -- r2, tc_4
          c3: all(x,y:G)
              require
                  r3: x in p
                  r4: [x,y] in r
              check
                  c4: y in x.image(r)  -- r4
                  c5: y in x.image(rc) -- c4,r2
              ensure
                  y in p+p.image(rc)
              end
          c4: (p+p.image(rc)).is_closed(r)   -- c3
      ensure
          pc <= p + p.image(rc)    -- c1,c4,r1
      end
  lemma_2:
  all(p,pc:G?, r,rc:[G,G]?)
      require
          r1: pc = p.closed(r)
          r2: rc = r.closed(is_transitive)
      check
          c3: p.image(r)  <= pc                     -- r1
          c4: p.image(r).closed(r) <= pc.closed(r)  -- c3, closure monotonic
          c5: p.image(r).closed(r) <= pc            -- c4, closure idempotent
          c6: p.image(rc) = p.image({x,y: y in x.image(r).closed(r)}) -- tc_6
          c7: p.image(rc) = p.image(r).closed(r)  -- c6
          c8: p.image(rc) <= pc                   -- c5,c7
      ensure
          p + p.image(rc) <= pc    -- c1,c8
      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: