Co to jest w rachunku konstrukcji?

11

Patrzę na Rachunek Konstrukcji i jego miejsce w Kostce Lambda .

Jeśli dobrze rozumiem, każdą oś sześcianu można uznać za dodanie innej operacji obejmującej typy do rachunku zwykłego, . Pierwsza oś dodaje operatory typu „typ do terminu”, drugie operatory typu „typ do typu”, a trzecia zależna typowanie, czyli operatory typu „typ do typu”. CoC ma wszystkie trzy.λ

Jednak CoC wprowadza termin i stwierdza, że według reguł wnioskowania , ale poza tym nie jest używany. Rozumiem, że dotyczy to zdań tytułowych, ale zdania logiczne nie są zdefiniowane w kategoriach tego.PropProp:Type

Czy mógłbyś mi wyjaśnić, do czego służy , gdzie / kiedy się pojawi, i wyjaśnić go w kategoriach osi sześcianu (jeśli rzeczywiście jest to możliwe)?Prop

Michael Rawson
źródło

Odpowiedzi:

15

W tradycyjnej teorii typów Martina-Löfa nie ma rozróżnienia na typy i zdania. Jest to pod hasłem „propozycje jako typy”. Ale czasem istnieją powody, aby je rozróżniać. CoC właśnie to robi.

Istnieje wiele wariantów CoC, ale większość miałaby ale nie . Kolejna różnica pojawia się, gdy mamy nieskończenie wiele wszechświatów typów i sprawiają, że impredykatywny (tak właśnie robi Coq). Konkretnie, rozważ wariant CoC, w którym mamy i nieskończenie wiele typów wszechświatów , , z Reguła formacji dla

Prop:Type
Type:PropPropPropType1Type2Type3
Prop:Type1Type1:Type2Type2:Type3
musi wyjaśnić, jak utworzyć gdy jest twierdzeniem lub typem, a jest albo twierdzeniem, albo typem. Istnieją cztery kombinacje:x:AB(x)AB(x)
  1. A:Propx:AB(x):Propx:AB(x):Prop
  2. A:Typeix:AB(x):Propx:AB(x):Prop
  3. A:Propx:AB(x):Typeix:AB(x):Typei
  4. A:Typeix:AB(x):Typejx:AB(x):Typemax(i,j)

Najciekawsza jest różnica między drugim a czwartym przypadkiem. Czwarta zasada mówi, że jeśli jest w wszechświecie, a jest w wszechświecie, to iloczyn jest w -tym wszechświecie. Ale druga zasada mówi nam, że to nie tylko „jeszcze jeden wszechświat na dole”, ponieważ ląduje w gdy tylko , niezależnie od tego, jak duże jestJest to impredykatywne, ponieważ pozwala nam zdefiniować elementyAiB(x)jmax(i,j)Propx:AB(x)PropB(x)APropprzez kwantyfikację samego .Prop

Konkretnym przykładem może być versus Pierwszy produkt mieszka w , ale drugi jest w (a nie w , mimo że kwantyfikujemy element ). W szczególności oznacza to, że jedną z możliwych wartości dla jest samego

A:Type1AA
A:PropAA
Type2PropType1Type1AA:PropAA
Andrej Bauer
źródło