Context-sensitive Innermost Reachability is Decidable for Linear Right-shallow Term Rewriting Systems
スポンサーリンク
概要
- 論文の詳細を見る
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 編集運営会議の論文
著者
-
Sakai Masahiko
Graduate School Of Information Science Nagoya Univ.
-
Kusakari Keiichirou
Graduate School Of Information Science Nagoya Univ.
-
Sakabe Toshiki
Graduate School Of Information Science Nagoya University
-
Nishida Naoki
Graduate School Of Information Science Nagoya University
-
Kojima Yoshiharu
Graduate School of Information Science, Nagoya University
関連論文
- Head-Needed Strategy of Higher-Order Rewrite Systems and Its Decidable Classes
- Recognizability of Redexes for Higher-Order Rewrite Systems
- Decidability of Termination and Innermost Termination for Term Rewriting Systems with Right-Shallow Dependency Pairs
- Static Dependency Pair Method Based on Strong Computability for Higher-Order Rewrite Systems
- Static Dependency Pair Method for Simply-Typed Term Rewriting and Related Techniques
- Head-Needed Strategy of Higher-Order Rewrite Systems and Its Decidable Classes
- Formation and Exchange Processes of Alkanethiol Self-Assembled Monolayer on Au(111) Studied by Thermal Desorption Spectroscopy and Scanning Tunneling Microscopy
- Thermal Desorption Spectroscopy of Alkanethiol Self-Assembled Monolayer on Au(111)
- Dimerization Process in Alkanethiol Self-Assembled Monolayer on Au(111)
- Argument Filterings and Usable Rules in Higher-order Rewrite Systems
- Primitive Inductive Theorems Bridge Implicit Induction Methods and Inductive Theorems in Higher-Order Rewriting
- Characterizing Inductive Theorems by Extensional Initial Models in a Higher-Order Equational Logic
- A Higher-Order Knuth-Bendix Procedure and Its Applications
- On Dependency Pair Method for Proving Termination of Higher-Order Rewrite Systems
- Higher-Order Path Orders Based on Computability(Foundations of Computer Science)
- Decidability of Innermost Termination for Semi-Constructor Term Rewriting Systems
- Confluence of Length Preserving String Rewriting Systems is Undecidable
- Static Dependecy Pair Method in Rewriting Systems for Functional Programs with Product, Algebraic Data, and ML-Polymorphic Types
- Formation and Exchange Processes of Alkanethiol Self-Assembled Monolayer on Au(111) Studied by Thermal Desorption Spectroscopy and Scanning Tunneling Microscopy
- Context-sensitive Innermost Reachability is Decidable for Linear Right-shallow Term Rewriting Systems
- Context-sensitive Innermost Reachability is Decidable for Linear Right-shallow Term Rewriting Systems