search

agl / critbit

Critbit trees in C
335 stars 31 forks source link

Incomplete proof that "the only non-zero values for which the sets of true bits for x and x − 1 are disjoint, are powers of two" #1

Open nolanw opened 12 years ago

nolanw commented 12 years ago

I'm curious about the proof you give, in section 12, for the statement "the only non-zero values for which the sets of true bits for x and x − 1 are disjoint, are powers of two". It seems incomplete to me.

You divide the number's bits up WLOG into three pieces: a (possibly empty) series of zeros, followed by a one, followed by a series ones and zeros. The number 1 (i.e. 0x01) cannot be split as such.

1 is of course a power of two, and the most-significant 1 is maintained as a result of the described operations, so I think all you need to do is point out that the third series of bits may also be empty.

(P.S. Thanks for the awesome explanation, I was kind of lost with djb's relatively terse description.)

agl commented 12 years ago

On Sun, Dec 4, 2011 at 2:57 AM, Nolan Waite reply@reply.github.com wrote:

I'm curious about the proof you give, in section 12, for the statement "the only non-zero values for which the sets of true bits for x and x − 1 are disjoint, are powers of two". It seems incomplete to me.

You're absolutely right, thanks for that.

I don't have cweb installed at the moment, so I haven't updated the PDF. But I've fixed the .w file and it'll get included the next time that I do so.

Cheers

AGL

Adam Langley agl@imperialviolet.org http://www.imperialviolet.org