HoTT за програмисти

[Krasimir Angelov]

Здравейте,

Последният път когато обсъждахме хомотопичната теория на типовете,
Бойко пита какъв е смисъла на теорията в контекста на програмирането а
не в абстрактната математика. Намерих слайдове от Dan Licata:

http://www.cs.cmu.edu/~drl/pubs/lh122tttalks/lh12wg2.8.pdf

Заслужава си човек да се зачете за да усети така наречения "аха"
момент. Накратко само ще кажа че прословутата аксиома за унивалентност
на Воеводски се свежда до следното:

univalence : (A,B : Type) -> Iso A B -> A = B

където Iso А B е типа на всички изоморфизми между A и B, т.е. трипъл
съдържащ две функции f и g и доказателство за това че f е обратната на
g и обратното.

Преди два дена бях на презентация на Thorsten Altenkirch който даде
още два програмистки примера. Ще се опитам да ги възпроизведа по
памет:

- Multiset е списък в който реда на елементите е без значение. Това
може да се представи с функцията:

(n : Nat) -> (A : Type) -> Fin n = Fin n -> Multiset n A =
Multiset n A

тук Fin е тип с n на брой елементи. Множеството от изоморфизми
(еквивалентностни) за Fin е точно множеството от пермутации на n
елемента. Прилагайки пермутацията върху даден мултисет получаваме
същия мултисет.

- Cycle е цикличен списък, т.е. списък без определено начало. Това
пък изразяваме така:

(n : Nat) -> (A : Type) -> Fin n -> Cycle n A = Cycle n A

Смисъла е следния, за всеки елемент от Fin n можем да съставим един
изоморфизъм в Cycle n A който измества началото в списъка съдържащ
елементите на цикличния списък.

Двата нови типа имат интересни zippers. Нормалният линеен списък е
zipper за цикличния списък. Мултисета е zipper сам за себе си. Тъй
като за да получим zipper за даден тип трябва да диференцираме
оригиналния тип, то се оказва че Мултисета е като експонентата в
нормалното диференциално смятане т.е.:

d(Multiset) = Multiset

Поздрави,
Красимир

[Slavomir Kaslev]

Интересно. Значи бях прав, че има тънка връзка между Homotopy type theory и (exponential в случая) generating functions от Analytical combinatorics.

Поне това, което пишеш е напълно съвместимо със Седждуик и Флажоле:

Cycle(x) = ln (1/(1-x)),   съответния zipper е  d/dx Cycle(x) = 1/(1-x),  т.е. списък

Set(x) = e^x, със zipper  d/dx Set(x) = e^x = Set(x)

Permutations(x) = Set(Cycle(x)) = 1/(1-x), пак списък

Но не знам как да минавам от твоята функционална нотация (например    (n : Nat) -> (A : Type) -> Fin n -> Cycle n A = Cycle n A за цикли)

във формула за експоненциалната генерираща функция на типа. Примерите, които дадох преди работят за пресмятане на обикновени генериращи функции от algebraic datatypes, но не и за експоненциални.

 

d(Multiset) = Multiset

Поздрави,
   Красимир

--
You received this message because you are subscribed to the Google Groups "Polyglot Quine" group.
To unsubscribe from this group and stop receiving emails from it, send an email to polyglot-quin...@googlegroups.com.
To post to this group, send email to polyglo...@googlegroups.com.
Visit this group at http://groups.google.com/group/polyglot-quine.
For more options, visit https://groups.google.com/groups/opt_out.

--
Slavomir Kaslev

[Krasimir Angelov]

На 6 февруари 2014 г., 10:50, Slavomir Kaslev
<slavomi...@gmail.com> написа:

> Интересно. Значи бях прав, че има тънка връзка между Homotopy type theory и
> (exponential в случая) generating functions от Analytical combinatorics.
> Поне това, което пишеш е напълно съвместимо със Седждуик и Флажоле:

Ами не знам. В началото като заговори за преминаване от тип в Хаскел
към алгебрични функции, първата ми асоциация беше точно за начина по
които се извеждат zippers. Даже го бях споменал в един e-mail. Само
дето книгата която беше препоръчал за четене е прекалено дълга за да
се зачета. Открито си казвам, че не се опитах да разбера
подробностите. После се започна едно дърлене от което още повече ми се
отщя.

[Slavomir Kaslev]

Съгласен съм, аналитичната комбинаторика изиксва малко дълбане, за да се разбере. А дърленето ми беше неприятно и на мен, защото бях положил нетривиално услилие, за да видя, че превеждането до обикновени генериращи функции работи. Също бях уверен, че работи, защото математиката даваше правилните отговори и го бях обсъдил с Дан Пипони (sigfpe) на обяд и във вътрешния @math списък под формата на задачки докато бях в гугъл. Нямаше как да е грешно, за това, че на някой не му харесва по "естетически" причини.

Ако разбереш как се смятат експоненциални генериращи фунцкии в Хаскел, непременно пиши, ще ми е много интересно. Вероятно ще е малко по-сложно от това с обикновените генериращи фунцкии, защото според мен алгебричните типове не са достатъчни да се дефинират типове на като Set и Cycle, но може и да бъркам.

--
You received this message because you are subscribed to the Google Groups "Polyglot Quine" group.
To unsubscribe from this group and stop receiving emails from it, send an email to polyglot-quin...@googlegroups.com.
To post to this group, send email to polyglo...@googlegroups.com.
Visit this group at http://groups.google.com/group/polyglot-quine.
For more options, visit https://groups.google.com/groups/opt_out.

--
Slavomir Kaslev

[Slavomir Kaslev]

Още едни слайдове от презентация на същата тема: http://www.cs.nott.ac.uk/~txa/talks/lyon14.pdf

--
You received this message because you are subscribed to the Google Groups "Polyglot Quine" group.
To unsubscribe from this group and stop receiving emails from it, send an email to polyglot-quin...@googlegroups.com.
To post to this group, send email to polyglo...@googlegroups.com.
Visit this group at http://groups.google.com/group/polyglot-quine.
For more options, visit https://groups.google.com/groups/opt_out.

--
Slavomir Kaslev

[Krasimir Angelov]

На 9 юни 2014 г., 17:59, Slavomir Kaslev <slavomi...@gmail.com> написа:

Още едни слайдове от презентация на същата тема: http://www.cs.nott.ac.uk/~txa/talks/lyon14.pdf

Това е точно презентацията която Thorsten представи докато беше при нас в Чалмърс. Явно я е качил в интернет.