Abstract
We prove that the inhabitation problem (“Does there exist a closed term of a given type?”) is undecidable for intersection types of rank 3 and exponential space complete for intersection types of rank 2.
Partly supported by Ministry of Science and Higher Education grant N N206 355836.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Alessi, F., Barbanera, F.: Strong conjunction and intersection types. In: Tarlecki, A. (ed.) MFCS 1991. LNCS, vol. 520, pp. 64–73. Springer, Heidelberg (1991)
Alessi, F., Barbanera, F., Dezani-Ciancaglini, M.: Intersection types and lambda models. Theoretical Computer Science 355(2), 108–126 (2006)
Bunder, M.W.: The inhabitation problem for intersection types. In: Harland, J., Manyem, P. (eds.) Computing: The Australasian Theory Symposium. Conferences in Research and Practice in Information Technology, vol. 77, pp. 7–14. Australian Computer Society (2008)
Coppo, M., Dezani-Ciancaglini, M.: An extension of basic functionality theory for lambda-calculus. Notre Dame Journal of Formal Logic 21, 685–693 (1980)
Dezani-Ciancaglini, M., Ghilezan, S., Venneri, B.: The “relevance” of intersection and union types. Notre Dame Journal of Formal Logic 38(2), 246–269 (1997)
Kfoury, A.J., Wells, J.B.: Principality and type inference for intersection types using expansion variables. Theoretical Computer Science 311(1–3), 1–70 (2004)
Kozen, D.: Automata and Computability. Undergraduate Texts in Computer Science. Springer, Heidelberg (1997)
Kozen, D.: Theory of Computation. Springer, Heidelberg (2006)
Kurata, T., Takahashi, M.: Decidable properties of intersection type systems. In: Dezani-Ciancaglini, M., Plotkin, G. (eds.) TLCA 1995. LNCS, vol. 902, pp. 297–311. Springer, Heidelberg (1995)
Kuśmierek, D.: The inhabitation problem for rank two intersection types. In: Ronchi Della Rocca, S. (ed.) TLCA 2007. LNCS, vol. 4583, pp. 240–254. Springer, Heidelberg (2007)
Leivant, D.: Polymorphic type inference. In: PoPL, pp. 88–98. ACM Press, New York (1983)
Liquori, L., Ronchi Della Rocca, S.: Intersection-types à la Church. Information and Computation 205(9), 1371–1386 (2007)
Lopez-Escobar, E.G.K.: Proof functional connectives. In: Methods in Mathematical Logic. LNMath, vol. 1130, pp. 208–221. Springer, Heidelberg (1993)
Mints, G.E.: The completeness of provable realizability. Notre Dame Journal of Formal Logic 30, 420–441 (1989)
Møller Neergaard, P., Mairson, H.G.: Types, potency, and idempotency: Why nonlinearity and amnesia make a type system work. In: ICFP, pp. 138–149. ACM Press, New York (2004)
Pottinger, G.: A type assingment for the strongly normalizable λ-terms. In: Seldin, J.P., Hindley, J.R. (eds.) To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pp. 561–577. Academic Press, London (1980)
Ronchi Della Rocca, S., Roversi, L.: Intersection logic. In: Fribourg, L. (ed.) CSL 2001. LNCS, vol. 2142, pp. 414–428. Springer, Heidelberg (2001)
Sørensen, M.H., Urzyczyn, P.: Lectures on the Curry-Howard Isomorphism. Elsevier, Amsterdam (2006)
TLCA List of Open Problems, http://tlca.di.unito.it/opltlca/
Urzyczyn, P.: The emptiness problem for intersection types. Journal of Symbolic Logic 64(3), 1195–1215 (1999)
Venneri, B.: Intersection types as logical formulae. Journal of Logic and Computation 4(2), 109–124 (1994)
Wells, J.B., Haack, C.: Branching types. In: Le Métayer, D. (ed.) ESOP 2002. LNCS, vol. 2305, pp. 115–132. Springer, Heidelberg (2002)
Yokouchi, H.: Embedding a second-order type system into an intersection type system. Information and Computation 117(2), 206–220 (1995)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Urzyczyn, P. (2009). Inhabitation of Low-Rank Intersection Types. In: Curien, PL. (eds) Typed Lambda Calculi and Applications. TLCA 2009. Lecture Notes in Computer Science, vol 5608. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-02273-9_26
Download citation
DOI: https://doi.org/10.1007/978-3-642-02273-9_26
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-02272-2
Online ISBN: 978-3-642-02273-9
eBook Packages: Computer ScienceComputer Science (R0)