[Termtools] Next competition

[slucas at dsic.upv.es]

Dear all,

Mensaje citado por Claude Marche <marche at lri.fr>:

> 2) To encourage the idea of having the tool provide evidence of
>    termination (or non-termination), the answer given on standard
>    output will be expected to have the form
>
>    first line : YES or NO

I think that some DON'T KNOW is also necessary...

>    remaining : a proof trace in english, with reference to criteria
>    involved.

Ok.

> On the other hand, I'd like to encourage more kinds of input problems,
> so
>
>    . the LP category will be resurrected
>    . the TRS subcategories with only one participant, cancelled last
>      year, will be resurrected too.
>
>      Remark: for the categories with strategies : in principle any tool could
>      participate, by ignoring the strategy if it does not support it.
>      it appears that in the TPDB, several problems classified in the
>      innnermost or context-sensitive category are in fact strongly
>      terminating. So I encourage author of tool to accept any strategy
>      in the input file, and not to fail like it is the case now.
>
>    . I'd like to propose new categories for functional programs and
>      imperative programs. I have no proposal for a official input
>      syntax, but if you are interested plase tell me.
>
>    . I suggest also a category for OBJ programs, which are close to
>      rewriting, but have sorts, programmable strategies, conditions.

I support this proposal.

Best regards,

Salvador.

----------------------------------------------------------------
This message was sent using IMP, the Internet Messaging Program.