SourceForge.net LogoThe Eiffel Compiler / Interpreter (tecomp)

doc/papers/proof/relations

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
 

Emacs suffix

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

- Introduction

- Binary relations

- Domain and range

- Inverse

- Composition

- Images and preimages

- Domain/range restrictions of relations

- Functional relations

- Endorelations

- Properties of endorelations

- Duality

- Transitivity and restricted relations

- Transitivity and images

- Closure systems

- Transitive closures

- Transitive relations with logical implication

- Inheriting properties via relations and transitive closures

- Reachability via a relation

- Equivalent expressions for transitive closures

- Equivalent expressions for closed sets

- Emacs suffix


ip-location