Recognizing when two arithmetic expressions are essentially the same | Hacker News Reader

Recognizing when two arithmetic expressions are essentially the same

blog.plover.com

102 pointsgbacon36 comments

Just 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) = 24

I'm guessing two variables here; I didn't look too closely. x=3, y=8

  x*(y*(x/x)) = f(x,y)
  x+((x*y)-x) = g(x,y)

These are pretty obviously both xy, but rather than solve it, find the maximum degree, which is 2, and make a few points:

(1,1) => 1(1(1/1)) = 1 = 1+((1*1)-1) (1,0) => 0 for both (1,2) => 2 etc.

It's an old technique; Alan Perlis taught it to me. If two polynomials of degree d agree on more than d points, then their difference (of degree <= d) has more than d roots, so their difference must be 0.

The Schwartz-Zippel lemma is a related, also based on roots https://cs.stackexchange.com/questions/33113/is-there-an-eff...

But your last sentence is only true among single-variable polynomials, isn't it? For example, f(x,y)=xy and g(x,y)=x^2 agree on infinitely many points.

Pick one value for x, now you have a single variable polynomial. Verify that it is equal with above mentioned technique.

Pick another value for x, do the same.

Pick a third...

I didn't prove this works, but I think it should. It is however exponential in the number of variables which may be seen as a downside.

Edit:

This can be proven by induction. Let V = (y, z, ...). Then the polynomial can be expressed as

p = (x-x2)(x-x3)f(V) + (x-x1)(x-3)g(V) + (x-x1)(x-x2)h(V), where x1, x2, x3 are the values we test for x. By inductive hypothesis we can prove each of f, g and h to be zero by testing. But if those are all zero then p is zero.

It seems to me that expanding everything to sum-of-products form and checking for equality directly would be simpler than your algorithm and would run about as fast.

You are correct. Apologies for misremembering. Looking it up shows (d+1)^n points are needed for multivariate.

Thanks, great explanation!

Nice! Maybe rational functions rather than polynomials though, because division is allowed. Anyway, equality of rational functions is reducible to equality of polynomials.

True, I ignored division.

I believe this is used in symbolic solvers to prove identities; that's the context where I learned it.

How 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.

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.

I think the difficulty is in defining the relation, rather than proving it. The problems are so small that it probably doesn't matter how you actually prove equivalence, once you've defined it.

It might be useful to find solutions in the first place. This article was about defining when two expressions are "essentially the same", though, and Z3 isn't going to help you construct a definition :-).

This isn't really an interesting question from the point of view of automated reasoning. The obvious canonical form for such an expression (with variables) is to represent it as a polynomial or rational polynomial, and I don't see why you'd ever do something like what the author of this blog post is doing.

Within 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:

https://en.wikipedia.org/wiki/Polynomial_identity_testing

Basic high school and college math.

https://nbviewer.jupyter.org/url/norvig.com/ipython/Countdow...

This 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.

For sure, only commenting that for that particular problem, brute force is viable. For many problems brute force is not viable.

I was grinding PE a couple years ago to pick up Haskell.

Thank 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)).
    numbers_tree(Vs0, binary(Left, Right)) :-
            permutation(Vs0, Vs),
            append([L|Ls], [R|Rs], Vs),
            numbers_tree([L|Ls], Left),
            numbers_tree([R|Rs], Right).

    tree_op_expr_value(leaf(N), _, number(N), N).
    tree_op_expr_value(binary(Left0, Right0), Op, expr(Op,Left,Right), Value) :-
            tree_op_expr_value(Left0, _, Left, VL),
            tree_op_expr_value(Right0, _, Right, VR),
            op_values_value(Op, VL, VR, Value).

    op_values_value(+, A, B, V) :- V is A + B.
    op_values_value(-, A, B, V) :- V is A - B.
    op_values_value(×, A, B, V) :- V is A * B.
    op_values_value(÷, A, B, V) :- B =\= 0, V is A rdiv B.

We can query it like this:

    ?- numbers_tree([4,6,6,6], T),
       tree_op_expr_value(T, _, Expr, 24).

On backtracking, it generates all solutions, reported as abstract syntax trees Expr.

This is of course not yet the full task. And I won't solve the full task here, because I would like to give others a chance to also have a look. However, I post a hint towards an efficient solution:

In such cases where you want to detect whether something is "essentially the same", consider applying a notion from term rewriting: In term rewriting, we apply rewrite rules, and in strongly normalizing systems, each term has a so-called normal form, which is its canonical representation.

Thus, in the language of term rewriting, when trying to decide if two terms are "essentially the same", you can reduce both of them to their respective normal forms, and then compare the normal forms! The two original terms are the same iff their normal forms are the same.

