Implementing Sets with Lists

Implementing Sets with Lists

Software engineers often face difficult problems for which they give 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 sets: 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. The reset method returns the set to being 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 what 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, to the extent that in mathematical axioms for set theory, two sets are defined to be equal iff they have the same elements, that is,

     A = B   iff   ( x) (x in A  iff  x in B) .

Continuing this unorthodox behavioral tour of set theory, it is highly suggestive to notice that the usual definitions of union and intersection are also behavioral,

    ( 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, and in to be an attribute. There appears to be a problem with union and intersection, because these are not monadic, as required by the conventional framework of hidden algebra. But the framework is easily extended to handle this situation, provided the non-monadic operations are not considered constructors, and provided they satisfy a property called coherence with respect to the basic theory of sets. Moreover, coinduction can still be used to prove behavioral properties of such operations.

For this example, a special kind of coherence called attribute coherence and coinduction called attribute coinduction, can be used; this special case is simpler to check and moreover is also easier to mechanize. The first thing to show is that lists implement, that is, provide a behavioral refinement of, behaviorally defined sets. After that, we can check that the usual properties hold for these behavioral sets, including of course commutativity and idempotence. Then it is automatic that all these properties also hold for the list implementation of sets.

It is interesting to notice that the behavioral sets of natural numbers obtained from the specification of this example include all the countable sets of natural numbers; this is in contrast to what happens with the perhaps more familiar initial algebra approach, which gives only the finite sets. Finally, it is interesting to speculate about whether there might be an axiomatic theory of behavioral sets, parallel to the usual axiomatic set theories in mathematics.

This websites has 12 goals:

First proof page for goal 1 .
First proof page for goal 2 .
First proof page for goals 3 to 6 .
First proof page for goals 7 to 9 .
First proof page for goals 10 to 12 .

Here is the duck code that generated this website.

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

The prose on this page was written by Joseph Goguen, the applet was written by Kai Lin and Almira Karabeg, and the proof was generated from code written by Grigore Rosu, using the Kumo system, on Mon Jun 15 13:46:51 PDT 1998. Kumo is implemented by Kai Lin.