互模拟证明方法及其在共代数理论中的应用

理论计算机科学电子笔记164（2006）105-119www.elsevier.com/locate/entcs一种有效的共代数互模拟证明方法罗凌云中国科学中国北京8718信箱，邮编：100080中国科学院研究生院北京玉泉街19号，邮编：100039摘要互模拟“最多-。. .“技术提供了一种有效的方法来减轻证明两个过程的双相似性的工作量。本文发展了一种新的和直接的方法来推广这一套理论的“高达-。. .“原则对余代数理论的建立起了重要作用。 引入了一致函数的概念，Sangiorgi声音函数的推广。 然后，为了证明在一个关系中只有双相似对，找到一个从它到它的图像在某个相容函数下的“提升”的态射就足够了。一个例子表明，在赋范BPA的每一个自互模拟正是这样一个关系。更重要的是，我们研究了跨度互模拟和参照互模拟之间的联系。因此，λ-互模拟被我们的新原理所覆盖关键词：互模拟“最多-. . . ”, coalgebra,1介绍根据Milner根据定义，互模拟关系中的一个对在一步之后到达的新对也必须在这个关系中这似乎太死板了。因此，验证过程可能相当复杂。不过，在一些特殊情况下，限制可以放松。为了保证一个关系中对的双相似性，它们的导数不需要再次在这个关系中。例如，CCS [ 8 ]中的互模拟后来，Sangiorgi提出了一个通用的互模拟证明方法，用于标记转换系统（LTS）[10]。引入了声音功能的概念，因此，在中国NSF基金604963201电子邮件地址：luoly@ios.ac.cn1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2006.06.007106L. Luo/Electronic Notes in Theoretical Computer Science 164（2006）105为了证明某个对的双相似性，找到一个包含它的关系并表明这个关系在某种声音函数下发展到这个理论是强大的。许多已有的互模拟证明方法都可以用它来解释，如上述两种。此外，还提出了一些新的声函数.例如，从“向上到上下文”技术中提取的上下文功能在过去的几年里，余代数理论的研究一直受到人们的关注[1，11，4，9]。许多系统都有自己的范畴描述，包括LTS和自动机，它们都可以被看作是余代数。相应地，共归纳的定义和规则进行了研究。在余代数理论中有三种主要的方法来定义互模拟。传统的一个是由Aczel和Mendler首先介绍的[1]，处理关系。一个关系是互模拟的，如果它是一个F-余代数的载体，使得两个投射函数π1和π2F-余代数同态; [11]给出了一个非常相似但更一般的定义，而不是关系，这也出现在[7]和[2]中。我们在这里称之为跨互模拟;最后一个使用了“关系提升”的概念对于集合上的函子F，互模拟就是一个Rel（F）-余代数，本文称之为ref-互模拟。类似地，为了减轻互模拟证明，一些共归纳证明原则出现在文献中。Lenisa在[7]中研究了集合论余归纳与余代数余归纳之间的关系. 通过采用分配律λ：TFFT，她提出了一个共代数共归纳. .”上述方法。基于这一思想，在跨度互模拟的基础上提出了λ-互模拟的概念[2]. λ-互模拟不是标准的跨距互模拟，因为它是FT-余代数的载体，而不是F-余代数的载体。在一定条件下，每个λ-互模拟都只包含互相似对.然而，声功能和它的范畴对应物都有自己的缺点。Sangiorgi例如，对于更重要的本文进一步研究了共归纳规则的范畴描述。我们放弃了分配律λ的概念，而引入相容函数.它是一种更一般和直接的共代数证明方法，基于参考互模拟，更倾向于集合论定义。这个定义非常简洁和具体，因为避免了许多涉及的概念。换句话说，我们的新原则将Sangiorgi的方法论推广到了Coalge- bra理论，但保留了它的优点。此外，我们还证明了声函数和λ-互模拟都属于这个新原理。每个声音函数都与F和（α，α）一致，其中FX=P（X），α表示L. Luo/Electronic Notes in Theoretical Computer Science 164（2006）105107对于F-余代数和上的每个λ-互模拟R，总能找到一个与F和（αX，αY）相容的函数g使它包含在一个标准的ref-互模拟中.此外，借助函数跟踪和反射，建立了跨互模拟与参照互模拟之间的一一对应关系。本文的其余部分组织如下：在第2节中，我们给出了关系提升和自反互模拟的定义。第三节介绍了相容函数第4节讨论了参照互模拟和跨度互模拟之间的关系，这有助于第5节证明λ互模拟也可以被我们的原理所覆盖。最后在第6节中，给出了结论和与相关工作的比较，以及未来的工作。在本文的其余部分，我们定义为集合范畴，并使用π1，π2作为关系上的投影函数。若F是明确的，则用<$X，α<$来表示F-余代数<$α：X−→F（X）<$.2预赛在这里我们采用[6]中的定义2.1关系提升对于集合和二元关系的范畴，我们写Sets和Rel。Rel中从R<$X1×X2到S<$Y1×Y2的态射是函数对f1：X1−→Y1，f2：X2−→Y2，它们满足以下性质：（f1，f2）R（x1，x2）=S（f1（x1），f2（x2））. 虚线箭头（如−−→）用于表示他们Rel（F）RelRel套×套F×F套×套Fig. 1.关系提升定义2.1对于内函子F：Sets−→Sets，关系提升是映射Rel（F）：Rel−→Rel，如图1所示。它在关系<$π1，π2<$：R <$→X1×X2为：Rel（F）（R）={u，v∈ F X1× F X2|F π1（w）= u且Fπ2（w）= v}.注：对于任何归纳定义的多项式函子F，相应的Rel（F）也以归纳的方式给出（参见[5]中的例子108L. Luo/Electronic Notes in Theoretical Computer Science 164（2006）105命题2.2满足以下性质：(i) 如果R<$S，则Rel（F）（R）<$Rel（F）（S）。(ii) 设R <$X × Y，S <$Y × Z，则Rel（F）（S <$R）= Rel（F）（S）<$Rel（F）（R）.(iii) Rel（F）（Rop）=（Rel（F）（R））op（Rop是R的逆）。（αX，αY）（αX，αY）(iv) 设R，S，T<$X×Y，若R−→Rel（F）（S）且S<$T，则R− →Rel（F）（T）。（αX，αY）(v) 设Ri，Si<$X × Y（i = 1. n）对于任意n，如果Ri− → Rel（F）（Si），则nR（αX，αY）n0i−→Rel（F）（0 Si）.前三个属性引自[6]，最后两个属性很容易从它们中得出2.2参照互模拟定义2.3关系R<$X×Y是F-余代数上的一个参互模拟（αX，αY）如果R−→Rel（F）（R），即对所有x∈X和y∈Y，R（x，y）=<$Rel（F）（R）（αX（x），αY（y））.换句话说，R是一个ref-互模拟，如果它是一个Rel（F）-余代数。余代数αX，αX与自身之间的参互模拟称为上的参互模拟。X，α，RX×Y（αX，αY）αX×αYRel（F）（R）F（X）×F（Y）图二. 参照互模拟设X，Y是集合，F是集合上的闭函子.对于余代数<$X，αX<$X和<$Y，αY<$X，命题2.2（v）确保了ref-互模拟是并闭的，因此存在一个最大的ref-互模拟关系，称为双相似性，写作Participate。特别地，余代数αX，αX和自身的双相似性记为α X.例2.4考虑最常见的有标号跃迁系统，比如说：，A<$，则它可以看作是一个F-余代数<$S，α<$其中FS=P（S）A且<$a ∈A.SJ∈α（s）（a）惠s-a→SJ.一个关系R<$S×S是R<$S上的一个互模拟，α<$ i <$i是Milner定义的一个强互模拟L. Luo/Electronic Notes in Theoretical Computer Science 164（2006）105109• xaJJaJ J J−→x ⇒ ∃y .y−→y且（x，y）∈ R.• y−a→yJxJ. x−a→xJand（xJ，yJ）∈R.110L. Luo/Electronic Notes in Theoretical Computer Science 164（2006）105−−−→B.3相容函数定义3.1设F是集合上的函子，且<$X，αX<$和<$Y，αY<$是F-余代数。 一个函数g：P（X×Y）−→ P（X×Y）被称为与F和（αX，αY）相容，如果<$R，S<$X×Y，（αX，αY）（αX，αY）R<$S<$（R− →Rel（F）（S））<$（g（R）− →Rel（F）（g（S）。有时我们只说g是相容的，如果不需要显示相关的函子和态射。（αX，αY）要知道Rel（F）（S）<$FX×FY，所以态射−−→非常不同从[ 10 ]中的级数关系然而，在应用此定义通过简单地将F取为FX=P（X），我们将发现R（αX，αY）Rel（F）（S）当且仅当R>−→S，如果我们在结论中加上g（R）<$g（S），则g为是一个健全的功能。对于另一个方向，每个声音函数都是与F和（αX，αY）一致的函数。实际上，当g（R）→g（S）被加时，我们也可以证明相容函数在某些组合运算下是闭的，如复合和并。（αX，αY）命题3.2如果R−→Rel（F）（g（R））和g：P（X×Y）−→P（X×Y）是与F和（αX，αY）一致，则R参与。（αX，αY）证据 找到一个关系B使得R <$B和B − → Rel（F）（B）就足够了。首先，我们归纳地构造一个关系序列Bi（i≥0）B0=RBi+1=Big（Bi）（i≥0）（αX，αY）接下来证明，如果Reli≥0，Bi−→Rel（F）（Bi+1）：（αX，αY）（αX，αY）如果i= 0，则R−→Rel（F）（g（R））给出R−→Rel（F）（R<$g（R）），因为提议2.2 ㈣。（αX，αY）当i>0时，Bi−1− →Rel（F）（Bi）直接由归纳hy得出（αX，αY）假设由于Bi−1根据定义是Bi，因此g（Bi−1）− →Rel（F）（g（Bi））（αX，αY）因为g和F是一致的使用命题2.2（v），Bi−1<$g（Bi−1）− →（αX，αY）Rel（F）（Big（Bi）），即Bi− →Rel（F）（Bi+1）。因此，∞B（αX，αY）（2）命题2.2（v）0i−→Rel（F）（1i再很明显，∞B=∞B，所以我们可以通过让∞B=0i1i0iL. Luo/Electronic Notes in Theoretical Computer Science 164（2006）105111Q112L. Luo/Electronic Notes in Theoretical Computer Science 164（2006）105→RE x示例3.3D定义一个函数：P（X×X）−→P（X×X）asg（R）=R。（α是αX上的双相似性，α是关系合成）。我们可以证明g与F和（α，α）是相容的。（α，α）设R<$S且R−→Rel（F）（S）。 对任意（x，y）∈g（R），必有设x<$xJ，（xJ，yJ）∈R，yJ<$y，则产生（α（x），α（xJ））∈Rel（F）（R），（α（XJ），α（YJ））∈Rel（F）（S），（α（YJ），α（y））∈Rel（F）（S）. 然后（α（x），α（y））∈Rel（F）（n）<$Rel（F）（S）<$Rel（F）（n）=Rel（F）（n<$S<$n）（p（α，α）2.2 ㈡）。因此，g（R）− →Rel（F）（g（S））。很明显，如果X是CCS过程，α代表跃迁关系，则遵循Milner在研究赋范BPA过程互模拟等价的可判定性问题时，Caucal给出了一个简洁的证明，证明了这个问题是可判定的[3]。他引入了自互模拟的概念，并证明了自互模拟中的所有对都是互模拟等价的。现在，我们给出了另一种证明它呼吁一致的功能。例3.4BPA过程可以看作是顺序标记重写系统中的状态，其中• V是变量的有限集合;V的元素被称为状态。• 标签是一个有限的标签集• ΔV××V是重写规则的有限集合，写为xa y对于x，a，y∈Δ，当通过以下预定义规则确定时：如果x→ay，则xz→ayz。因此，BPA系统也可以被视为F-余代数<$V <$，α<$，其中F（X）=对于任意x∈ V和z，xJ，yJ∈ V<$，P（X）<$和α满足以下性质：xJ∈α（x）（a）惠（x，a，xJ）∈Δ，和yJ∈α（xJ）（a）<$yJz∈ α（xJz）（a）.不存在t<$x∈V<$.<$x=x=x <$，nd<$a∈<$.α（<$）（a）=<$. LetIdf={（f，f）|f∈F（V）}，则可以检查对于V上的任何关系S，IdfRel（F）（g（S））。对于任意二元关系R×V，我们记为→最小预同余↔对于包含R的序列复合，用R表示其对称闭包→ ↔∗↔R，记R为R的自反传递闭包。在R上定义一个函数g使得g（R）是从以下规则导出的最小集合（x，y）∈R1.（x，y）∈g（R）2.（x，x）∈g（R）（x，y）∈g（R）3.（y，x）∈g（R）（x，z）∈g（R），（z，y）∈g（R）4.（x，y）∈g（R）（x，y）∈g（R）5.（z1xz2，z1yz2）∈gL. Luo/Electronic Notes in Theoretical Computer Science 164（2006）105113（R）114L. Luo/Electronic Notes in Theoretical Computer Science 164（2006）105↔∗证据 事实上， 我们可以 容易 看到 g（R）=R.在[3]中，R被称为自-互模拟，如果R>−→g（R）。 如前所述，此条件相当于（α，α）对于这个例子，R−→Rel（F）（g（R））。 所以如果g与F和（α，α）相容，我们还可以得到Caucal（α，α）接下来我们证明这个结果，证明如果R<$S和R− →Rel（F）（S），（α，α）则g（R）−− −→Rel（F）（g（S））。对于所有（x，y）∈g（R），任务是通过规则归纳来证明（α（x），α（y））∈Rel（F）（g（S））：(i) 归纳假设给出（α（x），α（y））∈Rel（F）（S）.由于S<$g（S），则（α（x），α（y））∈Rel（F）（g（S））。(ii) 平凡的，因为Idf<$Rel（F）（g（S））。(iii) 由于（α（x），α（y））∈Rel（F）（g（S）），通过IH，（α（y），α（x））∈（Rel（F）（g（S）op=Rel（F）（（g（S））op）=Rel（F）（g（S））由命题2.2（iii）和g（S）的对称性得出。(iv)由IH，（α（x），α（z））∈Rel（F）（g（S））和（α（z），α（y））∈Rel（F）（g（S）），所以（α（x），α（y））∈Rel（F）（g（S））<$Rel（F）（g（S））=Rel（F）（g（S）<$g（S））=Rel（F）（g（S））因为g（S）是传递的。(v) 只要找到一个χ∈F（g（S）），使得Fπ1（χ）=α（z1xz2），且Fπ2（χ）=α（z1yz2）。有四个分支需要考虑：• z1/=1/ 其中，α（z1）（a） ={ZJXZ2|zJ∈α（z1）（a）}1 1和α（z1yz2）（a）={ZJYZ2|ZJ∈α（z1）（a）}. 定义χ∈ P（g（S））为χ（a）=1 1{（zJxz2，zJyz2）|zJ∈α（z1）（a）}. 很容易检验Fπ1（χ）=α（z1xz2）1 1 1Fπ2（x）=α（z1yz2）.• z1=100x- 是的 IH给出了使得Fπ1（χJ）=α（x）的<$χJ∈F（g（S）），Fπ2（χJ）=α（y）。 定义χ（a）={（x1z2，y1z2）|（x1，y1）∈χJ（a）}则Fπ1（x）=α（xz2）和Fπ2（x）=α（yz2）。• z1= x=z2/=。它保持y =（如果y/=，则a∈ s.t. α（y）（a）/= α，由于α（x）（a）= α，不能找到χ∈ P（g（S））α使得Fπ1（χ）= α（x）和Fπ2（χ）= α（y），这与IH）相矛盾.因为Idf<$Rel（F）（g（S）），（α（z2），α（z2））∈Rel（F）（g（S））.L. Luo/Electronic Notes in Theoretical Computer Science 164（2006）105115• z1=x=z2=x。 则y=0。 （α（f），α（f））∈Rel（F）（g（S））.Q我们发现规则5在这里的特定情况下隐含着一个116L. Luo/Electronic Notes in Theoretical Computer Science 164（2006）105事实上，Sangiorgi指出，对于任何签名格式的一元De Simone格式规则，所有的上下文函数都是合理的。4与跨度互模拟的设R，X，Y是集合，r1，r2是函数.r1：R−→X和r2：R−→Y，则<$R，r1，r2<$称为X和Y之间的跨距。定义4.1对于函子F：Sets−→Sets，F-余代数<$X，αX<$X和<$Y之间的跨距互模拟，α Y<$X和Y之间的跨距<$R，r1，r2<$，使得存在一个箭头η将r1和r2转化为同态：Xr1αXRr2YηαYF（X）F（R）Fr1Fr2F（Y）图三. 跨互模拟定义跨距R，r1，r2的像为：I（R，r1，r2）={（r1（z），r2（z））|z∈R}，所以象函数将跨距<$R，r1，r2<$$>变为关系I（R）<$X × Y。为了简单起见，当r1，r2由上下文实现时，我们将I（R）写为I（R，r1，r2）的缩写此外，我们还定义了一个迹函数和一个反射函数来表示跨度与其图像之间的关系。在每个跨距R，r1，r2，r上，定义traR：R−→ I（R）为traR（z）=（r1（z），r2（z））。对于另一个方向refR：I（R）−→R，定义refR（x，y）=z使得x=r1（z）和y=r2（z））。注意，在定义refR时，I（R）的性质保证了这样的z. 当有多个时，refR只选择其中一显然，一个关系T<$X×Y决定了一个跨度s. t。I（T）=T和refT=IdT。命题4.2可以证明traR是满射的，refR是内射的，满足：• πi=rirefR（i= 1， 2）• ri=πitraR（i=1，2）或者，用图画的方式，下面的图表可以互换：L. Luo/Electronic Notes in Theoretical Computer Science 164（2006）105117R1RR2参见RX YI（R）RXtraRYI（R）见图4。 ref和tra实际上，回想一下关系提升的定义，我们可以发现Rel（F）（R）=I（<$F（R），Fπ1，Fπ2<$）。借助上面定义的函数，可以探索参考互模拟和跨度互模拟之间的直接联系。命题4.3假设R，r1，r2，R，S，s1，s2是X和Y上的跨距，F是一个函数，（αX，αY）在集合论中，证明了I（R）−−−→Rel（F）（I（S））i ≠存在一个箭头η使下面的图可交换：Xr1αXRr2YηαYF（X）F（S）F1F2F（Y）（αX，αY）图五、I（R）− →Rel（F）（I（S））证据定义η（z）= FrefS∈refF（I（S））（αX（r1（z）），αY（r2（z）.它遵循Fs1πη（z）=Fs1<$FrefS<$refF（I（S））（αX（r1（z）），αY（r2（z）=F（s1<$refS）<$refF（I（S））（αX（r1（z）），αY（r2（z）=Fπ1<$refF（I（S））（αX（r1（z）），αY（r2（z）（π1=s1<$refS）=π1（αX（r1（z）），αY（r2（z）（π1=Fπ1<$refF（I（S）=αX（r1（z））f：f（x，y）∈ I（R），交换性给出：αX<$r1（refR（x，y））=Fs1<$η（refR（x，y））=F（π1<$traS）<$η（refR（x，y））=Fπ1（FtraSπn（refR（x，y）。π1π2R2R1π1π2118L. Luo/Electronic Notes in Theoretical Computer Science 164（2006）105αY<$r2（refR（x，y））=Fs2<$η（refR（x，y））=F（π2<$traS）<$η（refR（x，y））=Fπ2（FtraSπn（refR（x，y）。L. Luo/Electronic Notes in Theoretical Computer Science 164（2006）105119由于αX<$r1（refR（x，y））=αX<$π1（x，y）=αX（x）和αY<$r2（refR（x，y））=αY<$π2（x，y）=αY（y），我们找到了一个z=FtraS<$η（refR（x，y））∈F（I（S））使得：αX（x）=Fπ1（z）和αY（y）=Fπ2（z），则（αX（x），αY（y））∈Rel（F）（I（S））由定义直接推出.Q特别地，当R=S时，则R是展互模拟，i ∈I（R）是参互模拟。有趣的是，如果R是一个参考互模拟，它也是一个跨度互模拟，因为I（R）=R。5λ-互模拟与相容函数从第3节的例子中，我们注意到，一些有用的证明技术，不能涵盖的λ-互模拟模式很容易表达和证明在我们的框架。现在我们继续证明每个λ-互模拟也可以用这种新的共代数证明方法来表示。首先，让定义5.1（一般）设F，T：集合→集合是函子。给定一个自然变换λ：T（Id×F）<$FT，若存在箭头η，β X和β Y，则跨距<$R，r1，r2<$是F-余代数<$X，αX <$，αY<$的λ -互模拟，使得图6中的下一个图交换（r1|βX是βX<$Tr1的表示法，r2也是如此|βY）：TIdX，αXTXβXTyTIdY，αYβYT（X×FX）XλXαXr1Rr2∃ηYT（Y×FY）αYλYFTXF（X）F（TR）F（Y）FTYF βXFr1|βXFr2|βYF βY见图6。λ互模拟在Bartels[2]的原始定义中，λ被称为分配律，并引入了“λ -双代数”和“上至β同态“等结构在这里，我们避开了这些概念，而更多地集中于基本部分。命题5.2对F-余代数<$X，αX<$X上的每个λ-互模拟<$B，b1，b2<$B，<$Y，αY<$，总存在一个函数g：P（X×Y）−→ P（X×Y），使得g是120L. Luo/Electronic Notes in Theoretical Computer Science 164（2006）105（αX，αY）与F和（αX，αY）一致，且I（B）− → Rel（F）（g（I（B）。证据 定义一个关于关系R X × Y的函数g为：g（R）= I（πTR，π1|βX，π2|βY β）。则对X和Y上的任意跨距B，b1，b2∈B，g（I（B））=I（T（I（B）.不难证明，I（λTB，b1|βX，b2|βY）= I（T（I（B）），π1|βX，π2|βY≠），所以g（I（B））= I（TB）。假设λ B，b1，b2λ是λ-互模拟，（αX，αY）I（B）−− −→Rel（F）（I（TB））（αX，αY）根据第4.3条。 换句话说，I（B）−→Rel（F）（g（I（B）。接下来我们证明g与F和（αX，αY）是相容的。对于两个关系R和S，如果R<$S和下面的左图交换，我们必须找到一个使右图也交换的ηJXπ1Rπ2YXπ1|βX TRπ2|βYYαXηαYαXηJαYF（X）F（S）F（Y）F（X）F（TS）F（Y）Fπ1Fπ2Fπ1|βXFπ|βY见图7。 左图的交换性隐含右图的交换性设ηJ=λS<$T<$IdR，其中IdR：R−→S。 因为R是S，所以它是定义良好的，很明显，π1<$IdR=IdX<$π1。图7左图的交换性给出Fπ1<$η=αX<$π1。它如下：（π1×Fπ1）πIdR，η=πIdX，αXππ1T（π1×Fπ1）Tπ1λX<$T（π1×Fπ1）<$T<$IdR，η=λX<$T<$IdX，αX<$Tπ1FTπ1<$λS <$T<$IdR，η=λX<$T<$IdX，αX<$Tπ1F βX<$FTπ1<$λS<$T<$IdR，η=F βX<$λX <$T<$IdX，αX<$T<$1F βX<$FTπ1<$λS<$T<$IdR，η=（αX<$βX）<$Tπ1L. Luo/Electronic Notes in Theoretical Computer Science 164（2006）105121Fπ1|βX <$ηJ= αX<$π1|βXFTπ1<$λS=λX<$T（π1×Fπ1）和αX<$βX=FβX<$λX <$T<$IdX，αX<$分别用于产生第四和第六方程其正确性是122L. Luo/Electronic Notes in Theoretical Computer Science 164（2006）105由图8的交换性保证(Be意识到右一个是由前提暗示的，左一个是由于λ是自然变换的事实λST（S×FS）FTSTXTβXT（X×FX）XT（π1×Fπ1）FTπ1λXαXT（X×FX）λXFTX图8.第八条。自然变换与双代数FTXF βXFX由于Fπ2|βY<$ηJ= αY<$π2|βY 也成立的对称性，证明完成。由于上述定理，命题3.2承诺存在一个参考-∼ ∼ ∼ ∼互模拟使得I（B）<$B= I（B）。 因为B也是一个跨互模拟，我们得到了与[2]中推论5.6相同的结果，使得如果B是λ-互模拟，∼在<$X，αX<$和<$Y，αY<$之间，则存在（标准）跨度互模拟B∼其中I（B）为I（B）。接下来，在[2]中挑选一个例子来说明上面的定理：例5.3假设F是集合上的函子，使得FX=R ×X（R是实数的集合）。则存在一个最终的F-余代数<$Rω，<$h，t<$h.由于共归纳法则，可以定义两个函数Rω×Rω−→ Rω，满足：h（στ）=h（σ）+h（τ），t（στ）=t（σ）<$t（τ），h（σ<$τ）=h（σ）<$h（τ），t（σ<$τ）=（h（σ）<$t（τ））<$（t（σ）<$τ），其中，+、分别表示实数上的标准“加”和“乘”运算符。很明显，和都是结合的和交换的。在下文中，我们使用σ0来证明h（σ），使用σJ来证明对于任何σ的t（σ），类似地，使用其他流。为了显示在上的分布性，构造一个关系式B={（σ（τρ），（στ）（σρ））}，并且在任何关系R上定义函数g为：g（R）={（α1<$α2，β1<$β2）|（α1，β1），（α2，β2）∈R}.有两个事实1. B（h，t，h，t）− →Rel（F）（g（B））。L. Luo/Electronic Notes in Theoretical Computer Science 164（2006）105123对于任意一对（x，y）∈B，其中x=σ（τρ），y=（στ）（σρ），由定义可知，h，t（x），h，t（y）分别等于下列两个元素（σ0<$τ0+σ0<$ρ0），（σ0<$（τJ<$ρJ））<$（σJ<$（τ<$ρ）），（σ0 <$τ0+ σ0<$ρ0），（（σ0 <$τ J）<$（σ0<$ρJ））<$（（σJ <$τ）<$（σJ <$ρ））。则h（x）=h（y）且由于（σ0∈g（B）. 设z=（（σ0<$τ0+σ0<$ρ0），（t（x），t（y））∈F（g（B）），则有：其中，f（x）=Fπ1（z），f（y）=Fπ2（z）。2. g与F和（f，h，t，h，t）一致对于任何T和T（h，t，h，t）−→Rel（F）（S），如果（x1<$x2，y1<$y2）∈g（T），因为对于（x1，y1）∈T和（x2，y2）∈T，我们有h，th，t（y1<$y2）=（h（y1）+h（y2），t（y1）<$t（y2））。（h，t，h，t）由于τi=1，2，（xi，yi）∈T且T −→Rel（F）（S），则h（xi）=h（yi）和（t（xi），t（yi））∈S. 因此，在本发明中，h（ x1）+h（ x2）=h（ y1）+h（ y2）且（t（ x1）<$t（ x2），t（ y1）<$t（y2））∈g（S）成立，从而给出，（h（x1）+h（x2），（t（x1）<$t（x2），t（y1）<$t（y2）∈F（g（S））和（g（S））∈Rel（F）（g（S））.毕竟，σ<$（τ<$ρ）<$（σ<$τ）<$（σ<$ρ）。再加上前提是<$Rω，<$h，t<$r是一个最终余代数，σ<$（τ<$ρ）=（σ<$τ）<$（σ<$ρ）成立.从上面的例子中，我们还可以发现，我们的共代数互模拟证明方法不仅适用于迁移系统，而且可以应用于其他结构。6结论本文提出了一种新的共代数互模拟证明方法。在互模拟的基础上，提出了相容函数对共归纳规则进行分类描述的工作是由Lenisa和Bartels开始的由于Bartels在他的论文[2]中声称Lenisa124L. Luo/Electronic Notes in Theoretical Computer Science 164（2006）105在本文中，λ-互模拟被我们的原理所覆盖，我们认为我们的工作在这个方向上取得了进展我们的相容函数更一般的原因是我们放弃了使用分配律λ：TFFT，它给结构附加了比所需更多的信息。虽然本文中我们定义为范畴集，但相容函数可以很容易地推广到任何范畴C。注意，在集合中，我们只在关系上定义一致函数，当遇到跨度时，通过研究它们之间的关系，将跨度转换为关系。 为什么不直接在跨度实际上，这可以通过在com上处理事情来轻松完成（αX，αY）变图例如，我们可以用图5代替R−→Rel（F）（S）因此，我们可以在任何类别C上得出命题3.2的对应命题。今后的工作有几个方向：• 如第3节所述，我们有理由相信相容函数在某些组合运算下是封闭的，我们将找到更多有趣的例子来说明这一观点。• 在他的论文的最后一部分，桑吉奥吉作出了一个小概括尊重职能，从一个方面的不动点理论。在这种情况下，存在着一些不能修正到范畴框架中的声音函数的概念。例如，如果在一些互模拟的定义中使用了数量化的“边条件”或“边条件”，由于范畴论的限制，我们将无法提供它们的共代数描述。这个问题也在[7]中提出• 我们在这里考虑的互模拟实际上是强互模拟。未来工作的一个方向是研究弱互模拟。如果能找到一个合适的范畴框架来表示弱双模拟，那么相关的共归纳规则将更容易得到。确认我想感谢刘欣欣阅读本文的草稿并提出改进建议。此外，与吴志林、周翔和金毅的讨论对我准备这篇论文有很大引用[1] P. Aczel和N.门德勒一个最终余代数定理在Category Theory and Computer Science，D.H.Pitt etal.eds.，Springer LNCS 389：357-365，1989年。[2] F.巴特尔斯广义共归纳。CMCS'01，A.Corradini，M.Lenisa和U.Montanari编辑，ENTCS 44，2001年。[3] D.[医]古柯属Graphesanoni quuesd egraphesal g'ebriques.Iinfor matiq ue T h'eoriq u etApplications（RAIRO），24（4）：339-352，1990.