可在www.sciencedirect.com在线获取理论计算机科学电子笔记319（2015）51-66www.elsevier.com/locate/entcs具体范畴中的开映射与前缀序的H. Beohar1，2德国杜伊斯堡-埃森大学理论计算机科学组P.J.L. Cuijpers3部数学和计算机科学技术大学埃因霍温，荷兰摘要开放映射，如Joyal，Nielsen和Winskel在并发理论中所介绍的，提供了一种抽象的方式，在各种各样的计算模型中定义函数互模拟（如标记转换系统，事件结构等）。此外，开映射的跨度的存在性刻画了在与这些计算模型相关的文献中发现的互模拟的众所周知的关系定义。然而，在我们的前缀序的工作范畴中（其中对象表示由任意动力系统生成的执行），开映射不会立即导致函数互模拟，并且开映射跨度的存在不会导致等价。这是相当令人惊讶的，因为prefix命令仅仅是（离散）执行树的概括，已知MAP方法是有效的。在仔细研究了开映射的定义之后，我们在本文中表明，这个问题可以通过将前缀序视为一个具体的范畴并从这个角度重新解释开映射的定义来解决。作为奖励，选择一个路径类别，开放映射的依赖成为一个自然的依赖，即嵌入的子范畴。虽然存在的跨度仍然不会导致等价，它表明，存在的cospans。 事实上，我们提出了一个表征的概念分支互模拟的范Glabbeek和Weijland，据我们所知，没有研究的框架中的开放地图关键词：开放映射，前缀序，分支互模拟，具体范畴。1介绍自从van Glabbeek1感谢PaulTaylor提供了他的宏，以便在LATEX中整洁地绘制一个WCOM U V E图。2电子邮件：harshbeohar@gmail.com3电子邮件：p.j.l. tue.nlhttp://dx.doi.org/10.1016/j.entcs.2015.12.0051571-0661/© 2015作者。出版社：Elsevier B.V.这是一篇基于CC BY-NC-ND许可证的开放获取文章（http://creativecommons.org/licenses/by-nc-nd/4.0/）。52H. Beohar，P.J.L.Cuijpers/Electronic Notes in Theoretical Computer Science 319（2015）51ˆˆOM一被认为在行为上等同（导致众所周知的van Glabbeek光谱）。在他们的开创性论文[14]中，Joyal，Nielsen和Winskel使用范畴论的语言提出了强互模拟的抽象定义，从而开始了在统一框架中捕获行为等价的方法。特别地，通过开映射的跨度（cospans）的双相似性被定义为两个对象之间的开映射的跨度（cospan）的存在，其中，对于子范畴P（表示为 p+）中的n y映射p，映射s和m使得外方交换（即，s·p= k·m），Bs）Dp+）CM在M中存在使两个内部三角形可交换的映射k（由虚线箭头强调的存在）（即，k·p=m和o·k=s）。这些箭头符号将在后面讨论开放性的具体范畴变体时以一种明显的方式被重载将M作为标记迁移系统的范畴，它们之间具有迁移保持映射，P作为路径扩展的范畴（包含迁移链之间的所有迁移保持映射）Joyal等人表明，通过开放映射的跨度的双相似性与并发理论中熟悉的强互模拟概念一致[15]。随后，通过开放映射的跨度或余跨度的双相似性已经被证明与许多替代行为模型中的双模拟的有用概念一致[3、9、11、12]）。尽管开放地图框架[13]具有普遍性，但它有两个局限性。首先，对于vanGlabbeek谱中的弱等价，还没有统一的处理方法（见[17]）。大多数关于弱等价的工作都涉及弱互模拟的概念（例如，[3，9]），并且似乎依赖于首先饱和（合并）所研究的过渡系统的所谓不可见步骤，然后在饱和版本上实例化强双相似性。正如从[19]中众所周知的那样，这种不可见步骤的饱和方法对于分支互模拟等价来说是不合理的;因此，[3，9]中开发的技术在表征分支互模拟等价方面不足。其次，为了通过开映射的跨度的双相似性导致等价，范畴M必须有拉回，这可能是一个难以获得的条件（参见[7，16]）。令人惊讶的是，在我们自己关于将行为系统描述为prefix有序执行集的研究中，分支互模拟的定义通过不同的路径自然产生，但即使对于强互模拟，我们也很难应用[14确切地说，没有合适的路径子范畴的选择，使得开映射将导致通常的功能互模拟概念（参见。[14，命题1]）。H. Beohar，P.J.L.Cuijpers/Electronic Notes in Theoretical Computer Science 319（2015）5153||）在我们试图纠正这一点的过程中，我们发现，在具体类别的背景下重新解释上述图表会带来许多新的见解。首先，它允许我们在以偏序为基范畴的prefix序的具体范畴中定义函数互模拟。其次，路径子范畴P的自然选择原来是嵌入的子范畴。第三，这些嵌入开映射的余跨距的存在性与分支互模拟一致，当前缀序是由一个标记的过渡系统。 最后，重新解释伴随着语法和语义的解释，我们认为具体（基本）范畴中的态射是实现（观察）。我们在本文中采取的重新评估现有分类概念的方法并不罕见。例如，在许多范畴中，单态概念是捕捉“子对象”概念的有效方法，但在具体范畴中，往往倾向于“嵌入”（一种特殊的单态）概念。类似地，我们希望我们对开放映射概念的修改将导致一个更广泛适用的“重新检查扩展”概念我们获得嵌入作为路径扩展子范畴的自然选择的事实暗示了这可能确实是这样。在下一节中，我们将在具体范畴的上下文中重新引入开映射的概念。我们再次强调的事实是，通过拉回或推出的开放地图的保存是足够的，以保证通过跨度或cospans，分别是一个等价的，我们表明，在有“足够”的开放地图的情况下，有一个开放地图的替代特性，可能会可悲的是，尽管有一些困难，我们没有找到一个很好的分类特征，在这个特征下，拉回和推出保持开放的地图，所以这仍然需要为每个类别单独证明。特别是，[14]的结果，即回调的存在表面上保证等价性，并不直接延续到具体的设置在第4节中，我们回顾了[4，5，8]中的prefix序范畴，并证明了嵌入-开映射是函数互模拟，并且推出保持了该范畴中的开映射，因此通过cospans的互模拟是等价的。最后，在第5节中，我们证明了如果前缀顺序的执行是由标记的迁移系统生成的，则第六部分是结论和对未来的建议。2在具体类别让我们从[14]中的开映射概念在具体范畴[1]的背景下进行调整开始。为此，我们首先回顾以下基本定义。定义2.1范畴P是M的一个子范畴，如果M的每一个态射或对象P分别是M的一个态射或一个对象。 范畴M是基上的具体范畴范畴S，如果存在忠实函子M.=== S，即，对于任意两个态射f，g：A → B，我们发现，|F|为|G|表示f= g。54H. Beohar，P.J.L.Cuijpers/Electronic Notes in Theoretical Computer Science 319（2015）51||）===一∪S和M的子范畴P，称M的映射O为P-开的（记为MM本文利用一个具有忠实函子M的.====S我倾向于把M的对象看作具体的行为模型，把S的对象看作行为的语义模型。 M的态射Af）B表示将B的行为（规范）实现为行为A（实现）的一种方式。 在语义层面上，g）D描述了C的行为可以作为D的行为的一部分被观察到。此外，在[14]中，M的子范畴P的对象表示需要保持的路径扩展的集合，但在本文中，我们仅将它们视为通过实现的任意行为扩展。我们强调扩展是具体的模型，直观地说，我们只对保留可以描述为M的对象的行为感兴趣，而不一定对可能发生在S中的所有语义行为感兴趣。非正式地说，一个P-o-pen映射X（？）O（？）Y是指，如果一个由X的一个顶点提供的节点具有感兴趣的具体扩展（即，从P），那么这个扩展也可以在X中观察到因此，简而言之，O反映了P的所有具体扩张。|S |s ）的方式|D|ˆ|+的|+|）|)ˆ|o||C|(a) 一个从M出发的映射O是P-开的，如果对于每个从P出发的扩张P，并且映射m，s从S出发，其中s·|p|为|O|·m，则存在一个来自S的映射k，使得图可交换。A BC(b) 如果两个来自M的对象A和B之间存在一个来自M的P-开映射的跨距，则它们通过跨距是P-双相似的。A BC(c) 如果两个来自M的对象A和B之间存在一个来自M的P-开映射的余跨度，则它们通过余跨度是P-双相似的。图1.一、通过开映射的跨度和上跨度的互模拟的具体定义定义2.2[Open map]给定一个具有忠实函子的具体范畴|. |)◦ ））如果对于每一个p从P和映射m，s从S，则s·|p|为|O|·m（即图1a中的外正方形在S中交换），存在来自S的映射k，使得这 是K|p|=m并且|O|·k=s（即图1a中的内部三角形也是互换的）。来自M的两个对象A和B通过跨距是P-双相似的，记为APs B，如果它们之间存在一个P -映射的区间，即. 如果存在H. Beohar，P.J.L.Cuijpers/Electronic Notes in Theoretical Computer Science 319（2015）5155一||）||）在M和P中的对象C-对象映射C（f））A和C（g））B，如图1b所示。它们是P-双相似的，记作APc B，如果它们之间存在P-开映射的余跨度，即.如果在M和P中存在对象C-图1c中的开映射A（f）C和B（g）C，as。显然，当M=S且忠实函子是单位元时，我们的具体定义与[14]中的定义一致。这意味着我们定义中唯一的“新”部分是具体地图和底图的使用之间的区别。就像在[14]中，开映射形成M的一个子范畴。定理2.3给定一个具有忠实函子M的具体范畴.=== S和子-categoryPofM，则M中的每个单位元都是P-open，并且如果Ap）p）B和Bq）q）C是P-开映射，则它们的合成q·p也是P-开映射。此外，如果回撤（推出）保持开放映射，则通过跨度的互模拟（cospans）是等价的，这很容易从图追踪中得出。定义2.4Gi v ena nycategoryMandacosspanXf）Z（ gY， aspann X（hPk）如果f·h=g·k且f或一个y跨度X（h′），则Y是一个pul_backQk′）Y，其中f·HJ=g·kj，存在唯一映射Qu）P满足h·u=HJ和g·u=GJ. 通常，给定跨度X（fZg）Y，cosspanXh）P（kY是如果h·f=k·g，则存在推出，并且对于任意y跨度Xh）′Q（k′Y，其中hJ·f=kJ·g，存在唯一映射P（u）Q，使u·h=HJ，u·g=GJ.定理2.5（通过跨距或余跨距的互模拟等价）具有忠实函子M的具体范畴.=S，通过跨度的互模拟是一个等价的条件是，任意映射X（（h）P（k））Z（（g）Y）都有一个由映射X（（h）P（k））Y组成的脉冲组。 其次，如果开映射的每个跨距都有开映射的一个推出，则通过cos p ans的互模拟是等价的。Joyal等人表明，在所有cospans都有回调的类别中，所有开放cospans也都有开放回调[14]。因此，在最初的定义中，通过跨度的双相似性在所有具有拉回的范畴中是等价的。然而，推出的存在并不足以保证通过cospans的双相似性是等价的。在我们对具体范畴的新解释中，这个结果不那么容易重复。我们已经发现了一些条件下，通过跨度的双相似性是一个等价的，但它们涉及到存在的基础范畴的收缩，并不是很此外，我们的工作范畴选择，prefix秩序与偏序作为一个基本范畴，不满足这些性质。因此，我们将这些结果排除在当前演示文稿之外事实上，在第4节中，我们证明了通过跨度的双相似性根本不是等价的，即使回调确实存在于这个范畴中。另一方面，通过cospans的双相似性确实是等价的，尽管我们还没有一个完整的范畴论证明。56H. Beohar，P.J.L.Cuijpers/Electronic Notes in Theoretical Computer Science 319（2015）51一一P||）=S和M的子范畴P，3作为路径扩展的在具体范畴中，“外延”的自然概念事实证明，嵌入的子范畴是范畴P的自然选择。|. |f定义3.1G iv enaconcretecategoryM=）S，amapA+）BfromMis一个嵌入，而B被称为A的扩展，如果：• （基础monos）对于S的所有映射g，h，|F|·g = |F|·h我们发现g = h;• （初始）f或S的nyg和M的h，其中|H|为|F|·g，存在M的g∈M，|g|=g.我们将通过跨度的嵌入双相似性简单地用s表示，通过cospans的嵌入双相似性用c表示。在[1]中，嵌入也被称为扩张，这导致我们研究使用嵌入作为路径扩张的子范畴但当我们发现P-开映射的定义与[1]中定义的P-内射对象的定义之间的相似性时，我们确信我们走上了正确的道路特别是，一个对象是绝对收缩的当且仅当它是具有足够内射对象的任何范畴中的内射对象（原始定义见[1]中的命题9.10），这一观察结果也被证明是对开映射设置的一个很好的翻译。下面的定义和定理是[1]中定义和定理的直接修改， 证明是完全类似的。Xf）Z|F ||Y|) |Y|∩ˆ|+ R|+ rY(a) 当每一个映射都可以被分割成一个扩展和一个P-开映射时，就有足够的-开映射.v|Z|(b) 一个映射有绝对可收缩性，如果它的源的每个扩张都有一个基收缩。图二、如果有足够多的开放地图，那么开放地图就是绝对的可伸缩地图。定义3.2给定一个具体范畴M.=S和M的子范畴P，我们说M有足够的P-开映射，如果对每个映射Xf）Z，存在一个po从P出发的扩张X_p~+）Y和P-p_en映射Y_p~+）Z使得o·p=f.定义3.3给定一个具体范畴MF|. |)p一个映射X）Y具有绝对P-可收缩性，如果对任意扩张X<$+）Z且映射|Z|g）的|Y|关于S与g·|p|为|F|，这是一个很好的方法，|Z|（ r）|X|的S，使得r·|p|=id和|F|·r= g。H. Beohar，P.J.L.Cuijpers/Electronic Notes in Theoretical Computer Science 319（2015）5157||）f）G||）|（f））|f))||）g）S定理3.4在具体范畴M中.=== S和M的子范畴P，如果M有如果有足够的P-开映射，则映射X（f）Y是P-开的，且它是绝对P-可收缩的。用具体范畴的观点来解释这个定理，具体态射表示实现，基态射表示观察，特别是考虑P作为嵌入的子范畴，我们看到，在一个有足够开映射的范畴中，映射Af）B是开的当且仅当A的行为的每个在B内可观察的扩展在A内已经可观察。换句话说，A的行为是B中所有可观察行为的完整表示。关于开映射的具体定义的另一个很好的结果是，所有的开映射都是满态的，假设忠实函子保持满态和范畴的初始对象事实上，所有打开的映射都是基本类别中的收缩。定义3.5给定一个范畴M，一个映射e是一个满射（记为，如果对于任何映射对B）C有f·e=g·e，我们发现f= g。（e））定义3.6给定一个范畴M，一个对象0称为初始的，如果对于任何对象X有一个独特的地图0）X. 具有忠实函子M的一个具体范畴保持M的初始对象，如果|0|也是S的首字母。.=S定义3.7给定一个具体范畴M.=Sa map X Y inMis a如果存在映射，则进行baseret rac t |Y|f←）|X|在S中，|F|·f←=id。定理3.8（嵌入开映射是基收缩）给定一个具体的M类.=S，如果M有一个初始对象0，并且忠实函子保持它，则每个嵌入开映射都是基收缩和满射。是的。 对于地图X，f）Y考虑|0|n）的|X|，m =id，并且|0|（p）|Y|.思恩策|0|是初始的，它除了同构之外没有传入流，因此p是一个e mbedding。 这给了我们一张地图|Y|（k）|X|这使得图1a中 的 图 是 可交换的，因此k是f在S中的基收缩，并且因为任何收缩是满射，f是满射，.最后，对于任何Y）Z与Hg·f = h·f我们发现|G|·|F|为|g·f|为|h·f|为|H|·|F|，所以|H|为|G|以信为本，|.| we have h = g.所以f是一个满射。Q4预定订单在[4，5]中，我们认为任何动态系统，无论是离散的，连续的还是混合的，都可以被认为是一组在其自然前缀排序下的执行，并且我们展示了诸如精化，互模拟和异步乘积等概念如何自然地出现作为历史保留映射，历史和未来保留的58H. Beohar，P.J.L.Cuijpers/Electronic Notes in Theoretical Computer Science 319（2015）51地图，以及保历史地图上的范畴积。由于这些结果，我们决定选择历史保持映射作为这个范畴的态射的自然概念定义4.1偏序<$U，≤ <$U是一个集合U，它具有一个自反、传递和反对称的关系≤ <$U× U。prefix order是满足以下条件的偏序：• 向下求和：<$x，y，z∈U（x≤z <$y≤z）<$$>（x≤y <$y≤ x）.两个偏序之间的函数f：U→V是保序的，如果对所有x≤y我们发现f（x）≤f（y），我们用Pos表示它们之间具有保序映射的偏序范畴。此外，我们写x−={y |y ≤ x}，对于点x ∈ U的下闭包或历史，以偏序或前缀序，记为f（A）={f（a）|a∈A}将函数提升为集合。然后，在前缀阶U，V之间的函数f：U→V被称为：•如果f（x）−=f（x−），则f（x）是历史保持的我们写Pfx为prefix序和它们之间的历史保持函数的范畴。为了在不使用范畴论的情况下定义前缀阶上的函数互模拟，我们明确地研究了路径及其延拓定义4.2一个子集PU是一条具有预定序U的路• P是链，即，x，y∈Px≤y <$y ≤x，并且• P是prefix封闭的，即，<$x∈Px− <$P此外，如果满足以下条件，则前缀阶之间的映射f：U→ V是函数互模拟：• f是历史保存，• 对任意路径P<$U和v∈V，f（P）<$v−，存在u∈U，P<$u−且f（u）=v。请注意，在transfinite执行的情况下，这个定义也与Zeno点和其他极限行为有关，将[6]的解决方案推广到一个在时间和混合系统[18，10]研究中广泛存在的问题。还要注意的是，这个定义与[ 5 ]中的定义略有不同，在[5]中，Zeno选择尚未被明确考虑。然而，对于更常见的计算模型的执行，例如标记的转换系统，它们是一致的。Pfx中的反例互模拟在对前缀序进行分类处理时，人们所关心的一个问题是，函数互模拟（目前）还不能仅仅用保留历史的映射来描述。 原因是对角线k在 图1a中存在，但是仅仅是顺序保持而不是历史保持。一个简单的例子是图3所示的映射o：{0， 1， 2} → { 0， 1}。根据上面的定义，这是一个功能互模拟，但也根据大多数H. Beohar，P.J.L.Cuijpers/Electronic Notes in Theoretical Computer Science 319（2015）5159===其他定义的功能互模拟已提出的文献。它也是历史保持的，因此是Pfx中的态射，取B ={ 0， 1}和A ={ 0}给我们一个历史保持映射的交换平方。然而，对于这个正方形来说，不存在保持历史的对角线k。在这种情况下，确实存在一个保序k的事实使我们研究了具体范畴论方法的可能性。2.....）的。. 1ˆ ˆ1ˆ0.......................）的。. 0图3.第三章。一个没有历史保持对角线k的历史保持函数互模拟o。通过span的反例等价性：第二个问题是，使用函数互模拟的跨度来定义前缀顺序之间的互模拟关系不会导致等价性。 在[5]中已经提到了一个例子，基于所有序数直到（但不包括）第一个不可数序数的集合−Ω，以相反的方向排序，以及所有自然数的集合−N以相反的方向排序。映射−N）1和−Ω）1都是函数互模拟，因此证明−N与1互相似，−Ω与1互相似（证明跨度是这些映射和恒等式）。然而，这两个映射的拉回，被认为是−Ω和−N的双相似性的证明，结果是空集。 没有其他的前缀序可能有到两个集合的保序满射，仅仅是因为从−Ω到−N没有保序满射。事实上，回调确实存在，但地图（Ω）-Ω和n）−N肯定不是泛函互模拟（它们甚至不是满射）。我们的结论是−N和−Ω之间的泛函互模拟的跨度不存在，因此它们通过跨度不是互相似的。在上一节中，我们已经为通过cospans分类定义互模拟铺平了道路。剩下要说明的是，嵌入开放映射确实给出了我们想要的互模拟概念。为了做到这一点，我们认为前缀序是偏序范畴上的一个具体范畴在下面的定理中，我们整理了一个与范畴Pfx和Pos有关的有趣事实的列表。每一项的证明都是标准的或平凡的。定理4.3（i）每个历史保持函数都是保序的，因此|. |)恒等函子Pfx=Pos，映射每个前缀顺序和历史保持映射自身是一个忠实的函子。(ii) 并发症中的并发症|.）|历史保存功能。正因为如此，才有了注射-(iii) 空集是Pfx和Pos的初始对象。60H. Beohar，P.J.L.Cuijpers/Electronic Notes in Theoretical Computer Science 319（2015）51(iv) 满射历史保持函数正是Pfx，和也是Pos 中的满态。(v) 所有的推出和回撤都存在于Pfx类别中。|.）|接下来，我们证明Pfx=中的开映射互模拟定理4.4映射o：U →VPOS正是功能性的|.）|在具体范畴Pfx=嵌入开放当且仅当它是函数互模拟。Pos是证据每一个开映射都是一个函数互模拟，这一点很容易证明，通过将函数互模拟定义中的任何路径P作为对象A和P， {v}如图1a中的B。由此产生的映射k将指出u=k（v），k的保序性给出P<$u−和o（u）=v。相反的方向，然而，是不那么平凡的，并需要集理论公理的选择。设o是Pfx的一个映射，使得对任意路径P，任意v∈V，且o（P）<$v−，存在u∈U，且P<$u−，且o（u）=v。然后，不难验证（使用o的顺序保持和≤的向下总体），此外，它还持有：<$v′o（P）<$vJ≤v =<$u′P<$uJ≤u<$o（uJ）= vJ.（*）这里，P≤uJ惠<$u∈Pu≤uJ。现在，考虑图1a的交换平方。我们需要找到一个订单保留函数|B|（k）|U|苏·C·H·K·|p|=m并且|O|·k= s。这是通过在B的prefix闭子集上的归纳来实现的。我们证明了对于p（A）<$B存在这样一个函数。随后我们将证明对于任意子集p（A）<$X<$B，其中X−=X，任意点b∈B，如果存在保序函数k X：X→ U满足k X·p=m，且|O|·k X=s X（其中s X是s的限制，如果b ∈ X，则定义为s X（b）=s（b），否则定义），则存在一个集合p（A）<$X <$Y <$B，其中Y−=Y且b∈Y，对于该集合存在一个类似的函数k Y，并且对于x ∈ X，还存在k X（x）= k Y（x）。这是一个标准的范畴论结果，即这种保序映射的无穷级数的极限再次导致这种保序映射，从而证明了本文的结论是：|B|（k）|U|存在.基本情况Pi ckX=p（A）并定义kX=m·p−1。 注意p−1是一个保序函数，因为p是一个嵌入，通过构造|O|·kX= sX。归纳情形Pick p（A）<$X <$B，其中X−=X，且任意点b∈B，设k X满足kX·p=m，|O|·kX=sX。如果b∈X，我们选择Y=X，w e完成。 因此，设b/∈X，构造路径P=kX（b−<$X）−<$U，以找到o（P）≤s（b）。条件（*）给出一个点u，使得P≤{u}，o（u）= s（b），并且<$b′ o（P）<$s（bJ）≤ s（b）=<$u′ P <$uJ≤ u <$o（uJ）= s（bJ）.注意，对于任何满足上述前提的b j，可能有不止一个uJ满足上述条件，但是应用选择公理我们仍然可以构造一个函数g：b−→u−su ch使得g（b）=u和o（g（bJ））=s（bJ）。作为第二阶段，我们使用quotient构造来构造函数gs：H. Beohar，P.J.L.Cuijpers/Electronic Notes in Theoretical Computer Science 319（2015）5161b−→u−62H. Beohar，P.J.L.Cuijpers/Electronic Notes in Theoretical Computer Science 319（2015）51||）证明了对于任意b，BJ∈B，满足s（b）=s（BJ），则存在gs（b）=gs（BJ），且存在 bj，使得s（b）=s（BJ J），gs（bj）=g（BJ J）。最后，我们可以定义Y=Xb−，并合并kX和gs以找到一个函数kY，使得kY（y）=kX（y）i fy∈X和kY（y） =gs（y）i fPy≤b。 注意，Y是prefix闭的，kY·p=m，|· k Y = s Y通过构造而满足;因此仍然需要证明k Y是保序的。|· k Y= sYsatisfies by construction; so it remains to show k Yis order preserving.为此，选择y，yJ∈Y，其中y≤yJ。 我们区分以下几种情况。• y，YJ∈X：平凡的，因为kX是保序的;• y/∈X和yJ∈X：导致矛盾，因为X=X−;• y∈X和y/∈X：由于y≤yJ，我们发现kY（y）=kX（y）∈P，并通过构造Pg（yJ）=kY（yJ）;• y，yJ/∈ X：则k Y（y），k Y（yJ）≤ k Y（b），并且通过向下的总体，我们有k Y（y）≤ k Y（yJ）（在这种情况下我们完成了）或k Y（yJ）≤k Y（y）。在 后一种情况下，我 们发现s（y） ≤s（ yJ） =o（ k Y（yJ））≤o（k Y（y））=s（y）因此s（y）=s（yJ）因此gs（y）=gs（yJ）因此kY（y）=kY（yJ）。这就证明了o是一个开映射。Q最后，我们已经看到通过跨距的互模拟不会导致等价，以−Ω）1（−N的拉回作为不保持开映射的拉回的例子。为了证明推出保持开映射，我们首先需要回忆一些关于推出构造的概念和定理定义4.5给定一个预定阶U，等价关系为• 序收缩，如果：<$u，v，w，x∈Uu≤v <$v<$w <$w ≤x <$x<$u <$u<$v。定理4.6每个态射f：U → V定义U上的一个阶压缩等价，由u∈uJ惠f（u）= f（uJ）给出。此外，等价类U/u通过定义[u] ± [uJ] iw，w′uw≤wJuJ和投影[. ] n：U）U/n是满射。定理4.7给定两个前缀序Y和Z，它们的余积是基础集合的不交并YZ，前缀序为关系±使得a±b当且仅当a≤b且a，b∈ Y，或a≤b且a，b ∈ Z.定理4.8给定两个历史保维映射X（一）Y和Xg）Z，推出是集合（YZ）/Σ，其中Σ是最小阶收缩等价，使得Σx∈Xf（x）Σg（x），自然投影由[. [.. ] Z →（Y Z）/Z。.定理4.9在具体范畴Pfx==Pospushouts保留打开的映射（因此，通过开映射的余跨度的互模拟是等价的）。是的。 Gi v enw o o p enmapsX）f）Y andX）g）Z，我们知道它们的推出是集合（Y Z）/Σ其中Σ是最小阶收缩等价，使得<$x∈Xf（x）<$g（x）. 看到这张地图[…] [] Y：Y→（Y Z）/Z是开放的（类似地H. Beohar，P.J.L.Cuijpers/Electronic Notes in Theoretical Computer Science 319（2015）5163对于Z），选取P <$Y在Y中的一条路径，对于某个v ∈（YZ）/<$，[ P ]<$v−。 所以存在y ∈Y或z ∈Z，分别满足[y]= v或[z]= v。此外，如果z存在，我们利用g是开的，因此有一个基收缩的事实来找到y= f（g←（z））<$z，因此[y]=v。因为取等价类是保序的，要么P∈y−（在这种情况下我们完成了），要么存在一个p∈P，它与y无关，但[p]≤[y]。通过历史的保存[。我们发现pJ≤y，其中p≠pJ。接下来，我们将通过归纳法来证明，后者会导致一个矛盾。 通过构造，可以通过六种方式获得ppJ• (rep=pJ，但p≤y;矛盾。• （对称性）pJp，在这种情况下，我们发现所有其他参数实际上都是对称的;• （传递性）pJPjp，在这种情况下，我们通过归纳发现yJy，使得pJJ≤yJ，并且通过再次使用归纳法ayJJ<$yJ，其中p≤yJ。矛盾。• (base存在x，xJ使得p=f（x），g（x）=g（xJ），且pJ=f（xJ）.但在这种情况下，我们使用f和g是开映射，因此函数互模拟找到一个点yJy，其中p≤yJ，因此[p]≤[yJ]=[y]。矛盾;• （序压缩）存在q，qJ使得p≤pJ<$q ≤qj<$p。但后来p≤pJ≤y。 矛盾;• （序压缩）存在q，qJ使得pJ≤p <$q ≤qj<$pJ。但是通过归纳法，有一个后继yJJ，其中qJ≤yJJ，通过归纳法，再次有一个yJJJ，其中p≤yJJJ，yJJJ<$yJJ<$y。矛盾。从这一点我们可以得出结论。]是一个函数互模拟，因此是一个开放映射。Q顺便说一句，在我们的具体范畴中有足够的开映射，允许我们使用定理2a来推理双极性。|.）|定理4.10在Pfx = Pos中，有足够的开映射。证据 给定一张地图Xf）如图2a中的Z，简单地从扩展所有路径开始在X中与映射到Z后获得的未来相关联。 这给出了嵌入p到Y，并且由于在将Y映射到Z时没有添加新的行为，因此所得映射o是函数互模拟，因此是开放的。Q5分支互模拟的一个刻画在最后一节中，我们证明了在研究标记迁移系统的执行时，通过前缀阶上的cospans得到的互模拟概念与分支互模拟一致。为了做到这一点，我们考虑标记转移系统上的执行作为片范畴Pfx/A中的对象，i.e.一个范畴，其中对象是从任意前缀序U到字母表A上字符串的固定前缀序A的形式为f：U）A的历史保持映射，并且其中f：U）一个人，g：V）AA是一个保历史映射h：U→ V使得f=g·h.64H. Beohar，P.J.L.Cuijpers/Electronic Notes in Theoretical Computer Science 319（2015）51一ε请注意，在不使用切片类别的情况下，前缀顺序表示系统的完全观察到的执行，但在切片类别中，前缀顺序仅表示映射的结果f：U）A是可观察的。因此，在切片范畴中，系统是作为“分支时间”的函数的观测。定义5.1一个标号转移系统是一个元组P，Aτ，→P，其中P是一组状态，→P×Aτ×P是字母表Aτ上的所谓转移关系，其中τ/∈A表示一个不可见的动作。通常，对于（p，a，q）∈→，我们写p − → aq。定义5.2从状态p开始的运行u是满足以下条件的函数σ − → P（来自某个w阶σ∈A<$τ的历史）：u（ε） =p，u（σJ）−→u（σja），对每一个σJ≤σ.我们将Runs（p）表示为所有从状态p开始运行，排序为：u≤uJ ⇐⇒ dom（u）dom（uJ）<$σ∈dom（u）UJ（σ）= u（σ）. 此外，obsp：σ（p）→Aτ表示观测函数，它简单地忘记了fτ在σ∈Aτ中的发生。 换句话说，看不见的步骤对应于观察没有变化。定理5.3从状态p开始的所有游程的集合，A τ，→ A τ，是一个预定序。此外，观测函数obsp是历史保持函数。定义5.4二元关系RP× P是分支互模拟关系，当且仅当满足以下传递性质(i) 如果pRpJ且p−→aq，则要么a=τ<$qRpJ，要么存在pJJ，qJ∈Psuch，一pJ→pJJ−→qJ，pRpJJ，和qRqJ。(ii) 若pRpJ且pJ−→aq，则要么a=τ<$pRq，要么存在pJJ，qJ∈Psuch，εp→pJJ−→aεqJ，pJJRpJ和qJRq。这里，→表示零个或多个τ步。两个过程p，q∈P是分支双相似的如果存在分支互模拟关系R使得pRq.定理5.5两个过程是分支双相似的，如果它们对应的Prefix阶是通过片范畴Pfx/A中开映射的余跨距双相似的。证据 设P（p），P（q）在片范畴Pfx/A中通过开映射的余跨距是双相似的. 也就是说，存在一个预定序R和嵌入开映射Runs（p）f）R（（g）Runs（q）和一个历史保持函数obs：R→A（g），其中obs p= obs·f，obs q= obs·g. 定义一个关系R P ×P，只要f（u）= g（v），通过关联π（u）R π（v），其中π（u）返回u访问的最后一个状态。很容易验证这个关系确实是一个分支互模拟关系（参见例如，[5]）。假设R是最大的分支互模拟关系，这是众所周知的存在于这种类型的运行之间，并且是一个等价关系（见[19]）。此外，从[2]中，我们知道在约化标号转移系统上存在满射f：P→ Pj，满足：(i) np，q∈P（p−→aq<$a∈A）=<$f（p）−→af（q）.(ii) p，q∈Pp−→τq=<$f（p）=f（q）<$f（p）−→τf（q）。aεJ aJ（iii）f∈P，q<$∈P′f（p）−→q<$=f<$p′，q∈Pp→p−→q<$f（p）=f（p）<$f（q）=q<$.H. Beohar，P.J.L.Cuijpers/Electronic Notes in Theoretical Computer Science 319（2015）5165接下来，可以使用对游程长度的归纳来验证函数f：满足条件（i）和（ii）的P→ Pj诱导出一个保历史函数fp：n（p）→n（R（p））（对任意p∈P），其中R（p）表示p的等价类.此外，条件（iii）保证fp是满射的，并且满足定理4.4的嵌入开映射的特征集合论条件。现在假设q是分支双相似于p。像fp一样，存在一个嵌入开映射fq：<$（q）→<$（R（q））（注：R（p）=R（q））;因此，根据需要，我们给出了嵌入开映射fp，fqQ6讨论和结论性意见在本文中，我们已经证明，对开映射定义的具体范畴论解释使得这一概念适用于更广泛的行为模型和更广泛的行为等价。特别是，我们已经证明了它能够在前缀序的设置中消除分支互模拟的概念（这在以前是不可能的）（其中开映射的原始定义没有产生令人满意的结果）。此外，我们还证明了在前缀序范畴中，通常参数化开映射概念的路径范畴可以被选择为嵌入的子范畴，从而赋予它一个自然的和完全的范畴论刻画。仔细研究一下我们在定理4.4中得到的互模拟的特征，就会发现被扩展的路径不一定有最大值。这意味着，也考虑了无限长路径的延续，例如在Zeno行为背景下的混合系统文献中出现的情况[18，10，6]。因此，我们希望开放地图可以用来保持这些现象在一个统一的方式。从哲学的角度来看，使用行为模型的具体类别意味着我们要以这样一种方式区分实现和观察，沿着这些思路解释定理3.4中的结果，我们看到X与Y是双相似的，并且实现Y的附加行为的X的任何可想象的扩展已经在X中可观察到（尽管可能已经被不同地实现）。仍然，它取决于具体的类别，哪些实现实际上是扩展，即。这是需要保留的嵌入。在寻求一种通用的方法来建模计算和其他动态行为，下一个合乎逻辑的步骤似乎是研究Pfx上的分裂忠实函子。这可能会给洞察力，其中嵌入是和不被考虑。在某种意义上，我们已经在第5节中研究了这样的分裂，只考察了标记的跃迁系统的游程，而没有考察跃迁系统本身。但更一般的理论可以在这里找到例如，取任意一类句法计算模型M。我们期望这个类别中的模型的执行将形成一个前缀顺序，这意味着M中的实现可以映射到Pfx中的历史保留映射和Pos中的顺序保留映射。从哲学的角度来看，M的句法结构是66H. Beohar，P.J.L.Cuijpers/Electronic Notes in Theoretical Computer Science 319（2015）51实现和Pos的保
我的内容管理
展开
