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

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.

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

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.