Undecidability Results on Orienting Single Rewrite Rules

René Thiemann 🌐, Fabian Mitterwallner and Aart Middeldorp 🌐

April 25, 2024

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.

License

BSD License

Topics

Session Orient_Rewrite_Rule_Undecidable