Abstract
In this paper we study normalization properties of rewrite systems that are typeable using intersection types with ω and with sorts. We prove two normalization properties of typeable systems. On one hand, for all systems that satisfy a variant of the Jouannaud-Okada Recursion Scheme, every term typeable with a type that is not ω is head normalizable. On the other hand, non-Curryfied terms that are typeable with a type that does not contain ω, are normalizable.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
S. van Bakel. Complete restrictions of the Intersection Type Discipline. Theoretical Computer Science, 102:135–163, 1992.
S. van Bakel. Partial Intersection Type Assignment of Rank 2 in Applicative Term Rewriting Systems. Technical Report 92-03, Department of Computer Science, University of Nijmegen, 1992.
S. van Bakel. Partial Intersection Type Assignment in Applicative Term Rewriting Systems. In Proceedings of TLCA’ 93. International Conference on Typed Lambda Calculi and Applications, Utrecht, the Netherlands, volume 664 of LNCS, pages 29–44. Springer-Verlag, 1993.
S. van Bakel and M. Fernández. Strong Normalization of Typeable Rewrite Systems. In Proceedings of HOA’ 93. First International Workshop on Higher Order Algebra, Logic and Term Rewriting, Amsterdam, the Netherlands. Selected Papers, volume 816 of LNCS, pages 20–39. Springer-Verlag, 1994.
F. Barbanera and M. Fernández. Combining first and higher order rewrite systems with type assignment systems. In Proceedings of TLCA’ 93. International Conference on Typed Lambda Calculi and Applications, Utrecht, the Netherlands, volume 664 of LNCS, pages 60–74. Springer-Verlag, 1993.
F. Barbanera, M. Fernández, and H. Geuvers. Modularity of Strong Normalization and Confluence in the λ-algebraic-cube. In Proceedings of the ninth Annual IEEE Symposium on Logic in Computer Science, Paris, France, 1994.
H. Barendregt, M. Coppo, and M. Dezani-Ciancaglini. A filter lambda model and the completeness of type assignment. Journal of Symbolic Logic, 48(4), 1983.
H.B. Curry and R. Feys. Combinatory Logic, volume 1. North-Holland, Amsterdam, 1958.
N. Dershowitz and J.P. Jouannaud. Rewrite systems. In Handbook of Theoretical Computer Science, volume B, chapter 6, pages 245–320. North-Holland, 1990.
J.-Y. Girard, Y. Lafont, and P. Taylor. Proofs and Types. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1989.
J.P. Jouannaud and M. Okada. Executable higher-order algebraic specification languages. In Proceedings of the Sixth Annual IEEE Symposium on Logic in Computer Science, pages 350–361, 1991. 12. J.W. Klop. Term Rewriting Systems. In Handbook of Logic in Computer Science, volume 2, chapter 1, pages 1–116. Clarendon Press, 1992.
W.W. Tait. Intensional interpretation of functional of finite type I. Journal of Symbolic Logic, 32(2):198–223, 1967.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1995 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
van Bakel, S., Fernández, M. (1995). (Head-)normalization of typeable rewrite systems. In: Hsiang, J. (eds) Rewriting Techniques and Applications. RTA 1995. Lecture Notes in Computer Science, vol 914. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-59200-8_64
Download citation
DOI: https://doi.org/10.1007/3-540-59200-8_64
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-59200-6
Online ISBN: 978-3-540-49223-8
eBook Packages: Springer Book Archive