Abstract
Simply typed term rewriting proposed by Yamada (RTA 2001) is a framework of term rewriting allowing higher-order functions. In contrast to the usual higher-order term rewriting frameworks, simply typed term rewriting dispenses with bound variables. This paper presents a method for proving termination of simply typed term rewriting systems (STTRSs, for short). We first give a translation of STTRSs into many-sorted first-order TRSs and show that termination problem of STTRSs is reduced to that of many-sorted first-order TRSs. Next, we introduce a labelling method which is applied to first-order TRSs obtained by the translation to facilitate termination proof of them; our labelling employs an extension of semantic labelling where terms are interpreted on a many-sorted algebra.
This work was partially supported by a grant from Japan Society for the Promotion of Science, No. 14780187.
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.
Similar content being viewed by others
References
T. Aoto and T. Yamada. Proving termination of simply typed term rewriting systems automatically. IPSJ Transactions on Programming, 44(SIG 4 PRO 17):67–77, 2003. In Japanese.
T. Arts and J. Giesl. Termination of term rewriting using dependency pairs. Theoretical Computer Science, 236:133–178, 2000.
F. Baader and T. Nipkow. Term Rewriting and All That. Cambridge University Press, Cambridge, 1998.
N. Dershowitz and J.-P. Jouannaud. Rewrite systems. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B, pages 243–320. Elsevier Science Publishers, 1990.
J.-P. Jouannaud and M. Okada. Executable higher-order algebraic specification languages. In Proceedings of the 6th IEEE Symposium on Logic in Computer Science (LICS’91), pages 350–361, 1991.
S. Kamin and J.-J. Lévy. Two generalizations of the recursive path ordering. Unpublished manuscript, University of Illinois, 1980.
J. W. Klop. Combinatory Reduction Systems. PhD thesis, Rijksuniversiteit, Utrecht, 1980.
J. W. Klop. Term rewriting systems. In S. Abramsky, D. Gabbay, and T. Maibaum, editors, Handbook of Logic in Computer Science, volume 2, pages 1–116. Oxford University Press, 1992.
R. Mayr and T. Nipkow. Higher-order rewrite systems and their confluence. Theoretical Computer Science, 192:3–29, 1998.
T. Yamada. Confluence and termination of simply typed term rewriting systems. In Proceedings of the 12th International Conference on Rewriting Techniques and Applications (RTA’01), volume 2051 of Lecture Notes in Computer Science, pages 338–352. Springer-Verlag, 2001.
H. Zantema. Termination of term rewriting by semantic labelling. Fundamenta Informaticae, 24:89–105, 1995.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Aoto, T., Yamada, T. (2003). Termination of Simply Typed Term Rewriting by Translation and Labelling. In: Nieuwenhuis, R. (eds) Rewriting Techniques and Applications. RTA 2003. Lecture Notes in Computer Science, vol 2706. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44881-0_27
Download citation
DOI: https://doi.org/10.1007/3-540-44881-0_27
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-40254-1
Online ISBN: 978-3-540-44881-5
eBook Packages: Springer Book Archive