\documentclass{rtaloop}
\rtalabel{graph-orderings}


\begin{document}
\begin{problem}{D. Plump, Bruno Courcelle}{}{June 1993, January 1998}

\begin{abstract}
  How can termination orderings for term rewriting be adapted to cover
  those cases in which graph rewriting is terminating although term
  rewriting is not?
\end{abstract}

Graph rewriting systems that implement term rewriting systems (see, for
example, \cite{BEGKPS87:pal}\cite{HP91:rairo}) are terminating whenever term
rewriting is. The converse, however, does not hold \cite{P91:ctrs}. How can
termination orderings for term rewriting be adapted to cover those cases in
which graph rewriting is terminating although term rewriting is not?

It would be interesting to see an example not too artificial where the
termination proof is difficult. Graph rewriting systems implementing term
rewriting do not duplicate subgraphs. So the major source of difficulty in
termination proofs disappears.

\begin{submitted}{Klaus Guenter Dabisch}{Mon Mar  9 13:44:57 MET 1998}

This problem was solved intuitively in \cite{Ohlebusch97alp}. One could solve
the difficult termination proofs in this way: The Gross-Knuth reduction is
defined by: Contract all redexes simultaneously \cite{BEGKPS87:pal}. Then,
however, one has to prove that the result is unequivocal.

\end{submitted}

\end{problem}
\end{document}