Order

Remco Bloemen

2015-08-26

Given a set 𝒮\mathcal S. Assume nothing of this set, other than that it may or may not have elements and that we can check if two elements are the same.

Think for example of a set of instances of a particular class.

I will now explain what it formally means to have an order between the instances. What different kinds of order there are and why it matters.

Relations

Suppose we have a function, taking two elements of this set and giving a boolean in return. We can formally write the type of this function as:

f:𝒮×𝒮𝔹 f : \mathcal S \times \mathcal S \rightarrow \mathbb{B}

Such functions, return true or false given two elements, is called a ‘binary relation’. The equality operation on the elements of our set is an example.

In mathematics the function notation is often replaced with an infix notation. Sometimes, the relation is even seen as something different than a function. I disagree with this, I find the function concept very useful when dealing with programming languages. This whole confusion is the reason why C++ has weird special functions like operator==.

Other examples of such functions are ‘divides’ on integers, ‘orthogonal’ on vectors and ‘less than’ on numbers.

Strict partial order

A strict partial order is a binary relation << with the following properties:

Irreflexivity:

𝒮x(x<x( \mathrm{\nexists }^{x}_{\mathcal S} \left(x < x\right(

Transitivity:

𝒮a𝒮b𝒮c(a<b((b<c((a<c( \mathrm{\forall }^{a}_{\mathcal S}\mathrm{\forall }^{b}_{\mathcal S}\mathrm{\forall }^{c}_{\mathcal S}\; \left(a < b\right( \wedge \left(b < c\right( \rightarrow \left(a < c\right(

From this we can derive more properties, for example asymmetry:

𝒮a𝒮b(a<b(¬(b<a( \mathrm{\forall }^{a}_{\mathcal S}\mathrm{\forall }^{b}_{\mathcal S}\; \left(a < b\right( \rightarrow \neg \left(b < a\right(

PROOF: Take the transitivity property and with c=ac = a: 𝒮a𝒮b(a<b((b<a((a<a(\mathrm{\forall }^{a}_{\mathcal S}\mathrm{\forall }^{b}_{\mathcal S}\; \left(a < b\right( \wedge \left(b < a\right( \rightarrow \left(a < a\right( We can rephrase the irreflexivity as 𝒮a¬(a<a(\mathrm{\forall }^{a}_{\mathcal S}\; \neg \left(a < a\right( From the law of the excluded middle we then have (a<a(\left(a < a\right( \leftrightarrow ⊥, substitute this: 𝒮a𝒮b(a<b((b<a(\mathrm{\forall }^{a}_{\mathcal S}\mathrm{\forall }^{b}_{\mathcal S}\; \left(a < b\right( \wedge \left(b < a\right( \rightarrow ⊥ Which means that: 𝒮a𝒮b¬((a<b((b<a((\mathrm{\forall }^{a}_{\mathcal S}\mathrm{\forall }^{b}_{\mathcal S}\; \neg \left( \left(a < b\right( \wedge \left(b < a\right( \right( 𝒮a𝒮b(a<b(¬(b<a(\mathrm{\forall }^{a}_{\mathcal S}\mathrm{\forall }^{b}_{\mathcal S}\; \left(a < b\right( \rightarrow \neg \left(b < a\right( QED.

We can also define a non-strict partial order as

(ab((a<b((a=b( \left(a \leq b\right( \leftrightarrow \left(a < b\right( \lor \left(a = b\right(

and introduce >> and \geq by flipping the arguments.

It is called a partial order because there can be incomparable objects. Some comparisons are inconclusive, we can have aba \neq b but a<ba < b and b<ab < a can still be both false.

The partial order relation defines a directed acyclic graph over the elements of 𝒮\mathcal S. Conversely, any directed acyclic graph can be turned into a partial order by taking the transitive closure. For example, the divides relation on integers is a partial order, even though it might seem to have little to do with an order.

In particular, any tree structure is a partial order with its non-direct descendant of relation. For example, subset of, substring of, etc…

Strict total order

A strict total order is a strict partial order with an addition axiom:

Totality:

𝒮a𝒮b(ab((a<b((b<a( \mathrm{\forall }^{a}_{\mathcal S}\mathrm{\forall }^{b}_{\mathcal S}\; \left(a \neq b\right( \rightarrow \left(a < b\right( \lor \left(b < a\right(

That this implies only one of a < b and b < a is true is a consequence of the asymmetry property we have proven.

Strict well-order

An order is well-order if for any element there are only a finite number of elements less than it.

This has a number of interesting mathematical consequences:

These orders allow induction over the element in the

,3,2,1,0,1,2,3, \ldots ,-3,-2,-1,0,1,2,3,\ldots

has no lest element, but if we re-arrange it to be:

0,1,2,3,,1,2,3, 0,1,2,3,\ldots ,-1,-2,-3,\ldots

it becomes a well-order of type ω+ω. This order can be easily defined in pseudo code

ω-order

The above example for the integers is still not as natural as I would like it to be. The problem is, it has two ellipsis (…). If I start counting from 0, I will never reach the negative numbers. But if we re-arrange it as:

0,1,1,2,2,3,3, 0, -1, 1, -2, 2, -3, 3, \ldots

For example with this function:

then it becomes countable!

A ω-order is countable. It can be brought in to one-on-one correspondence with the natural numbers without rearanging the order. As a consequence, these orders are perfectly concise Gödel numbering.

This conciseness is used in Google’s Protocol Buffers to store signed integers. They call it ZigZag encoding and found an elegant mapping between the integers and naturals by exploiting the twos-complement.

Well-founded strict total order.

See: http://www.karlin.mff.cuni.cz/~jezek/120/transitive1.pdf