Sorting lists with respect to a strict weak order

Assume first that $<$ is a strict weak order over a set $E$, that is, a strict partial order with a transitive incomparability relation, which are precisely the requirements in the predefined theory STRICT-WEAK-ORDER of Section 7.11.3.

In order to define a stable sorting of a list $L$ of elements over $E$, we consider 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: $(x, i) \ll (y, j)$ iff either $x < y$ or $(x \sim y$ and $i < j)$. Then, it follows from the properties of $<$ and $\sim$ that $\ll$ is a strict total order, i.e., it is irreflexive, transitive, and total.

We can now define the stable sorting under $<$ of a list $e_1, e_2,\ldots, e_n$ of elements from $E$ as follows: 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 parameterized module WEAKLY-SORTABLE-LIST, that specifies a stable version of mergesort on lists, imports ``standard'' lists (from Section 7.12.1), but first it is necessary to match the parameter theory TRIV of lists with the parameter theory STRICT-WEAK-ORDER. This is accomplished by means of the predefined view STRICT-WEAK-ORDER from TRIV to STRICT-WEAK-ORDER that forgets the order and its properties (see Section 7.11.3). A renaming is also applied to this instantiation in order to have more convenient sort names. This process is illustrated in the diagram of Figure 7.3, where STRICT-WEAK-ORDER has been abbreviated to S-W-O, the sort renaming has been abbreviated to $\alpha$, and where the different types of arrows represent the different relationships between modules: importation (triple arrow), views between theories (dashed arrow named S-W-O), instantiation (dashed arrow), and renaming (dotted arrow named _*($\alpha$), meaning the renaming whose second argument is $\alpha$ and whose first argument is still unknown).

Figure 7.3: From lists to weakly sortable lists

  fmod WEAKLY-SORTABLE-LIST{X :: STRICT-WEAK-ORDER} is
    pr LIST{STRICT-WEAK-ORDER}{X} 
         * (sort NeList{STRICT-WEAK-ORDER}{X} to NeList{X},
            sort List{STRICT-WEAK-ORDER}{X} to List{X}) .
    sort $Split{X} .

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

The main operation in this module is sort, that sorts a given list.^7.5It is defined by case analysis on the list: if it is either the empty list or a singleton list, then it is already sorted; otherwise, we split the given list into two sublists, recursively sort both of them, and then merge the sorted results in order to obtain the final sorted list. This process is accomplished by means of three auxiliary operations, whose names are self-explanatory: $split (for the splitting, with an auxiliary result sort $Split), $sort (for the recursive sorting calls), and $merge (for the final merging).

    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) .

The auxiliary operation $split has three arguments: the first one is the list to be split and the other two are accumulators (initially both empty) that keep the elements as they are moved from the main list into the appropriate sublists. In this way, we have an efficient tail-recursive definition.

    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') .

The auxiliary operation $merge also has three arguments, but now the first two are the lists to be merged and the third one is the accumulator where the result is incrementally computed by means of another efficient tail-recursive definition.

The module also provides an operation merge that simply calls the previous operation with the empty accumulator. Notice that if both lists are sorted then the result of calling merge on them is a sorted list, but in general merge is a total function that can be called on any two lists whatsoever.

    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(E L, L', A E')
        else $merge(L, E' L', A E)
        fi .
  endfm

The Maude prelude also provides another predefined module for sorting lists, namely, SORTABLE-LIST, where the required order is strict and total, as specified in the predefined theory STRICT-TOTAL-ORDER of Section 7.11.3. Since the theory STRICT-TOTAL-ORDER is a strengthening of STRICT-WEAK-ORDER with the additional requirement of totality, we can use it as a parameter theory to specialize our WEAKLY-SORTABLE-LIST module to strict total orders, thus getting the SORTABLE-LIST module. For this we need a view from the theory STRICT-WEAK-ORDER into the theory STRICT-TOTAL-ORDER, which is precisely the predefined inclusion view STRICT-TOTAL-ORDER in Section 7.11.3.

Moreover, since we also use another renaming to have more convenient sort names, the construction of the parameterized module SORTABLE-LIST on top of WEAKLY-SORTABLE-LIST mirrors the process of constructing WEAKLY-SORTABLE-LIST on top of LIST, as described in Figure 7.4, where the sort renaming has been abbreviated to $\alpha'$, WEAKLY-SORTABLE-LIST to W-S-LIST, STRICT-WEAK-ORDER to S-W-O, and STRICT-TOTAL-ORDER to S-T-O. The reader should compare this figure with Figure 7.3 to appreciate the similarity between both.

Figure 7.4: From weakly sortable lists to sortable lists

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

We can use the predefined view String< from STRICT-TOTAL-ORDER to String (where < is the lexicographic order on strings) to instantiate the previous module before doing some sample reductions.

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

  Maude> red in STRING-SORTABLE-LIST :
           $split("a" "quick" "brown" "fox" "jumps" 
                  "over" "the" "lazy" "dog", nil, nil) .
  result $Split{STRICT-TOTAL-ORDER}{String<}: 
    $split(nil, 
           "a" "quick" "brown" "fox" "jumps", 
           "over" "the" "lazy" "dog")

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

  Maude> red 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"