Techniki dowodowe pokazujące, że sprawdzanie typu zależnego jest rozstrzygalne

Jestem w sytuacji, w której muszę pokazać, że sprawdzanie typu ma decydujący wpływ na rachunek różniczkowy, nad którym pracuję. Do tej pory udało mi się udowodnić, że system silnie się normalizuje, a zatem równość definicyjna jest rozstrzygalna.

W wielu źródłach, które czytam, rozstrzygalność sprawdzania typów jest wymieniona jako następstwo silnej normalizacji i wierzę w to w tych przypadkach, ale zastanawiam się, jak się to faktycznie pokazuje.

W szczególności utknąłem w następujących kwestiach:

• To, że dobrze wpisane terminy silnie się normalizują, nie oznacza, że ​​algorytm nie zapętla się w nieskończoność na niepoprawnie wpisanych wejściach
• Ponieważ relacje logiczne są zwykle używane do wykazania silnej normalizacji, nie ma wygodnej malejącej miary w miarę postępu sprawdzania typów. Więc nawet jeśli moje reguły typu są ukierunkowane na składnię, nie ma gwarancji, że stosowanie reguł ostatecznie zakończy się.

Zastanawiam się, czy ktoś ma dobre odniesienie do dowodu rozstrzygalności sprawdzania typu dla języka zależnego od typu? Jeśli jest to mały rachunek różniczkowy, nic nie szkodzi. Wszystko, co omawia techniki dowodowe do wykazania rozstrzygalności, byłoby świetne.

Rzeczywiście jest tu subtelność, choć w przypadku sprawdzania typu wszystko działa dobrze. Spiszę tutaj ten problem, ponieważ wydaje się, że pojawia się on w wielu powiązanych wątkach, i spróbuję wyjaśnić, dlaczego wszystko działa dobrze, gdy sprawdzanie typu w „standardowej” zależnej teorii typów (będę celowo niejasny, ponieważ problemy te pojawiają się niezależnie od tego):

${\cal D}$$\Gamma\vdash t:A$${\cal D}'$$\Gamma \vdash A:s$$s$$u\leq t$$B$$\Delta$$\cal D''$$\Delta\vdash u:B$

Ten przyjemny fakt jest nieco trudny do udowodnienia i zrównoważony przez dość paskudny kontr-fakt:

$\cal D'$$\cal D''$ $\cal D$

Zależy to trochę od dokładnego sformułowania twojego systemu typów, ale większość „operacyjnych” systemów wdrożonych w praktyce spełnia fakt 2.

Oznacza to, że nie można „przejść do podokresów” podczas wnioskowania przez indukcję na podstawie pochodnych lub stwierdzić, że oświadczenie indukcyjne jest prawdziwe w odniesieniu do rodzaju terminu, w którym próbujesz coś udowodnić.

Fakt ten dość mocno cię gryzie, gdy próbujesz udowodnić pozornie niewinne stwierdzenia, np. Że systemy z konwersją typu są równoważne z systemami z konwersją bez typu.

$t$$\Gamma$$A, s$$\Gamma\vdash t:A$$\Gamma\vdash A : s$

Kluczowym przypadkiem (i jedynym przypadkiem, który naprawdę wymaga konwersji) jest aplikacja:

infer(t u):
   type_t, sort_t <- infer(t)
   type_t' <- normalize(type_t)
   type_u, sort_u <- infer(u)
   type_u' <- normalize(type_u)
   if (type_t' = Pi(A, B) and type_u' = A' and alpha_equal(A, A') then
      return B, sort_t (or the appropriate sort)
   else fail

Każde wezwanie do normalizacji odbywało się na dobrze napisanych terminach, ponieważ jest to niezmiennik infersukcesu.

Nawiasem mówiąc, po wdrożeniu Coq nie ma decydującego sprawdzania typu, ponieważ normalizuje treść fixinstrukcji przed próbą ich sprawdzenia.

W każdym razie granice normalnych form dobrze sformułowanych terminów są tak astronomiczne, że twierdzenie o rozstrzygalności jest w tym momencie głównie akademickie. W praktyce uruchamiasz algorytm sprawdzania typu, dopóki masz cierpliwość, i wypróbowujesz inną trasę, jeśli do tego czasu się nie zakończyła.