Abstract
In simply typed λ-calculus with one ground type the following theorem due to Loader holds. (i) Given the full model \(\mathcal F\) over a finite set, the question whether some element \(f\in{\mathcal F}\) is λ-definable is undecidable. In the λ-calculus with intersection types based on countably many atoms, the following is proved by Urzyczyn. (ii) It is undecidable whether a type is inhabited.
Both statements are major results presented in [3]. We show that (i) and (ii) follow from each other in a natural way, by interpreting intersection types as continuous functions logically related to elements of \(\mathcal F\). From this, and a result by Joly on λ-definability, we get that Urzyczyn’s theorem already holds for intersection types with at most two atoms.
This is a preview of subscription content, log in via an institution to check access.
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
Abramsky, S.: Domain theory in logical form. In: Symposium on Logic and Computer Science (LICS 1987), pp. 47–53. IEEE Computer Science Press (1987)
Amadio, R., Curien, P.-L.: Domains and lambda-calculi. Cambridge Tracts in Theoretical Computer Science, vol. (46). Cambridge University Press (1998)
Barendregt, H.P., Dekkers, W., Statman, R.: Lambda calculus with types (to appear), Draft available at http://www.cs.ru.nl/~henk/book.pdf
Coppo, M., Dezani-Ciancaglini, M., Venneri, B.: Functional characters of solvable terms. Mathematical Logic Quarterly 27(2-6), 45–58 (1981)
Joly, T.: Encoding of the Halting Problem into the Monster Type & Applications. In: Hofmann, M.O. (ed.) TLCA 2003. LNCS, vol. 2701, pp. 153–166. Springer, Heidelberg (2003)
Loader, R.: The undecidability of lambda definability. In: Logic, Meaning and Computation: Essays in Memory of Alonzo Church, pp. 331–342 (2001)
Plotkin, G.: Lambda definability and logical relations. Memorandum SAI-RM-4, School of Artificial Intelligence. University of Edinburgh (1973)
Salvati, S.: Recognizability in the Simply Typed Lambda-Calculus. In: Ono, H., Kanazawa, M., de Queiroz, R. (eds.) WoLLIC 2009. LNCS, vol. 5514, pp. 48–60. Springer, Heidelberg (2009)
Statman, R.: Completeness, invariance and λ-definability. The Journal of Symbolic Logic 47(1), 17–26 (1982)
Urzyczyn, P.: The emptiness problem for intersection types. The Journal of Symbolic Logic 64(3), 1195–1215 (1999)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Salvati, S., Manzonetto, G., Gehrke, M., Barendregt, H. (2012). Loader and Urzyczyn Are Logically Related. In: Czumaj, A., Mehlhorn, K., Pitts, A., Wattenhofer, R. (eds) Automata, Languages, and Programming. ICALP 2012. Lecture Notes in Computer Science, vol 7392. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-31585-5_34
Download citation
DOI: https://doi.org/10.1007/978-3-642-31585-5_34
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-31584-8
Online ISBN: 978-3-642-31585-5
eBook Packages: Computer ScienceComputer Science (R0)