\section{ An Example: A Graph Rewriting System for Combinatory Logic}
\label{crs}
Given the TRS rule 
${\sf F}(x) \reduce{}{} {\sf G}(x, x)$,
the term ${\sf F}({\sf +}({\sf 2},{\sf 3}))$
can be rewritten to
${\sf G}({\sf +}({\sf 2},{\sf 3}),{\sf +}({\sf 2},{\sf 3}))$.
That is, the term ${\sf +}({\sf 2},{\sf 3})$
is substituted for each occurrence of
the variable $x$ on the right-hand side of the above rule, and is
thus, {\it duplicated}. A graph rewriting system
avoids this duplication of work
by substituting a {\it pointer} to ${\sf +}({\sf 2},{\sf 3})$
for each reference to variable $x$, as depicted below:
\vspace{-0.1in}
\begin{center}
%\epsf{graphred1.ps}
\epsffile{graphred1.ps}
\end{center}
\vspace{-0.2in}
Our formalism for expressing graph rewriting
is based on the observation that
a natural way to represent a graph textually is to associate an
identifier to each node of the graph,
and then write down all the interconnections as a
{\it recursive let-block}.
Equivalently we can say that we associate a name to each
subexpression of a term.
For example, the above term ${\sf F}({\sf +}({\sf 2},{\sf 3}))$ 
will be expressed as
\[
\{ \begin{array}[t]{l}
t_1 = {\sf +}({\sf 2},{\sf 3});\\
t_2 = {\sf F}(t_1);\\
\;\; {\sf In} \; t_2 \} \enspace .
\end{array}
\]
In applying the above rule, the name $t_1$, and not
the expression ${\sf +}({\sf 2},{\sf 3})$, will be substituted for each
occurrence of $x$, leading to the term
\[
\{ \begin{array}[t]{l}
t_1 = {\sf +}({\sf 2},{\sf 3});\\
t_2 = {\sf G}(t_1,t_1);\\
\;\; {\sf In} \; t_2 \} \enspace .
\end{array}
\]
The substitution of an expression such as
${\sf +}({\sf 2},{\sf 3 })$ is not permitted to avoid duplication of work.
Only when ${\sf +}({\sf 2},{\sf 3})$ becomes a {\it value}, \ie ${\sf 5}$,
it can
be substituted for each free occurrence of $t_1$. 
Therefore, we think that an {\it  essential
feature of a language to model sharing is a recursive let-block construct with a
suitable notion of substitutable values}. 

The syntax of GRS terms is given in Figure \ref{crstermsyntax}.
\begin{figure}[htbp]
\centering{
\begin{tabular}{|l|} \hline
\\
$\begin{array}{lll}
S\!E & \in  & \mbox{Simple Expression} \\
E & \in  & \mbox{Expression} \\
{\sf F}^k & \in & {\cal F}^k \\
Constant  & \in & {\cal F}^0   \\
\end{array}$ \\
\\
$\begin{array}{llll}
S\!E & ::= & Variable  \mid Constant \\
E &::=& {S\!E} \\
& \;\;\mid  &   {\sf F}^k \; (S\!E_1, \cdots , S\!E_k)  \\
&\;\; \mid  &  Block \\
& \;\; \mid & \Omega \\
Block & ::= & \{  \; [Binding;]^* \mbox{  } {\sf In} \mbox{  } S\!E
\}   \\
Binding &::= & Variable = E \\
Term &::=& E \\
\end{array} $ \\
\\ \hline
\end{tabular}
}
\\
\caption{Syntax of terms of a GRS with signature ${\cal F}$}  
\label{crstermsyntax} 
\end{figure}
Superscript on a function symbol indicates its
``arity'' \ie the number of arguments it is supposed to have;
constants are assumed to be function symbols of arity 0.
Throughout this paper we consider constants to be (in implementation
parlance) ``unboxed". Thus, they are never shared and are freely substitutable.
``Boxed" values can be modeled in a straightforward manner by wrapping a
function symbol of arity one (say, called Box) around a value.
The textual order of bindings in a block is not relevant,  and the variable names 
on the left-hand side in a block must be pairwise distinct. 
Furthermore, for technical convenience we make a stronger
assumption, that is, no variable name can be defined more than once
regardless of its lexical level.
$\Omega$ is a special term whose significance 
will become clear when we formally define the notion of a redex
in Section \ref{formalGRS}.
Next we informally present  the GRS for combinatory logic, and relate
our GRS notation to Barendregt's \cite{Barendregt87c}.

\begin{figure}[htbp]
\centering{
\begin{tabular}{|l|} \hline
%\epsf{ctrsrule.ps}
\epsffile{ctrsrule.ps}
\\
\hline
\end{tabular}
}
     \caption{
        \label{graph}
         Graph rule for the {\sf S} combinator
             } 
\end{figure}

\label{rules}
Consider the ${\sf S}$ rule:
\[ {\sf Ap} \;
( {\sf Ap} \;( {\sf Ap} \;( {\sf S},\; x), \; y), \;z) \;\;
\reduce{}{} \;\;
{\sf Ap} \;( {\sf Ap} \;( x, \; z), \;{\sf Ap}\;(y, \;z)) \]
which is shown in Barendregt {\it et al}. graph notation
in Figure  \ref{graph}.
Intuitively, applying this rule consists of allocating three new
nodes, $root_r'$, $n_1'$ and $n_2'$, corresponding to
$root_r$, $n_1$ and $n_2$, respectively, ({\it build phase})
and redirecting all the
pointers to the redex node (\ie the node matching $root_l$)
to the node $root_r'$ ({\it redirection phase}).
Notice that the redirection phase does not affect the graph
matching the subgraph $g$ $\equiv$
${\sf Ap}\; ({\sf Ap} \;( {\sf S},\;x),\;y)$
(included in dotted lines in Figure \ref{graph}), thus  we
call the subgraph $g$ the {\it precondition} of the above rule.  In
order to represent the right-hand side (\ie rhs) of the S rule textually
we simply write down the graph rooted at
$root_r$ as a recursive let-block. 
Thus, the ${\sf S_g}$ rule, that is, the S rule in GRS
notation, can be written as follows:
\[  \frag{
x_1   =   {\sf Ap}\;(x_2, \; z_2) \;\;  ; \;\;
x_2  =  {\sf Ap}\; ({\sf S}, \; z_3)}
{
x={\sf Ap}\;(x_1, \; z_1 )\;\; \reduce{}{} \;\; 
x=\{ \begin{array}[t]{lll}
t_1 & = & {\sf Ap} \; (z_3, \; z_1);\\
t_2 & = & {\sf Ap} \; (z_2, \; z_1);\\
t & = & {\sf Ap} \; (t_1, \; t_2);\\
\multicolumn{3}{l}{
\;\;\; {\sf In} \; t  \} }
\end{array} } \enspace . \]

\noindent
Variables, such as $t_1, t_2$ and $t$, that occur on the rhs of the rule but not on the
lhs or in the precondition, generate new corresponding variables for each application of the rule.

\noindent
Similarly the ${\sf K_g}$ rule, that is, the ${\sf K}$ rule in GRS notation is
expressed as follows: 
$$ \frag{ \begin{array}{lll}
x_1 & = & {\sf Ap}\; ({\tt K}, \; z_2)  \\
\end{array}}
{
x={\sf Ap}\;(x_1, \; z_1 )\;\; \reduce{}{} \;\;  x=z_2 } \enspace . $$

