Rust: Should PartialOrd require irreflexivity over <?

[gnzlbg]

Why doesn't PartialOrd require irreflexivity !(a < a) over < ? AFAICT PartialOrd does not actually express any kind of ordering relation for <. For:

• a strict partial order on <: we need PartialOrd + Irreflexivity
• non-strict partial order on <=: we need PartialOrd + Eq since == must be reflexive.
• total order: we needPartialOrd + Eq + Total

Is this an oversight? If not, we should document that PartialOrd requires:

• irreflexivity: !(a < a)

as well. That would make PartialOrd's < denote a strict partial order on <.

AFAICT this is actually what was intended, since all the discussions I can find online about PartialOrd talk about floats, and floats are strictly partially ordered under <, but not non-strictly partially ordered under <=, which would fit our current model that floats don't implement Eq.

---

Also, the docs of PartialOrd do not say what le (<=) and ge (>=) actually mean. AFAICT they mean nothing for PartialOrd in isolation. From reading the source the default implementation is a < b || a == b, which would denote a non-strict total ordering over <= when Eq is implemented. But since Eq is not required for PartialOrd, I'd guess that those overriding these implementations are allowed to do something else as long as they don't implement Eq. It is unclear to me what that "something else" might mean, but the docs should probably say something about this.

---

Also, I haven't been able to find any document explaining why things are the way they are, but the fact that PartialOrd requires PartialEq makes no sense to me, and it doesn't make much sense either that PartialOrd exposes le (<=) and ge (>=) methods, since as mentioned above, without Eq, le and ge do not express any meaningful ordering relation. It seems that these traits, like all other "operators" traits, mix operator overloading with mathematical semantics: in some cases they are used to express mathematical concepts, like a strict partial ordering relation under <, and in some other cases they are used "to provide <= for floats". If anybody has any links to any discussions / documentation about why things are the way they are I'd like to read them, and maybe we should add rationale sections to the docs.

[LukasKalbertodt]

In the RFC thread for is_sorted, @ExpHP mentioned that PartialOrd probably also requires: (a < b) if and only if (b > a) (they called it "the 'notational' axiom").

Irreflexivity is implied by said notational axiom and the semantics of partial_cmp. Simple proof: for irreflexivity to not be satisfied, !(a < a) would have to be false for some a. This means that for some a, a < a would have to be true. Using the notational axiom that means that a > a would have to be true as well (I swapped the two as). But a < a and a > a cannot be true at the same time (this last fact is merely implied by the type Ordering... but I guess it's worth putting it in the docs explicitly).

Thus, instead of adding the axiom of Irreflexivity to the docs, one could also add the notational axiom (which we probably want to add anyway).

---

The docs are also unclear or plain wrong in regards to the provided methods lt, le and friends. The docs say:

PartialOrd only requires implementation of the partial_cmp method, with the others generated from default implementations.

However it remains possible to implement the others separately for types which do not have a total order.

This implies that one has to manually implement lt and friends to achieve a non-total ordering. This is false. In fact it's misleading because lt and friends need to be implemented in a way that has the same behavior as the default implementation. Otherwise partial_cmp would disagree with lt and friends. The docs should explicitly disallow such disagreement between methods. (Since semantics of lt and friends mustn't be changed, the only reason to provide a manual implementation is speed.)

[gnzlbg]

@RalfJung mentioned on IRC:

so x <= y must be (x < y || x == y)

PartialEq is more explicit: "Any manual implementation of ne must respect the rule that eq is a strict inverse of ne; that is, !(a == b) if and only if a != b."

I think that sentence was just forgotten for PartialOrd

That is, the docs should state that ge is equivalent to gt || eq and le is equivalent to lt || eq and that any manual implementation must respect that.

[RalfJung]

