Abstract
A rewrite sequence is said to be outermost-fair if every outermost redex occurrence is eventually eliminated. O'Donnell has shown that outermost-fair rewriting is normalising for almost orthogonal first-order term rewriting systems. In this paper we extend this result to the higher-order case.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
Yohji Akama. On Mints' reduction for ccc-calculus. In M. Bezem and J.F. Groote, editors, Proceedings of the International Conference on Typed Lambda Calculi and Applications (TLCA '93), pages 1–12, Utrecht, The Netherlands, March 1993. Volume 664 of Lecture Notes in Computer Science.
H.P. Barendregt. Lambda calculi with types. In S. Abramsky, Dov M. Gabbay, and T.S.E Maibaum, editors, Handbook of Logic in Computer Science, volume 2, pages 117–310. Oxford University Press, New York, 1992.
J.A. Bergstra and J.W. Klop. Conditional rewrite rules: Confluence and termination. Journal of Computer and System Sciences, 32:323–362, 1986.
Haskell B. Curry, Robert Feys, and William Craig. Combinatory Logic, volume I. Studies in Logic and the Foundations of Mathematics. North-Holland Publishing Company, Amsterdam, 1958.
Michael Hanus and Christian Prehofer. Higher-order narrowing with definitional trees. In Harald Ganzinger, editor, Proceedings of the 7th International Conference on Rewriting Techniques and Applications (RTA '96), volume 1103 of Lecture Notes in Computer Science, pages 138–152, New Brunswick, USA, 1996.
Gérard Huet. Confluent reductions: Abstract properties and applications to term rewriting systems. Journal of the Association for Computing Machinery, 27(4):797–821, October 1980.
Dale Miller. A logic programming language with lambda-abstraction, function variables, and simple unification. Journal of Logic and Computation, 1(4):497–536, 1991.
Richard Mayr and Tobias Nipkow. Higher-order rewrite systems and their confluence. Technical Report TUM-I9433, Technische Universität München, August 1994.
Tobias Nipkow. Higher-order critical pairs. In Proceedings of the sixth annual IEEE Symposium on Logic in Computer Science (LICS '91), pages 342–349, Amsterdam, The Netherlands, July 1991.
Michael J. O'Donnell. Computing in Systems Described by Equations, volume 58 of Lecture Notes in Computer Science. Springer Verlag, 1977.
Vincent van Oostrom. Confluence for Abstract and Higher-Order Rewriting. PhD thesis, Vrije Universiteit, Amsterdam, March 1994. Available at http://www.cs.vu.nl/∼oostrom.
Vincent van Oostrom. Higher-order families. In Harald Ganzinger, editor, Proceedings of the 7th International Conference on Rewriting Techniques and Applications (RTA '96), volume 1103 of Lecture Notes in Computer Science, pages 392–407, New Brunswick, USA, 1996.
Vincent van Oostrom. Personal communication, 1996.
Vincent van Oostrom and Femke van Raamsdonk. Weak orthogonality implies confluence: the higher-order case. In A. Nerode and Yu.V. Matiyasevich, editors, Proceedings of the Third International Symposium on Logical Foundations of Computer Science (LFCS '94), volume 813 of Lecture Notes in Computer Science, pages 379–392, St. Petersburg, July 1994.
Femke van Raamsdonk. Confluence and Normalisation for Higher-Order Rewriting. PhD thesis, Vrije Universiteit, Amsterdam, May 1996. Available at http://www.cwi.nl/∼femke.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
van Raamsdonk, F. (1997). Outermost-fair rewriting. In: de Groote, P., Roger Hindley, J. (eds) Typed Lambda Calculi and Applications. TLCA 1997. Lecture Notes in Computer Science, vol 1210. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-62688-3_42
Download citation
DOI: https://doi.org/10.1007/3-540-62688-3_42
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-62688-6
Online ISBN: 978-3-540-68438-1
eBook Packages: Springer Book Archive