Теория категорий в информатике и инженерии
С.П.Ковалев, А.В.Михалёв
Аннотация курса: Цель курса – ознакомить слушателей с современными математическими методами инженерии программного обеспечения, основанными на теории категорий. Теоретико-категорный аппарат позволяет формально описывать, анализировать, верифицировать и оптимизировать процессы создания сложных гетерогенных программных систем. В ходе курса будут изложены все базовые понятия теории категорий, и будет рассмотрен ряд специализированных теоретико-категорных конструкций для решения задач теории и практики разработки программ.
Тематическое содержание курса:
Тема 1 Принципы формального подхода в инженерии программного обеспечения
Тема 2 Алгебраический подход к формализации предметных областей
Тема 3 Понятие категории, появление категорий в информатике и инженерии
Тема 4 Классификация морфизмов, факторизационные системы
Тема 5 Диаграммное описание комплексирования программных систем, копределы, виды копределов
Тема 6 Формальная декомпозиция систем, пределы
Тема 7 Формальное мультимоделирование, функторы
Тема 8 Естественные преобразования, монады
Тема 9 Гармонизация формальных методов, сопряжение функторов
Тема 10 Формальные технологии проектирования программных систем
Тема 11 Трассируемые трансформации моделей программ, категории запятой
Тема 12 Теоретико-категорная семантика аспектно-ориентированного программирования
Тема 13 Категорная теория типов данных, экспоненты
Тема 14 Категорные модели вычислительных и интерактивных систем, алгебры и коалгебры
Тема 15 Категорная логика, топосы
Тема 16 Категорные модели схем, моноидальные категории
Тема 17 Категорификация знания, высшие категории
Тема 18 Теория категорий как математический аппарат системной инженерии
Типовые контрольные задания
• Постройте формальную модель качества какого-либо известного Вам программного изделия, и предложите формальные методы, подходящие для обеспечения основных требований качества.
• Постройте спецификацию мультиграфа как многосортной алгебраической системы.
• Докажите, что категория Mon всех моноидов и всех их гомоморфизмов является полной подкатегорией в CAT.
• Докажите, что произвольный регулярный мономорфизм является эпиморфизмом тогда и только тогда, когда он является изоморфизмом.
• Докажите, что категория Pos всех частично упорядоченных множеств и всех их гомоморфизмов имеет факторизационную систему (Epi, RegMono).
• Докажите, что произведение ассоциативно.
• Опишите способ построения копределов в категории стрелок над кополной категорий.
• Представьте (ко)предел как естественное преобразование.
• Постройте левый и правый сопряженные к забывающему функтору из категории Top в Set (Top – категория всех топологических пространств и всех непрерывных отображений).
• Сформулируйте понятие коэкспоненты, докажите, что в категории Set коэкспонента BA существует тогда и только тогда, когда хотя бы один из объектов A или B является пустым множеством.
• Докажите, что в любой формальной технологии проектирования функтор выделения интерфейсов сохраняет копределы всех конфигураций.
• Докажите, что среди всех функторов с областью Pos существует ровно два различных унивалентных корефлектора (с точностью до эквивалентности категорий), и объясните смысл этого факта в контексте моделирования поведения программных систем.
• Опишите способ построения копредела диаграммы в категории H-коалгебр для произвольного эндофунктора H.
Основная учебная литература:
• Голдблатт Р. Топосы. Категорный анализ логики. М.: Мир, 1983.
• Ковалёв С.П. Теоретико-категорный подход к метапрограммированию. M: ИПУ РАН, 2014. http://ccfit.nsu.ru/~kovalyov/publications/formal-tech-preprint.pdf.
• Маклейн С. Категории для работающего математика. М.: Физматлит, 2004.
• Непейвода Н.Н. Прикладная логика. Новосибирск: НГУ, 2000.
• Adámek J., Herrlich H., Strecker G. Abstract and Concrete Categories. NY: Wiley and Sons (1990). http://katmat.math.uni-bremen.de/acc/acc.pdf.
• Baez J., Stay M. Physics, Topology, Logic and Computation: A Rosetta Stone. Lecture Notes in Physics. 2011. Vol. 813. P. 95–172. http://math.ucr.edu/home/baez/rosetta.pdf.
Дополнительная учебная литература:
• Бениаминов Е.М. Алгебраические методы в теории баз данных и представлении знаний. М.: Научный мир, 2003.
• Ковалёв С.П. Формальный подход к разработке программных систем. Новосибирск: НГУ, 2004. http://ccfit.nsu.ru/~kovalyov/formal-IT/formal-IT-final.zip.
• Соммервилл И. Инженерия программного обеспечения. 6-е изд. М.: «Вильямс», 2002.
• Adámek J. Introduction to Coalgebra. Theory and Application of Categories. 2005. Vol. 14(8). P. 157–199.
• Barr M., Wells C. Category Theory for Computing Science. Prentice Hall, 1998.
• Diskin Z., Kokaly S., Maibaum T. Mapping-aware Megamodeling: Design Patterns and Laws. Lecture Notes in Computer Science. 2013. Vol. 8225. P. 322–343.
• Fiadeiro J.L. Categories for Software Engineering. Berlin Heidelberg N. Y.: Springer, 2005.
• Giesa T., Spivak D.I., Buehler M.J. Category Theory Based Solution for the Building Block Replacement Problem in Materials Design. Advanced Engineering Materials. 2012. Vol. 14, Issue 9. P. 810–817.
• Goguen J. A categorical manifesto. Mathematical Structures in Computer Science. 1991. Vol. 1(1). P. 49–67.
• Sassone V., Nielsen M., Winskell G. Deterministic behavioural models for concurrency. Lecture Notes in Computer Science. V. 711, 1993. P. 682–692.
Перечень ресурсов информационно-телекоммуникационной сети «Интернет»:
• https://ncatlab.org/nlab/show/HomePage
• http://www.logicmatters.net/categories/