[Termtools] Examples contextsensitive

[joerg at endrullis.de]

Actually Jambox will take part in the contextsensitive category.
The only thing I changed in Jambox was dropping the >= 1
requirement for the upper-left of matrices corresponding to
argument positions where rewriting is forbidden.

However, Hans Zantemas observation is absolutely right.
The examples are not intended to demonstrate the power of Jambox.
All examples apart from "cariboo_ex2" can easily be solved by the
2007 version of muTerm, thus the 2008 version will probably
solve all of them.

The idea of the collection was to have a transformation
of all challenging outermost termination examples I found
in the literature: that is the cariboo_ex* examples
and examples from:
  "A transformational approach to prove outermost termination automatically"
  by Matthias Raffelsieper and Hans Zantema
Pruning the list to 10, I would have to remove some
interesting examples.

Kind regards,
Joerg

>> ruling is: 10 examples per team per category. please prune this zip
> file to 10 examples.
>
> In my opinion here the upper bound of 10 is not applicable. The idea of
> this upper bound was that to show the particular power of some tool, the
> tool author may submit a limited number of examples designed for this goal
> just before the deadline.
>
> Here the situation is completely different. As far as I know Joerg is not
> involved in a tool for context-sensitive rewriting. Instead he recently
> developed a technique to transform outermost to context-sensitive. The
> proposed systems are results of this transformation. This is a first step
> towards a completely new application of termination of context-sensitive
> rewriting, and from that point of view interesting to have them in the
> problem set.
>
> Since the reason for the upper bound does not apply here and a new class
> of examples is created, I propose to include all 17 examples.
>
>
>             Best regards, Hans Zantema.
>
> _________________________________________________________
> Prof Dr Hans Zantema
> Technische Universiteit Eindhoven / Radboud Universiteit Nijmegen
> Primary address: Department of Computer Science
> P.O. Box 513, 5600 MB Eindhoven, The Netherlands
> e-mail: H.Zantema at tue.nl, homepage: www.win.tue.nl/~hzantema
> office: Hoofdgebouw room 6.73, tel: (040)2472749
>
>
> -----Original Message-----
> From: termtools-bounces at lists.lri.fr
> [mailto:termtools-bounces at lists.lri.fr] On Behalf Of Simon Bailey
> Sent: dinsdag 4 november 2008 8:04
> To: joerg at endrullis.de
> Cc: termtools
> Subject: Re: [Termtools] Examples contextsensitive
>
> hi jörg,
>
> On Nov 4, 2008, at 6:41 AM, joerg at endrullis.de wrote:
>> could you please import these 17 contextsensitive examples into the
>> TPDB:
>> http://infinity.few.vu.nl/productivity/contextSensitive.zip
>
> ruling is: 10 examples per team per category. please prune this zip
> file to 10 examples.
>
>> Using the web-interface there is no possibility for comment
>> annotations
>> and I do not understand the format for uploading contextsensitive
>> examples.
>> There is a field:
>> "The list of variables separated by spaces, without parentheses."
>> Usually the annotations are the mu-replacement maps in form of
>> (symbol argNr1 .. argNr2)+
>> that is, symbols with arguments where rewriting is allowed.
>>
>> For the furture, I think it would be good if there would be an
>> option for uploading the examples in the competition format,
>> and uploading of zip files containing multiple examples.
>> I think Aprove has a good parser (in Java) which is able to
>> parse all formats allowed by the TPDB specification, and
>> I guess they would support the web-interface by providing the
>> source code of the parser if needed.
>
> i already use the sablecc grammars supplied by aprove for importing
> the termination problems into the database. the web form has not been
> worked on since may as there has been discussion that the storage
> format of the TPDB will change. until the format of the files is not
> clear, i will not do any further work on importers, web-based or
> otherwise (wasted effort). i will take this interface offline later
> today before starting the competition.
>
> however, once the format is clear, then the web-interface will offer a
> possibility to upload multiple problems in form of a zip file.
>
> regards,
> sb
> _______________________________________________
> Termtools mailing list
> Termtools at lists.lri.fr
> http://lists.lri.fr/mailman/listinfo/termtools
>