Sets

Sets over a given sort of elements (provided by the theory TRIV) are built from the constant empty and singleton sets (identified with the corresponding elements by means of a subsort declaration) with an associative, commutative, and idempotent union operator written _,_. The first two such properties are declared as attributes, while the third is written as an equation; remember that the attributes idem and assoc cannot be used together (see Section 4.4.1).

  fmod SET{X :: TRIV} is
    protecting EXT-BOOL .
    protecting NAT .
    sorts NeSet{X} Set{X} .
    subsort X$Elt < NeSet{X} < Set{X} .

    op empty : -> Set{X} [ctor] .
    op _,_ : Set{X} Set{X} -> Set{X}
        [ctor assoc comm id: empty prec 121 format (d r os d)] .
    op _,_ : NeSet{X} Set{X} -> NeSet{X} [ctor ditto] .

    var  E : X$Elt .
    var  N : NeSet{X} .
    vars A S S' : Set{X} .
    var  C : Nat .

    eq N, N = N .

The prefix operator union is just another name for the infix operator _,_. Moreover, given the identification between elements and singleton sets, inserting an element is a particular case of union.

    op union : Set{X} Set{X} -> Set{X} .
    op union : NeSet{X} Set{X} -> NeSet{X} .
    op union : Set{X} NeSet{X} -> NeSet{X} .
    eq union(S, S') = S, S' .

    op insert : X$Elt Set{X} -> Set{X} .
    eq insert(E, S) = E, S .

The definitions of the operators delete, that deletes an element from a set, and _in_, that checks if an element belongs to a set, are based on the statement attribute otherwise (see Section 4.5.4):

1. When a given term representing a set matches the pattern (E, S) (modulo the equational attributes of the _,_ operator), then we can delete the element E (and continue deleting, since there may be repetitions of such element in the given term), and state that indeed the element E belongs to the set.
2. Otherwise, the element E does not belong to the set and deleting such element does not change the set.

    op delete : X$Elt Set{X} -> Set{X} .
    eq delete(E, (E, S)) = delete(E, S) .
    eq delete(E, S) = S [owise] .

    op _in_ : X$Elt Set{X} -> Bool .
    eq E in (E, S) = true .
    eq E in S = false [owise] .

The operator |_| computes the cardinality of a set. Its definition goes through an auxiliary operator $card with an additional accumulator argument that allows a tail-recursive definition. In turn, the specification of $card is based on an equation that eliminates repetitions of elements in a term representing a set; when such equation can no longer be applied (hence the owise attribute in the last equation), the accumulator argument does its job by counting once each different element.

    op |_| : Set{X} -> Nat .
    op |_| : NeSet{X} -> NzNat .
    eq | S | = $card(S, 0) .

    op $card : Set{X} Nat -> Nat .
    eq $card(empty, C) = C .
    eq $card((N, N, S), C) = $card((N, S), C) .
    eq $card((E, S), C) = $card(S, C + 1) [owise] .

Both the intersection and set difference operations also use an auxiliary operation with a tail-recursive efficient definition. The accumulator argument keeps the elements that belong to both sets (for intersection) or to the first but not to the second set (for difference).

    op intersection : Set{X} Set{X} -> Set{X} .
    eq intersection(S, empty) = empty .
    eq intersection(S, N) = $intersect(S, N, empty) .

    op $intersect : Set{X} Set{X} Set{X} -> Set{X} .
    eq $intersect(empty, S', A) = A .
    eq $intersect((E, S), S', A) 
      = $intersect(S, S', if E in S' then E, A else A fi) .

    op _\_ : Set{X} Set{X} -> Set{X} [gather (E e)].
    eq S \ empty = S .
    eq S \ N = $diff(S, N, empty) .

    op $diff : Set{X} Set{X} Set{X} -> Set{X} .
    eq $diff(empty, S', A) = A .
    eq $diff((E, S), S', A) 
      = $diff(S, S', if E in S' then A else E, A fi) .

The following two predicates check whether their first argument is a (proper) subset of the second argument. The second one is defined in terms of the first, and in both cases the corresponding equations use the short-circuit version _and-then_ of conjunction imported from the EXT-BOOL module.

    op _subset_ : Set{X} Set{X} -> Bool .
    eq empty subset S' = true .
    eq (E, S) subset S' = E in S' and-then S subset S' .

    op _psubset_ : Set{X} Set{X} -> Bool .
    eq S psubset S' = S =/= S' and-then S subset S' .
  endfm

The Maude metalevel (see Chapter 11) imports a set instantiation on the built-in data type of quoted identifiers.

  fmod QID-SET is
    protecting SET{Qid} * (sort NeSet{Qid} to NeQidSet, 
                           sort Set{Qid} to QidSet) .
  endfm

Another example of instantiation with some reductions is the following:

  fmod INT-SET is
    pr SET{Int} .
  endfm

  Maude> red in INT-SET : | -1, 2, -3, 3, 2, -1 | .
  result NzNat: 4

  Maude> red 4 in (-1, 2, -3, 3, 2, -1) .
  result Bool: false

  Maude> red insert(4, (-1, 2, -3, 3, 2, -1)) .
  result NeSet{Int}: 2, 3, 4, -1, -3

  Maude> red union((2, 3, 4, -1, -3, 0), (-1, 2, -3, 3, 2, -1)) .
  result NeSet{Int}: 0, 2, 3, 4, -1, -3

  Maude> red intersection((2, 3, 4, -1, -3, 0), 
                          (-1, 2, -3, 3, 2, -1)) .
  result NeSet{Int}: 2, 3, -1, -3

  Maude> red (2, 3, 4, -1, -3, 0) \ (-1, 2, -3, 3, 2, -1) .
  result NeSet{Int}: 0, 4