- Here is an initial proposal for COMPARABLE.

I think we can discuss this in one step, and vote on it

in a block doing the different issues in separate votes,

but at the same time or in rapid succession.

Points I see:

The name is misleading. What is modelled is a total

order. In mathematical terms "comparable" would

mean that there is an equality operator defined on a set,

not an order. Usually these exist and are total. The same

is true in Eiffel, look at feature "equal" to find it.

So COMPARABLE should really be named TOTALLY_ORDERED.

I am not proposing to change the name, but to change the

head comment. ELKS95 says

"Objects that may be compared according to a total order relation";

note: "The basic operation is `<` (less than); others are defined

in terms of this operation and `is_equal'."

I do not like the "may". It confuses things. My proposal:

"Objects of this type are ordered with respect to a total

order relation `<'. This basic operation is used together

with `is_equal' to define additional operators."

Furthermore I propose the following changes:

- Remove the invariant and put it in a postcondition

'strict' in '<'. Furthermore add a postcondition

'total' to '<'.

The advantage is that 'is_equal' need not be redefined

anymore as trichotomy is now defined in the contract of "<".

This is good as trichotomy is really a property of '<' that

is defined in relation to a given definition for 'is_equal'.

It is _not_ a constraint on 'is_equal'!

Affected: Features "<", 'is_equal'

Invariant 'irreflexive_comparison'

- 'min','max' are over-specified: When the elements are equal via

'is_equal' there is a preference for a specific result

(Current). The way I read the specification of 'is_equal' in

GENERAL is that a redefinition of 'is_equal' that has different

objects being equal is entirely permissible, as long as equality

implies same type and 'standard_is_equal' implies 'is_equal'. The

most general implementation would give 'is_equal' the same

semantics as 'same_type'.

I hope I got this right. Please correct me if not!

Change: Allow 'min', 'max' to return any argument

if arguments are equal via 'is_equal'.

Affected: Postconditions of features 'min', 'max'.

That seems to be it. If I missed something, please speak up!

Here is the rest of COMPARABLE from ELKS95. Places where I

think changes are needed are marked with '#' and a comment

behind it. The changes I propose are the following:

-----

feature -- Comparison

infix "<" (other: like Current): BOOLEAN

-- Is current object less than other?

require

other_exists: other /= Void

ensure

asymmetric: Result implies not (other < Current)

# Add the following:

#

# strict: Result implies not Current.is_equal(other)

# total: not Current.is_equal(other) implies

# (Current < other or other < Current)

#

# This is in part covered by the invariant, but I feel it is needed

# here, and here only. I propose to remove the invariant.

infix "<=" (other: like Current): BOOLEAN

-- Is current object less than or equal to other?

require

other_exists: other /= Void

ensure

definition: Result = (Current < other) or is_equal (other)

infix ">=" (other: like Current): BOOLEAN

-- Is current object greater than or equal to other?

require

other_exists: other /= Void

ensure

definition: Result = (other <= Current)

# Replace this with

#

# definition: Result = (other < Current) or is_equal (other)

#

# in order to get a direct dependency on the basic operations.

infix ">" (other: like Current): BOOLEAN

-- Is current object greater than other?

require

other_exists: other /= Void

ensure

definition: Result = (other < Current)

is_equal (other: like Current): BOOLEAN

-- Is other attached to an object considered equal

-- to current object?

-- (Redefined from GENERAL.)

require

other_not_void: other /= Void

ensure

symmetric: Result implies other.is_equal (Current);

consistent: standard_is_equal (other) implies Result;

trichotomy: Result = (not (Current < other) and not (other < Current))

#

# 'trichotomy' is redundant with the postcondition 'strict' on '<' and

# 'definition' on '>'. We could remove it and do without redefinition

# of 'is_equal' entirely. My personal feeling is that this would be the way

# to go: An order relation has to respect the already defined equality

# relation, _without_ putting any additional constraints on it.

# 'consistent' and 'symmetric' are already in GENERAL.

#

max (other: like Current): like Current

-- The greater of current object and other

require

other_exists: other /= Void

ensure

current_if_not_smaller: (Current >= other) implies (Result = Current)

other_if_smaller: (Current < other) implies (Result = other)

# This is too strict. If some objects change is_equal so that some

# different objects cannot be distinguished by 'is_equal' anymore

# this postcondition mandates that the result has to be 'Current'.

# There is no need for that.

# I would propose to replace the entire postcondition with

#

# definition: Result >= Current and Result >= other and

# (Result = Current or Result = other)

#

# neatly removing the problem.

min (other: like Current): like Current

-- The smaller of current object and other

require

other_exists: other /= Void

ensure

current_if_not_greater: (Current <= other) implies (Result = Current)

other_if_greater: (Current > other) implies (Result = other)

# Same thing as with 'max'. I propose to change the postcondition to

#

# definition: Result <= Current and Result <= other and

# (Result = Current or Result = other)

#

three_way_comparison (other: like Current): INTEGER)

-- If current object equal to other, 0; if smaller,

-- -1; if greater, 1.

require

other_exists: other /= Void

ensure

equal_zero: (Result = 0) = is_equal (other);

smaller_negative: (Result = -1) = (Current < other);

greater_positive: (Result = 1) = (Current > other)

invariant

irreflexive_comparison: not (Current < Current)

# I propose to remove this invariant. The postcondition 'strict' at

# feature '<' is entirely enough and is in the place where it belongs.

end

--

Arno Wagner, Communication Systems Group, ETH Zuerich, wagner@...

GnuPG: ID: 1E25338F FP: 0C30 5782 9D93 F785 E79C 0296 797F 6B50 1E25 338F

----

For every complex problem there is an answer that is clear, simple,

and wrong. -- H L Mencken - On Fri, Aug 09, 2002 at 12:01:39PM -0400, James McKim wrote:
> Hey Arno,

Thanks for the confidence! I'll do my best.

>

> Thanks for taking the lead, both for the group in

> general and for COMPARABLE in particular. I'm sure

> you'll do a great job!

I am sure it will be a learning experience though.

As for your comments, I might post a detailed answer

in the next days, but I have a wacky idea now:

[...]> I like this change, but note that actually we can do it

[...]

> entirely in terms of `<' as the basic specifier for

