Or you could cheat...jam them both into wolfram and see what comes out.
Recognizing when two arithmetic expressions are essentially the same
11–20 of 39 posts
Re: Recognizing when two arithmetic expressions are essentially the same
#12How would a therom prover like z3 handle this, out of interest? Isn't it the ideal domain for it?
Solving the problem of "recognizing when two arithmetic expressions are equivalent" is indeed ideal for an approach like Prolog or a SAT/SMT solver. In fact SMTLIB2 has a standardized expression for asserting if two expressions are identical. Conversely, many APIs make testing that sort of claim easy (and even emjoy tactics for things like synthesize new expressions w/ respect to some 'cost' function for each sub-expression, etc)
With that said, the author of this article seems to be interested in some sort of other question entirely.
Re: Recognizing when two arithmetic expressions are essentially the same
#13Thank you for sharing! A closely related puzzle was previously discussed at: https://news.ycombinator.com/item?id=14400017 The present puzzle can be seen as a natural continuation of this earlier thread, and the declarative programming language Prolog is again well-suited for this puzzle. For example, we can start with a short Prolog program that exhaustively generates all solutions: numbers_tree([N], leaf(N)). numbe…
It's kindof funny zmonx, whenever there is a challenge that I think "oh I can do this with a SAT solver" , you've already shown up and solved it with Prolog. I think you've gone for the more 'expressive' variant here. If I were writing SMTLIB directly or using an API, I'd prove the assertion that any possible parenthization is eqv by enumerating & checking them individually :)
This may get out of hand: The task asks not only for all parenthesizations, but also other equivalence classes. The rewrite rules and Prolog in general let you express the equivalence classes reasonably concisely and efficiently.
I'm still always interested also in other approaches, and greatly enjoy your SAT solutions!
Re: Recognizing when two arithmetic expressions are essentially the same
#14Just make the expressions into polynomials with variables x_1..x_k for the k different numbers, and see if they agree at (degree + 1) distinct points.
Re: Recognizing when two arithmetic expressions are essentially the same
#15This would have been very useful solving Project Euler's problem 93: https://projecteuler.net/problem=93 .
That problem is small enough to just brute force. There are only 1612800 calculations to do.
Of course... but for many people, in Project Euler the goal is not just to get a solution, it's to create a beautiful and/or efficient solution. This is why reading the comments and finding other people's solutions after solving a problem is usually as fulfilling as solving it, or even more.
Re: Recognizing when two arithmetic expressions are essentially the same
#16Re: Recognizing when two arithmetic expressions are essentially the same
#17Just make the expressions into polynomials with variables x_1..x_k for the k different numbers, and see if they agree at (degree + 1) distinct points.
Could you please show the polynomial forms for these, and an example of your technique?
3*(8*(3/3)) = 24
3+((3*8)-3) = 24Re: Recognizing when two arithmetic expressions are essentially the same
#18How would a therom prover like z3 handle this, out of interest? Isn't it the ideal domain for it?
Z3 and similar tools use a combination of canonicalization followed by brute force search. The canonicalization uses techniques similar to what the OP describes. (+ a (+ b c)) and (+ c (+ b a)) are both rewritten as (+ a b c). These rewrites rely on pattern matching.
At this point, if the query is syntactically solvable, we are done. Often queries are not, so the solver uses a symbolic decision procedure. The specific decision procedure depends on the formula. For example, Linear Integer Arithmetic (which allows addition of variables and multiplication by only constants) can be solved using Simplex.
Re: Recognizing when two arithmetic expressions are essentially the same
#19Thank you for sharing! A closely related puzzle was previously discussed at: https://news.ycombinator.com/item?id=14400017 The present puzzle can be seen as a natural continuation of this earlier thread, and the declarative programming language Prolog is again well-suited for this puzzle. For example, we can start with a short Prolog program that exhaustively generates all solutions: numbers_tree([N], leaf(N)). numbe…
You defined rewrite rules that reduce an expression down to a 'normalized' form such that two expression are equivalent if they reduce to the same 'normalized' form. These rules are obvious for simple arithmetic expressions.
Is it possible to deduce the normalized form and the rewrite rules from a set axioms automatically (e.g. for relational (like SQL) expression with operands like join, project, filter)?
Re: Recognizing when two arithmetic expressions are essentially the same
#20Within its domain, that's what the Oppen-Nelson simplifier did. Many provers since can do that. Amusingly, Plato, the first on-line teaching system, had a solver for that. It was used to check student's answers to math problems. It worked by plugging in some random numeric values and evaluating. If many sets of random values evaluated the same as the desired answer, it was accepted as equivalent.
what kind of math problems were the students supposed to solve? I ask because the approach you mention is still the best way we have of determining whether two polynomials are equivalent: