NV-Sequentiality: A Decidable Condition for Call-by-Need Computations in Term-Rewriting Systems
Michio Oyamaguchi · SIAM Journal on Computing · 1993
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 an arbitrary left-linear system is NV-sequential.