Strong Sequentiality of Left-Linear Rewrite Systems

Confluent term rewriting systems can be seen as a model for functional computations, in which redexes corresponding to instances of left hand sides of rules are repeatedly replaced by their corresponding right hand side instance. Lazy sequential strategies reduce a given redex in a term if and only if this redex must be reduced by any other sequential strategy computing the normal form of the term. Lazy strategies always terminate when a normal form exist, and are indeed optimal. In a landmark paper, Huet and Levy showed that such a strategy always exists for left linear non-overlapping rewrite systems that are {\em strongly sequential}, a property that they proved decidable for such systems. This paper generalises the result to the case of left-linear, possibly overlapping rewrite systems.

full paper