Żadnych naiwnych modeli teoretycznych polimorficznego rachunku Lambda?

15

W artykule Philipa Wadlera na temat Twierdzeń za darmo stwierdza w części 2, że parametryczność, że

nie ma naiwnych teoretycznych modeli polimorficznego rachunku lambda

W naiwnym modelu teoretycznym zestawu typy są zestawami, a funkcje są funkcjami zestawu teoretycznego, co wydaje się rozsądne. Dlaczego więc mówi, że nie ma naiwnych modeli teoretycznych polimorficznego rachunku lambda?

MK
źródło
5
OK, właśnie natknąłem się na ten artykuł: hal.inria.fr/inria-00076261/document . Będę musiał to przeorać.
MK
3
Ten artykuł Reynoldsa jest rzeczywiście odpowiedni do przeczytania! Pomijając wiele szczegółów, podsumowuje: rozważ data T = K ((T -> Bool) -> Bool). Wtedy, Ti ((T->Bool)->Bool)są izomorficzne. Jeśli mają model zestawu, w którym ->oznacza przestrzeń funkcji (jako zestaw), ta ostatnia ma większą liczność, więc nie może być izomorficzna T. Tak więc w modelu musimy interpretować ->inaczej - np. Jako przestrzeń funkcji ciągłych .
chi
Odpowiedziałem zbyt szybko i odpowiedziałem na złe pytanie. Przepraszam za to. Powód, dla którego polimorficzny rachunek lambda nie ma modelu w naiwnej teorii zbiorów, jest najwyraźniej inny niż ten dla rachunku lambda bez typu.

Odpowiedzi:

12

ΠSSetS×

2T=ΠX(X2)2(T2)2

Zauważ, że kolejny artykuł Andrew Pittsa pt. Polimorfizm jest teoretycznie ustalony , konstruktywnie , obala ten wniosek nieco, pokazując, że powyższą sprzeczność można skonstruować tylko w klasycznej teorii zbiorów, i że istnieje kilka konstruktywnych teorii zbiorów, w których polimorfizm może być interpretowane przy pomocy zwykłych interpretacji funkcji przestrzeni i produktów. W szczególności te „duże produkty” istnieją w Efektywnych Toposach, najbardziej kompleksowe ze wstępów przedstawionych przez Phoa .

cody
źródło