Swo extensions and C++

The specification of C++ binary search algorithms use the notion of partition to describe the acceptable algorithm arguments. For instance, the lower_bound algorithm:

template<class ForwardIterator, class T, class Compare>
ForwardIterator lower_bound(
  ForwardIterator first, ForwardIterator last,
  const T& value, Compare comp);

requires that the elements e of [first,last) be partitioned with respect to the expression comp(e,value), while equal_range:

template<class ForwardIterator, class T, class Compare>
pair<ForwardIterator, ForwardIterator> equal_range(
  ForwardIterator first, ForwardIterator last,
  const T& value, Compare comp);

requires that elements be partioned by comp(e,value) and by !comp(value,e), and moreover comp(e,value) must imply comp(e,value), i.e. the first partition must be a subset of the second.

Swo extensions and this kind of partitions are closely related:

Definition. Let (A,<_A) be a swo and X a subset of A. A subset P of X is said to be a partition of X if for every x in P, P includes every y in X such that not(x <_A y).

Theorem. Let (<_A→B,<_B→A) be a swo extension of <_A to B, X a subset of A and b an element of B. The sets

P = {x in X : x <_A→B b},
P' = {x in X : not(b <_B→A x)}

are partitions of X. Moreover, P is a subset of P'.

Proof. Let y such that not(x <_A y). By property 2 of the definition of a swo extension, if x <_A→B b and not(x <_A y) then y <_A→B b. Similarly, using property 3 of the definition of a swo we have that not(b <_A→B x) and not(x <_A y) implies not(b <_A→B y). The last claim is derived from property 1 of swos.

Theorem. Let (A,<_A) be a swo, B disjoint set of A, and P, P' : B → P(A) such that P(b) is included in P'(b) and both are partitions of A for every b. We define <_A→B : A → B and <_B→A : B → A as follows:

a <_A→B b iff a is in P(b),
b <_B→A a iff a is not in P'(b).

(<_A→B,<_B→A) is then a swo extension of <_A to B.

Proof. Property 1 of swos is derived from the fact that P(b) is included in P'(b) for every b in B. If not(a <_A→B b) , that is, a is not in P(b), and not(a' <_A a), that fact that P is a partition implies that a' is not in P(b), that is, not(a' <_A→B b). Finally, if not(b <_B→A a), that is, a is in P'(b), and not(a <_A a'), the fact that P' is a partition implies that a' is in P'(b), that is, not(b <_B→A a').

In my view, swo extensions allow for a richer mathematical treatment of the subject than a formulations based on partitions, but the latter are undeniably more comprehensible to the layman and so it is no wonder that partitions have been chosen to describe binary search algorithms in C++.

The draft of the upcoming C++0x standard gives the following definition of a partition:

A sequence [start, finish) is partitioned with respect to an expression f(e) if there exists an integer n such that for all 0 <= i < distance(start, finish), f(*(begin + i)) is true if and only if i < n.

At first look, our rendition of the concept of partition seems a univocal translation of the formulation given by the standard draft, but in reality the standard draft formulation is a little more lenient about the treatment of equivalent elements, i.e. elements a, b such that none is less than the other. So, there are C++-partitions that do not qualify as partitions according to our definition.