Skip to main content
SpringerLink
Log in
Book cover

International Conference on Typed Lambda Calculi and Applications

TLCA 1999: Typed Lambda Calculi and Applications pp 325–339Cite as

Characterising Explicit Substitutions which Preserve Termination

  • Conference paper
  • First Online:

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

Abstract

Contrary to all expectations, the λσ-calculus, the canonical simply-typed lambda-calculus with explicit substitutions, is not strongly normalising. This result has led to a proliferation of calculi with explicit substitutions. This paper shows that the reducibility method provides a general criterion when a calculus of explicit substitution is strongly normalising for all untyped lambda-terms that are strongly normalising. This result is general enough to imply preservation of strong normalisation of the calculi considered in the literature. We also propose a version of the λσ-calculus with explicit substitutions which is strongly normalising for strongly normalising λ-terms.

Research supported by EPSRC-grant GR/L28296 under the title “The eXplicit Substitution Linear Abstract Machine”.

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

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Martin Abadi, Luca Cardelli, Pierre-Louis Curien, and Jean-Jaques Lévy. Explicit substitutions. Journal of Functional Programming, 1(4):375–416, 1991.

    Article  MATH  MathSciNet  Google Scholar 

  2. Z.-E.A. Benaissa, D. Briaud, P. Lescanne, and J. Rouyer-Degli. λυ, a calculus of explicit substitutions which preserves strong normalisation. Journal of Functional Programming, 6(5), 1996.

    Google Scholar 

  3. R. Bloo and H. Geuvers. Explicit substitutions: on the edge of strong normalization. To appear in Theoretical Computer Science, 1998.

    Google Scholar 

  4. R. Bloo and K.H. Rose. Preservation of strong normalisation in named lambda calculi with explicit substitution and garbage collection. In Proc. CSN’95-Computer Science in the Netherlands, pages 62–72, 1995.

    Google Scholar 

  5. P.-L. Curien, Th. Hardin, and J.-J. Lévy. Confluence properties of weak and strong calculi of explicit substitutions. Journal of the ACM, 43:362–397, March 1996.

    Article  MATH  MathSciNet  Google Scholar 

  6. R. Di Cosmo and D. Kesner. Strong normalization of explicit substitutions via cut-elimination in proof nets. In Proc. of 12th IEEE Symp. on Logic in Computer Science, pages 35–47, 1997.

    Google Scholar 

  7. M.C. Ferreira, D. Kesner, and L. Puel. λ-calculi with explicit substitutions and compositions which preserve β-strong normalization (extended abstract). In Proc. of 5th Int. Conf. on Algebraic and Logic Programming (ALP), volume 1139 of Lecture Notes in Computer Science, pages 248–298, 1996.

    Google Scholar 

  8. N. Ghani. Adjoint Rewriting. PhD thesis, University of Edinburgh, 1995.

    Google Scholar 

  9. Thérèse Hardin. Confluence results for the pure strong categorical logic CCL. λ-calculi as subsystems of CCL. Theoretical Computer Science, 65:291–342, 1989.

    Article  MATH  MathSciNet  Google Scholar 

  10. F. Kamareddine and A. Rios. Extending a lambda-calculus with explicit substitutions which preserves strong normalisation into a confluent calculus on open terms. Journal of Functional Programming, 7(4):395–420, 1997.

    Article  MATH  MathSciNet  Google Scholar 

  11. F. Lang and K.H. Rose. Two equivalent calculi of explicit substitution with confluence on meta-terms and preservation of strong normalisation (one with names and one first order). In Proc. of Westapp’98, 1998.

    Google Scholar 

  12. P.-A. Mellies. Typed λ-calculi with explicit substitution may not terminate. In Proc. of TLCA’95, pages 328–334. LNCS 902, 1995.

    Google Scholar 

  13. C. Munoz. Confluence and preservation of strong normalisation in an explicit substitution calculus. In Proc. of 11th IEEE Symp. on Logic in Computer Science, pages 440–447, 1996.

    Google Scholar 

  14. E. Ritter and V. de Paiva. On explicit substitution and names (extended abstract). In Proc. of ICALP’97, LNCS 1256, pages 248–258, 1997.

    Google Scholar 

  15. Eike Ritter. Normalization for typed lambda calculi with explicit substitution. In Proc. of CSL’93, pages 295–304. LNCS 832, 1994.

    Google Scholar 

  16. K.H. Rose. Explicit substitution-tutorial & survey. Lecture series LS-96-3, BRICS, Department of Computer Science, University of Aarhus, 1996.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. School of Computer Science, University of Birmingham, Birmingham, UK

    Eike Ritter

Authors
  1. Eike Ritter
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. CNRS - UPR9016, Institut de Mathématiques de Luminy, 163 Avenue de Luminy, case 907, F-13288, Marseille cedex 9, France

    Jean-Yves Girard

Rights and permissions

Reprints and permissions

Copyright information

© 1999 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Ritter, E. (1999). Characterising Explicit Substitutions which Preserve Termination. In: Girard, JY. (eds) Typed Lambda Calculi and Applications. TLCA 1999. Lecture Notes in Computer Science, vol 1581. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48959-2_23

Download citation

  • DOI: https://doi.org/10.1007/3-540-48959-2_23

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-65763-7

  • Online ISBN: 978-3-540-48959-7

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation