Abstract
An extension of a modular termination result for term rewriting systems (TRSs, for short) by A. Middeldorp (1989) is presented. We intended to obtain this by adapting the dummy elimination transformation by M. C. F. Ferreira and H. Zantema (1995) under the presence of a non-collapsing non-duplicating terminating TRS whose function symbols are all to be eliminated. We propose a tree lifting ordering induced from a reduction order and a set G of function symbols, and use this ordering to transform a TRS R into R'; termination of R' implies that of RUS for any non-collapsing non-duplicating terminating TRS S whose function symbols are contained in G, provided that for any l → r in R (1) the root symbol of r is in G whenever that of l is in G; and (2) no variable appears directly below a symbol from G in l when G contains a constant. Because of conditions (1) and (2), our technique covers only a part of the dummy elimination technique; however, even when S is empty, there are cases that our technique has an advantage over the dummy elimination technique.
This work is partially supported by Grants from Ministry of Education, Science and Culture of Japan, #09245212 and #07680347.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
T. Aoto and Y. Toyama. Tree lifting orderings for termination transformations of term rewriting systems. Research Report IS-RR-97-0033F, School of Information Science, JAIST, 1997.
N. Dershowitz. Hierarchical termination. In Proceedings of the 4th International Workshop on Conditional (and Typed) Rewriting Systems (CTRS-94), LNCS 968, pages 89–105. Springer-Verlag, 1995.
M. Fernández and J.-P. Jouannaud. Modular termination of term rewriting systems revisited. In Proceedings of the 10th Workshop on Specification of Abstract Data Types, LNCS 906, pages 255–272. Springer-Verlag, 1995.
M. C. F. Ferreira. Termination of term rewriting. PhD thesis, Utrecht University, 1995.
M. C. F. Ferreira. Dummy elimination in equational rewriting. In Proceedings of the 1th International Conference on Rewriting Techniques and Applications (RTA-96), LNCS 1103, pages 78–92. Springer-Verlag, 1996.
M. C. F. Ferreira and H. Zantema. Dummy elimination: making termination easier. In Proceedings of the 10th International Conference on Foundamentals of Computation Theory (FCT'95), LNCS 965, pages 243–252. Springer-Verlag, 1995.
M. C. F. Ferreira, D. Kesner and L. Puel. Reducing AC-termination to termination. Manuscript, 1997.
M. R. K. Krishna Rao. Modular proofs for completeness of hierarchical term rewriting systems. Theoretical Computer Science, 151:487–512, 1995.
A. Middeldorp. A sufficient condition for the termination of the direct sum of term rewriting systems. In Proceedings of the 4th annual IEEE Symposium on Logic in Computer Science (LICS'89), pages 396–401. IEEE Computer Society Press, 1989.
A. Middeldorp, H. Ohsaki and H. Zantema. Transforming termination by selflabelling. In Proceedings of the 13th International Conference on Automated Deduction (CADE-13), LNAI 1104, pages 373–387. Springer-Verlag, 1996.
A. Middeldorp and H. Zantema. Simple termination of rewrite systems. Theoretical Computer Science, 175(1):127–158, 1997.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1998 Springer-Verlag
About this paper
Cite this paper
Aoto, T., Toyama, Y. (1998). Termination transformation by tree lifting ordering. In: Nipkow, T. (eds) Rewriting Techniques and Applications. RTA 1998. Lecture Notes in Computer Science, vol 1379. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0052375
Download citation
DOI: https://doi.org/10.1007/BFb0052375
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-64301-2
Online ISBN: 978-3-540-69721-3
eBook Packages: Springer Book Archive