|
Abstract : |
Abstract. Dealing properly with sharing is important for expressing some of the common compiler optimizations, such as common subexpressions elimination, lifting of free expressions and removal of invariants from a loop, as source-to-source transformations. Graph rewriting is a suitable vehicle to accommodate these concerns. In [4] we have presented a term model for graph rewriting systems (GRSs) without interfering rules, and shown the partial correctness of the aforementioned optimizations. In this paper we define a different model for GRSs, which allows us to prove total correctness of those optimizations. Differently from [4] we will discard sharing from our observations and introduce more restrictions on the rules. We will introduce the notion of Bohm tree for GRSs, and show that in a system without interfering and non-left linear rules (orthogonal GRSs), Bohm 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 Bohm tree. We will also show that orthogonal GRSs are a correct implementation of orthogonal TRSs. The basic idea of the proof is to show that the behavior of a graph can be deduced from its finite approximations, that is, graph rewriting is a continuous operation. Our approach differs from that of other researchers [6, 9], which is based on infinite rewriting. 1, |
