Sorting lists with respect to a total preorder

Assume now that $\leq$ is a total preorder over a set $E$, that is, a binary relation satisfying the requirements in the predefined theory TOTAL-PREORDER of Section 7.11.4.

To define a stable sorting of a list $L$ of elements over $E$, we consider again each element of the list $L$ as a pair $(x, i)$, where $x$ is the value of the element in $E$ and $i$ is the number indicating the position of $x$ in $L$. We define an ordering $\ll$ on such pairs as follows, where now the definition of $\ll$ is slightly different given the non-strict nature of total preorders: $(x, i) \ll (y, j)$ iff either $y \not\leq x$ or $(x \leq y$ and $i \leq j)$. Then, the properties of $\leq$ imply that $\ll$ is a (non-strict) total order, i.e., it is reflexive, antisymmetric, transitive, and total. From this, the definition of a stable sorting under $\leq$ of a list $e_1, e_2,\ldots, e_n$ of elements from $E$ follows exactly the same steps as before: Take the list $(e_1, 1), (e_2, 2), \ldots, (e_n, n)$, find its unique ordering $(e_{s_1}, s_1), (e_{s_2}, s_2), \ldots, (e_{s_n}, s_n)$ under $\ll$, and output $e_{s_1}, e_{s_2}, \ldots , e_{s_n}$.

The following modules WEAKLY-SORTABLE-LIST' and SORTABLE-LIST' specify the mergesort algorithm with respect to a total preorder and a (non-strict) total order, respectively. Their structure is completely analogous to the structure of WEAKLY-SORTABLE-LIST and SORTABLE-LIST already explained above. It is described in the two diagrams of Figure 7.5, where the sort renamings have been abbreviated to $\gamma$ and $\gamma'$, TOTAL-PREORDER to T-PREORDER, TOTAL-ORDER to T-ORDER, and WEAKLY-SORTABLE-LIST' W-S-LIST'.

Figure 7.5: Another version of sortable lists

  fmod WEAKLY-SORTABLE-LIST'{X :: TOTAL-PREORDER} is
    pr LIST{TOTAL-PREORDER}{X} 
         * (sort NeList{TOTAL-PREORDER}{X} to NeList{X},
            sort List{TOTAL-PREORDER}{X} to List{X}) .
    sort $Split{X} .

    vars E E' : X$Elt .
    vars A A' L L' : List{X} .
    var  N : NeList{X} .

    op sort : List{X} -> List{X} .
    op sort : NeList{X} -> NeList{X} .
    eq sort(nil) = nil .
    eq sort(E) = E .
    eq sort(E N) = $sort($split(E N, nil, nil)) .

    op $sort : $Split{X} -> List{X} .
    eq $sort($split(nil, L, L')) = $merge(sort(L), sort(L'), nil) .

    op $split : List{X} List{X} List{X} -> $Split{X} [ctor] .
    eq $split(E, A, A') = $split(nil, A E, A') .
    eq $split(E L E', A, A') = $split(L, A E, E' A') .

    op merge : List{X} List{X} -> List{X} .
    op merge : NeList{X} List{X} -> NeList{X} .
    op merge : List{X} NeList{X} -> NeList{X} .
    eq merge(L, L') = $merge(L, L', nil) .

    op $merge : List{X} List{X} List{X} -> List{X} .
    eq $merge(L, nil, A) = A L .
    eq $merge(nil, L, A) = A L .
    eq $merge(E L, E' L', A) 
      = if E <= E' 
        then $merge(L, E' L', A E)
        else $merge(E L, L', A E')
        fi .
  endfm

  fmod SORTABLE-LIST'{X :: TOTAL-ORDER} is
    pr WEAKLY-SORTABLE-LIST'{TOTAL-ORDER}{X} 
         * (sort NeList{TOTAL-ORDER}{X} to NeList{X},
            sort List{TOTAL-ORDER}{X} to List{X}) .
  endfm

Apart from the changes in the requirement theories and the module names, the main difference bewteen both approaches appears in the third $merge equation. In the WEAKLY-SORTABLE-LIST module we have

  eq $merge(E L, E' L', A) 
    = if E' < E 
      then $merge(E L, L', A E')
      else $merge(L, E' L', A E)
      fi .

Here we are dealing with a strict weak order. We test E' < E. If it is true, then by irreflexivity we know that E < E' is false, and the element E' from the second list is appended to the merged list. Whereas if E' < E is false, we know that either E < E' holds or E and E' are incomparable. Either way, the element E from the first list is appended to the merged list, either because it is smaller or because it is incomparable and we are preserving the original relative positions in the list (stability).

On the other hand, in the WEAKLY-SORTABLE-LIST' module we have

  eq $merge(E L, E' L', A) 
    = if E <= E' 
      then $merge(L, E' L', A E)
      else $merge(E L, L', A E')
      fi .

In this case we are dealing with a total preorder. We test E <= E'. If it is true, then either E' <= E is false or E and E' are equivalent. Either way, the element E from the first list is appended to the merged list, either because it is smaller or because it is equivalent and we are preserving the original relative positions in the list (stability). If E <= E' is false, then E' <= E holds by totality and therefore E' is appended to the merged list.

We can redo with these modules the same instantiation we considered above, but using now the predefined view String<= from TOTAL-ORDER to String, where <= is the non-strict lexicographic order on strings.

  fmod STRING-SORTABLE-LIST' is
    pr SORTABLE-LIST'{String<=} .
  endfm

  Maude> red in STRING-SORTABLE-LIST' :
           sort("a" "quick" "brown" "fox" "jumps" 
                "over" "the" "lazy" "dog") .
  result NeList{String<=}: 
    "a" "brown" "dog" "fox" "jumps" "lazy" "over" "quick" "the"

  Maude> red sort("a" "quick" "brown" "fox" "jumps" "over" "the" 
                  "lazy" "dog" "a" "quick" "brown" "fox" "jumps" 
                  "over" "the" "lazy" "dog") .
  result NeList{String<=}: "a" "a" "brown" "brown" "dog" "dog" "fox" 
    "fox" "jumps" "jumps" "lazy" "lazy" "over" "over" "quick" "quick" 
    "the" "the"