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 Entry

@inproceedings{MMT-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"
}