[Termtools] supplementing the competition input format

[Peter Schneider-Kamp]

Zantema, H. wrote:
> If there are reasons for extending TPDB by a new DP problem category it
> would make sense to execute your proposed extension. But I don't think
> this is the case. Moreover, I am not in favour of it since I guess that
> your DP problem format is strongly motivated by the AProVE architecture
> (or may be the other way around), and therefore not tool independent. Or
> are there problems occurring in nature which are essentially DP
> problems?

First, our DP problem format is strongly motivated by the DP framework.
In fact it is a an exact representation of this. AProVE is just an
implementation of this framework. In that way, the format is not
tailored to our tool but indeed our tool to the format. But I think
that tools like Jambox and TTT already implement something which
is pretty close to the DP framework. Indeed, one of the motivations
for the DP framework was the recursive SCC algorithm of TTT.

Second, regarding a new DP problem category in the TPDB, I think there
are quite a lot "problems occurring in nature" which are essentially
DP problems. If you, for example, take any Haskell program and analyze
the call structure, you end up with recursive function calls
(dependency pairs / top rewrite rules) plus a number of rules needed
to evaluate arguments of these function calls (rules / relative rules).

Translating Haskell functions from real programs and libraries
could result in a lot of interesting termination problems. Consider
that counting up to a limit or until some condition holds and similar
challenging issues occur naturally in (integer based) Haskell programs.

> It may make sense to extend the format for other reasons, for instance
> if you want to try Jambox on the DP problems obtained from the database
> of Haskell programs. But then I think you should agree with the Jambox
> author on this format. I have no problems with using the termtools list
> for discussions on such an exchange of such an internal format. But it
> should be clear that this has nothing to do with the competition and the
> TPDB format.    

Well, then I propose we use the termtools list to discuss about this
format. If we agree on something and at least two tools implement the
format, we can think about extending the competition format and having
a DP problem category.

Actually that is about what I had in mind in the first place. I am
sorry if I made the impression that we want to force an uneccessary
extension on the TPDB input format. I was rather trying to catch up
on our discussion at WST where we agreed that it would be nice to
be able to use all the techniques of tools like AProVE and Jambox
together with your "New Shiny Technqiue(TM)" without having to
reimplement all of them. I thought an agreed upon format would be
a good start at that. And for that reasons I exactly do not want it
to be an internal format only between Jambox and AProVE.

Best regards,
Peter