A Formal Approach for Reasoning about the Effectiveness of Partial Evaluation
Elvira Albert, Sergio Antoy, Germán Vidal · 2000
. The motivation of partial evaluation is to improve efficiency while preserving program meaning. Rather surprisingly, relatively little attention has been paid to the development of formal methods for reasoning about the effectiveness of this program transformation---usually, only experimental tests on particular languages and compilers are undertaken. In this work, we present a formal approach for measuring the effectiveness of partial evaluation which is intended to complement, rather than to replace, more traditional profiling approaches. For this purpose, we introduce several formal criteria to measure the efficiency of functional logic computations which are independent of a concrete implementation. We also provide a method to automatically infer some recurrence equations that relate the cost of executing the original and residual programs. Although a precise estimation of the speedup achieved by partial evaluation is generally undecidable, we outline how these recurre...