TOTAL-PREORDER and TOTAL-ORDER

The predefined TOTAL-PREORDER theory specifies, as its name clearly suggests, a total preorder, that is, a total binary relation which is reflexive and transitive. This theory will also be used as requirement for sorting lists in Section 7.12.6.

The notions of strict weak order (see Section 7.11.3) and of total preorder are complementary: the set-theoretic complement of a strict weak order is a total preorder and vice versa. They can also be related in a way that preserves the direction of the order. Given a strict weak order $<$, a total preorder $\leq$ is obtained by defining $x \leq y$ whenever $y \not< x$. In the other direction, a strict weak order $<$ is obtained from a total preorder $\leq$ by defining $x < y$ whenever $y \not\leq x$.

Given a total preorder $\leq$, we say that two elements $x$ and $y$ are equivalent iff both $x \leq y$ and $y \leq x$. Then, it follows from the properties of a total preorder that this is an equivalence relation and, furthermore, two elements are equivalent in a total preorder if and only if they are incomparable in the associated strict weak order (we have seen in Section 7.11.3 that the incomparability relation $\sim$ associated to a strict weak order is an equivalence relation).

Both kinds of relations capture the notion that the set of elements is split into partitions which are linearly ordered. This situation naturally arises when records are compared on a given field.

The theory TOTAL-PREORDER, as presented below, imports the theory TRIV and the module BOOL. The three equations express the required properties of the binary relation _<=_ on the sort Elt.

  fth TOTAL-PREORDER is
    protecting BOOL .
    including TRIV .
    op _<=_ : Elt Elt -> Bool .
    vars X Y Z : Elt .
    eq X <= X = true [nonexec label reflexive] .
    ceq X <= Z = true if X <= Y /\ Y <= Z [nonexec label transitive] .
    eq X <= Y or Y <= X = true [nonexec label total] .
  endfth

A total order is a total preorder that, in addition, is antisymmetric.

  fth TOTAL-ORDER is
    inc TOTAL-PREORDER .
    vars X Y : Elt .
    ceq X = Y if X <= Y /\ Y <= X  [nonexec label antisymmetric] .
  endfth

The theory TOTAL-ORDER is a different presentation of the equivalent theory NSTOSET for non-strict total orders introduced in Section 6.3.1. Its name follows the usual convention according to which, when nothing is said, a total order is assumed to be reflexive, that is, non-strict.

There is a view from TRIV to TOTAL-PREORDER, named like the target theory, that forgets the binary relation and its preorder properties.

  view TOTAL-PREORDER from TRIV to TOTAL-PREORDER is 
  endv

The following view represents the inclusion from the TOTAL-PREORDER theory into TOTAL-ORDER.

  view TOTAL-ORDER from TOTAL-PREORDER to TOTAL-ORDER is 
  endv

In the Maude prelude we can also find views that map from TOTAL-ORDER to several built-in data type modules by selecting the main sort and the standard non-strict total order between the corresponding elements, namely, the ``less than or equal to'' comparison between numbers and the lexicographic ordering between strings. These views are named by appending ``<='' to the name of the selected sort; for example, the standard view from TOTAL-ORDER into FLOAT is named Float<.

  view Nat<= from TOTAL-ORDER to NAT is
    sort Elt to Nat .
  endv

  view Int<= from TOTAL-ORDER to INT is
    sort Elt to Int .
  endv

  view Rat<= from TOTAL-ORDER to RAT is
    sort Elt to Rat .
  endv

  view Float<= from TOTAL-ORDER to FLOAT is
    sort Elt to Float .
  endv

  view String<= from TOTAL-ORDER to STRING is
    sort Elt to String .
  endv

Again, these views impose some proof obligations that are not discharged or checked by the system.