Narrowing-based simulation of term rewriting systems with extra variables and its Termination Proof

Term rewriting systems (TRSs) extended by allowing to contain extra variables in their rewrite rules are called EV-TRSs. They are ill-natured since every one-step reduction by their rules with extra variables is infinitely branching and they are not terminating. To solve these problems, this paper shows that narrowing can simulate reduction sequences of EV-TRSs as narrowing sequences starting from ground terms. We prove the soundness of ground narrowing sequences for the reduction sequences. We prove the completeness for the case of right-linear systems, and also for the case that any redex reduced in the reduction sequence is not introduced by means of extra variables. Moreover, we give a method to prove the termination of the simulation, extending the dependency pair method to prove termination of TRSs, into that of narrowing on EV-TRSs starting from ground terms. We show that the method is useful for right-linear or constructor systems.