Fabian Mitterwallner, Aart Middeldorp, René Thiemann
Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2024), ACM pp. 57:1-57:12, 2024.
pdf 
doi:10.1145/3661814.3662081
Abstract
By means of a simple reduction from Hilbert’s 10th problem we prove the somewhat surprising result that termination of one-rule rewrite systems by a linear interpretation in the natural numbers is undecidable. The very same reduction also shows the undecidability of termination of one-rule rewrite systems using the Knuth—Bendix order with subterm coefficients. The linear termination problem remains undecidable for one-rule rewrite systems that can be shown terminating by a (non-linear) polynomial
interpretation. We further show the undecidability of the problem whether a one-rule rewrite system can be shown terminating by a polynomial interpretation with rational or real coefficients. Several of our results have been formally verified in the Isabelle/HOL proof assistant.
BibTex
@inproceedings{FMAMRT-LICS24, author = "Fabian Mitterwallner and Aart Middeldorp and Ren{\'e} Thiemann", title = "Linear Termination is Undecidable", booktitle = "Proceedings of the 39th Annual {ACM/IEEE} Symposium on Logic in Computer Science", editor = "Pawel Sobocinski and Ugo Dal Lago and Javier Esparza", publisher = "{ACM}", pages = "57:1--57:12", year = 2024, doi = "10.1145/3661814.3662081"}