Re: [isabelle] bit vs. bool in HOL-Word



I'll try to give you my understanding of the situation.

As users, we mostly use these n-bit machine word representations:
  - as lists of booleans of length n (to_bl/of_bl)
  - as functions from a domain of cardinality n to bool (test_bit)
  - as naturals modulo 2^n (unat/of_nat)
  - as nonnegative integers modulo 2 ^ n (uint/word_of_int)
  - as a integers - 2 ^ (n - 1) <= x < 2 ^ (n - 1) (sint/word_of_int)

The word type could also have been defined as any of these representations, and the strength of the library is that the user doesn't need to care much what the underlying type definition is.

I think that HOL-Word has a lot of history in it. It was created around the time of an earlier change in the numeral representation, which annoyed its author somewhat and resulted in some compatibility layers. As a user, seeing these layers, types and definitions is a strong indication that you've dug too deep. The same goes for the "_ BIT _" representation. I suspect that these representations only get used in user proofs in evaluating concrete n-bit arithmetic (that is, the simpset introduces them then removes them again).

So, in short, go ahead and reconcile. I don't think users will have too much work to do if the key representations and theorems about them are preserved.

Final comment, the word_bitwise representation Sascha and I worked on in 2010 uses the boolean list representation (to_bl/of_bl) or, more precisely, its reverse (rev o to_bl/of_bl o rev). In hindsight, the HOL4 group's approach based on the function-to-bool representation (test-bit in Isabelle) is probably smarter, since it caches better, though it involves lots of natural inequalities which require simprocs to resolve in Isabelle and are a bit of a nuisance. I'm not sure if that is even slightly relevant.

Sincerely,
    Thomas.

On 19/08/13 03:35, Brian Huffman wrote:
I created Library/Bit.thy in February 2009 as a theory of the field of
integers mod 2. One motivation was to be able to have polynomials with
integers mod 2 as coefficients, which have applications in
cryptography. (I had also been working on Library/Polynomial.thy
around the same time.) As a field, it is possible to use type "bit"
with polynomial operations like div, mod, and gcd.

The connections between Bit.thy and the ancient numeral representation
using _ BIT _ are accidental (see rev. 8e33b9d04a82); it is just a
coincidence that the new type is also named "bit". The other uses of
Bit.thy in HOL-Word are also likely due to my choice of the name of
the type "bit" more than anything else. Perhaps "Z2" or "z2" would
have been a better name for the new type; I just thought that an
English word would fit better with Isabelle's naming conventions.

In summary: I never meant for Library/Bit.thy to have any connection
whatsoever to HOL-Word; I'd be in favor of converting HOL-Word to use
type bool instead. Also, I'm open to renaming Library/Bit.thy to more
accurately describe its contents and intended use.

- Brian

On Sun, Aug 18, 2013 at 7:35 AM, Florian Haftmann
<florian.haftmann at informatik.tu-muenchen.de>  wrote:
Hello all,

I have been revisiting the HOL-Word theories, and a central question
which has come to my mind is how bits are to be represented.  Some
theories are just using bool, but some use a dedicated but also
two-valued type bit.  This mixture is awkward.  Further, it seems to me
that the use of the bit type (in connection with the pseudo infix
constructor _ BIT _, which is the seed of almost all further usages of
type bit) goes back to the ancient numeral representation as signed bit
strings, which is now gone.

So, I would call for feedback from users of the HOL-Word theories:

* Is there a reason to prefer bit over bool or the other way round, and
if yes, in which situations?  Or does that just appear as accident?

* If bool would be the preferred type, is it feasible (wrt. to existing
applications »outside there«) to replace bit by bool entirely? This
could also include input syntax 0 and 1 for False and True respectively,
a conversion of_bool :: bool =>  'a::zero_neq_one etc.

Suggestions welcome,
         Florian

--

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.