Outermost

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.

Problem selection

• René Thiemann suggests:

all TRSs where full termination has not already been proven.

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.

Participants

insert your name here if you intend to participate.

• Olivier Fissore, Isabelle Gnaedig, Hélène Kirchner (Cariboo)
• Matthias Raffelsieper, Hans Zantema
• Rene Thiemann (TTT)
• Joerg Endrullis (Jambox)
• Johannes Waldmann (Matchbox), but will need more time (December 2008)