SOS规范与结构化余代数：从互模拟到同余关系的转化与闭包构造对系统的适用

URL：http://www.elsevier.nl/locate/entcs/volume 19. html24页s从SOS规范到结构化余代数：如何使互模拟成为同余1Andrea Corradinia Reiko HeckelbaDipa timentodiInformatica，Universit`adegliStudidiPisa，Corso Italia，40，I - 56125 Pisa，Italia，{andrea，ugo}@ di.unipi.itbUniversitétG H P ad erborn，FB17MathematikundInformatik，Warburger Str. 100，D-33098 Paderborn，Germany，reiko@uni-paderborn.de摘要在本文中，我们解决的问题，提供一个结构化的余代数表示的过渡系统的代数结构的状态所确定的方程规格Γ。更确切地说，我们的目标是把这样的系统表示为在Γ-代数范畴上的内函子的余代数我们所考虑的系统是通过使用SOS规则的一种非常通用的格式（代数格式）来指定的，这种格式通常不能保证双相似性是一个同余。我们首先表明，结构化的余代数表示只适用于系统，其中复杂状态的转换可以从相应的组件状态的转换导出。转换的这种分解性质确实确保了双相似性是一个同余。对于不能满足这一要求的系统，接下来我们提出了一种闭包构造，它添加了上下文转换，即，自发地将一个状态嵌入到更大的背景中，反之亦然。丰富系统的互模拟的概念与原始系统的动态互相似性的概念相一致，也就是说，粗互模拟是一个同余。这足以确保结构化余代数表示适用于作为闭包构造的结果而获得的系统1介绍结构操作语义学（SOS）[26]是一个非常流行和强大的-语言规范的完整风格，其中每个语言结构都由几个子句单独定义。进程代数领域的大多数发展都是基于SOS规范，但函数和高阶演算和语言也经常利用它们。特殊格式已被1 由MURST项目Tecniche Formali per Sistemi Software部分支持的研究，由TMR Network GETGRATS和Esprit WG APPLIGRAPH提供。1999年由ElsevierScienceB. V. 操作访问和C CB Y-NC-ND许可证。2⟨⟩定义（参见[8，13，2]），这自动保证了重要的性质，比如互模拟是定义下的微积分的同余，或者可以从SOS规则自动导出归约系统。普通SOS方法的可能局限性在于，实际上开发的模型理论很少，并且格式限制排除了一些最有趣的演算，如π演算2[22]。两种限制都源于从证据理论的角度来看，SOS的做法，以业务服务，mantics（抽象语义通常在连续的步骤中定义），它只在有限的范围内利用结构公理，主要对初始模型感兴趣。与SOS规范相关联的自然初始模型是一个标记的转移系统，它可以很容易地被看作是范畴Set中一个内函子的余代数。然而，这种表示忘记了状态的期限结构，这被看作是形成一个集合。因此，双相似性是一个同余的性质，这是必不可少的，使合成的抽象语义的基础上的双相似性，是没有反映清楚的代数结构。在[28]中，这个问题是通过定义所谓的双代数来解决的，即，代数-余代数对表示具有结构化状态和转换的转换系统。GSOS格式[2]中的一个规范用于导出称为分布律的某种自然变换，该变换确保了代数结构与余代数结构之间的这种相容性也确保了双相似性是一种全等性。虽然双代数的语义框架允许处理方程规格Γ=E，E的代数，但[28]中的方法（如GSOS方法）仅限于签名E的代数。[6]给出了代数与余代数的一种可供选择但等价的积分这里决定余代数结构的闭函子从Set提升到了Γ-代数范畴。这一范畴中余代数之间的态射既是Γ-同态又是余代数态射，因此，到最终余代数的唯一态射总是存在的，它在任何余代数上导出一个（粗）同余。在我们看来，[6]的发展非常自然地适合我们可以称之为结构化模型的方法，这种方法基于内部结构。 基本模型是用集合和函数建立的，基本模型之间的态射是用函数和公理来定义的，这些公理表示为集合中的图。通过将Set替换为环境类别C，我们可以自动地用C指定的结构丰富模型。结构化模型方法对于结构化转换系统[7]，其中基本版本被定义为状态集，图2适用于deSimone的π演算的一个版本（没有复制运算符）格式，因此可以立即推导出头部规范化公理系统，在[9]中描述。3Li转换和它们之间的函数对（即源和目标）3。事实上，结构化转换系统仅仅通过改变环境类别，就可以准确地描述诸如并发语法这样的不同计算模型，Petri网，并发项重写，逻辑程序设计，项图重写和图重写。更有趣的是，自由函子（它存在于C上的温和条件下）将C上的结构化变迁系统的范畴映射到C中的内部范畴的范畴，实际上对应于定义这些计算模型的操作语义另一个相关的例子在[23]中描述，其中[16]中基于开放映射的跨度的双相似性概念，最初为普通变迁系统定义，自动提升到某些历史依赖的变迁系统，这些变迁系统对π演算所需的名称生成和名称传递进行建模一般来说，内部结构可以使用草图[17]或使用代数理论的扩展来定义，这些扩展允许像范畴一样的部分代数（参见例如，[18]），其中内部结构表示为理论的张量例如，双范畴理论（Cat中的内部范畴）可以定义为范畴理论与自身的张量积[20]。在本文中，我们想研究在什么条件下，过渡系统可以表示为一个环境范畴的代数上的我们将一般（正）SOS规则形式化为有限蕴涵（Horn子句），指定一个trans-clause族位置关系−→ll∈L 其中L是一组标签。这自动定义了作为范畴初始对象的生成变迁系统的概念满足规则的系统。为了将SOS规则视为对转换的操作，进一步的研究基于（仍然相当一般的）代数格式[10]，其中规则的前提完全由变量上的转换组成，并且通过允许规则结论的源中的复杂项来推广deSimone格式[8]中的{xi−→yi}i∈Is−→lt其中s∈T∈（{x1. x n}），t∈T（{y1. y n}）。代数格式的规则是deSimone格式的，如果s = op（x1，.，xn），对某些运算op∈ φ.这里的条款 t和s被认为服从一组公理E。代数格式包括在文献中实际上已经提出的并且不能由“行为良好的”格式处理的几个规则例如，它能够通过公理化替换来表达π-演算的规则。也是一个公理的形式a. p|a'. q−τ→ p|Q这是典型的CHAM方法[1]，适用于代数格式，但不适用于任何普通格式，因为它适用于复数项。3还可以轻松添加转换、初始和最终状态的标签41n1n对于代数形式，我们的结果是：对于将满足规则的转移系统S，−→ S表示为Γ-代数范畴中的余代数，下面的条件是充要的。存在着一种过渡opA（a， . . ， a）−→l boutofacomposedd statei且仅当eisa（p可能地derived）rule in deSimone format with source op（x1，. ，xn），并且存在从1，. ，a n，使得将该规则应用于基本转换，得到A（a， .. . ， a）−→lb. 这意味着，一个与代数格式的规则不等同于具有deSimone格式4的规则的规范，它排除了生成的转换系统的结构化余代数解释因此，可以说，方法上的便利，即在SOS方法中，每种语言构造都由几个子句单独定义，这实际上是强制性的，以保证令人满意的代数结构。本文的第二部分考虑了一类不同的系统，但最终作为一种边效应，以代数形式解决了整个过渡系统的提升问题开放系统是当今分布式计算和网络计算的重要组成部分。它们的基本特性之一是能够适应新组件的添加，而无需重复编译和初始化。因此，要使两个开放系统等效，不仅要考虑基于与外部世界通信的实验在我们的设置中，这对应于允许互模拟定义中的一个额外条款，其中应用了任意上下文。由此产生的等价概念在[24]中已经考虑过，并称为动态双相似性。当然，当普通的双相似性是一个congru- ence，动态双相似性与它相吻合在任何情况下，它都可以被表征为粗互模拟，这是一个同余。动态双相似性是一个相当稳定的概念，可以用几种等价的方式定义。对于具有不可观测的τ跃迁的CCS，它与观测一致性不一致（这不是互模拟），但它更精细，并且它可以通过删除米尔纳的τ定律之一来公理化我们关于开放系统的结果是，它们总是符合我们的结构化组合特征。更准确地说，给定任何代数格式的SOS规范，我们可以定义它的上下文闭包，即。另一个具体化也包括可能的上下文转移，即所有导致添加某个上下文并由其标记的转移，我们证明了任何具体化的动态双相似性与其上下文闭包的普通双相似性一致此外，任何上下文闭包都可以看作是结构化的余代数。因此，开放系统，其中动态双相似性是自然的概念，总是有一个令人满意的代数结构。普通的系统，普通的双相似性是不是一个同余，可以获得这个属性（和一个令人满意的代数结构），也考虑动态双相似性。这是在4使用，例如，这就是具体化的公理。5一L并且ΓL表示为HTS。LLL一个更精细的观测一致性概念的代价，无论如何，这是粗略可能的，如果它必须是互模拟的话。2结构化变迁系统与互模拟在本节中，我们首先介绍互模拟、观测一致性和动态互模拟的概念。接下来，我们将介绍结构化的过渡系统，评论它们的一些优点和缺点。转换系统通常配备了一些关于状态的附加结构。我们在这里考虑的系统，其中状态的代数结构是由一个方程的一种代数规格确定的，我们用lg（Γ）表示全Γ-代数和-同态的范畴.定义2.1[异质转移系统]设Γ= Σ λ，Eλ是一个代数规范，使得Σλ至少包含一个常数，L是一组标号。一个（异质）5转移系统（在Γ和L上）是一对hts=<$A，−→hts<$其中A是一个Γ-代数且−→hts<$|一|×长×|一|是标记的（过渡）关系。对于εa，l，b<$∈−→htswewritea−→lHTSB、像往常一样环上（异质）跃迁系统的态射f：hts→htsJ且L是一个Γ-同态mf：A→AJsuchthata−→lHTSb意味着f（a）−→htsJf（b）。环Γ上的（异质）转移系统范畴L注意，签名中常数的存在确保了在Γ，L上的转换系统是非空的。现在我们介绍迁移系统互模拟的标准概念。直觉上，一个变迁系统的两个状态是双相似的，如果不仅存在从它们开始的具有相同标签的变迁序列， 而且在这种转换之后达到的状态是双向相似的。观测等价是双相似态对的最大集合，并且可以很容易地证明它是一个定义良好的等价关系。定义2.2[互模拟，观测等价]设hts=S，−→ S设R是一个二元系统，关系S。然后，从关系到关系的函数，定义为：（s，t）∈R当且仅当对所有l∈L：L• 当s−→sj时，存在TJ使得t−→TJ且（SJ，TJ）∈R;L• 当t−→tJ时，存在sJ使得s−→sJ且（sJ，tJ）∈R。一个关系R称为互模拟，当且仅当R（R）。[5]这种限定旨在强调这样一个事实，即在这些系统中，标签和转移关系具有比状态更弱的结构，这与下面介绍的结构化6∈∈∼∪{R|RR}的关系=（）被称为观测等价性，或者更简单的双相似性。一个等价ρ被称为关于算子f的同余，如果它被算子f遵守，即，（x，y）ρ蕴涵（f（x），f（y））ρ。等价是关于定义在系统状态上的所有运算符的同余，这是非常重要的：它们可以用来提供组合抽象语义。给定一个指定Γ = T，E，我们用T表示T上的项代数，用TΓ=T/E表示所谓的商项代数，即，T_n关于E生成的最小同余的商。此外，如果X是一个变量集，则T（X）表示X上的项代数，其载体是所有在X中有变量的-项的集合。TΓ（X）是关于E的相应商。现在，众所周知，T和TΓ都是它们各自范畴中的初始对象。从T到一个λ-代数A的初始同态是基项到A的元素的归纳求值，记为eval：T→A。代数T（X）在X上是自由的.如果ass：X→A是X到一个λ-代数A（的载体）的一个赋值，则它的自由扩张记为ass：Tλ（X）→A。定义2.3[context，congruence]给定一个指定Γ = E，E，一个在Γ上的context C是T（{·}）的一个元素，其中只有一个变量·出现。给定一个Γ-代数A，a∈A，用C[a]表示A的元素ass（C），其中ass（·）=a.A上的关系R是一个同余，如果只要（a，b）∈R，则对于Γ上的每个上下文C，（C[a]，C[b]）∈ R在许多情况下，观测等价不是一个同余，我们将在后面看到几个相关的例子，一个是Petri网，一个是π演算。这就自然地把我们引向观测全等的定义，它就是包含在观测等价中的粗全等。定义2.4[观测同余]设s，t∈S是给定的Γ上的过渡系统的两个状态。我们说s<$t当且仅当对于任意的上下文C在Γ上，C[s]<$C[t]。关系式称为观测一致性。在[24]中已经引入了动态互模拟动态互模拟的基本思想是，在互模拟的每一步，不仅允许一个动作的表现，而且还允许在同一个但任意的上下文中嵌入两个被测主体正如在引言中所强调的，互模拟的概念对于开放系统来说是非常自然的，它们也必须在响应动态重构（如添加新组件）的行为方面进行比较。下面的定义是关于允许的上下文集的参数7LLL∼∪{R|RR}C定义2.5[动态互模拟]设hts=<$S，−→ <$S是一个在Γ和L上的转移系统，C是一个在Γ上的上下文集，R是一个在S上的二元关系。由关系到关系的函数nΦCd定义如下：（s，t）∈ΦCd（R）i当且仅当对eacl∈L和对ccctextC∈C：L• 当C[s]−→sj时，存在TJ使得C[t]−→TJ且（SJ，TJ）∈ R;L• 当C [t] −→tJ时，存在sJ使得C [s] −→sJ且（sJ，rJ）∈R。R的一个关系式称为C-动态双模拟，它满足R∈ΦCd（R）。如果C是Γ上所有上下文的集合，则称之为动态互模拟TherereelationdC=ΦCd（）被称为d-动态观测等价。它被称为动态观察等价，或者仅仅是动态双相似，如果C是Γ上所有上下文的集合。如果U=d，则称Γ上的一组上下文U对hts是泛的。文[24]指出，动态观测等价是一个粗互模拟，它是一个同余。因此，它与观测同余一致，当（且仅当）它是互模拟。例如，对于具有弱互模拟的CCS [21]，这是[24]中的主要案例研究，因为对于这种过程代数，εd和ε d不是互模拟;相反，它们对于结构化转移系统是一致的，如下所示，以及对于本文的运行示例。结构转移系统是指状态和转移关系都具有代数结构的系统，因此它们可以看作是在Γ和L上的异质转移系统，其中L和转移关系都是Γ-代数。在[7]中已经提出了这种系统的一般理论，并且已经用于为许多形式主义提供计算语义，其中包括[19]意义上的P/T Petri网，项重写系统，项图重写[4]，图重写[5，14]和Horn子句逻辑[3]。定义2.6[结构化变迁系统]设Γ是一个代数规范，L是一个标号的Γ-代数一个结构化的转移系统（在Γ和L上）是一对sts=<$A，−→sts<$A，其中A是一个状态的Γ-代数，−→sts∈A×L×A是积A×L×A在Alg（Γ）中的子代数在Γ和L上的结构化迁移系统的范畴，其态射如定义2.1所定义，记为STSΓ。[6]的主要目标是在一个共代数框架中提供（结构化）变迁系统的等价表示。将Γ上的结构化转移系统表示为通过幂代数构造定义的Alg（Γ）上的内函子的余代数的自然思想不能正确工作，主要是因为在这样的系统中，一般来说，双相似性不是关于Γ的算子的同余事实上，回顾一下，双相似性正是由余代数的8LL公司简介∼NNn同态到终结余代数，如果要求这样的同态是Alg（Γ）的箭头，则它也必须是Γ-同态，即，双相似性必须与Γ的算子一致。文[6]提出的解决方法是通过引入松弛余代数的概念来削弱同态要求。下面的例子是从[6]的完整版本中借用的例2.7[在净变迁系统中，双相似性不是全等][19]深入讨论了在何种意义上交换幺半群是表征库所/变迁Petri网的代数结构。现在，设CM是交换幺半群的代数规范，设6L={t}，设M={a，b}.此外，设N=M，−→N是联系我们STSCM，使得−→N由跃迁a−→a，b−→ b自由生成ab−→tNM，其中，是么半群X的单位。系统N是一个Petri网的忠实表示，它有两个位置，a和b，以及一个转换t，它消耗来自a的一个令牌和来自b的一个令牌，并且不产生令牌。标签EML用于不改变状态的空闲转换。现在，很容易看出状态（标记）a和b是双相似的（a b）因为它们都只产生有限序列的观测值。当然，Bb，但是aBBb因为从a我们可以观察到转变T。这表明M上的观测等价不是同余，因为它与么半群运算不相容另一方面，可以证明，对于结构化变迁系统，观测同余是一种互模拟，因此它与动态观测等价是一致的。事实2.8（观察一致性是结构化t. s中的互模拟。s）设ts=S，−→ S是STS Γ中的系统。则是对ts的状态的互模拟，即，价格（见定义2.2）。因为，为了矛盾，假设互模拟不是互模拟。 然后有状态s，t，使得s ≠ t，并且存在跃迁序列s−l→1.. . −l→n s和t−l→1。 . −l→n 不使得S n/t n，即，存在关于Γ的上下文，比如E，使得E [s n]/E[t n]。 由于在Γ上的结构化转移系统中，转移关系在Γ上的上下文下是封闭的，通过将E应用于上述序列，我们得到序列E[l1]E[ln]E[l1]E[ln]E [s] −→. − → E [s n]和E [t] −→. −→E[tn]现在E [s n]/E [t n]意味着E [s]/E [t]，因为是互模拟。这与假设S是矛盾的。实际上，结构化变迁系统仅适用于建模6 我们用A表示由集合A生成的自由交换幺半群。n9NLL−→基于规则的系统（如Petri网），其中代数结构与转换结构正交。例如，对于进程代数，情况就不是这样了，这就是为什么我们在定义2.1中引入了只有状态是结构化的系统。例如，考虑以下具有早期绑定的π演算[22]的片段，这将是我们的运行示例（该演示将在下一节中更精确例 2.9[π- 演 算 片 段 ] 假 设 一 个 可 数 的 无 限 集 合 的 名 字 （ 由 x ， y ，z，. . ）、前缀（α，β，.）根据以下语法构建（我们假设τ/∈ N）：α=τ|x′y|x（y）则代理（P，Q，.. . ）的构建如下：P = 0 |α.P|P + Q|P|Q代理人被定义为α转换。此外，我们还假设，<$+，0 <$是一个半格，|，0是一个交换幺半群（见例3.5中的代数说明）。代理的操作语义由SOS规则指定如下。[out]x'y.Px′y−→[in]xzPx（y）。P−→P[z/y]对于每个z∈ N[ch]P−→PJ[平价]P−→PJ[com]x'yxyP−→PJ，Q QJP+Q−→lPJP|Q−→lPJ|QP|Q−τ→ PJ|QJ由于+和的交换性，|不需要后三个规则的对称变体。现在，刚刚引入的进程代数不能表示为结构化的转移系统，因为否则转移关系将在状态定义的操作下自动关闭。例如，这意味着要添加以下规则，P−→lPJP−→lPJ， Q−k→QJ0−→00α。P−α→。lα。PJP+Q−l+→kPJ+QJ(see也是示例3.4），这显然对示例没有意义。关键在于，在结构化转换系统框架中，所有操作都被解释为结构化操作，而像不作为0、前缀0、L. 和非确定性选择+在过程代数中具有纯随机意义。此外，这些行为操作生成系统转换的方式通常由SOS规则指定为了将[6]关于变迁系统的余代数表示的结果推广到更一般的系统，包括像上面这样的过程代数这就是为什么我们在定义2.1中引入了异质迁移系统，它在迁移关系上没有任何相关的结构：10LL∈∈L1LnLiLi|我这些可以用来定义具有结构化状态的系统，独立于转换的结构，可以通过适当的SOS规则来指定，利用下一节中介绍的转换指定的概念3SOS规则和过渡规范给定一个代数规范Γ和一组标签L，SOS规则的集合可以被视为HTSΓ的子范畴的一个规范，包括所有在给定规则下其转移关系是封闭的转移系统在下文中，SOS规则被正式定义为一个二元转换谓词−→上的序列，它被定义为每个标签l L.这样的规则可以被解释为Horn子句（具有相等性），其指定被视为关系结构的异构转换系统定义3.1[SOS规则，满意度，蕴涵，理论]给定一组标签L，一个代数规范Γ = λ，Eλ，和一个可数变量X，一个等式ts-→lt（overLandr）是一个三元组，其中el∈L是一个alabel，s，tT（X）是以X为变量的X-项。关于r，L，和X采取的形式S−→t，.，s−→t1 1n ns−→ltL其中si−→t和s−→t是在Γ、L和X上的序列。给定一个异质迁移系统hts=<$A，−→hts<$ A，一个赋值设X→A是方程s-→l到rr，L，和X的解，如果Las（s）−→HTS屁股（t）。 我们说hts满足上面的规则r，HTS|= r，如果s i−→t i的每个（联合）解，其中i = 1，...，n也是一种解决方案到s−→lt。在这个例子中，我们可以说这是一个R的模型。一组规则R必然包含规则r，记为R=r，如果R的所有模型也是r的模型。R的理论Th（R）被定义为R在这个蕴涵关系下的闭包。根据SOS规则作为Horn子句的形式化s−→lt是假设s和r是关系−→l。Mod-通过这种转换，上述通过转换系统满足规则的概念与通过相应的关系结构满足Horn子句的相等性相一致。因此，这种满意度的概念是定义良好的，并且具有合理且完整的等式的Horn子句逻辑的每个演算都为SOS规则提供了合理且完整的演算定义3.2[转换规范]转换规范是一个四元组TS=T r，L，X，R，T，由代数规范T，一组标签L，一组可数变量X和一组SOS规则R组成。11LL1LnLN1∈ N1n和X.用HTSTS表示HTSΓ的全子范畴，其中所有系统满足规则R。事实3.3范畴HTSTS有一个初始对象<$TΓ，−→ <$T，它的状态集是初始的Γ-代数TΓ。下一个例子表明，结构化变迁系统可以用一种相当明显的方式，通过一个合适的变迁规范来表征。例3.4[指定结构化变迁系统]结构化变迁系统的范畴可以通过以下方式作为异质变迁系统设Γ是一个特例，L是一个Γ-标号代数.此外，设X是可数变量集，设R由所有规则X−→y，.，x−→yop（x1，... ，x n）运算L（11，...，l n）−→op（y1，. ，y n）对于Γ中的元数n的每个运算op，以及对于标签l1，. ，l n∈ |L|.这确保了在一个系统中，它是R的模型，在代数运算下，转移关系是封闭的因此，范畴STSΓ同构于范畴HTSTS，其中TS = π Γ，|L|，X，R.现在让我们回到我们的运行示例。例2.9的π演算的片段可以被表征为以下具体化的初始模型。例3.5[π -演算的转换规范]设是一组通道名，设α，β，. 在例2.9中定义的前缀范围。然后，代理人被定义为以下一个排序，等式代数规范。7=排序代理运营商0：→代理α。 ：Agent→ Agent（对于每个前缀α）+：代理，代理→代理| : Agent, Agent → Agent[x/y]：Agent→ Agent（对于每对x，y∈ N）公理对于所有P，Q，R：Agent，x，y，z，v0+P=P，P+Q=Q+P，7一个更简单、更优雅的演示可以通过使用一个多排序的代数规范包括，除了Agent，还对Name和Prefix进行排序，并假设这些排序的固定解释（例如，隐代数[11]的风格）。 我们更倾向于坚持单排序的情况，以保持定义更简单。n12关于我们⟨⟩P + P = P，（P + Q）+R = P+（Q +R），（P |Q）|R = P|（Q|R）、 P|Q =Q|PP |0 = P0[z/x] = 0（τ.P）[z/x] =τ.P[z/x]（x′y. P）[z/x]=z<$y。P[z/x]，ifx/=y（x<$y. P）[z/y]=x<$z。P[z/y]，ifx/=y（x<$y. P）[z/v]=x<$y。P[z/v]，ifvx，y（x′x. P）[z/x]=z<$z。P[z/x]x（y）.P=x（z）.P[z/y]如果z/∈自由名（P）（x（y）.P）[z/v]=x（y）.P[z/v]，如果y/∈{z，v}且x/=v（x（y）.P）[z/x]=z（y）.P[z/x]，如果y/∈{x，z}（P+Q）[z/x]=P[z/x]+Q[z/x]（P |Q）[z/x]= P [z/x] |Q [z/x]此外，设L是标签（可观察动作）的集合，输出操作x<$yforeachx，y∈N对于每个x，y∈ N，输入动作 xy不可见作用量τ现在，转移规范Pi由四元组Pi=L1，L2，X，R3给出，其中R3由例2.9中列出的规则的所有实例组成。值得强调的是，在跃迁规范Pi的模型中，观测等价性不是一个一致性。例3.6[双相似性在π-演算中不是同余]设u，v∈ N其中u/=v。在HTSPi中的任何转换系统中，考虑两个代理P=u′y。0|v（z）。0 和Q=u′y。v（z）。0 +v（z）。是的。0很明显，P。现在考虑上下文C = x（v）。·超过1000。那么很容易检验C [P]= x（v）.P/x（v）.Q = C [Q]。其实我们徐τ徐x（v）. P−→P[u/v]=u<$y。0|u（z）。0−→0|0 [y/z]=0，而x（v）. Q−→Q[u/v]=u<$y。u（z）。0+u（z）。是的。0，而这一年龄没有任何外传-位置标记为τ。作为结构余代数的4-异质迁移系统13众所周知，标记转移系统可以表示为合适函子的coalge- bras [27]。让我们首先介绍函子的余代数的标准定义。14→ CLLXZNL定义4.1（余代数）设B：C → C是范畴C上的内函子。B或B-余代数的余代数是一个对A→ A，A→ A，其中A是C的对象，a：A→BA是一个箭头。一个B-同态f：A →A，a →AJ，a j →A是C的一个箭头f：A→AJ，使得(1)aJf = Bf a.记B-余代数和 B-同态的范畴B-Coalg。底层函子U：B-Coalg映射一个对象A，A和f的箭头。设PL：Set→Set为函子，定义为X<$→P（L×X）其中L是一个固定的标签集，P表示幂集函子。那么，这个函子的余代数<$S，σ<$表示一个标号转移系统<$S，−→ <$其中s−→sj，如果<$l，sj<$∈σ（s）。反之亦然，每个标记的转换系统<$S，−→ <$可以通过σ（s）= {<$l，s j <$$>映射到余代数<$S，σ：S→PL（S）<$|s−→lsJ}。该翻译是建立在一对一的基础上，PL-余代数与L上的标号转移系。这种表示的一个问题是，由于基数问题，函子PL不允许最终余代数[27]。一种可能的解决方案（在文献中经常采用）包括用有限幂集函子Pf替换幂集函子P，从而定义函子P f：X<$→Pf（L×X）这个内函子的余代数与有限分支转移系统一一对应，即，其中对于每个状态s，ss−→lt从sifinite转变。然而，在某些情况下，对于π演算，我们遇到了具有无限分支的转移系统，如下面的例子所示。例4.2[无限分支]考虑代理x（y）。0，可能是-在通道x上接收一个名称z ∈ N，进行一个转换x（y）。0−→ 0。以来如果要接收的潜在名称z的集合是可数无穷的，则存在这样的传出转移的可数无穷集合因此，π-演算转移系统是具有可数度的转移系统。由于我们的目标是将π-演算转换系统表示为余代数，我们定义了一个集上的函子，其余代数表示具有可数度的系统。一个（标记的、异质的或结构化的）迁移系统S，−→ S具有如果每个状态s∈Sthet{sJ，l j}，则（运行的）一个b le d e gr e |s−→l是可数的sJ}事实4.3（作为余代数的可数度的转移系统）设Pc：Set→Set为函子，定义为X<$→Pc（L×X）15LLP→LLLLLLLLLLLL其中c：Set Set是与每个集合X相关联的可数幂集函子，X的所有可数子集的集合。然后，L上可数度的转移系统与Pc-余代数一一对应.Pc-余代数与可数次转移系统之间的对应关系与非限制转移系统与PL-余代数之间的对应关系类似. 然而，与函子PL不同，函子Pc允许上自由和最终余代数命题4.4（最终和上自由Pc-余代数）明显的基础函子U：Pc-Coalg→Set有一个右伴随R：Set→Pc-Coalg与每个集合X相关联的是X上的余自由余代数。 因此，范畴Pc-Coalg有一个最终对象作为最终集合1上的余自由余代数R（1）。证据根据[27，15]，足以证明函子Pc是有界的。这是因为由Pc分配的子集的基数受ω限制（参见[27]，实施例6.8）。✷此外，很容易证明函子Pc保持弱拉回，这是大多数有用的煤炭机械的主要假设。集合中的gebras。因此，函子Pc有很多很好的特性函子Pf基于有限的幂集因此，我们将坚持这个函子在本文的其余部分，因为没有混淆的余地，我们将跳过指数c，简单地用PL表示Pc。在下文中，我们将具有代数结构的PL-余代数丰富为结构化余代数，即，代数范畴上闭函子的余代数这个函子将把集合上的内函子PL提升到Γ-代数的范畴，也就是说，它将像PL一样作用于载体集合，但是，另外，它必须定义运算。在异质变迁系统中，只有状态具有代数结构，但如前所述，变迁规范的SOS规则可以被认为是变迁上的代数结构（的规范）。然而，与状态代数相反，对转换的操作通常是部分的和非确定性的，也就是说，它们是在转换集合上定义的，而不是在单个转换上。例如，指定的选择操作+，解释为transitions，取两个transitionsP−→PJ的集合SP和SQ作为自变量和Q−k→QJ，分别从代理P和Q中产生，并作为结果传递一个集合SP+Q ={P+Q−→lPJ|P−→lPJ∈SP {P+Q−→QJ|Q−k→QJ∈SQ }的P+Q的输出跃迁。第一个子集对应于P的选择直接从转换规范中的规则[ch]导出第二个子集遵循+的交换性，这允许导出对称规则。例如，这种直觉在[27，28]中被形式化，其中使用GSOS规则[2]来定义余代数上的代数结构作为证据-K16⟨⟩LiLiLi→ii i∈Ijj∈{1，.，我Jj∈ {1，...，我在理论设置中，在[25]中使用转换系统实现了类似的思想，其中每个转换携带（除了源、目标和标签之外）证明项，该证明项表示其通过规则的推导，该规则充当对这种证明的操作。接下来，我们将介绍几种SOS规则的格式，这些格式使得将规则解释为对转换的操作变得更简单。特别地，我们考虑代数格式的规则[10]，其中规则的前提完全由变量上的转换组成，并且通过允许规则结论的源中的复杂项来定义4.5[代数形式的规则]关于r = r，E和L的规则是代数格式，如果它具有以下形式{xi−→yi}i∈Is−→lt在这里我将{1. n}，l i，l∈L，s∈T∈（{x1. x n}），t∈T（{y1. y n}），使得xi= y ji <$i = j且j/∈ I。 如果I ={1. n}。代数格式的规则是deSimone格式的，如果s=op（x1，.，xn），对某些运算op∈ φ.下面，只有完整的规则用于定义转换的代数结构。这一要求确保了出现在规则结论中的所有变量都被它们在前提中的出现所每一个具有代数形式规则的转移规范TS=L r，L，X，Rj可以变换为仅具有完全规则的规范C（TS）=L r，Lj {\displaystyle L\，X，R\，J}为此，我们为空闲转换添加了一个特殊的标签，并为每个操作op：n∈n引入了一个规则{xi−→yi}i∈{1，.，n}int x =1， . . ，xn）−→dupop （y1， . . ，yn）从而在空闲转换下感应地关闭系统R中的每个规则{xi−→yi}i∈Is−→lt然后用一个完整的规则代替代数格式{x−→y}，{x−→xxJ}s−→lt[xJ/x]通过为未出现在原始规则前提中的每个分量添加空闲转换xjXJj（其中XJj是新变量），并在t中用XJj替换xj的所有出现。注意，对于一个系统，A，−→ A，其状态集A是项生成的，该替换不改变T的含义。事实上，它很容易通过归纳法在术语“具有带标签的转换的结构”是空闲的，即，，ass（xj）−→这意味着对于任何赋值ass：X→A，ass（xj）=ass（xJj）。hts屁股（xJj）17⟨⟩HTSx′y−→LLiR这种转换背后的语义思想在下面的命题中陈述。命题4.6（完备化）给定一个标号集L和一个代数规范Γ = E，E，设TS是L和Γ上的一个转移规范，C（TS）是它的完备化。 假设异构转换系统hts =T ∈A，−→hts∈ L和Γ使得A是项生成的，即初始同态eval：T∈→A是满射的。则，如果且仅当它的“自反闭包”hts r =<$A，−→r 在L<${\displaystyle L\，}和Γ上，其中−→hts=−→hts{a，，a|a∈A}满足C（TS）。例4.7[补全]让首先，我们介绍了生成空闲转换的规则，标记为“空闲”。P−→PJ（forreveryprefixα） P−→pPJ， Q−→<$ QJ0−→∗0α。P−→ α。PJP+Q−→PJ+QJP−→<$PJ， Q−→<$ QJP−→PJ（对于所有x，y∈ N）P|Q−→ QpJ|QJP[x/y]−→ΔPJ[x/y]接下来，我们将例2.9的规则转换为完整的规则。[out]P−→PJx'y. P−→PJ[in]P−→nx（y）。P−x→zPJPJ[z/y] 对于每个z∈ NP−→ PJ， Q−→<$ QJP−→lPJ， Q−→<$ QJxyxyP PJ，Q−→QJ[ch][平价]LJ[com]lJ JP|Q−τ→ PJ|QJP+ Q −→ PP |Q −→ P |Q由此产生的规格用C（Pi）表示。从一个具有代数形式的完备规则的转移规范出发，我们导出了Set上的内函子PL到Alg（Γ）上的内函子的提升定义4.8[P L的提升]设TS= R r，L，X，Rr是具有代数格式的完整规则的转移规范，且r = R r，Er。 定义P TS：Alg（Γ）→ Alg（Γ），其中8A›→PA=P2P L（|一|），（op PA）op∈λ.op PA（S1，.，Sn）={t，ass（t）}|n{xi−→yi}i∈ {1，.，n}∈T h（R）op（x1，.. . ，xn）−→lt质量：X→Ai∈ {1，.，n}：<$l i，ass（y i）<$∈S i}[8]细心的读者可能会想到一个附加条件，如ass（xi）=Si。 然而，这样的条件并没有很好的定义，因为Si不是代数A的元素。而且由于规则是完整的，有一个序列txi−→Iyi 对于每个i∈ {1，.，n}，并且所有的x i和你是不同的。这一性质定义为所有在t中发生的变量xi，并且代数A中的项的赋值与变量xi的赋值无关。LL18∈LL∗1n1n1n请注意，只有deSimone格式的规则才真正有助于转换上的算法结构它们定义了签名的操作，而代数格式的规则一般适用于复杂的术语，其解释由操作决定。这种提升的“正确性”得到了以下事实的证实：将其应用于例3.4中的结构化变迁系统的具体化，它恰好产生了[6]中定义的提升。对于一个运算op：n nn，结构化变迁系统的规范TS导致op到标签后继对集合的以下逐点扩展，这对于[6]中的幂代数构造是典型的。OP PTS（A）（S，...，S）={L1，.，l），op A（b，.（b）|<$li，bi<$∈Si，其中1≤i≤n}下面的例子说明了我们为什么要用这个理论T h（R）而不是R。例4.9[内函子提升]对于π-演算片段，我们想要得到一个函子PC（Pi）：Alg（Π）→ Alg（Π），它将一个Π-代数A映射到1、A= A+ B + C+|一|），{α.，0，+，|，[x/y]}，其载体是所有L×A的可数子集例4.7中的所有规则都是deSimone格式的完整规则。尽管如此，上述定义仅限于R的规则，不会反映操作的预期含义。原因是在过渡规范中存在结构方程。 例如，考虑选择+下面的公式仅从施事P+Q的-转移规则导出例4.7中的规则[ch]9S1+ S2={\displaystyle {\pi}，P J+ QJ}}|⟨ ∗,PJ⟩∈S1, ⟨∗, QJ⟩∈ S2} ∪{\FN黑体\FS22\BORD1\S