> COMPARABLE.

We can, but it has some interesting consequences. If

we do a total order in terms of `<' only, that means

that equality will be defined in terms of `<' only.

(Equality is needed because of totality unless we

allow only `='-equality.)

Let `===' denote this type of "equality with respect

to `<'" for the moment.

The definition for `===' would be

for all a,b:

a === b if and only if ( not(a<b) and not(b<a) )

neatly enforcing totality of `<'. (Although probably

not quite in the way people expect. `===' would

be kind of a kernel relation here.) Without `==='

the problem would be that not(a<b) and not(b<a)

could be true, while a and b are not the same

object. This would make `<' partial.

If we spin this a little further, we can indeed use

the above definition of "equality with respect to `<'"

and define all the other operators according to it.

`>',`<=',`>=' are no problem. `===' is not even needed here.

max(a,b):

if a>b then max(a,b) = a

if b>a then max(a,b) = b

if a===b then max(a,b) = a or max(a,b) = b

`min' analog.

`three_way_comparison' analog.

Added benefit: `is_equal' does not make an appearence

in this at all! `===' and `is_equal' are completely

independent. Getting rid of the forced relation between

`===' and `is_equal' _would_ be nice in mu opinion.

(Everybody that wants this relation can still define

`<' accordingly.)

The one problem I see is what to do with `==='?

- First option: Redefine `is_equal' to

have the semantics of `==='. That is how it was done

up to now. Problem: `is_equal' is sort of a 'higher'

concept than `<'. To me it feels wrong to change the

basic notion of equality in order to accomodate the

less basic notion of order.

- Second option: Have a new explicit operator `==='

(naming to be determined). Would this operator really

offer an added benefit or just clutter the interface?

Personally I might prefer this one.

- Third option: Do not have an explicit `===' operator.

It is not a good idea to have a defined notion

for equality (`===') but no explicit name/operator for it,

so this is probably not be the way to go.

- Fourth option: Have `===' defined as `is_equal'

and constrain `<' accordingly. This would make sense

insofar as `is_equal' is meta-equality in Eiffel. On the

other hand we might just want a special kind of equality

with regard to order and constraining `<' is indeed not

elegant. (This was my original proposal.)

- Fifth option: Define `===' as `='. This seems very

constraining. On the other hand, is this not what we are

thinking of when we say "ordered"? Mathematically it is.

This option has one strong benefit: It ensures

that objects can always be sorted/orderd in one way only.

Of two different opjects one will always be larger.

In a sense all the other options above are only there

because we allow an equivalence relation (`is_equal') to

take the place of equality, but at the same time cannot do

a complete factoring, i.e. things that are equal via

`is_equal' can still be distinguished.

- Other ideas ??

This totality requirement has indeed some interesting

consequences....

Regards,

Arno

P.S.: I don't think a discussion about partial orders will

help us much. There are many types of these and often you

actually want a lattice, making things even more general

and the number of variants very, very large. So unless you

have this papers handy, don't bother.

---

Arno Wagner, Communication Systems Group, ETH Zuerich, wagner@...

GnuPG: ID: 1E25338F FP: 0C30 5782 9D93 F785 E79C 0296 797F 6B50 1E25 338F

----

For every complex problem there is an answer that is clear, simple,

and wrong. -- H L Mencken