Skip to main content
SpringerLink
Log in

Weak and strong beta normalisations in typed λ-calculi

  • Conference paper
  • First Online:
Book cover Typed Lambda Calculi and Applications (TLCA 1997)

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

Included in the following conference series:

Abstract

We present translation techniques to study relations between weak and strong beta-normalisations in various typed lambda-calculi. We first introduce a translation which translates lambda-terms into lambda-I-terms, and show that every lambda-term is strongly beta-normalisable if and only if its translation is weakly beta-normalisable. We then prove that the translation preserves typability of lambda-terms in various typed lambda-calculi. This enables us to establish the equivalence between weak and strong beta-normalisations in these typed lambda-calculi. This translation can handle Curry typing as well as Church typing, strengthening some recent closely related results. This may bring some insights into answering whether weak and strong beta-normalisations in all pure type systems are equivalent.

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. H.P. Barendregt (1984), The Lambda Calculus: Its Syntax and Semantics, North-Holland Publishing Company, Amsterdam.

    Google Scholar 

  2. H.P. Barendregt (1992), Lambda calculi with types, in Handbook of Logic in Computer Science Vol. 2, edited by S. Abramsky, D. M. Gabbay and T.S.E. Maibaum, Clarendon Press, Oxford, pp. 117–309.

    Google Scholar 

  3. J.A. Bergstra and J.W. Klop (1982), Strong normalization and perpetual reductions in the lambda calculus, J. Inform. Process. Cybernet. 18, pp. 403–417.

    Google Scholar 

  4. A. Church, (1941), The Calculi of Lambda Conversion, Princeton University Press, Princeton.

    Google Scholar 

  5. Th. Coquand and G. Huét (1988), The calculus of constructions, Information and Computation vol. 76, pp. 95–120.

    Google Scholar 

  6. M. Coppo and M. Dezani-Ciancaglini (1980), An extension of basic functionality theory for the lambda-calculus, Notre Dame Journal of Formal Logic 21 (4), pp. 685–693.

    Google Scholar 

  7. M. Coppo, M. Dezani-Ciancaglini and B. Venneri (1981), Functional characters of solvable terms, Zeit. Math. Logik und Grundlagen der Math. 27 (1), pp. 45–58.

    Google Scholar 

  8. P. de Groote (1993), The conservation theorem revisited, Typed Lambda Calculi and Applications: TLCA'93, LNCS vol. 664, Springer, pp. 163–178.

    Google Scholar 

  9. R.O. Gandy (1980), An early proof of normalisation by A.M. Turing, in To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, Academic Press, pp. 453–456.

    Google Scholar 

  10. R.O. Gandy (1980), Proofs of strong normalisation, in To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, Academic Press, pp. 457–478.

    Google Scholar 

  11. J.-Y. Girard (1972), Interprétation Fonctionnelle et Élimination des Coupures de l'Arithmétique d'Ordre Supérieur, Thèse de Doctorat d'Etat, Université Paris VII.

    Google Scholar 

  12. H. Geuvers and M.J. Nederhof (1991), A modular proof of strong normalisation for the calculus of constructions, J. Functional Programming 1, 155–189.

    Google Scholar 

  13. R. Harper, F. Honsell and G. Plotkin (1987), A framework for defining logics. In Proc. Second Annual Symposium on Logic in Computer Science, I.E.E.E., Ithaca, N.Y., pages 194–204.

    Google Scholar 

  14. R. Harper and M. Lillibridge (1993), Explicit polymorphism and CPS conversion, In Proceedings of the Twentieth ACM Symposium on Principles of Programming Languages, pp. 206–209

    Google Scholar 

  15. R. Harper and M. Lillibridge (1993), Polymorphic type assignment and CPS conversion, LISP and Symbolic Computation, vol. 6, 3(4), pp. 361–380.

    Google Scholar 

  16. Stefan Kahrs (1995), Towards a Domain Theory for Termination Proofs, Laboratory for Foundation of Computer Science, Report 95-314, Department of Computer Science, The University of Edinburgh.

    Google Scholar 

  17. M. Karr (1985), “Delayability” in proofs of strong normalisabilities in the typed lambda-calculus, in Mathematical Foundation of Computer Software, edited by H. Ehrig, C. Floyd, M. Nïvat and J. Thatcher, LNCS vol. 185, Springer, pp. 208–222.

    Google Scholar 

  18. J.W. Klop (1980), Combinatory Reduction Systems, Ph.D. thesis, CWI, Amsterdam, Mathematical Center Tracts, No. 127.

    Google Scholar 

  19. J.W. Klop, (1992), Term rewriting systems, in Handbook of Logic in Computer Science Vol.2, edited by S. Abramsky, D. M. Gabbay and T.S.E. Maibaum, Clarendon Press, Oxford, pp. 1–116.

    Google Scholar 

  20. J.L. Krivine (1990), Lambda-calcul, Types et Modèles, Masson, Paris.

    Google Scholar 

  21. A.J. Kfoury and J.B. Wells (1994), New notions of reduction and non-semantic proofs of β-strong normalisation in typed λ-calculi, Tech. Rep. 94-104, Computer Science Department, Boston University.

    Google Scholar 

  22. R.P. Nederpelt (1973), Strong normalization in a typed lambda calculus with lambda structured types, Ph.D. thesis, Technische Hogeschool Eindhoven.

    Google Scholar 

  23. G. Plotkin (1975), Call-by-name, call-by-value, and the lambda calculus, Theoretical Computer Science, vol 1, pp. 125–159.

    Google Scholar 

  24. J. van de Pol (1994), Termination proofs for higher-order rewrite systems, in Higher Order Algebra, Logic and Term Rewriting, edited by J. Heering, K. Meinke, B. Möller and T. Nipkow, LNCS vol. 816, Springer, pp. 305–325.

    Google Scholar 

  25. J. van de Pol and H. Schwichtenberg (1995), Strict functionals for termination proofs, Typed lambda calculi and applications: TLCA '95, LNCS vol. 902, Springer, pp. 350–364.

    Google Scholar 

  26. D. Prawitz (1965), Natural Deduction: A proof theoretical study, Almquist & Wiksell publishing company, Stockholm.

    Google Scholar 

  27. D. Prawitz (1971), Ideas and results of proof theory, in Proceedings of the 2nd Scandinavian Logic Symposium, edited by J.E. Fenstad, North-Holland Publishing Company, Amsterdam.

    Google Scholar 

  28. J. Reynolds (1974), Towards a theory of type structure, Colloquium sur la Programmation, LNCS vol. 19, Springer, pp. 408–423.

    Google Scholar 

  29. H. Schwichtenberg (1991), An upper bound for reduction sequences in the typed lambda-calculus, Archive for Mathematical Logic, 30, 405–408.

    Google Scholar 

  30. M.H. Sørensen (1996), Strong Normalization from Weak Normalization by A-Translation in Typed lambda-Calculi, Manuscript announced on the types mailing list, February.

    Google Scholar 

  31. J. Springintveld (1993), Lower and upper bounds for reductions of types in λω and λP, in Typed lambda calculi and applications: TLCA'93, LNCS vol. 664, Springer, pp. 391–405.

    Google Scholar 

  32. P. Urzyczyn (1995), Positive recursive type assignment, in Mathematical Foundations of Computer Science, LNCS vol. 969, Springer, pp. 382–391.

    Google Scholar 

  33. H. Xi (1996), On weak and strong normalisations, Research Report 96-187, Department of Mathematical Sciences, Carnegie Mellon University, Pittsburgh.

    Google Scholar 

  34. H. Xi (1996), Upper bounds for standardisations and an application, Research Report 96-189, Department of Mathematical Sciences, Carnegie Mellon University, Pittsburgh.

    Google Scholar 

  35. H. Xi (1996), An induction measure on λ-terms and its applications, Research Report 96-192, Department of Mathematical Sciences, Carnegie Mellon University, Pittsburgh.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Mathematical Sciences, Carnegie Mellon University, 15213, Pittsburgh, PA, USA

    Hongwei Xi

Authors
  1. Hongwei Xi
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Philippe de Groote J. Roger Hindley

Rights and permissions

Reprints and permissions

Copyright information

© 1997 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Xi, H. (1997). Weak and strong beta normalisations in typed λ-calculi. In: de Groote, P., Roger Hindley, J. (eds) Typed Lambda Calculi and Applications. TLCA 1997. Lecture Notes in Computer Science, vol 1210. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-62688-3_48

Download citation

  • DOI: https://doi.org/10.1007/3-540-62688-3_48

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-62688-6

  • Online ISBN: 978-3-540-68438-1

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation