Abstract

A terminating term rewriting system is called simply terminating if its termination can be shown by means of a simplification ordering, an ordering with the property that a term is always bigger than its proper subterms. Almost all methods for proving termination yield, when applicable, simple termination. We show that simple termination is an undecidable property, even for one-rule systems. This contradicts a result by Jouannaud and Kirchner. The proof is based on the ingenious construction of Dauchet who showed the undecidability of termination for one-rule systems.

BibTeX Entry

@inproceedings{MG-RTA93,
 author    = "Aart Middeldorp and Bernhard Gramlich",
 title     = "Simple Termination is Difficult",
 booktitle = "Proceedings of the 5th International Conference on Rewriting
              Techniques and Applications",
 series    = "Lecture Notes in Computer Science",
 volume    = 690,
 pages     = "228--242",
 year      = 1993,
 doi       = "10.1007/3-540-56868-9\_18"
}