Narrowing-based simulation of term rewriting systems with extra variables and its Termination Proof
✍ Scribed by Naoki Nishida; Masahiko Sakai; Toshiki Sakabe
- Publisher
- Elsevier Science
- Year
- 2003
- Tongue
- English
- Weight
- 251 KB
- Volume
- 86
- Category
- Article
- ISSN
- 1571-0661
No coin nor oath required. For personal study only.
✦ Synopsis
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.
Nishida, Sakai and Sakabe branching if we regard renamed terms as the same, and since none of them are terminating.
On the other hand, as a transformational approach to inverse computation, we have proposed an algorithm to generate a program computing the inverses of the functions defined by a given constructor TRS [15,16]. The generated programs are TRSs if the given TRSs are non-erasing. However, they are EV-TRSs in general. This fact gives rise to necessity of a method to simulate reductions of EV-TRSs.
This paper shows how to simulate reduction sequences of EV-TRSs, and also discusses how to prove termination of the simulation. We first show that narrowing [7] can simulate reduction sequences of EV-TRSs as narrowing sequences starting from ground terms. Such a simulation solves the infinitelybranchingness problem, and terminates for some EV-TRSs even if they are proper. We prove the soundness of the simulation. Then, we prove the completeness of the simulation in case of right-linear systems, and also in case that any redex reduced in the reduction sequences is not introduced by means of extra variables. One of the typical instances of the latter case is a sequence constructed by substituting normal forms for extra variables. As a technique to prove termination of the simulation, we extend the dependency pair method to prove termination of TRSs, which was proposed by T. Arts and J. Giesl [1], into that of narrowing on EV-TRSs, which starts from ground terms. We show that this technique is applicable to right-linear or constructor systems.
This paper is organized as follows. In Section 3, we explain the idea how to simulate the reduction of EV-TRSs using narrowing, and prove the soundness and completeness. In Section 4, we discuss the termination of the simulation, i.e., of narrowing starting from ground terms. Section 5 introduces related works. We give the proofs of some theorems and lemmas in the appendix.
2 Preparation
This paper follows standard notation of term rewriting [2,8,17]. In this section, we briefly describe notations used in this paper.
Let F be a signature and X be a countably infinite set of variables. The set of terms over F (and X ) is denoted by T (F, X ). The set T (F, ∅) of ground terms is simply written as T (F). For a function symbol f , arity(f ) denotes the number of arguments of f . The identity of terms s and t is denoted by s ≡ t. The set of variables in terms t 1 , . . . , t n is represented as Var(t 1 , . . . , t n ). The top (or root) symbol of a term t is denoted by top
We use O(t) to denote the set of all positions of term t, and O F (t) and O X (t) to denote the set of function-symbol and variable positions of t, respectively. We use ε to represent the top position. For p, q ∈ O(t), we write p ≤ q if there exists p satisfying pp = q. The subterm at a position p ∈ O(t) is