?

Log in

No account? Create an account
кортежи с именованными компонентами как dependent product - Программирование с зависимыми типами [entries|archive|friends|userinfo]
Программирование с зависимыми типами

[ userinfo | livejournal userinfo ]
[ archive | journal archive ]

кортежи с именованными компонентами как dependent product [Jul. 20th, 2010|04:11 am]
Программирование с зависимыми типами

ru_deptypes

[beroal]
Рассмотрим типизированные кортежи с именованными компонентами. Множество имён компонентов KS одно для всех кортежей, но кортеж может иметь не все компоненты. Есть функция typeof, которая отображает имя компонента на тип компонента. Множество функций с зависимым типом, у которых зависимость типа результата от значения аргумента задаётся typeof, и есть множество кортежей с компонентами из KS.

KS0 ⊆ KS ∧ KS1 ⊆ KS. Если истинно KS0 ⊆ KS1, то существует проекция, которая берёт кортеж с именами KS1 и возвращает кортеж с именами KS0. Проекция всего лишь выбрасывает те компоненты кортежа, имена которых ∈ KS1 и ∉ KS0, потому я назвал её проекцией. KS0 ⊆ KS1 можно превратить как каноническую инъекцию inj : KS0 → KS1. Тогда интуитивно это описывается как «инъекция превращается в проекцию». Если построить категорию (обозначим её (P KS)) из ЧУМ подмножеств KS, имею контравариантный функтор D : P KS → Set (и пучок).

Как доказать свойства D из свойств dependent product? typeof использовать не получится, вместо typeof имеем bundle для каждого KS0, KS0 ⊆ KS. pullback functor inj* должен отображать bundle для KS1 в bundle для KS0, bundle-ы разумеется связаны. Морфизм KS0→1 (назову его (final KS0)) (1 — это singleton, я работаю в Set) задаёт функтор Π (final KS0), который берёт bundle для KS0 и возвращает собственно множество кортежей с именами KS0.

Дальше затык. Информация по dependent product у меня очень скудная.
LinkReply

Comments:
[User Picture]From: thesz
2010-07-20 06:13 am (UTC)
О, блин.

А в Coq/Agda пробовал?
(Reply) (Thread)
[User Picture]From: beroal
2010-07-20 10:52 am (UTC)
Обычно начинают с доказательства на бумаге, это проще.

Или ты имел в виду shallow embedding? Должно сработать, надо будет попробовать. Хотя это не так интересно. ;)
(Reply) (Parent) (Thread)