数学运算语义中的行为内函子上的余自由单子的分配律与模块化帐户的操作语义相结合的研究

理论计算机科学电子笔记106（2004）185-200www.elsevier.com/locate/entcs数学运算语义Marco Kick和John Power1，2爱丁堡大学信息学院计算机科学基础实验室国王摘要几年前，图里和普洛特金给出了一个结构操作语义概念的精确数学公式：他们的公式等价于一个行为内函子上的余自由余点内函子上的签名上的自由单子的分配律。从这样一个分配律中，我们可以很容易地归纳出单子在行为内函子上的余自由单子上的分配律，并且它们的大部分分析可以在后一项中进行，从而增加了一点在这里被证明是至关重要的一般性。在这里，主要是在后者的一般性水平，我们调查的情况下，其中一个有两种行为，操作语义可能相互作用。我们领先的例子是结合行动和时间，与模块化帐户的操作语义的组合引起的每两个组件。我们的研究需要调查和新的结果，产品的comonads和提升单子的coalgebras类的产品comonads，提供建设，人们可以很容易地计算。关键词：数学运算语义，模块化，时间转移系统，comonads，分配律。1介绍Turi 和 Plotkin 在 他 们 的 论 文 “Towards a mathematical operationalsemantics”[ 17 ]中一开始是1这项工作得到了EPSRC资助GR/N64571、GR/R67842/01、GR/N23141和GR/586372/01以及EC资助IST-1999-29082的支持2电子邮件地址：mailto:ajp@inf.ed.ac.uk1571-0661 © 2004 Elsevier B. V.根据CC BY-NC-ND许可证开放访问。doi：10.1016/j.entcs.2004.02.030186M. Kick，J.理论计算机科学中的电力/电子笔记106（2004）185基本范畴C的有限积，C上的在温和的条件下，他们表明，每一个抽象的操作规则，产生了一个分配律的单子T的cofree comonadD上B，使他们能够模拟组合的操作和指称语义。更微妙的是，文[11]指出并在文[14]中进一步解释和利用了：给出一个抽象运算法则实际上等价于给出一个内函子B上的余自由共点内函子上的自由单子T的分配律，由此可以推出T在D上的图里和普洛特金在这里，我们在Turi和Plotkin提出的通用性水平上研究模块化，其确切意义是试图结合两种行为，即，从内函子B和BJ开始，或者更一般地从comonadsD和DJ开始，并尝试使用更原始的数据，以诱导T在B×BJ上的余自由余点内函子上的分配律，或者更一般地在余单子D×DJ上，如果后者存在的话。我们的主要例子涉及时机。时域是一个服从两个条件的幺半群（T，+，0）（见定义2.1）。 一个主要的例子是由一组自然数与加法。一个时间转移系统是一个标号转移系统（P，T，~），其中P是一组过程，T是一个时间域，~P×T×P是一个时间转移关系，即，它满足确定性、零延迟和连续性公理（见定义2.2）。定时转换系统的概念是第一作者论文的核心在[9]中进行了总结，并从文献中的各种时间记录中进行了综合，例如[6，13，18]。 给定有限作用集A，时域T和集合P，给出P上的一个非均匀迁移系统（P，A，T，→，~）通过• 一个像限跃迁系统（P，A，→），• 定时转移系统（P，T，~）对于余代数的认知者来说，这种情况需要分析：第一个转换系统相当于集合[5]上的内函子B时间转移系统更复杂，但我们可以证明它相当于集合上的一个余代数，其中ET由时域T生成，并有一个自然而简洁的描述（见定义2.5和定理2.4和2.6）。当时域是自然数的集合时，余单子ET是闭函子上的余自由余单子（见定理2.7），但这是非典型的。所以我们总是在Set上有一对单子D和Dj，以及一个D-余代数结构和一个DJ-余代数结构M. Kick，J.理论计算机科学中的电力/电子笔记106（2004）185187在同一个片场此外，我们可以假设D是闭函子B上的余自由余单子，并且存在一个重要的特殊情况，其中DJ也是闭函子BJ上的余自由余单子。我们在第2节中分析时间，在第3节中分析过渡系统的组合。为 了 给 出 一 个 统 一 的 操 作 语 义 ， 我 们 首 先 需 要 用 一 个 组 合的comonadG来代替comonad对D和Dj，对于这个组合的comonadG，一个G-余代数相当于一个集合，更一般地说，是一个范畴的对象，在这个集合上有一个D-余代数结构和一个DJ-余代数结构。但是comonads的产品并不总是存在的，当它们确实存在时，它们通常很难计算。在第三节中，我们证明了乘积做我们想要的工作，我们给出了暗示这样一个乘积存在的简单而一般的充分条件，并且，取[2]中关于单子的结果的对偶，我们用人们可以容易地计算的术语来表示乘积，假设其中一个单子在一个内函子上是余自由的，这对我们研究的所有例子都是正确的。如果两个余单子都在内函子上是余自由的，那么生活就变得简单得多，因为余单子的乘积就是内函子的乘积上的余自由余单子，而内函子的乘积又是逐点给定的。转向两个行为的操作语义的组合，出现了进一步的微妙之处[10]：并不总是有独立的行为对，即，一个人可能没有分配律公司简介和TDJDj人们试图将其结合成一种形式，T（D×DJ）（D×DJ）T这种情况有时会在实践中出现，我们在第4节中会很容易地处理它。但更一般地说，时间行为通常与动作行为交互：最一般的情况是，T（D×DJ）和T（D×DJ）DJT因此，第4节的大部分内容致力于推导组合的操作语义，给出了组合的必要和充分条件，必然允许参数化起始数据的可能性。188M. Kick，J.理论计算机科学中的电力/电子笔记106（2004）185我们认为本文的工作是[ 14 ]的自然发展，[14]是第一次尝试采用图里和普洛特金一个机构的建设和定理在其定义的一般性水平，反映和建议计算实践的例子。2时间转移系统本文的目的是在操作语义的行为组合在我们领先的例子中，其中一个行为是由时间给出的。因此，在本节中，我们简要地阐述了时间过程的解释，在第一作者的论文[ 10 ]和总结论文部分的论文[ 9 ]中有更充分的我们的分析与许多关于时间的文献一致，并推广了这些文献，例如[6，13，18]。定义2.1[10，定义3.1]时域是一个幺半群（T，+，0），满足反对称和左消去公理如下：（t，u T）.t + u = 0 t = u = 0（s，t，u T）.s + t = s + u t =u.有一系列明显的例子，主要的例子是由一套自然-和的集合，每一个都具有由和给出的幺半群结构。当然，在文献中还有大量的其他例子：参考文献列表见[9，10]定义2.2[10，定义3.5]定时转移系统是一个标记转移系统（P，T，~），其中P是一组过程，T是一个时间域，~P×T×P称为时间转移关系，满足确定性，零延迟和连续性公理，分别由下式给出：p~t pjp~tp~0pJ=pJppt~+upJ惠（pJJ）.p~tpJJ~upJ我们称（P，T，~）为T上的时间转移系统.这些公理的理由在[9，10]中有解释。这里要观察的关键点是，这只是关于时间：它不涉及任何其他可能的行为。它已被证明是有用的隔离的时间行为从所有其他可能的M. Kick，J.理论计算机科学中的电力/电子笔记106（2004）185189行为的过程[9，10]，但在本文中，我们要重组两种这样的行为与理论支持。文[9，10]的一个基本结果是：T上的时间转移系统与幺半群T的部分作用完全等价。为了使这一点精确，我们进行如下。定义2.3给定一个幺半群（M，+，0）和一个集合X，M在X上的部分（右）幺半群作用是一个部分函数α：X×M−→X，使得对于X中的所有x和M中的m，n，其中是Kleene等式，α（x，0）xα（α（x，m），n）α（x，m+n）有几种可能的方法可以使部分M-动作成为范畴M-pAct，但在这种情况下最有用的方法是将从（X，α）到（XJ，αJ）的映射定义为全函数f：X−→XJ，使得对于X中的所有x和M中的所有m，f（α（x，m））αJ（f（x），m）定理2.4给出一个时间转移系统（P，T，~）是给出一个局部的T-作用于 P，等价于p~t pJ惠pJα（p，t）[10]的中心结果是定理4.1，它断言对于时域T，范畴T-pAct，根据定理2.4，相当于一类定时转移系统，是Set上的余单元，其中余单元如下所示。定义2.5给定一个时域（T，+，0）和一个集合X，T-演化是满足以下两个公理的部分函数e：T~X电子邮件（0）（t，u T）.e（t+u）↓e（t）↓我们用ET X表示X上所有T-演化的集合，或者如果T从上下文中是清楚的，则简单地用EX表示。定理2.6 [10，定理4.1]对任意时域（T，+，0），从T-pAct到Set的遗忘函子是余单元的，余单元由ET给出.190M. Kick，J.理论计算机科学中的电力/电子笔记106（2004）185注意，一般来说，ET是一个不是闭函子上的余自由余单子的余单子：参见[10]中的一些例子。但在一个主要的例子中，即，在T是自然数的集合的情况下，它是。定理2.7[10，定理4.2] cf [3]设N表示带和的自然数幺半群. 则E N是由1+−给出的集合上的内函子上的余自由余子。定理2.6和2.7以及它们在[9，10]中的发展意味着，仅对时间运算行为的研究就归结为对自由单子T在行为单子ET上的签名上的分配律的研究，其中一个主要的例子是行为内函子上的余自由单子。这为我们在下文中分析行为组合提供了背景。我们只需要[10]中的一个结果就可以继续下去。命题2.8 [10，命题4.8]对于任何时域T，函子ET是可达的，其秩由任何大于T的基数的无穷正则基数给出。3comonads的乘积在本节中，我们希望考虑第2节中描述的时间行为与在余代数文献[5]中广泛研究的与动作相关的普通行为的组合。这使我们能够在接下来的部分中研究组合的操作语义。为了优雅起见，我们将根据一对共单子进行理论分析，其中一个或可能两个共单子在一个内函子上自由地给出。定义3.1[10，定义7.1]设A是有限的动作集，设T是时域，设P是集合。P上的一个异质迁移系统（P，A，T，→，~）由以下组成：• 一个像有限标号的转移系统（P，A，→），• 定时转移系统（P，T，~）我们在前一节中已经看到，对于前面定义的余代数ET，一个时间转移系统相当于一个ET我们早就知道，一个象有限标号的转移系统是由一个内函子B的一个B-余代数给出的，而且，我们可以把它看作是B上的余自由余单子D的一个D-余代数，它存在于所有的主要例子中[5]。 因此，一个异质转移系统相当于一个集合，它具有一对余代数结构，前者由余自由给出M. Kick，J.理论计算机科学中的电力/电子笔记106（2004）185191−−→comonad on an endofunctorB.因此，给定余单子D和DJ，我们试图将一个异质迁移系统解释为由D和DJ导出的余单子的余代数。事实上，如果它存在，组合的comonad必须是comonad的乘积D×DJ：注意，该乘积一般不是逐它不是由闭函子的乘积给出的。此外，它不需要总是存在。定义3.2给定范畴C上的comonadsD和DJ，定义范畴（D，DJ）-Coalg为由下式给出的大范畴中的拉回（D，DJ）−Coalg）DJ−CoalgUDJV VD Coalg）CUD其中UD和UDJ是遗忘函子。命题3.3如果遗忘函子U：（D，DJ）-Coalg C有一个右伴随G，则（D，DJ）-Coalg是C上的余单子，其余单子由G给出。证据利用Beck单子性定理的对偶同构的映射是平凡的：（D，DJ）-Coalg中的映射仅仅是C中保持两个余代数结构的映射，如果C中的映射是同构，则它的逆映射必须保持两个余代数结构。对于第二种情况，任何U-分裂均衡器对被发送到D-合并中的U-D-分裂均衡器对和D-J-合并中的U-D-j -分裂均衡器对.因此C中的分裂均衡器必须通过贝克定理的逆（简单）部分提升 函子U通过构造保持它Q在一般条件下，要直接证明遗忘函子U：（D，DJ）-Coalg−→C的右伴随的存在性并不容易，从而通过该命题得出共单性。但是一条间接的路线是容易获得的--通过对关于可及范畴的结果的稍微微妙的使用，我们能够获得[12]，cf [4]。定理3.4若C是局部可表示范畴， D和DJ是可达范畴，则范畴（D，DJ）-Coalg是局部可表示范畴，且遗忘函子192M. Kick，J.理论计算机科学中的电力/电子笔记106（2004）185−→−C有一个右伴随证据 首先观察到余代数结构沿着同构迁移，即，给定一个D-余代数（X，d）和C中的一个同构f：XXJ，则XJ具有一个（唯一的）D-结构，使得f是D -余代数中的一个同构.因此范畴（D，DJ）-Coalg等价于以下范畴：一个对象由一个D-余代数（X，d），一个DJ-余代数（XJ，DJ），以及X和XJ之间的C中的同构组成。后一类是等逗号对象P）DJ−Coalgn=UDJV VD Coalg）CUD在大类中。但可达范畴的大范畴在可达comonad取余代数范畴（见[4]），iso-comma对象[12]和范畴等价下是封闭的。所以（D， DJ）-Coalg是一个可达范畴.此外，由于D和DJ都是可达的，所以D-Coalg和Dj-Coalg是共完备的，而UD和UDj保持共极限.所以（D，DJ）-Coalg也是余完备的，并且C的遗忘函子保持余极限.因此（D，DJ）-Coalg是一个局部可表示范畴，C的遗忘函子保持上极限;因此后者有一个右伴随。Q因此，对于我们主要感兴趣的所有例子，例如对于C=Set和D和DJ是我们的任何领先例子，我们确实有一个comonad。[4]中对可及性的重要性进行了不寻常的是，但幸运的是，我们知道我们有一个comonad，这一事实允许我们将它作为D和DJ的乘积。假设我们有一个任意的类别C。给定一个C的对象X，考虑函子C（X，−）X：C−→C。 它将对象Y发送给X的C（X，Y）个副本的余积。对于任意的内函子H：C−→C，从米田引理可以得出，为了给出一个自然变换，χ：C（X，−）XH等价于给出一个映射x：X−→HX。人们可以很容易地证明，M. Kick，J.理论计算机科学中的电力/电子笔记106（2004）185193−×函子C（X，-）X具有自然的comonad结构，并且有[8]在[8]中的双重设置中广泛使用的以下等效性命题3.5对于C上的一个comonadD，给出一个comonadχ：C（X，−）XD等价于在对象X上给出一个D-余代数结构（X，x）。使用这个命题，可以立即证明以下内容。命题3.6对于C上的余子D和 DJ，如果存在余子D×DJ的积，则余代数范畴（D×DJ）-Coalg与拉回正则同构（D，DJ）−Coalg）D−CoalgUDJV VD Coalg）CUD证据给出一个D×DJ-余代数等价于给出一个形式为χ：C（X，−）XD×DJ但是，根据乘积的定义，这相当于给出一对映射，χ：C（X，−）XDχJ：C（X，−）XDJ这又等价于给出（D，DJ）-Coalg的对象。所有这些等价都是自然的，产生了结果。Q余代数的特征在于它们的余代数范畴，命题的规范同构与C的基本函数交换。所以这个命题有一个对偶命题如下。定理3.7若从（D，DJ）-Coalg到C的遗忘函子与余单子G是余单子，则余单子DDj的积存在并由G给出.194M. Kick，J.理论计算机科学中的电力/电子笔记106（2004）185⇒⇒××证据 典范函子（D，DJ）−Coalg−→D−Coalg与健忘的函子交换到C。因此，如果（D，DJ）-Coalg具有以下形式：G-Coalg ，函子必须具有以下形式δ−Coalg：G−Coalg−→D−Coalg对于一个comonadsδ：G D映射（对偶结果见[1]）。 因此我们有投影δ和δJ。现在，给定一个comonadW，给出一个comonad映射ω：W D等价于给出一个从W-Coalg到D-Coalg的函子，它与遗忘函子交换。使用（D，DJ）-Coalg的定义作为拉回，我们得到了从S-Coalg到G-Coalg的唯一函子，它与遗忘函子以及δ-Coalg和δJ-Coalg交换，从而得到了所需的唯一共单子映射。Q结合命题3.3、定理3.4和定理3.7，我们现在可以推出我们所寻求的结果。推论3.8如果C是局部可表示范畴，D和DJ是C上的可达余子，则积DDj存在，并且由从（D，DJ）-Coalg到C的遗忘函子的右伴随给出，表明（D，DJ）-Coalg为（D× DJ）-Coalg.这个推论包括了我们可能非常感兴趣的所有例子。但是它并没有给出一个我们可以容易地计算的乘积D×Dj的然而，在我们主要感兴趣的情况下，由动作行为给出的余单子之一是闭函子上的余自由余单子。在这种情况下，[2]中单子的结果的对偶不给我们一个合理的解释如下。定理3.9对任意范畴C和任意内函子B和余单子D，若B和BD上的余自由余单子B∞和（BD）∞存在，则积B∞D也存在，并由具有典范余单子结构的函子D（BD）∞给出。这个定理的对偶出现在[2]中，而这个定理直接出现在[10，定理7.1]中。我们在这里不包括详细的推导过程，尽管它确实包含了独立的结果。我们只是参考第一作者论文第7章的发展在共代数文献中有大量关于闭函子上的余自由余子的构造，例如[19]，但也可参见[7，14]。特别地，如果C是局部可表示的，M. Kick，J.理论计算机科学中的电力/电子笔记106（2004）185195−×× ×××且B和D是可达的，则余自由余单子B∞和（BD）∞存在[4]，因此定理成立。更具体地说，回想一下，我们关于时域的主要例子是由自然数给出的，对于这种特殊情况，余单子ET本身就是闭函子上的余单子，即1 +。因此，在D和DJ都是闭函子B和BJ上的余自由余单子的情况下，有一些兴趣。但这是一个特别简单的情况，因为那时，闭函子B的余代数范畴B-Coalg同构于余单子D的余代数范畴D-Coalg，因此，通过上述分析的一个变体，我们有以下结果。推论3.10给定范畴C上的闭函子B和BJ，乘积使得余自由余子B∞和BJ∞存在，产品余单子B∞BJ∞存在且由（B BJ）∞给出，其中B BJ是闭函子的逐点积，条件是BBj上的余自由余单子存在。4行为组合的结构化操作语义在这一部分，我们到达了论文的核心从第三节中我们知道，在比较温和的条件下，如何在余单子和基范畴上构造余单子的乘积的余代数范畴。我们可以在温和的条件下进一步证明乘积本身，只要其中一个分量在闭函子上是余自由的，就像我们前面的例子一样从第2节中，我们进一步得到了一类例子，说明为什么我们需要这样一种可能行为的产物。但是现在我们将这种分析与图里和普洛特金的思想结合起来，根据可证明的分配律来建模结构操作语义[17，11，14]。对我们来说，中心事实是我们在第3节中把范畴（D DJ）-Coalg刻画为（D，DJ）-Coalg，以及在[15]中把单子T在共单子D上的分配律刻画为T到D-Coalg的提升，[11]对此作了进一步的探讨。定理4.1 给定一个单子T，余单子D 和 DJ，以及分配律λ ：TD<$DT和λJ ：TJD<$DTJ，如果余单子D × Dj的乘积存在，则存在D × Dj上T的一个正则分配律。证据这是从[15]和命题3.6得出的。由前者，这两个分配律分别给出了T对D-Coalg和Dj-Coalg的提升.通过后者，这些提升产生（D×DJ）-Coalg上的单子，因为它是196M. Kick，J.理论计算机科学中的电力/电子笔记106（2004）185×回撤类别P。因此，通过[15]的逆部分，我们得到了我们所寻求的T在D×DJQ但是这个结果并不像人们所希望的那样具有普遍性，因为人们并不总是从分配律λ：TD<$DT和λJ：TJD<$DTJ或任何诱导它们的东西开始[10]。原因在于，在主要示例中，时间信息和动作信息通常相互作用[10，第7.3.2节]。所以我们考虑下面的问题：给定一个单子T和一个共单子D和DJ，什么是必要的和充分的数据，使D和DJ在某种程度上分开，但又使单子T提升到范畴（D，DJ）-Coalg？[15]中未明确说明以下结果，但确实根据其中的分析得出，而该分析又基于[16]中作为限度的D-Coalg命题4.2给定范畴C上的余单子（D，δD，D）和（E，δE，E）以及函子H：C−→C，给出 H到函子从 E-Coalg到 D-Coalg的提升等价于给出一个自然变换α：HEβDH根据以下两个图的可交换性HEα）DH HEα）DHHδEvδDHvD. HvHEE） DHE） DDHαE Dα利用这个命题的两个副本和我们在命题3.6中把（D DJ）-Coalg刻画为（D，DJ）-Coalg，我们可以很容易地推导出以下结果。命题4.3给定范畴C上的余单子D和 DJ，使得乘积D×DJ存在，并且给定函子T：C−→C，将T提升到（D×DJ）-Coalg上的内函子等价于给出自然变换λ：T（D×DJ）<$DT λJ：T（D×DJ）<$DJTM. Kick，J.理论计算机科学中的电力/电子笔记106（2004）185197×××遵循以下四个公理：T（D × DJ）λ）DTT（D×DJ）λ）DTT δ（D×D'）vδDTvGDTvT（D×DJ）（D×DJ））DT（D×DJ））DDT Tλ（D×DJ）DλT（D×DJ）λJ）DJT T（D×DJ）λJ）DJTT δ（D×D'）vδD'TvGJDvT（D×DJ）（D×DJ）J）DJT（D×DJ））DJDJT Tλ（D×DJ）DJλJ现在假设一个人不仅有一个内函子T，而且有一个想要提升的点内函子（T，η）。命题4.4给定范畴C上的余代数D和 DJ，使得乘积D DJ存在，并且给定C上的一个点内函子（T，η）以及内函子T到（D DJ）-Coalg的提升（或者等价地，用命题4.3的数据服从命题的公理T的单位 η提升当且仅当以下两个图交换：D×DJ）D D×DJ）DJη（D×DJ）DηVVη（D×DJ）vDJηvT（D DJ））DTλT（D×DJ））DJTλJ证据 我们已经有了单位的数据，自然条件是微不足道的。唯一的问题是找到自然变换的每个分量是（D，D j）-Coalg中的映射的必要和充分条件;但是我们知道（D，DJ）-Coalg中的映射是由C中的映射给出的，它们都尊重两个余代数结构，所以检查它是一个例行的事情。该条件的一个必要和充分条件：这样的结果出现在[15]中，它基本上是从[16]中收集的，但它也很容易直接看到，如在陈述中给出的。Q最后，给定一个单子（T，μ，η），我们寻找乘法提升的必要和充分条件。 这一点并不容易：198M. Kick，J.理论计算机科学中的电力/电子笔记106（2004）185×如命题4.3所示，单子的函子部分的提升产生一个分布律τ：T（D×DJ）<$（D×DJ）T。我们需要在对易的图中，使用这个导出的分配律，来使乘法上升。条件很容易写如果一个人愿意使用它分配律，但它确实使潜在的棘手的计算，在验证的例子满足条件，因为分配律是由更原始的数据。幸运的是，在特定的情况下，图的可交换性是相当常规的验证。命题4.5给定范畴C上的余单子D和 DJ，使得乘积D×DJ存在，并给定C上的单子（T，μ，η）以及点闭函子（T，η）到（D×DJ）-Coalg的提升（或等价于命题4.3和4.4的数据服从命题的公理T的乘法 μ提升当且仅当以下两个图交换：TT（D×DJ）T）τT（D×DJ）TλT）DT Tµ（D×DJ）DµVVT（D DJ））DTλTT（D×DJ）T）τT（D×DJ）TλJT）DJTTµ（D×DJ）vDJµvT（D×DJ））DJTλJ证据证明类似于命题4.4，利用拉回（D，DJ）-Coalg的万有性质，给出了自然变换的分量从C提升到D-Coalg和DJ-Coalg的一个充要条件.上面的图是相当常见的，但是我们确实需要直接从升力的角度来考虑，因为在两个图中都使用了τ。Q在命题4.5中τ的存在而不是在命题4.4中τ的存在意味着乘法的提升，与单子的单位的提升相反，对于每次提升，依赖于λ和λJ用于提升到D-Coalg和DJ-Coalg中的每一个。M. Kick，J.理论计算机科学中的电力/电子笔记106（2004）185199显然，命题4.3，4.4和4.5可以结合起来产生一个涉及八个图的定理。但如何做到这一点是显而易见的，所以我们把它留给任何感兴趣的读者。第4.5章特殊情况通常从以下形式公司简介动作行为，而只有一个自然的形式转换T（D×DJ）DJT时间的行为。这稍微降低了一些图的复杂性，上面的分配律经常通过[17，11，14]的路径来实现，但是我们仍然需要命题4.5中涉及τ的两个图中的第二个。在稍微不同的方向上，我们可以考虑D和DJ中的一个或两个是闭函子上的余自由余单子的情况，比如D在B上是余自由的。然后D-Coalg由B-Coalg的更简单的泛性质决定，因此可以避免提升函子所需的相干公理。生活也更简单，因为人们可以使用我们对商品的描述。因此，要将函子T提升到B-coalg，只需要任何自然变换，根本不受公理的约束，形式如下：α：TDJ（BDJ）∞BT并且这可以容易地例如由形式β：T（Id×B）DjBDJT将DJ应用于计数器（BDJ）∞Id，DJ（BDJ）∞<$DJ. 一个是典型的合成DJ（BDJ）∞<$（BDJ）∞<$BDJ因此，一个自然变换的形式为DJ（BDJ）∞<$（Id×B）DJ，因为内函子的乘积是逐点给出的（当然，假设C有乘积），因此将T应用于此，并与β和另一个嵌入的计数器产生一个自然的变换，其形式如下：TDJ（BDJ）∞<$T（Id×B）DJ<$BDJT<$BT。引用[1] 巴尔， M.， 和C.威尔斯， 三元组和理论，200M. Kick，J.理论计算机科学中的电力/电子笔记106（2004）185[2] Hyland，M.，G.D. Plotkin和A.J. Power，组合效应：总和和张量，理论计算机科学，出现。[3] Jacobs，B.，Monocongruences and cofree coalgebras，[4] Johnstone，P.，A.J. Power，T. Tsujishita，H. Watanabe和J. Worrell，余代数范畴的结构，理论计算机科学260（2001）87[5] Jacobs，B.，和J·鲁滕A tutorial on（co）algebras and（co）induction，Bulletin of theEuropean Association of Theoretical Computer Science62（1997），222[6] 杰奎琳·雷，助理检察官，S.A. Schneider和F.W.范德雷杰，[7] 凯利，通用汽车，A unified treatment of transfinite constructions for free algebras，freemonoid，colimits，associated sheaves，and soon. Bulletin Australian Mathematical Society22（1980），1-83.[8] 凯 利 ， 通 用 汽 车 ， 和 A.J.Power ， Adjunctions whose counits are coequalizers ， andpresentations of fennitary monads，Journal of Pure and Applied Algebra89（1993），163[9] Kick，M.，时间过程的双代数建模，[10] Kick，M.，“时间过程的数学模型”博士毕业论文，爱丁堡大学，2003年。[11] Lenisa，M.，A.J. Power和H.孙文，张文生，等.核函子的分布性，核函子的点和余点，单子和余单子，计算机理论电子笔记33（2000）.[12] Makkai，M.，和R.Pare，[13] Nicollin，X.，和j.Sifakis，An overview and synthesis of timed process algebras，[14] 鲍尔，AJTowards a theory of mathematical operational semantics，Electronic Notes inTheoretical Computer Science82.1（2003）.[15] 鲍尔，AJ和H. Watanabe，Combining a monad and a comonad，Theoretical ComputerScience280（2002），137[16] 斯特里特河Monads的形式理论，Journal of Pure and Applied Algebra2（1972），149-168。[17] Turi，D.，和G.D.李晓云，《数学运算语义学》，[18] 王玉，异步代理的实时行为，[19] Worell ， James ， Terminal sequences for accessible endofunctors ， Electronic Notes inTheoretical Computer Science19（1999）.