结构操作语义与模态逻辑的组合及其证明机制

理论计算机科学电子笔记264（2010）155-175www.elsevier.com/locate/entcs结构操作语义学与模态逻辑Bartek Klin1剑桥大学、华沙大学摘要先前介绍的结构操作语义的双代数方法与共代数模态逻辑的组合重新检查和改进的某些方面。首先，基于对模态逻辑的理解，给出了主组合性定理的一个更抽象的概念性证明的切片范畴中的余代数。其次，提供了一个更具体的理解定理的假设，证明组合性相当于找到两个谓词提升集合保留字：结构操作语义学，模态逻辑，余代数1介绍过程等价的组合性是结构操作语义学（SOS;参见例如[1，7]）理论中的重要问题。特定语言的组合性证明通常是乏味的，因此已经证明了大量的元结果，通过使操作规范受到某些语法限制（称为格式）来保证各种等价的组合性。在[28]的双代数框架中，在余代数的抽象层次上解释了从SOS规范诱导行为良好的转移系统的过程。 在那里，一个著名的SOS格式称为GSOS被理解为一个 行为和语法内函子之间的一种分配律。在一般性水平上解释了全球同步轨道系统引起的规范的LTS双相似性是组成性的这一事实。将该方法扩展到等价而不是双相似性的一种方法是将它们理解为某些模态逻辑的逻辑等价，并使用开发的模态逻辑的一般共代数方法，例如，在[4，5，10，12，16，18，19，23，27]中。1这项工作得到了EPSRC赠款EP/F042337/1的支持。电子邮件地址：klin@mimuw.edu.pl1571-0661 © 2010 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2010.07.019156B. Klin/Electronic Notes in Theoretical Computer Science 264（2010）155在[15，17]中，提出了双代数方法与共代数模态逻辑的这种组合。为了证明由某种逻辑在从SOS规范导出的转换系统上定义的等价是一个同余，需要为逻辑公式配备一个共代数行为，并在该行为上展示一个反映分配律模型的逻辑语法的“逻辑分配律”- SOS规格。从某种角度来看，[15，17]的数学经济性和实际可用性都不完全令人满意。首先，主要的组合性结果的证明，尽管是初级的，但涉及大量的图表追踪和归纳证明，并且通常不是很有启发性。第二，也许更痛苦的缺陷是，没有提供对逻辑公式的共代数行为的直观的一般理解。虽然某些特定类型的逻辑行为的逻辑分配律以一种吸引人的、类似于SOS的方式呈现，但对于其他类型的行为，没有找到对这些律的具体理解。此外，除了胡乱猜测之外，没有给出为逻辑公式寻找行为函子的指导方针。检查候选逻辑分配律是否正确涉及复杂自然变换的大量计算，远远超出了对公式和过程的普遍理解本文试图在一定程度上消除这两个缺陷。 首先，对[15]的主要组合性定理提供了一个更抽象的概念性证明（在此过程中，该定理被温和地推广）。 为此目的，模态逻辑在余代数中的解释被理解为从余代数的范畴到一个附加子的切片范畴的函子。然后，通过伴随提升定理，组合性定理从提升该函子到涉及进程语法的结构。其次，提供了一个重要的例子，其中过程和公式都生活在集合范畴的组合性定理的具体理解。公式的余代数行为用谓词提升来解释[22，27]，逻辑分配律是两个提升集合之间的句法分配律。证明逻辑等价的组合性相当于为进程语法找到一个合适的提升集合，以及一组涉及这些提升的方程。由于谓词提升的概念已经被很好地研究和理解，这个公式应该有助于理解我们对逻辑组合性的双代数方法本文的结构如下。在第二节和第三节中，简要回顾了SOS和余代数模态逻辑的双代数方法。第四节研究了片范畴中的内函子、代数和余代数，最后证明了主复合性定理。第五节用谓词提升的概念给出了定理的具体解释。最后，第6节解释了上述两个缺陷在本公式中如何在某种程度上持续存在。一些证据，不必要的主线推理，被降级到附录。对于那些不太关心组合性或SOS的读者来说，这篇论文的某些部分可能也会感兴趣。对于共代数模态逻辑的解释 在没有任何参与的情况下，B. Klin/Electronic Notes in Theoretical Computer Science 264（2010）155157⇒CλXP −PBX关于进程语法，阅读第3、4.1和4.2节就足够了。读者应该熟悉基本的范畴理论（[21]是一个标准的参考）和系统理论的共代数方法[26]。谢谢。作者感谢一郎Hasuo进行了许多有趣的讨论。2SOS和分配律在结构操作语义学的背景下，各种类型的转换系统通过使用推理规则的结构归纳来定义，并且在一些签名上具有封闭项作为状态。例如，给定一个固定的标签集合A，0→0xa→xJya →yJxya→xJyJ（一）（其中a的范围超过A）归纳地定义了文法上的封闭项t：：=0|一|t ≠ t（a ∈ A）.（二）在[28]中，这种情形用分布律和双代数表示在余代数中。例如，规则（1）定义了一个自然变换λ：λ B = B λ，其中λ是与文法（2）对应的集合上的多项式内函子，B=（ω）A，其中ω是有限幂集内函子; B-余代数是像有限A-标记的转移系统（LTS）。对于范畴上的任何内函子B和B，上述变换称为B上的内函子分配律，在B-余代数的范畴B-coalg诱导出一个内函子Bλ，在B-余代数的范畴B-coalg上诱导出一个内函子Bλ（XhBX）=<$X<$h<$BXλX B<$XBλ（<$XgX）=<$BX λB<$XBg BX和作为一个（分别）B）关于morphisms。很明显，λ提升了λ，Bλ提升了B，沿着相应的遗忘函子UB：B-coalg→ C和Uλ：B-alg→ C。很容易看出，一个λ-代数或一个Bλ-余代数由一个λ-代数g构成和具有相同载波的B-余代数h，使得图：XgX拉克什H，，BG（三）JBXλXBX上下班这样的结构被称为λ-双代数（带有载体X），λ-双代数态射是C中相应载体之间的映射，158B. Klin/Electronic Notes in Theoretical Computer Science 264（2010）155⇒P −×⇒××C ∈→λ-代数态射和余代数态射;这定义了λ-双代数的一个范畴λ有一个范畴的同构和一个遗忘函子的交换平方：λ-bialgU<$λB-coalgλ-bialg=λ-alg=Bλ-coalgUBλJ宾馆（4）J- algU.C.如果g是初始的λ-代数，则存在唯一的B-余代数h使得（3）交换，定义为从g到Bλ（g）的唯一λ-代数态射。结果是一个初始λ-双代数，如果λ对应于（1）中的SOS规范，则h对应于由该规范诱导的转移系统对偶地，如果一个最终B-余代数存在，它唯一地扩张到一个最终λ-双代数。这直接意味着：命题2.1对任意λ-双代数<$XgXH BX，唯一余代数从h到最终B-余代数的态射是从g到B-余代数的态射。当= Set时，给定余代数h：X BX的两个元素x，y X被称为观测等价的，如果它们被某些余代数态射所标识。特别地，如果存在最终B-余代数，则h上的观测等价是来自h的最终余代数态射的核关系。因此，命题2.1应用于初始双代数，意味着由指定诱导的转移系统上的观测等价是一个同余，如果指定对应于分配律λ。2命题2.1的实际适用性在这里是相当有限的，因为很少有有趣的例子实际上对应于上述的λ。在[ 28 ]中已经研究了更一般的定律，包括自由点内函子Id + ω和自由单子ω ω，以及余自由余点内函子Id B和余自由余单子Bω（假设它们存在）。特别地，Id B上的λ的分配律双射地对应于自然变换λ：λ（Id B）=对于B=（ω）A，这些对应于[2]充分研究的GSOS格式[ 3 ]中的SOS规范。类似地，Bω上Id + n的分配律对应于[ 28 ]中称为safe-ntree的格式。命题2.1对于这些更具表现力的定律中的每一个都被证明而没有太大的变化;事实上，人们不需要分别证明每一种情况，因为所讨论的每一种类型的定律都沿着[20]的路线导出了单子Bω上的单子分布律，命题2.1也适用于这样的定律，基本上是相同的证明。本文只给出了简单的分配律λ：λ B =B考虑。 这主要是为了在技术开发中简化演示和节省空间在第4节。一般情况下的分配律单子在comonads处理在一个完全类似的方式，但额外的检查，以确保2在[28]中，同余结果是针对余代数双相似性[26]而不是观测等价性来证明的;为此，需要B保持弱回调的额外假设B. Klin/Electronic Notes in Theoretical Computer Science 264（2010）155159⇒◦→E某些（co）自由（co）单子的存在性以及（co）单位与（co）乘法的相容性，最好留待本文的扩展版本3余代数模态逻辑一种基于反变函子的抽象方法来研究余代数的模态逻辑，已经引起了相当大的关注（例如，[4、5、10、12、16、18、27]）。假设一个加词SopET：C op →D，直觉上D的对象是公式的集合（或结构），C的对象是过程或状态的集合（或结构）。对于C上的一个内函子B，B-余代数的一个余代数模态逻辑由D上的一个内函子L（逻辑语法）和一个自然变换ρ：LT=LTBop（称为一个连接）给出在假设初始L-代数a：L Φ → Φ存在的情况下（直观上，它是逻辑公式的代数），逻辑（L，ρ）在给定余代数h：X → BX上的解释是通过沿着附接SopE T转置从a到ThρX的唯一L-代数态射s来获得的，如图所示：LTX，L，sLΦρXBX，，HXSΦJTBX日 JS=aΦJ（五）TX，， _SB其中左部分用C绘制，右部分用D绘制。例如C= D=Set和S=T=2−（其中2= {tt，ff}），B=（Pω −）A。B -余代数的Hennessy-Milner逻辑的迹片段（即LTS）具有由文法φ：：= T描述的语法|aρX（T）（b）=tt总是（6）ρX（y∈ b（a）. φ（y）= tt对于任何X。在B-余代数上证明（L，ρ）的解释（的核关系）是迹等价是很简单的.当寻找一个给定B的逻辑时，我们可以经常把注意力限制在某种形状的内函子上，而不失任何一般性。我们现在简单回顾一下[16]中的一个分析 连接ρ：LT= λ TBop 与 自 然 变 换 ρλ ： L= λ TB op 是 双 射 对 应 的 。TBopSopbyρ=ρSopLη，其中η：IdDT Sop是Sop的单位T. 如果坚持L是有限的，那么ρ通过TBopSop的有限限制因子。 后者是由一个余端公式定义的;不失一般性，可以用余积代替余端，对于D = Set，160B. Klin/Electronic Notes in Theoretical Computer Science 264（2010）155⇒∈→E⇒⇒ ×∧需要一个自然的转变ρ：L=TBSn×（−）n。n∈N对于S = T = 2 −和nTBSn的元素是函数β：B（2n） 2的 我们称之为n元B模态。(By Yoneda引理，这些双射对应于自然变换βY：（2−）n= 2B−，即，[27 ]第27话：因此，具有ρ的有限个L可以表示为B-模态的集合：族（Ln）n∈N集合Ln2 B2n 表示多项式内函子L=Ln ×（−）n，（7）n∈N其中ρ：L（2 −）=<$2 B−通过对每个n ∈ N和β ∈ L n的所有谓词提升βY：（2−）n=<$2 B−进行配对来定义。例如，B =（P ω −）A的跟踪逻辑由以下模态集合表示：L0= {T}，L1= {T ω−}|a ∈ A}，Ln= n，n > 1，其中T：B 1 → 2和n a ∈：B 2 → 2定义为：T（b）= tt总是，则a ∈ b（a）= tt ∈ tt。（八）我们顺便提到，这种逻辑方法支持与第2节中提到的类似的实际表达式问题。例如，虽然一个用于双相似性的无限Hennessy-Milner逻辑[8]版本可以这样定义，但它相当笨拙，具有无限多的任意性模态（见[16]）。这是因为基于S=T=2−的逻辑缺乏对命题连接词的内在支持，而命题连接词必须被编码为复杂模态的一部分避免这个问题的一种方法是改变所讨论的附加SopT（参见[12]的例子）。另一种方法是通过类比分配律和SOS，考虑更一般的联系类型例如，我们可以允许像ρ：LT=T（Id B）op这样的命题连接词，从而可以很容易地将诸如这样的命题连接词定义为简单的模态。我们甚至可以考虑像ρ：LT=T（Bω）op这样的连接来描述弱双相似性的Hennessy-Milner逻辑。同样，本文只考虑了简单的连接ρ：LT=TB;基于更复杂连接的余代数模态逻辑的问题留给了单独的研究。4逻辑等价的组合性我们的主要技术目标是修改命题2.1，以处理逻辑等价性，而不是观察等价性。我们将证明（定理4.6）在一定的假设下，对任意λ-双代数<$XgXhBX，在-逻辑（L，ρ）在h上的解释是g的一个n-代数态射。 为了公式化定理及其证明，我们介绍了一些基本概念和结果，B. Klin/Electronic Notes in Theoretical Computer Science 264（2010）155161• 在地图上，ρ^g，f=L g，Bf。^^^^D ↓D↓^^您的D ↓ → CD → D C → CD ↓ →D ↓（co）代数的一些性质。为了在某种程度上组织这个发展，我们将从函子的切片范畴开始，然后看看附加词SopET引入了什么额外的结构。4.1切片分类对于函子T：Cop → D，片范畴（D↓T）有：• 作为对象，三元组<$Φ，X，s <$，其中Φ ∈ D，X∈ C和s：D中的Φ →TX• 作为从φ Φ，X，s φ到φ Φ，Y，r φ的映射，对（g，f），其中g：Φ → φ在D中，f：Y→C中的X，使得ΦsTXgTf（九）J JT.Y.上下班存在明显的投影函子，记为<$1：（D ↓T）→ D和<$2：（D ↓T）→ Cop.如果D中存在初始对象0，则它确定完全嵌入0→：Cop →（D↓T），在对象上定义为0→（X）= 0，X， 0：0 →TX，其中箭头0通过初始性是唯一的，在箭头上定义为0→（g）= id0， g。很容易验证：第4.1节0→ 是左伴随的到2012：（T）op，附加的单位是恒等式的自然变换。Q切片内函子。假设内函子B：C → C和L：D → D，以及一个自然变换ρ：LT=TBop。这些成分定义了（D↓T）上的一个闭函子，记为ρ，如下所示：• 在ob<$，ρ^<$Φ，X，r<$=<$LΦ，BX，ρX<$Lr<$上很容易检查这是良好定义的和函式的。很明显，ρ沿着L的方向提升L，在这个意义上，L = L。类 似 地，ρ沿着ρ 2提升Bop。上一篇：（ 以这种方式产生的（T）将被称为（被ρ）切片。 不（T）上的每个内函子一般都是切片的，即使T是行为良好的（反例见附录）。然而：2.2.2考虑一个闭函子K：（ T） （ T），使得对于某些L：和 B：，K沿着λ 1提升L，沿着λ 2提升Bop。然后K以一种独特的方式切片。证据 见附录。Q紧接着，切片内函子在复合下是封闭的。然而，一个更直接的证明是可能的：对于ρ：LT=<$TBop和ρJ：LJT=<$T（BJ）op，很容易检查复合内函子ρρJ被以下切片162B. Klin/Electronic Notes in Theoretical Computer Science 264（2010）155ρ（BJ）op<$LρJ：LLJT =<$T（BBJ）op.（十）B. Klin/Electronic Notes in Theoretical Computer Science 264（2010）155163⇒ ⇒⇒⇒^ ^您的位置：^→ D → C→⇒^^D^P −让我们停下来思考一下ρ^-代数的意义：它们是→^CD^→切片自然变换。 假设连接ρ：LT = TBop和ρJ：LJT = TBJop。任意两个自然变换α：L=LJ和β：BJ=B，使得LTSρ zTBopαTTβop中中（十一）LJTρJ zTBjop换句话说，产生自然变换α②β：ρ= πρJ，定义为：α ② β<$Φ，X，s <$=<$αΦ，βX <$。（十二）不是每个切片内函子之间的变换都是这种形式的（关于反例，见附录）。 但是，在第4.2节中，我们将证明这是 如果T有一个左伴随。代数。给定一个联络ρ：LT = TBop，一个ρ-代数等价地是一个L-代数g：L ΦΦ in ，一个B-余代数h：XBX输入，以及映射s：ΦTX，使得图LΦLsLTXρX TBXgThJ J（十三）ΦsTX上下班此外，ρ-代数态射很容易被看作是一个L-代数态射和一个B-余代数态射对. 特 别 地，存在明显的投影函子<$1：ρ-alg → L-alg和<$2：ρ-alg →（B-coalg）op.B-余代数h（系统）与L-代数g（逻辑理论）一起在它们中解释（通过s）. 例如如果==Set且S=T= 2 −，函数s：Φρ-代数的载体中的TX就是Φ与X之间的关系。对于B=（ω）A和（L，ρ），由这个关系定义的X上的等价关系总是包含在h上的迹等价中，并且如果g是初始的，则与它重合。ρ-代数的态射反映了这些等价关系，隐含地存在于它们的载体中。这意味着当人们想研究余代数“直到”某种逻辑等价时，并且当寻找这些“直到”结构的显式余代数表示的任务（如[ 11 ]）看起来很困难或根本不值得时，人们可以尝试借助于在余代数中解释的理论来隐式地建模逻辑等价;这种观点在[ 23 ]中得到了提倡，本文可以被认为是它的一个例子应用。人们可以争辩说，正如结构运算语义学是对代数范畴中的余代数的研究一样回到正式发展：另一种解读 （13）S是L-代数态射换句话说， ρ-代数是L-之间的态射，有某种形状的代数。为了形式化这一点，观察ρ诱导函子T：（B-coalg）opL-alg定义为T（XhBX）=LTXρX TB XThT X在B-余代数上，T X在B-余代数态射上.164B. Klin/Electronic Notes in Theoretical Computer Science 264（2010）155^op（）有一个左伴随，并且该伴随的单位是单位元natural^ED → C环C → DEC → D D → C.bΦ）。b公式4.3ρ-alg=（L-alg↓T）。^证据我们已经基本上注意到了对象上的对应;形态学同样容易。Q推论4.4若初始L-代数存在，则投影函子<$2：ρ-alg →B-煤转型证据使用命题4.3并应用命题4.1。给定一个初始L-代数a，其左伴随记为a→。Q注意a→与来自ρ-alg的遗忘函子的复合：opa→Uρ^（B-煤g） ，β，zρ-algΠ2b（D↓T）几乎完全对应于B-余代数中的余代数模态逻辑的解释，如（5）中所构造的。实际上，在这个函子表示中唯一缺少的步骤是从初始L-代数转置语义映射s。 对于这最后一步，显然，函子T有一个左伴随是至关重要的;我们现在将用这个附加的假设进一步发展我们的理论4.2切片分类在本节中，我们假设T：op有一个左伴随Sop：op。附加项Sop的单位和计数T将被表示为η：Id=TS操作和：SopT=ID分别。 显然，Top：op是左伴随于S：op和ηop：TopS=Id和ηop：Id=STop是加法T op S的计数和单位。这种伴随情况意味着存在双射C（X，SΦ）=D（Φ， TX）自然在X∈ C和Φ ∈ D;我们将滥用符号，用− b表示这个双射的两边。划分的一个定义性质是片范畴的同构：（D ↓T）n=（C ↓ S）op（同构将对象nΦ，X，sn映射到X，，s作为函子的余代数模态逻辑。附加假设的一个直接结果是，可以将整个模态逻辑解释构造（5）表示为来自B-余代数范畴的函子g→（B-coalg）opzρ-algUρ，，Π2（D↓T）=（C ↓S）op（14）然而，当人们决定研究（D↓T）上切片内函子的余代数余代数 在4.1节考虑的情况下，余代数的范畴B. Klin/Electronic Notes in Theoretical Computer Science 264（2010）155165^^o p和：-coalg→（-alg）。2^^^^^D↓C↓^ ^您的位置：^ ^您的位置：^ ^您的位^ ^您的位置：^^因为切片内函子的结构一般比代数的结构少得多。考虑C上的闭函子和D上的Γ，以及4.1节中的连接：Γ T=T op。 一个π-余代数是D中的一个Γ-余代数h：Φ→ΓΦ，一个π-代数g：C中的<$X → X，以及映射s：Φ → TX，使得图<$Φ<$s<$TX<$X TX、、hTg（十五）ΦsTX在D中是交换的，一个Γ-余代数态射是一对Γ-余代数态射和一个Γ-余代数态射.这给出了投影函子1：-coalg→ Γ-coalg一般来说，与切片代数的情况相反，图（15）不能被读作余代数态射（在[23]中，它被称为“扭曲余代数态射”）。因此，没有类似于命题4.3的性质对一般的余代数成立然而，当我们假设一个左伴随SopET时，出现了额外的结构。事实上，那么联系：Γ T=T op与它们的伴随配偶是双射对应的[14]：S =SΓ op，由转置SopΓ η：Γ = T opSop定义。很容易就能检查出（）（S）=（T）o p。特别地，这意味着同构-coalg（十六）自然变换是切片的。最后，T有一个左伴随的事实意味着切片内函子之间的所有自然变换都是切片的。实际上，考虑任何ρ：ΓT = Top和ρJ：ΓJT = TJop。命题4.5如果SopE T，则自然变换κ：ρ =<$ρJ与对<$α：r =<$rJ，β：<$J=<$r j一一对应，使得Tβop<$ρ = ρJ<$αT，如（11）中所示。证据（12）显示了如何从α和β定义κ。关于另一个方向，请参见附录。Q4.3分层分配律与组合性现在我们继续研究切片内函子之间分配律的双代数。分割分配律。对于一个附加函数SopET：Cop→ D，考虑C和L上的内函子B，T，D上的Γ，以及定义切片内函子ρ，T on（D↓ T）的连接ρ：LT → TBop和τ：Γ T = T op。现在假设ρ在ρ上的分布律，即， 一个自然的变换κ：ρ=ρ。 根据（10），ρ ρ和ρ ρ都被切片，进一步根据命题4.5，对于某些分配律χ：L Γ =<$Γ L，κ具有形式κ = χ ② λ（见（12））166B. Klin/Electronic Notes in Theoretical Computer Science 264（2010）155⇒^ ^您的位置：^ ^您的位置：b^pbJGX^ ^您的位置：^ ^您的位置：^C◦ ◦→Bκ-双U ρbκ-偶联和λ：λ B =B λ，使得自然变换的六边形交换（参见（11））：LTχTL ZLTopρopzT（B）opT λop（十七）czzopzT（c）zop<$LT<$ρ <$TB切片双代数与第2节一样，κ律定义了在p-coalg上的闭函子ρκ和在ρ-alg上的闭函子ρ κ，具有范畴的同构和遗忘函子的交换平方（参见。（4））：κ-bialg=ρ^κ-alg=ρ^κ-coalgU κρ-aJlgUBU（D↓T）。（十八）为了表达一些直觉，提供一个更具体的κ-双代数的描述可能是有用的。其中的每一个都由一个χ-双代数LΦkΦl构成ΓΦ， aλ-双代数图表：H BX和D中的箭头s：Φ →TX，使得LΦkΦlΓΦLSJsΓsJ J（十九）LTXρX TBX日 TXTgTX，，τTX上下班κ-双代数的态射是αχ-和αλ-双代数态射对，特别地，存在一个明显的投影函子，我们将其记为 α2：κ-bialg→（λ-bialg）op.提升余代数模态逻辑。我们现在的直接目标是展示出一个关于α2的左伴随。 注意，（19）的底行不是χ-双代数，因此κ-bialg是 不容易成为一个切片类别，使用命题4.1的简单策略不能使用。相反，伴随提升可以按以下方式使用由于κ在-分支上充当λ（参见（12）），因此可以直接检查κ在ρ -代数及其态射的B-余代数分支上充当λ;形式上，κ=（α 2：ρ-alg（B-coalg）op. 这就定义了一个102的提升到一个从κ-coalg到（λ-alg）op的函子，如（A.1）;很容易检查这个提升的函子与λ2重合，这证明了它的名字。我们现在可以将命题A.1应用于（λ-bialg）op，β2，κ-bialg（Uλ）opUζκ（B-coaJlg）op，， ρ-aJlg2012年 2月并得到一个左伴随a→E2。 结合（18）和（16），这完成了一个B. Klin/Electronic Notes in Theoretical Computer Science 264（2010）155167ρ^ρ◦、、^CD- 如图所示的共代数模态逻辑语义（14）的提升a→Uρκ（λ-bialg）op，Π2κ-双链UB煤U= （^-alg）op（Uλ）opb（U/s）op（二十）Jopa→zJJJop（B-煤g），Π2-algUB（D↓T）=（C ↓S）注意，根据推论4.4和命题A.1之后的注释，单子2a→是（自然同构于）恒等式。这一点，连同明显的commuting广场健忘和投影函子：（UB） ）OP（λ-bialg）opλ （λ-alg）op，，Π2-bialgΠ2煤，， 、、、=（-alg）κUρbκ- -∼^٨op意味着（20）的顶行与从λ-bialg和λ^-alg到λ-alg的遗忘函子（的对立面）交换。我们得出的结论是，λ-双代数<$XgXH BX，逻辑ρ在h上的解释是一个载体一个G-代数和一个G-代数态射。请注意，在这个结论中既没有提到χ，也没有提到χ，所以最有用的表述方式是：定理4.6F或任意SopET ，λ，B，λ，L和ρ作为above，如果ar，λ和κ=χ②λ存在，则对任意λ-双代数<$XgXH BX，解释逻辑ρ在h上是g的一个n-代数态射。Q当应用于初始λ-双代数时，得到了[15]的定理25集合上的逻辑分配律定理4.6可以用来证明由结构运算规范（定义为λ）诱导的转移系统（B-余代数）上的逻辑等价（定义为语法L和语义ρ）是同余（关于语法λ）。为了使用这个定理，需要找到三个额外的成分：一个内函子Γ和自然变换和χ，使得（17）交换。到目前为止，我们还没有提供这些成分的直观含义。这就是本节的目的，我们将注意力限制在双重附加条件上 = =设置，S=T=2 −。5.1分配律与谓词提升对于给定的B，搜索Γ和ρ与搜索给定的B，搜索模态逻辑L和ρ完全类似，如第3节所述。因此，可以限制168B. Klin/Electronic Notes in Theoretical Computer Science 264（2010）155⇒i=1l=Σ→◦→注意函子的形式Γ = Γn ×（−）n，（21）n∈Nn其中，Γn <$2<$2。回想一下，我们可以有把握地假设L具有类似的形式（7）。这意味着，一旦选择了带π的Γ，定理4.6的最后一个缺失的成分χ是多项式函子之间的分配律χ这样的定律可以表示为方程组，如下。设Γ和L如（21）和（7）中所示，分别由（Γn）n∈N和（Ln）n∈N的 则一个分配律χ：L Γ= ΓL等价于以下形式的方程族β（σ1（x11，...，x1m1），.，σn（xn1，.， xnmn））=（22）σ（β1（γ11，…，y1l1），.，βk（yk1，...，yklk）），其中：• β∈Ln，σi ∈Γmi，σ ∈Γk，βi∈Lli，• 所有变量xij是不同的，• 每个变量yij都出现在左侧。后两个条件确定函数v：l→m，其中m=nmi和ki=1li是等式两边的点为了定义一个分配律χ，对于每个组合β，σ1，.，一个B-模态的σn（arity，比方说，n）和一个N-模态序列（长度n）。现在我们将用模态和方程来表述应用定理4.6所必需的条件（17 为此，首先注意每个β，σ1，.， σn在（ 2 2 ） 的左手边，定义了元数m =ni=1 mi，（其中σi∈ Γ mi），在[27]之后，将其表示为β（σ1，...，σn）：B（2m）2. 此外，还表示了复合多项式内函子LΓ通过所有这样的复合模态的集合，并且如（17）中的连接ρ opL （也参见（10））通过将所有相应的谓词提升（β（σ1，...，σn））Y.类似地，可以定义提升σ（β1，...，βk）：β B（2 l）2，来自（22）的右手侧。由于LΓ是多项式函子，因此条件（17）可以通过情况来检查，对于每个（的左手侧）等式（22）。每种情况都相当于检查以下自然变换的平方是否是可交换的：（2−）m（β<$（σ1，...，σn））Y z2B<$−（2−）v2λ公司简介（2−）l（σ（β1，.，βk））Y z2B−。B. Klin/Electronic Notes in Theoretical Computer Science 264（2010）155169→∅∈∨⊗⇐⇒ ∈ {⊗}∈ ∨⊗→⊗⇒联系我们通过米田引理，这相当于检查aritym的两个CIB-模态的相等性：（β（σ1，.，σn））<$λ2m =（σ（β1，.，βk））β-氨基丁酸B（2 v） （23）这种情况可以直观地解释如下。 对于一个固定集合X，如果X上的谓词被变量xi1，...，ximi，则表达式σ（xi1，...，ximi）在（22）的左边定义了一个关于X的谓词;类似地，整个左边从X上的m个谓词的集合中定义了一个关于B X的谓词。此外，右侧（连同方程中隐含的函数v：l m）定义了一个关于BX的谓词。现在，条件（23）意味着前一个谓词与后一个谓词在与λ预先组合时一致。5.2一个玩具的例子考虑第2节（2）和（1）中的λ、B和λ。还考虑，作为L和ρ，（6）中定义的迹等价，由（8）中给出的模态集合表示。为了应用定理4.6来推断由（1）定义的语言的迹等价的复合性，需要找到一个n-模态的集合（Γn）n∈N，以及一个方程（22）的集合，使得条件（23）对每个方程成立。作为第一次尝试，可以尝试空集合（Γn = 对于nN）， 也就是说，没有任何形式的歧视。只有（22）的一个左手边需要处理：0元B-模态T。然而，不幸的是，根本不可能有（22）的右手边，因此无法写出T的方程。为了修正这一点，我们可以包含一个然后我们可以写出一个T的方程：T =T（24）条件（23）成立。不幸的是，现在有更多的左手边需要照顾：没有合适的方程可以写为a（T）。后一个表达式表示一个0元的B-模态，直观地说，它检查一个过程的某个a-后继是否存在。 为了表达对应的（沿λ）λ B-模态，可以针对每个A向Γ 2添加新的一元λ B-模态a [ ]：λ 2 2，其正式定义为：[ ]（t）=ttt a，tttt，写出一个方程：a（二十五）直觉上，一个进程有一个a-后继者当且仅当它是进程a或者它是形式p q使得p和q都有a-后继者。 形式上，条件（23）对于该方程成立。然而，这里有一个小问题：形式上，这个方程的右手边不是（22）中允许的形式，因为 一不是L中使用的模态。 这个问题的一个原则性解决方案是允许在方程的右侧使用复合B模态;即， 考虑分配律χ：L Γ=就像SOS理论中考虑的复杂类型的分配律一样（见第2节）。另一种解决方案是简单地添加缺失的（0元）B模态170B. Klin/Electronic Notes in Theoretical Computer Science 264（2010）155联系我们联系我们CD◦na到L0，并继续寻找进一步的方程。改变一个逻辑来证明它的组合性是一个笨拙的步骤，但在这种情况下，它不会造成任何严重的伤害，因为结果逻辑的逻辑等价仍然是迹等价。形式上，然后需要在左手侧提供具有0元模态a的合适方程，但现在这是直接的：a（二十六）为了完成这幅图，人们仍然需要提出左手边的方程，如a（b <$[] x）。 这是通过将另一个一元模态[t]添加到Γ 1来解决的，定义为[t]（t）=ttt= tt t，其中等式a这些与（24-r 0={T}r 1={[]}{a [] |a ∈ A}r n= n（n > 1）并且条件（23）对每个方程都成立，因此我们可以利用定理4.6得出结论：迹等价是（1）的合成。 同样的结果在[15，17]中被用作例子;然而，我们对Γ和χ的粗略理解导致了不必要的丰富逻辑行为和复杂的分配律。5.3表达逻辑的组合性关于我们的组合性方法的鲁棒性的一个重要问题是定理4.6是否是命题2.1的推广，即，它是否涵盖了观察等效性而不失一般性。在[16]中研究的较弱条件下（如B的有限性）是某个逻辑（L，ρ）的逻辑等价（这种逻辑称为表达逻辑）。 如果这是，则命题2.1的结论是定理4.6的结论的特殊情况。然而，是否有一种表达逻辑满足定理4.6的假设？现在我们将对这个问题给出一个部分肯定的答案：我们将注意力限制在==Set和S=T= 2 −，多项式处理语法函子，以及保持有限集合的有限元B。在一般情况下，这个问题是开放的。对于我们的特殊情况，B-余代数的观测等价由所有有限B-模态的集合所表示的表达逻辑（L，ρ）定义，即，通过L =2B2n，其中n ∈ N. 我们现在将证明，这种逻辑满足以下假设：定理4.6当我们取由所有模态表示的Γ和π时，即，因= 2× 2n对于n∈N.为此，我们需要，对于每个B-模态β ∈ Ln和B-模态σ1，.，σn，以表示α B-模态（β α（σ1，…，σn））λ2m（其中m是σ i的概率之和）的形式（σ（β1，.，βk））β 2 v（27）B. Klin/Electronic Notes in Theoretical Computer Science 264（2010）155171∈→∈我对于一些σr k和β1，...，βkB-模态，具有i和v：l的特征和M一个函数之间的关系。在我们的假设下，这可以在不对β、σi或λ进行任何分析的情况下通过以下结果来完成：命题5.1如果A是多项式，B保持有限集合，那么元数m的每个A B-模态都可以像（27）那样分解。证据令n = i I（−）ni. 考虑任何γ：γB（2m）→ 2。 把k=|B（2个月）|（注意B（2 m）是有限的）。对任意b∈B（2m），定义βb：B（2m）→ 2：βb（bJ）=ttb=bJ.然后定义σ：Σ（2k）→ 2，通过：σ（i）i（p1，.，pni））= tt⇐⇒1、 .. . ，bni∈B2. .（j=1.尼岛 pj（bj）=tt（t）=tγi（b1， . ，bn））=tt，M其中，ii：（−）ni= π的范围涵盖到π π的联产品注入。这给出了一个元数为m×k的复合模态σb（βb）b∈B2m，结果表明，γ=（σB2π其中π：m×k →m是显式投影。Q6今后工作不幸的是，这两个缺陷，本文件旨在消除，仍然在一定程度上坚持在目前的提法。在抽象层次上，显然有一个2范畴的处理共代数模态逻辑等待被发现，并结合在[24]中开发的双代数。连接ρ和ρ是内函子的简单态射，就像λ和χ是它们上的自同态一样;在[ 24 ]的意义上，切片分布态射χ②λ也是分布态射。显然，故事的结构比目前解释的要多在具体层面上，非常需要一些更具体的指导方针，以找到合适的医疗模式集合。最后但并非最不重要的是，需要展示更多逻辑分配律的例子，以及它们与其他关于SOS组合性的工作（如[6]）的引用[1] L. Aceto，W. J. Fokkink和C.维尔霍夫结构操作语义学。在J.A. Bergstra，A. Ponse和S.Smolka，编者，《过程代数手册》，第197Elsevier，2002年。[2] F.巴特尔斯关于广义共归纳和概率特化定理。博士论文，工国委，阿姆斯特丹，2004年。[3] B.布鲁姆，S。Istrail和A.迈耶。 互模拟是无法追踪的。 Journal of the ACM，42：232-268，1995.[4] M. Bonsangue和A.库尔兹 变迁系统逻辑的对偶性。 在FOSSACS3441 ofLNCS，pages 455172B. Klin/Electronic Notes in Theoretical Computer Science 264（2010）155[5] M. B