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)

into

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?

Decidability of equivalence is broken somewhere between simply typed lambda calculus and System-F. Without recursive types you are strongly normalizing and thus "trivially" decidable. However, just adding recursive types does not break decidability (e.g. see http://www.di.unito.it/~felice/pdf/ictcs.pdf). Similarly, just adding some higher-order functions or parametric polymorphism does also not necessarily break decidability (e.g. see Hindley-Milner). In my (admittedly limited) experience, when making a type system stronger, it is usually some strange, som

... (read more)