We consider a number of problems which arise when performing term rewriting in algebraic specifications with each operator having an evaluation strategy for its arguments. Each problem is illustrated with an OBJ3 example. We propose a solution developed for the evaluation of functional modules in the Maude interpreter which is based on maintaining an invariant on the term graph by copying subgraphs where necessary. An executable Maude specification of this technique is presented.
(BibTeX entry) (gzip'ed Postscript)