Narrowing-based effective rewriting and its termination for term rewriting systems with extra variables

摘要

Term rewriting systems with extra variables (called EV-TRSs) were not used since each one-step reduction by their rule with extra variables is infinitely branching and they are not terminating. Then, we've proposed an effective rewriting technique, called EV-narrowing, which is a natural extension of narrowing, and shown that an EV-narrowing of an EV-TRS is terminating if a TRS which presents the relations between the original defined symbol's calls [11]. In this paper, we prove the termination of EV-narrowing and give an outline for it, extending and using the dependency pair technique [1] to prove the termination of TRSs.