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 ℓ→r, whether there is some reduction order ≻∈C such that ℓ≻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

Related publications

  • Mitterwallner, F., Middeldorp, A., & Thiemann, R. (2024). Linear Termination is Undecidable. Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science, 1–12. https://doi.org/10.1145/3661814.3662081

Session Orient_Rewrite_Rule_Undecidable

Depends on

Cite

× 
@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},
}
Download

Download

× Download latest

Older releases: