SourceForge.net LogoThe Eiffel Compiler / Interpreter (tecomp)

doc/papers/proof/order structure

Order structures: abstraction and multiple inheritance

Introduction

Order structures seem to be abstract concepts of theoretical mathematics with minor practical importance. But this is just at first glance. A closer look reveals that many data types have order structure.

Why is it necessary to carve out the order structure?

It is possible to prove a lot of properties by just using the definition of the functions of order relations. Any structure which inherits the appropriate order relation has access to all already proved asssertions. The order classes act as an "assertion library" and inheritance is reuse of these assertions.

The needed modules

Equivalence relation

In order to define the concept of a preorder we need the concept of an equivalence relation. The type COMPARABLE represents that concept.

  -- module: comparable
 
  deferred class 
    COMPARABLE 
  end
 
  feature 
    = (a,b:CURRENT): BOOLEAN 
      deferred end
 
    all(a,b,c:CURRENT) 
      deferred 
      ensure 
        reflexive: a=a 
        symmetric: (a=b) => (b=a) 
        transitive: (a=b) => (b=c) => (a=c) 
      end 
  end
 
  feature 
    all(a,b,c: CURRENT)
      ensure
        (a=b) = (b=a)
        (a=b) => (b/=c) => (a/=c)  -- proof: contrapositive 
       end 
  end 
 

Any binary relation which is reflexive, symmetric and transitive is an equivalence relation.

The class COMPARABLE has only the deferred feature "=" and postulates the main properties of "=" as deferred asssertions.

Predicates

A predicate "p" of type "T?" describes a set of elements of type T. The set contains all elements "a:T" for which the predicate "p" is satisfied, i.e. "a in p" is valid.

A predicate of type "T?" is a descendant of the type PREDICATE[T]. We assume in the following that the module "predicate" defines at least the following functions.

  -- module: predicate
  deferred immutable class
    PREDICATE[G]
  inherit
    ghost COMPARABLE
  end
 
  feature
    in (e:G, p:CURRENT): BOOLEAN
      deferred end
 
    = (a,b:CURRENT): ghost BOOLEAN
      ensure
        Result = all(e:G) (e in a) = (e in b)
      end
 
    False: CURRENT
      deferred ensure
        all(x:G) not (x in Result)
      end
 
    True: CURRENT
      deferred ensure
        all(x:G) not (x in Result)
      end
  end
 

Semipreorder

Basic declaration

Basic declaration of the class SEMI_PREORDER:

  -- module: semi_preorder
 
  deferred class
    SEMI_PREORDER
  inherit
    COMPARABLE
  end
 

The predicate "<=" (read: "reaches") is used to define the preorder relation.

  feature   -- reachability relation
    <= (a,b:CURRENT):BOOLEAN
        -- Can `a' reach `b'?
      deferred end
 
    all(a,b,c:CURRENT)
      deferred
      ensure
        reflexivity:  a<=a
        transitivity: (a<=b) => (b<=c) => (a<=c)
      end
  end
 

The "reaches" relation and its properties are defined as deferred. I.e. an effective descendent has to implement "reaches" in a way that the basic properties reflexivity and transitivity are satisfied.

We read "a<=b" as "a reaches b". It is not yet an order but very similar to an order. Therefore we use the symbol "<=" (is less or equal) from order relations. But preorders can have cycles. Therefore we talk about "<=" as a reachability relation.

Cycles

In a preorder we can go in cycles. I.e. it is possible that "a<=b" and "b<=a" are valid for different "a" and "b". We can use reachability to define the equivalence "=" relation inherited from COMPARABLE.

  feature     -- Equivalence relation
    = (a,b:CURRENT): BOOLEAN
      ensure
        Result = (a<=b) and (b<=a)
      end
 
    all(a,b,c:CURRENT)
      ensure
        eq_reflexive:   a=a
        eq_symmetric:   (a=b) => (b=a)
        eq_transitive:  (a=b) => (b=c) => (a=c)
      end
  end
 

The proofs of the three assertions are easy. They are immediate consequences of reflexivity and transitivity of the reachability relation and the symmetric definition of "=". In order to do the actual proof it is just necessary to expand the definition of "=".

