c Cambridge University Press Term Graph Narrowing

We introduce term graph narrowing as an approach for solving equations by transformations on term graphs. Term graph narrowing combines term graph rewriting with rst-order term unication. Our main result is that this mechanism is complete for all term rewriting systems over which term graph rewriting is normalizing and con uent. This includes, in particular, all convergent term rewriting systems. Completeness means that for every solution of a given equation, term graph narrowing can nd a more general solution. The general motivation for using term graphs instead of terms is to improve eciency: sharing common subterms saves space and avoids the repetition of computations. 1