NV-Sequentiality: A Decidable Condition for Call-by-Need Computations in Term-Rewriting Systems
NV-Sequentiality: A Decidable Condition for Call-by-Need Computations in Term-Rewriting Systems
复制标题
NV 顺序性：术语重写系统中按需调用计算的可判定条件
DOI：
10.1137/0222010
复制
发表时间：
1993
期刊：
影响因子：
--
通讯作者：
M. Oyamaguchi
中科院分区：
文献类型：
--
作者：
M. Oyamaguchi
1979年，Huet and Levy引入了一类顺序术语培训系统，在该系统中，可以有效地找到了一个称为强序的系统，在该系统中，可以有效地找到了称为强序列系统的子类，并定义了称为强顺序系统的子类[计算逻辑的一章：纪念Alan Robinson，J.-L。的论文Lassez和G. Plotkin，编辑，MIT Press，剑桥，马萨诸塞州，1991年]。本文引入了一个较大的子类，该子类是强序性的自然扩展，并基于对系统的左侧和一部分（即，不可变化部分）的分析，而强的顺序是基于的。单独分析左侧。这个新的顺序称为NV序列。结果表明，（i）NV序列系统的类别正确地包括了强序系统的类别，（ii）存在一种算法，用于在系统为NV序列时查找所需的redexes，以及（iii）是否可以决定...
In 1979 Huet and Levy introduced the class of sequential term-rewriting systems in which call-by-need computations are possible (without look-ahead) and defined the subclass called strongly sequential systems for which needed redexes in a given term are effectively found [chapter in Computational Logic: Essays in Honor of Alan Robinson, J.-L. Lassez and G. Plotkin, eds., MIT Press, Cambridge, MA, 1991]. This paper introduces a larger subclass that is a natural extension of strong sequentiality and is based on the analysis of both the left-hand sides and part of the right-hand sides (i.e., the nonvariable parts) of systems, whereas strong sequentiality is based on the analysis of left-hand sides alone. This new sequentiality is called NV-sequentiality. It is shown that (i) the class of NV-sequential systems properly includes the class of strongly sequential systems, (ii) there exists an algorithm for finding needed redexes for a given term when a system is NV-sequential, and (iii) it is decidable whether a...