Giulio Manzonetto (Université Paris-Nord), Loader and Urzyczyn are Logically Related

Programme

Résumé

In simply typed λ-calculus with one ground type the following theorem due to Loader holds. (i) Given the full model F over a finite set, the question whether some element f∈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 Barendregt-Dekkers-Statman'12. 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 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.