A Deterministic Lazy Narrowing Calculus

In this paper we study the non-determinism between the inference rules of the lazy narrowing calculus LNC(Middeldorpet al., 1996,Theoret. Comput. Sci.,167, 95–130. We show that all non-determinism can be removed without losing the important completeness property by restricting the underlying term rewriting systems to left-linear confluent constructor systems and interpreting equality as strict equality. For the subclass of orthogonal constructor systems the resulting narrowing calculus is shown to have the nice property that solutions computed by different derivations starting from the same goal are incomparable.