Если связанных с ней переименований не предполагать, то перестаёт работать лемма генерации (у Пирса - лемма инверсии) (Γ ⊢ λx:σ.M):ρ ⇒ ∃ τ (Γ,x:σ ⊢ M:τ ∧ ρ = σ → τ) поскольку мы не можем более предполагать, что x∉Γ.
(Γ ⊢ λx:σ.M):ρ ⇒ ∃ τ (Γ,x:σ ⊢ M:τ ∧ ρ = σ → τ)
(Γ ⊢ λx:σ.M):ρ ⇒ ∃ τ: ∃ Γ' ⊆ Γ: (Γ',x:σ ⊢ M:τ ∧ ρ = σ → τ)
![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
no subject
Date: 2013-01-12 10:17 am (UTC)Да, в таком виде, конечно, работать не будет. Но работает тривиальная модификация;
(Γ ⊢ λx:σ.M):ρ ⇒ ∃ τ: ∃ Γ' ⊆ Γ: (Γ',x:σ ⊢ M:τ ∧ ρ = σ → τ)На самом деле, я ничего не имею против отождествления альфа-эквивалентных термов. Но оно не было оговорено в статье. Я всего лишь заметил, что исходя из того, что описано в статье, приведенный терм не типизируется.