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

12

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

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

"и, следовательно, по лемме 4.1.19 (1), Γ,x:ρP:σ . "

Однако согласно лемме 4.1.19 (1) это должно быть Γ[α:=τ],x:ρP:σ , поскольку подстановка выполняется для всего контекста, а не только для x:ρ ,

Я думаю, стандартное решение может состоять в том, чтобы как-то доказать, что αFV(Γ) , но я не уверен, как это сделать.

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

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

Алехандро, округ Колумбия
источник
Barendregt предполагает так называемое соглашение о переменных, что связанные имена переменных и имена свободных переменных стандартизированы отдельно , а именно, мы неявно предполагаем, что они разные (используя α преобразование. Может быть, это поможет.
Дейв Кларк,
Γ,x:ρP:σΓ,x:ρP:σρ[α:=τ]=ρσ[α:=τ]=σ
Алехандро, округ Колумбия,

Ответы:

8

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

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

σ>ρ ifΓP:σΓP:ρ

Однако вместо того, чтобы определять его таким образом, он определяет отношение только с точки зрения типов. Преимущество определения его в терминах последовательностей заключается в том, что мы можем сделать вывод, что если , то , что именно то, что ему нужно в доказательстве (и откуда приходит неточность).σ>α.σαFV(Γ)

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