70《理论计算机科学电子札记》68卷第1期（2002）网址：http://www.elsevier.nl/locate/entcs/volume68.html16页混凝土工艺分类克日什托夫·沃里特凯维奇LTI，瑞士联邦理工学院，CH 1015-Lausanne摘要本文提出了一个相当具体的看法，语义宇宙类型的并发计算。从一个以类型论为特征的范畴B中组织的集合和函数的概念开始，我们将伪函子的松弛切片F//Span（B）从一个自由范畴识别为B上的跨度和三角形的双范畴，这些跨度和三角形向上交换为具有可表示组件的松弛自然变换，作为语义宇宙展开的并发模型的一个范畴。通过类比，我们称F//Span（B）的对象为范畴转移系统，并证明了它们在赋予一系列日常现象（包括命令程序之间的消息传递）意义方面的相关性。我们确定的双范畴跨度跨度（F//跨度（B））的组织过程在一个基本的水平，并解决其平等的问题，阐述了互模拟w.r.t. 在这种跨度的腿给出的界面处可观察到的动作一个适当的模拟概念产生了一个开映射系统，通过它可以商Span（F//Span（B）），这是一个最初由Cockett和Spooner在其一般性中考虑的构造。 结果过程范畴Proc（F//Span（B），α）恰当地包含了著名的相互作用范畴SProc。1介绍设计为在有限步数后终止的程序和设计为在正常情况下不终止的程序之间的区别 可以合理地被认为是传统智慧。同样众所周知的是，后者在理论层面上更难处理，所以事实上这种区别是一个分水岭：迄今为止还没有统一的计算理论这样的东西。在90年代早期[2])来解决这个问题 虽然统一计算理论的希望并没有完全实现，但他们的开创性工作提供了关键的见解，导致解决PCF长期悬而未决的完全抽象问题的技术。[3])，演示了如何从并发产生的想法可能适用于顺序设置。他们在交互类别上的工作的进一步结果是展示了2002年由ElsevierScienceB出版。 诉 操作访问根据C CB Y-NC-N D许可证进行。沃里特凯维奇71类型的概念在当时主要是无类型的过程演算（参见[14]）。十年后，很多关于类型并发计算和相关问题的文章（参见。[9]）。从广义上讲，大部分的工作都是基于进程演算和它们的语义对应物标记为transi-tion系统。由于它们的语法简单性，进程演算具有澄清基本概念的优点，但对于更实际的目的，例如程序验证，它们的缺点是它们作为语义设备的非常精细的颗粒事实上，可以公平地说，一个过程演算，无论是类型化的还是非类型化的，都持续地提供了对所谓微观现象的描述。例如，用π表示可变列表需要大量的（π-）过程，这对于手头的任务来说是相当可观的（参见[19]）。由此可见，“真实世界”编程语言的π-语义需要包括一层又一层的编码，这反过来又承担了模糊问题而不是澄清问题的风险，如果这个想法被太过字面化的话当考虑标记转换系统来赋予这些编程语言意义时，也会出现类似的困难这个基本的观察使我们考虑一个稍微不同的方法来处理这个问题，因为我们将语义信息附加到表示控制点和控制路径的图的边缘。我们称这样的实体为范畴转换系统或cts 然而，在考虑相关实例时，存在着一个关键的差异，被包含在口号“控制导向”与“控制导向”中。面向数据的程序表示。事实上，当程序的意义由LTS体现时，通常附加到转换的语义信息将后者分类，例如在最简单的情况下是可见的或隐藏的，而与实际计算相关的信息则以显式形式附加到状态。不同的是，lts语义通常表示程序的数据路径，即状态对应于在给定执行点存储在程序变量中的具体值的另一方面，在我们的方法中，一个控制transi- tion被直接标记的信息执行的计算在一个内涵的方式，这是一致的事实，状态标记的类型信息。这就是类型化计算的概念如何进入这个设置的。当然，在可能附加到转换的语义信息的种类中存在相当大的自由度，因此通常所说的方法可以被视为关系语义的变体。后者的功能介绍至少可以追溯到Burstall等人在70年代初的工作（参见1970年）[7]）。然而，几十年后，Errington沃里特凯维奇72所需的技术机制涉及到一个松散的概念的态射（cf.[11]）。本文将伪函子的松弛片范畴F//Span（B）从一个自由范畴推广到B上的双范畴Spans（cf.[6])以及三角形，其计算到可再现的松弛自然变换平面，这是CTS的方便类别的原理 我们研究了cts之间的路径模拟，强模拟和弱模拟的推广（参见，[23]）。具体地说，只要（可能组成的）标记跨度一致，单个转移就可以被适当的路径匹配，这类似于弱模拟和强模饱和单子之间的关系，但更一般。表征路径模拟的几种可能性是（同前，）.在本文中，我们使用了（到目前为止相当标准的）开放地图技术（参见。[4])因为它们的拉回稳定性允许商Span（F//Span（B）），这是Cockett和Spooner最初考虑的构造（同前，）.由此得到的过程范畴Proc（F//Span（B），）恰当地包含了著名的相互作用范畴SProc。 （同前，）.本文的结构如下。第3节提供了直观的设置，并介绍了范畴转移系统的概念第3节介绍路径模拟及其各种属性。第4节致力于构建一个过程类别，适当地包括SPROC，而第5节的结论是建议的可能性，如何进一步推动在文件中规定的想法2范畴迁移系统标记转移系统的一个流行的表示由图组成，该图配备了从边到一组标签的函数以及局部内射性条件，即没有具有相同标签的平行边。在本节中，我们将这一观点扩展到范畴转移系统或cts[6]）。def设Span=Span（Sets），并在上下文中考虑命令式程序x：=20;while x>0 do x：=x-1 end[x：nat]它产生了一个伪函子，其赋值的图形部分由下式表示：沃里特凯维奇73IDN⇒KKKKK → L KL·aw1NIDNλx：天然20{1，2，.. . }··中西二号N N{0}λx：nat.x−1•N特别地，程序的位置与控制流程图的顶点是一对一的显然，赋值是一个伪函子，因为它在复合路径上的值是span的组合.可以证明，命令式程序1以这种方式产生伪函子（参见。[24]）。当然，这个例子并没有阐明采用一般跨度而不是简单关系的优点，事实上，后者适用于顺序程序。然而，正如我们将看到的，在这种设置这是解释互动的一个不可或缺的要素。控制流图也被认为是不确定的。这对应于延迟单子的作用，并且是表示平行组合固有的潜在交织的方便方式 。 因 此 ， 给 定 来 自 自 反 图 及 其 态 射 的 范 畴 RGraph 的 附 加 FEU ：RGraph→Cat，上述伪函子的形式为p：FG→Span。注意，我们可以省去显示上图中的控制流程图，因为它可以从标签部分推导出来，并且它实际上只显示标签，只要满足某些约定具体地说，为了总是能够推导出控制部分，我们在必要时复制标签，就像在讨论草图的文献中所做的那样（参见图1）。[5]）。此外，如果上下文允许，我们省略了显示来自非单元的单元跨度（在控制端）定义2.1Let是一个bicategory 中态射就是一张地图 右伴随命题2.2 Span中的态射是一个映射，当它的左腿是iso时。证明了Span中映射的iso类有一个以单位左腿为标准表示的Span。定义2.3设s，t：是 双 范 畴 和 中 的 lax 函 子 。 laxreptransform α：s t是一种具有可表示成分（即映射）的lax自然变换。定义2.4（Lax切片）设是一个双范畴。类别F//由数据给出1对于基本类型的问题，我们沃里特凯维奇74FGp1p2FkαpFLβ不→ ⇒ ⇒ 3→(i) 对象：从自由范畴到K的规范化伪函子(ii) 态射：给定s：FG→ K和t：FH→ K正规化伪函子，态射α：p→q是一个laxrep自然变换α：s → q。其中k：G→H是图同态(iii) 组成：β<$α=（l<$k，lβ<$α），其中α：s<$t<$Fk，β：t<$u <$Fl垂直分量lβ<$ α由分量粘贴给出我们把F//Span中的对象称为范畴转移系统或cts命题2.5 F//Span（B）有有限的极限，只要B有。命题2.5是正确的一般原因（cf.[16、22]）。我们指出的结构拉回在手的情况下，所涉及的伪函子具有相同的域FK。这样做不会失去一般性，因为总是可以按照×FHFKFGFKFHS跨度设F，G，H：FKSpan，α：FG，β：HG和FKf：ab. 然后我们有FaidGaαaGaβaHaidHa（Ff）1FF（Ff）2（Gf）1αfGf（Gf）2βf（Hf）1HF（Hf）2FbidFbαbGbβbHbidHa在f.设f（s，t）是具有拉回的范畴中具有公共余域的态射s和t的拉回数据（即由拉回对象和投影组成的三元组）。有一个系列(i) （QJ，qJ，qJdef （α，（Gf））1 2）=a1(ii) （QJJ，qJJ，qJJdef （β，（Gf））1 2）=a1(iii) （Q，q，q定义（qJ） ，qJJ<$β）（1 2） =def2f2f(iv) （R，r1，r2）（v）（第3条第1款及第2款）=αa，βa）def=（αb，βb）B中的拉回数据和拉回α沿β在f处的求值为沃里特凯维奇75<（Ff）1q1，（Hf）1q2>Q<（Ff）2q1，（Hf）2q2>俄.西注意这个跨度的边是由万有性质决定的考虑平行合成x：=5;c！（x+x）[x：nat |c：nat]||c？z;z：=z*z[z：nat|c：nat]其中进程以CSP方式通过类型化通道c：nat进行通信这种情况反映在NidN！ id！ NidNIDNαuIDIDNλx：天然5βidNidN！ id！ NidNIDNαvID！π1NN2！βmπNidN！ id！ NidNIDNαidIDIDNidβnλz：nat.zzNidN！ id！ NidN其中ααv=αid，λx：nat.x+x，βm=ππ1，π2π=id。它是一个形状图·→·←·在F//Span中，所以它的回调对象是N2IDN2<（λx：nat. 第五章） π1，π2>N2<π1，π1<$π2>{（a，（b，a + a））|a，b ∈ N}<π1，π2π2>N2IDN2<π1，（λz：nat.z<$z） 公司简介N2其对应于关于这种相互作用的直觉，并提出了相互作用过程的共同行为的概念，即极限（cf. [15]）。这沃里特凯维奇76→−→该示例还证实了这样的主张，即对于基于控制转换和沿着通信信道的值传递的类型化交互的研究，实际上一般跨度和松弛变换是更精确的工具（比严格的交换关系）远程过程调用或并发对象的表示可以沿着这些线构造（参见[24]）。我们将在第4节中更多地讨论语义问题3路径模拟和打开地图回到标记跃迁系统的经典设置，可以认为lts的动态是通过组成跃迁和记录诱导的动作序列来观察的（参见。[12]）。如果把一个转移系统表示为从底层转移图到单顶点图的同态，其中各个标签是自环，那么动力学就通过自由构造来实现可以说，模拟的概念本身就与动力学有着内在的联系，因为它在形式上被定义为强动力学，但动力学是话语的领域。当考虑强模拟时，这并不立即符合眼睛。设G是一个图，G是一个集合，G是环上的自由幺半群，- 是的 一个带标号的转移系统也可以表示为一个同态t：G到图的基本范畴 G的在这种情况下，强模拟的公式在静态和动态方面是相同的然而，弱模拟的经典概念已经可以按照上面建议的方式在动力学方面提出：如果我们允许标签从一开始就额外地将空序列ε作为值，那么模拟的静态和动态概念就不同了，后者对应于弱模拟。很明显，这个技巧通过一个bac kdoor，如x−→ayeingsimulatedbyyu−→εv−→aw的例子所示。上述考虑可能是有趣的，因为不可见的动作实际上是不可见的，但其本身只不过是经典弱模拟的另一种在本节中，我们详细介绍了cts之间的路径模拟然后，我们继续给出一个表征的路径模拟方面的一个适当的概念，开放的地图（同上。）.定义3.1设s：FG→Span和t：FH→Span为cts。从s到t的路径模拟是关系r<$G0×H0s. t。(i) IS（r）(ii) x（r）xJx−→fy∈FGxJfJYJ∈FH. y（r）yJ &s（f）= t（fJ）沃里特凯维奇77→ ⇒◦→→→ 3→考虑一下这些计划x：=7 [x：nat]和x：=5;x：=x+2[x：nat]以及相应的CTSidλx. 7N←−N−−→N和idλx. 5idλx.x+2N<$−N−−→N<$−N−→N从第一个cts到第二个cts有明显的路径模拟然而，请注意，如果我们仅根据单个过渡更保守地重新表述强模拟，则根本不会有模拟定义3.2函子k：B C是开的，只要任何B f：t（a）c在k下提升。cts的态射α：st其中α：st F h是开的，条件是α = id且F h在Cat中是开的。定理3.3设s：FGSpanand t：FH是cts的。 有一个从s到t i的路径模拟，有一个图R，一个满射图同态d：R → G和一个函子C：F（R）→ F（H）s. t。FRFG通勤和F d是开放的。FH不跨度定义3.2和定理3.4代表了著名的开映射主题的一个变体（前引书）。）.设置背后的计算直觉是d对s的计算进行最后，给出了路径互模拟的明显概念，我们得到了推论3.4给定s和t如定理3.3，存在从s到t的路径互模拟i.存在一个图和一对满射图同态d：R → G和e：R → H，从而在Cat和s. t中产生开映射。FdCS沃里特凯维奇78FdFe上下班FRFGFH不跨度4工艺类别路径模拟概念背后的直觉源于对基于状态和控制概念的程序的研究。因此，从自由幺半群到像Span这样的双范畴标签的转变也对应着从符号或外延的计算概念到显式或内涵的计算概念的范式转变。这对我们如何看待模拟有影响如前所述，路径模拟是经典强模拟的结果。然而，它在许多方面表现得像经典的弱函数。更严重的是，弱路径模拟的概念没有直接意义。然而，这不是静态与动态的问题，而是标签的问题，因为经典的弱模拟与字母表的特定解释密切相关，而事实上，经典弱模拟是基于一种非对称的可观察和无声行为的分类，因为米尔纳这种不对称性是弱模拟概念的核心，但当标签是由跨度体现的一般内涵计算时，这种不对称性就消失了，因为后者本质上不是沉默的或可观察的。尽管如此，仅仅基于计算维度的模拟概念在相互作用的上下文中可能是不够的，因为正如我们将看到的，可观察的转变可能与不可观察的转变进行相同的计算。因此，在这样的背景下，需要一种比计算给出的跃迁更粗糙的跃迁分类形式，至少区分可观察的跃迁和不可观察的跃迁（参见图1）。[18]）。在这里讨论的设置中，一个明智的选择实际上是区分不可观察的转换和在给定接口端口处可观察的转换。最初由Cockett和Spooner研究的技术（参见。[8，9]）本质上应用并提供了这样的分类，从而可以免除手工进行界面官僚主义 结果类别正确地包含交互作用类别SProc（同前）。）定义4.1范畴B中的覆盖系统是包含所有同构的态射的集合，并且是复合稳定和拉回稳定的。命题4.2（Cockett和Spooner）假设范畴B有拉回，并配备了覆盖系统χ。 Span（B，）给定的Span（B）S沃里特凯维奇79X1R1X2y1R2y2K∼∼通过将2-胞腔限制为χ之外的态射，是一个子双范畴。定理4.3（Pa r′e）Letbeabicat egory.由hom-categories中的连通分支给出的1-cel上的r_K是一个同余。定理4.3见[20]。由于覆盖映射是拉回稳定的，所以Span（B，n）中的局部拉回是从Span（B）继承的由此可见，defχ=Span（B，λ）具有令人愉快的性质，即当存在覆盖图的连接跨度时，两个跨度精确相关，如Xa rby使得视线范围内的所有东西都可以往返。这特别意味着，不需要明确给定的字母表来分类转换，因为正是因为在上面的图中所有的东西都是交换的，所以存在转换的内在分类，并且所讨论的过程相对于r.t.是双相似的这个分类。Cockett和Spooner称这种情况为χ-互模拟。命题4.4 F // Span中的开映射集合是一个覆盖系统。如第2节所述，Span（F//Span）中的1-细胞头部作为一个过程的执行，而脚是它的接口到外部世界，输入和输出分别2。这些分支决定了进程的行为，也就是说，如果一个转换是隐藏的，如果不是，那么在哪个接口端口它是可观察的。AC-相应地，互模拟等价于过程w.r.t.在上述意义上的行为考虑一下这些计划（* P1 *）x：=5;x：=x+2;c！(x)[x：nat|c：nat]和（* P2*）[]y：=7;c！（十）[]y：= 52.如果左边的resp。右边的一个用作输入RESP。输出接口但必须遵守约定沃里特凯维奇80[] y：=y+2c！(y)[y：nat |c：nat]用Dijkstra'a语言的变体编写[10]）。对应的cts这也是一个简单的路径互模拟，因为对应于c！(x)- 语句标记有与表示P1的cts所建议的相同的单位跨度NidN！IDIDNαuidλx：天然5NidN！IDIDNαvidλx：nat.x+2NidN！IDid！NαwNid！然而，考虑到该计划（*P1skip [x：nat|c：nat]及其代表CTSNidN！IDNidN！IDIDNαuidλx：天然5NidN！IDIDNαvidλx：nat.x+2NidN！IDIDNαwidIDNidN！ID在P1'和P2之间也存在简单的路径互模拟，因为skip -语句具有与c相同的标签！(x)但它不是一个互模拟，因为P1'在界面上的行为不匹配，正如在α w的两个版本之间的差异所看到的。这个例子演示了如何以内在的方式实现转换的分类，以及当转换也携带非平凡的comm时，这种分类是多么重要沃里特凯维奇81∃∃⇒→假设。因此，lts的情况当前设置与交互作用类别之间的关系是什么？我们证明了从Span（F//Span）中通过quoti-enting（cf.[9]）正确地包含了著名的交互作用范畴SProc。设Lts是标号转移系统及其态射的范畴事实上，Lts是Ltg的一个完全子范畴，Ltg是标号变迁范畴标签同态不需要忠实的图，即允许具有相同标签的并行转换设是由提升性质（在Ltg中）给出的覆盖系统，如定义3.2所示定义4.5设C是一个配备有覆盖系统χ的范畴。χ-回撤是C s. t中的平方。内接拉回的中介态射在χ中。命题4.6包含Lts→Ltg是反射的一部分，其中反射器r：Ltg → Lts折叠具有相同标签的平行边。进一步(i) r保留了前向回撤(ii) 单位给出的每一个自然平方都是一个回撤。命题4.6的第（ii）项是从单位存在于每一个对象的事实中得出的。因此，应立即制定项目（i）和（ii）的适当版本。（ii）为列入而搁置;为了国家。定义4.72-category id由数据给出(i) 对象：范畴对（C，χ）和其中的特定覆盖系统(ii) 态射：f：（C，χ）→（D，χ）s.t. f映射χ-拉回到χ-拉回上(iii) 2-胞腔：自然变换α：fg：（C，χ）（D，χ）s.t.自然性方格是双回撤。设J是对Lts的限制。命题4.8对命题4.6的回答是 id其中，Lts被视为配备有RLJ。定义4.9一个覆盖系统是左因子闭的，如果gf∈f∈g∈不难看出，这是左因子封闭的。设Proc（B，χ）跨度（B，λ）/λχ3。def=引理4.10（Cockett和Spooner）设fEu：（C，χ）→（D，χ）是id s. t中的一个附加函数。对于左因子闭的χ j和j，单位在每个对象处都是χ jχ，计数在每个对象处都是J。然后过程（C，χ）过程（D，D）3见同前。从 id 到Cat 的赋值是2-函子的沃里特凯维奇82⊆∈defJ设SProc=Proc（Lts，Lts）。 一个重要的结果在同前。 是SProc实际上等价于homemandatory相互作用范畴。根据命题4.6和4.8以及引理4.10，我们有提案4.11 SProc过程（Ltg，Ltg）仍然可以看出Proc（F//Span，）包含SProc。设f是一个集合（即一个“字母表”），并考虑由控制图的边分配到以下形式的跨度所诱导的子范畴Cltg F // Span：1← {α} → 1对于απ，态射是在鼻子上交换的三角形。 让J是对Cltg的限制。提案4.12㈠CltgLTG㈡程序（Cltg，J）过程（Ltg，Ltg）第（i）项中的类别的等价性很容易看出。至于第（ii）项，关键的观察是，由J-映射的跨度给出的路径模拟对应于转移图之间的强模拟（参见第3条）。因此，命题4.13设f ∈ Span（Cltg）和k ∈ Span（F//Span）是态射s.存在互模拟。则k∈Span（Cltg）.给定标号的性质，命题4.13的证明需要一个涉及开映射提升性质的后者是最后一条信息，定理4.14 SProc_Proc（F//Span，）所构造的过程范畴具有有用的标准结构。命题4.15（Cockett和Spooner）Proc（B，χ）是紧闭的，前提是B类具有有限极限并配备有覆盖系统χ.因此，Proc（F//Span）是紧凑封闭的，因此不仅适合于支持状态和交互概念的类型化编程语言的各种变体，而且适合于基于线性逻辑的类型化组合语言（松散地）。事实上，一个紧闭范畴验证了一个线性类型的结构，包括根岑[1][24]，其中设计了用于并发对象的组合语言5总结发言我们已经将松弛切片F//Span识别为一类称为范畴转移系统的并发模型，并证明了它们的相关性沃里特凯维奇83在给一系列日常现象赋予意义方面，包括命令式程序之间的消息传递我们进一步确定了跨度跨度（F//Span）的双范畴作为基本层次上的组织过程，并解决了它们的平等问题，表达为互模拟。我们认为，模拟应该作为一个运行时或动态的现象进行研究，并形式化的概念作为路径模拟。我们提供了一个抽象的表征的路径模拟的开放地图。它允许商跨度（F//跨度），应用Cockett和Spooner介绍的结构由此产生的过程类别Proc（F//Span）正确地包含了众所周知的相互作用类别SProc，它提供了更多的证据w.r.t.建筑的相关性5.1相关工作显然，第4节直接建立在罗宾·科基特和大卫·斯普纳的工作上。他们研究的具体案例（与我们不同）是基于可勾画的并发模型。Lindsay Errington在他的博士论文[11]中引入了一个更一般的范畴转移系统概念，他称之twisted系统。 Gi venacategoryofcomputt.函数shp与函子Sκ：Shp→Cat，ErringtonS是从κJ到范畴C的函子。 他的互模拟概念是用静力学来表达的，并使用开放映射技术来表征。Marcelo Fiore在[13]中考虑了由ulf函子体现的过程的广泛概念。ulf函子涵盖了从离散系统到连续系统的广泛过程。菲奥雷他的特点互模拟抽象方面的规范给定的开放地图。Robert Walters和他的合作者在[17]中考虑了Span（Graph）上的双范畴结构。在这一点上，作者需要承认他对后一部作品的了解非常有限5.2未来研究路径模拟的概念在w.r.t.中仍然是相当 计算，因为它区分的鼻子，即。 模拟控制路径需要进行与模拟控制路径相同的计算。推广这种设置将产生一种松散路径模拟的概念，其中判别标准将是2-cell，从而为通过细化规范进行程序开发等应用程序的相关设置铺平道路。一个相关的问题是2-细胞如何表现w.r.t.一个过程类的构造已知一般的2-细胞不被保存，但可能存在其类别的情况。这样的2-细胞将对应于由Pavlovi′cin[21]提供的保持互模拟的模拟。沃里特凯维奇84致谢我非常感谢罗宾·科基特去年冬天在卡尔加里访问期间提出的许多建议和讨论，也非常感谢克劳迪奥感谢教授。Petitpierre感谢他的鼓励和支持。感谢Christoph Sprenger和Lindsay Errington的善意和建设性的批评。我想对匿名推荐人的中肯评论表示引用[1] S. Abramsky，S. Gay和R.纳加拉詹并发的规范结构和命题类型。计算机科学讲义，1043，1996。[2] Samson Abramsky，SimonJ. Gay，and Rajagopal Nagarajan.交互作用类别和类型 化并发编程 的基础在M.Broy，编 辑，演绎程 序设计：1994 年Marktoberdorf暑期学校，NATO ASI系列F：计算机和系统科学。Springer，1994年。[3] Samson Abramsky Radha Jagadeesan和Pasquale Malacaria PCF（ExtendedAbstract）在TACS '94的诉讼Springer，1994年。[4] A.Joyal，M.Nielsen，and G. Winnigel.互模拟和开放映射。信息与计算，1996年。[5] 迈克尔·巴尔和查尔斯·威尔斯目的、三元组和理论。施普林格出版社，柏林，1984年。[6] 让·贝纳布。《数学笔记》第47卷，《生物学导论》。斯普林格，1967年。[7] R. M.伯斯托对具有断言、验证和模拟的程序的代数描述。ACM SIGPLANNotices，7（1），1972.[8] J. R. B. Cockett和D. A. 斯普纳 SPROC绝对。 在CONCUR 94：第五届并发理论国际会议，乌普萨拉，瑞典，计算机科学讲义。Springer-Verlag，1994.[9] J. R. B. Cockett 和 D. A. 斯普纳构建过程类别。理论计算机科学，177（1），1997年4月。[10] E. W.迪杰斯特拉程序设计的一门学科。普伦蒂斯-霍尔，恩格尔伍德，新泽西州，一九七六年[11] 琳赛·埃林顿扭曲的系统1999年，伦敦帝国理工学院计算机系博士论文沃里特凯维奇85[12] 吉安路易吉·法拉利，乌戈·蒙塔纳里，米兰达·莫布雷。具有参数观测的结构化变 迁 系 统 ： 观 测 同 余 与 最 小 实 现 。 Mathematical Structures in ComputerScience，7（3）：241-282，June 1997.[13] 马塞洛·菲奥雷过程的纤维模型：离散、连续和混合系统。IFIP TCS 2000会议论文集，第457-473页。Springer-Verlag，2000.[14] 西蒙·盖伊通信进程的线性类型。博士论文，伦敦大学，1995年。[15] J·戈根分类宣言。技术报告PRG-72，编程研究小组，牛津大学，1989年3月[16] J. W. 格雷Proceedings of the Conference on Categorical Algebra ，La Jolla ，chapter Fibered and Co Fibered Categories，pages 21-83.斯普林格，1966年。[17] Piergiulio Katis，Nicoletta Sabadini和Robert F. C.沃特斯Span（graph）：一个过渡系统的范畴代数。AMAST1997，第307-321页，1997年。[18] 南希·A Lynch和Mark R.塔特尔输入/输出自动机的介绍。CWI-Quarterly，2（3）：219[19] R. Milner，J.Parrow，and D.沃克移动过程的演算（第一部分和第二部分）。信息与计算，100：1[20] 罗伯特·帕雷。 简单连接的限制。 加拿大 J. 数学，1990年。[21] 达斯科·帕夫洛维奇过程和模拟的方便分类：模强双相似性。In D. Pitt等人，编辑，Category Theory and Computer ScienceSpringer Verlag，1995年。[22] A.塔尔莱茨基河M. Burstall和J.A.高根计算语义的一些基本代数工具第3部分：索引范畴。预印本，1989年。[23] 克日什托夫·沃里特凯维奇路径和模拟。 已接受在2002年CTCS会议记录中出版。[24] 克日什托夫·沃里特凯维奇进程范畴中的组件与同步通信。博士论文，瑞士联邦理工学院，洛桑，2000年。
我的内容管理
展开
