# 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.

– The basic types NATURAL, INTEGER, FLOAT etc. have a total order

– The type SET[T] has a partial order with “is_subset” playing the role of

“<=”.

– All inductive types have a partial order where “a<=b” means “a has been used

directly or indirectly in the construction of b”. E.g. any subtree of a tree

is smaller than the tree.

– The nodes in a graph have a preorder relation with “a<=b” meaning “a can

reach b”.

– The functions “f:A->B” have a partial order where the “smaller” function has

the same values as the “greater” function but has a restricted domain.

– The predicates “p:T?” have a partial order where “a<=b” meaning “a” is

stronger than “b”, i.e. “a” has less elements for which it is true than “b”.

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 ensure Result = x:G -> (False:BOOLEAN) end True: CURRENT ensure Result = x:G -> (True:BOOLEAN) end all(e:G) ensure e in True not (e in False) 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 low 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 set 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 the requirement that “p” is satisfiable is. Without it, 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.