Document "latent requirements" of PartialOrd

[gnzlbg]

The PartialOrd docs do not document what is de facto required of trait implementors in order for data structures to work correctly. We should update them!

Per @RalfJung's comment below:

FWIW our conclusion was that we basically already require < to be irreflexive, since that is the only way the following equivalences can be upheld:

• x < y iff x.partial_cmp(y) == Some(Less)
• x == y iff x.partial_cmp(y) == Some(Equal)
• x > y iff x.partial_cmp(y) == Some(Greater)

The docs are not explicitly stating that these equivalences must hold, but it seems very much against the spirit of this trait to allow violations of these equivalences. The fact that PartialOrd: PartialEq is very useful here as it makes the 2nd axiom well-defined.

This post used to say something different. Here is the original post

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]

2. 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?