The formal conditions stated in Trait PartialOrd give surprising results

Location (URL)

https://doc.rust-lang.org/std/cmp/trait.PartialOrd.html

Summary

PartialOrd states the following requirements for partial_cmp():

consistency with PartialEq
transitivity
duality

Consistency with PartialEq means (see also #57157):

partial_cmp(x, y) == Some(Equal) iff eq(x, y) == true

Consider the following minimal example:

an underlying set { a, b, c }
a (total) equivalence relation with partition { a, b }, { c } (i.e., a == b and reflexivity)
a partial order { a < c, c > a } (not including b < c and c > b; including a == b and reflexivity)

Duality is satisfied, and transitivity is also satisfied (there is only one < relation, so no other implied relations).

In the above example, it is expected that a and b are interchangeable (this is the intuitive meaning of "equivalence"), but they are not:

(a < c) != (b < c)

Does the above example satisfy the (intended) requirements, or is something missing in the formal conditions? The link to the wikipedia article on partial order does not bring much light.

Apart from the theoretical aspect, there might be a practical issue. Assume (for simplicity) that I have a type T as in the above example, which in addition implements Clone, and a variable v = a. I define clone() as the mapping

a -> b; b -> b; c -> c

(i.e., it "normalizes" a to b). If I understand the clone() requirements correctly, this is acceptable, since

clone(x) == x for any x in T

Now I get the surprising result:

(v < c) != (clone(v) < c)

I would expect that cloning does not change the result of the comparison.

Does this example correctly implement the semantics you described? playground

use std::cmp::Ordering;

enum MySet {
    A,
    B,
    C,
}

impl PartialEq for MySet {
    fn eq(&self, other: &MySet) -> bool {
        use MySet::*;
        match (self, other) {
            // reflexivity
            (A, A) | (B, B) | (C, C) => true,
            // A == B
            (A, B) | (B, A) => true,
            // C not equal to anything else
            (A, C) | (B, C) | (C, A) | (C, B) => false,
        }
    }
}

impl PartialOrd for MySet {
    fn partial_cmp(&self, other: &MySet) -> Option<Ordering> {
        use MySet::*;
        match (self, other) {
            // reflexivity
            (A, A) | (B, B) | (C, C) => Some(Ordering::Equal),
            // A == B
            (A, B) | (B, A) => Some(Ordering::Equal),
            // A < C
            (A, C) => Some(Ordering::Less),
            (C, A) => Some(Ordering::Greater),
            // B, C unordered
            (B, C) | (C, B) => None,
        }
    }
}

impl Clone for MySet {
    fn clone(&self) -> Self {
        use MySet::*;
        match self {
            // A == A -> B == A
            A => B,
            // B == B -> B == B
            B => B,
            // C == C -> C == C
            C => C,
        }
    }
}

fn main() {
    let v = MySet::A;
    dbg!(v < MySet::C);         // true
    dbg!(v.clone() < MySet::C); // false
}

Yes, this is exactly my example.

You can add also:

    dbg!(v == v.clone()); // true

I think what is meant is that PartialOrd must "respect" PartialEq, in the sense that if x == y then x and y should be treated as interchangeable. This is the intended meaning of "partial equivalence" in general (for the whole application), and in particular for PartialOrd. In the above example, to respect a == b, partial_cmp should also define b < c and c > b.

The missing formal condition is that transitivity and duality must hold for the equivalent classes defined by PartialEq. This makes sense when Rhs==Self, and I suppose it can be extended to the general case where Rhs and Self are different. In any case it is more tricky than the stated formal conditions in the documentation. So either the documentation clearly states the formal conditions which give the intended behavior, or (as it is now) it leaves room for surprising (and unwanted) behavior.

It's a bit late for me to fully comprehend what is going on here but I'll double check for the sake of #164473 later. My gut feeling is just that either the intuition provided about partial orderings is incorrect (that they are interchangeable in partial equality) or that the reasoning about the requirements for partial orderings is not correct.

The only way to extend the above example to a total Ord, is to assign cmp(b, c) = Less. This respects the equivalence of a and b, i.e., a and b are interchangeable in the scope of Ord.

More generally, for a type T: Ord, assume two elements a and b in the same equivalence class (a == b), and an element c outside of this equivalence class. Then

a < c ==> b < c

All other choices are impossible: b == c is excluded by the assumption that c is not in the equivalence class of b; b <> c [this is a symbol for partial_cmp(b, c) == None] is excluded by the assumption that T is a total Ord; b > c is excluded due to transitivity (a < c && c < b ==> a < b, but we assumed a == b).

However for a type T: (Eq, PartialOrd) and for the same conditions as above,

a < c ==> (b < c) || (b <> c)

The last possibility (b <> c) makes a and b non-interchangeable in the scope of PartialOrd. It is true that a and b cannot have opposite comparison to c, i.e., (a < c) && (b > c) is always false, but otherwise they are not interchangeable. Maybe we could say that they are "partially interchangeable", although this term is not common. More formally,

(a == b) && (partial_cmp(a, c) == None) == (partial_cmp(b, c) == None) ==>
(a == c) == (b == c) && (a < c) == (b < c) && (a > c) == (b > c)

In words, for two equivalent elements a and b, same comparability with c implies same comparison with c.

For T: Ord comparability is always true, therefore the above statement simplifies to: two equivalent elements a and b have the same comparison with any element c.

Your example violates transitivity of <=. Too bad we don't require that, and it's not a corollary 🙃

We do require transitivity of <=, both in the new guarantees listed in #164473:

Transitivity: for all a, b, c of type A, a < b and b < c implies a < c. This must also work for longer chains and all possible operators such as > and ==.

And in the existing guarantees:

Transitivity: if A: PartialOrd<B> and B: PartialOrd<C> and A: PartialOrd<C>, then a < b and b < c implies a < c. The same must hold for both == and >. This must also work for longer chains, such as when A: PartialOrd<B>, B: PartialOrd<C>, C: PartialOrd<D>, and A: PartialOrd<D> all exist.

Simply put, if transitivity is guaranteed for both < and =, it is guaranteed for <=.

Simply put, if transitivity is guaranteed for both < and =, it is guaranteed for <=.

That does not follow. x == y < z does not let you infer x <= z from these axioms. This is exactly the case the example in the issue exploits

Exactly, this was my observation behind this example. Equality and inequalities are disconnected in the axioms.

In particular, if we had transitive <=, this would force b == a < c implies b <= c implies b < c or b == c, neither of which is the case here

So, it does turn out that the reasoning here is because we're using the definition of partial orderings incorrectly.

Ordinarily, partial orderings define transitivity in terms of <= for exactly this reasoning, and only strict partial orderings require transitivity for < as well. I can update this in the PR.

yeah this is clearly not the theory the docs intended to axiomatize

Thanks for finding this!

Transitivity of <= does imply transitivity of < however:

x < y < z implies x <= y <= z implies x <= z implies x < z or x == z

Suppose x == z. Then x <= y <= z <= x implies y <= x implies x >= y, which contradicts x < y, because the value of x.partial_cmp(y) is inconsistent.

Hence x < z

#164473 now has been updated to guarantee the properties which I believe to be substantially more correct with respect to ordering, which are also consistent with floating point numbers and our current implementations. Please do take a look at the docs (which have been rendered in the PR description for easy reading) to help ensure that they do what we want here.

I think it is useful to give the intended behavior of equivalence in the docs.

Under the axioms of A: Eq, the intuitive meaning of x == y is that x and y are interchangeable. Violation of this property may (or may not) be a logical error. The axioms of A: Ord enforce this property in the scope of Ord. If this is the wanted behavior of type A, the program should treat x and y as interchangeable, e.g., match branches for x and y should be equivalent.

Under the axioms of A: PartialEq, the elements of A are partitioned into equivalence classes containing one or more elements of A, and the class of divergent elements of A (which is empty for Eq). Elements belonging in the same equivalence class are not distinguishable using the == operator and can be considered as interchangeable. The divergent elements can be identified with x != x and ~~can be considered as interchangeable, since~~ they are not distinguishable using the == operator [EDIT: but may be distinguished using the < operator; see below].

Yup, exactly. And note that the new docs does mention the interchangeable property for ordering specifically (since we can't guarantee it for every operation):

Substitutability: if a == b, then for any given logical formula containing only logical operators and ordering relations (<, <=, ==, >=, >) you can replace a with b without changing its meaning, and similarly replacing b with a.

Like you said, PartialEq only indicates that some values are not equal to themselves, but those which are equal can be interchanged.

Divergent elements are not distinguishable using ==, but they may be distinguished using <. Example:

an underlying set { d1, d2 }
empty partial equivalence (eq(x, y) = false for any x, y)
partial order d1 < d2 and d2 > d1 (not including reflexivity)

If v is a value of this type, then

v == d1 is always false and doesn't give any information about v
if v < d2 is true then v must be d1; if v < d2 is false then v must be d2

Navigation Menu

Repository navigation

The formal conditions stated in Trait PartialOrd give surprising results #164184

Location (URL)

Summary

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

The formal conditions stated in Trait PartialOrd give surprising results #164184

Description

Location (URL)

Summary

Activity

asquared31415 commented on Oct 12, 2026

georgeef commented on Oct 12, 2026

georgeef commented on Oct 12, 2026

clarfonthey commented on Oct 22, 2026

georgeef commented on Oct 22, 2026

maxdexh commented on Oct 22, 2026

clarfonthey commented on Oct 22, 2026

maxdexh commented on Oct 22, 2026

georgeef commented on Oct 22, 2026

maxdexh commented on Oct 22, 2026

clarfonthey commented on Oct 22, 2026

maxdexh commented on Oct 22, 2026

maxdexh commented on Oct 22, 2026

maxdexh commented on Oct 22, 2026

clarfonthey commented on Oct 22, 2026

georgeef commented on Oct 22, 2026

clarfonthey commented on Oct 22, 2026

georgeef commented on Oct 23, 2026

Metadata

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Issue actions