Undecidability Results on Orienting Single Rewrite Rules (Q7361063)

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.