María Alpuente, Rachid Echahed, Santiago Escobar, and Salvador Lucas.
We demonstrate that the problem of identifying redundant arguments of function symbols, i.e. parameters which can be replaced by any expression without changing the associated semantics, boils down to proving the validity of a particular classs of inductive theorems in the equational theory of confluent, sufficiently complete TRSs. Hence, existing results for proving inductive theorems can be exploited, which solve the problem in many interesting cases where previously developed methods fail to recognize and remove redundancies. In particular, this novel formulation directly yields a new decidability result for the redundancy problem which is based on the so-called standard theories. As an additional result which stems from the inductive encoding of the redundancy problem, we finally propose two different techniques for the analysis of redundant arguments, which are respectively based on inductionless induction (a decision algorithm for induction theorems in standard theories) and abstract rewriting (a technique for approximating normal forms in sufficiently complete, left linear, canonical programs).