COMP 410 Assignment

UNC-CH COMP 410

Modify SET axioms

In class we developed these axioms for SET of ELT

SET of ELT

operations:
 
   new:            --> SET
   ins:  SET x ELT --> SET
   rem:  SET x ELT --> SET
   in:   SET x ELT --> boolean
   size: SET       --> nat


we let new and ins be the canonical operations

Axioms:

in ( new, a )      = false 
in ( ins(S,a), b ) = if (a=b) then true 
                              else in(S,b)

size ( new )      = 0
size ( ins(S,a) ) = if (in(S,a)) then size(S)
                                 else size(S)+1

rem ( new, i )      = new
rem ( ins(S,a), b ) = if (a!=b) then ins ( rem(S,b), a )
                                else if (in(S,a)) then rem(S,b)
                                                  else S

Create axioms for MSET of ELT

Create axioms for a different kind of set that we will call an MSET of ELT. An MSET can contain more than one of any ELT value. Data type MSET will have the same operations as SET, and will also have one more:

  count:  SET x ELT  --> nat

The count operation tells how many times an element appears in an MSET.

For example, if we start with this MSET:

  S is { 1, 4, 9 } 
  count(S,4) is 1  and in(S,4) is true  and size(S) is 3
  count(S,9) is 1  and in(S,9) is true
  count(S,8) is 0  and in(S,8) is false

and we do an ins(S,4) on it, we get this MSET:

  S is { 1, 4, 4, 9 } 
  count(S,4) is 2  and in(S,4) is true  and size(S) is 4
  count(S,9) is 1  and in(S,9) is true
  count(S,8) is 0  and in(S,8) is false

Now do a rem(S,9):

  S is { 1, 4, 4 } 
  count(S,4) is 2  and in(S,4) is true  and size(S) is 3
  count(S,9) is 0  and in(S,9) is false

Now do a rem(S,4):

  S is { 1, 4 } 
  count(S,4) is 1  and in(S,4) is true  and size(S) is 2
  count(S,9) is 0  and in(S,9) is false

Now do another rem(S,9):

  S is { 1, 4 } 
  count(S,4) is 1  and in(S,4) is true  and size(S) is 2
  count(S,9) is 0  and in(S,9) is false

So rem takes out one instance of an element, if there is one or more instances there. If there are none, the MSET contents do not change.

You should start with the axioms above for SET and alter the ones that need changing to reflect the new behavior. Also, you need to add two new axioms for the new count operation.

Bonus 5 pts

The operation size, as I defined it above, tells how many elements are in the set counting multiples. Add one more function "card" and create the 2 new axioms to define it:

  card:  SET --> nat

The card operation tells how many unique elements are in the set. For example:

  
S is { }                   then card(S) is 0
S is { 4 }                 then card(S) is 1
S is { 4, 4 }              then card(S) is 1
S is { 1, 4, 9 }           then card(S) is 3
S is { 1, 4, 4, 9 }        then card(S) is 3
S is { 1, 4, 4, 9, 9 }     then card(S) is 3
S is { 1, 4, 4, 8, 9, 9 }  then card(S) is 4