The class SEMI_PREORDER can be a base class for mutable and immutable types.

Mutable types can have equivalence relations which are different from identity. They can use an arbitrary equivalence relation to define "=".

This is not valid for immutable types. The language rules require that an immutable type must have an equivalence relation named "=" which implies identity. I.e. "=" must be Leibniz equality. Two equal objects of immutable type have to be indistinguishable. This is not the case in the above definition of "=".

Therefore if an immutable class inherits from SEMI_PREORDER then it has to rename "=" into another name (e.g. "=.cyc") and reserve the name "=" for an equivalence relation which is strong enough to serve as Leibnitz equality.

Reachability of sets

The first feature "a<=p" defines, if an element "a" can reach all elements of a set described by a predicate "p".

  <= (a:CURRENT, p:CURRENT?): ghost BOOLEAN
      -- Does `a' reach all elements in `p'?
    ensure
      Result = all(x:CURRENT) x in p => (a<=x)
    end
 

Note that "<=" is overloaded. We can compare two objects "a<=b" or an object with a set/predicate "a<=b".

The predicate "<=" satisfies the following closure property:

  all(a,b:CURRENT, p:CURRENT?)
    ensure
      (a<=b) => (b<=p) => (a<=p)
    end
 

The proof requires just to expand the definition of reaches (for sets) and to use the transitivity of "reaches". Here is a pedantic proof which can be done by the proof engine automatically.

  all(a,b:CURRENT, p:CURRENT?)
    require
      r1: a<=b
      r2: b<=p
    check
      c1: all(x:CURRENT) x in p => (b<=x)  -- def "b<=p"
 
      c2: all(x:CURRENT)
        require
          r1_1: x in p
        check
          a<=b  -- r1
          b<=x  -- c1, r1_1
        ensure
          a<=x  -- transitivity of "<="
        end
    ensure
      a<=p  -- c2, def of "<=" for predicates
    end
 

In the case that "p" is empty, i.e. is unsatisfiable, then all elements can reach all elements of "p" (because there are no elements in p). I.e. we get

  all(a:CURRENT)
    ensure
      a <= (False:CURRENT?)  -- def of "<=", def of "False"
    end
 

which is an immediate consequence of the definition of "a<=p" for a set "p".

Lower set

It is convenient to define the set of all elements "a" which can reach a set "p", i.e. for which "a<=p" is valid.

  low_set(p:CURRENT?): CURRENT?
    ensure
      Result = (x:CURRENT -> x<=p)
    end
 

The lower set has the following properties which are immediate consequences of the definitions of the involved functions.

  all(a:CURRENT, p:CURRENT?)
    ensure
      a in p.low_set = (a<=p)  -- def "low_set"
      a in p => (a>=p.low_set) -- def "low_set"
    end
 

Minima

We have defined that "a<=p" is valid if "a" can reach all elements in "p". The elements which satisfy "a<=p" and are within "p" form an interesting subset. We call these elements "minima". In order to study these elements we define the predicate "is_minimum".

  is_minimum(a:CURRENT, p:CURRENT?): ghost BOOLEAN
    ensure
      Result = (a<=p and a in p)
    end
 

All elements "a" for which "a.is_minimum(p)" is valid must be equivalent. This is expressed by the following property.

  all(a,b:CURRENT, p:CURRENT?)
    ensure
      a.is_minimum(p) => b.is_minimum(p) => (a=b)
    end
 

Note that the equivalence "a=b" does not imply that both objects are the same!

Here is a manual proof

  all(a,b:CURRENT, p:CURRENT?)
    require
      r1: a.is_minimum(p)
      r2: b.is_minimum(p)
    check
      c1: a <= p  -- r1
      c2: b in p  -- r2
      c3: a <= b  -- c1,c2
 
      c4: b <= p  -- r2
      c5: a in p  -- r1
      c6: b <= a  -- c4,c5
    ensure
      a=b  -- c3,c6
    end
 

