![[info]](http://l-stat.livejournal.com/img/userinfo.gif?v=92.1){kind=small}
![[info]](http://l-stat.livejournal.com/img/community.gif?v=92.1){kind=small}
Что уважаемое сообщество может порекомендовать из литературы по вычислительной теории категорий? Замечательную книгу Rydeheard, Burstall "Computational Category Theory" усвоил, однако её можно считать скорей введением и обзором возможностей ML в смысле реализации категориальных определений, чем существенной почвой для работы. Собственно, два сколько-нибудь существенных приложения в ней - алгоритм унификации и описание семантики, служат как proof of concept потенциальных расчётных задач: они неэффективны и могут быть лучше реализованы без привлечения высокоуровневых категориальных абстракций.
Какие интересные задачи решают, опираясь на (существенно) конструктивную природу категорий? Возможно, что-то из теории топосов? Заранее спасибо за любые предложения!
January 17 2012, 03:34:25 UTC 4 months ago
http://www.di.ens.fr/~longo/download.ht
а действительно интересные приложения? Пойдите на сайт Андреаса Бласса
http://www.math.lsa.umich.edu/~ablass/
и почитайте всё подряд,там много интересного. Вот, например, такой текст
http://www.math.lsa.umich.edu/~ablass/7
http://www.math.lsa.umich.edu/~ablass/7
Бласс старается применять абстрактные вещи "в мирных целях". Вот придумал, как применять ультрафильтры для доказательства финитных комбинаторных теорем
http://www.math.lsa.umich.edu/~ablass/u
http://www.math.lsa.umich.edu/~ablass/u
Могу похвастать, я придумал лямбда-исчисление с явной подстановкой и обычными переменными (а не деБрёйновскими цифирками), которое работает как часы. Глядя на аксиомы декартово замкнутой категории. Подождите немного, скоро будет написано (первый вариант уже написан и проверен на людях - надо переписать понятнее).
January 17 2012, 06:06:45 UTC 4 months ago
Но вот сейчас ещё раз посмотрел. Нашёл много интересного, спасибо! ;-)
Почему-то, долго не хотело ЖЖ отмечать этот коммент, как "not spam".
January 17 2012, 16:36:48 UTC 4 months ago
January 17 2012, 05:45:42 UTC 4 months ago
January 17 2012, 06:03:47 UTC 4 months ago
> опираясь на (существенно) конструктивную природу категорий?
Ну, с логикой и вычислениями работают "комбинаторно", но тем не менее, очень наглядно и понятно.
Где-то и в около геометрии возникает немало. Например, пучки весьма намекают — топос каких-нибудь пучков, как правило, не булевый.
Можно посмотреть за претопосы, хотя и пока что, сколько-то их пользуют, как модель предикативной математики. Но и многое другое в них можно делать. Например, в П-претопосах можно определить склейку.
С точки зрения программирования, претопосы можно уподобить Agda vs. CoQ — в претопосах нет классификатора.
Не знаю, что тут можно готового поизучать...
С этой стороны, меня интересуют категории
1. Конечно-порождённые
2. Те, которые были порождены конечно-порождёнными
3. Те, которые были порождены теми, что были порождены конечно-порождёнными
4. ...
;-)