When are two expressions 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