Sets Are Behavioral

Sets Are Behavioral

This page tries to introduce basic behavioral features of BOBJ through a rather personal commentary on a very basic example, so please forgive its informal tone.

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.


1. Behavioral Specification of Set Theory

The first theory below is the basic behavioral theory of sets; we use it to define some basic operations on sets in the second theory. BOBJ's default cobasis for this second module is too large, so we select the cobasis of the first module instead, for the proofs that follow. In each case, we run both 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. *** file: /groups/tatami/bobj/examples/set.bob ***> behavioral set theory *** basic set theory bth SET is sort Set. pr NAT . op empty : -> Set . op _in_ : Nat Set -> Bool . var N : Nat . eq N in empty = false . end *** the usual operations bth SETH is pr SET . op ins : Nat Set -> Set . op _U_ : Set Set -> Set . op _&_ : Set Set -> Set . vars M N : Nat . vars S S' S'' : Set . eq M in ins(N,S) = eq(M,N) or M in S . eq M in S U S' = M in S or M in S' . eq M in S & S' = M in S and M in S' . end *** some proofs set cobasis of SET . red ins(N, ins(N, S)) == ins(N, S) . cred ins(N, ins(N, S)) == ins(N, S) . red ins(N, ins(M, S)) == ins(M, ins(N, S)). cred ins(N, ins(M, S)) == ins(M, ins(N, S)). red S U S == S . cred S U S == S . red S U empty == S . cred S U empty == S . red S U S' == S' U S . cred S U S' == S' U S . red S U (S' U S'') == (S U S') U S'' . cred S U (S' U S'') == (S U S') U S'' . red S & empty == empty . cred S & empty == empty . red S & S' == S' & S . cred S & S' == S' & S . red S & (S' U S'') == (S & S') U (S & S''). cred S & (S' U S'') == (S & S') U (S & S'').

2. Output for Set Theory

awk% bobj \|||||||||||||||||/ --- Welcome to BOBJ --- /|||||||||||||||||\ BOBJ version 0.9.210 built: Fri Nov 22 14:09:23 PST 2002 University of California, San Diego Sun Nov 24 10:38:25 PST 2002 BOBJ> in set ========================================== ***> behavioral set theory ========================================== bth SET ========================================== bth SETH ========================================== set cobasis of SET ========================================== reduce in SETH : ins(N, ins(N, S)) == ins(N, S) result Bool: false rewrite time: 138ms parse time: 5ms ========================================== c-reduce in SETH : ins(N, ins(N, S)) == ins(N, S) using cobasis of SETH: op _ in _ : Nat Set -> Bool [prec 41] --------------------------------------- result: true c-rewrite time: 136ms parse time: 6ms ========================================== reduce in SETH : ins(N, ins(M, S)) == ins(M, ins(N, S)) result Bool: false rewrite time: 2ms parse time: 6ms ========================================== c-reduce in SETH : ins(N, ins(M, S)) == ins(M, ins(N, S)) using cobasis of SETH: op _ in _ : Nat Set -> Bool [prec 41] --------------------------------------- result: true c-rewrite time: 62ms parse time: 9ms ========================================== reduce in SETH : S U S == S result Bool: false rewrite time: 5ms parse time: 2ms ========================================== c-reduce in SETH : S U S == S using cobasis of SETH: op _ in _ : Nat Set -> Bool [prec 41] --------------------------------------- result: true c-rewrite time: 10ms parse time: 2ms ========================================== reduce in SETH : S U empty == S result Bool: false rewrite time: 1ms parse time: 2ms ========================================== c-reduce in SETH : S U empty == S using cobasis of SETH: op _ in _ : Nat Set -> Bool [prec 41] --------------------------------------- result: true c-rewrite time: 7ms parse time: 2ms ========================================== reduce in SETH : S U S' == S' U S result Bool: false rewrite time: 1ms parse time: 4ms ========================================== c-reduce in SETH : S U S' == S' U S using cobasis of SETH: op _ in _ : Nat Set -> Bool [prec 41] --------------------------------------- result: true c-rewrite time: 18ms parse time: 3ms ========================================== reduce in SETH : S U (S' U S'') == (S U S') U S'' result Bool: false rewrite time: 1ms parse time: 6ms ========================================== c-reduce in SETH : S U (S' U S'') == (S U S') U S'' using cobasis of SETH: op _ in _ : Nat Set -> Bool [prec 41] --------------------------------------- result: true c-rewrite time: 31ms parse time: 6ms ========================================== reduce in SETH : S & empty == empty result Bool: false rewrite time: 0ms parse time: 2ms ========================================== c-reduce in SETH : S & empty == empty using cobasis of SETH: op _ in _ : Nat Set -> Bool [prec 41] --------------------------------------- result: true c-rewrite time: 4ms parse time: 2ms ========================================== reduce in SETH : S & S' == S' & S result Bool: false rewrite time: 1ms parse time: 3ms ========================================== c-reduce in SETH : S & S' == S' & S using cobasis of SETH: op _ in _ : Nat Set -> Bool [prec 41] --------------------------------------- result: true c-rewrite time: 18ms parse time: 3ms ========================================== reduce in SETH : S & (S' U S'') == (S & S') U (S & S'') result Bool: false rewrite time: 1ms parse time: 7ms ========================================== c-reduce in SETH : S & (S' U S'') == (S & S') U (S & S'') using cobasis of SETH: op _ in _ : Nat Set -> Bool [prec 41] --------------------------------------- result: true c-rewrite time: 52ms parse time: 7ms BOBJ> q Bye. awk%

