Termination-Portal.org - User contributions [en]

Termination Competition Platform

2008-11-25T11:48:22Z

Hzantema: /* Wishlist: Query Interface */

= Note =

There is (will be) a well-defined process of making design decisions w.r.t. the Termination Competition Execution and Presentation Platform (via mailing list, steering committee), and then the Host decides on implementation.

For features that have run through this process, the [http://dev.aspsimon.org/bugzilla/buglist.cgi?bug_file_loc=&bug_file_loc_type=allwordssubstr&bug_id=&bug_status=NEW&bug_status=ASSIGNED&bug_status=REOPENED termcomp Bugzilla] is the right place for bug reports.

Below here, we just collect some ideas for later consideration.

= Wishlist: Query Interface =

The idea is to provide a web interface for queries over the results data base(s).
We aim for flexibility, but will start with some simple prototype.
Please list here some typical queries that you would want to execute.

* what problems were solved in srs-standard, but not in srs-standard-certified?
* what are the problems that were solved in (insert category here)-2008 but not in 2007 (yes, we plan to import earlier competition results into the data base)?
* what is the problem/tool in (insert category here) with the longest/shortest proof (file size)/execution time?

* what are the problems that generate a coq timeout for some tool?
* what is the average size of the (xml|coq) files generated by a given tool?
* what are the (problems|results) that are (solved|certified) by all the tools in some set of tools?

* here is a [http://color.loria.fr/comp.html result presentation for Color in certified categories] that Frederic built "by hand" (?) The query interface should automatically produce such or and similar charts.

what might also be helpful: can you name a web site with some configurable query functionality
that you think is especially well-designed and worth learning from?

Christian Sternagel: I would also like to be able to query the problem data base and not only the results data base(s). (J.W.: there is a [http://colo5-c703.uibk.ac.at:8080/termcomp/tpdb/tpsearch.seam query interface for tpdb] already. what features are missing? C.S.: Since it is currently not working, it is merely a placeholder for a query interface.)

Missing features:

* give me all problems from 2007 that are left linear/overlapping/dummy SRSs/... (i.e., properties of problems)
* boolean combination of properties
* wild cards
* give results statistics for parts of a category, e.g., only selected subdirectories

Outermost

2008-11-07T16:02:59Z

Hzantema: /* Problem selection */

This page is to record the current status of the proposed Outermost Strategy Category of the Termination Competition.

The first installation of this event is planned for November 4, 2008.

== Overview of the Event ==

It is a challenging topic to automatically prove
termination of term rewriting with respect to outermost rewriting strategy.
This strategy is especially interesting since it establishes the basis of
lazy programming languages as Haskell, Miranda or Clean
where programming with infinite structures is common practice and
therefore full termination (with respect to an arbitrary strategy) cannot be expected.

* Hans Zantema:

We should decide whether we take ground or open. For instance,

f(x,a) -> f(x,b)
b -> a
f(a,x) -> a
f(b,x) -> a
f(f(x,y),z) -> a

is ground outermost terminating (when restricting to symbols occurring in the TRS), but not outermost terminating if we allow open terms or allowed to extend the signature. Since the open variant is more robust (it does not change by extending the signature) I propose to allow open terms in the definition of outermost termination, by which the above example is NOT outermost terminating.

== Problem selection ==

* René Thiemann suggests:

All TRSs where full termination has not already been proven. If there is a special category of "interesting" outermost-examples then I suggest to add all non-terminating TRSs to this category. The reason is that these examples are interesting since only provers which are aware of the outermost-strategy can solve these examples.

* Hans Zantema:

I agree with Joerg that apart from these TRSs where full termination has not already been proven special TRSs with outermost strategy should be considered. Giving both of these subcategories equal weight is OK with me. The main point to be done now is to extend the present list of only 6 TRSs in TPDB with outermost strategy. A competiton does not make sense before this list has some reasonable size and content.

A proposal for 50 new examples is found in http://www.win.tue.nl/~hzantema/ex.zip. It is my intension to submit these. If you have remarks, or suggestions for extensions, please let me know.

* Joerg Endrullis:

Yes, I will add some more examples to the outermost category. Unfortunately the search in the termination competition interface does not work. Searching for outermost examples yields always the empty result, such that one cannot see which examples are already there.

== Scoring ==

* Joerg Endrullis suggests:

If we use all TRSs where full termination has not already been proven,
then these examples will dominate the outermost category.
However this is no problem, since a balance can be reached by
choosing an appropriate scoring.

I would suggest to split the score.
That is, give 50 points for the tool that proves
most of the examples with "STRATEGY OUTERMOST" terminating,
and 50 points for the tool that proves most
of the "TRSs where full termination has not already been proven"
to be outermost terminating.
The non-winning tools get in both categories
50 * (number of problems solved) / (number of problems solved by winner).
Thus in theory a tool winning both categories obtains 100 points.

* comment on Joerg's proposal (by René):

If the idea of a splitting is applied then I would count every valid answer for the "interesting" examples and not only the YES-answers.

== Participants ==

insert your name here if you intend to participate.

* AProVE-team
* Olivier Fissore, Isabelle Gnaedig, Hélène Kirchner (Cariboo)
* Matthias Raffelsieper, Hans Zantema
* Christian Sternagel and Rene Thiemann (TTT2)
* Joerg Endrullis (Jambox)
* Johannes Waldmann (Matchbox), but will need more time

Outermost

2008-11-07T16:00:50Z

Hzantema: /* Scoring */

This page is to record the current status of the proposed Outermost Strategy Category of the Termination Competition.

The first installation of this event is planned for November 4, 2008.

== Overview of the Event ==

It is a challenging topic to automatically prove
termination of term rewriting with respect to outermost rewriting strategy.
This strategy is especially interesting since it establishes the basis of
lazy programming languages as Haskell, Miranda or Clean
where programming with infinite structures is common practice and
therefore full termination (with respect to an arbitrary strategy) cannot be expected.

* Hans Zantema:

We should decide whether we take ground or open. For instance,

f(x,a) -> f(x,b)
b -> a
f(a,x) -> a
f(b,x) -> a
f(f(x,y),z) -> a

is ground outermost terminating (when restricting to symbols occurring in the TRS), but not outermost terminating if we allow open terms or allowed to extend the signature. Since the open variant is more robust (it does not change by extending the signature) I propose to allow open terms in the definition of outermost termination, by which the above example is NOT outermost terminating.

== Problem selection ==

* René Thiemann suggests:

All TRSs where full termination has not already been proven. If there is a special category of "interesting" outermost-examples then I suggest to add all non-terminating TRSs to this category. The reason is that these examples are interesting since only provers which are aware of the outermost-strategy can solve these examples.

* Hans Zantema:

I agree with Joerg that apart from these TRSs where full termination has not already been proven special TRSs with outermost strategy should be considered. Giving both of these subcategories equal weight is OK with me. The main point to be done now is to extend the present list of only 6 TRSs in TPDB with outermost strategy. I intend to submit some new systems; I hope other participants will do that too. A competiton does not make sense before this list has some reasonable size and content.

* Joerg Endrullis:

Yes, I will add some more examples to the outermost category. Unfortunately the search in the termination competition interface does not work. Searching for outermost examples yields always the empty result, such that one cannot see which examples are already there.

== Scoring ==

* Joerg Endrullis suggests:

If we use all TRSs where full termination has not already been proven,
then these examples will dominate the outermost category.
However this is no problem, since a balance can be reached by
choosing an appropriate scoring.

I would suggest to split the score.
That is, give 50 points for the tool that proves
most of the examples with "STRATEGY OUTERMOST" terminating,
and 50 points for the tool that proves most
of the "TRSs where full termination has not already been proven"
to be outermost terminating.
The non-winning tools get in both categories
50 * (number of problems solved) / (number of problems solved by winner).
Thus in theory a tool winning both categories obtains 100 points.

* comment on Joerg's proposal (by René):

If the idea of a splitting is applied then I would count every valid answer for the "interesting" examples and not only the YES-answers.

== Participants ==

insert your name here if you intend to participate.

* AProVE-team
* Olivier Fissore, Isabelle Gnaedig, Hélène Kirchner (Cariboo)
* Matthias Raffelsieper, Hans Zantema
* Christian Sternagel and Rene Thiemann (TTT2)
* Joerg Endrullis (Jambox)
* Johannes Waldmann (Matchbox), but will need more time

Outermost

2008-11-07T15:51:31Z

Hzantema: /* Overview of the Event */

This page is to record the current status of the proposed Outermost Strategy Category of the Termination Competition.

The first installation of this event is planned for November 4, 2008.

== Overview of the Event ==

It is a challenging topic to automatically prove
termination of term rewriting with respect to outermost rewriting strategy.
This strategy is especially interesting since it establishes the basis of
lazy programming languages as Haskell, Miranda or Clean
where programming with infinite structures is common practice and
therefore full termination (with respect to an arbitrary strategy) cannot be expected.

* Hans Zantema:

We should decide whether we take ground or open. For instance,

f(x,a) -> f(x,b)
b -> a
f(a,x) -> a
f(b,x) -> a
f(f(x,y),z) -> a

is ground outermost terminating (when restricting to symbols occurring in the TRS), but not outermost terminating if we allow open terms or allowed to extend the signature. Since the open variant is more robust (it does not change by extending the signature) I propose to allow open terms in the definition of outermost termination, by which the above example is NOT outermost terminating.

== Problem selection ==

* René Thiemann suggests:

All TRSs where full termination has not already been proven. If there is a special category of "interesting" outermost-examples then I suggest to add all non-terminating TRSs to this category. The reason is that these examples are interesting since only provers which are aware of the outermost-strategy can solve these examples.

* Hans Zantema:

I agree with Joerg that apart from these TRSs where full termination has not already been proven special TRSs with outermost strategy should be considered. Giving both of these subcategories equal weight is OK with me. The main point to be done now is to extend the present list of only 6 TRSs in TPDB with outermost strategy. I intend to submit some new systems; I hope other participants will do that too. A competiton does not make sense before this list has some reasonable size and content.

* Joerg Endrullis:

Yes, I will add some more examples to the outermost category. Unfortunately the search in the termination competition interface does not work. Searching for outermost examples yields always the empty result, such that one cannot see which examples are already there.

== Scoring ==

*
* Joerg Endrullis suggests:

If we use all TRSs where full termination has not already been proven,
then these examples will dominate the outermost category.
However this is no problem, since a balance can be reached by
choosing an appropriate scoring.

I would suggest to split the score.
That is, give 50 points for the tool that proves
most of the examples with "STRATEGY OUTERMOST" terminating,
and 50 points for the tool that proves most
of the "TRSs where full termination has not already been proven"
to be outermost terminating.
The non-winning tools get in both categories
50 * (number of problems solved) / (number of problems solved by winner).
Thus in theory a tool winning both categories obtains 100 points.

* comment on Joerg's proposal (by René):

If the idea of a splitting is applied then I would count every valid answer for the "interesting" examples and not only the YES-answers.

== Participants ==

insert your name here if you intend to participate.

* AProVE-team
* Olivier Fissore, Isabelle Gnaedig, Hélène Kirchner (Cariboo)
* Matthias Raffelsieper, Hans Zantema
* Christian Sternagel and Rene Thiemann (TTT2)
* Joerg Endrullis (Jambox)
* Johannes Waldmann (Matchbox), but will need more time

Outermost

2008-11-03T09:33:33Z

Hzantema: /* Problem selection */

People:Hans Zantema

2008-11-03T09:21:49Z

Hzantema: New page: <!-- Please fill in the data so that you can be added to some default categories and a simple user page can be created. You may extend that user page yourself after th...

{{Person
|firstname=Hans
|middlenames=
|lastname=Zantema
|titles=prof dr
|email=h.zantema@tue.nl
|homepage=www.win.tue.nl/~hzantema
|country=The Netherlands
|university=Technische Universiteit Eindhoven / Radboud Universiteit Nijmegen
|department=computer science
|role=Professor
}}