### Author Topic: haroldbot (theorem prover / solver)  (Read 16021 times)

0 Members and 1 Guest are viewing this topic.

#### harold

• LV5 Advanced (Next: 300)
• Posts: 226
• Rating: +41/-3
##### Re: haroldbot (theorem prover / solver)
« Reply #15 on: August 11, 2013, 11:27:16 am »
Update: added custom functions.
Blog about bitmath: bitmath.blogspot.nl
Check the haroldbot thread for the supported commands and syntax.
You can use haroldbot from this website.

#### harold

• LV5 Advanced (Next: 300)
• Posts: 226
• Rating: +41/-3
##### Re: haroldbot (theorem prover / solver)
« Reply #16 on: December 04, 2013, 03:29:09 pm »
Progress update:
I've been working on a complete rewrite - and I do mean complete. Everything from the BDD engine to the parser to the IRC interface is completely new and more awesome. The basic idea remains the same, but it should be more efficient, and allow for larger BDDs (no, not 32x32 multiplication) - no one has needed larger ones yet (and yes I do keep an eye on the queries), but whatever.
Some changes that already happened include (but are not limited to)
- using IRC colours for some things ..
- .. such as the biggest (so far) new feature: if the BDD associated with an AST node is not recognized, recurse to the children and stick an operator in between the results. This should do away with the dreaded "solution isn't constant". The colours indicate whether a node was recognized or not.
- very large expansion of the class of functions detected, such as functions with more than 2 inputs.

I will experiment with recursive functions. My idea is to use a new variable to stand in for the result of the recursive call, then fill in the function itself as that variable (which is pretending to be a function argument) using BDD function composition. Then it's 2 calls deep. Then compose two of those together. 4-deep. I'll keep doing that until the function no longer changes (which means it was expanded deeper than any set of arguments could make it go), or until it times out or runs out of space (functions that go too deep or get too complicated). Does anyone see any obvious problems with that?
Apparently that doesn't work. So no recursion, sorry.
« Last Edit: January 22, 2014, 02:04:06 pm by harold »
Blog about bitmath: bitmath.blogspot.nl
Check the haroldbot thread for the supported commands and syntax.
You can use haroldbot from this website.

#### harold

• LV5 Advanced (Next: 300)
• Posts: 226
• Rating: +41/-3
##### Re: haroldbot (theorem prover / solver)
« Reply #17 on: June 09, 2016, 01:09:11 pm »
Since version 2.0 is out (has been for a while actually) a small update.
A bunch of features that never really worked well are not in 2.0, such as functions, let-guards (what even are those, you're probably wondering), solve-with-arguments/universal quantification and the weirdest feature ever, "loop".

They probably won't be back, unless anyone complains. No one used them except to try them out. Solve-with-arguments was actually quite powerful, but I guess no one understood what it does (I'm not sure I understand it myself tbh), annoying to implement though.

The SAT part doesn't work properly so if you use queries that are too hard for BDDs it will just fail in some obscure way.
Blog about bitmath: bitmath.blogspot.nl
Check the haroldbot thread for the supported commands and syntax.
You can use haroldbot from this website.

#### SpiroH

• LV8 Addict (Next: 1000)
• Posts: 726
• Rating: +153/-23
##### Re: haroldbot (theorem prover / solver)
« Reply #18 on: June 10, 2016, 10:29:48 am »
Hi, Harold,
1. Is this basically an expression parser either numeric (calculation) or symbolic (theorem proving) or is there more to it?
2. Can you convince @Sorunome to try it out on OIRC (again )?

Although somewhat abstract in the language used it seems rather interesting.  IMHO you could (can) put it in simpler terms to make it more understandable (and interesting) for the general audience.
Why not make a simple toy calculator/evaluator in (eg) Java (as a concept proof) so that boys/girls can play with it to solve everyday's life problems? (A simple example is often worth a thousand words).

#### harold

• LV5 Advanced (Next: 300)
• Posts: 226
• Rating: +41/-3
##### Re: haroldbot (theorem prover / solver)
« Reply #19 on: June 10, 2016, 11:16:41 am »
It's symbolic, it can do concrete calculations too, that's necessary of course but also in a way a side effect of the symbolic engine. It's not terribly useful as Plain Old Calculator though.

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

Everyday's life problems though, I think that's more something for wolfram alpha. But perhaps I can explain just what it is that haroldbot does, without going too far into the technical details.

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).
Blog about bitmath: bitmath.blogspot.nl
Check the haroldbot thread for the supported commands and syntax.
You can use haroldbot from this website.

#### SpiroH

• LV8 Addict (Next: 1000)
• Posts: 726
• Rating: +153/-23
##### Re: haroldbot (theorem prover / solver)
« Reply #20 on: June 16, 2016, 09:54:15 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
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).
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

• LV5 Advanced (Next: 300)
• Posts: 252
• Rating: +10/-1
• The impossible chemical compound.
##### Re: haroldbot (theorem prover / solver)
« Reply #21 on: June 21, 2016, 09:47:33 pm »
Can someone explain why ""0x80000000 / -1" in signed mode" should error?
-German Kuznetsov
The impossible chemical compound.

#### harold

• LV5 Advanced (Next: 300)
• Posts: 226
• Rating: +41/-3
##### Re: haroldbot (theorem prover / solver)
« Reply #22 on: June 22, 2016, 03:34:07 am »
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.
« Last Edit: June 26, 2016, 08:24:48 am by harold »
Blog about bitmath: bitmath.blogspot.nl
Check the haroldbot thread for the supported commands and syntax.
You can use haroldbot from this website.

#### SpiroH

• LV8 Addict (Next: 1000)
• Posts: 726
• Rating: +153/-23
##### Re: haroldbot (theorem prover / solver)
« Reply #23 on: June 22, 2016, 09:58:52 am »
...
On the other hand, 0x80000000 is a fairly legitimate result for 0x80000000 / -1, because -0x80000000 = 0x80000000.
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?

#### harold

• LV5 Advanced (Next: 300)
• Posts: 226
• Rating: +41/-3
##### Re: haroldbot (theorem prover / solver)
« Reply #24 on: June 22, 2016, 10:04:56 am »
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
Blog about bitmath: bitmath.blogspot.nl
Check the haroldbot thread for the supported commands and syntax.
You can use haroldbot from this website.