Rozstrzygalność wnioskowania o typie i sprawdzania typu w MLTT

1. 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?

2. 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.

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 .

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ć.