Skip to main content
SpringerLink
Log in

Approximation and normalization results for typeable term rewriting systems

  • Conference paper
  • First Online:
Higher-Order Algebra, Logic, and Term Rewriting (HOA 1995)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 1074))

Abstract

We consider an intersection type assignment system for term rewriting systems extended with application, and define a notion of (finite) approximation on terms. We then prove that for typeable rewrite systems satisfying a general scheme for recursive definitions, every typeable term has an approximant of the same type. This approximation result, and the proof technique developed to obtain it, allow us to deduce in a direct way a head-normalization, a normalization, and a strong normalization theorem, for different classes of typeable terms.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Z. Ariola, R. Kennaway, J.W. Klop, R. Sleep, and F-J. de Vries. Syntactic definitions of undefined: on defining the undefined. In TACS '94, LNCS, 789, pages 543–554, 1994.

    Google Scholar 

  2. S. van Bakel. Complete restrictions of the Intersection Type Discipline. Theoretical Computer Science, 102:135–163, 1992.

    Google Scholar 

  3. S. van Bakel. Partial Intersection Type Assignment in Applicative Term Rewriting Systems. In TLCA '93, LNCS 664, pages 29–44, 1993.

    Google Scholar 

  4. S. van Bakel. Principal type schemes for the Strict Type Assignment System. Logic and Computation, 3(6):643–670, 1993.

    Google Scholar 

  5. S. van Bakel. Rank 2 Intersection Type Assignment in Term Rewriting Systems. Fundamenta Informaticae, 1996. To appear.

    Google Scholar 

  6. S. van Bakel and M. Fernández. Strong Normalization of Typeable Rewrite Systems. In HOA '93, LNCS 816, pages 20–39, 1994.

    Google Scholar 

  7. S. van Bakel and M. Fernández. (Head)-Normalization of Typeable Rewrite Systems. RTA '95, LNCS 914, pages 279–293, 1995.

    Google Scholar 

  8. H. Barendregt, M. Coppo, and M. Dezani-Ciancaglini. A filter lambda model and the completeness of type assignment. Journal of Symbolic Logic, 48(4):931–940, 1983.

    Google Scholar 

  9. F. Cardone and M. Coppo. Two Extensions of Curry's Type Inference System. In Logic and Computer Science, pages 19–75, 1990.

    Google Scholar 

  10. M. Coppo and M. Dezani-Ciancaglini. An Extension of the Basic Functionality Theory for the λ-Calculus. Notre Dame Journal of Formal Logic, 21(4):685–693, 1980.

    Google Scholar 

  11. H.B. Curry and R. Feys. Combinatory Logic, volume 1, 1958.

    Google Scholar 

  12. N. Dershowitz and J.P. Jouannaud. Rewrite systems. In Handbook of Theoretical Computer Science, volume B, chapter 6, pages 245–320, 1990.

    Google Scholar 

  13. M. Dezani-Ciancaglini and J.R. Hindley. Intersection types for combinatory logic. Theoretical Computer Science, 100:303–324, 1992.

    Google Scholar 

  14. J.-Y. Girard, Y. Lafont, and P. Taylor. Proofs and Types. Cambridge Tracts in Theoretical Computer Science, 1989.

    Google Scholar 

  15. G. Huet and J.J. Lévy. Computations in Orthogonal Rewriting Systems. In Computational Logic. Essays in Honour of Alan Robinson, 1991.

    Google Scholar 

  16. J.P. Jouannaud and M. Okada. Executable higher-order algebraic specification languages. In LiCS '91, pages 350–361, 1991.

    Google Scholar 

  17. R. Kennaway, V. van Oostrom, and F.J. de Vries. Meaningless terms in rewriting. Submitted for publication. Obtainable as: http://wwwbroy.informatik.tumuenchen.de/oostrom, 1996.

    Google Scholar 

  18. J.W. Klop. Term Rewriting Systems. In Handbook of Logic in Computer Science, volume 2, chapter 1, pages 1–116, 1992.

    Google Scholar 

  19. D. Leivant. Typing and computational properties of lambda expressions. Theoretical Computer Science, 44:51–68, 1986.

    Google Scholar 

  20. F. Pfenning. Partial Polymorphic Type Inference and Higher-Order Unification. In LISP and Functional Programming Languages '88, pages 153–163, 1988.

    Google Scholar 

  21. W.W. Tait. Intensional interpretation of functional of finite type I. Journal of Symbolic Logic, 32(2):198–223, 1967.

    Google Scholar 

  22. S.R. Thatte. Full Abstraction and Limiting Completeness in Equational Languages. Theoretical Computer Science, 65:85–119, 1989.

    Google Scholar 

  23. C.P. Wadsworth. The relation between computational and denotational properties for Scott's D∞-models of the lambda-calculus. SIAM J. Comput., 5:488–521, 1976.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computing, Imperial College, 180 Queens Gate, SW7 2BZ, London

    Steffen van Bakel

  2. École Normale Supérieure, DMI-LIENS (CNRS URA 1327), 45 Rue d'Ulm, 75005, Paris, France

    Maribel Fernández

Authors
  1. Steffen van Bakel
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Maribel Fernández
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Gilles Dowek Jan Heering Karl Meinke Bernhard Möller

Rights and permissions

Reprints and permissions

Copyright information

© 1996 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

van Bakel, S., Fernández, M. (1996). Approximation and normalization results for typeable term rewriting systems. In: Dowek, G., Heering, J., Meinke, K., Möller, B. (eds) Higher-Order Algebra, Logic, and Term Rewriting. HOA 1995. Lecture Notes in Computer Science, vol 1074. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-61254-8_17

Download citation

  • DOI: https://doi.org/10.1007/3-540-61254-8_17

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-61254-4

  • Online ISBN: 978-3-540-68389-6

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation