Dziedziczna substytucja z hierarchią wszechświata

Czytałem o dziedzicznej zamianie na prosty rachunek Lambda i na logiczną strukturę z odrębnymi terminami i typami.

Zastanawiam się, czy są jakieś przykłady dziedzicznej substytucji w systemie o typie zależnym i hierarchii wszechświata? tzn. gdzie $True : Set_0 : Set_1:Set_2$ itd.

Zastanawiam się w szczególności, jak ustalić miarę indukcyjną w takim systemie. Wersja o prostym typie zmniejsza się strukturalnie pod względem rodzaju zastępowanej zmiennej. Nie działa to z typami zależnymi, ponieważ w przypadku LF papier, który połączyłem, używa prostego skreślenia terminów, wykonując indukcję na kształt typu.

Jednak usuwanie do prostych typów nie działa z hierarchią wszechświata, ponieważ jeśli masz coś takiego:

• $f : (x : Set_1)\to x \to True$ implikuje to
• $f\ ((y : True) \to True \to True ): True \to True \to True$

tj. zastosowanie funkcji dało strukturalnie większy typ.

Zakładam, że rozwiązanie ma coś wspólnego z indeksami wszechświata, ale jeśli istnieje istniejąca technika ustalania, że ​​indukcja jest dobrze uzasadniona, wolałbym ją zacytować, niż wymyślić coś na własną rękę.

Oto odniesienie do predykatywnego Systemu F. Miara rzeczywiście obejmuje wielosekcję poziomów wszechświata w typie. Nie mogę wiele powiedzieć o tym, czy to podejście uogólnia na predykatywną teorię typów zależnych.

Począwszy od listopada 2018 r., Jak to zrobić w przypadku teorii typów zależnych z dużymi eliminacjami, pozostaje otwartym pytaniem.

Ustalenie, że rekurencja jest uzasadniona, nie jest takie złe; możesz użyć twierdzenia Patarai, aby udowodnić istnienie ustalonego punktu. Zobacz, jak Robert Harper * Konstruowanie systemów typów w ramach semantyki operacyjnej, aby uzyskać instrukcje. (Możesz to również zrobić za pomocą definicji indukcyjno-rekurencyjnej).

Trudną częścią jest właściwie sformułowanie dziedzicznej substytucji w przyjemny sposób - naturalny kierunek prowadzi cię do zastąpienia nie jednego terminu, ale całą substytucję kontekstu, co rodzi wiele pytań o to, kiedy i jak ustalić właściwości rzeczy jak kompozycje (dziedzicznych) podstawień.

Gdyby okazało się to niemożliwe, byłbym całkowicie zszokowany. Jednak obecnie nikt tego nie zrobił. Jeśli chcesz nad tym popracować, sugeruję skontaktowanie się z Andreasem Ablem, Danem Licatą i Mikiem Shulmanem. (Albo ja, jeśli o to chodzi.)