General Discussion > Computer Projects and Ideas

haroldbot (theorem prover / solver)

<< < (5/5)

SpiroH:

--- Quote from: harold on June 10, 2016, 11:16:41 am ---...
The bot on OIRC is dead because I lost my nice host that would let me run an IRC bot, I could find a new host I guess, but it wouldn't be the same as the website any more (it used to be the same program running the site and the IRC bot, though in IRC mode it kept its output short). The website is purely client side now, makes it a lot easier to find free hosts. So it's all in JS now, no more Java. I could dig up my little project to use Eeems' JS bot-framework with haroldbot, and then I'd still have to host it somewhere.. it could be done

--- End quote ---
I'd say, please do it!


--- Quote ---The fundamental difference between haroldbot and the average symbolic math thing is that it works with 32 bit integers. The usual tools typically have no (easy) way to do that (WA can do some of it, but it's awkward), but I needed it, so I filled the gap. This directly results in, for example, x == -x having the solution 0x80000000 as well as the usual 0, and x*3 == 1 having the solution x=0xAAAAAAAB.
The most important use case is testing whether two expressions (with variables in them) are equivalent, with all the math still being doing on 32 bit integers, so it can be useful when debugging some weird bithack you thought of. It can even give a proof in some cases (usually not), which serves two purposes: show that it didn't just lie (the steps can be checked, if it just said "well, they're equal" it's harder to trust that it's right) and, sometimes, show why something is true (for sufficiently legible proofs).

--- End quote ---
I personally like the way you tackle it. In general, it requires some energy to be innovative and break away with the standard reasoning mind set.

I hope someday, some guy from TI, HP or Google (yep!) will approach you with some tempting proposition (email). It will be mostly about work and then again more work. But it can be fun when you're young and you're looking for new experiences.
Keep it up and good luck. ;)

c4ooo:
Can someone explain why ""0x80000000 / -1" in signed mode" should error?

harold:
It doesn't even work right now (oops) (E: works now, without error though), and whether it should error is sort of debatable.. it errors on x86 with the justification that 0x80000000 has no positive equivalent. So it overflows, and x86 division considers overflow an error - usually such overflow would be caused by dividing a very large number by a not large enough number (since it divides a 64bit number by a 32bit number, it can easily be the case that the result does not fit in 32 bits), 0x80000000 / -1 is the only case that overflows without needing a dividend with more bits than the results.

On the other hand, 0x80000000 is a fairly legitimate result for 0x80000000 / -1, because -0x80000000 = 0x80000000.

SpiroH:

--- Quote from: harold on June 22, 2016, 03:34:07 am ---...
On the other hand, 0x80000000 is a fairly legitimate result for 0x80000000 / -1, because -0x80000000 = 0x80000000.

--- End quote ---
Well, it depends on your definition of legitimate. As you know, in (32-bit) two's complement notation, the maximal positive number is 0x7FFFFFFF and the minimal number is 0x80000000. So, -0x80000000 = 2147483648 does not really exist as a positive number.  I don't think this is arithmetically legitimate and you should handle the overflow exception. Or do you mean a possible value? :P

harold:
0x80000000 is also 2147483648 though, just read it as unsigned. -2147483648 and +2147483648 are in the same equivalence class modulo Z/232Z so in that sense they're not even different values

E: in general with haroldbot 2 I've followed the philosophy that the operation is typed, not the values (which are just bitvectors). I think that having it not be an error fits that philosophy, but ultimately the deciding factor is what behaviour is most useful, I've not made up my mind about that yet

Navigation

[0] Message Index

[*] Previous page