@article{oai:nagoya.repo.nii.ac.jp:00019057,
 author = {Kasuya, Hideto and Sakai, Masahiko and Agusa, Kiyoshi},
 issue = {2},
 journal = {情報処理学会論文誌, プログラミング},
 month = {Mar},
 note = {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.},
 pages = {144--165},
 title = {Head-Needed Strategy of Higher-Order Rewrite Systems and Its Decidable Classes},
 volume = {2},
 year = {2009}
}