Note that there might be no elements "a" for a certain "p" which satisfy "a in p" (in the case that "p" is empty, i.e. "False"). The same is true for "a.is_minimum(p)".

Minimal elements

In the previous section we defined "a" to be a minimum of a set represented by the predicate "p" if "a" is in "p" and "a" can reach all elements in "p".

A minimal element "a" in "p" is an element which can only be reached from elements of "p" which are equivalent to "a". Note that a minimal element is different from a minimum.

  is_minimal(a:CURRENT, p:CURRENT?): ghost BOOLEAN
    ensure
      Result = check
        a in p
        all(b:CURRENT) b in p => (b<=a) => (b=a)
      end
    end
 

We claim that a minimum is also a minimal element.

  all(a:CURRENT, p:CURRENT?)
    ensure
      a.is_minimum(p) => a.is_minimal(p) -- see proof below
    end
 

Here is the manual proof

  all(a:CURRENT, p:CURRENT?)
    require
      r1: a.is_minimum(p)
    check
      c1: a in p  -- r1, def "is_minimum"
      c2: a <= p  -- r1, def "is_minimum"
 
      c3: all(b:CURRENT) 
        require
          r31: b in p
          r32: b <= a
        check
          c31: a <= b  -- r31,c2
        ensure
          b=a  -- r32,c31
        end
    ensure
      a.is_minimal(p)  -- def "is_minimal, c1, c3
    end
 

Dual semipreoder

A dual semipreorder is a semipreorder where the reachability direction is reverted. We get a dual semipreorder by inheriting from a semi preoder and rename the functions appropriately.

  deferred class
    DUAL_SEMI_PREORDER
  inherit
    SEMI_PREORDER
      rename
        <=          as >=
        low_set as up_set
        is_minimum  as is_maximum
        is_minimal  as is_maximal        
      end
  end
 

Preorder

Merge of two semipreorders

A preorder is a merge of a semipreorder and a corresponding dual semipreorder.

  deferred class
    PREORDER
  inherit
    SEMI_PREORDER
    DUAL_SEMI_PREORDER
      undefine
        =
      end
  end
 
  feature
    >= (a,b:CURRENT): BOOLEAN
      ensure
        Result = (b<=a)
      end
  end
 

A preorder has a forward reachability relation "<=" and a backward reachability relation ">=". In the module "preorder" we define the backward reachability ">=" in terms of the forward reachability "<=". Therefore we can read "a<=b" as "a reaches b" and "a>=b" as "a is reachable by b".

Since equality is defined in a semipreorder, it is necessary to undefine one of the two. The definition of the undefined converts into a normal assertion which needs to be proved.

  all(a,b:CURRENT)
    ensure
      (a=b) = (a>=b and b>=a)  -- def ">=", def "="
    end
 

Due to the definition of ">=" we get the dual of reflexivity and transitivity.

  feature
    all(a,b,c:CURRENT)
      ensure
        dual_reflexivity:  a>=a
        dual_transitivity: (a>=b) => (b>=c) => (a>=c)
      end
  end
 

The proof just requires an expansion of the definiton of ">=".

Relation between lower and upper set

We expect that all elements "a" which are in the lower set of a predicate "p" can reach all elements of the upper set of "p". But this is valid only if there are elements in "p". I.e. we can state the properties

  all(a:CURRENT, p:CURRENT?)
    require
      some(x:CURRENT) x in p
    ensure
      a in p.low_set => (a<=p.up_set)
      a in p.up_set => (a>=p.low_set)
    end  
 

The first one has the following proof.

  all(a:CURRENT, p:CURRENT?)
    require
      r1: some(x:CURRENT) x in p
      r2: a in p.low_set
    check
      c1: all(x:CURRENT)
        require
          r11: x in p
        check
          a<=x  -- r2
          x<=p.up_set -- r11, def "up_set"
        ensure
          a<=p.up_set -- transitivity of "<="
        end
    ensure
      a<=p.up_set  -- r1, c1
    end  
 

Note how important it is that "p" is satisfiable. Without being satisfiable, we cannot draw the conclusion. We need an object "x" in the middle which can be reached by "a" and which can reach all elements in "p.up_set".

