3 ms·
Another common class of bugs in C++ is comparison functions that don't respect the strict weak ordering axioms [1]. I've seen a lot of implementations in which
by ot 9y ago
Another common class of bugs in C++ is comparison functions that don't respect the strict weak ordering axioms [1]. I've seen a lot of implementations in which cmp(x, x) is true.
This causes undefined behavior in STL algorithms, for example std::sort can easily go out of bounds.
A good rule of thumb to remember the axioms is that the comparator should behave like <, not <=.
[1] http://en.cppreference.com/w/cpp/concept/LessThanComparable http://en.cppreference.com/w/cpp/concept/LessThanComparable
- HumanDrivenDev 9y agoAre there type systems where these axioms can be encoded? Dependent typing, perhaps.
- im3w1l 9y agoInstead of having a function that says whether one object is bigger than another, you could define an ordering by having a function that maps objects to say natural numbers or real numbers or some other object with a known good comparison, and then compare the mapped objects. So instead of implementing f in f(a, b), you'd implement f in f(a) < f(b)
- abecedarius 9y agoAlso you could resolve hashing in the same way: i.e. making sure that hashing is consistent with equality. Two objects of the same type are equal if f(a) == f(b), and have hashcode hash(type, f(a)).
- aweinstock 9y agoAs an exercise in learning Coq, I've implemented a proof-carrying version of the partial-ordering relation: https://github.com/aweinstock314/coq-stuff/blob/a1831f9e1e957c0038996a5a65fcb4391967660a/poset_lattice.v#L3-L24 https://github.com/aweinstock314/coq-stuff/blob/a1831f9e1e95... There's four different types there: POSET, POSET_PROOFS, Pord, and POSET'. - POSET only has an underlying type t and a function "leq" that takes two elements of type t and returns a bool (but doesn't enforce semantics of that bool). - POSET_PROOFS embeds a POSET, and carries three proofs (reflexivity, antisymmetry, and transitivity) certifying that the underlying "leq" function is actually the less-than-or-equal function of a partial ordering. - Pord is a result type with 4 values meant to denote the exhaustive possiblities of "strictly less"/"equal"/"strictly greater"/"uncomparable". - POSET' has a type t', a function "pcomp" that takes two elements of type t' and returns a Pord, and a proof for transitivity in the "strictly less" case. POSET' has fewer fields to instantiate, but POSET_PROOFS allows writing proofs that are closer to traditional math. Fortunately, the fact that it's possible to write conversions between POSET_PROOFS and POSET' (done in the code as "from" and "to" in the POSET_ISOMORPHIMS module right below) indicate that they have the same properties.
- deleted 9y ago[deleted]
- contravariant 9y agoWeirdly enough in mathematics it's far more common to define <= instead of <. With a<b simply being shorthand for 'a<=b and not b<=a'. The definitions also seem to be simpler that way.
- baddox 9y agoIs that so? I thought the “equals” relation was usually well-defined in formal math. What’s an instance where this isn’t the case? Perhaps the reals?
- contravariant 9y agoEquality and equivalence get murky sometimes. Often there is some sense of equivalence that's 'good enough'. Like spaces that are isomorphic or functions that are equal 'almost everywhere'. Now in by far the majority of cases inequality is defined for partial orders, which have the property that a<=b and b<=a imply a=b, so in that case a<=b and not b<=a implies b=/=a, but (non-strict) weak orders can have a<=b and b<=a without necessarily a=b. I'm pretty sure there are also a few cases where they just prove reflexivity and transitivity and just make a and b where a<=b and b<=a equal by definition. I think you could use this in the definition for real numbers, but usually the equivalence classes are defined first and inequality is defined afterwards (which might be more work).