Abstract
For a hierarchy of properties of term rewriting systems, related to termination, we prove relative undecidability even in the case of single rewrite rules: for implications X ⇒ Y in the hierarchy the property X is undecidable for rewrite rules satisfying Y.
Work carried out at Universität Passau, Lehrstuhl für Programmiersysteme. Partially supported by grant Ku 996/3-1 of the Deutsche Forschungsgemeinschaft within the Schwerpunkt Deduktion.
Partially supported by the Advanced Information Technology Program (AITP) of the Information Technology Promotion Agency (IPA).
Chapter PDF
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
M. Dauchet. Simulation of Turing machines by a regular rewrite rule. Theoretical Computer Science, 103(2):409–420, 1992.
N. Dershowitz. Termination of rewriting. Journal of Symbolic Computation 3(1 & 2):69–116, 1987.
N. Dershowitz and J.-P. Jouannaud. Rewrite systems. In Handbook of Theoretical Computer Science, volume B, pages 243–320. Elsevier, 1990.
N. Dershowitz, J.-P. Jouannaud, and J.W. Klop. Problems in rewriting III. In Proc. 6th RTA, volume 914 of LNCS, pages 457–471, 1995.
M. Ferreira. Termination of term rewriting — well-foundedness, totality, and transformations. PhD thesis, University of Utrecht, 1995.
M. Ferreira and H. Zantema. Dummy elimination: Making termination easier. In Proc. 10th FCT, volume 965, pages 243–252, 1995.
M. Ferreira and H. Zantema. Total termination of term rewriting. Applicable Algebra in Engineering, Communication and Computing, 7(2):133–162, 1996.
A. Geser. Omega-termination is undecidable for totally terminating term rewriting systems. Technical Report MIP-9608, University of Passau, 1996. To appear in Journal of Symbolic Computation.
A. Geser, A. Middeldorp, E. Ohlebusch, and H. Zantema. Relative undecidability in term rewriting. In Proc. CSL, Utrecht, 1996. Available at http://www.score.is.tsukuba.ac.jp/∼ami/papers/cs196.dvi.
A. Geser, A. Middeldorp, E. Ohlebusch, and H. Zantema. Relative undecidability in the termination hierarchy of single rewrite rules. Technical report, 1997. Available at http://www-sr.informatik.uni-tuebingen.de/∼geser/papers/caap97-full. dvi.
G. Huet and D. S. Lankford. On the uniform halting problem for term rewriting systems. Rapport Laboria 283, INRIA, 1978.
P. Lescanne. On termination of one rule rewrite systems. Theoretical Computer Science, 132:395–401, 1994.
A. Middeldorp and B. Gramlich. Simple termination is difficult. Applicable Algebra in Engineering, Communication and Computing, 6(2):115–128, 1995.
A. Middeldorp and H. Zantema. Simple termination of rewrite systems. Theoretical Computer Science, 175, 1997. To appear.
David Plaisted. The undecidability of self-embedding for term rewriting systems. Information Processing Letters, 20:61–64, 1985.
E. Post. A variant of a recursively unsolvable problem. Bulletin of the American Mathematical Society, 52, 1946.
H. Zantema. Termination of term rewriting: interpretation and type elimination. Journal of Symbolic Computation, 17:23–50, 1994.
H. Zantema. Total termination of term rewriting is undecidable. Journal of Symbolic Computation, 20:43–60, 1995.
H. Zantema and A. Geser. Non-looping rewriting. Technical Report UU-CS-1996-03, Utrecht University, 1996. Available at ftp://ftp.cs.ruu.nl/pub/RUU/CS/techreps/CS-1996/1996-03.ps.gz.
Hans Zantema. Termination of term rewriting by semantic labelling. Fundamenta Informaticae, 24:89–105, 1995.
Author information
Authors and Affiliations
Corresponding author
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Geser, A., Middeldorp, A., Ohlebusch, E., Zantema, H. (1997). Relative undecidability in the termination hierarchy of single rewrite rules. In: Bidoit, M., Dauchet, M. (eds) TAPSOFT '97: Theory and Practice of Software Development. CAAP 1997. Lecture Notes in Computer Science, vol 1214. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0030600
Download citation
DOI: https://doi.org/10.1007/BFb0030600
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-62781-4
Online ISBN: 978-3-540-68517-3
eBook Packages: Springer Book Archive