Undecidability Results on Orienting Single Rewrite Rules

We formalize several undecidability results on termination for one-rule term rewrite systems by means of simple reductions from Hilbert's 10th problem. To be more precise, for a class \(C\) of reduction orders, we consider the question for a given rewrite rule \(\ell \to r\), whether there is some reduction order \({\succ} \in C\) such that \(\ell \succ r\). We include undecidability results for each of the following classes \(C\):

• the class of linear polynomial interpretations over the natural numbers,
• the class of linear polynomial interpretations over the natural numbers in the weakly monotone setting,
• the class of Knuth–Bendix orders with subterm coefficients,
• the class of non-linear polynomial interpretations over the natural numbers, and
• the class of non-linear polynomial interpretations over the rational and real numbers.