Przykład, w którym naruszenie ścisłego warunku dodatniego w typach indukcyjnych prowadzi do niespójności

9

Większość systemów typowanych zależnie ma ścisłe warunki dodatnie dla typów indukcyjnych. Czy ktoś zna przykład, w którym naruszenie warunku prowadzi do niespójności w systemie?

Konstantin Solomatov
źródło

Odpowiedzi:

10

W rzeczywistości można rozluźnić ścisłą pozytywność i zachować spójność. Na przykład wystarczy mieć warunek dodatni. Oznacza to, że możemy zaakceptować takie definicje typów

Tμα.(α2)2

gdzie zmienne typu rekurencyjnego występują po lewej stronie parzystej liczby strzałek i zachowują spójność.

Jednak teorie pozwalające na tego rodzaju indukcyjny typ nie mają modeli teoretycznych - nie można interpretować typów jako zbiorów, a terminów jako elementów zbiorów. W tym przypadku mówimy, że T jest izomorficzny w stosunku do swojego podwójnego zestawu sił (tj. TP(P(T)) ), a to narusza twierdzenie Cantora .

Ponieważ teorie typów zależnych są często używane do sformalizowania matematyki, ich projektanci zwykle wahają się dodawać zasady, które nie są zgodne z semantyką teoretyczną, nawet jeśli są spójne.

EDYCJA: Dodam tę zmianę w odpowiedzi na pytanie Andreja. Typ jest spójny, jeśli dodasz go do (powiedzmy) Agdy; nie ma z tym żadnych problemów. Mamy problem tylko wtedy, gdy połączymy nie ścisłą pozytywność z wykluczonym środkiem.T

Intuicja, dlaczego jest bezpieczny, jest najlepiej widoczna przez soczewkę parametryczną (IMO). W Systemie F możemy pokazać za pomocą parametryczności, że dla dowolnego definiowalnego funktora , typ jest rzeczywiście typem indukcyjnym.FμFα.(Fαα)α

Przypomnijmy teraz, że definiowalnym funktorem jest operator typu , wraz z operatorem spełniających warunki funkcjonalności (tj. i ).FF:

map:α,β.(αβ)FαFβ
mapid=idmapfmapg=map(fg

Teraz możemy zdefiniować operator typu dla podwójnego zestawu zasilającego

C=λα.(α2)2

a ponieważ występuje tylko pozytywnie, możemy również zdefiniować dla niego operatora mapy:α

mapC=λf:αβ,a:(α2)2,k:β2.a(λa:α.k(fa))

Wiemy więc, że jest uzasadnionym typem indukcyjnym.T=μC

Neel Krishnaswami
źródło
Czy możemy wymyślić przykład, który sam w sobie tworzy niespójność? Twój przykład jest niespójny, jeśli założymy również (wystarczająco) wykluczony środek.
Andrej Bauer,
Innym powodem jest to, że możemy dodać twierdzenie FAN do Agdy, po czym możemy udowodnić, że dany typ jest liczbami naturalnymi (izomorficznymi).
Andrej Bauer,
Myślę o powinno być całkiem złe. μα.(α2)α
Andrej Bauer,
1
Ach, źle zrozumiałem pytanie - chodzi o to, że ścisła pozytywność jest warunkiem wystarczającym, ale niekoniecznym. Twój przykład (z faktycznym negatywnym wystąpieniem) jest niespójny.
Neel Krishnaswami
Tak, właśnie to zrozumiałem. Mój przykład nie zawiera wody.
Andrej Bauer,