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"
}