Via:  uk.ac.nsf; 2 Jun 89 13:04 BST  (UK.AC.Cam.Cl.scaup)
Date: Fri, 2 Jun 89 4:12:36 BST
From: Tom Melham <tfm%uk.ac.cam.cl@uk.ac.nsf>
To: info-hol <info-hol%edu.ucdavis.clover@uk.ac.nsf>
Message-Id:  <8906020415.aa15942@scaup.Cl.Cam.AC.UK>
Sender: tfm <tfm%uk.ac.cam.cl%uk.ac.nsf@edu.ucdavis.clover>
Status: R

re: Steve Crocker's remarks about bit-strings
=============================================


Until I read Steve's recent info-hol message, in which he says:

+-------------------------------------
| After working with bitstrings for
| quite a while, I find I can see both sides of the issue.  I'd
| generally favor a regular theory that includes zero length bitstrings,
| but there are difficulties either way.
+-------------------------------------

I was beginning to suspect that I was the only one who thought that having the
empty bit-string can sometimes present practical problems.  Most people who
I've talked to seem to prefer the "empty option".  A theory of this already
exists in HOL, of course, in the form of the built-in type of lists. The
polished version of the bit-vector package will probably be based on (*)list,
since after talking to people I've been convinced that having the empty vector
is preferable to my original formulation. It's probably not worth the effort
and ad-hoc logical hackery necessary to offer an empty/non-empty option in the
library version.

Regarding the last point mentioned by Steve, it should be possible to prove
the theorem he mentioned fairly easily from the current HOL theory of lists.
I think what Steve suggested would provide a much more elegant theory of
bit-vectors (at least varying-length ones) than the approach outlined in my
original message. (I can't resist mentioning that the actual theorem cited by
Steve seems at first sight to be true only if the empty bit-vector is not
allowed.  Otherwise, I don't think that f would be unique.  I could, however,
be mistaken.)

The interesting thing is that the property of bit-vectors expressed by the
theorem in Steve's message is (more or less) what I'm trying to get the
planned extension to the recursive types package to derive automatically as
the characterization for an 'abstract type' described by user input of the
form:

  ty ::=   0 | 1 | APPEND v1 v2
  where APPEND (APPEND x y) z = APPEND x (APPEND y z)

This would indeed provide, as Steve said, "a theory that doesn't disclose
whether bitstrings are defined from left to right, from right to left, or some
other way."

Tom