\documentclass[a4paper]{article}
\usepackage{amssymb}
\pagestyle{empty}
\hoffset=-40pt
\voffset=-20pt
\textwidth 15.3cm
\textheight 22cm % to fit our printers

\begin{document}

\begin{center}{\huge 
Ordinal Terms as a Tool for the Classification of Computational Complexity
}\end{center}
\begin{center}{\large Adam Cichon}\end{center}
\begin{center}{\large Nancy}\end{center}

\bigskip
\large

	Proving termination of a rewrite system means 
establishing the well-foundedness of the induced
rewrite ordering. This problem is undecidable in general 
and so one cannot hope to characterise this
class of orderings completely. We are thus led naturally 
to investigations which attempt to
characterise ``large'' subclasses of these orderings. A 
syntactic approach based on Kruskal's
theorem has given rise to mechanisable methods with the 
definition of recursive path orderings. But
it is now known that the Multiset Path Ordering and 
Lexicographic Path Ordering, the main examples
of recursive path orderings, are restrained to primitive 
recursive and multiply recursive derivation
lengths respectively.

	An alternative method of proving termination of 
rewrite systems is by means of interpretations.
This consists in the assignment, to each symbol occurring 
in the rewrite system, of a monotonic
interpretation on a well-founded structure. In our case, 
we shall be concerned with interpretations on
natural numbers. We shall see that this gives information 
on the computational complexity of the
system in bounding derivation lengths. The problem is, 
however, that there is no general deterministic
method for defining suitable interpretations. Most of 
the time one has to guess. A natural question
arises: how can we rationalise this task ?

	We describe here how one can exploit subrecursive 
hierarchies of functions indexed by ordinals for
the termination problem. The main examples of such hierarchies 
are the {\em slow-growing hierarchy},
the {\em fast-growing hierarchy} and the {\em Hardy hierarchy}. 
Here we concentrate on the use of
the Hardy hierarchy where, in order to increase the applicability 
of standard hierarchy results, we are
led to introducing a flexible approach to developing ordinal 
notations.

\end{document}