Semantics-Based Proofs of Equivalence for Functions with Accumulators
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.
Sat 6 AprDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
16:00 - 18:00
|Automatic Equivalence Proofs for Programs with Algebraic Data Types|
|Proving Program Equivalence with Constrained Rewriting Induction and Ctrl|
|Semantics-Based Proofs of Equivalence for Functions with Accumulators|