Complete Strategies for Term Graph Narrowing

Abstract. Narrowing is a method for solving equations in the equational theories of term rewriting systems. Unification and rewriting, the central operations in narrowing, are often implemented on graph-like data structures to exploit sharing of common subexpressions. In this paper, we study the completeness of narrowing in graph-based implementations. We show that the well-known condition for the completeness of tree-based narrowing, viz. a normalizing and confluent term rewrite relation, does not suffice. Completeness is restored, however, if the implementing graph rewrite relation is normalizing and confluent. We address basic narrowing and show its completeness for innermost normalizing and confluent graph rewriting. Then we consider the combination of basic narrowing with two strategies for controlling sharing, obtaining minimally collapsing and maximally collapsing basic narrowing. The former is shown to be complete in the presence of innermost normalization and confluence, the l...

• Type: Conference
• Year: 1998
• Where: WADT
• Authors: Annegret Habel, Detlef Plump
• Keywords: Basic Narrowing, Narrowing, Software Engineering, Tree-based Narrowing, WADT 1998