Dowód Barendregta na redukcję podmiotu dla

Znalazłem problem w dowodzie Barendregta na redukcję podmiotu (Thm 4.2.5 rachunku Lambda z typami ).

Ostatni krok dowodu (strona 60) mówi:

„a zatem przez Lemma 4.1.19 (1), $\quad\Gamma,x:\rho\vdash P:\sigma'$ . ”

Jednak zgodnie z Lemmą 4.1.19 (1) powinno to być $\Gamma[\vec{\alpha}:=\vec{\tau}],x:\rho\vdash P:\sigma'$ , ponieważ podstawienie następuje w całym kontekście, a nie tylko na $x:\rho'$ .

Myślę, że standardowym rozwiązaniem może być jakoś udowodnienie, że $\vec{\alpha}\notin FV(\Gamma)$ , ale nie jestem pewien jak.

Miałem dowód, który to uprościł, rozluźniając lemat generacyjny abstrakcji, ale niedawno odkryłem, że był błąd i mój dowód jest błędny, więc nie jestem pewien, jak rozwiązać ten problem.

Czy ktoś może mi powiedzieć, czego tu brakuje?

— Alejandro DC
źródło

Barendregt zakłada tak zwaną konwencję zmiennych, że powiązane nazwy zmiennych i nazwy zmiennych swobodnych są standaryzowane osobno , mianowicie domyślnie zakładamy, że są one różne (przy użyciu konwersji

α

$\alpha$ . Może to pomaga.

— Dave Clarke

Γ, x : ρ ⊢ P : σ^{'}

$\Gamma,x:\rho\vdash P:\sigma'$

Γ, x : ρ^{'} ⊢ P : σ^{″}

$\Gamma,x:\rho'\vdash P:\sigma''$

ρ^{'} [\vec{α} := \vec{τ}] = ρ

$\rho'[\vec{\alpha}:=\vec{\tau}]=\rho$

σ^{″} [\vec{α} := \vec{τ}] = σ^{'}

$\sigma''[\vec{\alpha}:=\vec{\tau}]=\sigma'$

Nadal uważam, że istnieje nieprecyzja w tym, jak używa lematu. Istnieje jednak rozwiązanie (muszę podziękować Barbary Petit, która przyszła z rozwiązaniem).

W rzeczywistości rozwiązanie pochodzi z definicji (def. 4.2.1), co jest moralnie następujące: $\geq$

$\sigma>\rho\quad$ if $\quad\dfrac{\Gamma\vdash P:\sigma}{\Gamma\vdash P:\rho}$

Jednak zamiast zdefiniować go w ten sposób, definiuje relację tylko w kategoriach typów. Zaletą definiowania go w kategoriach sekwencji jest to, że możemy wywnioskować, że jeśli , to , czego dokładnie potrzebuje w dowodzie (i skąd pochodzi nieprecyzja). $\sigma>\forall\alpha.\sigma$ $\alpha\notin FV(\Gamma)$

— Alejandro DC
źródło

Zastosowałem tę technikę w rozszerzeniu Systemu F do rachunku liniowo-algebraicznego rachunku lambda. Artykuł ze wszystkimi szczegółami dowodu pojawił się dzisiaj w LMCS 8 (1:11) .

— Alejandro DC,