[Termtools] supplementing the competition input format

[Peter Schneider-Kamp]

Dear all,

I propose to amend the competition input format to
express settings commonly encountered in the DP framework.
Feel cordially invited to give feedback and discuss
the details either on the list or with me.

The hope is to accomplish the following:
* allow for the direct specification of termination
  problems as so-called "DP problems"
* allow for the use of e.g. AProVE's frontend for
  Haskell98 which produces DP problems rather than TRSs
* establish a format for tool cooperation on a deeper
  level than TRSs, for example by being able to
  integrate a new ordering as an external component
  into a DP-based tool such as AProVE or Jambox

The syntactical changes would be two new cases
for the productions of "decl"
* PAIRS listofrules
* RESTRICTION restrictiondecl
a new case for the production of "strategydecl"
* (QRESTRICTION listofterms)
and two new productions
* listofterms ::= e | term listofterms
* restrictiondecl ::= MINIMAL

Of course, the names for PAIRS, RESTRICTION, QRESTRICTION,
and MINIMAL are subject to discussion. We might want to
call PAIRS TOPRULES etc.

The semantics are that the rules in PAIRS can only be
applied at the top level while the rules of RULES can
be applied anywhere. For showing termination of such
a DP problem (or rather "finiteness") we have to show
that rules from PAIRS cannot be applied infinitely
often. This looks similar to relative termination,
but due to the top level restriction it is quite
a different beast.

If (RESTRICTION MINIMAL) then we only need to show that
rules from PAIRS cannot be applied infinitely often
for terms that are terminating w.r.t RULES.

If a non-empty (STRATEGY (QRESTRICTION f(0) g(x,y)))
is given, the evaluation may only take place
for positions where no subterm can be matched
by either f(0) or g(x,y). By having the left-hand
sides of (RULES ...) in the QRESTRICTION list,
we can simulate innermost. An empty (or not given
QRESTRICTION) corresponds to full termination.
This is useful as we do not lose completeness
in the innermost case when deleting rules. This
can also be used for regular TRSs.

If we can agree on such an extension, I would be happy
to help in reworking the input format definition.

We should also integrate semantical side conditions for
each of the sub categories of TRS (such as
context-sensitive etc.) as discussed on the mailing
list before.

Best regards,
Peter

P.S.: There are currently two different ways of expressing
      different term pairs. For relative termination
      we use (RULES s -> t u ->= v) whereas for termination
      modulo a theory we use (RULES s -> t)
      (THEORY (EQUATIONS u == v)).
      I have preferred the latter as there is a clearer
      separation between pairs of terms that have a
      different meaning. Anyway, I would think we should
      agree on a consistent way for this.
P.P.S: Actually, in AProVE we use the following syntax:
       three new cases for the productions of "decl"
       * PAIRS listofrules
       * Q listofterms
       * MINIMAL minimaldecl
       and two new productions
       * listofterms ::= e | term listofterms
       * minimaldecl ::= YES | NO
-- 
Peter Schneider-Kamp   mailto:psk at informatik.rwth-aachen.de
LuFG Informatik II     http://www-i2.informatik.rwth-aachen.de/~nowonder
RWTH Aachen            phone: ++49 241 80-21211