Head-Needed Strategy of Higher-Order Rewrite Systems and Its Decidable Classes
スポンサーリンク
概要
- 論文の詳細を見る
The present paper discusses a head-needed strategy and its decidable classes of higher-order rewrite systems (HRSs), which is an extension of the headneeded strategy of term rewriting systems (TRSs). We discuss strong sequential and NV-sequential classes having the following three properties, which are mandatory for practical use: (1) the strategy reducing a head-needed redex is head normalizing (2) whether a redex is head-needed is decidable, and (3) whether an HRS belongs to the class is decidable. The main difficulty in realizing (1) is caused by the β-reductions induced from the higher-order reductions. Since β-reduction changes the structure of higher-order terms, the definition of descendants for HRSs becomes complicated. In order to overcome this difficulty, we introduce a function, PV, to follow occurrences moved by β-reductions. We present a concrete definition of descendants for HRSs by using PV and then show property (1) for orthogonal systems. We also show properties (2) and (3) using tree automata techniques, a ground tree transducer (GTT), and recognizability of redexes.
- 2009-03-23
著者
-
Hideto Kasuya
Faculty of Information Science and Technology, Aichi Prefectural University
-
Masahiko Sakai
Graduate School of Information Science, Nagoya University
-
Kiyoshi Agusa
Graduate School of Information Science, Nagoya University
-
Kiyoshi Agusa
Graduate School Of Information Science Nagoya University
-
Hideto Kasuya
Faculty Of Information Science And Technology Aichi Prefectural University
-
Masahiko Sakai
Graduate School Of Information Science Nagoya University
関連論文
- Recognizability of Redexes for Higher-Order Rewrite Systems
- Head-Needed Strategy of Higher-Order Rewrite Systems and Its Decidable Classes
- Context-sensitive Innermost Reachability is Decidable for Linear Right-shallow Term Rewriting Systems
- Decidability of Reachability for Right-shallow Context-sensitive Term Rewriting Systems
- Determinization of Conditional Term Rewriting Systems for Program Generation