Доказательство Барендрегтом предметной редукции для

Я нашел проблему в доказательстве понижения субъекта Барендрегтом (Thm 4.2.5. Лямбда-исчисления с типами ).

Последний шаг доказательства (стр. 60) гласит:

"и, следовательно, по лемме 4.1.19 (1), $\quad\Gamma,x:\rho\vdash P:\sigma'$ . "

Однако согласно лемме 4.1.19 (1) это должно быть $\Gamma[\vec{\alpha}:=\vec{\tau}],x:\rho\vdash P:\sigma'$ , поскольку подстановка выполняется для всего контекста, а не только для $x:\rho'$ ,

Я думаю, стандартное решение может состоять в том, чтобы как-то доказать, что $\vec{\alpha}\notin FV(\Gamma)$ , но я не уверен, как это сделать.

У меня было доказательство, упрощающее его, ослабив лемму абстракций поколения, но недавно я обнаружил, что была ошибка, и мое доказательство неверно, поэтому я не уверен, как решить эту проблему больше.

Может кто-нибудь, пожалуйста, скажите мне, что мне здесь не хватает?

lo.logic type-theory lambda-calculus proof-theory Алехандро, округ Колумбия
источник

Barendregt предполагает так называемое соглашение о переменных, что связанные имена переменных и имена свободных переменных стандартизированы отдельно , а именно, мы неявно предполагаем, что они разные (используя

α

$\alpha$ преобразование. Может быть, это поможет.

Дейв Кларк,

Γ, 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'$

Алехандро, округ Колумбия,

Ответы:

Я все еще думаю, что в том, как он использует лемму, есть неточность. Однако есть решение (я должен поблагодарить Барбару Пети, которая пришла с решением).

Фактически, решение приходит из определения (определение 4.2.1), которое морально таково: $\geq$

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

Однако вместо того, чтобы определять его таким образом, он определяет отношение только с точки зрения типов. Преимущество определения его в терминах последовательностей заключается в том, что мы можем сделать вывод, что если , то , что именно то, что ему нужно в доказательстве (и откуда приходит неточность). $\sigma>\forall\alpha.\sigma$ $\alpha\notin FV(\Gamma)$

Алехандро, округ Колумбия
источник

Я использовал эту технику в расширении Системы F для линейно-алгебраического лямбда-исчисления. Документ со всеми деталями доказательства появился сегодня в LMCS 8 (1:11) .

Алехандро, округ Колумбия,