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. Our results may be summarized as follows: being simply terminating, (non-)self-embedding, and (non-)looping are undecidable properties of orthogonal, variable preserving, one-rule constructor systems.

BibTeX Entry

@article{MG-AAECC95,
 author    = "Aart Middeldorp and Bernhard Gramlich",
 title     = "Simple Termination is Difficult",
 journal   = "Applicable Algebra in Engineering, Communication and
              Computing",
 volume    = 6,
 number    = 2,
 pages     = "115--128",
 year      = 1995,
 doi       = "10.1007/BF01225647"
}