| coq затык |
[Nov. 17th, 2010|09:51 pm] |
Подскажите, пожалуйста.
Вот у меня есть индуктивный предикат:
Inductive last (a: A): list A -> Prop :=
| last_one: last a (a :: nil)
| last_many: forall (l: list A) (x: A), last a l -> last a (x :: l).
Очевидно?, что last a nil быть не может. Как тогда доказать что-нибудь типа такого?
Lemma last_nil: forall (a: A), last a nil -> False.
Спасибо. |
|
|
| кортежи с именованными компонентами как dependent product |
[Jul. 20th, 2010|04:11 am] |
Рассмотрим типизированные кортежи с именованными компонентами. Множество имён компонентов 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 у меня очень скудная. |
|
|
| coq-загадка |
[Jul. 6th, 2010|11:24 pm] |
А вот если выразить логические связки в таком виде:
Definition and (p q : Prop) := forall a : Prop, (p -> q -> a) -> a.
Definition or (p q : Prop) := forall a : Prop, (p -> a) -> (q -> a) -> a.
то для них, наверное, можно доказать какие-нибудь простые свойства:
Lemma or_distr : forall p q r, or p (and q r) -> and (or p q) (or p r).
Lemma or_assoc : forall p q r, or (or p q) r -> or p (or q r).
Только у меня почему-то, хоть убей, не получается.
Думал на хаскеле будет привычнее, перевёл or_assoc на него -- тоже не решается:
{-# LANGUAGE RankNTypes #-}
type OR p q = (forall a. (p -> a) -> (q -> a) -> a)
or_assoc :: OR (OR p q) r -> OR p (OR q r)
or_assoc h1 h2 h3 = undefined
h1 :: OR (OR p q) r -- ((forall b . (p -> b) -> (q -> b) -> b) -> a) -> (r -> a) -> a
h1 or_pq ra = undefined
h2 :: p -> a
h2 = undefined
h3 :: OR q r -> a
h3 or_qr = undefined
Отгадка для or_distr( Read more... )
Отгадка для or_assoc( Read more... )
Подскажите что-нибудь, пожалуйста. |
|
|
| She. |
[Apr. 3rd, 2010|07:09 pm] |
She is the Strathclyde Haskell Enhancement.
Препроцессор, добавляющий в Хаскель полезные вещи из области зависимых типов. Например, типы, индексированные данными.
Написан Конором МакБрайдом на его пути к Эпиграмму.
Узнал об этом через PFP Planet, из записи ![[info]](http://l-stat.livejournal.com/img/userinfo.gif?v=92.2) nealar. |
|
|
| observational type theory |
[Feb. 9th, 2009|07:48 pm] |
Кто-нибудь раскусил, что такое «observational type theory» и с чем её едят? (См. пример задачи ниже.) Иль её не едят, ею любуются? ;) P. S. Статьи просматривал, голова всё равно осталась пустой.
Например, нужно записать высказывание «у морфизма m:a→b есть прообраз по функтору F». Должно получиться ∃a0.F a0 = a → ∃b0.F b0 = b → ∃m0:a0→b0.F m0 = m. Проблема в том, что в равенстве F m0 = m правая и левая части имеют разные типы, а именно: F m0:F a0→F b0 и m:a→b. Чтобы приравнять типы, надо применить равенства F a0 = a и F b0 = b. |
|
|
| Знающие люди, подскажите! |
[Dec. 26th, 2008|01:22 pm] |
Категорная модель higher order типов -- это топос.
Категорная модель зависимых типов -- это Local CCC.
Естественно, что все-все возможные системы
с зависимыми типами на практике не нужны.
Какие-то из них вполне впихиваются в топосы.
Так вот, меня взяло сомнение, а все ли "полезные"
системы типов могут упихаться в некоторый топос?...
Есть ли какая очень нужная и полезная система
с зависимыми типами, которая не описывается топосом
(топосом из топосов и функторов между ними)?...
( Дополнение )
P.S.
Надеюсь, это не оффтопик.
Есличо, подскажите, куда лучше запостить?... |
|
|
| Это не совсем про зависимые типы данных. |
[Dec. 24th, 2008|12:04 am] |
Type safe pattern matching combinators.
При чтении этой статьи у меня всё время было стойкое чувство, что я это видел в районе generic programming with dependent types.
К тому же там есть пример написания функции наподобие taut на этих комбинаторах.
Вот taut:boolPower : {n : Nat} -> Set
boolPower Zero = Bool
boolPower (Succ n) = Bool -> boolPower n
taut : {n : Nat} -> boolPower n -> Bool
taut Zero v = v
taut (Succ n) f = taut n (f true) && taut n (f false)
Иными словами, функция, принимающая на вход функцию с произвольным числом аргументов.
И используемый в статье Хаскель очень простой, даже, по-моему, Haskell 98. |
|
|
![[info]](http://l-stat.livejournal.com/img/community.gif?v=92.2){kind=small}
ru_deptypes