Zrozumienie dowodu silnej normalizacji rachunku konstrukcji

Mam trudności ze zrozumieniem dowodu silnej normalizacji dla rachunku konstrukcji. Staram się podążać za dowodem zawartym w pracy Hermana Geuversa „Krótki i elastyczny dowód silnej normalizacji dla rachunku konstrukcji”.

Potrafię dobrze podążać za główną linią rozumowania. Konstrukcje Geuvers dla każdego typu $T$ interpretacja $[\![T]\!]_\xi$ na podstawie pewnej oceny zmiennych typu $\xi(\alpha)$ . A potem konstruuje jakąś interpretację terminów $(\!|M|\!)_\rho$ na podstawie pewnej oceny zmiennych terminowych $\rho(x)$ i dowodzi, że dla prawidłowych ocen twierdzenie $(\!|M|\!)_\rho \in [\![T]\!]_\xi$ dla wszystkich $\Gamma\vdash M:T$ trzyma.

Mój problem: dla łatwych typów (takich jak systemowe typy F) interpretacja typów $[\![T]\!]_\xi$ jest naprawdę zbiorem terminów, więc stwierdzenie $(\!|M|\!)_\rho \in [\![T]\!]_\xi$ ma sens. Ale w przypadku bardziej złożonych typów interpretacja $[\![T]\!]_\xi$ nie jest zestawem terminów, ale zestawem funkcji odpowiedniej przestrzeni funkcji. Myślę, że prawie rozumiem budowę przestrzeni funkcyjnych, jednak nie może ona przypisać żadnego znaczenia $(\!|M|\!)_\rho \in [\![T]\!]_\xi$ dla bardziej złożonych typów $T$ .

Czy ktoś może wyjaśnić lub podać linki do bardziej zrozumiałych prezentacji dowodu?

Edycja: Pozwól mi spróbować wyjaśnić pytanie. Kontekst $\Gamma$ ma deklaracje zmiennych typu $\alpha:A$ i zmienne obiektowe. Wycena typu jest ważna, jeśli dla wszystkich $(\alpha:A) \in \Gamma$ z $\Gamma\vdash A:\square$ następnie $\xi(\alpha) \in \nu(A)$ jest ważny. Ale $\nu(A)$ może być elementem $(SAT)^*$ i nie tylko $SAT$ . Dlatego nie można zdefiniować żadnej ważnej oceny terminu $\rho(\alpha)$ . $\rho(\alpha)$ musi być terminem, a nie jakąś funkcją przestrzeni funkcji.

Edycja 2: Przykład, który nie działa

Zróbmy następującą prawidłową pochodną:

\begin{array}{llll} [] & ⊢ & * : ◻ & axiom \\ [α : *] & ⊢ & α : * & variable introduction \\ [α : *] & ⊢ & * : ◻ & weaken \\ [] & ⊢ & (Π α : * . *) : ◻ & product formation \\ [β : Π α : * . *] & ⊢ & β : (Π α : * . *) & variable introduction \end{array}

$\begin{array}{llll} [] &\vdash & *:\square &\text{axiom} \\ [\alpha:*] &\vdash& \alpha:* &\text{variable introduction} \\ [\alpha:*] &\vdash& *:\square &\text{weaken} \\ [] &\vdash & (\Pi \alpha:*.*):\square &\text{product formation} \\ [\beta:\Pi \alpha:*.*] &\vdash& \beta:(\Pi \alpha:*.*) &\text{variable introduction} \end{array}$

W ostatnim kontekście poprawna ocena typu musi spełniać $\xi(\beta) \in \nu(\Pi \alpha:*.*) = \{f| f:\text{SAT} \to \text{SAT}\}$ . Dla tego typu oceny nie ma ważnej oceny terminu.

— helmut
źródło

Tak myśli połowa ludzi

S A T

$SAT$ jest SAT. Powinieneś wyjaśnić, co to jest. Ponadto twoje pochodzenie wydaje się nieco dziwne. Druga linia nie powinna wspominać

α

$\alpha$ na zakończenie powinien przeczytać coś w rodzaju

[α : *] ⊢ * : ◻

$[\alpha : *] \vdash * : \Box$ czy nie powinno?

— Andrej Bauer,

Używam notacji Herman Geuvers (która wydaje się być standardem w tej dziedzinie).

