Compositional Characterizations of λ-Terms Using Intersection Types

Extended Abstract
  • M. Dezani-Ciancaglini
  • F. Honsell
  • Y. Motohama
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1893)


We show how to characterize compositionally a number of evaluation properties of λ-terms using Intersection Type assignment systems. In particular, we focus on termination properties, such as strong normalization, normalization, head normalization, and weak head normalization. We consider also the persistent versions of such notions. By way of example, we consider also another evaluation property, unrelated to termination, namely reducibility to a closed term.

Many of these characterization results are new, to our knowledge, or else they streamline, strengthen, or generalize earlier results in the literature. The completeness parts of the characterizations are proved uniformly for all the properties, using a set-theoretical semantics of intersection types over suitable kinds of stable sets. This technique generalizes Krivine’s and Mitchell’s methods for strong normalization to other evaluation properties.


Normal Form Intersection Type Type Theory Evaluation Property Denotational Semantic 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    S. Abramsky. Domain theory in logical form. Ann. Pure Appl. Logic, 51(1–2):1–77, 1991.CrossRefMathSciNetzbMATHGoogle Scholar
  2. 2.
    S. Abramsky and C.-H. L. Ong. Full abstraction in the lazy lambda calculus. Inform. and Comput., 105(2):159–267, 1993.zbMATHCrossRefMathSciNetGoogle Scholar
  3. 3.
    F. Alessi, M. Dezani-Ciancaglini, and F. Honsell. A complete characterization of the complete intersection-type theories. In Proceedings in Informatics. ITRS’00 Workshop, Carleton-Scientific, 2000.Google Scholar
  4. 4.
    R. M. Amadio and P.-L. Curien. Domains and lambda-calculi. Cambridge University Press, Cambridge, 1998.zbMATHGoogle Scholar
  5. 5.
    S. van Bakel. Complete restrictions of the intersection type discipline. Theoret. Comput. Sci., 102(1):135–163, 1992.zbMATHCrossRefMathSciNetGoogle Scholar
  6. 6.
    H. Barendregt, M. Coppo, and M. Dezani-Ciancaglini. A filter lambda model and the completeness of type assignment. J. Symbolic Logic, 48(4):931–940, 1983.zbMATHCrossRefMathSciNetGoogle Scholar
  7. 7.
    H.P. Barendregtet. al. Typed λ-calculus and applications. North-Holland. (to appear).Google Scholar
  8. 8.
    C. Böhm and M. Dezani-Ciancaglini. λ-terms as total or partial functions on normal forms. In C. Böhm, editor, λ-calculus and computer science theory, pages 96–121, Lecture Notes in Comput. Sci., Vol. 37. Springer, Berlin, 1975.CrossRefGoogle Scholar
  9. 9.
    M. Coppo and M. Dezani-Ciancaglini. An extension of the basic functionality theory for the λ-calculus. Notre Dame J. Formal Logic, 21(4):685–693, 1980.zbMATHCrossRefMathSciNetGoogle Scholar
  10. 10.
    M. Coppo, M. Dezani-Ciancaglini, and M. Zacchi. Type theories, normal forms, and D∞-lambda-models. Inform. and Comput., 72(2):85–116, 1987.zbMATHCrossRefMathSciNetGoogle Scholar
  11. 11.
    M. Coppo, F. Honsell, M. Dezani-Ciancaglini, and G. Longo. Extended type struc-tures and filter lambda models. In G. Longo et. al., editors, Logic colloquium’ 82, pages 241–262. North-Holland, Amsterdam, 1984.Google Scholar
  12. 12.
    M. Dezani-Ciancaglini, F. Honsell, and Y. Motohama. Compositional cha-racterization of λ-terms using intersection types. Internal report, 2000, (
  13. 13.
    L. Egidi, F. Honsell, and S. Ronchi Della Rocca. Operational, denotational and logical descriptions: a case study. Fund. Inform., 16(2):149–169, 1992.zbMATHMathSciNetGoogle Scholar
  14. 14.
    S. Ghilezan. Strong normalization and typability with intersection types. Notre Dame J. Formal Logic, 37(1):44–52, 1996.zbMATHCrossRefMathSciNetGoogle Scholar
  15. 15.
    F. Honsell and M. Lenisa. Semantical analysis of perpetual strategies in λ-calculus. Theoret. Comput. Sci., 212(1-2):183–209, 1999.zbMATHCrossRefMathSciNetGoogle Scholar
  16. 16.
    F. Honsell and S. Ronchi Della Rocca. An approximation theorem for topological lambda models and the topological incompleteness of lambda calculus. J. Comput. System Sci., 45(1):49–75, 1992.zbMATHCrossRefMathSciNetGoogle Scholar
  17. 17.
    J.-L. Krivine. Lambda-calcul Types et Modéles. Masson, Paris, 1990. English translation: Lambda-calculus, types and models, Ellis Horwood, 1993.zbMATHGoogle Scholar
  18. 18.
    D. Leivant. Typing and computational properties of lambda expressions. Theoret. Comput. Sci., 44(1):51–68, 1986.zbMATHCrossRefMathSciNetGoogle Scholar
  19. 19.
    J. Mitchell. Foundation for Programmimg Languages. MIT Press, 1996.Google Scholar
  20. 20.
    G. D. Plotkin. Set-theoretical and other elementary models of the λ-calculus. Theoret. Comput. Sci., 121(1-2):351–409, 1993.zbMATHCrossRefMathSciNetGoogle Scholar
  21. 21.
    G. Pottinger. A type assignment for the strongly normalizable λ-terms. In J.R. Hindley and J.P. Seldin, editors, To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pages 561–577. Academic Press, London, 1980.Google Scholar
  22. 22.
    D. Scott. Continuous lattices. In F.W. Lawvere, editor, Toposes, Algebraic Geo-metry and Logic, pages 97–136. Lecture Notes in Math., Vol. 274. Springer, Berlin, 1972.CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2000

Authors and Affiliations

  • M. Dezani-Ciancaglini
    • 1
  • F. Honsell
    • 2
  • Y. Motohama
    • 1
  1. 1.Dipartimento di InformaticaUniversitá di TorinoTorinoItaly
  2. 2.Dipartimento di Matematica ed InformaticaUniversitá di UdineUdineItaly

Personalised recommendations