Descendants and Head Normalization of Higher-Order Rewrite Systems
Descendants and Head Normalization of Higher-Order Rewrite Systems
复制标题
高阶重写系统的后代和头标准化
DOI：
10.1007/3-540-45788-7_12
复制
发表时间：
2002
期刊：
影响因子：
--
通讯作者：
K. Agusa
中科院分区：
文献类型：
--
作者：
H. Kasuya;Masahiko Sakai;K. Agusa
本文描述了一个扩展的标题需要重写的长期重写系统的高阶重写系统。这种推广的主要困难是由高阶约化导出的β约化引起的。为了克服这个困难，我们定义了一个新的后代高阶重写系统。本文给出了正交高阶重写系统上后代的新定义、性质和头需要重写的头规范化。
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.