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 l → r, whether there is some reduction order > such that l > 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.

BibTeX

@article{Orient_Rewrite_Rule_Undecidable-AFP,
  author  = {René Thiemann and Fabian Mitterwallner and Aart Middeldorp},
  title   = {Undecidability Results on Orienting Single Rewrite Rules},
  journal = {Archive of Formal Proofs},
  month   = {April},
  year    = {2024},
  note    = {\url{https://isa-afp.org/entries/Orient_Rewrite_Rule_Undecidable.html},
             Formal proof development},
  ISSN    = {2150-914x},
}