高层次事务重写逻辑模块化方法的研究与应用

--理论计算机科学电子笔记71（2003）网址：http://www.elsevier.nl/locate/entcs/volume71.html20页重写逻辑中的平铺事务*罗伯托·布鲁尼a，1岁，何塞·梅塞格尔b，2岁，乌戈·蒙塔纳里a，1岁a意大利比萨大学计算机科学系b美国伊利诺伊大学厄巴纳-香槟分校计算机系摘要我们提出了一个模块化的高层次的方法来规范的事务重写逻辑，其中的操作和抽象的观点是相关的瓷砖理论和重写理论的类别之间的适当的解释。关键词：瓦片逻辑，重写逻辑，范畴理论，事务，零安全网，Petri网。1介绍万维网的巨大增长增加了对全球计算应用的需求，其中数据流和移动过程的“编排”是一个虽然在Web上同步通信是不现实的，因此异步正式模型是首选，许多应用程序通常需要一个协调层之间的分布式组件，设计和实现分开（例如，在电子商务或在线拍卖系统）。为此目的，像Java和JavaSpace这样的平台利用集中式事务管理器（TM）来保证所谓的ACID原子性、一致性、隔离性和持久性属性（例如，如果事务中止，则必须恢复一致的配置）。然而，TM例如：（1）缺乏正式的抽象模型;（2）运行TM的服务器上的繁重任务过载*研究得到IST-2001-32747 Project AGILE、意大利MIUR Project COMETA和ONR Grant N 00014-02-1-0715的支持。第一作者还得到了意大利CNR信息科学和技术研究奖学金以及伊利诺伊大学厄巴纳-香槟分校计算机科学系的支持。1电子邮件：bruni，di.unipi.it2电子邮件：meseguer@cs.uiuc.edu2003年由Else vierScienc e B出版。V. 操作访问根据C CB Y-NC-N D许可证进行。90BRUNI，MESEGUER和 MONTANARI91Pµ{}|−→−→µ（actµ）µ结构叠合. P−→PPµPJ（）（ass）P|（Q|R）（P |Q）|R−→µP|Q −→ P J|Qlparµ（sym）P |QQ|PP−→µQ|−→PJ（rparµ）Q|P J（id）P |0元JQQJ（）重写规则¯P|Q −→ P J|Q J（同步）P|-是的QP|Q图1. LTS与简化语义说明。在本文中，我们提出了一个高层次的规范形式主义的分布式事务与元理论的方法，其中两个视图是不同的，但正式相关：（i）一个抽象的观点，事务被视为原子活动，可以独立于系统的其余部分发生;(ii)一个细化的视图，其中协调层是明确的。这两种观点反映了定义许多演算的动力学的两种主要方式：（a）通过定义一个重写（或一个典型的例子说明了（a）和（b）的不同风格，它是一个带有非活动进程0、动作前缀μ的初等CCS类微积分。（以行动为基础）一阿（二）平行组合，其两个语义是图1中的比较（实际上，必须禁止在操作前缀下的减少）。假设上述演算中的过程P用于对用户Q1和Q2愿意通过其在某个信道a上通信的网络进行建模。然后LTS语义的SOS规则指定通信必须如何通过网络传播，而重写语义仅假设网络可以以Q1和Q2可以本地“握手”的方式重新排列由于它们作为规范和逻辑框架的通用性，我们选择重写逻辑和瓦片逻辑作为对分别见上文第㈠和㈡重写逻辑（RL）[13]不仅支持归约范式，而且还利用重写的证明项作为一等公民，赋予系统计算代数，可以进一步抽象以表征行为等价。此外，证明术语精确地表征并发计算。这些特性使RL成为并发、并行和交互的表达语义框架，并用于表示其他逻辑。Tile logic（TL）[10]是RL的扩展，它将LTS最有趣的功能和约简语义联系起来。瓦片逻辑利用了并发系统的三维视图：水平维度（空间）用于状态和组件的建模;垂直维度（时间）用于标记步骤的建模;第三维（并发性）用于活动的分布和重新分配。PBRUNI，MESEGUER和 MONTANARI92源这种关注点的分离使得有可能简单地通过微调空间和时间元素的代数结构并固定它们的相互作用来选择不同风格的TL。TL最近的应用涉及逻辑编程的交互视图[7]和以因果和空间方面为中心的并发语义的元理论[6]。 本文提出了一个更进一步的应用领域，即分布式事务的语义。还有两个原因促使我们的选择。第一个动机是，在合理的情况下，TL规范可以被转换为可执行的RL规范，通过利用反射和元策略[8]来控制重写（参见例如[15，4，2]）。由于事务本质上是“选择的”计算模式，因此它们可以直接转换为元策略，从而弥合了精炼和抽象级别之间的差距。第二个原因是，最简单的瓦片理论（称为零安全网），其中的配置和观察都是基本元素的多集，已经被证明可以用并发事务的概念扩展普通P/T Petri网（这只是重写理论的特例因此，将这种基于网络的交易账户推广到任意瓦片和重写理论，产生了一种高级的和表达性的规范形式主义，该规范形式主义适用于网络建模不适合或需要复杂编码的大范围应用。零安全网的主要参考文献是[5]。除了称为稳定的普通位置之外，零安全网还配备了零位置，这些零位置在任何稳定标记中都是空的;事务是可以使用零令牌作为触发器的并发计算，但仅定义了稳定标记之间的演化。零安全网N的抽象视图是一个普通的P/T Petri网，其库所是N的稳定库所，变迁是N的基本事务。零安全网与其抽象网之间的关系用范畴核反射表示论文[3]提出了零安全网的分布式实现，其中集中式TM被完全分布式提交算法取代。注意，解释器的任务是本文提出的思想可以作为更一般的分布式事务算法的基础实际上，我们将零安全网和P/T Petri网之间的关系推广到瓦片理论（系统设计层）和重写理论（抽象层），以定义事务的一般框架，其中：（1）系统的低层视图由在事务的ACID属性下运行的瓦片机给出;（2）系统的高层视图是由（精炼）瓦片理论生成的普通重写理论，使得瓦片机的每个并发事务都有一个重写规则。我们的主要结果是定义了重写理论范畴和具有适当精化morphism的tile理论范畴之间的共反射。这导致TL和RL是如何相关的概念澄清，并给出了一个忠实的描述重写规则模型协调所需的有效的通信机制。作为一个例子，我们给出了一个正式的理由，声称在通过从LTS的约简语义图1中有一个损失的信息的方式，实现同步BRUNI，MESEGUER和 MONTANARI93→⊗→⊗→⊗论文的结构。在§ 2中，我们确定了重写理论（§ 2.1）和瓦片理论（§ 2.2）的范畴表示。在§ 3中，我们回顾了零安全网的理论和在[5]中进行的代数构造。在§4中，我们将零安全方法扩展到瓦片，研究计算模型和抽象模型的代数构造。值得注意的是，零安全网的构造现在只是本文所发展的更一般理论的一个特例。我们的技术在§ 5中通过一个简单的例子来说明。结论见§6。附录A和B分别回顾了关于双范畴和双范畴的一些初步概念此外，附录B结尾的两个表格总结了本文中讨论的所有类别和所有结构。2计算广告和计算2.1重写逻辑和2-computadsRL的主要成分是配置的签名，结构公理集E，以及在同余类[t]E（的）上重写规则集RE）中的公理的模。然后，证明项通过简单的推理规则形成由R中的重写生成的carbohydr 2-范畴（参见例如。[12、13]）。在这里，我们通过在（严格）monoidal范畴C中取配置来给出重写逻辑的更抽象的表示。我们假设读者对范畴理论有一定的了解。定义域d（f）=a，余域c（f）=b的箭头f记为f：ab。我们用对象名称本身表示每个恒等式，用;表示ar-row合成（按图解顺序），用，表示monoidal张量积，用e表示单位元素。因为我们总是考虑严格monoidal范畴和函子，下面我们将省略“严格”一词标准的情况是把与方程理论（E，E）相联系的Lawvere理论L，E作为C。粗略地说，carnival范畴L，E有下划线的自然数作为对象（n表示一个有n个有序变量的集合，我们使用标准名称x1，...，x n），并且项[ t ] E（的等价类）的元组作为箭头（f：nm是x1，.，xn），其中组成由术语替换给出。L，E的乘积给出了10-根据配置对产品进行排序。我们使用从[18，19]借来的术语2-computads来描述重写理论的这种抽象风格。定义2.12-computad是一个4元组C=（C，R，l，r），其中C是配置的monoidal范畴，R是一组规则名，l，r：RC是表示每个规则r∈R的左侧和右侧的源函数和目标函数，约束条件为：（1）d（l（r））=d（r（r）），（2）c（l（r））=c（r（r））。注意，如果C只有一个对象（单位e），那么序列合成与张量积（通过的么正性和函子性）一致，并且定义2.1的约束（1从计算的角度来看，C中的箭头是系统的配置，它可以并行（）和顺序（;）组合。域BRUNI，MESEGUER和 MONTANARI94∈⊗∈⊗∗·r#∈→→f：a→b∈C（id）f：ffr∈R（gen）r：l（r）r（r）第一名：f1米1，第二名：f2米2（标准杆）1i：fi∈gi，i=1， 2，c（f1）=d（f2）（hseq）1：f中文（简体）(a) 推理规则。图2. rw（C）中的细胞。(b) 方程和codomain分别对组件的输入和输出接口进行建模规则r R模拟从配置l（r）到r（r）的基本约简。每个还原r可以独立于l（r）所在的上下文发生，因此任何配置f;l（r）;g可以通过应用r重写为f;r（r）;g。此外，鉴于两个规则r1，r2R和配置l（r1）; l（r2）和l（r1）l（r2），则同时约简是可能的，导致r（r1）; r（r2）和r（r1）r（r2）的值。这产生了一个2-范畴，其单元是并发计算。定义2.2给定一个2-computadC=（C，R，l，r），monoidal 2-categoryrw（C）具有与C相同的对象和箭头，以及由图2（a）中的推理规则定义的单元模图2（b）中的monoidal 2-category的定律（当-方程的两边都是正确定义的单元）。根据从左到右水平组合配置和从上到下垂直计算的图形惯例，组合和分别称为水平和垂直。例如，重写r，具有参数f并且在上下文g内，由证明项frg表示：l（r）afz，d（l（r））布雷尔r（r）c（l（r）） g，，zb定义2.3（C1，R1，l1，r1）和（C2，R2，l2，r2）之间的2-计算态射是一对（C，R），其中C：C1C2是一个monoidal函子，R：R1R2是一个函数，使得对任何rR1：（1）C（l1（r））=l2（R（r））和（2）C（r1（r））= r2（R（r））.我们让2Comp是其对象是2-computad且其箭头是2-computad态射（具有明显的恒等式和成对组合）的范畴。此外，我们用2Compc表示2Comp的全子范畴，其对象是2-具有交换monoidal类别的配置的计算（即，其中张量积是可交换的）。刚果民主共和阿吉耶====f·= a= fg=BRUNI，MESEGUER和 MONTANARI952-计算对象C通过一个附加函数与它们的计算rw（C）BRUNI，MESEGUER和 MONTANARI96−→−→→→初始输入接口Z，Z初始输出接口u最终输入接口吉夫tz，最终输出接口图3. The tile said：v命题2.4设2 MCat是monoidal 2-范畴（作为对象）和monoidal 2-函子（作为箭头）的范畴。明显的遗忘函子U2：2MCat →2Comp有一个左伴随F2：2Comp → 2MCat，其中F2（C）'rw（C）。2.2瓦片逻辑和D-计算瓦片扩展了普通的重写规则，在系统演化过程中可以改变输入和输出接口它们的变化方式用垂直类别中的箭头表示更一般地，垂直箭头模拟接口之间传递的信息。 从图形上看，这相当于表示规则为矩形，因此得名瓷砖。图3中的图块被写为：s ut，v并且表明初始配置S可以演变为最终配置T，当触发U由连接到S的输入接口的组件提供时产生效果V。箭头s、u、v和t形成了罗盘的边界，通常由四个主要罗盘点的首字母表示（例如：n（n）=s）。定义2.5D-计算是一个7元组D=（H，V，T，n，s，w，e），其中H是配置的monoidal类别，V是观测的monoidal类别，T是一组瓦片名称，n，s：TH和w，e：TV是（二维）源函数和目标函数，分别表示初始和最终配置，触发器和每个瓦片的效果r∈T，约束条件为：(i) 范畴H和范畴V具有相同的对象;(ii) d（n（r））=d（w（r）），对任意r∈T;(iii) c（n（r））=d（e（r）），对任意r∈T;(iv) d（s（r））=c（w（r）），对任意r∈T;(v) c（s（r））=c（e（r））.直接的是，任何2-计算只是一个特定的D-计算，其垂直观测范畴V是水平范畴H中对象的离散范畴（通过取C=H和l=n和r=s）。注意，图块重写不能应用于任意上下文中。例如，仅当瓦片r的触发w（r）可以与f协调并且瓦片r的效果e（r）与g协调时，瓦片r才可以应用于f;n（r）; g：afz，d（n（r））n（r），zc（n（r））gz，bw（r）re（r）？z，d（s（r））s（r），zc（s（r））z，？像重写规则一样，平铺可以水平、垂直和并行组合以生成更大的这三种BRUNI，MESEGUER和 MONTANARI97组合物如图4所示。由于BRUNI，MESEGUER和 MONTANARI98z，z，u1 2⊗1 2→ →→快，快，快阿利什阿斯图里亚斯◦什么？z，什么？，z？，，z，z什么？z，图4.水平、平行和垂直瓷砖组合。u wt：a→b∈H（hid）$1：s1−w→t1，：s2−→vt2（hseq）一t：t−→bt1u1u2u：a→b∈V（vid）：s-v→1 q，2：q−v→2t（vseq）uu：a−→ubu;u1·u1u2r∈T （gen） $1：s1−v→1t1，：s2−v→2t2（面值）w（r）r：n（r）−e（→r）s（r）乌乌1图5.在tl（D）中的细胞。由于空间的限制，我们参考文献[9，15，2]中关于普通双范畴和monoidal双范畴的理论为了读者的方便，在附录A中回顾了一些基础知识。粗略地说，monoidal双范畴的元素是类似于图3中矩形的单元，有两个连续的组合（水平和垂直）和一个张量积，所有的运算都是互函的。定义2.6给定一个D-计算D=（H，V，T，n，s，w，e），monoidal double范畴t1（D）有水平1-范畴H，垂直1-范畴V，和（double）由图5中的推理规则定义的单元，模么半群双范畴的定律[2，15]详细信息。定义2.7 D 1 和 D 2 之 间 的D-计算态射是三元组（H，V，T）使得H：H1H2和V：V1V2是么半群函子，T：T1T2是一个函数，使得：(i) 函子H和V在对象上重合;(ii) H（n1（r））=n2（T（r）），对任意r∈T1;(iii) H（s1（r））=s2（T（r）），对任意r∈T1;(iv) V（w1（r））=w2（T（r）），对任意r∈T1;(v) V（e1（r））=e2（T（r）），对任意r∈T1.我们让DComp表示其对象是D-计算且其箭头是D-计算态射的范畴。此外，我们用DCompc表示DComp的全子范畴，它由构型和观测都是交换monoidal范畴的D-计算组成。一个D-计算D与它的com的monoidal双范畴t1（D）BRUNI，MESEGUER和 MONTANARI99⊕∈→→ ⊕ ⊕ →通过一个附加条件。命题2.8设DMCat是monoidal双范畴（作为对象）和monoidal双函子（作为箭头）的范畴。明显的健忘函子Ud：DMCat → DComp有一个左伴随Fd，其中Fd（D）'tl（D）。3审查零安全办法P/T Petri网是一种图，它的节点集是空间S上的自由交换幺半群S，它的弧称为变迁。Petri网态射是一种图态射，它还保留了标记的幺半群结构（即节点分量是幺半群态射的图态射）。范畴Petri有Petri网作为对象和Petri网态射作为箭头。由于Petri网可以看作是一个具有唯一对象（单位e）的monoidal范畴，其元素为箭头，合成由m;MJ=MMJ给出，因此P/T Petri网可以通过将变迁直接转化为重写规则而被看作是2-计算.事实上，每个m S都精确地定义了一个位置的多重集合（标记），并且任何具有预设m和后置mJ的转换t都可以被视为重写t：m mJ。请注意，重写可以（并发地）应用于任何更大的多集合（参见[16]几种网络的RL命题3.1范畴 Petri同构于 2Compc(and因此是2Comp），其对象是形式为（S， T，l，r）的2-计算。零安全网[5]是一个P/T Petri网，其位置集S被划分为两个不相交的稳定位置L和零位置Z的子集，并且其转换以事务方式进行，如下所述。关键思想是，转换只能作为从稳定标记（即，元素的L）稳定的标记。从一个稳定的标记开始，网络通过触发可以获取两种标记的转换来计算。在每次触发之后，只有后集合中的零令牌可用于连续的触发：后集合中的稳定令牌将仅在提交时对系统可用，此时事务中没有任何零令牌。这种假设引入了一种可以在分布式语言中实现的转换之间的协调机制[3]。虽然零令牌是有用的规范级建模协调，在抽象层次上的系统可以被看作是一个普通的P/T Petri网，其地方是系统的稳定的地方，其过渡是基本的事务。其优点是零安全规范通常比其抽象视图更简单和更自然（有限规范可以产生无限多个事务）。此外，抽象视图可以通过下面从[5]回顾的分类附加来定义例如，让我们考虑具有两个稳定位置a和b的零安全网，零位置z和两个转移t1：a z b和t2：b z a。然后，如果初始标记是a，则不能执行任何事务，因为由t1的激发产生的b中的令牌将不能立即可用，并且因此t2将不会被启用。BRUNI，MESEGUER和 MONTANARI100⊕∗⊗→→∨∗→联系我们→→⊕ →⊕⊕ ⊕ ⊕∗⊗∗∗⊗∗⊗ ⊕ ⊕ ⊕→∗⊕ →⊕⊗ ⊕ ⊕ → ⊕ ⊕相反，如果初始标记是b，则可以首先触发t1，然后可以将最初存在于b中的令牌与t1产生的z中的令牌一起使用，以启用t2并关闭事务（其提交释放a和b中的新令牌）。设ZPetri是零安全网的范畴，以及它们之间明显的图同态（保持对稳定和零的位置划分），另一个条件，不同的零的地方有不相交的多集作为图像。第一步是定义一个零安全网的范畴HCatZPetri，它的变迁集有一个（交换的）monoidal操作，一个水平顺序操作（仅在零位置上连接，并表现为稳定的前和后集上的并行组合），以及恒等式，由合适的公理表示。HCatZPetri的态射是保持所有附加结构的零安全网态射水平组合允许构建利用零令牌流的交易在ZPetri和HCatZPetri之间存在一个附加项。我们让Z：ZPetriHCatZPetri表示自由函子。第二步是基本事务的特征化：给定一个过渡在HCatZPetri网的抽象中，我们说，如果它不能被分解为另外两个非平凡变迁的并发执行，则具有m和m j稳定的n：m m j是素数。形式上，如果= e，则是素数，并且如果每当=12时，则1=2=e。给定一个零安全网N，Z（N）中的素箭头被显示为精确地模拟N的（基本）事务，定义抽象网的实现因此，R：N1的影响是病态的N2是一个零安全网态射R：N1Z（N2），它将转换映射到素数箭头或N2的转换.在上面讨论的例子中，我们有t1t2：aBzBza，while t1 t2：aBBa（t 1产生的z中的令牌被t2消耗）。 此外，t1t2是一个质数箭头（唯一的一个），而例如（t1t1）（t2t2）：a b a bb a b a不是质数箭头，因为它可以分解为（t1t2）（t1t2）。 因此，抽象网有两个位置（a和b）和一个变迁t：a b b a，它可以通过细化态射映射到素箭头t1t2。(We更详细的例子参见[5]第三步是定义零安全网的范畴N（如对象）和细化态射（如箭头）。事实上，细化态射可以通过保持素性的提升来组合。范畴Petri是Petri网的一个共反射子范畴。此外，右伴随AZ：Z-N Petri网映射零安全网到它们的抽象对应物，并且伴随的计数映射抽象网的转移到它们表示的事务构造的性质表明Z和Az是4零安全重写理论我们首先详细解释了零安全网和瓦片之间的类比，然后将[5]中的构造推广到瓦片并重写理论。BRUNI，MESEGUER和 MONTANARI101∈⊕]“×∈⊕−→11e−→e·⊕⊕⊗∗4.1零安全网作为瓦片正如在第3节中所指出的，空间S上的自由交换幺半群S可以看作是一个具有唯一对象e的范畴。此外，如果L是零安全网的稳定库所集，Z是零安全网的零库所集，则很容易看出（L Z）<$L<$Z<$。我们已经注意到，P/T Petri网只是形式为（L，T，l，r）的2-计算，其中l和r是前集函数和后集函数，并且网态射的概念与2-计算态射的（提案3.1）。类似地，零安全网可以被认为是D-计算（L，Z，T，n，s，w，e），其中：（i）t T的预设是n（t）w（t）;并且（ii）t的后集T是s（t）e（t）。然后，可以很容易地验证，附加的代数HCatZPetri的对象中的转换的结构仅由瓦片的普通标识、并行和水平组成给出（但注意，这里的并行组合物是可交换的）。 例如，如果ai，bi是稳定的地方，z是零地点，t：aezb1是从a1到b1<$z的跃迁，t2：a2−→zb2是一种过渡从a2→z到b2，则它们的水平组成t1→t2：a1;a2eb1;b2形成a交易从1a2=a1;a2到b1b2=b1;b2.然而，在态射级别，DComp比ZPetri更宽容，因为两个不同垂直箭头（例如零位置）的图像不一定是不相交的多集。这个属性对于在箭头合成的CNON中使用的精化形态的提升是至关重要的。因此，ZPetri严格包含在DComp的完整子类别中，其对象是以下形式的所有D计算（L，Z，T，n，s，w，e）。为了使对应更精确，我们可以限制D-计算态射以满足不相交图像性质的扩展概念定义4.1从D1到D2的D-计算态射（H，V，T）是不相交的，如果函子V在对象上是单射的，并且忠实于箭头。我们称ZComp为我们用ZCompc表示ZComp的满子范畴，其对象是交换么半群范畴上的D-计算和不相交的D-计算态射。命题4.2范畴ZPetri自然同构于ZComp c的完全子范畴，其对象是形式为（L，Z，T，n，s，w，e）的D-计算。如构造t1（D）所例示的，D-计算具有标准的水平和平行组合，因此我们可以定义范畴HCatZComp，其中：（1）对象是D-计算，其瓦片集合具有monoidal操作和水平组合，其中水平组合具有用于观察的水平恒等式（但既不考虑配置的垂直组合也不考虑配置的垂直恒等式）;以及（2）箭头是表示所有附加结构的不相交D-计算态射。我们让HCatZCompc是HCatZComp，其D-计算具有可交换的并行组合。命题4.3范畴 HCatZPetri同构于HCatZComp c，其对象是形式为（L，Z，T，n，s，w，e）的D-计算。BRUNI，MESEGUER和 MONTANARI102CB∗∗⊗命题4.4在ZComp和HCatZComp之间有一个明显的附加功能，它构建了瓦片的水平计算。我们让D表示自由函子。类似地，在ZComp c和HCatZComp c之间有一个附加函数，我们让Dc表示相应的自由函子。然后，函子和明显嵌入的图ZPetriZz，HCatZPetri˛˛'ZC o？mpcz，HCat Z？公司简介D自然同构（natural isomorphism）在第4.2节中，我们展示了如何推广精化态射的概念，使得Petri（抽象视图）和ARBN（规范视图）之间的共反射可以适当地扩展到重写和瓦片理论。4.2从切片到事务重写规则这个想法是，从一个给定的配置开始，双计算可以开始重写它，产生必须在事务的继续中协调的观察。启用的重写可以并发执行。当所有动作都协调好后，事务就完成了（全局触发器和效果必须是标识，因为事务可以单独执行）。在抽象层次上，每个事务都是一个普通的重写规则。瓦片的二维表示标志着系统配置和重写协调中涉及从概念上讲，这类似于零安全方法，抽象视图可以通过基于细化态射的一般化代数结构来定义。第一步是推广素性的概念，从而刻画基本事务。定义4.5给定HCatZComp中的D-computad的tile，我们说，prime如果它不能被分解为两个其他非三个小瓶瓷砖。对于正规y，n：s−→at，/=e是素数，如果a和b是恒等式，=不幸的是，上述约束不足以保证主箭头表示原子活动。事实上，假设1=12，1和2互质，2的触发器（以及1的效果，必须相等）是一个标识箭头，那么假设1和2在相同的事务中交互是不正确的（除非1或2是对象标识）。区别在于零安全网的情况是由于在HCatZPetri中，如果如果= 12且2的触发器是e（唯一可能的恒等式），则可以应用=12为了保证原子性，我们必须避免基本事务之间任何可能的嵌入。BRUNI，MESEGUER和 MONTANARI103−→b2˜→ →˜→- 是 的- 是 的Σ→˜˜⊗⊗∗ ⊗ ⊗∗∗⊗定义4.6A prime tile1：s的11−b→1t1是初等的，如果1=t2=1= 2= a2.由于和是HCatZPetri中用于组成瓦片的唯一操作，因此上下文1（u1u2）2（其中u1和u2是合适的水平身份）对将事务嵌入另一事务的更一般情况进行建模。当然，像2这样的对象的身份不被认为是事务，并且可以在基本图块中使用。定义4.7计算细化态射M：D1D2是一个不相交的D-计算态射M：D1D[D2]，它将瓦片发送到D 2的瓦片或D [D2]的元素。引理4.8给定一个计算加细态射M：D1→D2，用M：D [D1] → D [D2]表示它在HCatZComp中通过伴随D的唯一扩张.然后，M保持基本瓦片。证明（草图）我们必须证明，如果M在D[D1]中是初等的，那么M（M）也是初等的。我们将m的表示固定为n个瓦片的水平组合，其形式为u iiv i（i=1.）。n，其中，nM（v）= M（u1）<$M（v1）<$M（v1）<$. M（u n）不是初等的，那么，通过利用不相交的D-计算形态的忠实性，也可以证明是非初等的，与假设相矛盾。(The关键事实是每个M（mi）必须是D 2的基本瓦片，由元素度m表示。由于引理4.8，两个计算加细态射M1：D1的合成 D2和M2：D2 D3被定义为态射M1; M2，它是 又是一个计算细化态射。因此，连同明显的恒等式，计算精化态射形成一个范畴。定义4.9范畴RComp有D-计算作为对象，计算细化态射作为箭头。网和计算机之间的类比现在可以充分利用，导致本文的主要结果。定理4.10范畴2Comp是RComp的一个上反射子范畴。证明（草图）首先，我们表明，明显列入I的2Comp到RComp它是完整的和忠实的。 如果D是2-计算的，则D[D]的基本箭头是只是重写规则的D。 这意味着，给定任何2-计算D1和D2，任何计算加细态射都是2-计算态射。另一方面，很明显，任何2-计算态射也是计算细化态射，因为它将转换映射到转换。其次，我们必须证明I有一个右伴随Ad。给定一个D-计算D=（H，V，T，n，s，w，e），设Ad[D]BRUNI，MESEGUER和 MONTANARI104→D一个c1µ⊗11⊗µ⊗¯actµ：µ。x1−→µx1 lparµ：x1|x2−→µx1|x2rparµ：x1|x2−→µx1|x2com数量：x1|2−→1 X1|X2图6.图1中SOS规则的切片是具有D的相同水平1-范畴的D-计算，由V的对象给出的离散垂直1-范畴，以及作为瓦片的D[D]的所有基本瓦片（具有明显的边界）。由于Ad[D]的垂直1-范畴是离散的，显然它的瓦片是普通的重写规则，因此Ad[D]只是一个2-计算的。通过将每个计算细化态射M：D1D2映射到它的提升版本中，可以将映射Ad扩展为函子，其中域限制为Ad[D1]中的瓦片。这个定义是正确的，因为提升保持了从计算加细态射的定义出发，给出了加细态射的证明。右伴随Ad通过与D-计算D=（H，V，T，n，s，w，e）、具有D的相同水平1-范畴的2-计算Ad[D]以及作为重写规则的D[D]的所有基本瓦片相关联来表征D-计算的抽象行为（计数器将Ad[D]的重写规则映射到它们表示的瓦片事务当考虑瓦片的交换张量积时，类似的构造也是可能的，产生范畴RCompc，其中2Compc是共反射子范畴。我们用Ac表示相应的右伴随。最后，Petri网在Petri网中的共反射成为2Compc和RCompc之间更一般的共反射的一个特例。命题4.11函子和直接嵌入的佩特里·阿扎罗夫˛˛'RCo？mpcz，2CompcD自然同构（natural isomorphism）5例如为了说明我们的构造，让我们再次考虑在引言中定义的简单过程演算（参见图1）。对应于LTS的D-computadCCS可以通过SOS规则的直接翻译来轻松定义（参见[2，15]中的示例）。我们把由过程签名生成的自由范畴（Lawvere理论）Proc作为配置的范畴。垂直范畴是通过对动作μ（看作从1到1的箭头）取自由么半群范畴而得到的。图6中示出了瓦片。让我们假设一个事务应该由两个进程的同步给出。在这种情况下，在同步之后，不应该进一步传播该同步动作，因为系统的其余部分可以独立地演进。为此，BRUNI，MESEGUER和 MONTANARI105⇒nnL1我Jnn1ni+ l+ r+kLi+l， kL+1Ln，氮L1、氮n+1，k基本事务（其中1≤ij≤n）

下载后可阅读完整内容，剩余1页未读，立即下载