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.
