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