Unification, Rewriting, and Narrowing on Term Graphs
Annegret Habel, Detlef Plump · Electronic Notes in Theoretical Computer Science · 1995
The concept of graph substitution recently introduced by the authors is applied to term graphs, yielding a uniform framework for unification, rewriting, and narrowing on term graphs. The notion of substitution allows definitions of these concepts that are close to the corresponding definitions in the term world. The rewriting model obtained in this way is equivalent to “collapsed tree rewriting” and hence is complete for equational deduction. For term graph narrowing, a completeness result is established which corresponds to Hullot's classical result for term narrowing. The general motivation for using term graphs instead of terms is to improve efficiency: sharing common subterms saves space and avoids the repetition of computations.