|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
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
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,
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,
( x) x in I = true .For example,
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
To the Tatami Project homepage.
To the UCSD Meaning and Computation Group homepage.