理论计算机科学电子笔记173（2007）177-201www.elsevier.com/locate/entcs超越集合的Bartek Klin1，2华沙大学、爱丁堡大学摘要在局部可表示范畴的背景下研究了多进余代数模态逻辑。 它表明，在一定的假设下，可达函子承认表达逻辑的余代数。例子包括典型的函子，用于描述系统与名称绑定，解释名义集。保留字：余代数，模态逻辑，局部可表示范畴1介绍近年来，余代数作为研究变迁系统的一种统一的抽象方法受到了广泛的关注[29，16].在理论计算机科学中考虑的许多类型的系统，包括标记的，概率的和时间的系统，都被建模为某些函子（在本文中称为行为函子）在集合和函数的范畴集合其他类别也被考虑过，例如预层类别[11]或标称集合的类别Nom[10]来建模具有名称绑定的进程代数共代数方法提供了一个抽象的观点上的概念，共归纳和互模拟。转移系统的性质通常用模态逻辑来描述。已经开发了各种逻辑来描述不同种类的系统的属性标记转移系统的Hennessy-Milner逻辑[14]，概率系统的概率模态逻辑[17]，或名称绑定系统的逻辑[24，8]。重要的是，这种逻辑是表达性的，即，它们表征了它们各自的双相似性概念。然而，这些逻辑的非表达性片段也经常用于表征过程等价的其他概念，例如，跟踪等价或测试等价[13]。一个成功的过渡系统的抽象理论必须提供一个普遍的观点模态逻辑及其性质。1由EPSRC赠款EP/D 039045/1支助2电子邮件：bklin@inf.ed.ac.uk1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2007.02.034178B. Klin/Electronic Notes in Theoretical Computer Science 173（2007）177余代数逻辑的第一个抽象方法是Moss的余代数逻辑[25]，为集合上的所有函子提供了表达逻辑。然而，一般的，共代数逻辑是相当困难的，在实践中使用，因为它的语法涉及的行为函子的应用程序的公式，它不提供简单和自然的形式，如已知的亨尼西-米尔纳或类似的逻辑。另一方面，在[15，19，26，28]中发展的逻辑接近于它们通常的具体表示，但它们的表达性取决于对行为函子施加的某些条件例如，[26]中的模态是谓词提升，它将X上的谓词映射到BX上的谓词，其中B是行为函子，并且如果存在足够的谓词提升，则所得到的模态逻辑是表达性的。B. 这是一个由Schréoder [30]提出的一种新的谓词提升方法，它指出谓词提升等价于函数B2→ 2，并被认为是多元模态逻辑，其中允许任何元的模态，如函数B（2n）→2.然后，他证明了polyadic模态逻辑表达所有可访问的行为函子。所有的结果都是在Set上创建一个函数。在particular，Scroder的表达性证明本质上是集合论的本文的目的是将多进模态逻辑的定义及其可表达性的证明推广到满足某些附加条件的局部可表示范畴上的可达函子。我们的方法受到Kurz和Bonsangue [6，7，20，21]最近工作的启发，他们使用Stone对偶来获得任意范畴上的余代数的逻辑，以及Pavlovic，Mislove和Worrell[27]的工作，他们利用数据和测试之间的逻辑联系来开发测试的抽象理论。在这些作品中，如在本文件中，逆变器提供的基础设施，连接过程和公式。在文献[6，7，20]中，我们假定这些对偶是范畴对偶。这很容易暗示所有函子的表达逻辑的存在，主要的任务是寻找这些逻辑的具体表示;为此，在[21]中使用了非对偶的表示在目前更灵活的方法中，没有作出对偶性假设。这通常使表达逻辑的具体表示更容易找到，并打开了以统一的方式处理各种有趣但非表达逻辑的可能性，但这是有代价的：表达逻辑的存在取决于某些条件，如[30]。另一方面，在[27]中，没有作出对偶性假设，并且这些假设来自于相关范畴中的某些共同生成元这并不适用于所有感兴趣的例子，在本文中，我们的工作与更一般的解释。此外，在[27]中，主要关注的是非表达性逻辑，并且没有提供表达性结果。本文件的结构如下。 在技术概要的§ 2之后，§ 3给出了一个Schroder的P o l y和D ic m o d a l逻辑的分类，它在§ 4中的某些条件下是可表达的。在§ 5中，提出了一个模态的范畴概念。在第6节中研究了三个不同范畴上的函子的例子。我知道。这篇文章是由J.J.Kurz和Sam Staton为提出强局部可表示范畴的概念所作的总结，Gordon Plotkin和John Power进行了有益的讨论，Alexander Kurz和Sam Staton对一个B. Klin/Electronic Notes in Theoretical Computer Science 173（2007）177179本文的前一稿。2预赛读者被假定熟悉基本范畴理论;[2，22]是很好的参考。满态e：X→Y是强的，如果对每个交换平方（i），mmono存在唯一的对角线d：Y→U使得（ii）可交换.Xe Y Xe YFGJ，C.J.fdgJ，UmZU m Z(i)（二）那么Y是X的强商。有人说，强epi和monos在范畴C中形成一个分解系统，如果C中的每个态射都可以分解为一个强epi后跟一个mono。源{fi：X→Yi|i∈I}是联合幺半群，如果对任意g，h：Z→X，有g = h，如果对任意i ∈ I，fi<$g = fi<$h.范畴C中的对象X是余生成元，如果对于每个对象Y，从Y到X的所有态射的源是联合幺一的。例如，每个至少有两个元素的集合都是集合中的共生成元。一个范畴D是过滤的，如果（i）对于每个d， DJ∈D，存在D中的余跨距d→djj<$DJ，（ii）D中的每个平行态射对都有D中的余均衡器.一个过滤的上极限是一个图的上极限，其域类别是非空的，二是要有一个明确的界限，即界限的界限。范畴C的对象X是有限可表示的，如果函子hom（X，−）：C →Set保持过滤余极限。例如，Set的有限可表示的对象是精确的有限集合，在代数的等式类中，代数是有限可表示的当且仅当它可以由有限个生成元和有限个等式表示。一个范畴C是局部有限可表示的，如果它是上完备的，并且有一个有限可表示对象的集合G，使得C的每个对象都是G中对象的一个过滤余限。对于C，D是无穷可表示的，函子B：C → D是无穷的，如果它保持过滤余极限。在局部可表示范畴中，一个对象是有限生成的，如果它是一个有限可表示对象的强商。在集合中，有限可表示的对象和有限生成的对象重合，一个代数是有限生成的当且仅当它在泛代数意义上是这样。上述概念可以推广到任意正则基数κ的κ-过滤余极限、局部κ-可表示范畴和κ-可达函子。本文给出的所有定义、结果和证明都适用于更一般的情形，没有任何变化。关于局部可表示范畴的更多信息和直觉，请参见[3，23]。对于范畴C上的内函子L，代数是对象X（载体），具有映射g：LX→X（结构）。 从g ：LX→X到 h： LY→Y的代数态射 是C 中的映射f ：X→Y，使得f<$g=h<$Lf。双，对于一个180B. Klin/Electronic Notes in Theoretical Computer Science 173（2007）177内函子B，余代数是一个对象X（载体），具有映射g：X→BX（结构）。从g：X→BX到h：Y→BY的余代数态射是C中的映射f：X→Y使得h<$f=Bf<$g。 例如，如果B=Pω（A×−）onSet，其中Pω是有限幂集函子，A是标签的固定集合，则B-余代数是有限分支标签转移系统（LTS）。对于集合中的余代数h：X→BX，元素（在本文中称为过程）x，y∈X在行为上等价，如果它们被下式的余代数态射所标识：H.对于集上的余代数LTS，行为等价与强双相似性相一致。余代数的更多信息和例子可以在[29，16]中找到在有限分支的LTS上，双相似性的特征在于无限Hennessy-米尔纳逻辑[14]，语法φ：：= T| ¬φ|φ1∧φ2|aX|=ax−a→ys.t。 y|=φ以及命题连接词的标准解释Hennessy-Milner逻辑的片段也被考虑过（参见[13]的调查）。例如，仅限于语法φ：：= T|中国（2）该逻辑表征LTS上的迹等价熟悉旨在将Hennessy-Milner和其他逻辑推广到其他函子（在集合上）的各种已知方法然而，如果不了解这些方法，就很难将目前的工作置于背景之下。由于缺乏空间，相关工作在这里没有描述;[30]是一个很好的参考，但例如[15，19，25，26，28]也值得一读。3逻辑连接我们对共代数模态逻辑的推广沿着与[27]类似的路线进行。为了获得动力，我们首先考虑熟悉的集合和函数的设置通常，逻辑的语义是某种满足关系|=<$X ×Φ之间的测试（公式）的集合Φ和测试实体（过程）的集合X，或等效的函数：|=: X × Φ → 2(here并且在下文中，2表示二元集合{tt，ff}）。它的两个转置：[[ ]]：Φ→ 2X[[ ]]b：X→2Φ（3）用适用于它们的公式集定义过程的语义，用满足它们的过程集定义公式的语义。特别是，两个B. Klin/Electronic Notes in Theoretical Computer Science 173（2007）177181ΦXX中的过程在逻辑上是等价的，如果它们被[]b等同。这种函数表示很容易推广到另一个集合用于“真值”的逻辑从集合范畴中抽象出来，考虑任何具有选择对象Ω的对称monoidal闭范畴（C，n，）。反变内hom-函子- -一种C上的Ω是自伴的，C（X，ΦΩ）<$=C（X<$Φ，Ω）<$=C（Φ<$X，Ω）<$=C（Φ， XΩ）（4）从对称monoidal封闭结构得到3更一般地说，我们假设任何逻辑联系，即，任何逆变附加项FC，巴塞里C（X，GΦ）=D（Φ， FX）（5），DG(theF和G的逆变性由交叉箭头尾标记），其中X∈ C，Φ∈ D。稍微滥用标记法，我们将（5）中双射的两边表示为−b. C的对象被认为是过程的集合（或结构），D的对象被认为是公式的集合（或结构）。连接（5）提供了用于关联过程和公式的基础结构。 显然，（4）是（5）的特例， 并且（3）是（4）的特殊情况在任何连接中，复合（协变）函子GF和FG分别是C和D上的单子。我们用ηGF，ηFG，μGF和μFG表示这些单子的单位和乘法。双射（5）可以用这些变换来表示：fb=FfηFGgb=GgηGF，（6）对于C中的f：X→GΦ和D中的g：Φ→FX.我们有时会使用以下属性的约束：FηGFηFGF = id.（七）下面是我们研究余代数逻辑的方法中的一个中心定义。定义3.1在（5）的情形中，对于C上的任何内函子B，B-余代数的多进余代数模态逻辑（或简称逻辑）是一对（L，ρ），其中L（称为语法）是D上的内函子，ρ：LF=FB（称为语义）沿着附接连接L和B上面的联络ρ定义伴随联络ρ：BG=GL，ρ=GLηFG<$GρG<$ηGFBG;（8）反过来，ρ通过ρ=（ρ）<$=FBηGF<$F ρF <$ηFGLF确定ρ。[3]在[27]中，真值对象Ω被假定为C中的共生成元。这里没有这样的假设，而且在§ 6.2中，真值的对象确实不是一个共生成元。 然而，我们稍后假设Ω是一个内部的共生成元，见注4.6。182B. Klin/Electronic Notes in Theoretical Computer Science 173（2007）177FXLHHHHH如果L有一个初始代数a：LΦL→ ΦL，那么ΦL可以被认为是L-公式的对象。给定任何余代数h：X→BX，h中ΦL的语义解释[]]h由D中的L-归纳定义：L[[]]hLFX，，_L_Φ_LρXJFBXa（九）FHJJ，，_Φ_[[]]h而它的转置[]]b：X→GΦL是一个映射，直观地说，它在逻辑上是等效过程。例3.2为了用一个简单的例子来说明到目前为止所描述的框架，考虑标记变迁系统上的迹等价逻辑。为此，设C=D=Set，F=G= 2−，B=P（A×−）为固定集合A。 语法（2）由函子L= 1+A× −和初始代数ΦL =A× − 来建模。在X处的连接ρ，即，函数ρX：L（2X）→（BX→2），由以下情况定义：ρX（T）（β）=tt始终ρX（ααφ）（β）= tt α φ（a，y）∈ β. φ（y）= tt，其中β∈BX，φ∈2X.这个定义与（2）的通常语义的相似性是显而易见的。 事实上，在任何LTS∗h：X→BX，[x]]b∈ 2A是x∈X，且[]b的核是h上的迹等价。我们现在开始公式化并证明逻辑（L，ρ）尊重行为，即，行为上的对等意味着逻辑上的对等。逻辑的这一性质通常是根据个别过程来定义的，然而在分类设置中，需要更抽象的方法。自[]以来b在逻辑上等同于直觉上等同于Lent过程和余代数映射标识行为上等价的过程，下面的定理合理地捕获了正确的范畴概念：定理3.3任何逻辑（L，ρ）都尊重行为，即，对于任何余代数h：X→BX，地图[[]]b分解通过每个余代数映射。证据 考虑任意余代数g：Y→BY和余代数映射f：X→YB. Klin/Electronic Notes in Theoretical Computer Science 173（2007）177183HG从H到G。 这足以证明[]b=[[ ]]b<$f，或等价地[]]h=184B. Klin/Electronic Notes in Theoretical Computer Science 173（2007）177FYHHHHFf[[]]g. 这可以通过从定义（9）中归纳得到证明，因为在图中L[[]]gLFX，，LFY，，LΦLρXρYJFBfJFBX，， FBYaFhFgJ JJ，ΦFf[[]]g左上部分通过ρ的自然性交换，右部分通过（9）交换，左下部分由于f是余代数映射。Q4表现力回想一下直觉，对于给定的逻辑（L，ρ），L允许初始代数，解释[]b在余代数h中：X→BX表示逻辑等价流程. 逻辑的表达性意味着逻辑等价意味着行为等价等价，因此可以说逻辑（L，ρ）是表达的，如果[]b是一种煤--从H.然而，这需要GΦL上的B-余代数结构，这在直觉上是一个不必要的强假设：对于表达性，它应该是充分地给出了[]]b在GΦL中的象上的一个B-余代数和一个态射从h到那个余代数 这导致以下定义：定义4.1B-余代数的逻辑（L，ρ）是表达的，如果对每个h：X→BX，地图[[]]b是一个从h到C中的mono的余代数态射。下面的定理给出了逻辑表达性的简单充分条件定理4.2在（5）的情形下，对任意B：C → C，对任意逻辑（L，ρ），B-余代数，如果• L有一个初始代数，• C有一个（StrEpi，Mono）-因子分解系统，• B保留单声道，并且• ρ∈：BG = ρGL是点态幺一的，则FXLB. Klin/Electronic Notes in Theoretical Computer Science 173（2007）177185（L，ρ）是表达式的.186B. Klin/Electronic Notes in Theoretical Computer Science 173（2007）177LηHH、η证据 下图中的C是通勤：BGF，ZerozXBηGFBG[[ ]]hBGΦ zSXSFXJGL[[ ]]ρΦLJBX，、、、GLF，X，hGLΦL，，，GρXGFBX，，zB，X，GaXGFXGF hGFXG[[]]hGΦL实际上，右下部分是沿着G映射的（9），右上部分是ρ的自然性，左下部分是ηGF的自然性，左上部分由（8）和（7）交换。这张图的外形是[[]]bBXhBGΦL，，zρsΦLJhGLΦL，，GaX[]b GΦL(see（6））。设m是[]b的强epi-mono分解。由于B保留了monos，Bm是一个mono：BXBeBI，BmBGΦ、、..H.我.zSΦJGL，Φ，Ga. ，XeImGΦ并且由于e是强的，所以存在如上所述的对角态射i：I→BI这使得e是来自h的余代数态射，m满足定义4.1。Q定理4.2的前三个条件在大多数实际例子中成立，通常要检查的关键条件是ρ的逐点幺正性。在例3.2中，对于任何Φ∈ D，函数ρ、ρB. Klin/Electronic Notes in Theoretical Computer Science 173（2007）177187ΦB：B（2Φ）→（LΦ→ 2）ρ188B. Klin/Electronic Notes in Theoretical Computer Science 173（2007）177XXΦıı、、、ıı定义如下：ρ（β）（T）=tt始终ρ（β）（ααφ）= tt（α，y）∈ β. y（φ）= tt，其中β∈B（2Φ）=P（A×2Φ）且φ∈Φ，并且它并不总是逐点monic的：例如，对于Φ ={φ，φ}，可以直接检查ρ（{（a，{φ}），（a，{φ}）}）= ρ（{（a，{φ，φ}）}）.Φ Φ实际上，迹的逻辑对于B-余代数是没有表现力的.然而，注意定理4.2的条件对于（L，ρ）是表达性的不是必需一个自然的问题是，对于给定的B在C上，什么条件足以使表达逻辑存在。假设已经选择了D、F和G，则有希望的选择是L=FBG，其中正则ρ=FBηGF：LF=FBGF=FBρ=ηGFBG：BG=GF BG=GL而单子单位ηGF通常是逐点单子的（见注4.6）。不幸的是，FBG经常没有初始代数。 例如，如果C=D=Set，F=G= 2−，则即使对于无穷B，例如B=Pω，函子FBG也没有初始代数。为了寻找L的更好的候选者，请注意局部有限可表示范畴上的有限函子具有初始代数[3]。假设D是局部有限可表示的，将D上的任何函子L限制为“几乎”充当L的有限LωLω= LanI（LI）其中I：PresωD → D是有限可表示对象的全子范畴的包含函子。用更基本的术语来说，为了计算LωΦ，将Φ表示为有限个可表示对象的图DΦ的滤波余限，沿着L映射DΦ，也就是说，求出（滤波）图LDΦ，取其余限为LωΦ。Φ100，γLωΦLΦ________ııııı，，，我...你好，ıci，kLci中国ııııck...... ııııLckr~~，r~，（十）ııılj， ，，Φi....Φı联系我们，，LΦi...联系我们ıjDΦ， LΦj，，LDΦ唯一的中介态射γΦ扩展到自然变换γ：Lω= λıB. Klin/Electronic Notes in Theoretical Computer Science 173（2007）177189YJΦΦΦL，且Lω与PresωD上的L重合。此外，Lω是无穷的，即使L不是[23，Prop。2.4.3]。我们现在可以用规范连接ρ来定义Lω=（FBG）ω：FB和ρω：BG=ωGLω，定义为：ρ = FBηGF<$γFρ<$= Gγ<$ηGFBG。（十一）如前所述，很自然地假设ηGF是逐点幺一的，但Gγ几乎从来不是。然而，在某些附加条件下，它们的合成是逐点幺一的。为了阐明这些条件，还需要一个更重要的概念：第 四 章 .3[Adamek]Alocallyfinitelypresentablecategeryisstronglylocalyfinitelypresentable if for every cofiltered limit cone{li：Y→Yi}i∈I，and for any monof：X→YwithX finitely generated，there existi∈I使得lif是a单核细胞增多症是的， .，。，i，Yk，ııııılil˛ııııkX，fY（十二）例如，Set和Pos都是强局部有限可表示的（而局部可数可表示的ωCpo也是强局部有限可表示的）。一元代数的范畴Un不是强局部有限可表示的，即使它是局部有限可表示的（见[1]）。现在我们可以给出（11）中ρ是点态幺半群的充分条件定理4.4在（5）的情形下，对于C上的B，Lω和ρ如上定义，如果• C是强局部有限可表示的，• D是局部有限可呈现的，• B是有限的，并保留单，和• ηGF是点态幺半群，则ρ∈= Gγ ∈ ηGFBG是点态幺半群。证据 对于D 中 的 一个对象Φ，我们将证明ρε：BG Φ → GLω Φ是一个单声道.回想（10），LωΦ是一个上锥的一部分{li：FBGΦi→Lω Φ}i∈I对于图FBGDΦ，其中DΦ是有限可呈现的滤波图以Φ为colimit的对象。 为了证明ρε是单声道的，这足以表明，源{Gli：BGΦ →GF BGΦi}i∈I（13190B. Klin/Electronic Notes in Theoretical Computer Science 173（2007）177）B. Klin/Electronic Notes in Theoretical Computer Science 173（2007）177191ΦΦ是共同的monic。此外，对于任何i∈I，有GliGFBGΦi◦ BGci;事实上，ρsJ'\JBGΦGFBGΦGFBG，Φ GγΦGLκΦ、、BGci、、GLIJBGΦiηGFGFBGci ，zJGFBGΦiBGΦi其中左边的正方形是ηGF的自然性，三角形与（10）中γ由于ηGF是点态幺正的，为了证明（13）的联合幺正性，只需表明源{BGci：BGΦ →BGΦi}i∈I是共同的monic。为此，考虑C中的对象X和映射f，g：X→BGΦ，使得对于每个i∈I：我们必须证明f=g。BGcif= BGcig。由于C是局部有限可表示的，有限可表示的对象生成它，并且不失一般性，我们可以假设X是有限可表示的。此外，GΦ是有限可表示对象的过滤图E的余极限。将限制性可可酮表示为{nj：Yj→G Φ}j∈J.由于B是无穷的，它保持了上极限，{Bnj：BYj→BGΦ}j∈J是滤波图BE的共限上锥。通过X的有限可表示性，存在aj∈J和两个映射fJ，gJ：X→BYj，使得f = Bnj<$f J和g = Bnj<$gJ。由于C是局部有限可表示的，强epi和mono形成了一个分解系统[3]，映射nj：Yj→GΦ分解成一个强epie：Yj→Z和一个monom：Z→GΦ。根据定义，Z是无限生成的。回想一下，Φ是图DΦ的上极限，并将上极限上锥表示为{ci：Φ i→ Φ}i∈I.=ηη192B. Klin/Electronic Notes in Theoretical Computer Science 173（2007）177ωωG是一个逆变伴随，它把上锥映射到一个极限锥{Gci：GΦ →GΦi}i∈I图GDΦ。现在，通过C的强局部有限可表示性，存在一个指数i∈I使得Gcim是单声道的。因为B保持单声道，所以BGci<$Bm也是单声道。注意f=Bm<$Be<$fJ和g=Bm<$Be<$gJ。此外，根据我们对f和g的假设，BGci<$Bm<$Be<$fJ=BGci<$Bm<$Be <$gJ通过BGci<$Bm的monicity，有Be<$fJ=Be<$gJ，并且最终f= Bm <$Be<$f J= Bm <$Be<$gJ= g.Q推论4.5在（5）的情形中，如果C是强局部有限可表示的，D是局部有限可表示的，且ηGF是逐点幺半群，则C上的每个保持幺半群的无穷函子都有一个表达逻辑。证据结合定理4.2和4.4。唯一的非平凡点是，在每一个局部可表示的范畴中，强epis和monos形成一个因子分解系统[3，Prop。1.61]。Q注4.6当上述结果专门用于由对称monoidal闭范畴中所选对象产生的映射时，如（4）中那样，ηGF的点态monicity的意义一个对象Ω是一个内共生元，如果对任意X，映射ηX：X→（XΩ）Ω是单声道。 例如用于F=G= Ω− onSet，点态monicity假设意味着逻辑值必须至少有两个元素。推论4.5专门用于：推论4.7如果一个强局部有限可表示的、对称的monoidal闭范畴C有一个内部的余生成元，那么C上的每一个保持monos的有限函子都有一个表达逻辑。5多元模态在§4中证明的结果表明如何保证B-余代数存在一个表达逻辑然而，如何在具体情况下呈现逻辑的语法和语义可能并不清楚。此外，到目前为止所提出的发展并没有建议对规范逻辑的（可能是非表达性的）片段进行任何处理。例如，知道根据定义3.1的每一个逻辑是否都是表达逻辑的一个片段是有用的。本节讨论这些问题。首先，我们分析了规范逻辑Lω的结构，并定义了一个逻辑L+，其语义与Lω基本相同，但语法允许以获得更简单的具体示例。L+的结构提出了一种多元模态的一般概念它还表明，任何逻辑与无穷B. Klin/Electronic Notes in Theoretical Computer Science 173（2007）177193ωωωωω语法规范地表示在Lω中。这些结果将大大简化我们在第6节中的主要例子。根据定义，LωΦ = colim（λ，λ →Φ）∈I/Φ FBGλ（见（10））。用一个副产品代替上极限，定义为L+Φ =光纤光栅D（λ， Φ）·FBG光栅（14）（θ，θ →Φ）∈I/ Φθ其中右边的余积是在一个选定的有限可表示对象的生成集上索引的，·表示余幂。明显的中介态构δΦ：L+Φ→Lω Φ推广到一个自然变换δ，并且是epi. G是一个逆变伴随，它将epis映射到monos，因此是正则伴随联络GδGγηGFBG：BG=GL+是点态幺一的当且仅当Lω的相应联络（11）是点态幺一的。因此，L+是可表达的当且仅当Lω是，只要它是无穷的并且允许初始代数。在具体的情况下，L+比Lω更容易在语法上表示.它的结构也暗示了多元模态的一般概念：直观上，在一个明显的意义上，元数n的模态（或实际上任何逻辑连接符）是将公式的n一个有限可表示的对象可以看作是一个arity对象，而一个map→ Φ可以看作是一个以为索引的元组。这与（14）的结构一起，激发了以下定义：定义5.1对于一个有限的可呈现的对象，FBG对象是B的客体--自然性的模态。§6中的例子将证实这个定义的可接受性。我们继续证明，每一个具有有限语法的逻辑（L，ρ）都可以看作是Lω的一个片段。我们从逻辑态射的基本概念开始定义5.2对于C上的任何B，逻辑（L，ρ）在（LJ，ρJ）中表示为θ：L= θLJ如果方程保持。ρ=ρJ<$θF（15）显然θ保留了语义ρ。此外，对于任何L和逻辑（LJ，ρJ），变换θ：L=<$LJ通过（15）定义了L的语义特别地，逻辑L的语义可以通过展示语法L是如何嵌入的来定义。在Lω.下面的表示定理表明，每一个具有有限语法的逻辑都可以这样定义。T. 对于一个BonC，一个具有L有限个的ylogic（L，ρ）是在Lω，FBηGF<$γF.我的律师。第一，第二。otthatany（kL，ρ）（其中kL不一定是精确的）在FBG中表示，FBηGF由ηρ：L=ηFBG定义为194B. Klin/Electronic Notes in Theoretical Computer Science 173（2007）177ωωωωω伴随连接ρρ，或者更明确地通过ρ=ρG<$LηFG。实际上，直接计算示出（15）对于θ=ιρ是可交换的。如果L是无穷的，表示|p产生变换|p：L=Lω沿着双射Nat（L，FBG）=Nat（LI，FBGI）=Nat（LI，LωI）=Nat（L，Lω）其中I：PresωD → D是包含函子，左和右双射成立，因为（通过无穷性）L=LanILI，中间方程成立，因为LωI=FBGI定义为Lω。 现在，变换γπρ：L=λFBG也被映射到ρ沿着相同的双射序列：γIρ→（γIρ）I=γIρI=ρIρ→ρω ω ω ω ω因此，根据双射性，等式（15）ρ=ιρFFBηGF=ιρFγFFBηGF保持。Q结合本节前面对Lω上结构的观察，上述定理允许我们给出表达和非表达逻辑的更具体的表示下一节中的例子说明了这一点。6示例本节说明定义4.1和5.1是如何专门针对具体环境中的有用和自然概念的，以及定理4.2和4.4是如何被用来为变迁系统寻找表达在第6节中。1、集合和函数的集合的集合和函数的集合的集合。Schr？odeer的多元共代数模态逻辑[30，18]被证明是本方法的一个 特 例， 因 此 所有 的 例 子 都是 这 里 的然 而 ，对于完备性，我们描述了有限Hennessy-Milner逻辑的经典例子。在§ 6.2中，研究了名义集合和等变函数的情况，并显示了Milner-Parrow-Walker逻辑[24]如何用于具有名称绑定的系统上的后期双相似性，是我们的L ω的表达片段。最后，§ 6.3以一元代数和同态为例说明了定理4.4中强局部可表示性的技术假设的重要性。6.1集合与有限Hennessy-Milner逻辑设C=D=Set，F=G= 2−，并考虑C上的任意无穷元B。一个有限可表示集（同构）于一个有限基数n∈N，根据定义5.1，元n的模态是一个函数λ：B（2n）→ 2，ιB. Klin/Electronic Notes in Theoretical Computer Science 173（2007）177195ωωXLωωωX（2）并且语法L+可以由以下语法描述：φ：：= [λ]（φ1，.，φn）其中n∈N且λ：B（2n）→2. 逻辑Lω还被模态的直接等价所证明，确保忽略其某些参数的模态等于具有较小元数的模态给定h：X→BX，[]]h：ΦL+→2X的归纳定义（9）转化为收件人：[[[λ]（φ1，. ，φn）]] h= 2 h（ρX（[λ]（[[φ1]] h，... ，[[φn]] h）== 2小时（2BηGFB2（[[φ1]]h，.，[[φn]]h）=λ<$B2（[[φ1]]h，. . ，[[φn]]h）<$BηGF<$h==λ B（[[φ1]] h，. ，[[φn]] h）b h == w <$B <$[[φ1]] h，. ，[[φn]] hh.注意，（[[φ1]] h，. ，[[φn]] h）：n → 2 X是一个函数元组，且n [[φ1]] h，. ，[[φn]]h：X→2n是一个通过元组化得到的函数。以上Φ+的语法和语义都完全对应于多元ω[30，18]的共代数模态逻辑，因此这是本AP的特殊情况接近另外，[30]中关于表达性多元模态逻辑存在的结果也可直接从推论4.7得出。事实上，Set是carlan-closed和强局部有限可表示的，并且任何至少有两个元素的集合都是一个内部共生成元。此外，Set上的所有函子保持具有非空域的monos，并且在[4]中展示了如何修改Set上的任何函子，使其保持所有monos，而其余代数范畴没有实质性变化。对于一个特殊的应用，考虑B=Pω（A×−）对于一个固定的标签集A;B-余代数是有限分支的标签转移系统。根据定义5.1的B-模态是函数w：Pω（A×2n）→2，其中n∈N。任何这样的函数都可以表示为一个由否定、有限连词、菱形模态和占位符构建的表达式，其解释如Hennessy-Milner逻辑。例如，表达式<$a<$（− <$$> −）<$$>b<$−定义了一个函数w：Pω（A×23）→2。很容易看出，任何模态w都可以用这样的表达式来描述。L+中的公式是由这样的表达式构建的，并且规范连接ρ：L+2− =<$2Pω（A×−）是从它们的解释中推导出来的，例如：ρX（a）b⎧x∈ β. φ（x）= tt，φ（x）= ff，n/n（b，x）∈β.σ（x）= tt。语法L+显然与有限Hennessy-Milner逻辑（1）有关。很容易看出，给定LTSh：X→Pω（A×X），如（9）中定义的映射[]]h因此，无穷Hennessy-Milner逻辑是本方法的一个特例，其表达性由推论4.5得出。（λ））=196B. Klin/Electronic Notes in Theoretical Computer Science 173（2007）177ωωωΦΦ不可否认，上面使用的多元模态相当复杂，这使得L+相当尴尬，因为它只不过是有限的Hennessy-Milner逻辑。人们可以通过选择L+的一个片段并使用定理4.2来证明它仍然是可表达的来缓解这个问题例如，考虑一个由下式定义的逻辑L：语法φ：：=aj =1..nj|电话（16）Σ也就是说，通过函子LΦ =A×n∈N（2× Φ）n在集合上。明显包括L+中的L确定了一个联络ρ：L2−=<$2Pω（A×−），如§5所示;明确地，伴随联络ρ：Pω（A×2−）=<$2L−定义为：⎧٨⎨ψi=φi⇒y(φi)=ttρΦ（β）（αα（α1）···αn））= tt α β（α，y）∈ β. 1.n. ⎩i=<$φi根据定理4.2，为了证明L是可表达的，只要证明ρ∈是点态幺半群就足够了。 为此，对于任何不同的β，γ∈B2Φ，需要找到a∈A，n∈N，φi∈Φ且φi∈ {φi，<$φi}使得ρ（β）（a（1··n））ρ（γ）（a（1··n））在不失一般性的情况下，假设β/γ，并且fix任何（a，x）∈β使得（a，x）/∈γ。通过以下公式定义δφ2Φδ={y：（a，y）∈γ}显然，δ是有限的。 选择n = |δ|. 对于任何y∈δ，我们有y/=x，因此可以chooseanelemntφy∈Φsuchthatx（φy）=/φ=ay（φy）。 定义φ∈LΦ：埃什基y∈δ其中，|i=φi||x（φy）=tt，否则|i=<$φi。可以直接检查ρ（β）（φ）=tt 和ρ（γ）（φ）=ffΦ Φ因此ρ（β）/=ρ（γ）且ρ是点态幺半群。Φ Φ Φ6.2具有名称绑定的名义集合和系统我们首先回顾一下名义集合的基础知识有关更多信息，请参见[12 ]第10段。在本节中，固定一个可数的有限集合N ={a，b，c，. . }的名字。对称群Sym（N）的作用（即，N的置换群）在集合X上有一个函数·X：Sym（N）×X→X使得对任意x∈X有idN·Xx =x，对任意π，σ∈Sym（N）有（πσ）·Xx=π·X（σ·Xx）. 一个集合N0<$N支持一个x∈X，如果对于所有的π，fixN0有π·Xx=x。 一个元组（X，·X）是一个名义集合，记为X，如果X的每个元素都是支持的以一个有限的集合。在一个名义集合中，每个元素x都有最小的支持集，记为supp
