A typical transformation for optimizing recursive functions is to add an additional parameter called an accumulator, which holds the current result of the computation. The transformed function is usually tail-recursive, enabling the compiler to emit efficient code.

Typically, the optimized version of a function (i.e., the tail-recursive version) is simply assumed to be functionally equivalent to the original function. However, as we show here, this is not necessarily the case. We introduce a method for proving, in a semantics-based fashion, functional equivalence between recursive functions and their tail-recursive version, when the equivalence actually holds.

Our method requires a new technical development in the context of constrained term rewriting systems that we call defined functions, which can be used to mimic typical bigops in mathematics such as Σ, Π, ∀, etc. These defined functions can be then be used to define synchronization points in the two versions of the functions. Using unification modulo defined functions as a primitive, we define an algorithm for proving simulation between program configurations. Two-way simulation is used to show equivalence.

This paper presents work-in-progress results. Some of the technicalities involved are simplified in order to ensure a more straightforward presentation.