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

Kojima Yoshiharu, Sakai Masahiko, Nishida Naoki, Kusakari Keiichirou, Sakabe Toshiki

doi:10.2197/ipsjtrans.2.162

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

DOI Web Site 参考文献9件オープンアクセス

Kojima Yoshiharu

Graduate School of Information Science, Nagoya University
Sakai Masahiko

Graduate School of Information Science, Nagoya University
Nishida Naoki

Graduate School of Information Science, Nagoya University
Kusakari Keiichirou

Graduate School of Information Science, Nagoya University
Sakabe Toshiki

Graduate School of Information Science, Nagoya University

説明

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/>