helphome pageduck scriptspecificationfirst proof page

Behavioral Properties of Set

Software engineers often face tricky problems to which they find clever solutions. One such problem is how to implement sets, including their commutative and idempotent properties, which run counter to the linear, sequential organization of computer memory. A solution, going back to the days when Lisp programmers began to explore symbolic computation, is to represent sets as lists, with the empty set as nil (the empty list), with adding an element to a set as cons (left juxtaposition), and with union as append (concatenation). Then the commutative and idempotent laws are false - but if the programmer is careful, they will be behaviorally true; this depends in part on a careful choice of attributes, that is, of visible valued functions defined on sets, and of course on writing methods that respect these attributes.

Below is an applet that illustrates how sets of natural numbers may be implemented with lists: It starts with two sets, A and B, each the empty set, represented as the empty list; you can add elements to either by using the add method, and you can check whether some number is in the list with the in? attribute (note that it both requires an natural number argument and returns a Boolean value). The reset method reinitializes the selected set to the empty set. The third region of the display will show either the union or the intersection of A and B, depending on which button you push; you can also check which elements are in the result set with the in? attribute.

If you don't see applet, your browser doesn't support applet.

Membership is clearly the most important and characteristic attribute for sets, and in particular, the usual axioms for mathematical set theory define two sets to be equal iff they have the same elements, that is,

     A = B   iff   ( x) (x in A  iff  x in B) .
Notice that this is a behavioral definition, as are also the usual definitions of union and intersection,
    ( x) x in A U B   iff   x in A or  x in B .

    ( x) x in A & B   iff   x in A and x in B .
To formalize this in hidden algebra, we take the empty set to be a hidden constant, add to be a method, in? to be an attribute, and union and intersection to be methods; these last two methods are excellent motivation for our generalization of hidden algebra to allow non-monadic operations.

In this example, it suffices to use a special kind of coinduction called attribute coinduction, which is simpler to check and easier to mechanize; but in Kumo it is easier to use the very general circular coinductive rewriting algorithm that is implemented in BOBJ.

We will first show that lists implement sets behaviorally, that is, that they provide a behavioral refinement for sets, and then we will check that some familiar properties of sets (commutativity, idempotency, de Morgan, etc.) hold for our specification of sets; it is then automatic that these properties also hold for the list implementation of sets.

It is interesting to notice that our behavioral specification of sets includes not only all finite sets of natural numbers, but also all cofinite sets of natural numbers, via the complement operation, neg, which forms the difference of its argument from the "universal" set, I, which could have been defined by

     ( x) x in I  =  true .
For example, neg(add(0,empty)) is the set of all positive integers. (As an exercise, the reader might want to consider how to represent cofinite sets as what might be called "negative lists.")

It is also interesting to speculate about an axiomatic theory of behavioral sets, parallel to the usual axiomatic set theories in mathematics.

To the Kumo demos homepage.
To the Tatami Project homepage.
To the UCSD Meaning and Computation Group homepage.

       This page was generated by Kumo on Tue Feb 13 11:31:33 PST 2001.