3. List Implementation of Set

You might worry that we propose to implement potentially infinite sets with just finite lists, which obviously cannot be done. But what a refinement proof does, is show that the target (or "finer") theory (behaviorally) satisfies the axioms of the source (original) theory, which only means that all models of the target theory are also models of the source theory - but not conversely. So it is ok that the source theory (of sets) has infinite models whereas the target theory (of lists) does not. Our theory of lists is an initial theory, rather than a behavioral theory, so our proofs show that the set equations hold strictly in all initial models of the theory, which of course implies that they also hold behaviorally in these models.

For the first two equations,

eq N in empty = false . eq M in ins(N,S) = eq(M,N) or M in S . there is actually nothing to show, because their translations into the syntax of lists are already in the specification. eq N in nil = false . eq M in cons(N,L) = eq(M,N) or M in L . However, it is interesting to notice that the interpretations of these equations are completely different in the two specifications. The first set equation is actually a behavioral definition of 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.

*** file: /groups/tatami/bobj/examples/list.bob ***> lists satisfy the set axioms *** basic set theory bth SET is sort Set. pr NAT . op empty : -> Set . op _in_ : Nat Set -> Bool . var N : Nat . eq N in empty = false . end *** the usual operations bth SETH is pr SET . op ins : Nat Set -> Set . op _U_ : Set Set -> Set . op _&_ : Set Set -> Set . vars M N : Nat . vars S S' S'' : Set . eq M in ins(N,S) = eq(M,N) or M in S . eq M in S U S' = M in S or M in S' . eq M in S & S' = M in S and M in S' . end ***> data type of lists dth LIST is sort List . pr NAT . op nil : -> List . op cons : Nat List -> List . op car_ : List -> Nat . op cdr_ : List -> List . vars M N : Nat . vars L L' : List . eq car cons(N, L) = N . eq cdr cons(N, L) = L . op _in_ : Nat List -> Bool . eq N in nil = false . eq M in cons(N,L) = eq(M,N) or M in L . end dth APD is pr LIST . vars-of LIST . op apd : List List -> List . eq apd(nil, L) = L . eq apd(cons(N,L'), L) = cons(N, apd(L',L)). end dth PROOF is pr APD . ops m n : -> Nat . ops l l' : -> List . let eqn = m in apd(l,l') == (m in l or m in l') . end open . ***> base case eq l = nil . red eqn . close open . ***> induction step vars-of LIST . op l0 : -> List . eq l = cons(n,l0) . eq m in apd(l0,l') = m in l0 or m in l' . red eqn . close

