Formalised in the study of symmetric monoidal categories, string diagrams are a graphical syntax that has found applications in many areas of Computer Science. Our work aims at systematising and expanding what could be thought of as the core of this visual formalism for dealing with relations and partial functions. To this end, we identify gs-monoidal categories and their graphical representation as a convenient, minimal structure that is useful to formally express such notions. More precisely, to show that such structures naturally arise, we prove that the Kleisli category of a strong commutative monad over a cartesian category is gs-monoidal. Then, we discuss how other categories providing a formalisation of "partial arrows", such as p-categories and restriction categories, are related to gs-monoidal categories. This naturally introduces a pre-order enrichment on gs-monoidal categories, and an equivalence of arrows, called "gs-equivalence": we conclude presenting a completeness result of this equivalence for models defined as lax functors to $\mathbf{Rel}$.
翻译：字符串图是一种图形语法,它已经在计算机科学的许多领域找到了应用。 我们的工作旨在系统化和扩大可以被视为处理关系和部分功能的视觉形式主义核心的内容。 为此, 我们确定基因- 分子分类及其图形表达方式是一个方便、 最低限度的结构, 有助于正式表达这些概念。 更准确地说, 为了显示这种结构自然产生, 我们证明, 一种强烈的交融性月球的Kleisli类别是gs- monad。 然后, 我们讨论其他类别如何提供“ 局部箭头” 的正规化, 如 p- 分类和限制类别。 这自然地引入了一种对gs- mondal 类别和箭头等同的顺序前浓缩, 称为“ Q- evalence ” : 我们得出结论, 将这种等同性作为被定义为 $\\\ mathb{Rel$} 。
相关内容
微信扫码咨询专知VIP会员