Abstract
In this paper we review some well-known theory about reduction strategies of various kinds: normalizing, outermost-fair, cofinal, Church-Rosser. A stumbling block in the definition of such strategies is the presence of reduction cycles that may ‘trap’ a strategy as it is memory-free. We exploit a recently (re)discovered fact that there are no reduction cycles in orthogonal rewrite systems when each term has a normal form, in order to enhance some of the theorems on strategies, both with respect to their scope and the proof of their correctness.
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
Antoy, S., Middeldorp, A.: A sequential reduction strategy. Theoretical Computer Science 165(1), 75–95 (1996)
Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998)
Barendregt, H.P.: The Lambda Calculus, its Syntax and Semantic, of Studies in Logic and the Foundations of Mathematics, 2nd edn., vol. 103. North-Holland, Amsterdam (1984)
Barendregt, H.P., Bergstra, J.A., Klop, J.W., Volken, H.: Degrees, reductions and representability in the lambda calculus. Technical Report 22, Utrecht University (February 1976)
Bergstra, J.A., Klop, J.W.: Church-Rosser strategies in the lambda calculus. Theoretical Computer Science 9(1), 27–38 (1979)
Kennaway, J.R.: Sequential evaluation strategies for parallel-or and related reduction systems. Annals of Pure and Applied Logic 43, 31–56 (1989)
Ketema, J., Klop, J.W., van Oostrom, V.: Vicious circles in orthogonal term rewriting systems. In: Antoy, S., Toyama, Y. (eds.) WRS 2004. Proceedings of the 4th International Workshop on Reduction Strategies in Rewriting and Programming. Electronic Notes in Theoretical Computer Science, vol. 124, pp. 65–77. Elsevier, North-Holland, Amsterdam (2005)
Ketema, J., Klop, J.W., van Oostrom, V.: Vicious circles in rewriting systems. In: DiCosmo, R., Toyama, Y. (eds.): WRS 2005. Proceedings of the 5th International Workshop on Reduction Strategies in Rewriting and Programming (2005)
Klop, J.W.: Reduction cycles in Combinatory Logic. In: Hindley, J.R., Seldin, J.P. (eds.) To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pp. 193–214. Academic Press, San Diego (1980) Also available via http://web.mac.com/janwillemklop/iWeb/Site/Bibliography.html
Middeldorp, A., Ohsaki, H.: Type introduction for equational rewriting. Acta Informatica 36(12), 1007–1029 (2000)
Nipkow, T.: Higher-order critical pairs. In: Proceedings of the 6th annual IEEE Symposium on Logic in Computer Science (LICS 1991), pp. 342–349, Amsterdam, The Netherlands (July 1991)
O’Donnell, M.J.: Computing in Systems Described by Equations. LNCS, vol. 58. Springer, Heidelberg (1977)
van Oostrom, V.: Normalisation in weakly orthogonal rewriting. In: Narendran, P., Rusinowitch, M. (eds.) RTA 1999. LNCS, vol. 1631, pp. 60–74. Springer, Heidelberg (1999)
Statman, R.: Effective reduction and conversion strategies for combinators. In: Comon, H. (ed.) Rewriting Techniques and Applications. LNCS, vol. 1232, pp. 203–213. Springer, Heidelberg (1997)
Terese,: Term Rewriting Systems. In: Cambridge Tracts in Theoretical Computer Science, vol. 55, Cambridge University Press, Cambridge, UK (2003)
Toyama, Y.: Reduction strategies for left-linear term rewriting systems. In: Middeldorp, A., van Oostrom, V., van Raamsdonk, F., de Vrijer, R. (eds.) Processes, Terms and Cycles: Steps on the Road to Infinity. LNCS, vol. 3838, pp. 198–223. Springer, Heidelberg (2005)
Waldmann, J.: The combinator S. Information and Computation 159, 2–21 (2000)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Klop, J.W., van Oostrom, V., van Raamsdonk, F. (2007). Reduction Strategies and Acyclicity. In: Comon-Lundh, H., Kirchner, C., Kirchner, H. (eds) Rewriting, Computation and Proof. Lecture Notes in Computer Science, vol 4600. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-73147-4_5
Download citation
DOI: https://doi.org/10.1007/978-3-540-73147-4_5
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-73146-7
Online ISBN: 978-3-540-73147-4
eBook Packages: Computer ScienceComputer Science (R0)