Nothing Special   »   [go: up one dir, main page]

Information and Media Technologies
Online ISSN : 1881-0896
ISSN-L : 1881-0896
Computing
Context-sensitive Innermost Reachability is Decidable for Linear Right-shallow Term Rewriting Systems
Yoshiharu KojimaMasahiko SakaiNaoki NishidaKeiichirou KusakariToshiki Sakabe
Author information
JOURNAL FREE ACCESS

2009 Volume 4 Issue 4 Pages 802-814

Details
Abstract

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.

Content from these authors
© 2009 by Information Processing Society of Japan
Previous article Next article
feedback
Top