Call by need computations to root-stable form
Call by need computations to root-stable form
复制标题
按需要计算调用根稳定形式
DOI：
10.1145/263699.263711
复制
发表时间：
1997
期刊：
影响因子：
--
通讯作者：
A. Middeldorp
中科院分区：
文献类型：
--
作者：
A. Middeldorp
Huet和Lévy的以下理论构成了所有结果的基础，以正交术语重写系统的最佳减少策略：每个术语不以正常形式以正常形式包含所需的REEX，并且需要重复的所需ReexES以正常形式产生术语，如果该术语均为术语。考虑到我们将这种理论推广到根稳定的形式，我们认为，在无限制正常化方面，产生的根含量概念比（其他变体）更基本。
The following theorem of Huet and Lévy forms the basis of all results on optimal reduction strategies for orthogonal term rewriting systems: every term not in normal form contains a needed redex, and repeated contraction of needed redexes results in the normal form, if the term under consideration has one. We generalize this theorem to computations to root-stable form and we argue that the resulting notion of root-neededness is more fundamental than (other variants of) neededness when it comes to infinitary normalization.