Abstract
We design a strategy that for any given term t in an Orthogonal Term Rewriting System (OTRS) constructs a longest reduction starting from t if t is strongly normalizable, and constructs an infinite reduction otherwise. For some classes of OTRSs the strategy is easily computable. We develop a method for finding the least upper bound of lengths of reductions starting from a strongly normalizable term. We give also some applications of our results.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
Barendregt H. P., Bergstra J., Klop J. W., Volken H. Some notes on lambdareduction, in: Degrees, reductions and representability in the lambda calculus. Preprint no.22, University of Utrecht, Department of mathematics, p. 13–53, 1976.
Courcelle B. Recursive Applicative Program Schemes. In: J.van Leeuwen ed. Handbook of Theoretical Computer Science, Chapter 9, vol.B, 1990, p. 459–492.
Dershowitz N., Jouannaud J.-P. Rewrite Systems. In: J.van Leeuwen ed. Handbook of Theoretical Computer Science, Chapter 6, vol.B, 1990, p. 243–320.
Huet G., Lévy J.-J. Computations in Orthogonal Rewriting Systems. In Computational Logic, Essays in Honour of Alan Robinson, ed. by J.-L. Lassez and G. Plotkin, MIT Press, 1991.
Khasidashvili Z. Optimal normalization in orthogonal term rewriting systems. In: Proc. of the fifth International Conference on Rewriting Techniques and Applications, Springer LNCS, vol. 690, C. Kirchner, ed. Montreal, 1993, p. 243–258.
Khasidashvili Z. On the equivalence of persistent term rewriting systems and recursive program schemes. In: Proc. of the second Israel Symposium on Theory and Computing Systems, Natanya, 1993, p. 240–249.
Khasidashvili Z. Perpetual reductions and strong normalization in orthogonal term rewriting systems. CWI Report CS-R9345, Amsterdam, July 1993.
Khasidashvili Z. Perpetual reductions in orthogonal combinatory reduction systems. CWI Report CS-R9349, Amsterdam, July 1993.
Klop J. W. Combinatory Reduction Systems. Mathematical Centre Tracts n. 127, CWI, Amsterdam, 1980.
Klop J. W. Term Rewriting Systems. In: S. Abramsky, D. Gabbay, and T. Maibaum eds. Handbook of Logic in Computer Science, vol. II, Oxford University Press, 1992, p. 1–116.
Nederpelt R. P. Strong normalization for a typed lambda-calculus with lambda structured types. Ph. D. Thesis, Eindhoven, 1973.
O'Donnell M. J. Computing in systems described by equations. Springer LNCS 58, 1977.
Van Raamsdonk F. A simple proof of confluence for weakly orthogonal combinatory reduction Systems. Report CS-R9234, CWI Amsterdam, 1992.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1994 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Khasidashvili, Z. (1994). Perpetuality and strong normalization in orthogonal term rewriting systems. In: Enjalbert, P., Mayr, E.W., Wagner, K.W. (eds) STACS 94. STACS 1994. Lecture Notes in Computer Science, vol 775. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-57785-8_139
Download citation
DOI: https://doi.org/10.1007/3-540-57785-8_139
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-57785-0
Online ISBN: 978-3-540-48332-8
eBook Packages: Springer Book Archive