Category: functors | Component type: concept |
First argument type | The type of the Strict Weak Ordering's first argument. |
Second argument type | The type of the Strict Weak Ordering's second argument. The first argument type and second argument type must be the same. |
Result type | The type returned when the Strict Weak Ordering is called. The result type must be convertible to bool. |
F | A type that is a model of Strict Weak Ordering |
X | The type of Strict Weak Ordering's arguments. |
f | Object of type F |
x, y, z | Object of type X |
Name | Expression | Precondition | Semantics | Postcondition |
---|---|---|---|---|
Function call | f(x, y) | The ordered pair (x,y) is in the domain of f | Returns true if x precedes y, and false otherwise | The result is either true or false |
Irreflexivity | f(x, x) must be false. |
Antisymmetry | f(x, y) implies !f(y, x) |
Transitivity | f(x, y) and f(y, z) imply f(x, z). |
Transitivity of equivalence | Equivalence (as defined above) is transitive: if x is equivalent to y and y is equivalent to z, then x is equivalent to z. (This implies that equivalence does in fact satisfy the mathematical definition of an equivalence relation.) [1] |
[1] The first three axioms, irreflexivity, antisymmetry, and transitivity, are the definition of a partial ordering; transitivity of equivalence is required by the definition of a strict weak ordering. A total ordering is one that satisfies an even stronger condition: equivalence must be the same as equality.