Order structure, an excercise in abstraction and multiple inheritance

Order structures seem to be abstract concepts of theoretical mathematics with
minor practical importance. But this is just at first glance. A closer look
reveals that many data types have order structure.

  • The basic types NATURAL, INTEGER, FLOAT etc. have a total order
  • The type SET[T] has a partial order with "is_subset" playing the role of
  • All inductive types have a partial order where "a<=b" means "a has been used
    directly or indirectly in the construction of b". E.g. any subtree of a tree
    is smaller than the tree.
  • The nodes in a graph have a preorder relation with "a<=b" meaning "a can
    reach b".
  • The functions "f:A->B" have a partial order where the "smaller" function has
    the same values as the "greater" function but has a restricted domain.
  • The predicates "p:T?" have a partial order where "a<=b" meaning "a" is
    stronger than "b", i.e. "a" has less elements for which it is true than "b".

The article Order structure, an excercise in abstraction and multiple inheritance
describes preorders and partial orders together with the basic assertions which can
be derived from the basic structure and its functions.

Why is it interesting to carve out the order structure?

It is possible to prove a lot of properties by just using the definition of
the functions of order relations. Any structure which inherits the appropriate
order relation has access to all already proved asssertions. The order classes
act as an "assertion library" and inheritance is reuse of these assertions.

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Felix version

Interesting to compare with the Felix version:


These are basically Haskell style typeclasses with assertions thrown in. Virtual functions are replaceable in instances, but they may come with defaults so you don't need to replace all of them. "axiom" is a misnomer, the set may neither be independent nor spanning.

Not shown: Felix also supports lemmas, theorems, and reductions. A lemma is a theorem that is simple enough an automatic theorem prover is expected to be able to prove it. At one stage Felix actually generated Why format files containing lemmas as proof goals, and Why, using Ergot, actually managed to prove one.

A reduction is an axiom or lemma that is actually executed by the compiler to reduce a term.

Felix also has a "axiom_check(..)" function which tests all matching axioms. Useful, proved my assertion that floating point addition was associative incorrect.

You may want to change the

You may want to change the settings on your Web server. I can access all kinds of log files, backups and even your SSH private keys!

Impressive. I didn't know of

Impressive. I didn't know of this language. Is it used actively?