Abstract

In this paper we prove via a reduction from Hilbert’s 10th problem that the problem whether the termination of a given rewrite system can be shown by a polynomial interpretation in the natural numbers is undecidable, even for rewrite systems that are incrementally polynomially terminating. We also prove that incremental polynomial termination is an undecidable property of terminating rewrite systems.

BibTeX

@inproceedings{FMAM-FSCD22,
 author    = "Fabian Mitterwallner and Aart Middeldorp",
 title     = "Polynomial Termination over $\mathbb{N}$ is Undecidable",
 booktitle = "Proceedings of the 7th International Conference on Formal
              Structures for Computation and Deduction",
 editor    = "Amy Felty",
 series    = "Leibniz International Proceedings in Informatics"
 volume    = 228,
 pages     = "27:1--27:17",
 year      = 2022,
 doi       = "10.4230/LIPIcs.FSCD.2022.27"
}