Show Posts

This section allows you to view all posts made by this member. Note that you can only see posts made in areas you currently have access to.


Messages - harold

Pages: 1 ... 6 7 [8] 9 10 ... 16
106
Computer Programming / Addition in the bitfield domain
« on: July 16, 2013, 01:54:05 pm »
Ok I lied, there isn't just one bitfield domain, there are two. And I'm interested in both in them.

One them (henceforth BD1), as described here (chapter 2.8) works like this:
An abstract value in BD1 is a pair (z, o) describing the set { x for which (x | z) == -1 and (x | o) == o } (I know the o is easy to confuse with zero, but it's really an o and I didn't choose this notation)
So, in English, z is a bitmask where a zero at position k means that no elements in the set are allowed to have bit k set to zero, a one in z at position k means that elements in the set may have bit k set to zero (but they don't necessarily). o on the other hand is a mask that describes which bits are allowed to be one.
For example,
Code: [Select]
z = 1110
o = 0001
set: { 0001 }

z = 1111
o = 0011
set: { 0000, 0001, 0010, 0011 }

z = 1111
o = 1110
set: even numbers
Some abstract operators are:
Code: [Select]
(z1, o1) | (z2, o2) = (z1 & z2, o1 | o2)
(z1, o1) & (z2, o2) = (z1 | z2, o1 & o2)
(z1, o1) ^ (z2, o2) = ((z1 & z2) | (o1 & o2), (z1 & o2) | (o1 & z2))
And obviously you can build addition out of those, but that's not very efficient. So, question 1, does anyone have a better idea for how to implement addition in BD1? Something nice and elegant like the ones above?

The other obvious implementation of a bitfield domain, BD2, is with a bitmask m that says which bits are known and a value v in which only the bits that are set in m are relevant and the rest are zero for convenience. Unlike BD1, BD2 has no representation for the empty set (BD1 has multiple such representations, namely all those where at some position k, both z and o have a zero).
Anyway, a value in BD2 is thus a tuple (m, v) and as example
Code: [Select]
m = 1111
v = 0101
set: { 0101 }

m = 1001
v = 0000
set: { 0000, 0010, 0100, 0110 }

m = 0001
v = 0000
set: even numbers
Some abstract operations are:
Code: [Select]
(m1, v1) | (m2, v2) = ((m1 & m2) | v1 | v2, v1 | v2)   // both known or one of them is 1
(m1, v1) & (m2, v2) = ((m1 & m2) | (m1 ^ v1) | (m2 ^ v2), v1 & v2) // both known or one of them is 0
(m1, v1) ^ (m2, v2) = (m1 & m2, (v1 ^ v2) & m1 & m2)
Most things get more complicated in this formulation, except XOR.
In BD2, building addition from these primitives is even worse than it was in BD1.
You can rewrite it a little and get this, which is about 14 times faster in practice:
Code: [Select]
uint abm = m1 & b2;
uint knownzero = m1 ^ v1 | m2 ^ v2;
uint knownone = v1 | v2;
uint cm = 1 | ((abm & ~(v1 ^ v2)) << 1);
uint cv = (v1 & v2) << 1;
uint m = 0;

for (int i = 0; i < 32; i++)
{
    uint e = cm & abm;
    m |= e;
    uint t = (cm & cv & knownone) << 1;
    cm |= ((e | cm & ~cv & knownzero) << 1) | t;
    cv |= t;
}
v = v1 + v2;
But I suspect that there's some trick I'm missing. Something elegant I'm overlooking. Something like this:
Code: [Select]
(m1, v1) + (m2, v2) = (~(v1 + v2) ^ ((v1 | ~m1) + (v2 | ~m2)), v1 + v2)But that doesn't work. This is basically saying "a bit of the result is known if it is the same in (minimum element in set 1 + minimum element in set 2) and in (maximum element in set 1 + maximum element in set 2)", which is not true in general, because for example (now using the general notation where an * means "unknown") 000* + 000* = 00** whereas the above code would conclude that the least significant bit is known to be zero.
So question 2, is there a better way to implement addition in BD2?

Any useful (or interesting, or better yet: both) ideas are appreciated.

107
Math and Science / Propagating bounds through OR and AND
« on: June 19, 2013, 06:16:34 pm »
Problem description:
There are two variables, x which is known to be in the range [a, b], and y which is known to be in the range [c, d].
The problem is, compute the tightest range that contains all the possible values that x|y  (that's a bitwise OR) could have.

The solution, if you want it, can be found in Hacker's Delight.

Now, the real reason I posted this is that I discovered a more efficient algorithm than the one in HD (it's actually on the HD website as of recently, in the Contributions from Correspondents section), and I'd like to try to prove its correctness formally (I only have a sort of informal justification for it).

Spoiler contains the algorithm I discovered + justification (no proof).

Spoiler For Spoiler:
Explanation below.
Code: [Select]
unsigned minOR(unsigned a, unsigned b, unsigned c, unsigned d)
{
   unsigned settablea = (a ^ b) == 0 ? 0 : 0xFFFFFFFF >> nlz(a ^ b);
   unsigned settablec = (c ^ d) == 0 ? 0 : 0xFFFFFFFF >> nlz(c ^ d);
   unsigned candidatebitsa = (~a & c) & settablea;
   unsigned candidatebitsc = (a & ~c) & settablec;
   unsigned candidatebits = candidatebitsa | candidatebitsc;

   unsigned target = candidatebits == 0 ? 0 : 0x80000000 >> nlz(candidatebits);
   // small optimization compared to ~a & target
   unsigned targeta = c & target;
   unsigned targetc = a & target;

   unsigned newa = a & (targeta == 0 ? -1 : -targeta);
   unsigned newc = c & (targetc == 0 ? -1 : -targetc);
   // no need to actually set the target bit, it will be 1 in the other bound by construction
   return newa | newc;
}

It's based on the algorithm from HD. It uses the same strategy, but takes a shortcut. The way both algorithm work is by increasing a or c in a way that you set a bit that is already set in the other (so setting them does not increase the value of a|c) but in return that lets you reset all the bits that are less significant than that bit, so the value of a|c can do down. Of course you can not increase a beyond b, not c beyond d. It should be possible to prove that it actually results in the lower bound if you pick the highest bit that you can set in that way.
HD's algorithm starts at the top bit and works its way down until it finds the first bit it can set in either a or c.
The algorithm I discovered relies on the fact that a <= b, and therefore the the highest bit k at which a and b differ must be 0 in a and 1 in b. (a | (1 << k)) & -(1 << k)  must then be less than or equal to b, because it has the same prefix and then continues with only zeroes.
So the "using this bit won't make a bigger than b"-test is a simple bitmask. That mask can be ANDed with the other condition (let's name the result of that AND the candidate bits), and then the highest set bit is the highest bit that passes both tests. If you do this for both bounds, then the highest set bit in the union of the two sets of candidate bits is the bit that can be set in some bound (you forgot, at that point, which bound - but that's easy to find out again) such that it minimizes a|c.

So.. any tips on how to prove it formally?

108
Computer Programming / Re: I'm learning C++!
« on: June 10, 2013, 04:23:48 pm »
I believe there are execution paths in which for example "sanity" is read without ever having been written to (though I admit I did not look that closely), that could give trouble

Simple way to fix that would be to just set them to some value when declaring them.

109
Computer Projects and Ideas / Re: haroldbot (theorem prover / solver)
« on: June 07, 2013, 07:12:32 pm »
Update: !!changed the meaning of >>>!! added some functions, added a fallback to a SAT solver, and improved the detection of simple expressions (ie when you say "haroldbot: a + b" it should say "[a + b]" instead of "[solution not constant]")

110
Other / Re: New Desktop. Or as I like to call it, Batman.
« on: May 24, 2013, 01:34:37 pm »
No it doesn't, i7 Extreme's (often grouped with i7) have 6 cores. Regular i7's are quad cores.
At least, that has been the pattern so far.
Source:
http://en.wikipedia.org/wiki/Haswell_%28microarchitecture%29
http://en.wikipedia.org/wiki/Ivy_Bridge_%28microarchitecture%29
http://en.wikipedia.org/wiki/Sandy_Bridge_%28microarchitecture%29

111
Other / Re: New Desktop. Or as I like to call it, Batman.
« on: May 24, 2013, 07:54:35 am »
Stock cooler? Why?

112
Introduce Yourself! / Re: Hi, it's Stolen Goods.
« on: May 24, 2013, 03:53:19 am »
I'm curious, what's the story behind your nick?

Also,

113
Miscellaneous / Re: Religion Discussion
« on: May 22, 2013, 03:53:26 am »
Ok, fine. So he was always there? Or just appeared? But it doesn't really matter anyway. I just threw that into the mix because I thought it would be an interesting alternative.
That's all it will be anyway - potentially interesting thoughts. None of it can be verified.

The concept of something creating itself is interesting, right? Well at least I think so.
He couldn't appear because according to the religious, He's the inventor of the time. So He was "always" here.
And you're theory isn't really interesting because it's impossible. A think can't create itself, since it has to already exist to do so.
That sort of reasoning applies only to normal things. Why should gods care about a little problem like causality? They violate the rules anyway. Might as well violate one more.
Time travel would be a potential mechanism for it - go back in time to before you existed, then create yourself. How do you even get into that "loop"? Whether you can do that, and how, depend on how time travel would work. For example if you have alternate time lines, perhaps it would work such that every possible time line has to exist, for some definition of possible. That could mean there are time lines where deities create themselves, depending on the definition of possible. These time lines could perhaps be purely circular.
Impossible? Of course. But still interesting. Lots of impossible things are interesting.

114
Miscellaneous / Re: Religion Discussion
« on: May 21, 2013, 02:52:58 pm »
So am I, it violates causality big-time. But that's why it's interesting

115
Miscellaneous / Re: Religion Discussion
« on: May 21, 2013, 02:46:38 pm »
What if God created himself? Infinite chain broken. And never mind that it doesn't make sense, making sense was never a requirement..
God wasn't created.
Ok, fine. So he was always there? Or just appeared? But it doesn't really matter anyway. I just threw that into the mix because I thought it would be an interesting alternative.
That's all it will be anyway - potentially interesting thoughts. None of it can be verified.

The concept of something creating itself is interesting, right? Well at least I think so.

116
Miscellaneous / Re: Religion Discussion
« on: May 21, 2013, 02:36:35 pm »
The argument "no proof that it doesn't exist" can be applied to a ton of things that no one believes in, including of course, a bunch of "rival" deities. It's not wrong, but neither is a theory positing the existence of a deity.

117
Miscellaneous / Re: Religion Discussion
« on: May 21, 2013, 10:13:14 am »
What if God created himself? Infinite chain broken. And never mind that it doesn't make sense, making sense was never a requirement..

What if He did? It doesn't matter.
It answers how he came to be without having an infinite regress, that's the point - though it is, arguably, no better explanation than an infinite regress.

118
Miscellaneous / Re: Religion Discussion
« on: May 21, 2013, 10:07:05 am »
What if God created himself? Infinite chain broken. And never mind that it doesn't make sense, making sense was never a requirement..

119
Miscellaneous / Re: Religion Discussion
« on: May 21, 2013, 09:53:24 am »
So I took a look at Romans 1:20, it says
Quote
For since the creation of the world God’s invisible qualities—his eternal power and divine nature—have been clearly seen, being understood from what has been made, so that people are without excuse.
Which is basically says "if God made everything and stuff exists, then God has eternal power and a divine nature". Let's analyze that:
Let's use X for "god made everything", Y for "stuff exists" and Z for "god has eternal power and a divine nature". Then it translates to (X ∧ Y) → Z. Without assumptions, does this imply Z? Nope. Does it imply ¬Z? Nope.
If you assume X and Y, then Z. Z could also be true regardless, because it's not a two-way implication. Or ¬Z, because one or both assumptions could be false.
Then there's an other issue: all of this assumes the statement was true in the first place, and there's no guarantee of that. The statement isn't proven, merely stated. It makes sense though - if god created everything then it's fair to say he's divine and powerful.

So what does Romans 1:20 do? Nothing but add to the confusion, really.

120
Update: everything is now signed. You can go back to unsigned with the keyword "unsigned".

Pages: 1 ... 6 7 [8] 9 10 ... 16