Теория категорий [entries|friends|calendar]
Теория категорий

[ userinfo | livejournal userinfo ]
[ calendar | livejournal calendar ]

This is the (co)end, my only (co)friend [07 May 2015|10:46am]
nivanych
"Раз пошла такая пьянка" и у ivan_gandhi
в его блоге постоянно стали упоминаться
(ко)концы и расширения Кана, то возник повод
вспомнить и про соответствующую статью ;-)
Кое-кто будет на неё ругаться и даже обзываться,
но я таки отрекламирую —

http://arxiv.org/abs/1501.02503
This is the (co)end, my only (co)friend
Fosco Loregian
The present note is a recollection of the most striking and useful applications of co/end calculus.
We put a considerable effort in making arguments and constructions rather explicit:
after having given a series of preliminary definitions, we characterize co/ends as particular co/limits;
then we derive a number of results directly from this characterization.
The last sections discuss the most interesting examples where co/end calculus serves as a powerful abstract way to do explicit computations in diverse fields like Algebra, Algebraic Topology and Category Theory.
The appendices serve to sketch a number of results in theories heavily relying on co/end calculus;
the reader who dares to arrive at this point, being completely introduced to the mysteries of co/end fu, can regard basically every statement as a guided exercise.
2 comments|post comment

A first-order logic for string diagrams [05 May 2015|10:42am]
nivanych
Ещё всем известные тов. Joyal & Street немало постарались формализовать "Tensor Calculus".
Вот некая попытка сделать шаг вперёд —
http://arxiv.org/abs/1505.00343
A first-order logic for string diagrams
Aleks Kissinger, David Quick
Equational reasoning with string diagrams provides an intuitive means of proving equations between morphisms in a symmetric monoidal category.
This can be extended to proofs of infinite families of equations using a simple graphical syntax called !-box notation.
While this does greatly increase the proving power of string diagrams, previous attempts to go beyond equational reasoning have been largely ad hoc, owing to the lack of a suitable logical framework for diagrammatic proofs involving !-boxes.
In this paper, we extend equational reasoning with !-boxes to a fully-fledged first order logic called with conjunction, implication, and universal quantification over !-boxes.
This logic, called !L, is then rich enough to properly formalise an induction principle for !-boxes.
We then build a standard model for !L and give an example proof of a theorem яfor non-commutative bialgebras using !L, which is unobtainable by equational reasoning alone.
1 comment|post comment

[12 Apr 2015|09:50pm]

66george
Человек говорит, что в параграфе про декартовы квадраты все линии без стрелок. Я смотрю Adobe Reader и стрелки вижу. Есть такая проблема или нет?

P.S. Проблемы нет "В Evince на Debian — не видны при масштабе 125% и менее"
4 comments|post comment

Учебник, версия 8 [29 Mar 2015|05:37am]

66george


http://www.mediafire.com/download/gvmqendnmctjeor/%D0%A3%D1%87%D0%B5%D0%B1%D0%BD%D0%B8%D0%BA+%D0%B2%D0%B5%D1%80%D1%81%D0%B8%D1%8F+8.pdf

Уравнители, декартовы квадраты, топосы, монады, чуть-чуть про Мартин-Лёфа. Главу про монады, в принципе, можно читать сразу, хотя я поместил её в конец. Но не обещаю, что будет просто, хотя я старался. Совсем простая наука, видимо, закончилась. Напишу ещё одну серию (про пределы) и составлю, наконец, указатель, с которым были трудности из-за палёного миктеха. Буду рад критике.

P.S. "Можно читать сразу" тем, кто читал седьмую версию, конечно.
53 comments|post comment

[20 Dec 2014|11:34pm]

66george
И теперь вопрос, что мне дальше писать. Чисто категорного материала осталось мало (пределы и копределы). Я хотел ещё написать большую развесистую главу про лямбда-исчисление, но тут выбор такой:
1) Писать, как Барендрегт (то есть, замалчивать самые сложные места);
2) Писать лучше Барендрегта, но для этого в данный момент у меня нет авторитета, отложим до лучших времён.
Замечено две опечатки и один умеренный ляп в не самом важном месте. Так что склоняюсь к тому, чтобы дописать пределы и копределы, исправить опечатки и пока закончить. Могу также разбить главу про сопряжённость на несколько разделов поменьше.
Вообще, первоначально был план "написать популярную брошюрку страниц на сто", план уже перевыполнен в два раза, пора заканчивать.
3 comments|post comment

Щедров в Москве [15 Dec 2014|12:30am]

66george
"Дорогие участники семинаров. Пересылаю информацию о предстоящих лекциях Андрэ Щедрова и Макса Кановича на факультете компьютерных наук ВШЭ.

From A. Scedrov:

Max and I are teaching a course at the new HSE location near the metro station Aeroport. Please see the schedule of the lectures at
http://aspirantura.hse.ru/cs/syllabus/collaborative
Basically I will be starting my part of the course (1-4) next week, December 16 and Max will be starting his part (5) the following week, December 21. If you or your colleagues have any students interested in this material, please let them know about the course."

