Lecture Notes in Computer Science, 2002, Volume 2441/2002, 198-211, DOI: 10.1007/3-540-45788-7_12

Descendants and Head Normalization of Higher-Order Rewrite Systems

Hideto Kasuya, Masahiko Sakai and Kiyoshi Agusa

View Related Documents

Abstract

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.

Fulltext Preview

Image of the first page of the fulltext document