?

Log in

Влажные мечты о категорной имплементации математики - Дважды мудак [entries|archive|friends|userinfo]
Декларативное рулит

Site Meter

[ website | Мой сайт ]
[ userinfo | livejournal userinfo ]
[ archive | journal archive ]

Влажные мечты о категорной имплементации математики [фев. 22, 2017|10:59 am]
Andy Melnikov
[Tags|, , ]

У меня давно была мечта - чтобы было такое компактное здание математики, где определения и теоремы даются в одну строчку из более общих. Не важно в каком виде (формального текста, естественного текста, интерактивной тулзы).

Условно, что монада - это моноид в категории эндофункторов, такой птичий язык, сепульки-сепулькарии-сепуление, но без циклов.

Сегодня столкнулся с проблемой, что в Coq нет доки по структурной коиндукции и коиндуктивным типам.

Нет чтобы просто сказать, что СЕПУЛЬКАРИИ — устройства для сепуления структурная корекурсия встроена в ядро, продуктивность фикспоинтов коалгебр постулируется, а ключевое слово CoFixpoint просто говорит коку, что дальше у нас Мю Ню и коалгебра.

Вместо этого у них целый туториал как официальная дока, где рассусоливают на 5 страницах что-то про guardedness. Тьфу на них.
СсылкаОтветить

Comments:
[User Picture]From: zinal
2017-02-22 07:51 pm
Вы таки не поверите - они ж для людей стараются. Которые в теории не очень бум-бум, но на практике таки нуждаются. Вот для них туториал очень даже, да, - в отличие от птичьего языка!
(Ответить) (Thread)
[User Picture]From: nponeccop
2017-02-22 08:52 pm
Ну я не против туториалов, но отсутствие какой-либо доки по коиндукции, кроме туториала - это как-то слишком.
(Ответить) (Parent) (Thread)
[User Picture]From: maxim
2017-02-23 02:31 am
> продуктивность фикспоинтов коалгебр постулируется

почему только коалгебр, фикспойнты алгебр тоже постулируются!
(Ответить) (Thread)
[User Picture]From: nponeccop
2017-02-23 02:50 am
так с документацией рекурсии получше
(Ответить) (Parent) (Thread)