Павел Собоцинский: «Алгебраические теории и струнные диаграммы»

30 сентября 2021 г. Часть коллоквиума Института Топос. - Аннотация: В теориях Ловера центральную роль играют категории с конечными произведениями. Свободная категория с конечными произведениями на одном объекте (FinSet^op) — это теория Ловера пустой алгебраической теории, а свободная категория с конечными произведениями на сигнатуре (алгебраической теории) имеет конкретное описание как категория классических синтаксических терминов. Но, используя теорему Томаса Фокса, мы также можем хорошо описать эти категории с помощью строковых диаграмм. Строковый диаграммный подход позволяет продвинуться дальше обычного синтаксиса. В статье на POPL 21, написанной совместно с Иваном ди Либерти, Фоско Лореджианом и Чадом Нестером, мы разработали подход в стиле Ловера к алгебраическим теориям с частично определенными операциями. Оказывается, что в этом контексте вместо категорий с конечными произведениями релевантным понятием являются дискретные декартовы категории ограничений (dcrc). Диаграммы строк — это подходящий синтаксис для данной ситуации: они позволяют нам описать свободную dcrc объекта и свободную dcrc сигнатуры. Я кратко изложу некоторые из наших результатов и расскажу о некоторых последствиях, включая диаграммное описание категорий со свободными конечными пределами.