Dlaczego nieskończona hierarchia typów?

18

Coq, Agda i Idris mają nieskończoną hierarchię typów (Typ 1: Typ 2: Typ 3: ...). Ale dlaczego nie zrobić tego zamiast λC, układu w sześcianie lambda najbliższego rachunku różniczkowego konstrukcji, który ma tylko dwa rodzaje, i , i te reguły? $*$ $◽$

\frac{}{\emptyset ⊢ * : ◽}

$\frac {} {∅ ⊢ * : ◽}$

\frac{Γ ⊢ T_{1} : s_{1} Γ, x : T_{1} ⊢ t : T_{2}}{Γ ⊢ (λ x : T_{1}, t) : (Π x : T_{1}, T_{2})}

$\frac {Γ ⊢ T _ 1 : s _ 1 \qquad Γ, \: x : T _ 1 ⊢ t : T _ 2} {Γ ⊢ (λ \: x : T _ 1, \: t) : (Π \: x : T _ 1, \: T _ 2)}$

\frac{Γ ⊢ T_{1} : s_{1} Γ, x : T_{1} ⊢ T_{2} : s_{2}}{Γ ⊢ (Π x : T_{1}, T_{2}) : s_{2}}

$\frac {Γ ⊢ T _ 1 : s _ 1 \qquad Γ, \: x : T _ 1 ⊢ T _ 2 : s _ 2} {Γ ⊢ (Π \: x : T _ 1, \: T _ 2) : s _ 2}$

To wydaje się prostsze. Czy ten system ma ważne ograniczenia?

coq dependent-type calculus-of-constructions

— Rui Baptista
źródło

19

W rzeczywistości podejście CoC jest bardziej wyraziste - pozwala na dowolną impredykatywną kwantyfikację. Na przykład wpisz $\forall a.\; a \to a$ można utworzyć z sobą, aby uzyskać $(\forall a.\; a \to a) \to (\forall a.\; a \to a)$ , co nie jest możliwe w przypadku hierarchii wszechświata.

Powodem, dla którego nie jest powszechnie stosowany, jest to, że impredykatywna kwantyfikacja jest niezgodna z logiką klasyczną. Jeśli go masz, nie możesz podać modelu teorii typów, w którym typy są interpretowane jako zbiory w naiwny sposób - patrz słynny artykuł Johna Reynoldsa „ Polimorfizm nie jest teoretyką zbiorów” .

Ponieważ wiele osób chce wykorzystać teorię typów jako metodę sprawdzania maszynowego zwykłych dowodów matematycznych, generalnie nie są entuzjastycznie nastawieni do cech teoretycznych, które są niezgodne ze zwykłymi podstawami. W rzeczywistości Coq początkowo popierał impredykatywność, ale stopniowo ją porzucał.

— Neel Krishnaswami
źródło

9

Uzupełnię odpowiedź Neela (jak zwykle doskonała) nieco bardziej objaśnieniem, dlaczego poziomy są stosowane w praktyce.

Pierwszym ważnym ograniczeniem CoC jest to, że jest to banalne! Zaskakujące jest spostrzeżenie, że nie ma typu, dla którego można udowodnić , że ma więcej niż jeden element, a tym bardziej nieskończoną liczbę. Dodanie tylko 2 wszechświatów daje liczby naturalne z nieskończenie wieloma elementami i wszystkimi „prostymi” typami danych.

Drugim ograniczeniem są reguły obliczeń: CoC obsługuje tylko iterację , tzn. Funkcje odzyskujące nie mają dostępu do podokresów swoich argumentów. Z tego powodu wygodniej jest dodawać typy indukcyjne jako prymitywną konstrukcję, dającą początek CIC. Ale teraz pojawia się inny problem: najbardziej naturalna zasada indukcji ( w tym kontekście zwana eliminacją ) jest niezgodna z Wykluczonym Środkiem! Te problemy nie pojawiają się, jeśli ograniczysz regułę indukcyjną do typów predykcyjnych za pomocą wszechświatów.

Podsumowując, wydaje się, że CoC nie ma ani wyrazistości, ani solidności w stosunku do spójności, jakiej chciałbyś w systemie fundamentalnym. Dodanie wszechświatów rozwiązuje wiele z tych problemów.

— cody
źródło

Czy masz jakieś odniesienia do pierwszego ograniczenia? Jeśli nie, czy mógłbyś podać wskazówki, w jaki sposób drugi wszechświat pomaga udowodnić (propozycyjną? Meta?) Nierówność?

— Łukasz Lew

@ ŁukaszLew To właściwie prosta konsekwencja modelu „nieistotnego dowodu”, do którego można łatwo przejść w wyszukiwarkę. W tym modelu żaden typ nie ma więcej niż 1 element. Posiadanie 2 wszechświatów zapobiega istnieniu tego modelu. Teza Alexandre Miquela stanowi odniesienie do typu o nieskończonej liczbie elementów z 2 wszechświatami.

— cody