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 describes the new definition and its properties and head normalization of head needed rewriting on orthogonal higher-order rewrite systems which is an important feature of the rewriting strategy.