[Termination tools] Several issues

[Aart Middeldorp]

Juergen Giesl wrote:

>  > + Now for a proposal to make the competition more attractive for
>  >   outsiders (and insiders?): Every year a particular method (e.g.
>  >   LPO) is selected and everyone is invited to implement the method;
>  >   the implementations are then compared on the problems in the TPDB.
>  >   So the emphasis will be on efficiency. We believe this might
>  >   attract many new people to the area which in turn could stimulate
>  >   further termination research.
> 
> Indeed, I agree that would be interesting. As I mentioned above,
> I believe that in order to be as successful as possible, one has to
> combine many techniques in a sophisticated way. But how to implement
> each of these techniques efficiently is also an interesting question.
> 
> However, I see the problem that simply
> comparing the runtimes does not give an objective comparison since people
> use different programming languages. I guess that there exist some
> investigations on the speed of different languages. Maybe one could 
> multiply
> the runtimes in this special efficiency-competition by a certain factor
> depending on the language used.

Why so complicated? This is *not* about comparing the LPO implementation in
TTT (written in Ocaml) with the one in AProVE (written in Java). One can
qualify the results by mentioning the language. Maybe I'm too optimistic
here, but I imagine that this could be an attractive student project in
many places. To facilitate the work, parsers for the TPDB format can be
made available in a variety of programming languages.

I have seen very little discussion on this topic. Am I the only one who is
concerned about the size of our community? Any other ideas to attract new
people to our area?!

-- Aart