Problem #87 (Solved !)
Originator: Hans Zantema
Date: April 1995
Summary:
Is it decidable whether a single term rewrite rule can be proved
terminating by a monotonic ordering that is total on ground terms?
Termination of string-rewriting systems is known to be undecidable
[HL78]. Termination of a single term-rewriting rule was
proved undecidable in [Dau92, Les94]. It is also undecidable
whether there exists a simplification ordering that proves
termination of a single term rewriting rule [MG95] (cf.
[JK84]). Is it decidable whether a single term rewrite
rule can be proved terminating by a monotonic ordering that is total
on ground terms? (With more rules it is not [Zan94].)
Remark
A negative solution has been given in [GMOZ97]. More about the
history of this problem in the context of the question of one-rule
termination can be found in [Der05].
References
-
[Dau92]
-
Max Dauchet.
Simulation of Turing machines by a regular rewrite rule.
Theoretical Computer
Science, 103(2):409–420, 1992.
- [Der05]
-
Nachum Dershowitz.
Open.
Closed. Open.
In Jürgen Giesl, editor, 16th International
Conference on Rewriting Techniques, volume 3467 of Lecture Notes in Computer
Science, Nara, Japan, April 2005.
Springer-Verlag.
- [GMOZ97]
-
Alfons Geser, Aart Middeldorp, Enno Ohlebusch, and Hans Zantema.
Relative undecidability in the termination hierarchy of single
rewrite rules.
In Michel Bidoit and Max Dauchet, editors, Theory and Practice
of Software Development, volume 1214 of Lecture Notes in Computer
Science, pages 237–248, Lille, France, April 1997.
Springer-Verlag.
- [HL78]
-
Gérard Huet and Dallas S. Lankford.
On the uniform halting problem for term rewriting systems.
Rapport laboria 283, Institut de Recherche en Informatique et en
Automatique, Le Chesnay, France, March 1978.
- [JK84]
-
Jean-Pierre Jouannaud and Hélène Kirchner.
Construction d’un plus petit ordre de simplification.
RAIRO Theoretical Informatics, 18(3):191–207, 1984.
- [Les94]
-
Pierre Lescanne.
On termination of one rule rewrite systems.
Theoretical Computer
Science, 132(1–2):395–401, September 1994.
- [MG95]
-
Aart Middeldorp and Bernhard Gramlich.
Simple termination is difficult.
Applicable
Algebra in Engineering, Communication and Computing, 6(2):115–128, 1995.
- [Zan94]
-
Hans Zantema.
Total termination of term rewriting is undecidable.
Technical Report UU-CS-1994-55, Utrecht University, December 1994.