From crocker%la.tis.com Fri, 02 Jun 89
To: info-hol@clover.ucdavis.edu
Subject: Stumbling over empty bit vectors
Date: Fri, 02 Jun 89 09:39:57 PDT
From: crocker%la.tis.com
Status: RO

I had suggested that the following might be a theorem and might be
useful in building up a theory of bitstrings that hides its development.

        Let f be any function over bitstrings which meets the
        following conditions:

        a) f("0") = a0
        b) f("1") = a1
        c) f(APPEND(x,y)) = op(f(x),f(y)), where op is associative

        Then f exists and is uniquely (and fully) determined.

In discussing this theorem, Tom Melham noted that it "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."


I think Tom is right.  One way to fix this problem is by adding f("")
= ae to give a value to f when it's applied to the empty string.
Another approach is to limit the theorem to monoids (semigroups with
identity).  This is more in keeping with the intuition I was trying to
capture, and all of the examples I showed meet this constraint.  I
don't know of any nice ("nice" = elegant and useful) examples where op
is the operator in a semigroup that is not a monoid.

It might be possible to have this both ways.  Is it possible to set
this up as one theorem that applies to all semigroups, and in
addition, if the semigroup is also a monoid, then the value of f when
applied to zero length bitstrings is automatically determined?