并发系统中的类型结构和范畴框架：基于CCS风格进程通信的研究

47→→→→《理论计算机科学电子札记》68卷第1期（2002）网址：http://www.elsevier.nl/locate/entcs/volume68.html23页拉尔夫·施魏迈尔英国伦敦城市大学计算机系ralf@soi.city.ac.uk一种用于CCS风格进程通信类型化的摘要范畴论在顺序编程语言的类型系统研究中被证明是一个有用的工具。已经提出了各种方法来使用的基本模型来检查类型结构适合并发系统。在本文中，我们概述了其中的一些方法，如交互类别，并认为它们不适合用于CCS或π演算中的握手通信机制建模。我们提出了另一种通用的范畴框架来研究这类系统的类型结构，并展示了它的范畴结构，这是类似于现有的方法。然后，我们详细研究了这个框架的一个实例，基于CCS的一个简单的片段。我们证明，它是同构的一个语法类别构造从一个过程代数类似CCS，融合算子，在融合演算。 因此，我们显式的一些类型结构隐含在这样的进程代数。1介绍对于顺序编程语言，分类方法在类型结构的研究中非常有用[11]。 有人试图在利用范畴理论研究并发系统。一般的想法，如主张，例如。 在[2]中，将类型建模为对象，将过程建模为态射。在这种情况下，类别中的构造对应于类型构造函数和过程构造函数，提供了根据类型规则组合过程的方法。并发系统中的关键操作，交互，是由范畴中的原语操作，态射组合来建模的。因此，将一个过程看作一个态射p：A B，对象A和B表示一个过程的接口，分为两部分。态射p：A B和q：B C的组合产生一个过程p;q：A C，它由在B型接口上交互的过程组成，然后对外界隐藏。该操作对应于在CCS等进程演算中具有隐藏/限制的并行组合[24]。在此设置的图形表示中，作为态射p的过程：2002年由ElsevierScienceB出版。 诉 操作访问根据C CB Y-NC-N D许可证进行。S·施威迈尔48ppBQQp→→→→ → ⊗ →⊗(1) 过程（2）合成（3）张量积p qp;qA BA BA CC DFig. 1. 流程的图形视图一个B被看作是一个图，其输入边代表类型A，输出边代表B，如图1（1）所示。在此表示中，边表示线路或通道，一个进程可以在其上与其他进程交互。过程p：A B和q：B C的组成可以用图1（2）来表示。为了使两个进程相互作用，它们通过它们匹配的B型接口连接起来，在结果进程p;q：A→C中，这个接口对外界是隐藏的。没有相互作用的过程的合成由张量积来模化，在范畴上产生么半群结构。对于态射p：A B和q：C D，张量积p：A C B D可以如图1（3）所示。张量积可以被看作是一种配对运算，它将两个过程组合在一起，而它们之间没有相互作用，并使它们的界面都对外界可用。可能存在其他有趣的结构，如对偶性，表示界面两侧之间的对称性;或紧凑的闭合结构[20，2]或允许形成循环网络的迹[19，1，36，26]的过程。按照这些思路，对过程类别有各种不同的方法交互类别[2]基于类似于同步CCS [23]的进程演算，并且具有丰富的类型结构，例如允许指定死锁自由[3]。在[36]中引入了一个类似的类别，基于CCS类进程演算的转换系统来研究异步进程的结构。动作演算[27]提供了一个通用的设置，在其中研究各种顺序或并发演算，基于名称和控件的基本概念。控件是流程的基本构建块，而名称则提供交互点。 瓦片模型[14]是一种通用的范畴模型，其目的与动作演算类似：给出一个统一的框架来建模各种过程演算;它们基于转换系统的一般概念。这些分类模型都有一个共同的对称monoidal结构，由其他结构丰富，如时间结构来模拟过程的动态[2]，或跟踪monoidal [19]，紧凑封闭[20]或类似的结构[7，8]来模拟过程的连通性。在本文中，我们将简要介绍其中的一些范畴框架S·施威迈尔49→并认为它们不足以对CCS [24]，π演算[28]或并发ML [31]等语言中的握手通信机制进行建模。然后，我们将激励和提出一个替代的分类框架，在其中为CCS风格的通信类型建模。该模型是通用的，应该允许各种过程语言的建模，以及不同类型的信息。我们详细研究了该模型的一个特定实例，基于进程代数CCS。特别地，我们证明了这个模型是作为一个带有融合的CCS风格进程代数的语法范畴出现的，就像在融合演算中一样[29]。本文的结构如下：在下一节中，我们提出了一些过程的分类框架，并概述了为什么我们认为它们不适合建模CCS风格的通信。然后，我们提出了一个替代的一般范畴模型的过程类型信息。在第3节中，我们基于CCS的一个简单片段给出了该模型的一个实例。然后，我们在第四节中引入了一个融合的进程代数，在第五节中我们从它构造了一个句法范畴，并证明了它与一般模型的实例2打字过程2.1动机我们想定义一个CCS进程的类别，用类型信息来表达进程的通信能力根据交互作用类别[2]和异步过程的类别模型[36]，一个明显的方法如下：• 对象是有限集合。• 态射AB是CCS术语，其自由名称为A+B，被视为一种适当的双相似形式。• 态射p：A→B和q：B→C的复合由平行复合加限制给出：p; q =（p|q）\B.这种组合确实是联想的，直到强双相似性，但身份是什么？在[2]的交互类别中，通信是同步的，如SCCS [23]。因此，一个恒等态射是一个在其接口的两端不断执行相同操作的进程-它可以被看作是一个立即发送它收到的任何消息的缓冲器。因为它是同步的，所以接收和发送动作同时发生，因此无法区分消息是否通过缓冲器发送。有一个异步版本的交互类别，其中允许进程空闲，因此在同步演算中编码异步进程，类似于异步SCCS [23]。然而，异步交互猫-S·施威迈尔50BBegory仍然包含同步进程;特别地，标识是同步缓冲器。然而，在异步设置中，例如在CCS中，缓冲器通常不会用作组合的标识。例如，在上面的设置中，可以尝试通过以下保护递归将恒等态射idA：A→A定义为具有A + A中的自由名称的CCS过程B方程：B=a∈Aa1。a'2. B+a2. a¯1. 其中a1和a2是a的两个副本A+A。 然而，B未能对某些过程进行识别。例如，与零过程的组合产生（a∈Aa1. a'2. B+a2. a¯1. B|nil）\A2，其中A2={a2|a ∈A}。 然而，这并不等于nil，因为它可以对a∈A执行任何动作a1。在[36]中，一个范畴是通过把恒等式定义为buberger，并把态射集限制到那些buberger的过程p而得到的，即。;p; . 因此，这些bu-1是明显的身份。 在[35]中，给出了用于对缓冲过程进行分类的公理.这些公理相当强。例如，它们要求进程在每个状态下都可以在每个输入通道上进行输入转换。对于先进先出缓冲器，它们要求每个状态最多有一个输出转换。因此，如果我们想要一个所有CCS过程的类别，我们需要寻找不同的身份。恒等式的一个自然选择是nil过程：态射复合是平行复合，而nil过程是平行复合的恒等式。我们建议将流程分为接口部分和行为部分。那么，结构态射（如恒等式）应该有一个这样的设置应该在接口的概念和进程行为的概念上进行参数化，从而提供一个灵活的框架，在其中为不同的进程演算或模型提供各种类型的信息。类似的想法存在于动作演算[27]和瓦片模型[14]中，其中态射是从给定签名的构造器构建的，身份和其他结构态射只是在这些模型中，需要通过给出合适的签名将现有演算编码到框架中。与此相反，我们希望我们的范畴的态射直接由微积分或过程模型中的过程给出，就像在相互作用范畴[2]中，态射是同步树，或者[36]的异步过程模型，态射是转移系统。2.2模型我们现在将正式定义一个进程类别Proc，作为进程行为加上接口信息，如前一节所述。该模型在类别A上参数化，在类别A中对（接口的）类型进行建模，在类别P中对过程行为进行建模，以及函子ar：P→A，S·施威迈尔51→→→→→→→→→→→→→→⊗Ⓢ--→为每个进程行为分配一个arity或type。 我们要求函子是一个上纤维[17]，具有适当的对称monoidal结构。定义2.1设π：CB是一个函数。 态射u：XY in C以上f=πu：A称B中的B为余Z in C使得πv= f; g，对于某个g：BπZ在B中，存在唯一的w：YZ高于g，使得u;w=v。一个函子π：C B称为余纤维化，如果对于C中的每个对象X和态射f：πX B，存在B上的对象Y和f上的余Carnival态射u：X Y。我们称u为f和X的余笛卡尔提升，并将y写成f∈（X），u写成f′（X）。通过滥用语言，我们有时将f∈（X）称为共轴提升。定义2.2设（C，，I）和（B，，J）是对称monoidal范畴。严格对称的monoidal余纤维化是函子π：CB是严格对称monoidal函子和余纤维，对于B中的态射f：A→AJ和g：B→BJ，以及A上的对象X和B上的对象Y，我们证明了f<$（X）<$g<$（Y）：X<$Y→f<$（X）<$g<$（Y）是上笛卡尔提升，fg：AB→AJBJ.现在我们准备列出模型所需的成分• 一个有限余完全范畴A，即它有一个初始对象，二元余积和推出。它有一个对称的幺半群结构，由余积+作为张量积和初始对象0作为张量单位给出。• 一个对称monoidal范畴P.我们把张量积写成②，O表示张量单位。• 一个严格对称的幺半群余纤维化ar：P →A。A上的结构需要对一个空接口、接口的组合和“线”的识别进行建模。我们写作！A：0A表示从初始对象到A的唯一态射，对于态射f：A C和g：B C，我们将从A + B到C的中介态射写为[f，g]：A+B C。当我们要求ar是一个对称幺半群函子时，我们指的是由余积和初始对象定义的A在P中，对象是指过程行为，其中张量积记作P②Q，是平行合成，而张量单位记作O，是零过程。ar是monoidal的事实意味着nil过程的接口是空的，并且并行合成中的接口保持不相交。一个对象P关于态射f：X Y的余卡里提升f（P），ar（P）=X，目的是根据映射f来模拟P（类型X）中自由名的替换。我们把f∈F（P）写成P f，来强调这一事实。S·施威迈尔52→→⟨ ⟩→在第3节中，我们构造了一个严格对称的monoidal上纤维，一个类似 于 CCS 的 进 程 代 数 。 在 [37] 中 ， 并 发 模 型 （ 如 transition 系 统 和synchronization tree）被证明是协同的，通过重新标记给出协同提升。更一般地说，并发的预层模型[10]通常是一类标签集上的构造。现在我们将假设一个对称的么半群上纤维ar：PA为给定的且固定的，并定义一个范畴Proc=Proc（ar）及其结构。类别范畴Proc的对象是A的对象。 A态射p：A B在过程中，B不As X在A中（即一个co-span s，t：A中的A B，参见[4，6]），以及P中的对象P 其中ar（P）=X。与类型论中的符号类似，我们将ar（P）= X写成X <$P，并将Proc中的态射写成图B不AsXP直观地说，态射s和t描述了进程P的接口X如何通过分成两部分A和B的接口对外界可用。余跨距自然地形成一个双范畴[4];为了得到一个范畴，我们定义直到X的同构的态射的相等。设两个同构p，q∈Proc（A，B）是等价的，p<$q，如果在P中存在同构u：P→Q，使得A中的下图可交换B不AsXPSJTJar（u）YQ对于对象A，Proc中的单位态射idA由下式给出：一IDAAidA 一个人！A}S·施威迈尔53⊗其中O是P中的张量单位，ar（O）=0，并且！A是从0到A的唯一态射。因此，恒等态射具有态射复合由下图定义，其中平方是A中态射t和sJ的推出，[e1，e2]是从余积X+Y到Z的中介态射。注意ar（P②Q）=X+Y，因为ar是严格的么半群。直观地说，复合被定义为这种模拟了一个共同的腕关节提升。p：A→Bq：B → Cp; q：A→ CCTJBsJYQ不AsXPCTJBsJYQte2AsX<$Pe1Z<$（P②Q）{[e1，e2]}单轴结构张量单位被定义为A中的初始对象0。在物体上，张量积由余积定义：AB=A+B。在态射上，张量积由下图定义p：A→B q：C→D p<$q：A<$C→B<$DB不AsXPDTJCsJYQB+Dt+tJA+Cs+sJ X+YP②Q张量积的结合性、左单位和对称性的结构同构由下图定义，其中态射αABC、ρA和σAB是结构同构，它们定义了A中关于余积和初始对象的对称幺半群结构，和！表示从0开始的唯一态射。A+（B+C）IDA+（B+C）（A+B）+CαA BCA+（B+C）O{！}一IDAA+0ρAAO{！}B+AidB+AA+BσABB+AO{！}S·施威迈尔54→比姆托范畴Proc具有一些更进一步的结构，类似于交互范畴[2]、异步过程的范畴模型[36]、动作计算[27，15，38]和瓦片模型[14]。我们现在将定义这个结构;为了简洁，我们写得好像C是严格的monoidal，并省略结合性和单位同构。定义2.3设C是一个对称monoidal范畴。C中的交换幺半群是C中的对象A连同态射<$A：A<$A→A和νA：I→A满足下面的公理（1）对偶地，交换可换性是对象A连同态射A：A→A→A，ωA：满足公理（4）-（6）的AI。一个可交换的双半群是一个对象，它是一个可交换的幺半群和一个可交换的双半群。（一）（AidA）;A=（idAA）;A（4）A;（AidA）=A;（idAA）（二）（三）（vAidA）;A=idAσAA;σA=σA（五）（六）A;（ωAσAA=σA定义2.4具有离散双模的范畴是对称monoidal范畴C，其中每个对象都是交换双模，满足以下相干条件。（七）A(9)νAA=νAνA（八）A(10) ωA<$A=ωA<$ωA(11)（AidA）;（idAA）=A;A=（idAA）;（AidA）（12）A;A=idA从公理（11）可以得出，具有离散对偶的范畴是紧闭的[20]，其中对偶是对象上的恒等式，单位和计数分别由νA; ωA和ωA因此，它们也是被追踪的么半群范畴[19]，其中迹是根据紧闭结构来定义的。类似的范畴结构在[7，8]中进行了研究。与我们最相似的是匹配份额范畴，它们几乎是具有离散双态性的范畴，只是它们缺少ν和ω态射;以及部分monoidal范畴，它们是具有离散双态性的范畴，并且还满足公理νA;ωA=idI。对称作用演算[38]具有非常相似的范畴结构。它们实际上是部分monoidal范畴。Proc上的离散双模态结构由以下直径定义克.S·施威迈尔55→[idA，idA]一A：A→AAidA+A[idA，idA]一个人！A}Aid0！一一个人！A}A+A一IDA一个人！A}一IDA0分！ 一个人！A}定理2.5 Proc是一个具有离散双序结构的对称么半群范畴。见[33]，见[34]。3二氧化碳捕获和储存进程在本节中，我们定义了上述一般框架的一个实例，通过定义由基于CCS[24]的一小部分的过程代数中的项组成的过程行为P的范畴，并在有限集合和函数的范畴FinSet中给出这些过程项，从而定义了对称monoidal上纤维ar CCS：P A根据定义中的要求 的Proc。签名我们给出了CCS术语的多排序签名，其中N、A和P分别表示名称、动作和进程以及函数符号in：（N）→AInputactionout：（N）→AOutputactionτ：（）→A Silent action0：（）→P零过程. ：（A，P）→ P 前缀| : (P, P) → PParallel composition+：（P，P）→P 非确定性选择像往常一样，我们将二元运算符写成fix形式。在例子中，我们有时会分别使用更熟悉的a.p和a¯.p来表示in（a）.p和out（a）.p。我们假设替换绑定最紧密，而前缀绑定比并行组合和选择更紧密。项t中T型自由变量的集合fvT（t）的定义是标准的，根据函数f：X→Y（其中fvT（t）<$X），同时将f（a）代入每个a∈fvT（t）。方程我们在过程项上施加一组方程ECCS，如图1所二、这些只是使并行复合成为可交换的一一S·施威迈尔56def►→联系我们联系我们|联系我们| ∼12def（|- 天冬氨酸） （p|（q）|r = Cp|（q|（|-Comm） p|q = Cq|p（|- 单位） p|0 = Cp图二. CCS方程以0为单位的幺半群乘法-代数自由CCS-代数由代数一词给出. 我们只关心在过程中，即P类型的术语，并且不允许任何自由变量，除了N类型的变量，即自由名称。因此，我们在给定的集合X中使用具有自由名称的P型项的项代数TC（X），定义如下：TC（X）={t|t是类型P的CCS项，fvN（t）<$X，并且fvA（t）= fvP（t）=<$}和T<$C（X） ={[t]=C|t∈TC（X）}，其中[t]=C是t的=C-等价类. 通过这种方式，我们可以将TC（X）中的过程视为在上下文X p中给定的过程，其中p的自由名包含在X中。显然，进程代数CCS [24]，具有（强或弱）双相似性作为项上的同余，是一个（CCS，ECCS）-代数。我们可以将TC和T∈C推广到函子FinSet→Set：Forf：A→B，FinSet定义TC（f）：TC（A）TC（B）byTC（f）（t）=f。 同样对于TC-因为一个函子C集合是一个（离散的）共索引类别，我们可以应用Grothendieck构造[17]来获得（离散）纤维化。我们构造了T∈C，并利用CCS-代数结构将上纤维化为一个对称幺半群函子.定义3.1.类别“T”C是由下列定义给出的：• O b<$Pairs（A，p），其中A是有限集，p∈T<$C（A）. 我们也写一个小矮人。• 态射A态射f：（A，p）→（B，q）由函数f：A给出B满足T∈C（f）（p）=q，即 pf=Cq。 态射组成和恒等式继承自FinSet。• 张量积在物体上，张量积被定义为（A，p）<$（B，q）=A+B，p{in}|q{in}）给定态射f：（A，p）→（AJ，pJ）和g：（B，q）→（BJ，qJ），f∈g：A<$B→AJ<$BJ定义为f+g：A+B→AJ+ BJ。1不幸的是，这对CCS生物相似性来说并不十分有效;例如，a′ba'. b+b。a<$，but（a<$b）a/b（a）b+b。a）a/b。 在这种情况下，我们需要一种更强形式的双相似性，它尊重替换，例如融合演算的超双相似性[29]。S·施威迈尔57∅∫∫→∈∈›→张量单位I由对象（，0）给出。 结合性、单位和对称同构是从FinSet上的余积结构继承而来的。• 有一个明显的严格对称monoidal函子arCCS：T∈C→FinSet由CCS（f：（A，p）→（B，q））=f：A→B给出.函子arCCS是一个离散的自同构：给定一个箭头f：A→B，在T_∞C中，当（A，p）为有限集合时，T_∞Ca~b中存在唯一的一个解f的定义域为（A，p），由f：（A，p）→（A，p{f}）给出. 它从下面的图中的方程2的T∈C是对称的么半群，而arCCS是对称的么半群余纤维。命题3.2函子arCCS：CCCFinSet是对称么半群共纤维化。我们现在可以使用函子arCCS：ProcC→FinSet来定义上一节中定义的流程模型的实例Proc CCS。ProcCCS中的态射由图给出B不AsXp其中A，B和X是（通道名称的）有限集合，p是X中具有自由名称的CCS过程。 函数s和t描述了p对外界可用：每个名字a A代表p中的名字s（a），每个名字b B代表p中的名字t（b）。 p中那些没有被s或t映射到的名字是隐藏的。 的一些名字在X中的可能不会发生在p中，但可以在接口A和B.例3.3CCS处理a. x. b和x'。在Pr o c CC S中，p：{a，b，c}→{x，b}和q：{x，b}→{b}是两个相同的概念，如下图所示，其中还显示了它们的组成p;q：{a，b，c}→{b}。{二}{x，b}{x，b}x<$。b{a，b，c}c›→a{a，b，x}<$a.x.b{a，b，x}<$a.x.b|x′。b其中ca表示将c映射到a的函数，以及所有其他元素对他们自己然后，在组合p;q中，名称a对左手界面可用两次，作为a和c;名称b对左手和右手界面都可用，但也可以执行内部S·施威迈尔58→联系我们X是对外部世界隐藏的，并且只能用于内部通信。✷图4 CCS的进程代数我们现在将定义一个进程代数FCCS，它通过名称的限制扩展了CCS，以及一个用于等同名称的构造，类似于融合演算中的融合[29，16]。我们将建立一个范式结果，它表明每个过程都可以写成CCS-过程，带有一些“全局”融合和限制，类似于这将使我们能够在下一节中定义一个具有类似Proc结构的句法范畴，并最终证明它与ProcCCS同构。签名FCCS的签名是多排序绑定签名[13]。名称、动作和过程的类型为N、A和P;功能符号为in：（N）→AInputactionout：（N）→AOutputactionτ：（）→ASilent action0：（）→P零过程. ：（A，P）→ P前缀| : (P, P) → PParallel composition+：（P，P）→P非确定性选择ν：（[N]P）→P限制=：（N，N）→P融合其中符号ν：（[N]P）P表示ν是一个绑定运算符，它接受一个P类型的参数，并在该参数中绑定一个N类型的变量。在项t中T型自由变量的集合fvT（t）的定义是标准的。我们把自由名集合fv N（t）写成fn对于一个项t，其中fn（t）X，和一个函数f：XY，我们写t f，表示名称f（a）对a的避免捕获的同时替换。方程我们对FCCS项施加一组方程，如图3所示。我们写EFCCS的一组方程，和=F的同余产生它。方程是那些从CCS，和一些公理确保融合作为一个等价关系的名称，并融合和限制是在[16]中给出了一个类似的方程理论作为融合演算的结构同余S·施威迈尔59（|- 砷）（|- 通信）（|- 单位）（p|（q）|r = Fp|（q |r）的p|q = Fq|pp|0 = Fp（ν-通信）（νa）（νb）p=F（νb）（νa）p（v-范围）（（νa）p）|q= F（νa）（p|（q）如果a∈fn（q）（v/+-CommL）（（νa）p）+q=F（νa）（p+q）如果a∈fn（q）（v/+-CommR）p+（（νa）q）=F（νa）（p+q）如果a∈fn（p）（v/.-通信）α。（（νx）p）=（（νx）α.p）ifα/∈{x，x<$}（=/+-CommL）（=/+-ComR ） （ =-/-Comm）（[a = b] |p）+q = F[a = b]|（p +q）p+（[a = b] |q）= F[a = b]|（p + q）α。（[a = b] |p）= F[a = b] |α.p（=-丢弃）（=-Re）（νa）[a=b]=F0[a=a]=F0如果a/=b（=-Symm）[a=b]=F[b=a]（=-反式）[a = b]|[b = c]= F[a = b]|[a = c]（=-Subst-In）（=-替换-输出）[a = b]|在（a）中，p = F[a = b]|（b）.p[a = b] |out（a）.p = F[a = b] |out（b）.p图三. FCCS项的方程代数自由FCCS-代数由FCCS的代数项给出. 对于有限集合A，定义T F（A）为A中所有具有自由名s的FCCS -项的集合，满足α-等式：TF（A）={[t]α|t是ty peP的F CC S −项，fvN（t）<$X，且fvA（t）=fvP（t）=<$}。类似地，FCCS的术语代数满足方程EFCCS由模=F项给出，由yEFCCS 生 成 的 事 件：TF（A）={[t]=F|t∈TF（A）}.形式上，绑定签名的代数是预层FinSet→设置[13]。 我们可以让TF和TF 在预表中，定义对名称替换的态射则TF是自由FCCS-代数，T∈F是自由（F CCS，EFCCS）-代数。技术细节见[33]。融合构造背后的直觉是过程中名称的识别-融合在过程的自由名称上生成等价关系。那些只由融合的平行组合物组成的术语起着特殊的作S·施威迈尔60用。公理（=-Re）、（=-Symm）和（=-Trans）确保了这些项的=F-等价类一一对应S·施威迈尔61.∈通过等价关系，[a1=b1]|···|[an=bn]Participate {（a1，b1）， . ，（an，bn）}其中R是R的自反、对称、传递闭包。从现在开始，我们将经常识别A上的等价关系和TF（A）中融合的平行组合，并写作，例如。R|pforr[a1=b1]|[an=bn]|p，其中R={（al，bl）， . ，（an，bn）}n.融合的目的是标识进程中的名称。我们在下面的命题中将其形式化，该命题指出，由对应于融合的平行组合的等价关系相关的名称可以相互替换。命题4.1设p ∈ T F（A）且f：A → A使得（a，f（a））∈R，对a lla∈A.则R|p=FR|p{f}。具体而言，[a=b] |p=F[a=b] |p{b/a}。正规形现在我们将陈述一个定理，该定理建立每个FCCS-项都有一个标准形式，其中所有的融合和限制都在顶层。这一结果对于从基于FCCS的句法范畴到第三节的范畴ProcCCS的转换是至关重要的：对于TF中的范式，通过去除顶层融合和限制，我们得到TC融合和限制，然后建模的共同跨度。定理4.2存在一个自然变换nf：TF→TF，分量nfA为每个p∈TF（A）指定一个标准形，使得p = FnfA（p）<$R|（v X）pJ对等价的C∈R<$A2，有有限集合X使得A<$X=A，且有PJ∈TC（A + X）.此外，如果R|（νX）pJ= FS|（νY）qJ，其中pJ∈T C（A+X），qJ∈TC （ A + Y ） ， 则 R = S ， 存 在 一 个 双 射 σ ： X → Y 使 得pJ{[−]R+σ}=CqJ{[−]R+idY}.见[33]，见[34]。该定理包含几个陈述：1.正规形式R|（νX）PJ= Fp对每一项p∈TF（A）都存在. 2.函数nfA为每个p TF（A）指定一个这样的标准形式。它是通过使用图的公理3.将融合和限制提升到最高水平。3.第三章。的nf是自然变换的陈述意味着通过替换来保持正规形式。4.最后一个陈述涉及范式的唯一性：在范式中，等价关系R是唯一的，并且CCS项pJ是唯一的，直到=C，以及绑定名称X的重命名，并且A中的R-等价名称。S·施威迈尔62►→►►|►→···≤≤111nn例4.3我们举例说明FCCS项的标准形式是如何计算的.（vx）（a.x|（vy）（[x=y]|是的。c¯|（vz）（z. B|[c=z]）|[a=b]））=F（νxyz）（a.x|[x=y]|是的。c¯|z. B|[c=z]|[a=b]）（ν-Scope）=F（νxyz）（a.x|[x=y]|x′。c¯|C.B|[c=z]|（建议4.1）=F（νx）（a.x|x′。c¯|C.B|[a=b]）（=-丢弃）=F[a=b]|（vx）（a.x|x′。c¯|c.b）（ν-Scope）注意不同的融合是如何在限制之外被提升的：在[a=b]中，两个名字都是自由的，所以融合可以在限制之外被提升;在[c=z]中，c是自由的，z是绑定的，所以融合和对z的限制使用（=-Discard）被丢弃;在[x=y]中，两个名字都是绑定的5一个基于CCS的融合句法范畴从FCCS的术语代数，我们现在将定义一个结构类似于Proc的句法范畴，并证明它实际上同构于第3节中定义的ProcCCS进程代数TF中的项在上下文中给出（A表示TF（A）中的项）。 因此，与引言中的动机类似，态射p：AB是一个过程p，其接口（上下文）分为两部分A和B：A+B p。组合是由平行组合加上限制给出的。沿着类似的思路，在[12]中展示了如何将交互范畴构造为某些过程演算的句法范畴假设A 、B 和C 不相交，我们定义A+B p 和B+C q 的合成为A+C（νB）（p q）。然而，我们需要稍微小心一点，因为我们想在不相交的并集中识别一个名字的不同副本，例如，在余积A+A中A的两个副本，就像在Proc中定义恒等态射一样。 所以我们使用注入来确保所涉及的集合是互不相交的。我们在FinSet中选择余积，A1+···+An= in1（A1）<$···<$in n（An），其中n≥ 2。然后通过i中的i：Ai进行注射A1++ A n，对于每个1 in. 为了便于句法范畴的界定，我们对限制与融合进行了扩展操作，并替换为名称集如下。[g（A）=h（A）]d=ef[g（a）=h（a）]|···|[g（a））=h（a）]（νf（A））pd=ef（νf（a））·· ·（νf（a））pp{g（A）/f（A）}d=efp{g（A）， . ，g（an）/f（a1）， .. . ， f（an）}nS·施威迈尔63其中A={a1，...，和f：A→B和g：A→C是注射。我们把（ν idA（A））p写成（νA）p。定义5.1范畴Synt由以下数据给出• 对象：有限集合。• 态射：态射p：A→B是FCCS项A+B<$p，在T<$F（A+B）中被看作相等y。• 恒等式：恒等式idA：A→A由下式给出：A+A[in1（A）=in2（A）]• 复合：给定态射A+B<$p：A→B和B+C<$q：B→C，它们的组成p;q：A→C定义为：A+ C<$（νin3（B））（p{in3（B）/in2（B）}|q{in3（B）/in1（B）}），其中in1：B → B + C，in2：B → A + B，in3：B → A + C + B。def• 张量：在物体上，张量由余积给出：A<$B=+B。张量单位I被定义为空集：Id=e f。如果态射A+B<$p：A→B和C+D<$q：C→D，它们的张量积p<$q：A<$C→B<$D定义为：（A+C） +（B+D）p{inA B}|q{inCD}其中在AB和CD中是从A+B和C+D到（A+C）+（B+D）的明显注入• 结构同构：定义对称monoidal结构的自然同构定义为α ABC：（（A + B）+C）+（A+（B + C））[in1（in 1（in1（A）= in2（in1（A））]|[in1（in1（in2（B）= in2（in2（in1（B）]|[in1（in2（C））=in2（in2（in2（C）]ρA：（A+A） +A[in1（in1（A））=in2（A）]σ AB：（A + B）+（B + A）[in1（in1（A））= in2（in2（A））]|[in1（in2（B））=in2（in1（B））]S·施威迈尔64► → ► → ►→• Bimplant：Synt中的bimplant结构定义如下：A：A+（A + A）|[in1（A）= in2（in2（A））]ωA：A+ω0A：（A + A）+A [in1（in1（A））= in2（A）]|[in1（in2（A））= in2（A）]νA：+A0定理5.2 Synt是一个具有离散对偶的对称么半群范畴证据 证明了态射复合的恒等式和结合性公理。见[33]，见[34]，见[35]。身份设（A+B<$p）：A→B.i dA;p=（νin3（A））（[in1（A）=in2（A）]{in3（A）/in2（A）}|p{in3（A）/in1（A）}）=（vin3（A））（[in1（A）=in3（A）]|p{in3（A）/in1（A）}）=（vin3（A））（[in1（A）=in3（A）]|p{in3（A）/in1（A）}{in1（A）/in3（A）}）（建议4.1）=（ν in3（A））（[in1（A）= in3（A）]|（p）=（ν in3（A））（[in1（A）= in3（A）]）|p（ν-范围）=零|p（=-丢弃）=p（|- 单位）合成的结合性设（A+B p）：AB，（B+C q）：BC和（C+D r）：CD.为简单起见，假设A、B、C和D互不相交，并省略注入。（p; q）; r =（νC）（（νB）（p|（q）|r）的=（νC）（νB）（（p|（q）|r）（ν-范围）=（νB）（νC）（（p|（q）|r）（ν-Comm）=（νB）（νC）（p|（q|（r））（|- 砷）=（νB）（p|（v C）（q|（v-范围）=p;（q;r）✷S·施威迈尔65CCS}--{∈|联系我们我们现在将定义范畴ProcCCS和句法范畴Synt之间的结构保持翻译，并证明它们形成同构。从ProcCCS到Synt的翻译我们定义一个函子ps：ProcCCS→Synt。 在对象上，ps是单位：ps（A）d=e f. 设P：A→B在Proc中由图给出B不AsXp则定义ps（P）：A→B为A+B<$（νin3（X））（[i n1（A）=in3（s（A））]|[i n2（B）=in3（t（B））]|p{i n3}）其中i是A+B+X的注入。因此，函数s和t，使p的某些名称对外界可见这些融合对应于A+B上的等价关系，由s和t定义为（a，b）（A+B）2[s，t]（a）= [s，t]（b）。注意，在翻译ps（P）中，p的所有名称都是受限制的;然而，融合使那些由s和t可见的名称完全可见。例5.3考虑态射p： a、b、cx、b和q： x，bB在Ex。3.3.他们的翻译，和他们的正常形式根据Thm。4.2由{a，b，c，xJ，bJ}<$（νaJ JbJ JxJ J）（[a=aJ J]|[b=bJ J]|[c=aJ J]|[xJ=xJ J]|[bJ=bJ J]|aJ J.xJ J.bJ J）= F[a = c]|[b = bJ] |a.x.b{x，b，bJ}<$（vxJ JbJ J）（[x=xJ J]|[b=bJ J]|[bJ=bJ J]|xJ J. bJJ）=F[b=bJ] |x′。b然后，Synt中的组合物ps（p）;ps（q）由下式给出：{a，b，c，bJ}<$（vxJ JbJ J）（[a=c]|[b=bJ J]|a. xJ.b|[bJJ=bJ]|xJ J. bJJ）=F[a=c]|[b=bJ]|（vx）（a.x.b|x′。b）p的翻译;q是{a，b，c，bJ}<$（νaJJbJJxJJ）（[a = aJ]|[b = bJJ]|[c = aJJ]|[bJ= bJJ]|aJJ.xJJ.bJJ|xJJ.bJJ）一个简单的计算表明它的标准形等于ps（p）;ps（q）的标准形。✷S·施威迈尔66R||从Synt到ProcCCS的翻译现在我们定义一个函子sp：Synt → ProcCCS。在 对象上，sp是单位元：sp（A）d=e f。 设（A+B∈p）：A→B是Synt中的态射. 然后，由Thm。4.2，p= FR|（v X）（pJ），其中pJ在T C（A + B + X）中。 我们定义sp（A + Bp）为图B[in2（−）]RA[在1（−）中] （A+B）/R+X<$pJ{[−]R}为了翻译FCCS-过程p，我们根据Thm从p去除所有融合和限制。4.2、得到一个CCS-进程pJ。然后，我们通过一个co-span对p例5.4例3.3中过程p; q的ps平移为[a=c]|[b=bJ]（vx）（a.x.bx. （b）。使用sp将其转换为ProcCCS，我们得到{bJ}{a，b，c}{{a，c}，{b，bJ}，x}{a，c}. x. {b，bJ}|x′。{b，bJ}这在ProcCCS中等于p;q，通过同构f：{{a，c}，{b，bJ}，x}→{a，b，x};f（{a，c}）=a，f（{b，bJ}）=b，f（x）=x.✷这些例子说明了翻译的一些性质。事实上，这些转换在ProcCCS和Synt之间形成了一个保持同构的结构;这在下面的定理中得到了总结，其证明可以在[33]中找到。定理5.5函子ps和sp保持对称么半群和离散双紧结构，并在ProcCCS和Synt之间形成同构。这个同构结果使我们对第2节中的构造所获得的模型的性质有了一些了解当应用到CCS的片段，得到一个范畴，这是同构的句法范畴构造从同一个过程代数丰富的限制和融合。我们可以预期，任何这样的范畴Proc另一方面，结果意味着Proc的类型结构已经隐式地存在于FCCS这样的进程代数中。过程演算