deniok: (Default)
[personal profile] deniok
Сделал в ру-Википедии статью про сабж. Еле поспел к Рождеству.  Держите.
(deleted comment)

Date: 2013-01-11 10:33 am (UTC)
From: [identity profile] ro-che.info (from livejournal.com)
Индукцией по генерации M вроде даказывается.
Я ж выше привел пример, когда это просто неверно.

Не предполагая этого правила ("в контекст можно добавлять "свежую" для этого контекста переменную"), тип (\x:a.\x:b.x) вывести нельзя.

Поэтому это правило надо формально добавить в набор правил типизации.

Date: 2013-01-12 10:17 am (UTC)
From: [identity profile] ro-che.info (from livejournal.com)
Если связанных с ней переименований не предполагать, то перестаёт работать лемма генерации (у Пирса - лемма инверсии)
 (Γ ⊢ λx:σ.M):ρ ⇒ ∃ τ (Γ,x:σ ⊢ M:τ ∧ ρ = σ → τ) 
поскольку мы не можем более предполагать, что x∉Γ.


Да, в таком виде, конечно, работать не будет. Но работает тривиальная модификация;

(Γ ⊢ λx:σ.M):ρ ⇒ ∃ τ: ∃ Γ' ⊆ Γ: (Γ',x:σ ⊢ M:τ ∧ ρ = σ → τ)

На самом деле, я ничего не имею против отождествления альфа-эквивалентных термов. Но оно не было оговорено в статье. Я всего лишь заметил, что исходя из того, что описано в статье, приведенный терм не типизируется.
Edited Date: 2013-01-12 10:17 am (UTC)

Date: 2013-01-12 10:37 am (UTC)
From: [identity profile] deni-ok.livejournal.com
Согласен, без какой-то обработки альфа-эквивалентных термов или дополнительных правил типизации этот терм не типизируется. Но мне кажется, что это такой немножко маргинальный факт, касающийся скорее весьма свободной дисциплины именования переменных "пользователем", а не коренных свойств этой системы типов. Я думаю, что в небольшой энциклопедической статье его обсуждать было бы неуместно. К тому же в обоих АИ для статьи (Барендрегт и Пирс) простые типы типизируются именно так, с одной аксиомой (и подразумеваемым соглашением Барендрегта).

Profile

deniok: (Default)
deniok

February 2022

S M T W T F S
  12345
6789101112
13141516171819
20212223 242526
2728     

Most Popular Tags

Style Credit

Expand Cut Tags

No cut tags
Page generated Jul. 11th, 2025 08:57 pm
Powered by Dreamwidth Studios