\newcommand*{\tpkt}{\rlap{$\;$.}}
\newcommand*{\tkom}{\rlap{$\;$,}}

\section{Complexity} \label{sec:complex}

%successful start of new category.

% may turn out important for applications
% (because in so-called reality, Ackermann is equivalent to non-termination).

% Basic methods are in place:
% upper triangular standard matrix interpretations give polynomial bound,
% arctic and matchbound interpretations give linear bound.

% different performance of implementations only due to
% technicalities (bit widths, search order etc.)

% this is an invitation to come up with substantially fresh methods.

% other extensions: 
% \begin{itemize}
% \item larger complexity classes (e.g. exponential, elementary, primitive recursive)
% \item lower bounds (e.g. give families of derivations that witness certain derivation lengths)
% \item certification
% \end{itemize}


In this year's termination competition for the first time a 
\emph{complexity category} was present. 
It is a  challenging topic to automatically determine  upper bounds on
the complexity of rewrite systems.  Here complexity is measured as the
maximal  length of derivations,  where either  no restrictions  on the
initial   terms  are   present  (\emph{derivational   complexity})  
or  only constructor   based  terms   are   considered  
(\emph{runtime complexity}).
Additionally  one distinguishes between  complexities induced  by full
rewriting as  opposed to complexities induced  by specific strategies,
as for example innermost rewriting. 
%
In this year this variety was represented trough four sub-categories:
\emph{derivational complexity}--\emph{full rewriting}, 
\emph{derivational complexity}--\emph{innermost rewriting},
\emph{runtime complexity}--\emph{full rewriting}, and
\emph{runtime complexity}--\emph{innermost rewriting}.

As test-bed we used the TRSs of the categories \emph{TRS Standard} and
\emph{TRS Innermost} where TRSs that occur in both categories where
considered once. For the sub-category 
\emph{derivational complexity}--\emph{full rewriting}, 
only \emph{non duplicating} systems were
tested as the current focus of the complexity category is on 
polynomial derivational/runtime complexity. 

As test-bed the collection of all ``standard'' TRSs together with
all TRSs with flag ``(STRATEGY INNERMOST)'' were used. Here TRSs in the current TPDB
which only differ by the flag  are only considered once.
However for the sub-category \emph{derivational complexity}--\emph{full rewriting}, 
only \emph{non duplicating} systems were tested as the current focus of the complexity category is on 
polynomial derivational/runtime complexity. 
%GM: die zahlen auf termcomp sind derzeit falsch (unter 'View Results'), werden
%aber korrigiert, die zahlen bei 'View Problems' enthalten *alle* TRS der TPDB
%und können (laut SB) derzeit nicht angepasst werden
%
In sum this amounts to 1404 examples for the full test-bed and 446
TRSs for the restricted test-bed.

In  the  sub-categories for derivational  complexity, 
$\CAT$ and $\TCT$ ran a  competition, which was won by $\CAT$. 
% We would like to take this  opportunity  to congratulate  the  $\CAT$  
% developers Martin  Korp, Christian  Sternagel  and  Harald  Zankl  
% to  this  victory.   
In  the sub-categories  for runtime  complexity,
$\TCT$ ran as a demonstration.

The most challenging part in the design of this category was the definition
of the competition semantics. While it was clear from the beginning that
the current focus should be on \emph{polynomial bounds}, it turned out to
be not so easy to suit the existing competition semantics suitably to complexity
analysers: while for the ``standard'' categories it has always been understood
that the power of a tool should be measured by the number of successful runs
the tool manages, the situation is not so clear for complexity analysis.
What is a ``successful run'', if the prover is supposed to measure the
complexity of a given TRS?

An ad-hoc solution would have been to test for polynomial bounds and
the competing tools simply answer ``yes'' if this bound is verified. 
However this somehow blurs the potential of complexity analysis and does not 
really represent the research in this area. Hence we decided to extend the output certificate so that
an (asymptotic) complexity function is rendered as output. Thus the tool providing 
the more accurate output (either as a lower or as an upper bound) should
be considered the winner for the specific TRS tested.

In this year's competition only upper bounds have been tested as not much is
currently known on how to (automatically) test for lower bounds on the complexity.
Still the output format is already equipped to handle such an analysis as well.
%
The following grammar is used:
%
\begin{align*}
  \mathsf{S} &\to \texttt{NO} \mid \texttt{MAYBE} \mid \texttt{YES}(\mathsf{F},\mathsf{F}) \mid
  \texttt{YES}(\texttt{?},\mathsf{F}) \mid \texttt{YES}(\mathsf{F},\texttt{?})  \\
  \mathsf{F} &\to \texttt{O}(1) \mid \texttt{O}(n^m)  \mid \texttt{POLY} \tkom
\end{align*}
%
where $m$ is a natural number.

As said, we currently focus on (polynomial) upper bounds.
Firstly, for each  TRS the competing tools are  ranked, where the
tool with the lowest upper bound wins with respect to the given TRS. For each
place in this ranking, points are given. Finally the obtained points are summed
up and the tool that achieved the most points in total wins the the competition, 
see~\url{http://termination-portal.org/wiki/Complexity} for more
details.
This more refined competition semantics caused some overhead
in its implementation, but it has proven its functionality in the execution.



Let us come back to the actual competition between $\CAT$ (short for Complexity And Termination)
and $\TCT$ (short for Tyrolean Complexity Tool). 
%
Both tools are partially built up on basic libraries of $\TTTT$ which explains
the common output format. Both tools implement direct termination methods, sometimes restricted, that
induce polynomial derivational complexity; for 
example \emph{match-bound techniques}, \emph{triangular matrix interpretations}, 
and \emph{root labeling} are implemented.

In addition $\CAT$ uses the \emph{arctic matrix method} as another
direct termination technique and $\TCT$
incorporates transformation techniques like
\emph{weak dependency pairs}, \emph{weak dependency graphs}, \emph{polynomial
path orders}, and \emph{finite semantic labeling}. 
%
Note that the mentioned transformation techniques are only used in the
sub-category ``runtime complexity''.
%
The main reason why $\CAT$ won amounts (i) to a cleverer strategy
that uses (triangular) matrix interpretations also for higher dimensions and 
(ii) the use of the arctic matrix method.


% In concluding we want to mention two observations of this competition that
% are perhaps of interest in the context of other categories of the competition as well.
% %
% First, although the more refined competition semantics caused some overhead
% in its implementation, it has proven its functionality in the execution. Moreover
% the ranking of tools provided excitement till the end. As better certificates
% are taken into account the race remains open longer, almost till the very end.
% %
% Second, it is perhaps of general interest that both tools are (partly) 
% open source under the GNU Lesser General Public License. In particular
% the sources of the competing tools are available via their respective
% web pages, see~\url{http://termination-portal.org/wiki/Category:Tools} for further details.


For the future it seems to be of utmost importance to increase the number of
participants. Moreover fresh methods are required in all sub-categories to
extend the number of TRSs that can be analysed, with respect to lower and upper
bounds, respectively. Clearly at the moment the TPDB is not an ideal test-bed
for complexity analysis, but we expect that this will change due to addition
of new examples to the TPDB in the course of future competitions. 

For the moment we suggest to keep the focus on \emph{polynomial} complexity analysis. Within
this focus there are still a vast number of challenging problems, foremost 
the proper incorporation of incremental termination techniques like the dependency
pair framework. Currently the extension to higher complexity classes and/or
certification, although envisaged, feels premature.