The dual property has a similar proof.

Infima and suprema

An infimum of "p" is a maximum of all elements which can reach all elements of "p", i.e. an infimum of "p" is a maximum of the lower set of "p".

  is_infimum(a:CURRENT, p:CURRENT?): BOOLEAN
    ensure
      Result = a.is_maximum(p.low_set)
    end
 

A supremum of "p" is a minimum of all elements which can be reached by the elements of "p", i.e. a supremum of "p" is a minimum of the upper set of "p".

  is_supremum(a:CURRENT, p:CURRENT?): BOOLEAN
    ensure
      Result = a.is_minimum(p.up_set)
    end
 

A minimum is always an infimum and a maximum is always a supremum (the reverse is not generally true, because infima and suprema need not belong to the set).

  all(a:CURRENT, p:CURRENT?) 
    ensure
      a.is_minimum(p) => a.is_infimum(p)
      a.is_maximum(p) => a.is_supremum(p)
    end
 

We prove the first one by

  all(a:CURRENT, p:CURRENT?)
    require
      a.is_minimum(p)
    check
      c1: a <= p  -- def "is_minimum"
      c2: a in p  --     "
 
      c3: a >= p.low_set           -- c2, def "low_set"
      c4: a in p.low_set           -- c1, def "low_set"
      c5: a.is_maximum(p.low_set)  -- def "is_maximum"
    ensure
      a.is_infimum(p)  -- def "is_infimum"
    end
 

The proof of the second one is similar.

Partial order

The class PARTIAL_ORDER is defined as a descendant of PREORDER in the following manner.

  -- module "partial_order"
  deferred class
    PARTIAL_ORDER
  inherit
    PREORDER
      undefine 
        = 
      end
  end
 
  feature
    < (a,b:CURRENT): BOOLEAN
      ensure
        Result = (a<=b and a/=b)
      end
 
    > (a,b:CURRENT): BOOLEAN
      ensure
        Result = (a>=b and a/=b)
      end
 
    all(a,b,c:CURRENT)
      deferred
      ensure
        reflexivity:  (a=b) => (a<=b)
        antisymmetry: (a<=b) => (b<=a) => (a=b)
        transitivity: (a<=b) => (b<=c) => (a<=c)
      end
 
    all(a,b:CURRENT)
      ensure
        a<=a  -- implied by reflexivity and reflexivity of "="
 
        ((a<=b) and (b<=a)) = (a=b)
          -- forward:  consequence of antisymmetry
          -- backward: consequence of reflexivity
      end
  end
 

A partial order and a preorder are practically the same. There are some minor differences.

A preorder defines "=" based on "<=". The partial order undefines this definition. Therefore the descendents of of PARTIAL_ORDER can provide their own definition.

The undefinition of "=" turns the definition of "=" from PREORDER into an assertion which has to be proved. It can be proved by the axioms "reflexivity" and "antisymmetry".

The reflexivity in PARTIAL_ORDER is not defined in the usual way as "a<=a" but as "a=b => a<=b". This definition is stronger. The classic reflexivity is proved as a consequence. We use this axiom in order to be able to derive mutable an immutable descendants from PARTIAL_ORDER.

For mutable types "=" does not imply identity. Therefore we require that any "a" and "b" which are equivalent according to the definition of the descendent have to satisfy "a<=b" in order to be consistent with the order relation.

For immutable types "=" does imply identity. Therefore the stronger requirement for reflexivity is an immediate consequence of classical reflexivity "a<=a". Note that for immutable types the assertion "a=b" guarantees that "a" is indistinguishable from "b". Therefore "a<=a" and "a=b" imply "a<=b" which is the above requirement.

Emacs suffix

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

- Introduction

- The needed modules

- Equivalence relation

- Predicates

- Semipreorder

- Basic declaration

- Cycles

- Reachability of sets

- Lower set

- Minima

- Minimal elements

- Dual semipreoder

- Preorder

- Merge of two semipreorders

- Relation between lower and upper set

- Infima and suprema

- Partial order

- Emacs suffix


ip-location