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

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.