\documentclass{rtaloop}
\rtalabel{Hardy}


\begin{document}
\begin{solvedproblem}{Andreas Weiermann}{}{April 1995}

\begin{abstract}
  Is it possible to bound the derivation lengths of simply terminating
  rewrite systems by a multiply recursive function?
\end{abstract}
If the termination of a finite rewrite system over a finite signature
can be proved using a simplification ordering, then the derivation
lengths are bounded by a Hardy function of ordinal level less than the
small Veblen number $\phi_{\Omega^\omega}0$.  (See
\cite{Weiermann:jsc}.)  Is it possible to lower this bound by
replacing the Hardy function by a slow growing function?  That is, is
it possible to bound the derivation lengths by a multiply recursive
function?

\begin{remark}
H\'el\`ene Touzet \cite{Touzet:thesis} has shown in her thesis that the answer
is negative, exhibiting a simplifying rewrite system which has derivation
bounds "longer" than multiply recursive. This work leaves open the question
about what complexity can be achieved using simpifying rewrite systems. An
improved version of the proof is given in \cite{touzet98}.

In \cite{touzet99rta}, Touzet has shown that for any multiple recursive
function $f$ there is a simplifying string rewriting system whose derivation
length function dominates $f$.

The complete solution to the problem is contained in \cite{lepper:04}, where
it is shown that the upper bound from Weiermann is tight, hence for any Hardy
function $h$ of ordinal level below the small Veblen ordinal there is a
simplifying term rewrite system whose derivation length function dominates $h$
(see also \cite{lepper:phd}).
\end{remark}

\end{solvedproblem}
\end{document}