\begin{figure}[htbp]
\centering{
\begin{tabular}{|l|} \hline
%\epsf{graphexample1.ps} 
\epsffile{graphexample1.ps} 
\\
\begin{minipage}{6.2in}
$ \{\begin{array}[t]{l}
\multicolumn{1}{l}{
\framebox[3.5cm]{$ \begin{array}{l}
w_1  =  {\sf Ap}\;({\sf S},\;{\sf P});\\
w_2  =  {\sf Ap}\;(w_1,\;{\sf Q});
\end{array}$}}\\
w_3  =  \underbrace{{\sf Ap}\;(w_2,\;{\sf R});}_{\rho}\\
w_4  =  {\sf G}\;(w_1,\;w_3);\\
\multicolumn{1}{l}{
\;\;\;{\sf In} \; w_4 \}}
\end{array} \!\!
\reduce{w_3}{} 
M_1 \equiv \begin{array}[t]{l}
\{w_1  =  {\sf Ap}\;({\sf S},\;{\sf P});\\
\;\;w_2  =  {\sf Ap}\;(w_1,\;{\sf Q});\\
\;\;w_3  = \{
\begin{array}[t]{l}
t_1'  =  {\sf Ap}\;({\sf P},\;{\sf R});\\
t_2'  =  {\sf Ap}\;({\sf Q},\;{\sf R});\\
t'  =  {\sf Ap}\;(t_1',\;t_2');\\
\multicolumn{1}{l}{
\;\;\;{\sf In} \; t' \}}
\end{array} \\
\;\;w_4  =  {\sf G}\;(w_1,\;w_3);\\
\multicolumn{1}{l}{
\;\;\;{\sf In} \; w_4 \}}
\end{array} \!\!  \equiv_{\alpha} \!\!
\begin{array}[t]{l}
\{ w_1  =  {\sf Ap}\;({\sf S},\;{\sf P});\\
\;\;w_2  =  {\sf Ap}\;(w_1,\;{\sf Q});\\
\;\;t_1'  =  {\sf Ap}\;({\sf P},\;{\sf R});\\
\;\;t_2'  =  {\sf Ap}\;({\sf Q},\;{\sf R});\\
\;\;t'  =  {\sf Ap}\;(t_1',\;t_2');\\
\;\;w_4  =  {\sf G}\;(w_1,\;t');\\
\multicolumn{1}{l}{
\;\;\;{\sf In} \; w_4 \}}
\end{array}   \!\! \equiv_\alpha  \!\!
\begin{array}[t]{l}
\{w_1  =  {\sf Ap}\;({\sf S},\;{\sf P});\\
\;\;t_1'  =  {\sf Ap}\;({\sf P},\;{\sf R});\\
\;\;t_2'  =  {\sf Ap}\;({\sf Q},\;{\sf R});\\
\;\;t'  =  {\sf Ap}\;(t_1',\;t_2');\\
\;\;w_4  =  {\sf G}\;(w_1,\;t');\\
\multicolumn{1}{l}{
\;\;\;{\sf In} \; w_4 \}}
\end{array}
$
\end{minipage}
\\ \hline
\end{tabular}
}
     \caption{
        \label{graphexample}
             Graph reduction and its corresponding GRS reduction 
             }
\end{figure}


In Figure \ref{graphexample} we show the graph reduction
in Barendregt notation and our notation using
the following term:
\[ M \equiv \{\begin{array}[t]{lll}
\multicolumn{3}{l}{
\framebox[4cm]{$ \begin{array}{lll}
w_1 & = & {\sf Ap}\;({\sf S},\;{\sf P});\\
w_2 & = & {\sf Ap}\;(w_1,\;{\sf Q});
\end{array}$}}\\
w_3 & = & \underbrace{{\sf Ap}\;(w_2,\;{\sf R});}_{\rho}\\
w_4 & = & {\sf G}\;(w_1,\;w_3);\\
\multicolumn{3}{l}{
\;\;\;{\sf In} \; w_4 \} \enspace . } 
\end{array} \] 



\noindent
Intuitively, the two bindings in the box inside $M$ match the precondition and the subterm $\rho$ matches the lhs of the ${\sf S_g}$ rule according to the following
substitution:
\[ x=w_3, \; x_1 = w_2,\;x_2=w_1,\;z_3={\sf P},\;z_2={\sf Q},\;z_1={\sf R} 
\enspace . \]
\noindent
Since $w_3$ corresponds to $x$, it is called the root of the redex.
Using the above substitution an instance of the rhs of the ${\sf S_g}$
rule is created. It introduces fresh copies for the bound variables of
the rhs of the ${\sf S_g}$ rule.  This step corresponds to the {\it
build phase} of the Barendregt system. Subsequently, variable $w_3$ is
bound to the newly instantiated term. Thus obtaining $M_1$.  This
rebinding of $w_3$ corresponds to the {\it redirection phase} in
Barendregt.  $M_1$ is then {\it canonicalized} by flattening blocks
and substituting variables and constants in $M_1$.  The introduction
of fresh variables during the instantiation of the rhs of a rule
removes the need to rename variables when blocks are flattened.  There
is one more step called the {\it garbage collection}, that is, the
deletion of nodes that are not reachable from the root.  Thus, the
definition of variable $w_2$ is eliminated because it is no longer
reachable from node $w_4$.  The term $M$ is said to rewrite to the
final term so obtained.  Notice that the final term is indeed the term
corresponding to the rightmost graph in Figure \ref{graphexample}.

There is, however, a subtle difference between the two systems which shows up
in the presence of ``projection'' rules and cyclic graphs.
For example, given the rule $x={\sf I}(y) \reduce{}{} x=y$,
and the cyclic term $M \equiv \{ t={\sf I}(t); \; {\sf In} \; t \}$,
$M \reduce{}{} M$, following the Barendregt system,
while
$M \reduce{}{} \{ t = t; \; {\sf In } \; t \}$,
following our system. As
explained later
$\{ t = t ; \; {\sf In} \; t \}$ becomes {\bf $\odot$}, a symbol
which represents a ``meaningless'' term.
This difference has a strong impact on the confluence
of GRSs. We will further clarify these issues after 
introducing GRSs formally in Section \ref{formalGRS}. 
