Solving Equations by Graph Transformation
Annegret Habel, Detlef Plump · Electronic Notes in Theoretical Computer Science · 2002
We review the concept of term graph narrowing as an approach for solving equations by transformations on term graphs. Term graph narrowing combines term graph rewriting with first-order term unification. This mechanism is complete for all term rewriting systems over which term graph rewriting is normalizing and confluent. This includes, in particular, all convergent term rewriting systems. Completeness means that for every solution of a given equation, term graph narrowing can find an equivalent or more general solution. 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.