====== Теория категорий в информатике и инженерии ====== === С.П.Ковалев, А.В.Михалёв === ---- **Аннотация курса**: Цель курса – ознакомить слушателей с современными математическими методами инженерии программного обеспечения, основанными на теории категорий. Теоретико-категорный аппарат позволяет формально описывать, анализировать, верифицировать и оптимизировать процессы создания сложных гетерогенных программных систем. В ходе курса будут изложены все базовые понятия теории категорий, и будет рассмотрен ряд специализированных теоретико-категорных конструкций для решения задач теории и практики разработки программ. **Тематическое содержание курса:** Тема 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. **Перечень ресурсов информационно-телекоммуникационной сети «Интернет»:** • http://www.tac.mta.ca/tac/ • https://ncatlab.org/nlab/show/HomePage • http://www.logicmatters.net/categories/ • http://math.mit.edu/~dspivak/informatics/ • http://ccfit.nsu.ru/~kovalyov/