Anzeige
Erschienen in:
2012 | OriginalPaper | Buchkapitel
Loader and Urzyczyn Are Logically Related
verfasst von : Sylvain Salvati, Giulio Manzonetto, Mai Gehrke, Henk Barendregt
Erschienen in: Automata, Languages, and Programming
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
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.