Context-sensitive Innermost Reachability is Decidable for Linear Right-shallow Term Rewriting Systems

Access this Article



The reachability problem for given an initial term, a goal term, and a term rewriting system (TRS) is to decide whether the initial one is reachable to the goal one by the TRS or not. A term is shallow if each variable in the term occurs at depth 0 or 1. Innermost reduction is a strategy that rewrites innermost redexes, and context-sensitive reduction is a strategy in which rewritable positions are indicated by specifying arguments of function symbols. In this paper, we show that the reachability problem under context-sensitive innermost reduction is decidable for linear right-shallow TRSs. Our approach is based on the tree automata technique that is commonly used for analysis of reachability and its related properties. We show a procedure to construct tree automata accepting the sets of terms reachable from a given term by context-sensitive innermost reduction of a given linear right-shallow TRS.<br/>


  • Information and Media Technologies

    Information and Media Technologies 4(4), 802-814, 2009

    Information and Media Technologies Editorial Board


  • NII Article ID (NAID)
  • Text Lang
  • Data Source
Page Top