If we expand out an arbitrary program, we get a (usually infinite) expression tree. For instance, we can expand
fact(n) := (n == 0) ? 1 : n*fact(n-1)
fact(n) = (n == 0) ? 1 : n*(((n-1) == 0) ? 1 : (n-1) * ( (((n-1)-1) == 0) ? ... ))))
Let's call two programs "expression-equivalent" if they expand into the same expression tree (allowing for renaming of input variables). Two interesting problems:
- Write an efficient algorithm to decide expression-equivalence of two given programs.
- Write a program M which decides whether a given program is expression-equivalent to M itself.
I'm pretty sure these are both tractable, as well as some relaxations of them (e.g. allowing for more kinds of differences between the expressions).
Does anybody know of an existing name for "expression-equivalence", an existing algorithm for solving either of the above problems, or any relevant literature?