Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Date: Wed, 15 Jan 92 17:13:11 gmt
From: Roger Fleming <raf@com.hp.hpl.hplb>
Message-Id: <9201151713.AA08331@eeyore.hpl.hp.com>
To: info-hol-request@edu.uidaho.cs.ted, info-hol@edu.uidaho.cs.ted
Subject: Re: Why sets?
Cc: chou@edu.ucla.cs

I personally stand in the predicates camp.

Reasons:

1. I think that sets add nothing to the tools available to the theorem prover
other than excess baggage.  It would have made sense to use sets if the logic
were first order, but as things stand, they just add to the things people have
to learn about.  In the case of sets the "conceptual baggage" is tolerable as
the ideas and notation are so familiar.  However theorem provers always come
with a welter of "tools baggage" as well.  We not only have to know about the
intersection operator as well as conjunction, for example, but we have to know
about the theorems, remember their names, know about various conversions and so
on.  The cost of introducing sets is therefore quite large.  (About 2 apw*.)

2. The presence of extra specification tools like this always introduce
specification decisions --- should I use sets or predicates here? --- and give
the user more scope to make a mess of his/her specifications by being irregular
in these choices.  (Projects where several members are independantly writing
different parts of the specification should be specially careful.)

3. In the course of constructing proofs involving terms containing sets, I
found myself quite frequently having to eliminate the set notation (so the use
of sets just added further steps --- occassionally quite awkward ones --- to
the proof).  The tools for dealing with the HOL logic directly are, and always
will be, much more extensive than those for handling sets, so I suspect this
phenomenon must be quite common.

4. Lastly there is a problem with the set comprehension notation.  There is no
explicit binder for the bound variables.  Hence
                  {x + y | x < y}
effectivley makes a guess at what the user intended the bound variables to be.
(x and y are bound by the set comprehension operator in this case.)  It is a
consistent notation, but a little inflexible, and invites misunderstanding.
For example
           0 < x ==> !z. z IN {x + y | x <= y} ==> 1 < z
is not valid, dispite appearances, because the x in the comprehension term is
bound within that term.  (To get the intended effect, something like
           0 < x ==> !z. z IN {u | ?y. x <= y /\ (u = x + y)} ==> 1 < z
would do, but the need to do this kind of thing subverts the intent of the
comprehension notation.)

A notation like
                  {x + y | y. x <= y}
which has explicit binders would, I think, have been clearer.

Nonetheless, the HOL set theory is useful in providing a theory of finite sets
and the cardinality operator.  In the absence of set theory, a theory of finite
predicates and a notion of cardinality for predicates is needed.

(In fact I have constructed this, but must admit to having been totally
unscrupulous.  I just used the correspondence between sets and predicates to
plagiarise the results, "lifting" them from set theory to predicate theory.  I
hesitate to lob the theory into contrib as it is now quite extensive, and makes
extensive use of some DIY tactics based on unification.  However if anyone
really wants it, I will be happy to oblige.)

Roger Fleming


* - asprins per week