Complexity of Strongly Normalising λ-Terms via Non-idempotent Intersection Types

  • Alexis Bernadet
  • Stéphane Lengrand
Part of the Lecture Notes in Computer Science book series (LNCS, volume 6604)

Abstract

We present a typing system for the λ-calculus, with non-idempotent intersection types. As it is the case in (some) systems with idempotent intersections, a λ-term is typable if and only if it is strongly normalising. Non-idempotency brings some further information into typing trees, such as a bound on the longest β-reduction sequence reducing a term to its normal form.

We actually present these results in Klop’s extension of λ-calculus, where the bound that is read in the typing tree of a term is refined into an exact measure of the longest reduction sequence.

This complexity result is, for longest reduction sequences, the counterpart of de Carvalho’s result for linear head-reduction sequences.

References

  1. [Abr93]
    Abramsky, S.: Computational interpretations of linear logic. Theoret. Comput. Sci. 111, 3–57 (1993)MathSciNetCrossRefGoogle Scholar
  2. [BBdH93]
    Benton, N., Bierman, G., de Paiva, V., Hyland, M.: A term calculus for intuitionistic linear logic. In: Bezem, M., Groote, J.F. (eds.) TLCA 1993. LNCS, vol. 664, pp. 75–90. Springer, Heidelberg (1993)CrossRefGoogle Scholar
  3. [BCDC83]
    Barendregt, H., Coppo, M., Dezani-Ciancaglini, M.: A filter lambda model and the completeness of type assignment. J. of Symbolic Logic 48(4), 931–940 (1983)MathSciNetCrossRefGoogle Scholar
  4. [BEM10]
    Bucciarelli, A., Ehrhard, T., Manzonetto, G.: Categorical models for simply typed resource calculi. ENTCS 265, 213–230 (2010)MathSciNetMATHGoogle Scholar
  5. [BM03]
    Baillot, P., Mogbil, V.: Soft lambda-calculus: a language for polynomial time computation. CoRR, cs.LO/0312015 (2003)Google Scholar
  6. [Bou03]
    Boudol, G.: On strong normalization in the intersection type discipline. In: Hofmann, M. (ed.) TLCA 2003. LNCS, vol. 2701, pp. 60–74. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  7. [CD78]
    Coppo, M., Dezani-Ciancaglini, M.: A new type assignment for lambda-terms. Archiv für mathematische Logik und Grundlagenforschung 19, 139–156 (1978)MathSciNetCrossRefGoogle Scholar
  8. [CD80]
    Coppo, M., Dezani-Ciancaglini, M.: An extension of the basic functionality theory for the λ-calculus. Notre Dame J. of Formal Logic 21(4), 685–693 (1980)MathSciNetCrossRefGoogle Scholar
  9. [CS07]
    Coquand, T., Spiwack, A.: A proof of strong normalisation using domain theory. Logic. Methods Comput. Science 3(4) (2007)Google Scholar
  10. [dC05]
    de Carvalho, D.: Intersection types for light affine lambda calculus. ENTCS 136, 133–152 (2005)MathSciNetMATHGoogle Scholar
  11. [dC09]
    de Carvalho, D.: Execution time of lambda-terms via denotational semantics and intersection types. CoRR, abs/0905.4251 (2009)Google Scholar
  12. [DCHM00]
    Dezani-Ciancaglini, M., Honsell, F., Motohama, Y.: Compositional characterizations of lambda-terms using intersection types (extended abstract). In: Nielsen, M., Rovan, B. (eds.) MFCS 2000. LNCS, vol. 1893, p. 304. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  13. [DCT07]
    Dezani-Ciancaglini, M., Tatsuta, M.: A Behavioural Model for Klop’s Calculus. In: Corradini, F., Toffalori, C. (eds.) Logic, Model and Computer Science. ENTCS, vol. 169, pp. 19–32. Elsevier, Amsterdam (2007)MATHGoogle Scholar
  14. [ER03]
    Ehrhard, T., Regnier, L.: The differential lambda-calculus. Theoret. Comput. Sci. 309(1-3), 1–41 (2003)MathSciNetCrossRefGoogle Scholar
  15. [Ghi96]
    Ghilezan, S.: Strong normalization and typability with intersection types. Notre Dame J. Formal Loigc 37(1), 44–52 (1996)MathSciNetCrossRefGoogle Scholar
  16. [Gir87]
    Girard, J.-Y.: Linear logic. Theoret. Comput. Sci. 50(1), 1–101 (1987)MathSciNetCrossRefGoogle Scholar
  17. [GR07]
    Gaboardi, M., Ronchi Della Rocca, S.: A soft type assignment system for lambda -calculus. In: Duparc, J., Henzinger, T.A. (eds.) CSL 2007. LNCS, vol. 4646, pp. 253–267. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  18. [How80]
    Howard, W.A.: The formulae-as-types notion of construction. In: Seldin, J.P., Hindley, J.R. (eds.) To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism, pp. 479–490. Academic Press, London (1980), Reprint of a manuscript written 1969Google Scholar
  19. [KL07]
    Kesner, D., Lengrand, S.: Resource operators for the λ-calculus. Inform. and Comput. 205, 419–473 (2007)MathSciNetCrossRefGoogle Scholar
  20. [Klo80]
    Klop, J.-W.: Combinatory Reduction Systems, volume 127 of Mathematical Centre Tracts. CWI, PhD Thesis (1980)Google Scholar
  21. [KW99]
    Kfoury, A.J., Wells, J.B.: Principality and decidable type inference for finite-rank intersection types. In: Proc. of the 26th Annual ACM Symp. on Principles of Programming Languages (POPL 1999), pp. 161–174. ACM Press, New York (1999)Google Scholar
  22. [Laf04]
    Lafont, Y.: Soft linear logic and polynomial time. Theoret. Comput. Sci. 318(1-2), 163–180 (2004)MathSciNetCrossRefGoogle Scholar
  23. [Lei86]
    Leivant, D.: Typing and computational properties of lambda expressions. Theoretical Computer Science 44(1), 51–68 (1986)MathSciNetCrossRefGoogle Scholar
  24. [Len05]
    Lengrand, S.: Induction principles as the foundation of the theory of normalisation: Concepts and techniques. Technical report, PPS laboratory, Université Paris 7 (March 2005), http://hal.ccsd.cnrs.fr/ccsd-00004358
  25. [Len06]
    Lengrand, S.: Normalisation & Equivalence in Proof Theory & Type Theory. PhD thesis, Univ. Paris 7 & Univ. of St Andrews (2006)Google Scholar
  26. [NM04]
    Neergaard, P.M., Mairson, H.G.: Types, potency, and idempotency: why nonlinearity and amnesia make a type system work. In: Okasaki, C., Fisher, K. (eds.) Proc. of the ACM International Conference on Functional Programming, pp. 138–149. ACM Press, New York (September 2004)Google Scholar
  27. [Sør97]
    Sørensen, M.H.B.: Strong normalization from weak normalization in typed lambda-calculi. Inform. and Comput. 37, 35–71 (1997)CrossRefGoogle Scholar
  28. [Val01]
    Valentini, S.: An elementary proof of strong normalization for intersection types. Arch. Math. Log. 40(7), 475–488 (2001)MathSciNetCrossRefGoogle Scholar
  29. [vB92]
    van Bakel, S.: Complete restrictions of the intersection type discipline. Theoret. Comput. Sci. 102(1), 135–163 (1992)MathSciNetCrossRefGoogle Scholar
  30. [vRSSX99]
    van Raamsdonk, F., Severi, P., Sørensen, M.H.B., Xi, H.: Perpetual reductions in λ-calculus. Inform. and Comput. 149(2), 173–225 (1999)MathSciNetCrossRefGoogle Scholar
  31. [Xi97]
    Xi, H.: Weak and strong beta normalisations in typed lambda-calculi. In: de Groote, P. (ed.) TLCA 1997. LNCS, vol. 1210, pp. 390–404. Springer, Heidelberg (1997)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2011

Authors and Affiliations

  • Alexis Bernadet
    • 1
    • 2
  • Stéphane Lengrand
    • 1
    • 3
  1. 1.École PolytechniqueFrance
  2. 2.École Normale Supérieur de CachanFrance
  3. 3.CNRSFrance

Personalised recommendations