Abstract
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.