Generalized sets

The construction of generalized or nestable sets follows exactly the same pattern as the one we have seen for generalized lists in the previous section, but now we use braces instead of square brackets to make explicit the level of nesting. In particular, there is no empty ``preset.'' Note that braces {_} and comma _,_ exactly reflect standard set theory notation.

Notice that the sort named Element plays here the same role as Item played for nestable lists; do not confuse this sort with the sort Elt coming from the parameter theory TRIV in the form X$Elt.

The module SET* provides for generalized sets the same operations we have seen in Section 7.12.2 for ``standard'' sets, and, in addition, it specifies a powerset operator that was not possible in the previous setting.

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

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

    vars P Q : PreSet{X} .
    vars A S : Set{X} .
    var  E : Element{X} .
    var  N : NeSet{X} .
    var  C : Nat .

    eq {P, P} = {P} .
    eq {P, P, Q} = {P, Q} .

The operations for insertion, deletion, and membership testing now work for items that can be either basic elements or nested sets, but always at the first level of nesting. For example, the membership predicate _in_ cannot be used to test if a basic element belongs to a set inside another set, but on the other hand can check if a set is a member of another set. In other words, the operation _in_ exactly corresponds to the set theory membership predicate $\in$. As in Section 7.12.2, the operators delete and _in_ are defined by means of the otherwise attribute. Moreover, each one has an additional equation for the singleton case, which is treated separately because there is no empty ``preset.''

    op insert : Element{X} Set{X} -> Set{X} .
    eq insert(E, {}) = {E} .
    eq insert(E, {P}) = {E, P} .

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

    op _in_ : Element{X} Set{X} -> Bool .
    eq E in {E} = true .
    eq E in {E, P} = true .
    eq E in S = false [owise] .

The cardinality operator |_| computes the number of items (either basic elements or other sets, at the first level of nesting) in a given set. It is defined with the help of an auxiliary tail-recursive operator $card on ``presets.''

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

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

The union operator union on generalized sets is based on the ``union'' operator _,_ on the ``presets'' inside the generalized sets.

    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 .
    eq union(S, {}) = S .
    eq union({P}, {Q}) = {P, Q} .

The intersection and set difference operations for generalized sets have a specification very similar to the one seen in Section 7.12.2, including the use of tail-recursive auxiliary operations on ``presets''.

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

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

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

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

The powerset 2^ X of a set X is computed by case analysis on the set X: it is either the empty set {} or a singleton set {E}, or it has two or more items {E, P}. In the last case we compute the total powerset 2^ X by computing first the powerset 2^{P} of the set without item E and then the union of this powerset 2^{P} with the result of inserting the distinguished item E into all the items in the same powerset 2^{P}. The last process is done by means of an auxiliary operation $augment.

    op 2^_ : Set{X} -> Set{X} .
    eq 2^{} = {{}} .
    eq 2^{E} = {{}, {E}} .
    eq 2^{E, P} = union(2^{P}, $augment(2^{P}, E, {})) .

    op $augment : NeSet{X} Element{X} Set{X} -> Set{X} .
    eq $augment({S}, E, A) = insert(insert(E, S), A) .
    eq $augment({S, P}, E, A) 
      = $augment({P}, E, $augment({S}, E, A)) .

The specification of the subset predicates that check whether a set is included in another is completely analogous to the specification of the corresponding operations in Section 7.12.2.

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

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

We consider the following instantiation and sample reductions:

  fmod QID-SET* is
    pr SET*{Qid} .
  endfm

  Maude> red in QID-SET* : {'a} in {{'a}, {'b}, {'a, 'b}} .
  result Bool: true

  Maude> red | {{'a}, {'b}, {'a, 'b}} | .
  result NzNat: 3

  Maude> red union({{'a}, {'b}}, {{'a, 'b}}) .
  result NeSet{Qid}: {{'a}, {'b}, {'a, 'b}}

  Maude> red intersection({{'a}, {'b}}, {{'a, 'b}}) .
  result Set{Qid}: {}

  Maude> red 2^ {'a, 'b, 'c, 'd} .
  result NeSet{Qid}: 
    {{}, {'a}, {'b}, {'c}, {'d}, {'a, 'b}, {'a, 'c}, {'a, 'd},
     {'b, 'c}, {'b, 'd}, {'c, 'd}, {'a, 'b, 'c}, {'a, 'b, 'd},
     {'a, 'c, 'd}, {'b, 'c, 'd}, {'a, 'b, 'c, 'd}}