?

Log in

Программирование с зависимыми типами [entries|archive|friends|userinfo]
Программирование с зависимыми типами

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

Как матчит Агда? [Oct. 16th, 2013|08:59 pm]
Программирование с зависимыми типами
nealar
[Tags|]

В брутальном [мета-]введении в Агду попался пример

data _≤_ : ℕ → ℕ → Set where
z≤n : ∀ {n} → zero ≤ n
s≤s : ∀ {n m} → n ≤ m → succ n ≤ succ m

sub₀ : (n m : ℕ) → m ≤ n → ℕ
sub₀ n zero (z≤n .{n}) = n
sub₀ .(succ n) .(succ m) (s≤s {m} {n} y) = sub₀ n m y

Не могу понять, как определение sub0 раскрывается в case, а главное, почему так.

Тайна раскрыта
Агда матчит в том порядке, в котором написано в программе: по первой строчке выбирается паттерн с конструктором, соответствующая переменная раскрывается в case, и так далее.
Ошибка oxij в том, что по аргументам с точкой паттерн-матчить вообще нельзя

Приз "за лучшую подсказку" уходит к nivanych
Link16 comments|Leave a comment

Dependently-Typed Metaprogramming in Agda by Conor McBride [Aug. 30th, 2013|12:26 am]
Программирование с зависимыми типами

lelf
https://www.youtube.com/channel/UCqm9psjm_czCS0EXCjr3A4w
LinkLeave a comment

The HoTT Book [Jun. 21st, 2013|02:53 pm]
Программирование с зависимыми типами
nivanych
http://homotopytypetheory.org/book/
http://homotopytypetheory.org/2013/06/20/the-hott-book/
http://golem.ph.utexas.edu/category/2013/06/the_hott_book.html
LinkLeave a comment

Уникальные типы в Агда [Jan. 24th, 2013|12:30 am]
Программирование с зависимыми типами
dima_starosud
[Tags|]

Теперь можно доказывать корректность императивных программ с помощью зависимых типов.
Link1 comment|Leave a comment

Введения в Agda [Jan. 23rd, 2013|11:09 pm]
Программирование с зависимыми типами

deni_ok
[Tags|]

Пара хороших введений в Агду. Оставлю здесь, чтобы было куда ссылаться.

Peter Divianszky (Eötvös Loránd University, Department of General Computer Science)
https://people.inf.elte.hu/divip/AgdaTutorial/Index.html

Thorsten Altenkirch (School of Computer Science, the University of Nottingham)
http://www.cs.nott.ac.uk/~txa/g53cfr/
Link7 comments|Leave a comment

coq затык [Nov. 17th, 2010|09:51 pm]
Программирование с зависимыми типами

zelych
Подскажите, пожалуйста.
Вот у меня есть индуктивный предикат:
  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.

Спасибо.
Link5 comments|Leave a comment

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

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 у меня очень скудная.
Link2 comments|Leave a comment

сайт вопросов и ответов, посвящённый информатике [Jul. 16th, 2010|02:39 am]
Программирование с зависимыми типами

beroal
то бишь computer science. Здесь собирают подписи.
LinkLeave a comment

coq-загадка [Jul. 6th, 2010|11:24 pm]
Программирование с зависимыми типами

zelych
А вот если выразить логические связки в таком виде:

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_distrRead more...Collapse )
Отгадка для or_assocRead more...Collapse )
Подскажите что-нибудь, пожалуйста.
Link14 comments|Leave a comment

She. [Apr. 3rd, 2010|07:09 pm]
Программирование с зависимыми типами

thesz
[Tags|, ]

She is the Strathclyde Haskell Enhancement.

Препроцессор, добавляющий в Хаскель полезные вещи из области зависимых типов. Например, типы, индексированные данными.

Написан Конором МакБрайдом на его пути к Эпиграмму.

Узнал об этом через PFP Planet, из записи nealar.
Link2 comments|Leave a comment

navigation
[ viewing | most recent entries ]
[ go | earlier ]