A refinement of strong sequentiality for term rewriting with constructors (Q1093366)

The paper introduces a refined version of strong sequentiality for term rewriting systems, and this version is called left sequentiality. The difference is that left sequentiality is based on possible rather than arbitrary sequences of reductions. The results of the paper indicate that the left and strong sequentiality coincide when considered as properties of admissible sets of left-hand sides for systems of equations, but that left sequentiality is more general when applied to individual terms. It is shown that, improving on Huet and Levy's result, there is no redex selection algorithm which is safe for all systems based on a set of left- hand sides if that set is not left sequential.