Here is part of the term rewriting system I have come up with for this task, implemented in Prolog:

    commutative(+).
    commutative(×).

    expr_normal_form(number(N), number(N)).
    expr_normal_form(expr(Op,A0,B0), expr(Op,A,B)) :-
            commutative(Op),
            expr_comparison(A0, B0, Comp),
            smaller_first(Comp, A0, B0, A, B).
    expr_normal_form(expr(Op,A0,B0), expr(Op,A,B)) :-
            \+ commutative(Op),
            expr_normal_form(A0, A),
            expr_normal_form(B0, B).

    smaller_first(=, A0, B0, A, B) :-
            expr_normal_form(A0, A),
            expr_normal_form(B0, B).
    smaller_first(<, A0, B0, A, B) :- smaller_first(=, A0, B0, A, B).
    smaller_first(>, A0, B0, A, B) :- smaller_first(<, B0, A0, A, B).

    expr_comparison(number(A), number(B), C) :- compare(C, A, B).
    expr_comparison(number(_), expr(_,_,_), <).
    expr_comparison(expr(_,_,_), number(_), >).
    expr_comparison(Expr, Expr, =).
    expr_comparison(expr(Op1, _, _), expr(Op2, _, _), C) :-
            dif(Op1, Op2),
            compare(C, Op1, Op2).
    expr_comparison(expr(Op,A0,B), expr(Op,A,B), C) :-
            dif(A0, A),
            expr_comparison(A0, A, C).
    expr_comparison(expr(Op,A,B0), expr(Op,A,B), C) :-
            dif(B0, B),
            expr_comparison(B0, B, C).

It works by imposing an order on terms, and recursively rewriting a single term to its normal form, which is smaller than or equal to the original term according to that (self-imposed) order.

We can now use an additional predicate like the following to collect all solutions, remove duplicates, then rewrite each solution to its respective normal form, and then remove duplicates again:

    all_expressions(Ls, Value, Exprs) :-
            findall(Expr, (numbers_tree(Ls, T),
                           tree_op_expr_value(T, _, Expr, Value)), Exprs0),
            sort(Exprs0, Exprs1),
            maplist(expr_normal_form, Exprs1, Exprs2),
            sort(Exprs2, Exprs).

For example, in the [4,6,7,9] = 24 case, this algorithm reduces the expressions to 5 solutions:

    ?- all_expressions([4,6,7,9], 24, Exprs),
       maplist(portray_clause, Exprs),
       length(Exprs, L).
    expr(×, number(6), expr(÷, expr(+, number(7), number(9)), number(4))).
    expr(×, expr(+, number(7), number(9)), expr(÷, number(6), number(4))).
    expr(÷, number(6), expr(÷, number(4), expr(+, number(7), number(9)))).
    expr(÷, expr(+, number(7), number(9)), expr(÷, number(4), number(6))).
    expr(÷, expr(×, number(6), expr(+, number(7), number(9))), number(4)).
    Exprs = [...],
    L = 5 .

I leave adding more rewrite rules as a challenge.

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)?

In the terminology (may I say: terms) of term rewriting, you are looking for a so-called completion procedure. This takes a set of axioms and turns it into a convergent term rewriting system (or not, because it may not terminate!).

If the completion procedure succeeds, you end up with rules that always terminate, and which reduce any given term to its normal form. In the literature, search for Knuth-Bendix and Huet completion procedure, if you are interested. For SQL, it may get quite complex, but still doable, potentially with some extensions of the primary method.

There are all kinds of variations on the general scheme. If you are interested in term rewriting, a solid starting point is Term rewriting and all that by Baader and Nipkow.

Thank you very much. I checked Wikipedia for Knuth-Bendix and will try to get hold on the book.

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!

>operator inversion identities like a−(b+c)=(a−b)−ca−(b+c)=(a−b)−c, a−(b−c)=(a−b)+ca−(b−c)=(a−b)+c, and their multiplicative analogues. I don't know names for these algebraic laws either.

Isn't that the distributive property of multiplication over addition? There is a -1 that gets multiplied.

> One of my neighbors has the license plate JJZ 4631. «4 6 3 1 ⇒ 24» is one of the more difficult puzzles.

I'm surprised no-one has posted the solution on here yet. Oh well, back to thinking. about it.

Or you could cheat...jam them both into wolfram and see what comes out.

Missing the point. The question here is more about how to generate inputs that would yield the same result in wolfram.

This would not work for floating point arithmetic in computing. The order in which you perform a calculation changes the outcome, since not every number can be precisely represented by the IEEE 754 standard.

Reply on news.ycombinator.com