\section{Future directions}
\label{conclusions}
We have defined a class of GRSs which can express sharing of terms,
including cyclic terms. Our GRS admits both non left-linear and
left-cyclic rules.  We prove the confluence of GRS$_{\sf NI}$, that
is, a GRS with non interfering rules, and develop a term model a la
L\'evy for these GRS. Furthermore, we apply the semantic relation to
show the partial correctness of important optimizations such as the
common subexpression elimination and the cyclic implementation of the
${\sf Y}$-rule. The main advantage of our approach is its simplicity
because it avoids infinitary terms and associated transfinite
reduction.

The motivation for this work came from a desire to formalize the
compilation process of Id, an implicitly parallel language
\cite{Nikhil90c}.  Id has a purely functional, higher-order,
non-strict core. In addition Id also contains logical variables in the
form of I-structures and mutable variables in the form of M-structures.
The compiler of Id is expressed as a series of translations into
simpler and simpler languages.  In our prior work we have introduced
the Kid (Kernel id) language \cite{Zena91a} and the P-TAC (Parallel
Three Address Code) language \cite{Zena89}, and provided the
translation of Id into Kid and of Kid into P-TAC \cite{Zena92b}.  We
have tried to formalize many optimizations in the Id compiler in terms
of source-to-source transformations on these intermediate languages.

Functional subset of P-TAC can be seen as an example of the GRS
presented in this paper.  Functional Kid, however, is more general due
to the presence of $\lambda$-abstraction.  A model for a GRS with
$\lambda$-abstraction will provide a sound mathematical basis for the
functional subset of the
Id language. However, even proving confluence for the $\lambda$-calculus
with sharing is a difficult problem. 

Another direction of work would be to incorporate a notion of types, and
the distinction between strict and non-strict  operators in our GRS
framework. This will allow one to prove the correctness of 
compiler optimizations, such as the algebraic rules.

Yet another direction would be incorporate I-structures and M-structures
in our GRS. Elsewhere, we have shown the confluence of a GRS with I-structures \cite{Zena89}.
I-structures operations can be expressed  using ``multi-rooted rules''. 
However, a term model for a GRS with I-structures would require a very 
different treatment of unconnected subterms and garbage collection.



\section*{Acknowledgements}
This work was done at the Laboratory for Computer Science at MIT, and
at the University of Oregon. Funding for this work has been provided
in part by the Advanced Research Projects Agency of the U.S.
Department of Defense under the Office of Naval Research contracts
N00014-92-J-1310 (MIT)

We would like to express immense gratitude to
Jean-Jacques L\'evy, and  Jan Willem Klop for insightful
discussions. 

