Rozstrzygalność wnioskowania o typie i sprawdzania typu w MLTT

W Intuitionistycznej teorii typów: część predykcyjna Martina-Löfa udowodniono, że sprawdzanie typów $a \colon A$ podlega rozstrzygnięciu z zastrzeżeniem $a$ przede wszystkim do pisania , poprzez udowodnienie twierdzenia o normalizacji dla zamkniętych terminów do pisania. Z drugiej strony widziałem, jak napisano w wielu miejscach (Wikipedia, Nördstrom itp.), Że sprawdzanie typu (intensywne) MLTT jest rozstrzygalne; czy domyślnie ograniczają się do terminów pisanych na maszynie?
Czy coś wiadomo na temat rozstrzygalności wnioskowania o typie lub sprawdzania typu w intensywnym MLTT, jeśli nie ograniczamy się do terminów typowalnych? Na przykład być może istnieje proces decyzyjny, który rozpoznaje terminy nieopisane, powiedzmy przez normalizację do formy, która nie odpowiada żadnemu konstruktorowi, lub przez wykazanie, że nie istnieje nieokresowa sekwencja redukcji dla dowolnego terminu nieopisanego.

Nie znalazłem wiele w literaturze.

reference-request type-theory type-inference

— Josh Chen
źródło

Odpowiedzi:

Z pewnością problem decyzyjny

Biorąc pod uwagę (przed) termin $a$ Czy jest jakiś typ $A$ takie, że $\vdash a :A$ można uzyskać w MLTT?

Czasami napisane $\vdash a\ :\ ?$ (i nazywany problemem wnioskowania typu ) jest rozstrzygalny, co oznacza, że nie ma znaczenia, czy $a$ jest dobrze wpisany lub nie, aby uzyskać odpowiedź. Rzeczywiście, wszystkie weryfikatory dowodu oparte na MLTT implementują pewną wersję tego algorytmu decyzyjnego!

Oczywiście problem występuje w niepustym kontekście ( $\Gamma\vdash a\ :\ ?$ ) również jest rozstrzygalne, zwykle musisz rozwiązać ten drugi, aby rozwiązać ten pierwszy.

To powinno odpowiedzieć na pytania 1 i 2. Algorytm nie wymaga normalizacji $a$ , co na ogół byłoby złą wiadomością, ponieważ nie można rozstrzygnąć, czy niepoprawny termin normalizuje się do czegokolwiek. Jednak rodzaj algorytmu sprawdzania nie wiązać normalizacji rodzajów , które są konstrukcyjnie doskonale wpisał się.

W rezultacie normalizacja dobrze wpisanych terminów jest niezbędnym warunkiem rozstrzygnięcia problemu wnioskowania typu.

Możesz sprawdzić Nordström, Petersson i Smith w celu uzyskania wstępu.

Nie znam żadnego ogólnego opisu algorytmu wnioskowania typu dla normalizacji teorii typów, chociaż Pollack daje całkiem niezły przegląd (chociaż stan techniki uległ poprawie) w sprawdzaniu typów w Pure Type Systems .

— cody
źródło

Co powiesz na pretypy (terminy rzekomo oznaczające typ)? Warto też wyjaśnić ich status.

— Andrej Bauer,

Dziękuję cody, czy odnosisz się do algorytmów sprawdzania typu wdrożonych przez asystentów ds. Weryfikacji, takich jak ALF i Coq? Według mnie są to algorytmy dla konkretnych wariantów MLTT, na których się opierają (CIC dla Coq, coś innego dla ALF), ale nie jest dla mnie jasne, w jaki sposób można ich użyć do sprawdzenia konkretnego MLTT z '73. W szczególności, jeśli hierarchia wszechświata lub inne różnice w szczegółach mogą coś zmienić ...

— Josh Chen

... Czy algorytmy są na tyle ogólne, aby uwzględnić te różnice? Mam problem ze znalezieniem wyników w takiej ogólności; Wydaje mi się, że w moich poszukiwaniach literatury pojawiają się bardzo konkretne wyniki, często szczególnie dostosowane do podstawowej teorii jakiegoś asystenta dowodu.

— Josh Chen

@JoshChen algorytmy są bardzo ogólne, ponieważ obejmują wyszukiwanie ukierunkowane na typ, naprzemiennie z krokami normalizacji na dobrze wpisanych terminach, jak wyjaśnił Andrej. Niestety nie znam ogólnego opisu algorytmu, choć dodam częściowe odniesienie do mojej odpowiedzi.

— cody

@JoshChen Nie wyjaśniają, ale mogą odnosić się do typów wnioskowania dla terminów „curry-style”, dla których wnioskowanie jest nierozstrzygalne. Bardziej szczegółowo wchodzę

— cody

Chciałbym uzupełnić odpowiedź cody o ogólną obserwację, przekazującą moje zrozumienie, dlaczego działają algorytmy sprawdzania typu.

W przypadku szerokiej klasy teorii typów sprawdzanie lub wnioskowanie odbywa się w taki sposób, że nigdy nie próbujemy normalizować terminu, chyba że wcześniej ustaliliśmy, że jest on dobrze wpisany. Podobnie, nigdy nie próbujemy normalizować typu, chyba że już ustaliliśmy, że jest to typ. Z tego powodu możemy być pewni, że normalizacja zakończy się (co wymaga osobnego dowodu).

Należy spojrzeć na określone algorytmy i przekonać się, że tak naprawdę działają w ten sposób, ale działają. Chciałem tylko powiedzieć, co sprawia, że tyka. Lub lepiej, dlatego przestają tykać.

— Andrej Bauer
źródło