[bazizbaziz]

Undecidable in general, but there are two approaches I've seen work based on AST manipulation and comparison:

1. Solvers that search for applicable re-write rules to transform X into Y, such as Cossette for SQL. These may not terminate because undecidability lol http://cosette.cs.washington.edu/

2. Canonicalization of the AST. This is a form of #1 but much more restricted, and the hope is that functions that are equivalent end up canonicalized in the same way. LLVM and GCC do this for a variety of reasons. In the example given, you'd hope that both functions get canonicalized to either the left or right hand side. https://gcc.gnu.org/onlinedocs/gccint/Insn-Canonicalizations... http://llvm.org/docs/MergeFunctions.html