Lists

There are different ways of building lists. One possibility is to begin with the empty list and the singleton lists, and then use the concatenation operation to get bigger lists. However, concatenation cannot be a free list constructor, because it satisfies an associativity equation and has the empty list as identity. This approach will be used in the predefined module for generic lists described in Section 7.12.1, and appears in many similar examples throughout this book. Given the support for equational attributes (associativity, commutativity, etc.) in Maude, as explained in Section 4.4.1, one can argue that this is indeed the most natural specification for lists in Maude.

Here we use instead the two standard free constructors for lists that can be found in many functional programming languages: the empty list nil, here denoted [], and the cons operation that adds an element to the beginning of a list, here denoted with the mixfix syntax _:_. This approach facilitates proving properties of lists by structural induction in Maude's inductive theorem prover (ITP), and provides a simple basis for specifying sorted lists and sorting operations on them in Section 6.3.6.

As usual, head and tail are the selectors associated with the _:_ constructor. Since they are not defined on the empty list, we avoid their partiality in the same way as we have done for stacks and queues in the previous sections by means of a subsort NeList of non-empty lists.

  fmod LIST-CONS{X :: TRIV} is
    protecting NAT .

    sorts NeList{X} List{X} .
    subsort NeList{X} < List{X} .

    op [] : -> List{X} [ctor] .
    op _:_ : X$Elt List{X} -> NeList{X} [ctor] .
    op tail : NeList{X} -> List{X} .
    op head : NeList{X} -> X$Elt .
    
    var E : X$Elt .
    var N : Nat .
    vars L L' : List{X} .

    eq tail(E : L) = L .
    eq head(E : L) = E .

Three interesting operations on lists are list concatenation (here denoted with mixfix syntax _++_), the length of a list, and reversing a list. The length operator has a result of sort Nat, that comes from the predefined module NAT, imported in protecting mode. These three operations are defined as usual by structural induction on the two constructors, with an equation for the empty base case and another for the cons case E : L.

Here we are not concerned with efficiency and therefore we just specify the operations in a simple way, without using, for example, tail-recursive auxiliary operations in the style of Section 7.12.1.

    op _++_ : List{X} List{X} -> List{X} .
    op length : List{X} -> Nat .
    op reverse : List{X} -> List{X} .
    
    eq [] ++ L = L .
    eq (E : L) ++ L' = E : (L ++ L') .
    eq length([]) = 0 .
    eq length(E : L) = 1 + length(L) .
    eq reverse([]) = [] .
    eq reverse(E : L) = reverse(L) ++ (E : []) .

In this specification of generic lists we also add two operations that will be useful later, in Section 6.3.6, when sorting lists: take_from_ and throw_from_. The first one builds a list by taking the first $n$ elements of the given list, while the second one deletes the first $n$ elements of the given list. Both of them are defined by structural induction on both arguments, the base case being when either the first is 0 or the second is empty. As usual, s_ denotes the successor operator on natural numbers.

    op take_from_ : Nat List{X} -> List{X} .
    op throw_from_ : Nat List{X} -> List{X} .
    
    eq take 0 from L = [] .
    eq take N from [] = [] .
    eq take s(N) from (E : L) = E : take N from L .
    
    eq throw 0 from L = L .
    eq throw N from [] = [] .
    eq throw s(N) from (E : L) = throw N from L .
  endfm

The following sample reduction shows the result of reversing a list of character strings.

  fmod LIST-CONS-TEST is
    protecting LIST-CONS{String} .
  endfm

  Maude> red reverse("one" : "two" : "three" : []) .
  result NeList{String}: "three" : "two" : "one" : []