#
Redundancy of Arguments Reduced to Induction

### Authors

María Alpuente, Rachid Echahed, Santiago Escobar, and Salvador Lucas.

### Abstract

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).