Dealing properly with sharing is important for expressing some of the common compiler optimizations as source-to-source transformations, such as common subexpressions elimination, lifting of free expressions and removal of invariants from a loop. Term graph rewriting is a computational model to accommodate these concerns. In this paper we are interested in defining a term model for term graph rewriting systems, which allows us to prove total correctness of those optimizations. We introduce the notion of Böhm tree, and show that for orthogonal term graph rewriting systems, Böhm tree equivalence defines a congruence. Total correctness then follows in a straightforward way from showing that if a program M contains less sharing than a program N, then both M and N have the same Böhm tree.

Using Böhm trees we also show that orthogonal term graph rewriting systems are a correct implementation of orthogonal term rewriting systems. This boils down to showing that the behavior of a term graph can be deduced from its finite approximations, that is, graph rewriting is a continuous operation. Our approach differs from that of other researchers which is based on infinite rewriting.