4. Output for List Implementation of Set

awk% bobj \|||||||||||||||||/ --- Welcome to BOBJ --- /|||||||||||||||||\ BOBJ version 0.9.210 built: Fri Nov 22 14:09:23 PST 2002 University of California, San Diego Sun Nov 24 10:38:02 PST 2002 BOBJ> in list ========================================== ***> lists satisfy the set axioms ========================================== bth SET ========================================== bth SETH ========================================== ***> data type of lists ========================================== dth LIST ========================================== dth APD ========================================== dth PROOF ========================================== open ========================================== ***> base case ========================================== eq l = nil ========================================== reduce in PROOF : eqn result Bool: true rewrite time: 162ms parse time: 0ms ========================================== close ========================================== open ========================================== ***> induction step ========================================== vars-of LIST ========================================== op l0 : -> List ========================================== eq l = cons(n, l0) ========================================== eq m in apd(l0, l') = (m in l0) or (m in l') ========================================== reduce in PROOF : eqn result Bool: true rewrite time: 51ms parse time: 2ms ========================================== close BOBJ> q Bye. awk%

5. Some Infinite Sets

Here we briefly show how to define and manipulate some infinite sets using the behavioral specification of Section 1. We first give a specification of the natural numbers, because we need the Peano numbers, not BOBJ's builtin version. *** file: /groups/tatami/bobj/examples/iset.bob ***> some infinite sets dth NAT is sort Nat . op 0 : -> Nat . op s_ : Nat -> Nat . op eq : Nat Nat -> Bool [comm] . vars N M : Nat . eq eq(N,N) = true . eq eq(0, s N) = false . end *** basic set theory bth SET is sort Set. pr NAT . op empty : -> Set . op _in_ : Nat Set -> Bool . var N : Nat . eq N in empty = false . end *** the usual operations bth SETH is pr SET . op ins : Nat Set -> Set . op _U_ : Set Set -> Set . op _&_ : Set Set -> Set . vars M N : Nat . vars S S' S'' : Set . eq M in ins(N,S) = eq(M,N) or M in S . eq M in S U S' = M in S or M in S' . eq M in S & S' = M in S and M in S' . end bth INFS is pr SETH . ops nats evens odds : -> Set . var N : Nat . eq N in nats = true . eq 0 in evens = true . eq s 0 in evens = false . eq s s N in evens = N in evens . eq N in odds = not N in evens . end open . op S : -> Set . cred nats & S == S . cred evens & odds == empty . cred evens U odds == nats . close Here is the BOBJ output from the above input. The desired equations are again proved using coinduction and builtin Boolean equations. awk% bobj \|||||||||||||||||/ --- Welcome to BOBJ --- /|||||||||||||||||\ BOBJ version 0.9.210 built: Fri Nov 22 14:09:23 PST 2002 University of California, San Diego Sun Nov 24 13:34:42 PST 2002 BOBJ> in iset ========================================== ***> some infinite sets ========================================== dth NAT ========================================== bth SET ========================================== bth SETH ========================================== bth INFS ========================================== open ========================================== op S : -> Set ========================================== c-reduce in INFS : nats & S == S using cobasis for INFS: op _ in _ : Nat Set -> Bool [prec 41] --------------------------------------- result: true c-rewrite time: 61ms parse time: 2ms ========================================== c-reduce in INFS : evens & odds == empty result: true c-rewrite time: 26ms parse time: 2ms ========================================== c-reduce in INFS : evens U odds == nats result: true c-rewrite time: 20ms parse time: 2ms ========================================== close BOBJ> q Bye. awk%
To the BOBJ Examples homepage
To Tatami project homepage
Maintained by Joseph Goguen
Last modified: Sun Nov 24 14:44:55 PST 2002