Symmetric monoidal and cartesian double categories as a semantic framework for tile logic
Symmetric monoidal and cartesian double categories as a semantic framework for tile logic
复制标题
对称幺半群和笛卡尔双范畴作为瓦片逻辑的语义框架
DOI：
--
复制
发表时间：
2002
影响因子：
0.5
通讯作者：
U. Montanari
中科院分区：
文献类型：
--
作者：
R. Bruni;J. Meseguer;U. Montanari
瓦片系统提供了一个通用的模式，并发系统的模块化描述的基础上，一组重写规则的副作用。Monoidal double categories是瓦片系统的自然语义框架，因为描述系统状态和同步动作的数学结构（在我们的术语中分别称为配置和观测）是具有相同对象（系统的接口）的monoidal categories。特别是，配置和观察的基础上，净过程和长期结构通常被描述在对称monoidal和carnival类别，其中的辅助结构的接口的重排对应于适当的自然变换。本文讨论了这些辅助结构到双范畴的提升。我们注意到，双范畴的内部构造产生了一种病态的自然变换的不对称概念，这种概念只在一维中得到充分利用（例如，对于构型或对于观察，但不是对于两者）。在Ehresmann（1963）之后，我们克服了这个有偏见的定义，引入了四个双函子（而不是两个）之间的广义自然变换的概念。因此，对称么半群和卡列（具有一致选择的乘积）双范畴的概念以一种自然的方式从相应的普通版本中产生，在构形和观测的辅助结构之间给出了非常好的关系。此外，凯利-麦克-莱恩凝聚公理可以毫不费力地提升到我们的设置，这要归功于两个合适的对角范畴的特征化，它们总是存在于一个双重范畴中。然后，对称monoidal和carnival双范畴的过程和长期瓷砖系统提供了足够的语义设置。
Tile systems offer a general paradigm for modular descriptions of concurrent systems, based on a set of rewriting rules with side-effects. Monoidal double categories are a natural semantic framework for tile systems, because the mathematical structures describing system states and synchronizing actions (called configurations and observations, respectively, in our terminology) are monoidal categories having the same objects (the interfaces of the system). In particular, configurations and observations based on net-process-like and term structures are usually described in terms of symmetric monoidal and cartesian categories, where the auxiliary structures for the rearrangement of interfaces correspond to suitable natural transformations. In this paper we discuss the lifting of these auxiliary structures to double categories. We notice that the internal construction of double categories produces a pathological asymmetric notion of natural transformation, which is fully exploited in one dimension only (for example, for configurations or for observations, but not for both). Following Ehresmann (1963), we overcome this biased definition, introducing the notion of generalized natural transformation between four double functors (rather than two). As a consequence, the concepts of symmetric monoidal and cartesian (with consistently chosen products) double categories arise in a natural way from the corresponding ordinary versions, giving a very good relationship between the auxiliary structures of configurations and observations. Moreover, the Kelly–Mac Lane coherence axioms can be lifted to our setting without effort, thanks to the characterization of two suitable diagonal categories that are always present in a double category. Then, symmetric monoidal and cartesian double categories are shown to offer an adequate semantic setting for process and term tile systems.