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

Problem #29

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]