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

• Item type: Trans(1)
• 公開日: 2009-07-10
• タイトル: Context-sensitive Innermost Reachability is Decidable for Linear Right-shallow Term Rewriting Systems
• タイトル / 言語: en
• タイトル: Context-sensitive Innermost Reachability is Decidable for Linear Right-shallow Term Rewriting Systems
• 言語: eng
• キーワード / 主題Scheme: Other
• キーワード / 主題: 通常論文
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_6501
• 資源タイプ: journal article
• 著者所属: Graduate School of Information Science, Nagoya University
• 著者所属: Graduate School of Information Science, Nagoya University
• 著者所属: Graduate School of Information Science, Nagoya University
• 著者所属: Graduate School of Information Science, Nagoya University
• 著者所属: Graduate School of Information Science, Nagoya University
• 著者所属(英): en
• 著者所属(英): Graduate School of Information Science, Nagoya University
• 著者所属(英): en
• 著者所属(英): Graduate School of Information Science, Nagoya University
• 著者所属(英): en
• 著者所属(英): Graduate School of Information Science, Nagoya University
• 著者所属(英): en
• 著者所属(英): Graduate School of Information Science, Nagoya University
• 著者所属(英): en
• 著者所属(英): Graduate School of Information Science, Nagoya University
• 著者名: Yoshiharu, Kojima; Masahiko, Sakai; Naoki, Nishida; Keiichirou, Kusakari; Toshiki, Sakabe
• 著者名(英): Yoshiharu, Kojima; Masahiko, Sakai; Naoki, Nishida; Keiichirou, Kusakari; Toshiki, Sakabe
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: 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.
• 論文抄録(英) / 内容記述タイプ: Other
• 論文抄録(英) / 内容記述: 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.
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AA11464814
• 書誌情報: 情報処理学会論文誌プログラミング（PRO）; 巻 2, 号 3, p. 20-32, 発行日 2009-07-10
• ISSN / 収録物識別子タイプ: ISSN
• ISSN / 収録物識別子: 1882-7802
• 出版者 / 言語: ja
• 出版者: 情報処理学会