Skip to main content
SpringerLink
Log in

Eta-expansions in F ω

  • Conference paper
  • First Online:
Computer Science Logic (CSL 1996)

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

Included in the following conference series:

Abstract

The use of expansionary η-rewrite rules in typed λ-calculi has become increasingly common in recent years as their advantages over contractive η-rewrite rules have become more apparent. Not only does one obtain simultaneously the decidability of βη-equality and a natural construction of the long βη-normal forms, but rewrite relations using expansions retain key properties when combined with first order rewrite systems, generalise more easily to other type constructors and are supported by a categorical theory of reduction.

However, one area where η-contractions have until now remained the only possibility is in the more powerful type theories of the λ-cube. This paper begins to rectify this situation by considering a higher order polymorphic λ-calculus known as F ω.

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. Y. Akama. On Mints' reduction for ccc-calculus. In Typed λ-Calculus and Applications, volume 664 of Lecture Notes in Computer Science, pages 1–12. Springer Verlag, 1993.

    Google Scholar 

  2. H. Barendregt. The Lambda Calculus: Its Syntax and Semantics (revised edition). Number 103 in Studies in Logic and the Foundations of Mathematics. North Holland, 1984.

    Google Scholar 

  3. V. Breazu-Tannen and J. Gallier. Polymorphic rewriting preserves algebraic strong normalisation. Theoretical Computer Science, 83:3–28, 1991.

    Google Scholar 

  4. V. Breazu-Tannen and J. Gallier. Polymorphic rewriting preserves algebraic confluence. Information and Computation, 114:1–29, 1994.

    Google Scholar 

  5. R. Di Cosmo and D. Kesner. Simulating expansions without expansions. Mathematical Structures in Computer Science, 4:1–48, 1994.

    Google Scholar 

  6. R. Di Cosmo and D. Kesner. Combining algebraic rewriting, extensional λ-calculi and fixpoints. In TCS, 1995.

    Google Scholar 

  7. D. Dougherty. Some λ-calculi with categorical sums and products. In Rewriting Techniques and Applications, volume 690 of Lecture Notes in Computer Science, pages 137–151. Springer Verlag, 1993.

    Google Scholar 

  8. G. Dowek. On the defintion of the η-long normal form in type systems of the cube. Informal proceedings of the 1993 Workshop on Types for Proofs and Programs, 1993.

    Google Scholar 

  9. J. Gallier. On girard's candidats de reductibilite. Logic and Computer Science, pages 123–203, 1990.

    Google Scholar 

  10. H. Geuvers. The Church-Rosser property for βη-reduction in typed λ-calculi. In LICS, pages 453–460. IEEE, 1992.

    Google Scholar 

  11. N. Ghani. Adjoint Rewriting. PhD thesis, University of Edinburgh, Department of Computer Science, 1995.

    Google Scholar 

  12. N. Ghani. βη-equality for coproducts. In Typed λ-calculus and Applications, number 902 in Lecture Notes in Computer Science, pages 171–185. Springer Verlag, 1995.

    Google Scholar 

  13. G. Huet. Résolution d'équations dans des langages d'ordre 1,2,⋯, ω. Thése d'Etat, Université de Paris VII, 1976.

    Google Scholar 

  14. C. B. Jay. Modelling reduction in confluent categories. In Applications of Categories in Computer Science, volume 177. London Mathematical Society Lecture Note Series, 1992.

    Google Scholar 

  15. C. B. Jay and N. Ghani. The virtues of eta-expansion. Journal of Functional Programming, Volume 5(2), April 1995, pages 135–154. CUP 1995.

    Google Scholar 

  16. G. E. Mints. Teorija categorii i teoria dokazatelstv.i. Aktualnye problemy logiki i metodologii nauky, pages 252–278, 1979.

    Google Scholar 

  17. D. Prawitz. Ideas and results in proof theory. In J.E. Fenstad, editor, Proc. 2nd Scandinavian Logic Symposium, pages 235–307. North Holland, 1971.

    Google Scholar 

  18. R. A. G. Seely. Modelling computations: A 2-categorical framework. In Proc. 2nd Annual Symposium on Logic in Computer Science. IEEE publications, 1987.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Ecole Normale Superieure, LIENS-DMI, 45, Rue D'Ulm, 75230, Paris Cedex 05, France

    Neil Ghani

Authors
  1. Neil Ghani
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Dirk van Dalen Marc Bezem

Rights and permissions

Reprints and permissions

Copyright information

© 1997 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Ghani, N. (1997). Eta-expansions in F ω . In: van Dalen, D., Bezem, M. (eds) Computer Science Logic. CSL 1996. Lecture Notes in Computer Science, vol 1258. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-63172-0_39

Download citation

  • DOI: https://doi.org/10.1007/3-540-63172-0_39

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-63172-9

  • Online ISBN: 978-3-540-69201-0

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation