STRICT-WEAK-ORDER and STRICT-TOTAL-ORDER

Although in Section 6.3.6 we have defined the notion of sorted list as based on a totally ordered set of elements, we will see in Section 7.12.6 how to relax this requirement in two different ways. The first possibility is to consider a partially strictly ordered set where the incomparability relation is transitive, that is, if $a$ is not comparable with $b$ and $b$ is not comparable with $c$ with respect to the given order, then $a$ and $c$ are not comparable either. The predefined STRICT-WEAK-ORDER theory below specifies a strict partial order with this additional requirement, a concept known as strict weak order. The second possibility is to consider a total preorder, as specified in Section 7.11.4 below.

Given a strict partial order $<$, that is, an irreflexive and transitive binary relation, we define the incomparability relation by $x \sim y$ iff both $x \not< y$ and $y \not< x$. Incomparability is symmetric by definition, and its reflexivity follows from the irreflexivity of $<$. Therefore, when we impose the additional requirement of transitivity of incomparability, we get that the relation $\sim$ for a strict weak order is an equivalence relation.

Notice that STRICT-WEAK-ORDER, as presented below, imports the theory TRIV and also (in protecting mode) the module BOOL. The three equations express the required properties (antisymmetry is derivable from irreflexivity and transitivity) of the binary relation _<_ on the sort Elt, as is made explicit in the corresponding labels.

  fth STRICT-WEAK-ORDER is
    protecting BOOL .
    including TRIV .
    op _<_ : Elt Elt -> Bool .
    vars X Y Z : Elt .
    ceq X < Z = true if X < Y /\ Y < Z [nonexec label transitive] .
    eq X < X = false [nonexec label irreflexive] .
    ceq X < Y or Y < X or Y < Z or Z < Y = true if X < Z or Z < X
      [nonexec label incomparability-transitive] .
  endfth

The following theory extends the previous one with a totality requirement, thus specifying a strict total order. Under these conditions, the incomparability relation reduces to the identity (because any pair of different elements is comparable) and the transitivity of incomparability holds trivially.

  fth STRICT-TOTAL-ORDER is
    including STRICT-WEAK-ORDER .
    vars X Y : Elt .
    ceq X = Y if X < Y = false /\ Y < X = false [nonexec label total] .
  endfth

The theory STRICT-TOTAL-ORDER is a different presentation of the equivalent theory STOSET for strict total orders introduced in Section 6.3.1.

There is a view from TRIV to STRICT-WEAK-ORDER that forgets the order and its properties. The name of this view coincides with the name of the target theory.

  view STRICT-WEAK-ORDER from TRIV to STRICT-WEAK-ORDER is 
  endv

The inclusion from the theory STRICT-WEAK-ORDER into STRICT-TOTAL-ORDER gives rise to another view, which is also called as the target theory.

  view STRICT-TOTAL-ORDER from STRICT-WEAK-ORDER
    to STRICT-TOTAL-ORDER is 
  endv

The Maude library includes views that map from STRICT-TOTAL-ORDER to built-in data type modules by selecting the main sort and the standard strict total order between the corresponding elements, namely, the ``less than'' comparison between numbers and the lexicographic ordering between strings, as described in previous sections. Again, operator mappings that are the identity (in this case of the form op _<_ to _<_) do not appear explicitly in the following views, but are left implicit. These views are named by appending ``<'' to the name of the selected sort; for example, the standard view from STRICT-TOTAL-ORDER into RAT is named Rat<.

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

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

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

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

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

As explained in Section 6.3.2, these views impose some proof obligations corresponding in this case to the properties that are stated about the binary relation selected in the target module; recall that such proof obligations are not discharged or checked by the system.