Co to jest w rachunku konstrukcji?

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.$\lambda_\to$

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.$Prop$$Prop : 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$

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

$$\mathsf{Prop} : \mathsf{Type}$$ $\mathsf{Type} : \mathsf{Prop}$$\mathsf{Prop}$$\mathsf{Prop}$$\mathsf{Type}_1$$\mathsf{Type}_2$$\mathsf{Type}_3$ $$\begin{align*} \mathsf{Prop} &: \mathsf{Type}_1 \\ \mathsf{Type}_1 &: \mathsf{Type}_2 \\ \mathsf{Type}_2 &: \mathsf{Type}_3 \\ &\vdots \end{align*}$$ $\prod$musi wyjaśnić, jak utworzyć gdy jest twierdzeniem lub typem, a jest albo twierdzeniem, albo typem. Istnieją cztery kombinacje:$\prod_{x : A} B(x)$$A$$B(x)$

1. $$\frac{A : \mathsf{Prop} \qquad x : A \vdash B(x) : \mathsf{Prop}} {\prod_{x : A} B(x) : \mathsf{Prop}}$$
2. $$\frac{A : \mathsf{Type}_i \qquad x : A \vdash B(x) : \mathsf{Prop}} {\prod_{x : A} B(x) : \mathsf{Prop}}$$
3. $$\frac{A : \mathsf{Prop} \qquad x : A \vdash B(x) : \mathsf{Type}_i} {\prod_{x : A} B(x) : \mathsf{Type}_i}$$
4. $$\frac{A : \mathsf{Type}_i \qquad x : A \vdash B(x) : \mathsf{Type}_j} {\prod_{x : A} B(x) : \mathsf{Type}_{\max(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ć elementy$A$$i$$B(x)$$j$$\max(i,j)$$\mathsf{Prop}$$\prod_{x : A} B(x)$$\mathsf{Prop}$$B(x)$$A$$\mathsf{Prop}$przez kwantyfikację samego .$\mathsf{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

$$\prod_{A : \mathsf{Type}_1} A \to A$$ $$\prod_{A : \mathsf{Prop}} A \to A$$ $\mathsf{Type}_2$$\mathsf{Prop}$$\mathsf{Type}_1$$\mathsf{Type}_1$$A$$\prod_{A : \mathsf{Prop}} A \to A$