Abstract
We propose simply typed term rewriting systems (STTRSs), which extend first-order rewriting by allowing higher-order functions. We study a simple proof method for con uence which employs a characterization of the diamond property of a parallel reduction. By an application of the proof method, we obtain a new con uence result for orthogonal conditional STTRSs. We also discuss a semantic method for proving termination of STTRSs based on monotone interpretation.
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
J.A. Bergstra and J.W. Klop. Conditional rewrite rules: Confluence and termination. Journal of Computer and System Science, 32:323–362, 1986.
F. Baader and T. Nipkow. Term Rewriting and All That. Cambridge University Press, 1998.
N. Dershowitz and J.-P. Jouannaud. Rewrite systems. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B, chapter 6, pages 243–320. The MIT Press, 1990.
B. Gramlich. Confluence without termination via parallel critical pairs. In Proceedings of the 21st International Colloquium on Trees in Algebra and Programming, 1996. Lecture Notes in Computer Science 1059, pp. 211–225.
J.R. Hindley and J.P. Seldin. Introduction to Combinators and λ-Calculus. Cambridge University Press, 1986.
G. Huet. Confluent reductions: Abstract properties and applications to term rewriting systems. Journal of the Association for Computing Machinery, 27(4):797–821, 1980.
J.-P. Jouannaud and M. Okada. Executable higher-order algebraic specification languages. In Proceedings of the 6th IEEE Symposium on Logic in Computer Science, pages 350–361, 1991.
J.W. Klop. Combinatory Reduction Systems. PhD thesis, Rijks-universiteit, 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, chapter 1, 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. Nipkow and C. Prehofer. Higher-Order Rewriting and Equational Reasoning, volume I, pages 399–430. Kluwer, 1998.
T. Suzuki, A. Middeldorp, and T. Ida. Level-confluence of conditional rewrite systems with extra variables in right-hand sides. In Proceedings of the 6th International Conference on Rewriting Techniques and Applications, 1995. Lecture Notes in Computer Science 914, pp. 179–193.
J. van de Pol. Termination proofs for higher-order rewrite systems. In Proceedings of the 1st International Workshop on Higher-Order Algebra, Logic and Term Rewriting, 1994. Lecture Notes in Computer Science 816, pp. 305–325.
V. van Oostrom. Developing developments. Theoretical Computer Science, 175:159–181, 1997.
F. van Raamsdonk. Higher-order rewriting. In Proceedings of the 10th International Conference on Rewriting Techniques and Applications, 1999. Lecture Notes in Computer Science 1631, pp. 220–239.
H. Zantema. Termination of term rewriting: Interpretation and type elimination. Journal of Symbolic Computation, 17:23–50, 1994.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Yamada, T. (2001). Confluence and Termination of Simply Typed Term Rewriting Systems. In: Middeldorp, A. (eds) Rewriting Techniques and Applications. RTA 2001. Lecture Notes in Computer Science, vol 2051. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45127-7_25
Download citation
DOI: https://doi.org/10.1007/3-540-45127-7_25
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-42117-7
Online ISBN: 978-3-540-45127-3
eBook Packages: Springer Book Archive