Descendants and Head Normalization of Higher-Order Rewrite Systems

This paper describes an extension of head-needed rewriting on term rewriting systems to higher-order rewrite systems. The main difficulty of this extension is caused by the ?-reductions induced from the higher-order reductions. In order to overcome this difficulty, we define a new descendant of higher-order rewrite systems. This paper shows the new definition of descendant, its properties and head normalization of head-needed rewriting on orthogonal higher-order rewrite systems.