Strict weak ordering extensions

A strict weak ordering (swo for short) is a binary relation < on a set A such that its complementary relation ≥ = AxA − < is a total preorder (reflexive, transitive and such that x ≥ y or y ≥ x, or both, for all x, y in A).

We introduce the notion of an extension to a strict weak ordering: Given <_A a swo on A, a swo extension of <_A to B, where B is a set disjoint with A, is a pair of relations <_A→B from A to B and <_B→A from B to A for which there is some swo <_AUB on AUB such that <_A = <_AUB ∩ AxA, <_A→B = <_AUB ∩ AxB, <_B→A = <_AUB ∩ BxA.

Theorem. (<_A→B,<_B→A) is a swo extension of <_A iff for all a, a' in A, b in B.

1. a <_A→B b → not(b <_B→A a),
2. not(a <_A→B b) and not(a' <_A a) → not(a' <_A→B b),
3. not(b <_B→A a) and not(a <_A a') → not(b <_B→A a').

Proof. If (<_A→B,<_B→A) is a swo extension of <_A, 1, 2 and 3 follow trivially from the properties of a swo on AUB. As for the converse, let us define the binary relation <_B on B as follows: b <_B b' iff there is some a in A such that at least one of the following two conditions hold:

1. not(a <_A→B b) and a <_A→B b',
2. b <_B→A a and not(b' <_B→A a) .

We will prove that <_AUB = <_A U <_A→B U <_B→A U <_B is a swo on B by showing that ≥_AUB = (AUB)x(AUB) − <_AUB is a total preorder. In the following we will consider x, y, z in AUB:

• Reflexivity (x ≥_AUB x): if x is in A, reflexivity follows from the properties of <_A. If x is in B and x <_AUB x, there would be some a in A verifying the contradictory (not(a <_A→B x) and a <_A→B x) or (x <_B→A a and not(x <_B→A a)).
  
• Transitivity (x ≥_AUB y and y ≥_AUB z → x ≥_AUB z):
  
  1. x, y, z in A: from the properties of <_A.
  2. x, y in A, z in B: from property 2.
  3. x in A, y in B, z in A: If x <_A z then not(z <_A x), which along with the hypothesis not(x <_A→B y) implies by property 2 that not(z <_A→B y), in contradiction with not(y <_B→A z) by property 1.
     
  4. x in A, y, z in B: if x <_A→B z, we would have by the hypothesis not(y <_B z) and the definition of <_B that x <_A→B y, in contradiction with the hypothesis not(x <_A→B y).
     
  5. x in B, y, z in A: from property 3.
  6. x in B, y in A, z in B: for any a in A, if not(a <_A y) then by property 2 not(a <_A→B z); and if not(y <_A a) we have by property 3 that not(x <_B→A a). So, the conditions for x <_B z are never satisfied.
  7. x, y in B, z in A: if x <_B→A z then by the hypothesis not(y <_B z) and the definition of <_B we would have the contradictory x <_B y.
  8. x, y, z in B: for any a in A, if not(a <_A→B x) then not(a <_A→B y) and thus not(a <_A→B z); whereas if x <_B→A a then y <_B→A a and hence z <_B→A a; so, it is not the case that x <_B z.
     
• Comparability (x ≥_AUB y or y ≥_AUB x):
  
  1. x, y in A: from the properties of <_A.
  2. x in A, y in B: from property 1.
  3. x in B, y in A: from property 1.
  4. x, y in B: if x <_B y then there exists some a in A such either not(a <_A→B x) and a <_A→B y, which implies not(a <_A→B x) and not(y <_B→A a); or else x <_B→A a and not(y <_B→A a), which also implies not(a <_A→B x) and not(y <_B→A a). Thus in either case y≥_AUB a ≥_AUB x, and by the transitivity of ≥_AUB, it follows that x ≥_AUB y.
     

Swos are important in C++ because sorting algorithms take comparison objects with swo semantics. The swo extension concept that we have developed is related to the notion of partitioning introduced by the C++ standard to describe binary search algorithms, as we will see in a later entry.