(Since semantics of lt and friends mustn't be changed, the only reason to provide a manual implementation is speed.)

Agreed. This is stated explicitly for PartialEq, it seems it as forgotten here.

it doesn't make much sense either that PartialOrd exposes le (<=) and ge (>=) methods, since as mentioned above, without Eq, le and ge do not express any meaningful ordering relation.

I think that's the wrong way to think about it: PartialOrd is only a single operation, partial_cmp. This operation is then used to define <, <=, > and >=. There is no choice left here, the only reason it is possible to override the default implementations (as @LukasKalbertodt said) is to make them go faster.

[RalfJung]

@ExpHP mentioned that PartialOrd probably also requires: (a < b) if and only if (b > a) (they called it "the 'notational' axiom").

Yeah that sounds pretty reasonable. I'd express this as "> is the dual to <", I think that's the common terminology in maths.

I briefly wondered how this relates to antisymmetry... but antisymmetry is a strange axiom in this context. In fact, antisymmetry is impossible to violate! If a < b, then partial_cmp(a, b) == Some(Less), so we already have !(a > b). So, I think we can just drop it. If we require that lt and gt are defined in terms of partial_cmp (or equivalent), antisymmetry will always hold.

(EDIT: This assume !(a < b) is the negated boolean a < b... because I cannot imagine any other reasonable interpretation.)

[gnzlbg]

So, I think we can just drop it. I

Wouldn't we then need to require that if partial_cmp(a,b) == Some(Less) then partial_cmp(b, a) == Some(Greater) or something like that?

EDIT: I see this as just trading one axiom for another. We probably should document the axioms both in term of the comparisons <, ==, ... (which is more easy for some people to understand) and in terms of partial_cmp (which is what everybody has to implement).

[RalfJung]

Wouldn't we then need to require that if partial_cmp(a,b) == Some(Less) then partial_cmp(b, a) == Some(Greater) or something like that?

That's the "notational" (or "duality") axiom: a < b implies b > a.

[gnzlbg]

That's the "notational" (or "duality") axiom: a < b implies b > a.

Aha! Yeah if we add that axiom then we don't need anti-symmetry. Nice!

The wikipedia page on strict partial orders actually mentions this, that one axiom follows from the other two:

* not a < a (irreflexivity),
* if a < b and b < c then a < c (transitivity), and
* if a < b then not b < a (asymmetry; implied by irreflexivity and transitivity).

(just note that we don't require irreflexivity yet)

[gnzlbg]

So to make a more concrete proposal. We currently have PartialOrd specified as:

Trait for values that can be compared for a sort-order.

The comparison must satisfy, for all a, b and c:

• antisymmetry: if a < b then !(a > b), as well as a > b implying !(a < b); and
• transitivity: a < b and b < c implies a < c. The same must hold for both == and >.

Note that these requirements mean that the trait itself must be implemented symmetrically and transitively: if T: PartialOrd<U> and U: PartialOrd<V> then U: PartialOrd<T> and T: PartialOrd<V>.

Including all feedback above, we could change that to (strawman):

Strict partial ordering relation.

The comparison must satisfy, for all a, b and c:

• transitivity: if a < b and b < c then a < c
• duality: if a < b then b > a

that is, in terms of partial_cmp:

• transitivity: if partial_cmp(a,b) == Some(Less) and partial_cmp(b, c) == Some(Less) then partial_cmp(a,c) == Some(Less)
• duality: if partial_cmp(a, b) == Some(Less) then partial_cmp(b, a) == Some(Greater)

The semantics of le (<=) and ge (>=) are defined as:

• le(a,b) == (a < b || a == b)
• ge(a,b) == (a > b || a == b)

The lt , le, gt, and ge methods are implemented in terms of partial_cmp according to these rules. The default implementations can be overridden for performance reasons, but manual implementations must satisfy the rules above.

From these rules it follows that PartialOrd must be implemented symmetrically and transitively: if T: PartialOrd<U> and U: PartialOrd<V> then U: PartialOrd<T> and T: PartialOrd<V>.

Stronger ordering relations:

• partial_cmp is a non-strict partial ordering relation if T: PartialOrd + Eq
• partial_cmp is a total ordering relation if T: Ord

Corollaries: follow from _transitivity_ of < and _duality_

• _irreflexivity_ of <: !(a < a)

• _transitivity_ of >

• _asymmetry_ of <: if a < b then !(b < a)

• _antisymmetry_ of <: if a < b then !(a > b)

I am not sure if everything does indeed follow properly from duality and transitivity. Even if it does, this is a question that some might have, and even if this is all trivial to prove, I think we should have a "Proofs" section in the docs of PartialOrd with the proofs. Do you think that such a section makes sense?

[LukasKalbertodt]

@gnzlbg Awesome, thank you! A few things though:

(1.)

partial_cmp is a non-strict partial ordering relation if T: PartialOrd + Eq

Are you sure? I don't think transitivity ("a <= b and b <= c implies a <= c") can be derived from the axioms. E.g. if a == b and b < c, then either a < c or a and c could be uncomparable. I don't see how the current axioms prevent a and c from being uncomparable, but maybe I missed something.

(2.)

Strict partial ordering relation.

I would change this to "Strict partial ordering relationS." as the trait adds < and >, two new strict partial ordering relations. Maybe even change it to "Strict partial ordering relations < and >."

(3.)

Maybe we want to explicitly state that lt and friends return false if partial_cmp returns None. Or in general we might want to talk about what returning None means. And maybe add the information implied by Ordering: "At most one of a < b, a == b and a > b is true."

(4.)

transitivity of > is implied by symmetry of ==, transitivity of < and ==, and duality of <.

I don't think you only need duality and transitivity of < here:

      a > b ⋀ b > c ⇒ a > c        | using duality to mirror all relations
⇔    b < a ⋀ c < b ⇒ c < a        | just change the order of the AND operands
⇔    c < b ⋀ b < a ⇒ c < a        | we're done as this is the transitivity of `<` axiom

[gnzlbg]

1. I would change this to "Strict partial ordering relationS." as the trait adds < and >, two new strict partial ordering relations. Maybe even change it to "Strict partial ordering relations < and >."

I was talking here about partial_cmp, not < and > which "follow" from it. I don't know a better way to put it yet, but I wanted to emphasize that partial_cmp is the "relation" that users have to implement. From there it follows that < and > are strict partial orders. I don't know, I find partial_cmp a bit weird to think about.

Maybe we want to explicitly state that lt and friends return false if partial_cmp returns None

So when I wrote the axioms in term of partial_cmp I wrote a < b == (partial_cmp(a,b) == Some(less)). Maybe we should explicitly mention this:

• a < b is partial_cmp(a,b) == Some(Less)
• a > b is partial_cmp(a,b) == Some(Greater)

I don't think you only need duality and transitivity of < here:

Yes you are correct, I ninja edited the post.

("a <= b and b <= c implies a <= c") can be derived from the axioms. E.g. if a == b and b < c, then either a < c or a and c could be uncomparable.

Step by step: "if a == b and b < c implies a < c || a == c" is equivalent to "a < c implies a < c || a == c which is equivalent to "a < c implies a < c or a < c implies a == c" which is "true or false" which is "true". Or what am I missing?

I don't see how the current axioms prevent a and c from being uncomparable, but maybe I missed something.

The only requirement of Eq over PartialEq is reflexivity: a == a. So IIUC that requires a to be comparable with itself.

[LukasKalbertodt]

I was talking here about partial_cmp, not < and > which "follow" from it. I don't know a better way to put it yet, but I wanted to emphasize that partial_cmp is the "relation" that users have to implement. From there it follows that < and > are strict partial orders. I don't know, I find partial_cmp a bit weird to think about.

Mhh, yes that's tricky :/

But as far as I understand it, partial_cmp is not a relation in the mathematical sense. From the Wikipedia article it looks like a binary relation is just a subset of the cartesian product X × Y of two sets. Basically meaning that a relation just says true or false for every pair of members of the two sets. partial_cmp certainly says more than that.

In fact, I think that partial_cmp defines exactly three (disjunct) relations (disjunct meaning that no two of those relations have a member in common). I mean yes, "relation" is also just an English word that would fit here from a non-math standpoint. But since the documentation mentions some exact math terms, I wouldn't use "relation" (which has an exact mathematical definition) in the non-mathematical sense.

Maybe the first paragraph of PartialOrd docs should be targeted at the standard user who is not interested in axioms or exact mathematical terms. Maybe explain it in terms of "comparison"?

Types that can be compared to one another (defines the operators <, <=, => and >).

---

Maybe we should explicitly mention this:

I'd say so.

Step by step: "if a == b and b < c implies a < c || a == c" is equivalent to "a < c implies a < c || a == c" which is equivalent to "a < c implies a < c or a < c implies a == c" which is "true or false" which is "true". Or what am I missing?

I'm not sure about your first step: you say "a == b and b < c" is equivalent to "a < c". I mean it intuitively makes sense but can that be derived from the axioms? As far as I can think it through, you can only show that:

• a > c is false: otherwise a == b ⋀ b < c ⋀ a > c is true, which is equivalent to a == b ⋀ a > c ⋀ c > b (duality and swapping two terms), which is equivalent to a == b ⋀ a > b (transitivity of >), which is false (disjunction of > and == relation).
• a == c is false: otherwise a == b ⋀ b < c ⋀ a == c is true, which is equivalent to b == c ⋀ b < c, which is false (again due to disjunction of < and ==)

So we still have two possibilities: either a < c (what we want to show) or a and c are not comparable. To show that a < c is in fact implied, we'd have to show that a and c are necessarily comparable, right? And:

The only requirement of Eq over PartialEq is reflexivity: a == a. So IIUC that requires a to be comparable with itself.

This only requires everything to be comparable with itself, which doesn't help us because a and c are not the same element.

But again, maybe I'm missing something.

[RalfJung]

@gnzlbg nice first strawman! I overall like it. I think before stating any axioms, however, we should define <, <=, > and >= (or maybe just < and >) in terms of partial_cmp. Otherwise the axioms don't actually mean anything. Moreover, we should spell out what it means to "agree" with PartialEq, I guess we want an axiom like "partial_cmp(a, b) == Some(Equal) if and only if (a == b)"?

partial_cmp is a non-strict partial ordering relation

partial_cmp is a total ordering relation

As @LukasKalbertodt pointed out, these statements are not well-typed: partial_cmp is not a relation (it does not have type fn(T, T) -> bool). Please spell out which relation(s) you mean: <, <=, >, >=?

Corollaries: follow from transitivity of < and duality

I'd add "and from the definition of < et al. in terms of the same partial_cmp"

I'm not sure about your first step: you say "a == b and b < c" is equivalent to "a < c".

This is some kind of congruence statement: Essentially, we demand that a == b implies partial_cmp(a, c) == partial_cmp(b, c), or similar (and also for replacing the second argument).

So maybe, instead of what I said above, the real meaning of "PartialCmp agrees with PartialEq" is

• a1 == a2 and b1 == b2 imply partial_cmp(a1, b1) == partial_cmp(a2, b2), AND
• partial_cmp(a, b) == Some(Equal) if and only if (a == b)

However, these may be too strong for irreflexive equalities? NaN seems fine though (this mandates that partial_cmp(NaN, NaN) == None, but that seems reasonable).

Can we derive one of these axioms from the other? Or find one nicer axiom that implies both of them?

[ExpHP]

So, I've only been half-following this. I'm afraid I'll really only just be adding to the noise; but here's how I feel inclined to look at it:

• We need at least as many axioms as we have methods. This is unavoidable. Most axioms can be as boring as the notational/duality axiom, simply defining one method in terms of another.
• I am fairly certain that all methods of the traits can be defined in terms of <= alone. Is difficult to elaborate right now as I am on my phone, but I picture the directed graph formed by edges from a to b wherever a <= b.
• What are the axioms of <=? I think that for PartialOrd, it's just ~associativity.~ i mean transitivity!

[steveklabnik]

Tagging with @rust-lang/lang; they need to make a call before we can write docs.

[joshtriplett]

Seems reasonable. The docs in this comment seem plausible to me.

Would it make sense to use rfcbot to gather consensus asynchronously?

[gnzlbg]

Is there a recommended way to put up a documment that we could quickly edit for this collaboratively?

It appears to me that after @LukasKalbertodt and @RalfJung comments we are 95 % there, we just need to finish it, and for that it might be better if we would just have something that's "uptodate" and that we can quickly eidt.

[LukasKalbertodt]

@gnzlbg I don't know if that's what you had in mind, but I created a HackMD document from your comment. Everyone can login via GitHub and edit. But it might be better to have a tiny repository where we submit the documentation as PR and we can leave line comments?

[gnzlbg]

@LukasKalbertodt thanks! I worked a bit on it there and this is how it looks now (it would be cool if the tool could create diffs, so maybe a github repo would be better for something like this in the future):

---

PartialOrd Documentation

Strict partial ordering relation.

This trait extends the partial equivalence relation
provided by PartialEq (==) with partial_cmp(a, b) -> Option<Ordering>,
which is a trichotomy
of the ordering relation when its result is Some:

• if a < b then partial_cmp(a, b) == Some(Less)
• if a > b then partial_cmp(a, b) == Some(Greater)
• if a == b then partial_cmp(a, b) == Some(Equal)

and the absence of an ordering between a and b when partial_cmp(a, b) == None.

Furthermore, this trait defines <= as a < b || a == b and
>= as a > b || a == b.

The comparisons must satisfy, for all a, b, and c:

• _transitivity_: if a < b and b < c then a < c
• _duality_: if a < b then b > a

The lt (<), le (<=), gt (>), and ge (>=) methods are
implemented in terms of partial_cmp according to these rules.
The default implementations can be overridden for performance reasons,
but manual implementations must satisfy the rules above.

From these rules it follows that PartialOrd must be implemented
symmetrically and transitively: if T: PartialOrd<U> and U: PartialOrd<V>
then U: PartialOrd<T> and T: PartialOrd<V>.

The following corollaries follow from transitivity of <, duality,
and from the definition of < et al. in terms of
the same partial_cmp:

• irreflexivity of <: !(a < a)
• transitivity of >: if a > b and b > c then a > c
• asymmetry of <: if a < b then !(b < a)
• antisymmetry of <: if a < b then !(a > b)

Stronger ordering relations can be expressed
by using the Eq and Ord traits, where the
PartialOrd methods provide:

• a non-strict partial ordering relation if T: PartialOrd + Eq
• a total ordering relation if T: Ord

---

[LukasKalbertodt]

@gnzlbg

(it would be cool if the tool could create diffs, so maybe a github repo would be better for something like this in the future)

Yes, diffs and PR-comments would be nice. I created a temporary repository and submitted the current documentation as PR. I'd suggest we could discuss everything there. I already left a few comments on the PR.

I also gave you push access to the repo, so feel free to change things as you like.

[eddyb]

(small note: < is the "strict partial order", and <= the "non-strict partial order" - but the latter also requires Eq - mathematically, the "operators" are the orders, not {partial_,}cmp)

[LukasKalbertodt]

@eddyb I added a comment with an alternative formulation here.

[eddyb]

Looks like C++ went with something a bit more complex.
I'm not sure, but it almost seems like they have an Ord + PartialEq combination?

[gnzlbg]

@eddyb The latest paper is P0515r3. The most relevant section for this discussion is probably "Section 2: Design" which defines the following comparison categories as types:

• weak_equality
• strong_equality is a weak_equality
• partial_ordering is a weak_equality
• weak_ordering is a partial_ordering
• strong_equality is a weak_ordering and a strong_equality

The values of the equality categories are:

• weak_equality returns {equivalent, nonequivalent}
• strong_equality returns {equal, unequal} which are converted to {equivalent, nonequivalent} when converted to weak_equality results.

This is very similar to rust: interpret PartialEq::eq -> bool returning true as equivalent and false as nonequivalent, and when Eq is also implemented interpret these as equal and unequal respectively.

The orderings are also pretty similar:

• partial_ordering values are {less, equivalent, greater, unordered} which can be implicitly converted to the weak_equality values as {nonequivalent, equivalent, nonequivalent, nonequivalent}
• weak_ordering values are {less, equivalent, greater} and implicitly convert to:
  
  
  
  • weak_equality values as {nonequivalent, equivalent, nonequivalent}
  
  
  • partial_ordering values as {less, equivalent, greater}
  
  
• strong_ordering values are {less, equal, greater} and implicitly convert to:
  
  
  
  • weak_ordering values as {less, equivalent, greater}
  
  
  • strong_equality values as {unequal, equal, unequal}
  
  
  • weak_equality values as {nonequivalent, equivalent, nonequivalent}
  
  

The paper is a bit light on math details; maybe some of this is covered in Stepanov's "From Mathematics to Generic Programming" or "Elements of Programming, worth checking this out.

Basically, the paper says that a type should implement _equality if only a == b should be provided, and only _ordering if a < b should also be provided. It also says that it should implement partial_ if values can be unordered, weak_ if a == b does not imply f(a) == f(b), and strong_ if a == b implies f(a) == f(b), where in both last cases "f reads only comparison-salient state that is accessible using the public const members".

The most interesting examples are:

• floats: implement multiple orderings. The default provided by operator<=> is partial_order because of NaN, however a total ordering is available in an opt-in way via the named comparison functions. That is a < b returns the partial order, but std::strong_order(a, b) returns the IEEE total order. The system is flexible enough to support this. It is as if in Rust one could implement PartialOrd::partial_cmp with different semantics than Ord::cmp, and also choose whether the PartialOrdor the Ord implementations map to < (I happen to think that one of Rust's std lib biggest mistakes is mixing operator overloading with mathematical semantics; they are orthogonal concerns that don't mix well).

• CaseInsensitvieString implements weak_ordering because a == b does not imply f(a) == f(b)

[gnzlbg]

Another related concern I have with how the current traits work is that there is no way to express that some PartialOrd relations actually denote a total order. For example, given:

impl PartialOrd<Foo> for Bar { ... }

there is no way to implement Ord<Foo> for Bar.

[RalfJung]

I am confused, of course you can implement Ord...? Or do you mean because it requires Eq?

[gnzlbg]

@RalfJung I've filled an issue in the rfc repo: https://github.com/rust-lang/rfcs/issues/2511

Maybe the explanation there is more clear?

[RalfJung]

Yes, I understand now where you are coming from. Thanks.