e.g. $xy+x+y=x+y(x+1)$ ?
The expressions are from ordinary high-school algebra, but restricted to arithmetic addition and multiplication (e.g. $2+2=4; 2.3=6$), with no inverses, subtraction or division. Letters are variables.
If it helps, we can forbid any expression representable with numeric values other than $1$; i.e. not $x^2$ nor $3x$ nor $4$:
- multilinear, no powers other than $1$: $x+xy \equiv x^1+x^1y^1$ is OK, but not $x^2+x^3y^4$, and not anything that could be represented as that, as in a full expansion to sum-of-products e.g. not $x(x+y) \equiv x^2+y$;
- all one, no coefficients other than $1$: $x+xy \equiv 1.x+1.xy$ is OK, but not $2x+3xy$, and not anything that could be represented as that, as in a full expansion to sum-of-products e.g. not $a(x+y)+x(a+b) \equiv 2ax+ay+bx$ ; and
- no constants other than $1$: again, in the fully expanded sum-of-products e.g. not $(a+1)+(b+1) \equiv a+b+2$
$Q.$ Is there an efficient algorithm to determine if two expressions are equivalent?
To illustrate, here's an inefficient brute-force algorithm with exponential time:
expand both expressions fully to sum-of-products, which can easily be checked for equivalence (just ignore order, since commute/associate can reorder).
$(a+b)(x+y) \rightarrow ax+ay+bx+by$
$a(x+y)+b(x+y) \rightarrow ax+ay+bx+by$
This seems a well-known problem - even high school students are taught manual ways to solve it. It's also solved by automated theorem provers/checkers, but they concentrate on more sophisticated aspects.
Here's a working online automated theorem prover: http://tryacl2.org/, which shows equivalence by finding a sequence of commute/associate/distribute etc:
(thm (= (+ (* x y) x y) (+ x (* y (+ x 1))) )) --- 188 steps
(thm (= (+ y (* x (+ y 1))) (+ x (* y (+ x 1))) )) --- 325 steps
This is my first question here, so please let me know if I've chosen the wrong place, wrong tags, wrong way of describing/asking etc. Thanks!
NB: this question has been rewritten in response to comments
Thanks to all responders! I've learned a lot.