Не знаю, пускают ли туда и какой нужен пропуск, спрашивайте Шеня (a_shen)
1 comment|post comment

Сборка `программистских` статей "про категории" [22 Nov 2014|01:16pm]

beroal
Originally posted by nivanych at Сборка `программистских` статей "про категории"
Нуу, программистскими те объяснения можно считать условно, но всё-таки.
http://bartoszmilewski.com/category/category-theory/
Всё-всё не читал, но что проглядел — вроде, неплохо написано.
(жаль, но забыл уже, кто мне ссылку подогнал, а то поблагодарил бы)
post comment

теория категорий пришла на смену UML [21 Oct 2014|02:54pm]

beroal
Вы увидите, что ТК:

- позволяет обоснованно, стройно и логично спроектировать классы
- пришла на смену UML

Отзывы людей, уже знакомых с ТК:

Теория категорий настолько универсальна, что в её терминах можно описать все, что угодно, например, математические выражения, алгоритмы или поход в магазин.

Евгений Черный.

Как же можно обойтись без восхищённых отзывов? Мы своей головой судить не можем. Монадические технологии идут на смену крестьянской лошадке! Концентрированная менеджерская уткоречь. «Вконтакте».

«С тех пор, как я начал заниматься теорией категорий, у меня повысилось самочувствие и появилось много жизненной энергии. Я чувствую себя на 20 лет моложе!»
27 comments|post comment

унификация термов [20 Oct 2014|02:33am]

beroal
Полемика по поводу Joseph A. Goguen. “What is Unification? A Categorical View of Substitution, Equation and Solution.” (1989). Эта статья описывает унификацию в русле традиции, то есть подробно обсуждает унификацию 2 термов, то есть решение 1 уравнения. На практике приходится решать систему уравнений. Возьмём вывод типов для лямбда-исчисления. Каждый узел абстрактного синтаксического дерева программы даёт несколько уравнений, причём эти уравнения обычно имеют примитивную форму вроде τ01→τ2. В этом уравнении нечего решать. :-) Зато уравнений много. Более того, терм можно разбить на систему примитивных уравнений, например
f0(v0, f1(v1, f2(v2)))

f0(v0, v3);
v3 = f1(v1, v4);
v4 = f2(v2).
Примитивные уравнения я считаю более общей постановкой задачи, так как не знаю способа, как соединить систему примитивных уравнений в 1 уравнение термов (существует ли этот способ?). Хочу увидеть теоретический фундамент именно для системы уравнений.
3 comments|post comment

Вопросы про identity types [27 Sep 2014|07:19pm]

os80
Коллеги, может быть, вопрос не совсем в тему сообщества, но куда задать вопрос по теории типов — не знаю.
А так как началось всё с HoTT, про которую узнал тут, решил здесь и спросить.

Никак не могу понять, что такое identity types, которые "b =A c".
1. Может ли кто-то понятно объяснить с конкретными примерами, что это такое?
2. Знает ли кто-нибудь хороший paper на эту тему?
3. Читаю "Martin-Löf's Type Theory" by Nordström et al. Там на 8-й странице (вторая снизу формула) делается следующее утверждение: если a∈A, то a=a∈A. С учётом написанного там ранее, это у меня интерпретируется как "если 1 принадлежит натуральным числам, то доказательство того, что 1=1 тоже принадлежит натуральным числам". Но это же бред, товарищи, в каком месте я не прав?
15 comments|post comment

Нуб нид хелп [15 Sep 2014|10:17am]
tancorko
Господа, наверняка я не первый кто пристает с вопросом с какой книги лучше начать знакомство. Не могли бы вы мне помочь?
К примеру пока рассматриваются: Голдбалтт Топосы. Категоральный анализ логики, Маклейн Теория категорий для работающего математика, учебник Георгия (66george).
23 comments|post comment

Category Theory Using String Diagrams [26 Aug 2014|10:05am]
nivanych
Может, кому пригодится.
Category Theory Using String Diagrams
Dan Marsden
AbstractCollapse )
http://arxiv.org/abs/1401.7220
6 comments|post comment

Новый термин узнал — The Schanuel topos [19 Jul 2014|12:52pm]
nivanych
The Schanuel topos (also called the Myhill-Schanuel topos) is the Grothendieck topos of combinatorial functors.
It plays an important role in computer science in the theory of name-binding calculi and in William Lawvere’s approach to petit toposes.
http://ncatlab.org/nlab/show/Schanuel+topos
И вроде, у Johnstone'а это есть, но как-то пропустил...
3 comments|post comment

Corecursive Algebras, Corecursive Monads and Bloom Monads [17 Jul 2014|11:07am]
nivanych
Jiří Adámek, Mahdie Haddadi, Stefan Milius
Corecursive Algebras, Corecursive Monads and Bloom Monads

