\section{Comments from Termtools mailings (merge with other sections)}

(warning: raw form, needs editing)

\subsection{Loop detection:}

http://lists.lri.fr/pipermail/termtools/2008-November/000644.html

\emph{nonloop} by Martin Oppelt.

His program finds some cases of non-looping non-termination,
including the classical examples by Zantema/Geser,
like \verb|( RULES b a L -> L a L X b a b b  , b L -> L b )|,
submitted as \verb|SRS/oppelt/*|

As a side-effect, "nonloop" is quite good at finding loops as well.
E.g. it solves SRS/Waldmann07b/size-12-alpha-3-num-170.srs
which no-one could do last year.


\url{http://lists.lri.fr/pipermail/termtools/2008-November/000652.html}

Did \TTTT use the "SAT for loop-detection" idea this time?

Harald Zankl: Yes. All loops found within the DP-setting are due to this idea.
We just searched for looping reductions of lenth at most 20 where
all terms within the loop are at most of length 20. Probably other
configurations produce better results ...

\subsection{Double Complexity}

\url{http://lists.lri.fr/pipermail/termtools/2008-November/000667.html}


J: What I don't get is why all of a sudden
there are two competing complexity teams from the very same site
(same floor, even?). 

Georg:
That is very simple to answer: Chris, Harald, and Martin realised that 
it was very easy
for them to take a  subset of the \TTTT code and transform it into a 
complexity analyser.
And, apparently they did a good job.

When they informed me about this plan, I of course encouraged it. Actually
I would be very pleased, if all authors of termination provers think about
entering the complexity category with suitable adaptions of their tools.

J: How different are these implementations?
Perhaps the respective authors can enlighten us ... - Johannes.


G: Both tools are partially build up on basic libraries of \TTTT, that explains
for example the common output format. Moreover the tools have 
implemented triangular
matrices, match-bounds and root labeling. In addition CaT uses arctic 
matrix method and TCT
incorporates weak dependency pairs, weak dependency graphs, POP* and
finite semantic labeling.  The main reason why the CaT tool won is (i) a 
cleverer strategy
that uses (triangular) matrix interpretations for higher dimensions and 
(ii) arctic matrix method,
which I suppose will please you.

As indicated, both tools are open source, hence the source is available 
in the respective
web pages, available via the termination-portal since November 1, which 
also includes further documentation.

\subsection{Certified the proof but not the theorem?}

\url{http://lists.lri.fr/pipermail/termtools/2008-November/000649.html}

Olivier Pons: \dots the trs being
proved is not equivalent to the initial srs. This is due to an
ERRONEOUS VERSION OF OUR SRS PARSER. The proofs we generate are correct
but they prove the termination of a wrong trs.

\subsection{Is that even a TRS?}

\url{http://lists.lri.fr/pipermail/termtools/2008-November/000671.html}

J.W.: Matchbox just "proved" termination of
\begin{verbatim}
TRS/TRCSR/Ex1_2_Luc02c_L.trs = (VAR X Y  )
(RULES 2nd ( cons ( X ) ) -> Y  from ( X ) -> cons ( X ) )
\end{verbatim}
and of course Coq rejected that.

Somehow this restores my faith in verification,
and I'm happy to withdraw matchbox from the category.

\subsection{Complexity needs Certification?}

\url{http://lists.lri.fr/pipermail/termtools/2008-November/000692.html}
Georg: \dots found an embarrassing
mistake in \dots. Luckily the mistake can be easily
healed without major changes in the experimental data.

Still this influences the soundness of TCT on the subcategories for runtime
complexity and I would kindly ask for its disqualification.

\subsection{TTT2 Report}

\url{http://lists.lri.fr/pipermail/termtools/2008-November/000695.html}

Martin Korp:

Here is a short report on the performance of \TTTT at the recent
termination competition. \TTTT participated in two categories, SRS
standard and TRS standard, with two aims:

\begin{itemize}
\item to win the SRS category
\item to have a very fast but still powerful tool for the TRS category
\end{itemize}

Johannes already remarked that arctic matrices play an important role in
(1). \TTTT uses fewer techniques than AProVE, but we use matrices with
higher dimensions.

We are not sure about the outcome, if the best SRS tools of 2007
(Matchbox and TORPA) would have participated.

Concerning (2), we wanted to demonstrate that there is no need for a 60
seconds timeout. Running \TTTT at full power would have brought additional
TRSs, but still far short of AProVE's score.  We believe that some
measures are in order to encourage other tools to participate in the TRS
category.

Inspired by the observation that building a fresh tool (CaT, TCT) on an
existing tool (\TTTT) is considerably less work than starting from
scratch, one contribution we can (and will) do is to clean up the \TTTT
source and make it publicly available.

\subsection{Certified Report}

by Frederic, but link is broken?
\url{http://lists.lri.fr/pipermail/termtools/2008-November/000697.html}

\subsection{Fun}

\url{http://lists.lri.fr/pipermail/termtools/2008-December/000710.html}
I am very sorry, but I have just killed the competition webserver.


