[Termtools] Call for Complexity Related Problems

[Georg Moser]

Dear Fabian,

thank you very much for your observation! You are right, we should not 
consider these examples for the RC, iRC categories.

On the other hand for some of the examples you would like to exclude, I 
would prefer a different remedy. Consider for example AG01/#3.21: 
wouldn't it make more sense to alter this TRS so that the constant $1$ 
is represented as $s(0)$? Then we can indeed speak about the runtime 
complexity of $times(s^n(0),s^m(0))$ proper.

Coming back to my earlier email: I suspect that at least for the 
majority of the examples you mention, there should be sensible TRSs 
which could be put into a new family RC.

best wishes,
Georg

ps: Note that we have only considered a part of these examples in the 
last competition, in particular we do not consider TRSs in 'innermost' 
or 'SRS' families, for obvious reasons. Only those TRSs in the following 
list were selected (see also the corresponding entry in the wiki.)

AG01 

AotoYamada_05 

Applicative_05 

Applicative_first_order_05 

AProVE_04 

AProVE_06 

AProVE_07 

AProVE_08 

Beerendonk_07 

CiME_04 

Der95 

Endrullis_06 

GTSSK07 

HirokawaMiddeldorp_04 

Mixed_TRS 

Rubio_04 

Secret_05_TRS 

Secret_06_TRS 

Secret_07_TRS 

SK90 

Strategy_removed_AG01 

Strategy_removed_CSR_05 

Strategy_removed_mixed_05 

Transformed_CSR_04 

Various_04 

Waldmann_06 

Zantema_05 

AProVE_09_Inductive

Still your analysis shows that an impressive list of problems need not 
be considered.