← All problems
Unverified

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

The source page states the original problem together with its recorded qualifications and progress updates as follows.

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 RR is said to be coarser than a relation SS if xSyxSy implies xRyxRy).

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)?

Recorded progress.

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.

Coming soon

Organizer

Boyuan Wang portraitBoyuan Wang
Minghan Wang portraitMinghan Wang
Bochao Li portraitBochao Li
Hongwei Hu portraitHongwei Hu