[Termination tools] Termination of context-sensitive rewriting strategies

[Salvador Lucas]

Dear Claude and all,

Regarding the consideration of CSR into the TPDB
format, first I want to thank to you and Albert
for including it. I also want to thank both of
you for your work during these years on this
initiative and for your work during these months
collecting all these examples which will greatly
help to improve (and promote) termination tools.

However, I would like to mention that including
CSR as a kind of strategy restricts the flexibility
of the format. In fact, you can consider many
different context-sensitive rewriting strategies.
For instance, there are specific transformations
(developed by Giesl and Middeldorp) for proving
termination of *innermost* CSR.

The current format does not allow to express that
you want to prove termination of innermost CSR...

Regarding the tools involved in this mailing list,
this has some consequences. For instance, as we
discussed in a previous e-mail, CARIBOO can prove
termination of rewriting with strategy annotations
for symbols like,  e.g., \phi(cons)=(1 0) for the
list constructor 'cons'. Provided that no other
symbol receive any special annotation, this would
correspond to (termination of) leftmost-innermost
CSR.

On the other hand, termination of CSR for the
replacement map mu(cons)={1} is a stronger notion
which implies termination of innermost CSR
but also outermost CSR or any kind of CS-strategy.

Since (in general) termination of innermost CSR
does not imply termination of CSR, a proof of
termination with CARIBOO could erroneously be
interpreted as a proof of termination of CSR...

Thus, I suggest to permit something like

(STRATEGY INNERMOST CONTEXTSENSITIVE ... )

This would not be so difficult to reflect in the
current grammar. For instance, we could split
the rule for 'strategydecl' as follows:

strategydecl ::= INNERMOST restrictiontype
restrictiontype ::= e | CONTEXTSENSITIVE csstratlist

or, if you want to be more general (e.g., to
further consider the OUTERMOST strategy):

strategydecl ::= strategytype restrictiontype
strategytype ::= INNERMOST | OUTERMOST
restrictiontype ::= e | CONTEXTSENSITIVE csstratlist

On the other hand, a new production

RESTRICTION restrictiontype

could be added to the definition of 'decl'. In this
way, termination of CSR itself, and termination of
CS-strategies would be covered by the format. Other
restrictions of rewriting could also be considered
now by adding more 'restriction types'...

Best regards,

Salvador.