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.
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.
Nice! Maybe rational functions rather than polynomials though, because division is allowed. Anyway, equality of rational functions is reducible to equality of polynomials.
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:
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.
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.
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:
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.
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.
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.
