  The 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
expression does not change the result. In this work, we provide methods 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 languages. On
the basis of the uselessness of redundant arguments, we also propose an erasure
procedure which may avoid wasteful computations while still preserving the
semantics (under ascertained conditions). A prototype implementation of these
methods has been undertaken, which demonstrates the practicality of our
approach.
