[Termtools] supplementing the competition input format

[Zantema, H.]

A first reaction:

Why should we do this? The format was defined for being able to run a
competition with several tools on the same programs / rewrite systems,
to be collected in TPDB.

Therefore for these programs/rewrite systems a common format was needed.
>From the competition view point the only reason for extending the format
is that it is required for systems in (a category of) TPDB.

If there are reasons for extending TPDB by a new DP problem category it
would make sense to execute your proposed extension. But I don't think
this is the case. Moreover, I am not in favour of it since I guess that
your DP problem format is strongly motivated by the AProVE architecture
(or may be the other way around), and therefore not tool independent. Or
are there problems occurring in nature which are essentially DP
problems?

It may make sense to extend the format for other reasons, for instance
if you want to try Jambox on the DP problems obtained from the database
of Haskell programs. But then I think you should agree with the Jambox
author on this format. I have no problems with using the termtools list
for discussions on such an exchange of such an internal format. But it
should be clear that this has nothing to do with the competition and the
TPDB format.    


            Best regards, Hans Zantema.

_________________________________________________________
Dr Hans Zantema            
Technische Universiteit Eindhoven, 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 Peter
Schneider-Kamp
Sent: vrijdag 22 september 2006 14:44
To: termtools at lists.lri.fr
Subject: [Termtools] supplementing the competition input format

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



_______________________________________________
Termtools mailing list
Termtools at lists.lri.fr
http://lists.lri.fr/mailman/listinfo/termtools