Omnimaga
General Discussion => Technology and Development => Computer Projects and Ideas => Topic started by: harold on April 05, 2013, 12:40:19 pm
-
haroldbot (http://haroldbot.nl/) (development name: TheoremBot) was an IRC bot (now only a website) that proves theorems, solves equations, and can even calculate. All in the 32-bit bitvector domain (if that means nothing to you, take that to mean "it calculates with unsigned ints, not natural numbers or real numbers or anything like that).
Warning: the interpretation of >> has changed between versions, it is and was an unsigned shift in the current and the first version, but a signed shift in some versions in between.
Warning: the interpretation of >>> has changed between versions, it is now a rotate.
Warning: in version 5d, theorem proving mode has become much more sensitive to divisions by zero, so sensitive that if there's any possibility of division by zero it will freak out. I'll try to do something about that at some point.
How to use it
There are three basic modes.
- The "solve" mode. Just type in any boolean expression. haroldbot will try to solve it, and give (if applicable) cases of inputs that make it true, false, or result in a divby0. If an expression is always true, haroldbot will search for a proof. Example: "x * 3 == 1" or "x + y == y + x"
- The calculation/simplification mode. Used for any non-boolean expression. You can make any expression non-boolean by surrounding it with parentheses. For non-constant results, only some inputs result in anything interesting (if the resulting BDD can be matched against a known pattern). Example: "1+2+3+4^15" or "a | a"
note: haroldbot tries to answer you regardless of what else you put in a message as long as it has the string haroldbot: in it. If it doesn't answer, usually that means you asked something it didn't like.
note: sometime it will say something like "time-out while counting solutions". That means the BDD approach didn't work out and it had to switch to the SAT solver - don't worry if you don't know what that means, it's the implication of that that's important: it will not find try to find "nice" results, it will find just any old result. Quantified mode does not fall back to the SAT solver (yet?).
Signedness
Values in haroldbot have no signedness, instead the operations have signedness. All operators and functions are unsigned by default, append s (operators) or _s (functions) to get the signed version, if there is one.
Expression syntax
Operator precedence and associativity are almost the same as in C, but not quite. Notably the comparisons have a lower precedence than bitwise operations (but still higher than boolean operations). Here is a list of available operators and their gotcha's, in order of precedence (groups of equal precedence not shown)
- ~ bitwise NOT, aka 1's complement.
- - unary minus, aka 2's complement.
- * multiplication. haroldbot doesn't really like multiplication, especially not if neither of the two operands is a constant. Computation tends to be slow (using the SAT solver fallback) or even time out and give no result.
- /, /u, /s division. The warning about multiplication also applies to division. Note that "0x80000000 / -1" in signed mode doesn't "error", as it usually would.
- %, %u, %s remainder, aka modulo (in the unsigned case). Signed remainder has the sign of the dividend. The warning about multiplication also applies to remainder.
- + addition.
- - subtraction.
- << left shift. haroldbot doesn't like shifts where the right operand isn't a constant, but you can sometimes get away with it. It's not as bad as multiplication.
- >>, >>u, >>s signed right shift in signed mode, unsigned right shift in unsigned mode. The warning about shifts also applies to signed right shift.
- & bitwise AND.
- ^ bitwise XOR.
- | bitwise OR.
- ==, !=, <, <u, <s, >, >u, >s, <=, <=u, <=s, >=, >=u, >=s signed or unsigned comparisons. '=' is not a comparison. Comparisons give a mask of all 1's or all 0's instead of being a boolean true or false.
- => implies. implemented as (~a | b) == -1.
- && boolean AND.
- || boolean OR.
- ?: actually a bitwise mux, acts like the usual ternary operator if the condition can only be 0 or -1 (for example, if the condition is a boolean expression).
- let name = expression in expression used to give names to things. Useful to factor out common sub-expressions. For example: "haroldbot: let m = x >> 31 in abs(x) == (x + m) ^ m"
Built-in functions:
- min(a, b) takes the signed or unsigned minimum of a and b.
- min_s(a, b) takes the signed minimum of a and b.
- min_u(a, b) takes the unsigned minimum of a and b.
- max(a, b) takes the signed or unsigned maximum of a and b.
- max_s(a, b) takes the signed maximum of a and b.
- max_u(a, b) takes the unsigned maximum of a and b.
- popcnt(a) the population count aka hamming weight (number of 1 bits) of a.
- nlz(a) number of leading 0's in a.
- ntz(a) number of trailing 0's in a.
- reverse(a) reverses the bits in a.
- abs(a) takes the absolute value of a where a is interpreted as signed (otherwise it would do nothing).
How it works
It builds an array of 32 binary decision diagram (http://en.wikipedia.org/wiki/Binary_decision_diagram)'s of the input (one for each bit), and does some fairly standard operations on them (quantified solve mode uses universal quantification over all the variables that you didn't mention, which is a bit rare). There's no magic. If you want to learn more about BDD's, you can read the draft of Knuth's Chapter 7.1.4 (http://www.cs.utsa.edu/~wagner/knuth/fasc1b.pdf).
When that fails (that is, there are more than about a hundred thousand nodes in the BDD), it switches to a SAT solver. It switches when the BDDs get too big to fit in their pre-allocated array, the time that takes depends on the speed of the client.
The proofs it finds (if any), are made using the fairly brute-force approach of taking both "ends" of the proof and applying rewrite rules until they meet in the middle. This process is guided somewhat by selecting candidate expressions to rewrite based on their "weight", the weight is a combination of how many steps away it is from the original expression and, crucially, how complicated the expression is. It's an empirical observation that it's usually not necessary to have expressions in a proof that are a lot more complicated than the most complicated "end" of the proof. Of course this does not always hold, so this optimization makes it slower to find some proofs, while making it faster to find typical proofs. A second important component is two forms of hashing. One form that helps to match expressions that are overall structurally equal (all explored expressions are put into hash sets using this type of hash, to make it fast to detect when the two expanding clouds of expressions meet). That hash the usual "combination of hashes of child nodes and this node". The other hash is one that helps to match rewrite rules to expressions, it considers only a node and its immediate children. Rewrite rules are put in bins according to which hashes they would match onto, when rewriting this is used to only attempt to match a rule pattern to an expression if it has a decent chance of actually matching.
I'm open to requests, but BDDs are no silver bullet and will not solve everything, and the SAT solver fallback tends to be really slow (through no fault of its own, it's just that it automatically only gets to deal with hard problems - everything easy is solved by the BDDs). For example multiplication, division and remainder, are just fundamentally hard to deal with. It's also not really a good framework for simplification, but you can use theorem proving mode to test if your own simplification is correct.
-
I tested it; I had fun. I just keep forgetting to use * and == even though I know I am supposed to :P
-
haroldbot now also accepts a single = for equality.
-
wow, this is pretty amazing O.O
-
I added showing up to 4 results to "solve" mode, as well as showing the total number of solutions.
-
Awesome, this will be useful to cheat on tests. Just kidding I might need it from time to time. :P
Also will we be able to use it from OmnomIRC in the future?
-
Wait, in the future? Isn't that possible right now?
-
Here it works from OmnomIRC :)
-
Wait, in the future? Isn't that possible right now?
Ah I didn't know it was implemented already. Many bots creators tend to forget OmnomIRC at first, so I tend to ask if it will be planned :P
-
Actually, for the first couple of hours, it only worked with OmnomIRC :)
-
Update: added abs, changed >> to signed, added >>> as unsigned shift, solved a big bug in quantified solve mode
This new version is now online.
-
This bot is just getting so awesome, nice work! :D
-
Update: everything is now signed. You can go back to unsigned with the keyword "unsigned".
-
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]")
-
Small update: added ternary operator.
-
Update: added custom functions.
-
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.
-
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.
-
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).
-
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).
-
...
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!
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. ;)
-
Can someone explain why ""0x80000000 / -1" in signed mode" should error?
-
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.
-
...
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? :P
-
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