We know that an expression can be written in various forms. For example: (x - 2)^2 and 4 + x^2 - 4x are the same function.
Given a set of substitution rules (such as the default ones in SymbolicUtils.jl), what is the best way to know if two expressions are equal?
In general, equality of real numbers is not decidable, which means given two expressions you cannot always determine whether they are equal or not. This is Richardson’s theorem.
For some special cases, e.g. when your expressions are polynomials with rational coefficients, the equality is decidable.In that case, you can use e.g. Knuth-Bendix algorithm, which tells you what rewriting rules you need to reduce the expressions to a “normal form” and hence check if they are equal
2 Likes