[Termtools] Outermost Category

[Zantema, H.]

Dear all,

> > We should include outermost to have an objective comparison of the  
> tools.


> that would indeed be a good idea. However, the question arises which  
> examples to use. I would go for all TRSs where full termination has  
> not already been proven.

This is a low cost approach to generate lots of uninteresting examples.
We can include some of them, but I think for getting a sensible comparison we need a list of examples in which the majority is really about outermost.

Of course it is very subjective when an example is 'interesting'. But I am not in favour of running a competition about a sensible variant of rewriting and only apply it to artificial / uninteresting examples, and then draw conclusions about the tools based on the results on these examples. In fact this is the same as what happened with SRS termination where the focus is on artificial extremely small examples (in retrospect I must admit I was partly responsible for that).

Due to the extremely simple format of SRS there is an argument for being interested in artificial examples: in fact many people were triggered by termination problems of extremely small SRSs. But I think for outermost TRS termination there is not such an argument, and a competition only makes sense after building up a set of examples not only being artificial.  


            Best regards, Hans Zantema.

_________________________________________________________
Prof Dr Hans Zantema            
Technische Universiteit Eindhoven / Radboud Universiteit Nijmegen 
Primary address: 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