An algebra is called corecursive if from every coalgebra a unique coalgebra-to-algebra homomorphism exists into it.
We prove that free corecursive algebras are obtained as coproducts of the terminal coalgebra (considered as an algebra) and free algebras.
The monad of free corecursive algebras is proved to be the free corecursive monad, where the concept of corecursive monad is a generalization of Elgot's iterative monads, analogous to corecursive algebras generalizing completely iterative algebras.
We also characterize the Eilenberg-Moore algebras for the free corecursive monad and call them Bloom algebras.
http://arxiv.org/abs/1407.4425
2 comments|post comment

Lawvere's fixed point theorem [05 Mar 2014|11:05am]
nivanych
http://ncatlab.org/nlab/show/Lawvere%27s+fixed+point+theorem
For any cartesian closed category, if there is an epimorphism from some object A to the exponential object/internal hom from A into some other object B
A⟶B^A
then every endomorphism f:B→B of B has a fixed point.

Дайте хороших жизненных примеров! ;-)
21 comments|post comment

Free Applicative Functors [05 Mar 2014|11:04am]
nivanych
Applicative functors are a generalisation of monads.
Both allow the expression of effectful computations into an otherwise pure language, like Haskell.
Applicative functors are to be preferred to monads when the structure of a computation is fixed a priori.
That makes it possible to perform certain kinds of static analysis on applicative values.
We define a notion of free applicative functor, prove that it satisfies the appropriate laws, and that the construction is left adjoint to a suitable forgetful functor.
We show how free applicative functors can be used to implement embedded DSLs which can be statically analysed.
http://arxiv.org/abs/1403.0749
post comment

Почему порождающие семейства следует называть "порождающими"? [11 Feb 2014|04:32pm]
oskar_808
Несколько месяцев назад в сообществе был задан вопрос - как перевести на русский язык слово "generator" и словосочетание "generating family": http://category-theory.livejournal.com/22084.html#comments. Участники предложили массу различных вариантов перевода, однако все сошлись на мнении, что переводы "порождающий объект" и "порождающее семейство" не подходят по смыслу, так как они "ничего не порождают"(см. комментарии). Я тоже тогда с этим согласился - именно поэтому я решил "исправиться" и сделать данный разъясняющий постинг.

Пост состоит из трёх частей: в первой части будут представлены аргументы за довольно популярные на данный момент переводы "разделяющий объект" и "разделяющее семейство", также будут даны определения и примеры этих самых "разделяющих семейств" - надеюсь, эта часть будет доступна всем участникам сообщества; во второй части я постараюсь объяснить, почему всё-таки переводы "порождающий объект" и "порождающее семейство" также подходят по смыслу; в третьей части я введу в обращение новый тип порождающих семейств(расщепимые порождающие семейства), кое-что про них расскажу и сделаю заключительные комментарии.

1. "Разделяющие" семейства.Collapse )
2. "Порождающие" семейства.Collapse )
3. Расщепимые порождающие семейства.Collapse )

Выводы. Безусловно, оба перевода("разделяющий" и "порождающий") уместны. Но надо заметить, что термин "разделяющий" отражает лишь смысл самого первого определения, в то время как термин "порождающий" отражает важнейшее свойство порождающих семейств(лемма 1). При доказательстве сложных теорем(таких как SAFT), особенно важно понимать, что всякий объект категории является факторобъектом копроизведения порождающих "кирпичиков", либо, если речь идёт о копорождающих семействах - подобъектом произведения копорождающих "кирпичиков".

Спасибо за внимание!
4 comments|post comment

Учебник, версия 7 [02 Feb 2014|03:03am]

66george
http://www.mediafire.com/view/w31ptgbpzdvwea8/Учебник%20версия%207.pdf

Ага, первый ляп найден (определение скелета категории 16.91). Кроме того, исправлена опечатка в примере 15.14 (в предпоследней строчке справа было указано правило VI, на самом деле VE)

P.S. Может, такая ссылка лучше

http://www.mediafire.com/download/w31ptgbpzdvwea8/%D0%A3%D1%87%D0%B5%D0%B1%D0%BD%D0%B8%D0%BA+%D0%B2%D0%B5%D1%80%D1%81%D0%B8%D1%8F+7.pdf
2 comments|post comment

Учебник, версия 6 [30 Jan 2014|09:07am]

66george
https://www.mediafire.com/?a7ypzohii4xgwx1

Написал ещё три больших главы (на самом деле, четыре, но четвёртую пока придержу). Но чем больше пишу, тем больше остаётся написать!
К главе про натуральные числа в конце добавил поучительную историю, как Клини лечил зубы под кайфом. К главе про сопряжённость в самом конце добавил две диаграммы.
Прошу всех, кто разбирается в категориях, посмотреть две последние главы на предмет грубых ляпов. Всякой другой критике тоже буду рад.
28 comments|post comment

[26 Nov 2013|11:34pm]

66george
Стоит ли переводить "bicartesian closed category" как "би-декартово замкнутая категория"? Или уж писать "декартово замкнутая категория с конечными копроизведениями"?

Русский язык длинней английского, зато витиеватей и извилистей.
1 comment|post comment

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