Abstract
A rewrite system is called uniformly normalising if all its steps are perpetual, i.e. are such that if s → t and s has an infinite reduction, then t has one too. For such systems termination (SN) is equivalent to normalisation (WN). A well-known fact is uniform normalisation of orthogonal non-erasing term rewrite systems, e.g. the λI-calculus. In the present paper both restrictions are analysed. Orthogonality is seen to pertain to the linear part and non-erasingness to the non-linear part of rewrite steps. Based on this analysis, a modular proof method for uniform normalisation is presented which allows to go beyond orthogonality. The method is shown applicable to biclosed first- and second-order term rewrite systems as well as to a λ-calculus with explicit substitutions.
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
F. Baader and T. Nipkow. Term Rewriting and All That. CUP, 1998.
H. Barendregt. The Lambda Calculus, Its Syntax and Semantics. NH, 1984.
Z. Benaissa, D. Briaud, P. Lescanne, and J. Rouyer-Degli. λv, a calculus of explicit substitutions which preserves strong normalisation. JFP, 6(5):699–722, 1996.
R. Bloo. Preservation of Termination for Explicit Substitution. PhD thesis, Technische Universiteit Eindhoven, 1997.
C. Böhm and B. Intrigila. The ant-lion paradigm for strong normalization. I&C, 114(1):30–49, 1994.
E. Bonelli. Perpetuality in a named lambda calculus with explicit substitutions. MSCS, to appear.
Alonzo Church. The Calculi of Lambda-Conversion. PUP, 1941.
Georges Gonthier, Jean-Jacques Lévy, and Paul-André Melliès. An abstract standardisation theorem. In LICS’92, pages 72–81, 1992.
Bernhard Gramlich. Termination and Confluence Properties of Structured Rewrite Systems. PhD thesis, Universität Kaiserslautern, 1996.
Gérard Huet. Confluent reductions: Abstract properties and applications to term rewriting systems. JACM, 27(4):797–821, 1980.
Gérard Huet and Jean-Jacques Lévy. Computations in orthogonal rewriting systems, I. In Computational Logic: Essays in Honor of Alan Robinson, pages 395–414. MIT Press, 1991.
Z. Khasidashvili. On the longest perpetual reductions in orthogonal expression reduction systems. TCS, To appear.
Z. Khasidashvili, M. Ogawa, and V. van Oostrom. Perpetuality and uniform normalization in orthogonal rewrite systems. I&C, To appear. http://www.phil.uu.nl/~oostrom/publication/ps/pun-icv2.ps.
Jan Willem Klop. Combinatory Reduction Systems. PhD thesis, Rijksuniversiteit Utrecht, 1980. Mathematical Centre Tracts 127.
J.W. Klop. Term rewriting systems. In Handbook of Logic in Computer Science, volume 2, pages 1–116. OUP, 1992.
Yves Lafont. From proof-nets to interaction nets. In Advances in Linear Logic, pages 225–247. CUP, 1995.
Richard Mayr and Tobias Nipkow. Higher-order rewrite systems and their confluence. Theoretical Computer Science, 192:3–29, 1998.
Paul-André Melliès. Description Abstraite des Systèmes de Réécriture. Thèse de doctorat, Université Paris VII, 1996.
Paul-André Melliès. Personal communication, 1999.
Vincent van Oostrom. Confluence for Abstract and Higher-Order Rewriting. Academisch proefschrift, Vrije Universiteit, Amsterdam, 1994.
Vincent van Oostrom. Development closed critical pairs. In HOA’95, volume 1074 of LNCS, pages 185–200. Springer, 1996.
Vincent van Oostrom. Normalisation in weakly orthogonal rewriting. In RTA’99, volume 1631 of LNCS, pages 60–74. Springer, 1999.
F. van Raamsdonk. Confluence and Normalisation for Higher-Order Rewriting. Academisch proefschrift, Vrije Universiteit, Amsterdam, 1996.
M.H. Sörensen. Effective longest and infinite reduction paths in untyped lambda-calculi. In CAAP’96, volume 1059 of LNCS, pages 287–301. Springer, 1996.
Yoshihito Toyama. Strong sequentiality of left-linear overlapping term rewriting systems. In LICS’92, pages 274–284, 1992.
J.B. Wells and Robert Muller. Standardization and evaluation in combinatory reduction systems, 2000. Working paper.
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
Khasidashvili, Z., Ogawa, M., van Oostrom, V. (2001). Uniform Normalisation beyond Orthogonality. 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_11
Download citation
DOI: https://doi.org/10.1007/3-540-45127-7_11
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