\documentclass{rtaloop}
\rtalabel{commutation}

\begin{document}
\begin{problem}{Jean-Pierre Jouannaud}{}{April 1991} 

\begin{abstract}
  Which is the coarsest relation such that its union with any rewrite relation
  preserves termination?
\end{abstract}

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 \emph{fully invariant} (closed under instantiation).
Which is the coarsest (maximal) relation with these properties? (A relation
$R$ is said to be \emph{coarser} than a relation $S$ if $xSy$ implies $xRy$).

The answer is not ``the subterm relation''. Is \emph{encompassment}
(``containment'', the combination of subterm and subsumption) the coarsest
relation which preserves termination (without full invariance)?

\begin{remark}
  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.
\end{remark}

\end{problem}
\end{document}