\section{Termination Problems}\label{sec:cat}

We give an overview of the kind of termination problems
that are present in the Termination Problem Data Base (TPDB), 
and are being used in competitions.

In the most general view, each entry in the data base
specifies a relation. The task of the termination prover
is to analyze this relation.

\subsection{Specifying Computations}

The relation describes one step of the computation 
in the following models:
\begin{itemize} \itemsep 1pt
\item a rewriting system (given by a set of rewrite rules),
\item a logic program (given in Prolog notation),
\item a functional program (given in Haskell notation).
\end{itemize}

These relations are classified  by additional criteria.
For term rewriting systems, 
we have the syntactic criterion on the signature:
\begin{itemize} \itemsep 1pt
\item string rewriting (all function symbols are unary),
\item term rewriting (arbitrary signatures).
\end{itemize}
Then, several variants are used
in defining the relation from the set(s) of rules.
The rewrite relation can be restricted by \emph{strategies}:
\begin{itemize} 
\item no strategy (reduce any redex),
% \item 
~ $\bullet$
  innermost,
% \item 
~ $\bullet$
  outermost,
\item context-sensitive (using replacement maps).
\end{itemize}
The relation can also be restricted by prescribing \emph{start terms}.
\begin{itemize} \itemsep 1pt
\item no restrictions,
\item start term is constructor-based. (The resulting complexity notion
  is called  \emph{run time} complexity.)
\item start term is a Prolog query, or a Haskell expression.
  (This is mandatory for the respective categories.)
\end{itemize}
The relation $\to_1$ defined by one set of rules 
can be combined with some other relation $\to_2$:
\begin{itemize} \itemsep 1pt
\item no combination (just one relation $\to_1$)
\item \emph{relative} rewriting: 
  consider $\to_1 \circ \to_2^*$,
\item \emph{equational} rewriting: 
  consider $\to_1 \circ \leftrightarrow_2^*$.

  In particular, $\leftrightarrow_2$ may encode commutativity,
  associativity or idempotency of function symbols,
  and this is called ``rewriting modulo theories''.
\end{itemize}

This gives a huge design space,
and not all combinations are actually present 
(and some would have no reasonable semantics).

\subsection{Properties of Computations}

For relations that are given by the above specifications,
two types of questions are considered by the provers:
\begin{itemize} \itemsep 1pt
\item \emph{Termination}: 
  there is no infinite derivation,
\item 
  for terminating relations, \emph{Derivational complexity}:
  the maximal length of a derivation, 
  as function of the size of the start configuration.
\end{itemize}
The answers produced by the provers (YES, NO, or complexity bounds)
are to be accompanied by a proof that is given in a form 
\begin{itemize} \itemsep 1pt
\item that can be verified by a mechanical proof checker,
\item or at least be believed after human inspection.
\end{itemize}
We remark that not all of the $2 \times 2$ combinations
of the above features do occur at present.
The ultimate goal is indeed that a prover's output
is as detailed as possible (i.e., it contains complexity information),
and as trustworthy as possible (i.e., mechanically verifiable)
but this is certainly a long-term process.

\subsection{Current Contents of TPDB}

The termination competition 2008 used version 5 
of the Termination Problems Data Base. 
Ignoring the refinements discussed above (strategies, theories, etc.)
its summarized contents is:
\begin{center}
\begin{tabular}{r||r|r|r|r}
combined categories & FP & LP & SRS & TRS \\ \hline
number of problems & 1676 & 351 & 777 & 2036 
\end{tabular}.
\end{center}
The data base is freely
available from \url{http://termination-portal.org/wiki/TPDB}.

