Skip to main content
SpringerLink
Log in
Book cover

International Symposium on Programming Language Implementation and Logic Programming

PLILP 1996: Programming Languages: Implementations, Logics, and Programs pp 378–392Cite as

Generalized β-reduction and explicit substitutions

  • λ-Calculus and Rewriting
  • Conference paper
  • First Online:

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

Abstract

Extending the λ-calculus with either explicit substitution or generalised reduction has been the subject of extensive research recently which still has many open problems. Due to this reason, the properties of a calculus combining both generalised reduction and explicit substitutions have never been studied. This paper presents such a calculus λsg and shows that it is a desirable extension of the λ-calculus. In particular, we show that λsg preserves strong normalisation, is sound and it simulates classical β-reduction. Furthermore, we study the simply typed λ-calculus extended with both generalised reduction and explicit substitution and show that well-typed terms are strongly normalising and that other properties such as subtyping and subject reduction hold.

This work was carried out under EPSRC grant GR/K25014.

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

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. M. Abadi, L. Cardelli, P.-L. Curien, and J.-J. Lévy. Explicit Substitutions. Journal of Functional Programming, 1(4):375–416, 1991.

    Google Scholar 

  2. Z.M. Ariola, M. Felleisen, J. Maraist, M. Odersky, and P. Wadler. A call by need lambda calculus. Conf. Rec. 22nd Ann. ACM Symp. Princ. Program. Lang. ACM, 1995.

    Google Scholar 

  3. H. Barendregt. λ-calculi with types. Handbook of Logic in Computer Science, II, 1992.

    Google Scholar 

  4. Z. Benaissa, D. Briaud, P. Lescanne, and J. Rouyer-Degli. λν, a calculus of explicit substitutions which preserves strong normalisation. Personal communication, 1995.

    Google Scholar 

  5. R. Bloo. Preservation of Strong Normalisation for Explicit Substitution. Technical Report 95-08, Department of Mathematics and Computing Science, Eindhoven University of Technology, 1995.

    Google Scholar 

  6. R. Bloo, F. Kamareddine, and R. Nederpelt. The Barendregt Cube with Definitions and Generalised Reduction. Information and Computation, 126 (2):123–143, 1996.

    Google Scholar 

  7. R. Constable et al. Implementing Mathematics with the NUPRL Development System. Prentice-Hall, 1986.

    Google Scholar 

  8. P.-L. Curien. Categorical Combinators, Sequential Algorithms and Functional Programming. Pitman, 1986. Revised edition: Birkhäuser (1993).

    Google Scholar 

  9. P.-L. Curien, T. Hardin, and J.-J. Lévy. Confluence properties of weak and strong calculi of explicit substitutions. Technical Report RR 1617, INRIA, Rocquencourt, 1992.

    Google Scholar 

  10. N. G. de Bruijn. A namefree lambda calculus with facilities for internal definition of expressions and segments. Technical Report TH-Report 78-WSK-03, Department of Mathematics, Eindhoven University of Technology, 1978.

    Google Scholar 

  11. P. de Groote. The conservation theorem revisited. Int'l Conf. Typed Lambda Calculi and Applications LNCS, 664, 1993.

    Google Scholar 

  12. G. Dowek et al. The coq proof assistant version 5.6, users guide. Technical Report 134, INRIA, 1991.

    Google Scholar 

  13. F. Kamareddine. A reduction relation for which postponement of k-contractions, conservation and preservation of strong normalisation hold. Technical report, Glasgow University, 1996.

    Google Scholar 

  14. F. Kamareddine and R. Nederpelt. A useful λ-notation. Theoretical Computer Science, 155:85–109, 1996.

    Google Scholar 

  15. F. Kamareddine and R. P. Nederpelt. On stepwise explicit substitution. International Journal of Foundations of Computer Science, 4(3):197–240, 1993.

    Google Scholar 

  16. F. Kamareddine and R. P. Nederpelt. Generalising reduction in the λ-calculus. Journal of Functional Programming, 5(4):637–651, 1995.

    Google Scholar 

  17. F. Kamareddine and A. Ríos. A λ-calculus à la de Bruijn with explicit substitutions. Proceedings of PLILP'95. LNCS, 982:45–62, 1995.

    Google Scholar 

  18. F. Kamareddine and A. Ríos. The λs-calculus: its typed and its extended versions. Technical report, Department of Computing Science, University of Glasgow, 1995.

    Google Scholar 

  19. F. Kamareddine and A. Ríos. Extending a λ-calculus with Explicit Substitution which preserves Strong Normalisation into a Confluent Calculus on Open Terms. Journal of Functional Programming, 1996. To appear.

    Google Scholar 

  20. F. Kamareddine and A. Ríos. Generalised β-reduction and explicit substitutions. Technical Report TR-1996-21, Department of Computing Science, University of Glasgow, 1996.

    Google Scholar 

  21. M. Karr. Delayability in proofs of strong normalizability in the typed λ-calculus. Mathematical Foundations of Computer Software, LNCS, 185, 1985.

    Google Scholar 

  22. A.J. Kfoury, J. Tiuryn, and P. Urzyczyn. An analysis of ML typability. ACM, 41(2):368–398, 1994.

    Google Scholar 

  23. A.J. Kfoury and J.B. Wells. A direct algorithm for type inference in the rank-2 fragment of the second order λ-calculus. Proc. 1994 ACM Conf. LISP Funct. Program., 1994.

    Google Scholar 

  24. A.J. Kfoury and J.B. Wells. Addendum to new notions of reduction and nonsemantic proofs of β-strong normalisation in typed λ-calculi. Technical report, Boston University, 1995.

    Google Scholar 

  25. A.J. Kfoury and J.B. Wells. New notions of reductions and non-semantic proofs of β-strong normalisation in typed λ-calculi. LICS, 1995.

    Google Scholar 

  26. Z. Khasidashvili. The longest perpetual reductions in orthogonal expression reduction systems. Proc. of the 3rd International Conference on Logical Foundations of Computer Science, Logic at St Petersburg, 813, 1994.

    Google Scholar 

  27. J. W. Klop. Combinatory Reduction Systems. Mathematical Center Tracts, 27, 1980.

    Google Scholar 

  28. P.-A. Melliès. Typed λ-calculi with explicit substitutions may not terminate in Proceedings of TLCA'95. LNCS, 902, 1995.

    Google Scholar 

  29. C. A. Muñoz Hurtado. Confluence and preservation of strong normalisation in an explicit substitutions calculus. Technical Report 2762, INRIA, Rocquencourt, December 1995.

    Google Scholar 

  30. R. P. Nederpelt, J. H. Geuvers, and R. C. de Vrijer. Selected papers on Automath. North-Holland, Amsterdam, 1994.

    Google Scholar 

  31. S.L. Peyton-Jones. The Implementation of Functional Programming Languages. Prentice-Hall, 1987.

    Google Scholar 

  32. L. Regnier. Lambda calcul et réseaux. PhD thesis, Paris 7, 1992.

    Google Scholar 

  33. L. Regnier. Une équivalence sur les lambda termes. Theoretical Computer Science, 126:281–292, 1994.

    Google Scholar 

  34. A. Ríos. Contribution à l'étude des λ-calculs avec substitutions explicites. PhD thesis, Université de Paris 7, 1993.

    Google Scholar 

  35. A. Sabry and M. Felleisen. Reasoning about programs in continuation-passing style. Proc. 1992 ACM Conf. LISP Funct. Program., pages 288–298, 1992.

    Google Scholar 

  36. M. Sørensen. Strong normalisation from weak normalisation in typed λ-calculi. Submitted.

    Google Scholar 

  37. D. Vidal. Nouvelles notions de réduction en lambda calcul. PhD thesis, Université de Nancy 1, 1989.

    Google Scholar 

  38. H. Xi. On weak and strong normalisations. Technical Report 96-187, Carnegie Mellon University, 1996.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computing Science, University of Glasgow, 17 Lilybank Gardens, G12 8QQ, Glasgow, Scotland

    Fairouz Kamareddine & Alejandro Ríos

Authors
  1. Fairouz Kamareddine
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Alejandro Ríos
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Herbert Kuchen S. Doaitse Swierstra

Rights and permissions

Reprints and permissions

Copyright information

© 1996 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Kamareddine, F., Ríos, A. (1996). Generalized β-reduction and explicit substitutions. In: Kuchen, H., Doaitse Swierstra, S. (eds) Programming Languages: Implementations, Logics, and Programs. PLILP 1996. Lecture Notes in Computer Science, vol 1140. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-61756-6_98

Download citation

  • DOI: https://doi.org/10.1007/3-540-61756-6_98

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-61756-3

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

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation