When I was first learning set theory, I remember thinking it seemed a odd that equality, and all the set operations, are defined indirectly via the membership relation. This is quite different from how the various kinds of number are defined, via explicit constructions. It is also quite different from the explicit constructions of lists, and most other data structures used in mathematics and computer science.

I had a similar feeling of oddness while learning `LISP`

, when I
came across the implementation of sets by lists. It seemed intuitively right,
and of course it always gave the right answers, but there was no explanation
for why it worked, much less a proof of correctness.

I wonder if others have shared these feelings of oddness? It was only
after developing hidden algebra that I was able to understand these little
mysteries. The key for me was to see that *sets are behavioral*, i.e.,
they have behavioral semantics, not initial semantics, not loose semantics.
The "observer" for sets is the single Boolean-valued attribute
`in`

, testing whether or not an element is in a set; then two sets
`S, S'`

are **behaviorally** (or **observationally**)
**equivalent** if and only if `e in S`

iff `e in S'`

for all elements `e`

. Perhaps the fact that the insides of sets
are *hidden* helps to explain why millions of school children (and many
of their teachers) have trouble with sets. Hidden sorts and behavioral
equality are not immediately intuitive concepts.

Section 1 below gives a behavioral specification for sets of natural numbers, taking the approach sketched above. The specification is followed by a number of test cases, including several proofs. The output from having BOBJ execute them is given in Section 2. It should not be thought that only finite sets can be defined this way; indeed, some infinite sets are defined in Section 5, and some simple properties are proved.

Section 3 proves that lists do indeed behaviorally implement sets; this is
a behavioral refinement proof. Section 4 gives the BOBJ output from executing
this proof, vindicating McCarthy et al in the original **LISP 1.5
Programmer's Manual**.

Functions can also be defined behaviorally, by an observer that gives the value of an element of the domain of definition of the function. Similarly, pairs may be defined by two observers, which extract the first and second components, respectively. Thus there are many examples of behavioral, or hidden, constructions even in pure mathematics.

`red`

and `cred`

, the first of which always fails, while
the second always succeeds, showing that these are behavioral properties,
rather than purely equational properties. Note that equations in BOBJ's
builtin theory of booleans are much used in doing the proofs. The properties
proved are all very basic, the idempotent and commutative laws for the
operation that inserts an element into a set, and idempotent, identity,
commutative, associative and distributive laws for union and intersection.
For the first two equations,

`empty`

,
whereas its translation for lists is part of the inductive definition of the
membership function. Similarly, the second set equation is a behavioral
definition for the insert operation, whereas its translation for lists is the
second case of the inductive definition of membership.
After that, we define the append operation on lists (denoted
`apd`

), and show that it correctly implements the union operation
on sets, by proving that the translation of the defining equation for set
union holds for lists; this is a proof by induction.

To the BOBJ Examples homepage

To Tatami project homepage

Maintained by Joseph Goguen

Last modified: Sun Nov 24 14:44:55 PST 2002