A class of ambiguous linear term‐rewriting systems on which call‐by‐need is a normalizing reduction strategy

Tohru Naoi, Masafumi Yamashita, Toshihide Ibaraki, Namio Honda

Research output: Contribution to journalArticle


The term‐rewriting system is of a recent concern, since there can be various applications, including the execution mechanism for the programming language based on the equality. However, in its application there must be a normalizing reduction strategy, which ensures that the normal form can always be reached if the given term has a normal form. Huet and Lévy proposed the call‐by‐need strategy as a normalizing reduction strategy for unambiguous linear term‐rewriting systems. This paper extends their result to the case containing ambiguity. A sufficient condition is shown first for the call‐by‐need in a linear term‐rewriting system containing ambiguity to be a normalizing reduction strategy. The condition properly includes the result of Huet and Lévy. Then considering an arbitrary linear term‐rewriting system, in which the call‐by‐need is a normalizing reduction strategy, a condition is presented under which a new rewriting rule can be added, while retaining the properties. Combining the result with the previous result, a wider class of ambiguous term‐rewriting system is obtained in which the call‐by‐need is a normalizing reduction strategy.

Original languageEnglish
Pages (from-to)19-30
Number of pages12
JournalSystems and Computers in Japan
Issue number9
Publication statusPublished - Jan 1 1987


All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Information Systems
  • Hardware and Architecture
  • Computational Theory and Mathematics

Cite this