ro-che.info (from livejournal.com)2013-01-11 09:10 am (UTC)(link)
Да, я там явно не сказал про операцию расширения контекста: в контекст можно добавлять "свежую" для этого контекста переменную. Да. То есть надо ввести правило (Г |- M:t) => (Г,x:t' |- M:t)
А с этим правилом аксиому для переменной можно упростить таким образом: x:t |- x:t.
При типизации лямбды, кстати, эта возможность используется без явной оговорки. Не понял, о чем ты, честно говоря. Типизация какой лямбды?
Ну я, конечно, пользуюсь ещё Thinning Lemma: если один контекст является подмножеством другого, то утверждения о типизации, сделанные в более узком контексте, верны в более широком.
Чтобы это было леммой, оно должно доказываться из аксиом :)
(deleted comment)
no subject
ro-che.info (from livejournal.com)2013-01-11 10:33 am (UTC)(link)
Индукцией по генерации M вроде даказывается. Я ж выше привел пример, когда это просто неверно.
Не предполагая этого правила ("в контекст можно добавлять "свежую" для этого контекста переменную"), тип (\x:a.\x:b.x) вывести нельзя.
Поэтому это правило надо формально добавить в набор правил типизации.
no subject
ro-che.info (from livejournal.com)2013-01-12 10:17 am (UTC)(link)
Если связанных с ней переименований не предполагать, то перестаёт работать лемма генерации (у Пирса - лемма инверсии)
(Γ ⊢ λx:σ.M):ρ ⇒ ∃ τ (Γ,x:σ ⊢ M:τ ∧ ρ = σ → τ)
поскольку мы не можем более предполагать, что x∉Γ.
Да, в таком виде, конечно, работать не будет. Но работает тривиальная модификация;
На самом деле, я ничего не имею против отождествления альфа-эквивалентных термов. Но оно не было оговорено в статье. Я всего лишь заметил, что исходя из того, что описано в статье, приведенный терм не типизируется.
Согласен, без какой-то обработки альфа-эквивалентных термов или дополнительных правил типизации этот терм не типизируется. Но мне кажется, что это такой немножко маргинальный факт, касающийся скорее весьма свободной дисциплины именования переменных "пользователем", а не коренных свойств этой системы типов. Я думаю, что в небольшой энциклопедической статье его обсуждать было бы неуместно. К тому же в обоих АИ для статьи (Барендрегт и Пирс) простые типы типизируются именно так, с одной аксиомой (и подразумеваемым соглашением Барендрегта).
![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
no subject
Да. То есть надо ввести правило
(Г |- M:t) => (Г,x:t' |- M:t)А с этим правилом аксиому для переменной можно упростить таким образом:
x:t |- x:t.Не понял, о чем ты, честно говоря. Типизация какой лямбды?
Чтобы это было леммой, оно должно доказываться из аксиом :)
no subject
Я ж выше привел пример, когда это просто неверно.
Не предполагая этого правила ("в контекст можно добавлять "свежую" для этого контекста переменную"), тип
(\x:a.\x:b.x)вывести нельзя.Поэтому это правило надо формально добавить в набор правил типизации.
no subject
Да, в таком виде, конечно, работать не будет. Но работает тривиальная модификация;
(Γ ⊢ λx:σ.M):ρ ⇒ ∃ τ: ∃ Γ' ⊆ Γ: (Γ',x:σ ⊢ M:τ ∧ ρ = σ → τ)На самом деле, я ничего не имею против отождествления альфа-эквивалентных термов. Но оно не было оговорено в статье. Я всего лишь заметил, что исходя из того, что описано в статье, приведенный терм не типизируется.
no subject