Completeness of narrowing in non-copying implementations

Narrowing provides an operational semantics for languages combining functional and logic programming. Unification and rewriting, the central operations in narrowing, are in practice often implemented on graph-like data structures in order to discard copying of subexpressions in favour of sharing subexpressions. This improves the efficiency of narrowing not only in space but also in time, since duplication of work in unification and rewrite steps is avoided. In this paper, we study the completeness of narrowing in non-copying implementations. We show by a counterexample that the well-known condition for the completeness of narrowing on trees, viz. a confluent and normalizing term rewrite relation, is not sufficient for non-copying implementations. Instead, one has to require that the implementing graph rewrite relation is confluent and normalizing. We provide completeness results for three narrowing strategies in non-copying implementations: minimally collapsing narrowing, maximally collapsing narrowing and basic narrowing. While minimally collapsing and basic narrowing are complete whenever the underlying graph rewrite relation is confluent and normalizing, maximally collapsing narrowing requires confluence and termination. Our result on basic narrowing improves (and corrects) a recent result of Krishna Rao which requires that rewrite rules are right-linear. (orig.)SIGLEAvailable from TIB Hannover: RO 8347(1997,19) / FIZ - Fachinformationszzentrum Karlsruhe / TIB - Technische InformationsbibliothekDEGerman