SAT

$\text{SAT}$ jest zbiorem wszystkich nasyconych zestawów wyrażeń lambda. Dla drugiego wiersza mojej pochodnej: jest to reguła wprowadzająca dla zmiennych systemu czystego typu. Ta reguła brzmi

\frac{Γ ⊢ T : s}{Γ, x : T ⊢ x : T}

$\frac{\Gamma \vdash T:s}{\Gamma,x:T\vdash x:T}$ gdzie

s

$s$ jest jakoś.

— helmut

Rozumiem, skąd masz drugą linię, ale nie jest to właściwe założenie do utworzenia trzeciej linii, prawda? Jaka reguła podaje trzecią linię.

— Andrej Bauer,

Reguła tworzenia produktu PTS mówi

\frac{r (s_{1}, s_{2}, s_{3}; Γ ⊢ A : s_{1}; Γ, x : A ⊢ B : s_{2}}{Γ ⊢ (Π x : A . B) : s_{3}}

$\frac{r(s_1,s_2,s_3;\, \Gamma\vdash A:s_1;\: \Gamma,x:A\vdash B:s_2}{\Gamma\vdash (\Pi x:A.B): s_3}$ . Rachunek konstrukcji ma regułę

r (*, *, *)

$r(*,*,*)$ . To pozwala mi użyć pierwszej i drugiej linii do uzyskania trzeciej. Miałem jednak literówkę w swoim poście. Brakowało tekstu w trzeciej linii, który teraz dodałem.

— helmut

Nie powinien wtedy czytać pierwszego wiersza

[] ⊢ * : *

$[] \vdash * : *$ ? A może się pomieszałeś?

*

$*$ i

◻

$\Box$ gdzieś? Druga linia nie może być drugą przesłanką reguły tworzenia produktu, ponieważ oznaczałoby to, że próbujesz utworzyć coś w rodzaju

\prod α : * . α

$\prod \alpha : * . \alpha$ zamiast

\prod α : * . *

$\prod \alpha : * . *$ .

— Andrej Bauer,

Niestety nie jestem pewien, czy istnieje więcej przyjaznych zasobów dla początkujących niż konto Geuvers. Możesz wypróbować tę notatkę Chrisa Casinghino, która podaje kilka dowodów w rozdzierających szczegółach.

Nie jestem pewien, czy rozumiem sedno waszego zamieszania, ale myślę, że jedną ważną rzeczą, na którą należy zwrócić uwagę, jest następujący lemat (wniosek 5.2.14), udowodniony w klasycznym tekście Barendregta :

Γ ⊢ M : T \Rightarrow Γ ⊢ T : * or ◻

$\Gamma \vdash M:T\ \Rightarrow\ \Gamma \vdash T:*\mbox{ or }\square$

Oznacza to, że podczas gdy $[\![T]\!]_\xi$ może być skomplikowaną funkcją, jeśli $\Gamma \vdash M:T$ trzyma zatem $[\![T]\!]_\xi$ musi być zbiorem warunków .

Jest to insynuowane w zarysie (sekcja 3.1), gdzie $(\!|t|\!)_\sigma\in[\![T]\!]_\xi$ tylko, jeżeli $\Gamma \vdash t:T :*$ , co jest zgodne z naszymi oczekiwaniami, a mianowicie, że interpretacja typu musi być zbiorem terminów, tj ${\cal V}(*)\subseteq{\cal P}(\mathrm{Term})$ (w rzeczy samej, ${\cal V}(*)=\mathrm{SAT}$ !)

Jest to powszechna sytuacja w teorii typów, mimo że interesuje nas tylko „rodzaj podstawowy” (tutaj $*$ ), wciąż musimy zdefiniować semantykę dla rzeczy wyższych rodzajów (stąd potrzeba wprowadzenia $\mathrm{SAT}^*$ ). Na koniec wszystko się ułoży, bo jest tylko rodzaj zamieszkały przez typy $*$ (i $\square$ , ale to nie jest tak naprawdę ważne).

— cody
źródło

Dziękuję za wyjaśnienie. To rozwiązuje mój problem niezrozumienia funkcji użytych w dowodzie Geuvera. Miałem już podejrzenia, że przeczytałem i ponownie przeczytałem gazetę Geuvera, ale wyraźnie to wyjaśniłeś.

— helmut