[Termtools] competition

[Prof. Geser]

Dear all,

I am strictly against applying rules that have not been stated when
the competition started. There is a principle in law: you cannot be
convicted for your deed perpetrated when there was no law for
it. According to our current competition rules, Mu-Term cannot be
disqualified.

I suggest to give Salvador the chance to withdraw Mu-Term from this
competition. Of course I am looking forward to see Mu-Term competing
next time.

We can, however, and we should, change the competition rules for next
time.  Here are a few suggestions for future rules:

1) a tool author may choose to withdraw his/her tool. Then the results
will not be shown.

2) if anyone can demonstrate that a tool yields, under competition
conditions, a false answer for some system then that tool will be
disqualified. The example system need not be in the database.

A false answer also includes a false justification of an otherwise
correct answer.

Point 1 gives the authors the possibility to withdraw when they
suspect that their tool is not reliable. Point 2 extends the
disqualification to false answers outside the database.

 > I know at least one other buggy tool:
 > matchbox/satelite gives a wrong answer for
 > (VAR x)(STRATEGY INNERMOST)(RULES  a -> x)
 > because the *-bound computer does not handle
 > new-born variables correctly. For standard rewriting this bug
 > is hidden because the loop checker finds a loop earlier.
 > But the loop checker is turned off with strategies.
 > (I subscribe to Claude's viewpoint that this really
 > *is* a rewriting system and this really *is* a bug.)

Wait a minute. What a term rewriting system is, is not stated in the
rules of the competition. So one could construe that a term rewriting
system is whatever definition (s)he could find in the literature. If
we want a consistent definition, then we have to cast it into a
competition rule, which will be applicable next time:

3) a term rewriting system, for the purposes of this competition, may
introduce fresh variables at right hand sides, and may have variables
as left hand sides. In the ordinary case (without strategies, types,
or conditions), this will imply that the system is non-terminating.

And, finally, a meta-rule:

4) the rules of the competition are decided during a meeting at the
end of the previous competition. This includes new categories or
syntax extensions.

Kind Regards,
Alfons

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