论文标题
常规逻辑的字符串图（扩展摘要）
String Diagrams for Regular Logic (Extended Abstract)
论文作者
论文摘要
常规逻辑可以被视为常规类别的内部语言，但是逻辑本身通常没有给予分类。在本文中，我们了解一组T的免费常规类别FRG（t）的规则逻辑规则。从这个角度来看，常规理论是从适当的2类上下文（FRG（t）中的2类关系）中的某些单型2函数 - for posets。此类函子分配给每个上下文中的公式集，并按需要命令。我们将这样的2个函数称为常规的微积分，因为它自然会引起Joyal and Street精神的图形弦图演算。我们将证明每个自然类别都有相关的常规演算，相反，每个常规的演算都可以构建常规类别。
Regular logic can be regarded as the internal language of regular categories, but the logic itself is generally not given a categorical treatment. In this paper, we understand the syntax and proof rules of regular logic in terms of the free regular category FRg(T) on a set T. From this point of view, regular theories are certain monoidal 2-functors from a suitable 2-category of contexts -- the 2-category of relations in FRg(T) -- to that of posets. Such functors assign to each context the set of formulas in that context, ordered by entailment. We refer to such a 2-functor as a regular calculus because it naturally gives rise to a graphical string diagram calculus in the spirit of Joyal and Street. We shall show that every natural category has an associated regular calculus, and conversely from every regular calculus one can construct a regular category.
