[kraghen]

All orderings must be specified as a reduction to a primitive order using the fact that if you have an equivalence relation on some type A and a reduction f : B -> A then you have an equivalence on B defined by x = y when f(x) = f(y).

Now, take the rational numbers. For the usual binary comparison we can simply define (a/b) < (c/d) as ad < cb. It's not obvious how to express this as a reduction to a primitive ordering (the answer is to compute the continued fraction).

In fact, I'm not aware of any systematic way of deriving discrimination-suitable orderings from binary predicates -- it might be an open research problem, as far as I am aware.

[KirinDave]

> In fact, I'm not aware of any systematic way of deriving discrimination-suitable orderings from binary predicates -- it might be an open research problem, as far as I am aware.

That'd be an even more remarkable discovery in light of the stuff you worked on though, wouldn't it?

[kraghen]

It might, I never really discussed this aspect with Fritz! For my thesis I was mostly focussed on applications to database queries, and I never encountered any concrete examples of orderings that couldn't be dealt with in an obvious way using discrimination based sorting.