Compositional Characterizations of λ-Terms Using Intersection Types
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.
KeywordsNormal Form Intersection Type Type Theory Evaluation Property Denotational Semantic
Unable to display preview. Download preview PDF.
- 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
- 7.H.P. Barendregtet. al. Typed λ-calculus and applications. North-Holland. (to appear).Google Scholar
- 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.M. Dezani-Ciancaglini, F. Honsell, and Y. Motohama. Compositional cha-racterization of λ-terms using intersection types. Internal report, 2000, (http://www.di.unito.it/~yoko/paper/dezahonsmoto2000.ps).
- 19.J. Mitchell. Foundation for Programmimg Languages. MIT Press, 1996.Google Scholar
- 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