理论计算机科学电子笔记264（2010）63-81www.elsevier.com/locate/entcs对称族作为资源绑定西恩佐·钱西亚1Institute for Logic，Language and Computation（荷兰阿姆斯特丹）亚历山大·库尔兹2莱斯特大学（英国）乌戈·蒙塔纳里3Universit`adi Pisa（IT）摘要以资源分配结构为特征的演算（例如pi演算或融合演算）需要特殊类型的模型。最著名的是预层和名义集。但命名集合的优点是在其他两个集合无限的情况下，它们都是有限的。这三种模式是等价的。命名集的完备性与命名集的有限支集和相应的预层的概念严格相关。我们表明，命名集概括的范畴模型的家庭，也就是说，免费的余积完成，索引的对称性，并解释如何当地的接口提供良好的计算性能的家庭。我们通过引入一个概念推广了以前的等价结果最小支持在preheaf类别索引小类别的monos。 函子和范畴余代数可以定义在族上。我们证明了最终余代数具有最大可能的对称性，直到双相似性，这可以通过沿着终端序列迭代来计算，这要归功于表示的有限性。关键词：预层，族，命名集，历史相关自动机，余代数，对称约化，划分细化1引言完全抽象和名义演算。编程语言语义中最大的关注点之一是找到完全抽象的模型，1由马德里社区方案PROMESAS（S-0505/TIC/0407）和荷兰科学研究组织（NWO）的VICI赠款639.073.5012EPSRC部分支持的研究EP/G 041296/13由欧盟FP 6-IST IP 16004项目SENSORIA部分1571-0661 © 2010 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2010.07.01464诉Ciancia等人/理论计算机科学电子笔记264（2010）63§等同的程序被识别。一个困难的问题是如何为所谓的交互系统做到这一点，其中重点不是计算的最终结果，而是沿着系统的可能的非终止行为与环境的相互作用。对于像CCS[35]或π演算[36]这样的语言，操作语义是用标号转换系统（LTS）来表示的，而完全抽象模型是所有可能的系统关于双相似性的商。具有资源分配机制的演算（所谓的名义演算）通常具有互模拟的概念，该概念与LTS上的标准概念不一致。因此，标准的定义和算法不能被重用。这可以通过诉诸于预层范畴来解决，即从小范畴C到Set的函子范畴（参见[23，10，9，24，34，33]，以及Moggi [37]的基础工作），或者如[38]所做的那样诉诸于标称集[25预置层处理名称，在一般资源中，在所有可能的进程中具有全局意义。因此，每个新生成的名称必须与所有先前的名称不同，从而在存在循环的情况下产生无限状态因此，演算的操作语义通常具有有限状态，即使对于非常简单的过程，也使得计算抽象语义或实现有限状态方法（例如最小化，等价检查或模型检查）变得困难。命名集。 在命名集合[40，41]的平行研究中，这些困难通过使用局部名称来克服;在这种情况下，只要两个元素相关，就必须在元素名称之间建立绑定。 这台机器允许人们重新使用以前生成的已被丢弃的名称。在[41]中，许多形式主义（例如Petri网和进程演算）已经以完全抽象的方式映射到命名集。这里最重要的发现是，对每个代理的对称群进行建模是有必要的，以获得π演算的唯一抽象模型，从而导致[20，43，21]，其中π演算的共代数最小化（分区细化）算法已经实现，基于历史依赖自动机，即命名集合范畴中的共代数。建模对称性的重要性在编程语言语义理论[45]和实际应用（如模型检查[18]）中都得到了认可。由于群论的众所周知的结果（特别是拉格朗日此外，许多对群的运算可以在压缩表示上计算[32]。在[27，22]中已经建立了名义集合、命名集合和集合I的保持拉回的全子范畴4（称为Schanuel topos在[12，13]中，一些用于π演算的命名集上的ad-hoc构造被转化为范畴概念，如乘积，余积，幂集和名称抽象，从而允许重用相同的机器来表示其他具有名称的演算的语义我们的贡献。预层范畴的一个优点是通过改变索引范畴C可以获得可伸缩性，从而产生更复杂的结构。[4]这里I是自然数的有限子集和它们之间的注入的范畴。诉Ciancia等人/理论计算机科学电子笔记264（2010）6365§§§§§[2019 -03 -28][2019 - 03 - 18][2019 - 03 - 18][2019 - 03 - 19][2019 - 03 - 19]当使用命名集合时，这种可伸缩性就丧失了，因为索引类别被固定为I。首先，在2中，我们引入族作为自由余积完备化的具体表示。我们的贡献开始于3观察到，具有对称性的命名集被自同构和相关态射的群的范畴上的家族的范畴模型推广，我们称之为Sym（C）。这个模型在范畴意义上等价于集合C的一个完全子范畴，即对称可表示项的余积，也就是说，可表示项通过与自同构群的合成而被表示。预层由族表示为在其可用局部界面上具有附加对称性的元素集。在某种意义上，这已经推广了[27，22]的等价结果。然而，精确刻画哪些预层是（同构于）对称表示的余积是一个困难的问题。也许[25]中最重要的主题是有限支持的概念，它概括了自由变量的概念。 支持度又是定义命名集合和两者之间的范畴等价的关键因素。在第四章中，我们引入了预层范畴中支撑的一般概念。 利用这个定义，我们证明了[27，22]的等价结果可以扩展到由小范畴索引的预层，满足三个条件：索引范畴具有宽回调，并且预层保持它们;索引范畴由mono组成;从对象到自身的索引范畴的所有箭头都是同构。 关于这些条件的一个非平凡的例子是有限等价关系的范畴E和它们的基础集合之间的内射映射，在[3，4]中用于表示进程演算中名称的显式融合前体和族具有非常不同的性质。 我们称之为接口的局部性。 在5我们给出了这个属性的数学解释， 这反映在产品结构中。 在预层中，乘积只是逐点计算，而在族的情况下，它涉及到每个所涉及元素的局部界面到更大界面的映射。这对应于两种完全不同的观点，尽管它们是等价的，关于系统如何与接口相关的观点：要么假设一个命名机构为每个可用的资源提供全局意义，要么依赖于连接不同系统的局部范围的链接在6中，我们展示了如何计算一个余代数的元素的行为对称性，也就是说，最大的同构群，使一个元素与自身双相似。我们注意到，§5和§6不依赖于§4的条件，而是在§3的一般框架中。相关工作。据我们所知，对族的研究是为了有效地表示程序设计语言的语义，并将它们的性质解释为接口局部性理论，这是新的，以前从未被研究过。对称表示的余积也是有趣的，作为Joyal [30]的解析函子的推广。这是由Ad'amek和Velebil[2]的情况下，locally可presentable指数范畴。这条研究路线在范围和目的上与这项工作不同：在那里，分析函子之间的态射的表征（解析函子的正则自然变换）。66诉Ciancia等人/理论计算机科学电子笔记264（2010）63§⊆→| |对于中的共管道P，我们使用对{x，p} 的集合，|x∈S，p∈P}.xxx∈S∈{n}Iii∈Iff∈我∈H对于每个i ∈ I，ni∈|C|. 一箭i∈I{ni}到j∈J{mj}是一个元组i∈I我我[30]）是可取的，但它仍然是一个开放的问题。 而应 4我们发展范畴的等价，通过族的态射来表征子范畴的所有自然变换。此外，[2]对称化的可表示项的余积和我们的余积并不互相暗示，并且有一些与我们的目的有关的范畴的例子，它们只属于我们的条件（见§4）。2背景在这里，我们介绍了与族构造Fam（C）有关的基本概念，Fam（C）是C的自由余积完备化的表示。备注2.1（符号约定）。对于C一个范畴，我们用C表示它的对象，用C（n，m）表示从n到m的箭头的集合。我们扩展了一些分类符号的箭头集。 设FC（n，m）是一个集合;我们定义dom（F）=ncod（F）=m. 当F和G是两个这样的集合，dom（F）=cod（G），f：cod（G）→ mJ，g：mJJ → dom（F）时，我们定义f<$G= {f <$g|g ∈ G}，F <$g ={f} |f ∈ F}，且F <$G ={f <$g |f ∈ F，g ∈ G}. 作为元素的符号设置箭头元组fi∈ I的配对记为i Ifi。在函数和函子的应用中，我们经常省略括号，例如，我们写Ffx来表示函子F：CSet在箭头f上的作用，应用于元素x。对于回调，我们实际上指的是宽的，但很小的回调，也就是说，由任意数量的箭头组成的图表。范畴C的自由余积完备化的一个直接描述是通过族构造得到的，定义如下。定义2.2给定一个小范畴C，范畴Fam（C）的对象是C的对象的族，即Set中单例的余积，其中是一个集合，其中f：I→J，对于每个i∈I，H：ni→ mf（i）.一个族是一个集合I，其中每个i I都有一个相关联的C对象ni. 例如，集合I可以表示系统的状态集合。对象ni表示状态i的接口。例如，ni可以是一组名称、网络拓扑或与过程演算的状态相关联的任何其他可能的特征。每个箭头都是两个集合I和J之间的函数f，对于每个i I，都有一个从i的接口到f（i）的接口的映射f。这反映了接口对于每个元素都是局部的想法，因此要正确定义这些元素之间的函数，还必须指定目标元素和源元素的接口是如何相关的。当我们使用族来表示预层时，这些映射是从另一个方向进行的，即从目的地到源。从上面的定义来看，这并没有太大的区别，因为我们可以只考虑范畴Fam（Cop）来得到这些“向后”的箭头，正如我们在下面将要做的那样 一个有助于直觉的本地接口的真实例子是内存的内射重新标记诉Ciancia等人/理论计算机科学电子笔记264（2010）6367{n}{m}iji∈Ij∈J在垃圾收集语言中，在调用垃圾收集器之后可能发生的位置。在这种情况下，系统状态有一个相关的内存布局（在我们的术语中是“接口”），它可能在执行的每一步都发生变化。重新标记是我们提到的“向后”箭头，映射内存布局将目的地的变量转换为源的变量，从而跟踪变量的历史以及它们在计算过程中的内存位置。Fam（C）中的余积是自由生成的，并描述如下。定义2.3两个对象在Fam（C）中的余积，定义为k∈ I+J {ok}，其中ok= ni，如果k=<$I，i <$，并且ok= mj，如果k=<$J，j<$。3对称族在这一节中，我们介绍了集合C中的预层的一个条件，即是对称表示的余积。这个术语是从[2]中借用的。在本文的其余部分，我们将讨论良好的计算性能，这样的表示，并介绍了一个表示性准则的指标范畴monos上的预层。3.1Sym（ C）类首先，给定一个小范畴C，我们定义一个自同构群范畴， 以及它们之间的态射，我们称之为Sym（C）。定义3.1我们定义C上对称的（小）范畴Sym（C）：|Sym（C）|={Φ C（n，n）|Φ是一个群w.r.t. 组成}n ∈|C|Sym（C）（Φ 1，Φ 2）= {h <$Φ 1|h ∈ C（dom（Φ 1），dom（Φ 2））<$Φ 2<$h <$h<$Φ 1}每个对象的目标是idΦ=iddom（Φ）<$Φ=Φ，f1=h1<$Φ1的组成f2= h2<$Φ 2定义为f2<$f1= h2<$h1 <$Φ 1。Sym（C）的一个对象仅由群Φ表示，省略了恢复为dom（Φ）的余积的索引n，dom（Φ）是Φ中所有自态射的公共域。范畴的箭头是来自C的箭头集合，通过用单个箭头合成一组同构而获得。请注意，最后一个等式左侧的组成符号是Sym（C）中的组成，而右侧的组成是组成箭头组，如备注2.1所示。 然而，下面的引理确保了两种可能的解释是一致的。 这是一个条件的后果Φ2 h h Φ1.引理3.2考虑两个Sym（C）arrowh2<$Φ2：Φ2→Φ3和h1<$Φ1：Φ1→Φ2。 它认为（h221|1∈ Φ 1}。最后，我们注意到C完全嵌入Sym（C）。68诉Ciancia等人/理论计算机科学电子笔记264（2010）63−◦→| |−→ →◦→--{|→}−定义3.3嵌入J：C→Sym（C）在对象上定义为J（n）={idn}和箭头上的J（f）={f}。3.2对称表示族在 本 文 中 ， 我 们 让 C 表 示 一 个 小 范 畴 。 我 们 记 得 ， （ 协 变）hom函子C（n，）：CSet，对于n是C的对象，作用于每个对象m作为C（n，m），并作用于每个箭头f：m1m2为C（n，f）（g：nm1）=fg：nm2。 集合C中的可表示预层是同构于C（n，）的函子，其中n是C的对象。定义3.4设Φ是Sym（C）的一个定义域为n的对象。我们称一个对称可表示的C（n，−）/Φ为一个由指标关系g1<$mg2<$mrp ∈ Φ.g1=g2<$ρ表示的可表示的，其中g1，g2：n → m。这样的商在每个指数m处的等价类方便地描述为每个可能的箭头与Φ的合成，即（C（n，）/Φ）m=hΦh：nm。在下文中，我们假设对称的可表示物是这种形式。 请注意，任何fΦ都是Sym（C）的箭头，这产生了我们提出的表示。为方便起见，我们也说明对称表示在C的箭头上的作用，即（C（n，−）/Φ）f（h<$Φ）=f<$h <$Φ。在集合C中的预层中，有一些同构于对称表示的余积，从而产生了集合C的一个完全子范畴。这个subcatory等价于Fam（Sym（C）op）。 在本文的其余部分，我们将主张， 使用族的表示对于计算机科学应用是有吸引力的第一尽管等价性的证明很容易理解，但我们通过下面的著名命题（见[8]，引理42），也在[42]中使用，来证明命名集和Schanuel拓扑之间的等价性，命题3.5设DJ是一个具有小上积的局部小范畴，D是一个小范畴。一个函子F：D DJ可以扩展为从Fam（D）到DJ的等价，如果它满足以下条件：F是一个嵌入（它在对象和态射上是单射的）; F的像中的对象是不可分解的（对于D中的每个n，hom函子DJ（Fn，）保持余积）; D J的每个对象都是F的像中的对象的余积。这里我们用D=Sym（C）和DJ是集合C中对称表示的余积的子范畴来举例证明这个定理。首先，回想一下，如果C是小的，函子范畴集合C是局部小的，并且有余积（逐点定义），因此命题3.5是适用的。我们现在展示一个函子F：Sym（C）op→SetC。定义3.6函子F作用于对象的形式为F Φ = C（dom（Φ），−）/Φ。F作用于Sym（C）op的ea ch owhΦ1：Φ2→Φ1，返回自然变换，在每个索引n处定义为（F（hΦ1））n（hJΦ 2）= hJ h Φ 1。接下来，我们证明F满足命题3.5的第一和第二个条件。第三个条件是通过构造来满足的，即把F的余域限制为对称的可表示的。诉Ciancia等人/理论计算机科学电子笔记264（2010）6369我P，−P{}ii/Φi∈Ii∈IiF我∈定义3.8函子Presh：Fam（Sym（C）op）→SetC映射对象i∈I{Φi}H令Q=j∈JC（dom（Φj），-）/Φj，g：P→Q是一个自然变换，（i∈I我命题3.7F是一个函子，特别是一个嵌入，即在对象和态射上的内射。对于每个对象Φ：Sym（C），F Φ是不可分解的，也就是说，母集函子SetC（F Φ，−）保持余积。因为集合C有余积，所以F扩展为从Fam（Sym（C）op）到集合C的函子。成i∈I FΦi和箭头F Φf，i∈I{Hf}时间：i∈I联系我们j∈J{ΦJj}进入自然状态-拉尔变换J（if（i）<$FHf），其中if（i）表示第f（i）次注入，余积j∈JFΦJ。i∈ Ii根据定义，Presh图像中的每个预层都是对称的可代表的人函子是满的、虚的，当它的余域限制在它的象上时，函子成为范畴等价另一个方向由函子K将对称表示的余积映射到Fam（Sym（C）op）中给出。 对对象的操作是相当琐碎的。给定=C（dom（Φ）），我们有K=Φ。对箭头的作用更多mation。我们定义了族K（g：P→ P J）= K_f之间的态射，为每个，（Φ. 然后我们让 ）JΦ{H}。i∈Igni，iddom（Φi）i吉吉f（i）=j，f= hJΦ j。 函数f由F的像中的对象的不可分解性很好地定义（Prop。3.7），反过来又来自于G的自然性。K在箭头上的作用可以用族中局部界面的概念来粗略地解释。在引入轨道和代表的概念后，这一点会得到更好的理解，这在§4中已经完成。4回撤-保存、单操作系统和最小支持在这一节中，我们将说明在由单元索引的范畴中对称化可表示对象的余积的特征，作为保持所有拉回的函子。我们考虑Gabbay和Pitts关于名词语法的工作中的有限支撑条件[26]：每个系统都有一个唯一的最小回调的保持意味着在非常一般的意义上保持“接口的交集”，并且使得有可能恢复预层P的元素x Pn在任意范畴C上的支撑的概念作为最小索引nj，其中元素x j ∈ Pn j存在，使得对于某个箭头f Pfx j =x。这里给出的结果在精神上类似于Joyal [30]给出的将解析函子表示为种的方法，因此也类似于[2]，在[ 2 ]中，与我们相似的条件被勾画出来，以确定对称表示的余积。我们强调，后者的研究路线的目的是扩展和扩展Joyal因此，我们能够提供范畴的等价。此外，[2]中的索引范畴应该是局部可表示的（或者至少应该有一个初始对象，参见其中的§3），从而裁定70诉Ciancia等人/理论计算机科学电子笔记264（2010）63⟨⟩给出了离散范畴和范畴的余积（因此我们的结果和[2]是逻辑独立的）。在不同的著作中已经研究了预层作为族的可表示性和拉回保持之间的联系。众所周知，[7]。在那里，连接的限制，广泛的回调保存和家族代表性之间的存在的连接进行了解释。但是在那里，家族表示的索引范畴仍然是前层范畴的同一索引范畴C，而不是它上面的对称范畴，后者确实提供了一个多一点的结构，我们然后将其用于§6的对称约化过程。用对称族表示拉回保持的预层的思想来自Staton [42]，在那里它作为一种证明技术出现，以证明命名集和Schanuel拓扑是等价的。我们在本节中提出的技术结果是该工作的直接概括，尽管目的不同，因为我们的目标是解释家庭模型的计算特性，这在本文的其余部分完成宽回调是任意基数的上锥的极限（而普通回调是只有两个箭头的上锥的极限请注意，在[42]的Schanuel topos的特殊情况下，这些图必然是有限的，因此宽回调是由二进制决定的从现在开始，我们让集合C表示集合C在以下条件下进行实例化♦. 我们的理论是准则4.1我们假设C的所有箭头都是monic的，C有（小的，宽的）回调，并且对于C的每个对象n，每个f ∈ C（n，n）是同构。注意，我们不需要C的强性质，例如完备性或余完备性。一些例子可以阐明特性的适用性离散类别：单对象单箭头类别1可以用作索引，导致框架的退化实例化，实际上只包含集合和函数。这是正确的，因为Set1是Set。 更一般地，可以使用离散范畴，在这种情况下，我们将定义的表示只是每个预层的元素集合，即对n，x，其中n是x所在的索引。这是一个非常自然的多排序集的表示。这两个例子表明，定义也适用于这些退化的情况，给出了预期的表示。范畴的余积两个非空范畴的余积当然没有初始对象，它也不是完备的。然而，从编程语言语义的角度来看，这些索引类别可以用来表示具有几种不同类型的代理的演算，每一种代理都有不同的相关接口概念有限集和注入：在这种情况下，所获得的等价性是Schanuel topos和[22，27]的命名集之间的等价性。正如我们已经强调的那样，相关的类别已经在广泛的应用中使用。族和命名集之间的对应关系通过范畴定义而变得清晰诉Ciancia等人/理论计算机科学电子笔记264（2010）6371♦♦♦⟨ ⟩ ∈[44][45][46][47][48][49] [4有限图和注入：这一类别可用于建模演算，其网络结构在语义上是显式的（与π演算相反，π演算的网络结构在代理的通道知识中是隐式网络协调策略演算（NCP）[11]是由第一作者等人在面向服务计算的形式化方法的背景下开发的。 在微积分中，状态是由网络拓扑组成的对， 一个图表，一个政策，一个程序。整个新鲜的子拓扑可以动态地分配沿操作语义的过渡。尽管在这项工作中没有使用范畴理论，但似乎很明显，语义可以使用标准的预层方法来表示，使用有限图和注入作为索引范畴。 在NCP中，互模拟用于定义规范和实现的一致性，因此高效互模拟检查器的实现（考虑框架的动态分配能力）具有高度相关性。因此，微积分将是一个有吸引力的案例研究对称性约简算法，我们在这项工作中素描。融合：融合可以用一元箭头的等价关系的索引类别E来描述[3]。这个类别有回调，落入我们框架的条件，它有丰富的对象结构，用于融合(see（28，34）。4.1预层的对称分解我们现在证明，在Crit.4.1下，集合C同构于余积对称的可表示对象，也就是函子Presh的图像中的对象。因此，全范畴集合C与coprod的子范畴完全一致。对称可表示的结构。我们再次使用3.5号提案来追求我们的目标。F是一个嵌入，其图像中的对象的不可分解性不受附加假设的影响。然而，我们必须证明F的图像中的每个预层是拉回保持的。定理4.2对于每个Φ，假设条件4.1，F Φ保持宽回调。本节的其余部分致力于证明Prop.3.5的最后一个必要条件，即每个保留拉回的预层是对称表示的余积我们回想一下预层的元素的概念。此后，我们设G表示集合C中的任意函子。定义4.3G的元素集定义为El（G）=n∈|C|Gn.为了可读性，但不失一般性，在下文中，我们假设所有Gn都是不相交的，使得我们能够仅用x表示元素n，xEl（G）。必要时，我们将x的阶段n表示为st（x）。粗略地说，我们的目标是通过表示所有的元素来表示预层，72诉Ciancia等人/理论计算机科学电子笔记264（2010）63{→|{\fn方正黑体简体\fs18\b1\bord1\shad1\3cH2F2F2F}||♦∈X^X^当Pel（G）={x^|x∈El（G）}.定义4.8设x∈El（G）. We表示x的代表，即，N^定义4.9x∈Pel（G）的对称性是同构群Gxb=X现在我们可以从集合C定义一个函子（一）与人交往;可以为了使这个公式形式化，我们引入了轨道的概念。定义4.4给定x∈El（G），它的轨道Ox是元素y∈El（G）的集合，使得存在一个跨距st（x）fxsfyst（y）和一个元素ntz∈Gs，其中Gfz=x且Gfyz=y。←→换句话说，轨道是元素范畴中的连通分量。在下文中，对于xEl（G），我们设Dx是C中由态射组成D：nst（x）yG（n）. Gdy=x，对于n的范围为 C. 注意，对于每个d，y是唯一确定的：Gd是单射的，因为G是拉回保持的，因此是单保持的。下面的引理构成了我们表示法的基础 这可能是轨道最重要的性质，因为集合C的拉回保持性。引理4.5设x和y属于同一轨道。设n是Dx的回调对象，m是Dy的回调对象。n和m之间存在同构，使得n是Dy的拉回.我们现在定义元素x的支集，粗略地说，这是可以找到具有与x相同性质的元素的最小索引定义4.6设xO表示Ox中元素的选择。我们定义x的支撑，用Sx表示，作为D（xO）的拉回对象，归一化箭头Nx：Sx →st（x）作为Dx的拉回图的对角线，其中我们通过引理4.5选择Sx作为拉回对象。这里的对角线是指Dx中的任何箭头与相应的箭头的合成，这些箭头使拉回可交换。我们将看到集合C的一个对象被确定（直到同构）一组代表x♦的元素，称为适当的元素，并由一组同构在一个其作用不被改变的空间上。保持回调在这里起着重要的作用，允许我们证明下面的引理并定义元素的表示引理4.7re存在唯一元素x∈GSx使得GNx^=x。GSx的元素，使得GNx（x）=x。 定义了G的真元集合，在这个构造中，x扮演着一个规范箭头的角色，x代表x。这种对称性使每一个适当的元素Sym（C）的对象^{ρ：Sx→Sx|Gρx^=x^}。^函子Presh♦第3.8节，完成了分类等价。诉Ciancia等人/理论计算机科学电子笔记264（2010）6373^SX^^bb♦♦{}∈1→2定义4.10对称分解SymDec：SetC→Fam（Sym（C）op）是定义在每个预层G和自然变换f：G上 B.G. 作为SymDec（G）={Gb}SymDec（f）=Σλx^. f^x（x^）， {Nf （xb）<$Gf^（xb）}<$Xxb∈Pel（G）Sxb∈Pel（G1）函子对对象的作用只记录了G的真元及其对称性。对箭头的作用是Fam（Sym（C）op）的箭头，因此是两个索引集之间的函数，以及Sym（C）op中的箭头族。前者回归，对于每个代表x，f（x）的代表关联的映射^Sx^箭头是每个获得的元素的归一化箭头，由对应的对称性。 使用它，我们可以从它的表达式重建fSx（x），感情用事通过将元素的支撑和对称性考虑为该元素的一个局部界面，可以获得更多的直观性。Nf （xb）的幂级数Gf^（xb）emb将f^（x）in的 in界面添加到f的 in界面（x），其中ch与x相同因为Sx^SX ^ ^您的位置：f是点式定义的。正常化箭头是所谓的在命名函数的文献中使用了沿着态射的名字垃圾收集器在编程语言的实现引理4.11我们有Ghx=x，且N Ghx∈ h<$G x。定理4.12集合C中的每个预层G同构于Presh（SymDec（G）），其中-前集合C等价于Fam（Sym（C）op）。注4.13所提出的用族表示预层的一个很大的优点是减少了所表示的预层的大小（元素的数量），甚至从无限集合中得到有限集合，同时保持了美学性质。例如，集合I中的“包含”预层Gn = n，Gf = f，即集合I中的名称对象，由Fam（Sym（I）op）中具有单个元素6的族表示，即i 1 id 1。这一命题的直观含义是，每个自然数与任何其他自然数都没有区别，并且有一个单一的“名称”（和平凡的对称性）作为其界面。这种5界面的局部性：产品结构在[44]中，其中一位作者将[27，22]的等价性推广到等价内函子的余代数范畴，以便对过去用于命名集的各种构造（包括π-演算的最小化）给出范畴刻画。在这里，我们概括的产品上的结果命名的集合。[5]在我们的例子中，我们应该称之为沿着态射的界面的历史6G与最终对象i ∈ 1 { id 0 }不同，有一个具有平凡接口的元素74诉Ciancia等人/理论计算机科学电子笔记264（2010）63cod（）.⟨⟩×∪∪∈ ∈ ∈JJ=， =.Gk∈KKk∈KKK多（余）积是多（余）极限概念的一种特殊化，”[16]《明史》：“明。众所周知（例如见[14]，注释5），只要C有多个乘积，Fam（C）就有乘积，并且对偶地，如果C有多个余积，Fam（Cop）就有乘积。在这里，我们提供了一个具体的特征函子，强调全局和局部接口之间的区别。这里给出的结果不依赖于C的箭头是单的。定义5.1给定一个由对象n1，...，nk，D的多重余积是D上的余锥的集合mcp（D），使得对于所有余锥LJ= n f1：n1→ mJ，.，fk：nk→ mJ在D上存在唯一的上锥L=n 11：n1→ m，.，<$k：nk→ m <$∈ mcp（D），以及一个唯一的箭头uLJ：m → mJ使得图L LJuLJ可换.唯一的上锥L将被表示为mcp（LJ），具有一点重载换句话说，两个对象P和Q的多重余积是它们之间的一组典型余跨距，在这个意义上，它们被余跨距的同构所约束，并且它们是最小的。我们注意到Sym（C）有多重余积。定理5.2如果C有宽回调，则Sym（C）有多重余积。在下面的定义中，我们假设C有多重余积，P= iI{ni}，Q =iJ{mj}，R=kK{ok}是Fam（Cop）的三个任意对象，并且我们用S表示集合{ki，j，k i1，k2} |i ∈ I <$j ∈ J <$1，<$2<$∈ mcp（<$ni，mj<$）}。定义5.3Fam（Cop）中P和Q的乘积定义为对象P×Q =i，j，1}乘积P Q的元素是三元组，由P的一个元素、Q的一个元素和一个与它们的对称性相关的（正则）cosspan构成定义5.4设π1J和π2J表示三元投影的前两个投影。乌特河 投影π1：P×Q →P和π2：P×Q →Q定义为：π1<$π1，<$i，j，<$i1，<$2 <$$> ∈S{i1}<$π 2<$π2，<$i，j，<$i1，<$2<$$> ∈S{i2}<$定义5.5f，{Hf}的配对：R→P和g，{H }：R→Q是箭头h，{Hh}，其中h（k）=f（k），g（k），mcp（Hf，Hg），和Hh = ufg.k∈Kk k kHk， Hk定理5.6上面给出的乘积、投影和配对在Fam（Cop）中同构地标识二元乘积。在上面的定义中，mcp（n f，H gn）和ufg来自Def.5.1。我们kk Hk， Hk保持直觉，即集合C中的索引类别C应该被视为一组可能的类型，或预层元素的接口在这个意义上，上面的积的定义给出了族中界面局部性的概念，而不是在预层范畴中的全局诉Ciancia等人/理论计算机科学电子笔记264（2010）6375在集合C中，乘积是逐点定义的，如果两个元素在适当的（公共的）上下文中，它们可以通过配对来关联。也就是说，任何两个接口都有一个嵌入到一个共同的，更大的接口的自然选择在名称的情况下（也就是说，索引类别是I），这是π演算所采用的观点，其中主体的所有非限制通道的名称在系统的所有参与并行组件中具有全局的，唯一的含义，就好像有一个命名权威为任何名称分配含义在Fam（Cop）中，每当我们将两个元素放入一个关系中时，我们必须通过将它们显示为一个公共对象的子对象来显式地在它们的接口之间建立一个链接，充当所获得的元组的接口。在姓名方面，这对应于必须在这可能是最自然的选择，只要你想对没有命名权威的系统建模，作为对等系统。例如，Fam（Cop）中的双相似性由三元组组成，因为它是产品的子对象：为了比较两个系统，我们需要在它们的本地接口之间建立对应关系。6基于最终语义的操作语义的预层方法大致包括定义一个项的预层P，即一个预层范畴上某个内函子的初始代数，以及某个内函子T的从P到TP的余代数，从而提供了演算的语义。到T的最终余代数的唯一态射于是给出了抽象语义的余归纳定义。在这里，我们将Fam（Sym（C）op）中元素的对称性与行为等价联系起来，定义为余代数态射的拉回对象。 我们注意到，如果行为函子T保持弱回调，则共代数双相似性和行为等价性重合（详见[31]或[1]）。给定Fam（Sym（C）op）中的一个余代数，和一个元素i，具有对称性Φ，其中dom（Φ）=n，我们解释了如何沿着唯一态射计算i到最终余代数中的像对应于识别n的子对象，该子对象在i的语义中是活动的，以及在这个对象上保持行为等价的最大可能对称性。这个结果的意义在于为语义的对称约简提供了一个清晰的框架（即预层和族之间的等价性的编程语言。对称性约简是计算机科学中一个活跃的研究课题，它包括寻找具有对称性的系统的压缩表示（参见[15]和随后的作品，或最近的[19]）。这通常是通过利用演算语法上的方程，或者通过“手动”向模型添加对称信息来完成的。我们的方法是非常不同的：它允许一个计算的行为对称性，也就是说，最好的对称互模拟。在互模拟是选择的等价关系的所有情况下，这当然是需要的（例如，面向服务计算中的静态分析与模型检测76诉Ciancia等人/理论计算机科学电子笔记264（2010）63§我n我我ZH我我G=i∈IFΦi，一个自然变换f：G→GJ，以及相应的箭头◦ H我我n我我我我我我Hennessy-Milner-like logics）。模型检查可以在对称性存在的情况下有效地执行[18]。6.1对称约化注6.1等价性扩展到合适的“等价”内函子的余代数范畴。特别地，在集合C中具有最终余代数的对称表示的余积的全子范畴上的每个闭函子TJ具有 Fam（Sym（C）op）上的等价的内函子，它允许一个最终余代数，得到（直到同构）为T=SymDec <$TJ<$Presh。下面我们假设这样一对等价的闭函子TJ和T。即使对于本工作的范围来说，T的给定定义是充分的，也可能需要有一个T的合成定义，以便T（P）的元素从P的元素导出。例如，在乘积的情况下，5的定义与我们刚才提到的定义同构，但不相同。这个问题已经在[44]中详细研究过了我们现在观察到，对称化的可表示物的余积之间的每一个自然变换在其源的元素上诱导对称性，明确地表示在Fam（Sym（C）op）的相应箭头中。考虑一个预层布雷格，i∈I{Hg}尺寸：i∈I{Φi} →j∈J{ΦJj}。定义6.2令Rf表示来自核对的关系，componentff在n。 设x∈Gn. 我们称集合Gh={ρ：n→n|Gρx Rfx}nxn由f引起的x上的对称性。命题6.3对于每个i ∈ I，n ∈ |C|，h <$Φ i∈ F Φ in，且ρ：n → n，我们有（F Φ ρ（h <$Φ））Rf（h <$Φ）当且仅当ρ <$h<$Hg = h <$Hg.观察到ρ<$H<$H g=h <$Hg意味着，对于h<$Hg中的每个h j，同构ρJ∈ ΦJg（i）使得ρ<$hJ=hJ<$ρJ，即由f在ΦJg（i）中表示。现在很明显可以观察到，由余代数态射诱导的对称性与互模拟有关。 当f是最终余代数的唯一态射时，诱导对称是最大可能的子集。我们称之为行为对称。在这种情况下，hg中的箭头标识n的子对象，其直观地是元素的活动不触及它的操作可能不会改变语义。 为了使这一点更精确，观察到，对于每个hJ ∈ h <$Hg，我们要么有ρ <$hJ/= hJ，要么有ρ <$hJ= hJ。第一种情况是对称性ΦJg（i）实际上起作用的情况在第二种情况下，所有的箭头在hHg中，通过hJ与ΦJ中的箭头合成而获得，合成g（i）而ρ保持不变。 那么ρ在某种意义上作用于h所标识的子对象之外G. 例如，当索引类别为I时， h的图像是系统的活动名称的集合，即在最终语义中可观察的名称。诉Ciancia等人/理论计算机科学电子笔记264（2010）6377∈ {G}→◦∈ {G } →→◦◦◦◦◦∈P ×−∈ {G } →6.2作为通用对称约简算法的在这里和下一节中，我们将解释如何在某些有限性条件成立的情况下计算微积分项的子集上的考虑在集合C中配备语义的演算，s：PTJP，其中P表示语法。据我们所知（见Rem。6.1），如果P是对称表示的余积，则在对应于TJ的适当的闭函子T的Fam（Sym（C）op）中存在对应的余代数t：PJTPJ。Fam（Sym（C）op）中的划分细化可以在对象q Qq上计算。（拟作为上述PJ的子对象）如下。 首先，我们给出一个抽象的定义--首先给出了一般算法的基本描述，然后详细说明了算法的各个步骤，并讨论了在Fam（Sym（C）op）中计算它们的有限性条件定义6.4Fam（Sym（C）op）中的余代数划分精化是一个使用三个变量f、h和z的迭代算法，表示Fam（Sym（C）op）中的箭头。设f=t，h：q Qq1是到Fam（Sym（C）op）的最终对象的唯一态射，z是从T1到1的唯一态射。迭代步骤（f，h，z）：如果限制到Im（Th f）的z是Fam（Sym（C）op）中的同构，则返回Thf。 否则，设fJ= Tff，hJ=Th，zJ=Tz，并计算迭代步长（f J，zJ，wJ）。该算法的正确性是众所周知的余代数理论（见例[46]）。直觉可以给出如下。在算法的第n次迭代时，T h的核 f：Q QQTn1是Q的一个划分，它在n步中对具有相同观测值的元素进行划分。在每一步，这个划分被细化，也就是说，可能分裂，根据系统的第n次迭代中所做的观察当z是同构时，到达一个固定点，并且保证在所有连续的步骤中，划分将保持不变。因此，被Thf均衡的Q的元素是双相似的。同构z是最终余代数的一个子对象，表示Q的元素的行为。算法的收敛性等价于确定程序的语义，因此不能保证对所有演算都是先验的。对于图灵等价语言，算法收敛于所有可能程序的不可判定子集.在标号转移系统中，如果从给定的初始状态集可达的状态集是有限的，则收敛。 当使用余代数时 在预层上，即使是平凡的程序也有有限的状态，但相应族的元素的有限性足以保
我的内容管理
展开
