María Alpuente, Santiago Escobar, and Salvador Lucas.
The uncontrolled application of automatic transformation processes during the formal development and optimization of programs can introduce encumbrances in the generated code that programmers usually (or presumably) do not write. An example is the introduction of redundant arguments in the functions defined in the program. Redundancy of a parameter means that replacing it by any value does not change the result since the value is not used. In this work, we give a theoretical foundation for the analysis and elimination of redundant arguments in term rewriting systems as a model for the programs that can be written in more sophisticated declarative languages. The framework is independent from both the considered semantics and the framework -operational or denotational- which is used to describe (and approximate) the observed meaning. We particularize our method to the standard (reduction) semantics of term rewriting systems including the standard normalization semantics (typical of pure rewriting) and the evaluation semantics (closer to functional programming). On the basis of the analyses, we formalize an erasure procedure which preserves the semantics and produces smaller programs which are easier to understand and maintain. Finally, we indicate how the present method can be extended to more sophisticated program observable properties such as computed answers.
Term rewriting, declarative programming, formal methods, semantics, program analysis and optimization