图形符号基础：超图和双图在计算系统中的应用

346理论计算机科学电子笔记45（2001）网址：http://www.elsevier.nl/locate/entcs/volume45.html12页计算图的代数基础John Power1，3 and Konstantinos Tourlas2，4爱丁堡大学信息学系Edinburgh EH93JZ英国摘要我们开发了一些基于图形的结构的代数基础，这些结构是用于计算系统的规范、建模和编程的各种流行图形符号的基础 以超图和双图为例，定义了局部序范畴C中图的局部序范畴Graph（C），并赋予其对称monoidal闭结构. 另外两个operation- erations上higraphs和变种，选择相关的计算应用程序，概括在这种设置。1介绍近年来，在计算系统的规范、建模和编程中，图形符号迅速、持续地普及。其中最值得注意的是Statecharts [4]，一种用于对反应式系统建模的符号，以及统一建模语言（UML）[10]，一系列用于基于对象建模的图形符号。不可避免的是，在这种复杂的图的基础上是一些图的概念，根据特定于应用的需求，在其上添加标签和其他语言或视觉注释（参见例如[10，9，3]的各种示例）。除了普通图之外，这里研究的两个主要例子是超图和双图[5]。后者是许多复杂的图解形式主义的基础，其中最突出的是国家图表，1这项工作是在EPSRC赠款GR/M56333和英国文化委员会赠款以及STA日本COE预算的支持下完成的2感谢支持EPSRC赠款GR/N12480和STA日本的COE预算3 电子邮件地址：ajp@dcs.ed.ac.uk4电子邮件：kxt@dcs.ed.ac.uk2000年1月，出版社dbyElsevierScienceB。 V. 在CCBY-NC-ND许可下开放访问。鲍威尔和图尔拉347UML图，以及用于编程反应式系统的特定领域语言Argos [8]。通过大大减少指定转换关系所需的边的数量，Higraphs允许非常简洁，经济地表示复杂的状态转换系统，例如那些潜在的现实反应系统。这是通过用具有相同目标的单个转换替换具有例如共同目标状态的多个转换来实现的，但是源是包含原始转换的所有源状态的新的“超状态”。由此产生的复杂性的减少是n2的顺序，其中n是状态的数量我们开始我们的分析，观察到图，超图和higraphs都是相同结构的实例，即一个图在一个类别C，与C分别是集，Rel和偏序集。也考虑了其他变体在论文草稿[13]中，对higraphs的情况进行了广泛而具体的动机和研究。后者只假定读者具有范畴论的基本知识，以便广大读者能够理解对科学和实践有直接兴趣的计算机科学家 在UML和Statecharts中的应用。在本文中，第2节介绍了我们的主要例子，随后在第2.4节中定义了局部序范畴C中的图的范畴Graph（C）。底层Statecharts是一个二元运算，它给出StatechartsS并且SJ产生对应于S和SJ操作的语义的第三个同时。我们展示了如何同样适用于higraphs和超图。在这里，我们通过在图（C）上定义一个对称的monoidal封闭结构，用代数术语精确而一致地表达这一点我们在第3节中这样做。进一步证明了当Cat（C）范畴具有Cat上的“另一个”对称monoidal闭结构的推广时，存在连接图（C）和Cat（C）的对称monoidal闭附接在实际应用中，利用higraphs中边的层次来产生复杂反应系统的简洁规范。为了理解高级边的含义，我们在第4节中介绍了一种双图的完成操作。这被证明是图（C）包含到图opl（C）中的右伴随的实例，后者具有oplax自然变换作为箭头。证明了一个定理，说明了这种右伴随存在的条件为了支持用户使用代表复杂系统的大型分层结构图，需要有效的机制来重新组织，抽象和过滤图中的信息[9]。这里研究的主要例子是对higraphs的滤波操作，由Harel在[5]中以缩小的名义引入和激发。我们在第5节中展示了它如何推广到非平凡局部有序范畴中的图。鲍威尔和图尔拉348−→−→EBCDF一Fig. 1.一个简单的超图图二、一个简单的higraph2主要例子和主要定义我们首先回顾一下（有向多）图的标准定义，它由一个顶点集V，一个边集E和两个函数s，t组成：V给出每个边缘的源和目标。也就是说，图是范畴Set中的一对平行箭头s，t：E−→V。2.1超图超图是图的一种推广，其中每条边都可以有一组顶点作为其源和目标。这种有向超图的典型图形表示如图1所示因此，超图由顶点集V、边集E和两个函数s，t组成：E2V给出源和目标。 等式，s和t可以被看作是从E到V的关系，从而得出以下结果：定义2.1超图是（小）集合和关系范畴Rel中的一对平行映射。2.2希格斯特Higraph是Harel[5]创造的一个术语，是层次图的缩写，但通常用于包括几个变体。所有变体共同的higraphs的定义性特征被称为深度，这意味着节点可以包含在其他节点中。图2示出了由六个节点和四条边组成的higraph的标准图形表示，其中标记为B、C和D的它因此是常见的，我们将在下文中遵循惯例，将higraphblob的节点称为它们的图形表示的指示，鲍威尔和图尔拉349≤−→··平面上的凸轮廓更多细节请参考[13]。通过要求blob集合上的偏序集结构来捕获blob上的包含关系。这里发展的higraph的概念扩展了这一点。对边缘集的要求：定义2.2双图是范畴偏序集中的一对平行的箭头s，t：E B.在实践中，一个双图通常是一个图（B，E，s，t）和一个偏序B在B。 在这种情况下，E上的偏序集结构可以被认为是离散的。然而，E上的其他顺序的选择通常是有用的，例如，用于对Statecharts中采用的冲突解决方案[6]进行编码。 在大多数higraphs的应用中，特别是Statecharts，直观的un.对边e的理解是暗示存在从包含在s（e）中的所有斑点到包含在t（e）中的所有斑点的边缘一般来说，多个边隐含在一个单独的、显式显示的高层边中。在Statecharts中，该设备用于表示中断转换，从而大大减少了指定所表示的转换系统的状态之间的转换关系所需的边缘数量。2.3组合和变体为了处理真实的图，人们可能还希望结合不同图概念中的特征，例如，允许higraphs中的边具有多个源和目标，这在一些状态图中确实是允许的。由此产生的图的概念，简单higraphs（如上定义）和超图的组合，可以通过考虑偏序集的范畴和它们的基础集之间的具有所有二元sup（和sup保持单调映射）的偏序集范畴BSup给出了Statecharts中更好的深度模型。也可以考虑具有ω-完全偏序的范畴ω-Cpo2.4局部序范畴我们关于“图的概念”的每一个主要例子都是按照一个适当的范畴C中的一对平行映射来描述的我们的例子中另一个不太明显的共同点是，C是一个局部有序范畴，也就是说，一个在偏序集的carnival闭范畴偏序集中得到丰富的范畴，这一事实将在后面得到大量的应用。(The范畴集在平凡意义上是局部有序的：每个hom-object是离散偏序集。从我们的情况可以概括为：定义2.3设C是局部有序范畴。设Graph（C）表示C中图的局部序范畴，即函子范畴[→，C]当recategory·→·同时存在两个对象和两个非同一性对象时，示出了→✷鲍威尔和图尔拉350BCFKHEGeBFKJ FGHECGe一个D图3.第三章。简单的状态图jfg=图四、图1的状态图的基础操作3因此，Graph（C）的一个对象由C的一对对象E和V，以及C中的一对映射s，t：E−→V组成。图（C）中从（E，V，s，t：E−→V）到（EJ，VJ，sJ，tJ：EJ−→VJ）的箭头由映射fE：E−→EJ和fV：V−→VJ使得fVs=sJfE和fVt=tJfE。的图（C）的局部序由C的局部序生成，即，（fE，fV）≤（gE，gV）如果fE≤gE和fV≤gV。3图（C）的一个对称幺半群闭结构我们现在继续研究图（C）上的一些额外结构，对于行为良好的C。我们的动机来自于在Statecharts中应用higraphs。由于涉及大量的状态，直接用过渡系统来描述复杂的反应系统变得不切实际。Statecharts通过允许直接根据可识别的并发子系统对反应系统进行建模来处理这个问题：例3.1考虑图3中的状态图，它表示两个子系统A和D同时运行。假设并发的交错模型，就像Statecharts的情况一样，这张图片的含义被操作精确地捕获，其中所产生的转换系统正是完整系统的预期行为。✷我们在本节中的结果的结果是，上述操作， 在[5]中被称为B、EKHeB、FG地下bFJJ FFC、FGC、GeKC、EHJ鲍威尔和图尔拉351⊗× ××⊗顺利地到higraphs。这是确定支持Statecharts语义的精确数学结构的重要步骤。因为，更一般地，图3中的子系统A和D的规范通常具有higraph结构。因此，对于我们的下一个主要结果，我们观察到，推广例3.1中C=Set的情况，这里不需要C上的局部序结构，我们有定理3.2对任意具有有限余积的Carnival闭范畴C，范畴Graph（C）具有如下对称幺半群结构：给定G=（E，V，s，t）和GJ=（EJ，VJ，SJ，TJ），图G GJ有顶点对象V VJ和边对象（EVJ）+（V EJ），源映射和目标映射是明显的。 这种对称的monoidal结构的单位由V = 1给出，E = 0。证据这是一个双函子直接从C中的二元积和余积的性质得出。所需的同构可以很容易地从C上由它的carnoid结构诱导的对称monoidal结构中推导出来，并且所需的相干条件的验证是常规的。✷例3.3在双图上，图3给出了图4中运算的简单推广。 特别地，对于χ j中的每个边b 1 → b 2和χ j中的斑点b j，χ <$χ j包含边<$b1，b j <$→<$b2，bJ<$，并且对于Χ J中的每个边bJ1 → bJ2和χ中的斑点b，包含边<$b，b j 1<$→ <$b，b j 2 <$。包容性由以下公式给出：b1，bJ1 ≤ b2，bJ2ib1≤ b2和bJ1 ≤ bJ2。 在超图的情况下，H <$H J包含一条边{x1，xJ}，.，xn，xJ对于每个边{x1，.，xn} →{y1，.， ym}在H中，顶点xJ在χJ中，并且对于H j中的边也类似。定理3.4对任意具有有限余积和有限极限的Carnival闭范畴C，定理3.2中给出的图（C）上的对称么半群结构是闭的。证据指数对象[GJ，GJJ]的顶点对象是从[V J，V JJ]×[EJ，EJJ]到[EJ，V J]× [EJ，V J]的两个映射的均衡器的域，由π0和π1给出，其中π0，π1是[VJ，V JJ] × [EJ，EJJ]的投影。 [GJ，GJJ]的边的对象是映射s<$π0<$q <$π0J，π0<$q<$π2J和<$[VJ，SJJ]<$π1J，[VJ，TJJ]<$π1J<$的等化环的定义域，它们都具有定义域V × [VJ，EJJ] × V和余域[VJ，VJJ] × [VJ，VJJ]，其中πIJ是V × [VJ，EJJ] × V的三个投影.✷特别要注意的是，图（C）范畴中的指数与定理中定义的张量积是特别自然的。顶点对象表示从G到Gj的所有图同态，边对象表示图同态之间的所有变换。鲍威尔和图尔拉352−→⊗×−→3.1对称么半群闭附集众所周知，人们可以在任何范畴C中定义具有有限极限的范畴，通常的范畴Cat同构于适当的有限极限草图[1]的集合中的模型范畴Cat（Set）对于C中的范畴的范畴，我们将写Cat（C），隐含地断言C具有所需的有限虽然大家都知道Cat是一个Carnival闭范畴，但很少有人知道Cat[2，12]上还存在另一个对称monoidal闭结构。我们将另一个称为Cat上的另一个对称monoidal闭结构，它可以概述如下：• 指数A−→B由从A到B的函子集合给出，从g到h的态射是箭头α x的赋值：gxhx到A的每个对象x。组成是显而易见的。我们将把A−→B的箭头称为变换。• 张量积可以用一个普适性质来描述：它是全称D，对于A的每个对象x，都有一个函子hx：B−→D和对于B的每个对象y，函子ky：A−→D使得对于每个（x，y）hxy=kyx。张量积的单位是单位范畴。解释一下，A和B的张量积AB具有对象集ObA ObB，并且从（x，y）到（xJ，yJ）的箭头由非恒等箭头的有限序列组成，交替的箭头形成A中的有向路径，其他箭头形成B中的有向路径。组合是由串联，那么A和B的组合所给予的抵消。对称性是显而易见的。除了有有限个极限之外，如果C是余完备的且是Carnival闭的，那么另一个对称的monoidal闭结构扩展到Cat（C），这是一个例行的验证。我们现在可以陈述关于Cat（C）和Graph（C）的定理：定理3.5对于有限极限的余完备范畴C，遗忘函子U：Cat（C）Graph（C）是关于Cat（C）上的另一张量积和Graph（C）上的上述对称monoidal闭结构的对称monoidal闭附函数的一部分.证据 为了证明，考虑C是Set的情况，并简单地将论点内在化。✷请注意，即使在C=Set的情况下，相应的结果也不适用于Cat（C）和Graph（C）的carbohydrate闭结构，因此我们将此结果视为该结构自然性的有力证据最后，在这种情况下，我们观察到定理3.6对于具有有限余积的Carnival闭C，从图（C）到C的遗忘函子是一个对称monoidal闭伴随的一部分，鲍威尔和图尔拉353⟨ ⟨ ⟩⟩ ≤≤××−→图五、完成一个简单的双图，其中添加的边用虚线表示图（C）上的对称幺半群结构的关系。证据对于一个证明，考虑C=Set的情况下的证明，并常规地将其内化为C。✷同 样 ， 即 使 在 C=Set 的 情 况 下 ， 相 应 的 结 果 对 于 图 （ C ） 的carbohydrate闭结构也不成立，它不向Graph的终端对象发送1，因为后者有一条边。4完成操作在理解双图及其变体的语义（例如涉及范畴BSup或ω-Cpo的语义）时，一个有用的构造是明确所有被理解为隐含地存在于双图中的边（回忆一下2.2节末尾的讨论）。这个定义4.1设χ=s，t：E B是一个双图.双图T（χ）称为χ的完备化，它有斑点B和由e，b，bj组成的子集E（B B）的边，使得bBs（e）和bJBt（e）按点序偏序，源和目标由投影给出.✷定义4.2给定一个局部有序范畴C，我们用Graphopl（C）表示局部有序范畴，其对象是C中的图，其箭头是oplax变换，即 对（fE：E −→EJ，fV：V −→ VJ）使得fVs≤ SJFE和fVt≤ TJFE，具有由C的局部序结构诱导的局部序结构. ✷为了陈述我们的定理，使用一点2-范畴理论，特别是一些有限极限是方便的。对这种限制的一个方便的解释是[7]。特别地，我们需要使用映射的oplax极限的概念。所以我们在这里回顾一下。定义4.3给定局部序范畴C中的一个箭头f：X−→Y，鲍威尔和图尔拉35401−→×⟨⟩f的oplax极限由以下形式的图给出：LπoX满足两个性质：id≤f❄ ❄LYπ1• 对于任何其他形式的图表，Kh0Xid≤f❄ ❄KYh1存在唯一的箭头u：K−→L，使得π0u=h0且π1u=h1，且• (the二维属性）的形式Kh0XKJ0XKYh1KYJ1其中h0≤hJ且h1≤HJ，则u ≤UJ。✷定理4.4若局部序范畴C有有限极限，则图（C）到图opl（C）的包含有右伴随。证据给定一个图G =（E，V，s，t），其右伴随的顶点对象由V给出，边对象由映射s，t的oplax极限给出：EV V.证明这个构造产生一个右伴随是2-范畴中的一个例行练习.✷2-范畴理论专家会注意到，我们在C中只使用了饼极限，这在适当的时候可能会变得重要[11]。也许证明中使用的oplax极限的一个更熟悉的表达式是C中从V×V上的恒等映射到映射E−→V×V的逗号对象。如果HHID≤FID≤F❄❄❄❄鲍威尔和图尔拉355H∈−→HH\{|}EBCDF一EF一图六、缩小higraph中的blobC是局部序范畴Poset，则右伴随可以通过放置一条从v到vj的边来显式地描述，如果G中存在从一个大于或等于v的顶点到一个大于或等于vj的顶点的边.这完全符合我们在定义4.1中对T的对偶地，如果C有有限余极限，则图（C）到图opl（C）的包含有左伴随。5缩小我们首先回顾Harel为了捕捉在higraph中选择blob的概念，我们需要以下内容定义5.1一个点双图是由一个普通双图χ = s，t：E−→B和一个特殊的blob组成的，这个blob在偏序集上被表示为一个映射1 −→B，称为点双图。范畴H以点双图为对象，并映射那些保持点的双图。设Hmin为由点是极小的所有对象（点双图）组成的图的全子范畴。blob上的偏序;换句话说，重点是原子团 设I是包含H，min到H的全函子。✷考虑一个具有χ =（s，t：E）的点双图B）和点，说，pB.通过缩小图中的点而获得的点higraphZ（Z）， 由以下数据确定：• 斑点：BJ=BBB P（通过对部分B j的限制排序） B）;• 边：E，源函数和目标函数分别为qs和qt，其中q：B−→BJ是（明显单调的）函数映射eachb/ipnBtoob∈B J和eachb < ptoop∈B J;• 点：p现在有以下几个[13]：命题5.2函数Z扩展为从λ到λ，min的它与包含函子I左伴随。✷这个命题将用下面定理5.5的一个例子来证明. Gener-鲍威尔和图尔拉356−→−→−→在分析我们的主要例子的基本结构时，我们有：定义5.3给定一个局部有序范畴C，用Graph（C）表示这个局部有序范畴，对于这个局部有序范畴，一个对象由C中的一个图（E，V，s，t）和一个映射v组成：1Vin C. 这些地图是成对的地图，严格保持结构。✷定义5.4给定一个局部序范畴C，记为Graph（C）min图（C）的局部序全子范畴，使得点v：1V是偏序集C（1，V）中的极小元。✷定理5.5若C是余完备局部序范畴，则图（C）的包含有左伴随。证据 给定（E，V，s，t）和v：1V，取v与偏序集C（1，V）中所有小于或等于它的元素的联合余均衡器。✷例5.6对于BSup中的图，在存在二元Sup给出的额外结构的情况下，该定理给出了Poset中图的缩小操作的预期推广。然而，缩小并不能推广到Rel中的图，或者偏序集的范畴及其基础集之间的关系，因为终端对象是空集（偏序集）。6进一步工作我们的目标是发展，在一个渐进的和有原则的方式，承担足够的细节，以 模 拟 现 实 的 图 形 符 号 的 结 构 。 目 前 ， 我 们 正 在 努 力 为 一 大 类Statecharts提供这样的模型，其中包括higraphs和hypergraphs中的功能。本文提出的工作奠定了抽象的基础，我们的方法，其中的概念图及其组合可以进行研究。我们工作的另一个方面是研究对这些图概念的扩展，例如，Harel在[5]中简单地介绍了对higraphs的温和扩展，允许边.其基本原理是指出所表示系统中一些尚未指定或故意省略（例如，由于缩小）的部分之间的过渡或关系。 有关动机和细节，请参考读者至[13]。最后，我们指出，这种具有“松散边”的图EBF一鲍威尔和图尔拉357有有限的（饼）共极限，因此允许用箭头偏序集定义张量。引用[1] M. Barr和C.井计算科学的范畴理论。Prentice-Hall，1990年。[2] F. Foltz，C.M. Kelly和C.巢穴具有很少的么半群双闭结构或没有的代数范畴。Journal of Pure and Applied Algebra，17：171-177，1980.[3] 科林·古尔和康斯坦丁诺斯·图拉斯软件工程图的原则性设计。第22届国际软件工程会议论文集，第509-520页。ACM，IEEE计算机协会，ACM出版社，2000年。[4] 大 卫 · 哈 雷 尔 。 Statecharts ： AVisualApproachtoComplexSystems.Science of Computer Programming，8（3）：231[5] 大卫·哈雷尔。关于视觉形式主义。Communications of the ACM，31（5）：514[6] 大卫·哈雷尔和阿姆农·纳马德。Statecharts的STATEMATE语义ACM软件工程方法学汇刊，5（4），1996年10月[7] 通用汽车凯利关于2-范畴极限的初步观察。布尔澳大利亚数学学会第301-317页[8] F. 马拉宁奇 Argos语言：自动机的图形表示和反应系统的描述。IEEE视觉语言研讨会论文集，1991年。[9] 邦妮·M纳迪编程的一个小问题：终端用户计算的观点。MIT Press，1993.[10] 罗伯·普利和珀迪塔·史蒂文斯使用UML。艾迪森·韦斯利1999年[11] A.J.鲍尔和E.P.罗宾逊饼极限的一个特征剑桥哲学会数学学报，110：33[12] 约 翰 · 鲍 尔 和 埃 德 蒙 · 罗 宾 逊 Premonoidal 范 畴 和 计 算 概 念 MathematicalStructures in Comp. Science，11，1993.[13] 约翰·鲍尔和康斯坦丁诺斯·图尔拉斯。图的代数基础。2001年3月提交出版