Redundancy of Arguments Reduced to Induction
Marı́a Alpuente, Rachid Echahed, Santiago Escobar, Salvador Lucas · Electronic Notes in Theoretical Computer Science · 2002
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 class of inductive theorems in the equational theory of confluent, sufficiently complete term rewriting systems (TRSs). Hence, existing results for proving inductive theorems can be exploited to 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 and abstract rewriting (a technique for approximating normal forms in sufficiently complete, left linear, canonical TRSs).