Innermost Reachability and Context SensitiveReachability Properties Are Decidable for Linear Right-Shallow Term Rewriting Systems

摘要

A reachability problem is a problem used to decide whether s is reachable to t by R or not for a given two terms s, t and a term rewriting system R. Since it is known that this problem is undecidable, effort has been devoted to finding subclasses of term rewriting systems in which the reachability is decidable. However few works on decidability exist for innermost reduction strategy or context-sensitive rewriting. In this paper, we show that innermost reachability and context-sensitive reachability are decidable for linear right-shallow term rewriting systems. Our approach is based on the tree automata technique that is commonly used for analysis of reachability and its related properties.