Making lists out of sets

In Section 7.12.3 we have seen an operation makeSet that transforms a list into a set with the same elements. On the other hand, transforming a set into a list imposes some order on the given elements, which can be done in many different ways, and therefore only makes sense as a function when we have additional information over those elements that allows us to choose a unique sequence. The solution adopted here is to require either a strict or a non-strict total order on the elements, so that the resulting list is the corresponding sorted list. For this we use the sort operation defined either in the SORTABLE-LIST module or in the SORTABLE-LIST' module described in the previous section. In both versions the main operation makeList is defined in terms of an auxiliary operation $makeList with an accumulator in order to have a more efficient definition.

In both versions the LIST-AND-SET module is imported with a double renaming (different in each case), which is needed for correct sharing of a renamed copy of the LIST module, because Core Maude does not evaluate the composition of renamings but applies them sequentially. If we computed manually and used this simpler renaming, we would get a different renaming of LIST imported by each protecting declaration; then, while these renamings would have the same effect, we would import two renamed copies of LIST rather than a shared copy.

This is the first version, using a strict total order.

  fmod SORTABLE-LIST-AND-SET{X :: STRICT-TOTAL-ORDER} is
    pr SORTABLE-LIST{X} .
    pr LIST-AND-SET{STRICT-WEAK-ORDER}{STRICT-TOTAL-ORDER}{X} 
         * (sort NeList{STRICT-WEAK-ORDER}{STRICT-TOTAL-ORDER}{X} 
              to NeList{STRICT-TOTAL-ORDER}{X},
            sort List{STRICT-WEAK-ORDER}{STRICT-TOTAL-ORDER}{X} 
              to List{STRICT-TOTAL-ORDER}{X}) 
         * (sort NeList{STRICT-TOTAL-ORDER}{X} to NeList{X},
            sort List{STRICT-TOTAL-ORDER}{X} to List{X},
            sort NeSet{STRICT-WEAK-ORDER}{STRICT-TOTAL-ORDER}{X} 
              to NeSet{X},
            sort Set{STRICT-WEAK-ORDER}{STRICT-TOTAL-ORDER}{X} 
              to Set{X}) .
  
    var E : X$Elt .
    var L : List{X} .
    var S : Set{X} .

    op makeList : Set{X} -> List{X} .
    op makeList : NeSet{X} -> NeList{X} .
    eq makeList(S) = $makeList(S, nil) .

    op $makeList : Set{X} List{X} -> List{X} .
    op $makeList : NeSet{X} List{X} -> NeList{X} .
    op $makeList : Set{X} NeList{X} -> NeList{X} .
    eq $makeList((E, E, S), L) = $makeList((E, S), L) .
    eq $makeList((E, S), L) = $makeList(S, E L) [owise] .
  endfm

Notice that makeList is only a partial inverse to makeSet, not only because of sorting the elements, but also because in a set repetitions do not matter. In general, for a set S and a list L we have $\texttt{makeSet(makeList(S))} = \texttt{S}$, but in general $\texttt{makeList(makeSet(L))} \neq \texttt{L}$.

We consider an instantiation with the predefined view Int< and some sample reductions.

  fmod INT-SORTABLE-LIST-AND-SET is
    pr SORTABLE-LIST-AND-SET{Int<} .
  endfm

Notice that in the following first reduction we get a list different from the original one, while in the second reduction we get a different representation (where repetitions have been eliminated) of the same set. Those possible repetitions are already eliminated before producing the corresponding list, as shown in the third reduction.

  Maude> red in INT-SORTABLE-LIST-AND-SET : 
           makeList(makeSet(1 -1 1 -2 1 0)) .
  result NeList{Int<}: -2 -1 0 1

  Maude> red makeSet(makeList((5, 4, 3, 4, 5))) .
  result NeSet{Int<}: 3, 4, 5

  Maude> red makeList((5, 4, 3, 4, 5)) .
  result NeList{Int<}: 3 4 5

This is the second version, using a non-strict total order.

  fmod SORTABLE-LIST-AND-SET'{X :: TOTAL-ORDER} is
    pr SORTABLE-LIST'{X} .
    pr LIST-AND-SET{TOTAL-PREORDER}{TOTAL-ORDER}{X} 
         * (sort NeList{TOTAL-PREORDER}{TOTAL-ORDER}{X} 
              to NeList{TOTAL-ORDER}{X},
            sort List{TOTAL-PREORDER}{TOTAL-ORDER}{X} 
              to List{TOTAL-ORDER}{X}) 
         * (sort NeList{TOTAL-ORDER}{X} to NeList{X},
            sort List{TOTAL-ORDER}{X} to List{X},
            sort NeSet{TOTAL-PREORDER}{TOTAL-ORDER}{X} to NeSet{X},
            sort Set{TOTAL-PREORDER}{TOTAL-ORDER}{X} to Set{X}) .
  
    var E : X$Elt .
    var L : List{X} .
    var S : Set{X} .

    op makeList : Set{X} -> List{X} .
    op makeList : NeSet{X} -> NeList{X} .
    eq makeList(S) = $makeList(S, nil) .

    op $makeList : Set{X} List{X} -> List{X} .
    op $makeList : NeSet{X} List{X} -> NeList{X} .
    op $makeList : Set{X} NeList{X} -> NeList{X} .
    eq $makeList(empty, L) = sort(L) .
    eq $makeList((E, E, S), L) = $makeList((E, S), L) .
    eq $makeList((E, S), L) = $makeList(S, E L) [owise] .
  endfm

We redo the same instantiation, now with the non-strict total order on integers.

  fmod INT-SORTABLE-LIST-AND-SET' is
    pr SORTABLE-LIST-AND-SET'{Int<=} .
  endfm

  Maude> red in INT-SORTABLE-LIST-AND-SET' : 
           makeList(makeSet(1 -1 1 -2 1 0)) .
  result NeList{Int<=}: -2 -1 0 1

  Maude> red makeSet(makeList((5, 4, 3, 4, 5))) .
  result NeSet{Int<=}: 3, 4, 5

  Maude> red makeList((5, 4, 3, 4, 5)) .
  result NeList{Int<=}: 3 4 5