[Submit a comment] [RTALooP home] [Index] [Previous] [Next] | [Postscript] [PDF] [BibTeX Source] [LaTeX Source] |

*Originator: Jean-Pierre Jouannaud *

*Date: April 1991*

Summary: Which is the coarsest relation such that its union with any rewrite relation preserves termination?

Any rewrite relation commutes with the strict-subterm relation; hence, the
union of the latter with an arbitrary terminating rewrite relation is
terminating, and also *fully invariant* (closed under instantiation).
Which is the coarsest (maximal) relation with these properties? (A relation
*R* is said to be *coarser* than a relation *S* if *xSy* implies *xRy*).

The answer is not “the subterm relation”. Is *encompassment*
(“containment”, the combination of subterm and subsumption) the coarsest
relation which preserves termination (without full invariance)?

The coarsest relation we know of which could answer the first question is the variant of subterm that allows multiple occurrences of variables to be renamed apart.

[Submit a comment] [RTALooP home] [Index] [Previous] [Next] | [Postscript] [PDF] [BibTeX Source] [LaTeX Source] |