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