\section{Introduction}

Sharing of subexpressions is of utmost importance in the
implementation of functional languages.  Consider the function
definition ${\sf F} \; x = x + x$ and the expression ${\sf F}(2+3)$.
Any decent implementation, independently of the evaluation strategy
(normal-order or applicative-order) it employs, will evaluate the
subexpression $2+3$ only once.  Several compiler optimizations are
about increasing the sharing of subexpressions to avoid their repeated
evaluation.  In this paper, we discuss the syntactic and semantic
properties of a calculus, which is adequate for capturing the sharing
of subexpressions in first-order functional languages.  The results of
this paper are also relevant to compiling higher-order functional
languages, because compilers of such languages often employ a
technique known as ``lambda-lifting" \cite{Johnsson85}.
The program that results after
lambda-lifting is in a ``supercombinatory" form, and is treated as a
first-order program \cite{Hughes82}.

A way to capture sharing is to represent the expression as a graph
instead of a linear text string or tree.  This allows sharing of
identical terms through pointers, and avoids repeated evaluation of
identical terms as it is commonly done in normal-order reduction.
Graph reduction for the $\lambda$-calculus was proposed by Wadsworth
in order to bring together the advantages of both the applicative and
the normal order evaluation \cite{Wadsworth}.  Wadsworth also formally
proved the correctness of his graph reduction technique. As an
aside, Wadsworth also showed that his graph reduction did not capture
enough sharing to lead to an optimal interpreter.  More recently a new
graph structure, which allows sharing of ``{\it contexts}'', has been
proposed in \cite{Vinod90,Lamping90}.  This latter technique leads to
provably optimal interpreters for the $\lambda$-calculus
\cite{Levy78b}.  In this paper, however, we are not concerned with
optimality questions, and we restrict our attention to
``argument sharing'' in a language which is simpler 
than the $\lambda$-calculus.

Much of the past work on graph rewriting has been to prove its
correctness with respect to either the $\lambda$-calculus
\cite{Wadsworth} or Term Rewriting Systems
\cite{Dutch86,Barendregt87c,Bru87,Kennaway90}.  In contrast, this
paper explores graph rewriting as a system in its own right, and makes
no attempt to prove the correctness of a graph implementation with
respect to a ``tree (or unshared) view" of the computation.  Motivated
by what we have observed in real implementations of functional
languages, we explore syntactic and semantic properties of graphs with
cycles, and rewriting rules that recognize or create cycles.  In this
respect our calculus goes farther than either \cite{Wadsworth} or
\cite{Barendregt87c} where only acyclic graphs are considered.
Without cyclic graphs some important implementation ideas are ruled
out.  More recently, Klop {\it et al}. \cite{Klop91} have extended the
Barendregt's graph rewriting system to deal with cycles. However,
their approach is significantly different from ours in that they model
cyclic graph rewriting as ``transfinite reduction'' of infinitary
graph terms.

In the following, we formally introduce a Graph Rewriting System
(GRS). The basic feature of a GRS is the {\it block} construct, \ie
{\it letrec}. A block in a GRS is not treated as syntactic sugar for
application; it is central to expressing the sharing of
subexpressions. Our GRS includes cyclic terms and permits both {\em
non-left-linear rules} and {\em left-cyclic rules}.  We prove that in
the absence of {\em interfering rules} a GRS is confluent.  This is a
more general result than the confluence theorem in \cite{Klop91}.  We
think that our approach also leads to a simpler proof of confluence
than in \cite{Klop91}.

We also develop a term model for a GRS without interfering rules along
the lines of L\'evy's term model for the $\lambda$-calculus.  We
introduce the notion of ``information content" associated to a term,
and show that the information content defines a congruence on the set
of terms. This result can be applied in a straightforward manner to
show the partial correctness of those optimizations that simply
increase the sharing in a term. An example of such an optimization is
the common subexpression elimination.  Moreover, the result implies
the partial correctness of the cyclic implementation of the ${\sf
Y}$-rule.

The paper is organized as follows: In Section \ref{crs}, we introduce
graph rewriting taking combinatory logic as an example, and compare our
notation with that of Barendregt's \cite{Barendregt87c}.
We formally describe GRSs, in Section \ref{formalGRS}.
We introduce an
ordering on terms based on sharing of subterms, and formulate the
notion of a redex using this ordering.  In Section
\ref{orthogonal}, we introduce GRSs without interfering rules and
prove their confluence. Section \ref{equivalence} gives a term model
for non-interfering GRSs.  In Section \ref{opti}, we
apply the results of Section \ref{equivalence} to prove the
correctness of some compiler optimizations, while in Section
\ref{conclusions} we discuss directions for future work.
