自动机与余代数的理论联系与应用

→理论计算机科学电子笔记106（2004）355-375www.elsevier.com/locate/entcs余代数的自动机与不动点逻辑Yde Venema1阿姆斯特丹大学逻辑、语言和计算研究所Plantage Muidergracht 24，NL摘要本文的目的是将自动机和逻辑之间的现有联系推广到更一般的共代数水平。设F：集合设为一个标准函子，保持弱回调。 我们引入了F-自动机的概念，它是一种在指向的F-余代数上操作的设备;自动机接受或拒绝一个点余代数是用一个无限的两人图博弈来表示的。我们还介绍了一种语言的余代数不动点逻辑的F-余代数，我们提供了一个游戏语义这种语言。最后，我们表明，任何公式p的语言可以转化为一个F-自动机Ap，这是相当于p的意义上说，Ap接受正是那些指出F-余代数中，p举行。关键词：余代数，自动机，模态逻辑，不动点算子，博弈语义，互模拟，奇偶博弈1介绍在理论计算机科学中有一个悠久而值得尊敬的传统，将自动机理论和逻辑的研究领域联系起来。当自动机被用来对单词、树或图形等有限对象进行分类时，这种联系变得特别强大。有趣的是，这一研究领域不仅提供了基本的理论结果，如拉宾1电子邮件：yde@science.uva.nl1571-0661 © 2004 Elsevier B. V.根据CC BY-NC-ND许可证开放访问。doi：10.1016/j.entcs.2004.02.038356Y. Venema/Electronic Notes in Theoretical Computer Science 106（2004）355在过去的十年里，逻辑和自动机理论之间的联系变得越来越强，以至于在许多情况下，自动机和公式之间的区别几乎消失了。在已经获得的许多有趣的结果中，我们只提到JANIN WALUKIEWICZ[9]在模态定点逻辑（如模态μ-演算）和在标记转移系统上运行的交替奇偶自动机之间建立 对于自动机，逻辑和无限游戏世界的最新介绍，我们请阅读GrDEL，THOMAS&WILKE[5]。虽然这对我们的知识从来没有被利用，甚至明确，大部分的工作有关的逻辑和自动机理论有一个强大的coalgebraic construavour。就其本身而言，这并不令人惊讶，因为（模态）逻辑和自动机理论都承认一个有利可图的共代数观点。这当然适用于逻辑，特别是模态逻辑。由于余代数可以看作是基于状态的动力学的一个非常一般的模型，模态逻辑可以看作是动力系统的一种逻辑，所以模态逻辑与余代数之间的关系从MOSS[11]的工作开始，各种作者，包括JACOBS[6]，KURZ[1 0]，PATTINSON[12]和ROIGER[1 4]，都在积极地追求和研究用于确定余代数性质的模态语言。 然而，考虑到共代数模态语言作为限制基于状态的系统行为的规范的预期应用，令人惊讶的是，直到现在还没有开发出包含显式不动点运算符的语言。此外，唯一的工作，共代数模态语言，其中不动点公式的样本被承认，或其中需要共代数模态不动点逻辑进行了讨论，似乎是由[8]和[7]。关于自动机的余代数观点可能还没有发展得如此系统，自动机理论包含了余代数的一些范例，因为任何对余代数领域的介绍都是见证作为例子，我们确认自己提到Rutten总结上述讨论，我们发现，自动化理论和（模态）逻辑之间的关系已经得到了深入和细致的研究，但还没有统一或系统地研究。对于任意类型的余代数，各种模态语言已经被统一地发展出来，但是这些语言都不允许显式的不动点算子。最后，我们看到从余代数的角度研究了某些类型的自动机，但还没有开发出任意余代数的自动机。因此，这里似乎有一个明显的空白，而我们打算用本文件开始填补的正是这个空白。Y. Venema/Electronic Notes in Theoretical Computer Science 106（2004）355357L我们相信，自动机和逻辑之间的联系可以，也许应该从一般的，共代数的角度来研究，这是本文的主要目的，介绍一个框架这样做。我们将注意力集中在标准的并保持弱回调的函子F：Set→Set上--这样的函子将被称为R-标准的。对于每个这样的函子F，我们将定义F-自动机的概念;目的是其中的一个方法是对点F-余代数（由一个F-余代数和该余代数的一个载体集的元素组成的对）进行分类。这样一个自动机A接受或拒绝这样一个点余代数（S，s）的标准，可以用一个无限二人博弈来表述，这个博弈是在由A，S和s导出的某个图上进行的。我们还介绍了一种用于F-余代数的余代数不动点逻辑语言μF这种语言是无限的，因为每个公式都有一组有限结合来自JANIN WALUKIEWICZ[9]制定的模态μ-演算的游戏语义的思想，BALTAG[2]引入的共代数语言的语义博弈，我们为这种语言提供了一个博弈论语义。最后，这些对策与F-自动机的接受对策之间的相似性导致了本文的主要结果：定理2指出，任何μLF-公式都可以转化为精确接受那些指向的F-余代数的F-自动机其中公式为真。应该提到的是，还有其他方法从范畴理论的角度研究自动机。例如，Arbib和Manes的一系列文章以及由Ada′m ek，Trn kova′andothers开发的函子自动机理论[1]（所有函子自动机）。这个工作当然与我们的有关，但两个不同之处是，所提到的研究集中在代数而不是共代数框架上，并且它将自动机推广为有限对象而不是无限对象。然而，与这项工作的确切联系仍有待研究概述我们首先定义了基于集合的函子和余代数的符号和术语，并定义了R-标准函子;我们还简要介绍了两人无限奇偶博弈。第三节介绍了R-标准函数的F-自动机，并详细描述了F-自动机的接受对策。然后我们转向逻辑：在第4节中，我们介绍了R-标准函子上的余代数的余代数不动点逻辑μLFF. 下面的部分提供了这种语言语义的博弈论方法的细节第六部分是本文最重要也是最有意义的部分：在这里我们陈述了上述的主要结果358Y. Venema/Electronic Notes in Theoretical Computer Science 106（2004）355的论文。我们用一系列进一步研究的想法来完成这篇论文2预赛本文的前提是对范畴论和泛余代数的基本概念有一定的了解。本节的主要目的是固定符号和术语。我们也给一个非常简短的介绍所谓的图形游戏。2.1集基函子与余代数基础知识我们让Set表示具有函数的集合的范畴对于一个闭函子F：Set→Set，一个F-余代数是由一个集合S和一个函数σ：S→FS组成的对S=（S，σ）. 给定两个F-余代数S=（S，σ）和T=（T，τ），函数f：S→T是F-余代数态射或F-同态，如果F（f）<$σ=τ<$f.范畴Coalg（F）以F-余代数为对象，以F-同态为箭头.一个关系Z<$S×T是F-互模拟，如果我们可以在Z上加上余代数结构<$：Z→FZ，使得两个投影π1：Z→S和π2：Z→T是F-余代数态射.如果Z是S和T之间的互模拟，将s∈S连接到t∈T，则我们写Z：S，sParticipate T，t，如果存在这样的Z，则写S，sParticipate T，t。函子和关系子设Rel表示以集合为对象、二元关系为态射的范畴。对于任何集合S，该类别中的单位元箭头由下式给出：S={（s，s）|s ∈ S};这类箭 的 合 成 是普通的关系复合，但我们将像通常的函数一样编写复合。一个函子Q：Rel→Rel称为关系子。众所周知，Set可以通过图函子Rel嵌入到Rel中，图函子Rel是集合上的恒等式，它将函数f：S→T映射到它的图Rel（f）={（s，f（s））|s∈S}。我 们 说一个关系子Q：Rel→Rel扩张一个函子F：Set→Set，如果满足：（i）对于所有集合S，QS = FS;（ii）对于所有函数f：S → T，Q（Rel（f））= Rel（F（f））。扩张不一定总是存在的，但如果存在，则扩张是唯一的;我们用F表示函子F的扩张。由Carboni，Kelly和Wood [3]的结果可以得出，Set上的内函子可以扩展为关系子当且仅当它保持弱拉回。接下来我们将需要以下事实;详情请参阅RUTTEN[16]。事实2.1设F：Set → Set是一个保持弱回调的函子。然后Y. Venema/Electronic Notes in Theoretical Computer Science 106（2004）355359∈∈→∈⊆∪ ∈∈∈1. 对于R<$S×T，由F（R）=F（π2）<$F（π1）−1。2. F是单调的，也就是说，如果R<$Q，则F（R）<$F（Q）。3. Z是S和T之间的互模拟i <$（s，t）Z蕴涵（σ（s），τ（t））FZ，对于所有s，t。R-标准函子一个函子F：Set→Set称为标准函子，如果它保持包含;也就是说，只要f： A<$→B 是 包 含 ， 那 么 F（f） ： FA <$→FB 也 是 包 含 。 我 们 需 要在ADA′MEK&TRNKOVA′[1]中提供的foll o wing prop y。事实2.2设F是集合上的标准闭函子。则F保持有限交，即：F（A<$B）=FA<$FB。在本文的大部分时间里，我们将使用Set上的内函子，它们既是标准的，也是保持弱回调的。因此，引入术语是方便的。定义2.3一个函子F：Set Set被称为R-标准的，如果它是标准的并保持弱回调。2.2图游戏两人有限图游戏，或简称图游戏，定义如下。对于这些游戏的更全面的说明，读者是redtoGRDEL，THOMAS&WILKE[5]。首先是一些关于序列的问题给定一个集合A，设A，Aω和A分别表示A上的有限序列、无限序列和所有序列的集合（因此，A=AAω.）给定αA和β我们用明显的方式定义α和β的连接，我们用并置简单地表示A的这个元素：αβ。给定一个无限序列α∈Aω，设Inf（α）表示在α中无限频繁出现的元素a∈A的集合。图游戏是在棋盘B上进行的，即一组位置。b∈ B中的每一个点都是两个参与人之一，（E′lo ise）和（A b′elard）。形式上我们写为B = B<$$> B<$，对于每个位置b，我们用P（b）来表示参与人i，使得b Bi。此外，董事会被赋予二元关系E，因此每个位置b B都有一个后继集合E[b]B。形式上，我们说这个博弈的竞技场由一个有向二分图B=（BB，E）组成比赛的游戏包括两个球员移动一个卵石周围的董事会，从一些初始位置b0。 当石子到达位置b∈B时，轮到参与人P（b）360Y. Venema/Electronic Notes in Theoretical Computer Science 106（2004）355G联系我们ΩΩ···∈到他们喜欢的新位置，但选择仅限于b的继任者。如果E[b]是空的，那么我们说参与人P（b）被卡在了这个位置。 一场比赛或游戏因此构成了（有限或无限）序列位置b0b1b2... 使得biEbi+1（对于每个i，定义bi和bi+1）。一个完整的游戏是（i）无限游戏或（ii）最后一个玩家卡住的有限游戏。不完全的打法称为部分打法。游戏的规则将一个赢家和（因此）一个输家与游戏的每一次完整的游戏相关联。 一个有限的完全发挥是由被卡住的球员失去的;无限游戏的获胜条件是由Bω的子集Ref给出的（Ref是“裁判”的缩写因此，图博弈被正式定义为一种结构=（BB，E，Ref）。有时我们想把注意力限制在某个初始位置的博弈上;在这种情况下，我们会说在这个位置初始化就像自动机一样，有各种众所周知的获胜条件;在这里，我们将把注意力限制在奇偶博弈上，也就是说，集合Ref是根据奇偶函数定义的。 奇偶校验函数在一个集合A上，是一个具有有限值域的映射A→ω;换句话说，A上的一个奇偶映射是一个映射A → Ω：A0，...，K对于某个自然数k。 给定奇偶性A上的地图，我们把(1)Aω：={α∈Aω|max {n（a）：a∈Inf（α）}是偶数}。在一个奇偶对策中，对于某个奇偶函数，董事会B。局中人i的策略是一个函数，它将部分局β = b0···bn，其中P（bn）=i映射到下一个可允许的位置，即映射到E [bn]的元素。这样，一个策略告诉i如何下局：一个策略β与策略f是一致的，如果对于β的每个适当的初始序列b0···bn，当P（bn）= i时，我们有bn+1=f（b0bn）。 A策略是从b位置获胜B如果它保证i赢得任何初始位置为b的比赛，无论对手如何比赛-注意，不需要P（b）= i。一个位置b∈B称为参与人i的获胜位置，如果i从位置b有获胜策略;博弈G中i的获胜位置集合记为Wini（G）。奇偶博弈由于具有许多优良的性质，如历史无关的确定性等，成为一个有吸引力的重要博弈模型。然而，这些都不需要在本文件中-感兴趣的读者再次参考[5]。Y. Venema/Electronic Notes in Theoretical Computer Science 106（2004）355361∈∈Ω3余代数自动机理论3.1基本定义我们的第一个定义涉及论文中最重要的概念：F-自动机。定义3.1设F是集合上的R-标准内函子。一个（交替）F-自动机是一个四元组A=（A，aI，n，Acc），其中A是一个有限的对象集合，称为状态，aI∈A是初始状态，n：A→ PPFA是阶跃函数，Acc<$Aω是接受条件。一个F-自动机被称为孤立（或非确定），如果所有的成员都是单例。一个F-自动机被称为确定性的，如果对于每个a∈A，有一个元素δ（a）∈FA，使得δ（a）={{δ（a）}}（特别地，这样的自动机是孤立的）。当我们在下面讨论接受博弈时，这个定义的含义应该会变得清晰在续集中，我们将永远不会显式地使用形容词'交替'时，描述自动机。我们只是在定义中提到它，以明确在我们的框架中，通用自动机是交替的，确定性自动机和孤立自动机是交替自动机的特殊实例。这一问题将在下文中更详细地讨论从文献中已知有各种验收条件对于几乎所有这些，无限序列α Aω是否属于Acc的标准都是根据集合Inf（α）来制定的。例如，一个Bu？chi条件使α一个c-c-if和o-c-ifInf（α）是一组特殊接受状态的集合。在本文中，我们将专门与奇偶自动机。定义3.2设F是集合上的R-标准内函子。一个平价F-自动机是F-自动机A=（A，aI，A c，Acc），使得Acc=Aω为某些宇称映射A：A→ω，见（1）。 这样的自动机通常是预-记作A=（A，aI，n， n）。映射的奇偶性被称为自动机的奇偶性函数。3.2接受博弈F-自动机被假定在点F-余代数上操作。一个点F-余代数是一个对（S，s）使得S是一个F-余代数并且s是S的（底层集合）的一个元素。基本上，这个想法是F-自动机将接受或拒绝给定的点F-余代数。 表达导致接受或拒绝的评估过程的最佳方式是两人有限图博弈或图博弈，见第2节。但据362Y. Venema/Electronic Notes in Theoretical Computer Science 106（2004）355∃B∈××首先考虑另一个图形游戏的例子。例3.3将互模拟的概念引入博弈论框架有多种方法。在这个阶段，考虑BALTAG[2]的以下方法是非常有益的。设S=（S，σ）和SJ=（SJ，σJ）是两个具有某个内函子的FF在保持弱回调的集合上。S和SJ之间的互模拟博弈B（S，SJ）被定义为图博弈（B，B，E，Ref），其中B：=S×SJ，B：=P（S×SJ），Ref：=Bω（即，所有在有限的比赛都赢了，），而边关系E给出如下：• 在位置（s，SJ）上，σ可以选择任意集合Z<$S×Sj，且（σ（s），σJ（SJ））∈FZ;• 在位置Z<$S×SJ中，Z可以选择Z的任何元素（t，tJ）。我们留给读者去验证，（s，sJ）∈Win<$（B）i <$S，sParticipsSJ，sJ.对于从左到右的方向的关键观察是，关系Win（）本身是S和S之间的互模拟。对于另一个方向，让在任意位置（t，tJ）选择S和SJ之间的任何互模拟将t连接到tJ，参见事实2.1（3）。定义3.4设A=（A，aI，σ， σ）是F-自动机，S=（S，σ）是F-余代数。与A和S相关联的接受博弈G（A， S）是奇偶图博弈（B，B，E，），B：=A×S<$FA×FSB<$：=P（FA）×S<$P（A×S），而E和λ由下表给出职位：bP（b）允许的移动：E[b]（b）（a，s）∈A×S（f，s）∈ P（FA）×S（τ，τ）∈FA×FSZ∈ P（A×S）∃∀∃∀{（f，s）∈ P（FA）×S|∈{（τ，τ）∈FA×FS|<$∈ <$且τ = σ（s）}{Z ∈ P（A×S）|（τ，τ）∈ FZ}Z（a）000最后，A接受点F-余代数（S，s），如果（aI，s）是博弈G（A， S）中的为了理解这个博弈，考虑一个F-自动机A和一个F-余代数S. 在博弈G=G（A， S）中的所有位置中，A S中的位置是基本位置，其他位置只是中间阶段。粗略地说，我们应该把一对（a，s）A S看作一种情况，在这种情况下，自动机处于状态a，检查余代数的点s的目的Y. Venema/Electronic Notes in Theoretical Computer Science 106（2004）355363G∃∀∈∈×∈×∈ ×∃∈×是为了表明这种描述首先，我们来看两种特殊情况。首先假设自动机A是确定性的。也就是说，存在一个映射δ：A→FA使得对于每个a∈A，它保持<$（a）={{δ（a）}}。 现在，在博弈G的任何位置（ a ， s ） ∈A×S 上 ， R2 只 能 走 一 步 ， 即 到 位 置 { （ δ （ a ） ， s ） } ∈ P（FA×S）;在那之后，R2也没有选择：他必须把鹅卵石移到（δ（a），σ（s））FAFS。注意这个位置完全由第一个位置决定--因此得名“确定性”。形式为（δ（a），σ（s））的位置类似于例3.3的互模拟博弈的位置（a，s）：Z1选择一个关系Z<$A×S，使得（δ（a），σ（s））∈FZ，之后，Z1选择一个新的对（b，t）∈Z，我们回到一个基本位置。所以在确定性的情况下，宇称自子本身可以表示为一个同样，这样一个自动机的接受博弈（A， S）就像一个“装饰”的双模拟博弈。但当然，自动机在有限对象上工作的大部分力量恰恰源于“装饰”的复杂性现在考虑更一般的情况，我们只知道A是孤立的，并考虑一个位置（a，s）∈A×S。 在这里，她有一个真正的选择：她可以从（a）中选择任何单例{α}，并将鹅卵石移动到位置{（α，s）} ∈ P（FA×S）。在那之后，他的选择是被迫的：他必须将鹅卵石移动到位置（α，σ（s））FA S。因此，在位置（a，s）处，它是开的。她自己的谁决定后来的位置（α，σ（s））FA S-这解释了为什么我们称这样的自动机为注意，在形式为（α，σ（s））FA S的位置上，博弈像确定性情形一样进行，直到到达另一个中心位置。最后，我们考虑最一般的情况下，其中A是一个任意的自动机。在这里，目标仍然是从位置（a，s）∈A×S开始到达位置（α，σ（s））∈FA×S，但是现在，为了到达那里，R2和R3玩了一个小“子博弈”。在这里介绍的版本中，首先，她进行预选，也就是说，她选择某个子集A;然后，她挑选一个元素A。而新的位置是（σ，σ（s））;从这里开始，游戏像以前一样进行。因此，在这种最一般的情况下，我们处理的是一个交替自动机。3.3变种：色F-自动机读者可能还没有认识到他或她最喜欢的，或者至少是熟悉的，定义3.1中的自动机类型。特别是，在（无限）单词或树上操作的标准自动机的转换函数或关系从字母表或标签集合中获取在这里，我们简要说明如何将其轻松地纳入我们的方法。364Y. Venema/Electronic Notes in Theoretical Computer Science 106（2004）355G∃∀定义3.5设F是范畴Set上的内函子，C是我们称之为颜色的任意有限对象集。我们用FC表示函子FCS=C×FS。F-C-余代数也称为C-着色F-余代数.注意，FC-余代数是形式S =（S，σ）的对，其中σ：S→C×FS。我们用π1和π2来表示两个投影函数，并称π1σ（s）∈C为s的颜色。很明显，我们可以用F-C自动机FC-余代数，但下面的定义似乎更符合自动机理论中的标准用法定义3.6设F是集合上的R-标准内函子。C上的色F-自动机是一个五元组A=（A，aI，C，n，Acc）使得n：A×C→ PPFA（并且A，aI和Acc与前面一样）。给定这样一个自动机和一个FC-余代数S=（S，σ），我们用与前面非常类似的方式定义接受博弈C（A， S），见下表：职位：bP（b）允许的移动：E[b]（b）（a，s）∈A×S（f，s）∈ P（FA）×S（τ，τ）∈FA×FSZ∈ P（A×S）∃∀∃∀{（f，s）∈ P（FA）× S |<$∈ <$（a，π1σ（s））}{（τ，τ）∈FA×FS|且τ = π2 σ（s）}{Z ∈ P（A×S）|（τ，τ）∈ FZ}Z（a）000例3.7不幸的是，我们这里没有足够的空间来给出一个详细的例子。然而，我们不难证明，例如，C -1二叉树上的非确定性布赫自动机， 对于二元树 函数BS=S×S，可以表示为C上的一个简单的、色性布赫自动机。同样值得注意的是，识别C-着色F-余代数的两种自组织之间的差异只是表面的：命题3.8FC-自动机和C上的色F-自动机识别同一类的点FC-余代数.事实上，有相当直接的程序把一个FC-自动机变成一个等价的C上的色F-自动机，反之亦然。由于篇幅所限，我们不能详述。3.4变体：逻辑自动机对F-自动机A的阶跃函数f的不同观点是，对于所有状态a，f（a）是FA的元素的合取的析取。在接受博弈中，我们看到在选言之间进行选择，在合取之间进行选择。这表明了以下的概括。Y. Venema/Electronic Notes in Theoretical Computer Science 106（2004）355365n0• 微升nnnn∈ωn包含X和DL（X）.P和当P是一组对象时，（1）在两个不同的条件下，选择一个条件，从（P，s）到aF定义3.9GivenasettX，letDL（X）behesmallestconobjections设F是Set上的R-标准内函子。逻辑F-自动机是一个四元组A=（A，aI，Δ c，Δ c），其中A，aI和Δ c如前所述，并且Δ c：A→DL（FA）。这个A的接受博弈是以一种完全明显的方式定义的，使A在析取之间进行选择，对于某些人来说，从（P，s）移动到（p，s位置（p，s），其中p∈P，直到到达位置（α，s），其中α∈FA。这种对逻辑自动机的推广很好，也很有用，但它并没有给我们的自动机增加任何识别能力命题3.10 F-自动机和逻辑F-自动机识别相同类的点F-余代数.这个命题可以用一些标准的博弈论论证来证明（基本上，它只涉及应用析取对合取的分配律，反之亦然）。4余代数不动点逻辑4.1语法定义4.1设F是Set上的R-标准内函子，X是一组称为变量的对象。对于每个自然数n，我们用归纳法定义了深度为X的余代数不动点公式的集合μLF（X）编号：• μLF（X）是最小集合S，它包含T、λ和X中的所有变量，满足：（i）如果p和q属于S，则p ∈ q和p ∈ q也属于S;（ii）如果p属于S，则对于每个x ∈X，μx.p和νx.p也属于S。Fn+1个（X）是包含公式π的μLF（X）的最小超集对于属于F的每个πQ，对于某个有限的Q∈LF（X），它是封闭的，根据相同的成立规则（i）及（ii）。并集μLF（X）=μLF（X）是所有余代数不动点X上的公式给定一个公式p∈μL（X），我们将p的深度定义为最小自然数n，使得p∈μLF（X）。很多时候，我们没有理由使变量集合X显式化，所以我们经常写μLF而不是μLF（X）。366Y. Venema/Electronic Notes in Theoretical Computer Science 106（2004）355P ×PnnnL∈L∈a→Φ等于{{}}|p∈ Φ}[a]{p|p∈ Φ}。 这当然例4.2我们的定义旨在将模态μ -演算的定义推广到集合上的任意R-标准内函子。回想一下，模态μ-演算是一种用于函子FS=（Prop）（S）Act的余代数的语言，其中Prop是一些命题变量的集合，Act是一些原子动作的集合在JANINWALUKIEWICZ[9]的模态μ-演算公式模态运算符[a]和[a]被替换为单个连接词对有限公式集进行运算：如果Φ是有限公式集，则a→Φ是公式。 a→Φ的含义可以用α和[a]表示：在共代数逻辑中非常熟悉，并且很容易重新措辞Janin Walukiewicz的语言，以这样的方式保留了一系列模态运算符，每个都表示形式q∈Prop±q（a→Φa）a∈Act其中±q表示q或<$q。这样做，我们就可以使模态微演算的语言完全符合我们定义的格式在我们转向这种语言的共代数语义之前，有一些语法问题需要解决。我们从一个重要的观察开始，即每个共代数不动点公式都有一个唯一的构造树;这里的关键见解是，每个公式p都有一个唯一的、自然定义的“立即”集。子公式。 如果p的形式为<$π∈µLF，则此见解基于对于所有的有限集合Q μF，以及所有的π，FQ有一个（唯一）最小集合QJμF，使得πFQJ-从事实2.2可以很容易地得出这样一个集合的存在性。我们让读者给它一个正式的定义构造树;我们确实提供了子公式概念的明确定义。定义4.3如果q是p的一个子公式，我们将写qp。归纳地，我们定义p的子公式的集合Sfor（p）如下：Sfor（p）：={p}如果p∈{T，<$}<$X，Sfor（p<$q）：={p<$q}<$Sfor（p）<$Sfor（q）如果<$∈ {k，k}，Sfor（ηx.p）：={ηx.p}<$Sfor（p）ifη∈ {µ，ν}，Sfor（nπ）：={nπ} np∈Base（π）Sfor（p），其中Base（π）表示最小集合Q，使得π∈FQ;基（π）称为ππ的直接子公式。下面的命题可以通过一个简单的归纳来证明。Y. Venema/Electronic Notes in Theoretical Computer Science 106（2004）355367∈L公式的复杂性命题4.4每一个公式p∈μLF都有有限个子公式。定义4.5不动点运算符μ和ν在它们所应用的子公式中的任何地方都绑定与它们一起出现的变量。绑定的概念是完全标准的，公式的自由变量和绑定变量的集合FVar（p）和BVar（p）的定义也是完全标准的p∈µLF. 集合Var（p）=FVar（p）<$BVar（p）表示所有在p中出现的变量，自由的或束缚的。在一阶逻辑中，我们将没有自由变量的公式称为句子。一个公式p µF被称为干净的，如果没有变量在p中同时出现自由和有界，并且没有两个不同的固定点运算符绑定同一个变量。因此，在一个干净的公式p中，对于每个x∈BVar（p），我们可以关联p的一个唯一的子公式，其中x是有界的;我们将这个公式记为ηxx.qx，如果η x = μ，则称x为μ-变量，如果ηx=ν，则称x为ν-变量。一个公式p∈μLF称为守护的，如果p的每个子公式ηx.q都有这样的性质，即x在q内的所有出现都在一个π的范围内。现在让p是一个干净的公式。 我们定义了以下关系式：BVar（p）×BVar（p）：FrOcc（x，y）：在FVar（qx）中自由发生的随机变量，设≤p<$BV（p）×BV（p）表示关系的传递闭包FrOcc. 这个关系称为p的依赖顺序。4.2语义现在我们介绍余代数不动点逻辑的语义。虽然我们主要对句子的解释感兴趣，但我们也需要担心具有自由变量的公式的语义。为此，我们定义了一组变量上的F模型的概念定义4.6设F是Set上的R-标准内函子，X是变量的集合。X上的F-模型是一个三元组（S，σ，V）使得S=（S，σ）是一个F-余代数，V：X→ P（S）是S上的一个赋值.给定S上的这样一个赋值，一个变量x∈X和一个子集T<$S，我们将赋值V[x<$→T]定义为由V [x<$→T]（x）=T给出的映射，而V [x<$→T]（y）=V（y）对于所有不同于x的变量y∈X。当然，将F-模型（S，σ，V）作为函子FP（X）的余代数来表示，更符合余代数范式的风格（参见：定义3.5）。我们采用目前的方法，因为它似乎更适合于对不动点算子的处理。368Y. Venema/Electronic Notes in Theoretical Computer Science 106（2004）355∇∈∇⊆⊆P →P4.7我们归纳地定义真理的概念，即，我们定义当一个μLF（X）-公式p在赋值V下为真或在余代数S=（S，σ）的状态s处成立。更精确地说，我们定义一个关系DV<$S×µLF（X）;当对（s，p）属于DV时，我们说p在赋值V下在s∈S为真或在s ∈ S中成立，通常写为S，V，sDp。 我们还使用[·]来表示余代数中公式的扩张：[p]] S，V：={s∈S|S，V，sD p}。归纳真理定义的条款如下：S，V，SDT，S，V， sS，V，sDx如果s∈V（x）S，V，sDp<$q如果S，V，sDp和S，V，sDq，如果S，V，sDp或S，V，sDq，S，V，sDµx.p 如果s ∈{T <$S |[[p]] S，V[x <$→T]<$T}，S，V， SD νx. pifs∈ {T<$S|T<$[[p]]S，V[x <$→T]}，S，V，sD<$π如果（σ（s），π）∈F（DTBase（π）），其中，在最后一个子句中，集合DTBase（π）<$S×µLF（X）表示为DTBase（π）=D（S×Base（π））。我们说公式p在模型M=（S，V）中为真，记法：MDp，如果[[p]]M<$S。公式有效，符号：|= p，如果它在所有模型中都为真;两个公式p和q称为等价的，记法：p<$q，如果对所有模型M，[[p]] M= [[q]] M。这个真理定义的所有子句都是完全标准的，可能除了π的子句。来自文献的标准定义（参见MOSS[11]）要求S，V，sDπ，如果（σ（s），π）F（D）. 然而，考虑到我们对语言的定义，以及公式的真值应该只取决于对其直接子公式的解释的假设，π的真值定义似乎是相当自然的。我们不知道是否有我们的定义真的会偏离莫斯的情况。关于不动点算子，为了方便起见，引入一些进一步的术语。定义4.8设S是一个集合，且（S）（S）地图。子集XS称为X的预定点，如果X是X，则称为X的后定点，如果X（1）当X = 0时，X是一个固定点。Y. Venema/Electronic Notes in Theoretical Computer Science 106（2004）355369L∇从定义中可以直接得出，集合[µx.p]] M是映射λX <$S的所有预定点的集合的交集。[[p]]M[x <$→X]，而[v x.p]]M是这个地图的所有后固定点的集合的并集4.3基本语义结果在我们做任何有趣的事情之前，我们必须解决一些技术问题首先，我们需要一个简单引理，说明公式的真值只取决于它的自由变量。由于篇幅不够，我们略去了证明。命题4.9（可积性）设F是集合上的R-标准内函子，Y<$X是两个变量集，（S，σ）是F-余代数。现在假设V和VJ是S上的两个X-赋值，使得对于所有y ∈ Y，V（y）= VJ（y）。则对于所有p，其中FVar（p）<$Y，且所有s∈S，S，σ，V D pi <$S，σ，VJD p.特别是对于句子来说，从前面的命题可以得出：我们考虑哪种估值并不重要。这启发了以下定义。定义4.10设F是集合上的R-标准内函子，p是μF-语句，S是F-余代数，s是S中的点。然后我们说p在S中的s处为真，记法：S，sDp，如果S，V，sDp对于某个赋值V，（或者等价地，对于所有赋值V）。接下来我们转向单调引理。命题4.11（单调性）设F是集合上的R-标准内函子，X是变量集合，S是F-余代数。现在假设V和VJ是S上的两个X-赋值，使得对所有x ∈ X，V（x）<$VJ（x）。 则对于所有p，FVar（p）<$X成立，[[p]]S，V[[p]]S，VJ，即：对所有s ∈ S，只有当S，σ，VjDp时，我们才有S，σ，VDp。证据这可以通过对p的复杂性的标准归纳来证明。 在p=π的归纳情形下的证明是基于F是单调的这一事实（事实2.1）。Q注4.12单调性引理以我们的形式主义的名义证明了术语不动点：通过不动点理论中的Knaster-Tarski定理，完备格（如满幂集）上的每个单调运算都有一个最小和一个最大不动点，并且这些不动点可以作为370Y. Venema/Electronic Notes in Theoretical Computer Science 106（2004）355∞∞∞F∞LF一些序数，和{pα|α <β}是LF（X）-公式集，则pα集合的公式，其中包括集合{T，}X和满足（i），如果β是α β∞α β为和，形成了这种语言的自然语义。分别是X的前固定点和后固定点的集合的交集。特别地，对于每个公式p和每个模型M =（S，σ，V），集合[μx.p]] M是运算λX∈ P（S）的最小不动点。[[p]]M[x <$→X]，而集合[νx.p]]M是这个运算的最大不动点。注4.13从标准不动点理论还可以得出，完备格（如满幂集代数）上单调运算的最小和最大不动点可以用序数开折近似。利用这一点，我们的共代数不动点逻辑和更标准的共代数逻辑之间有一个很好的联系。设无穷余代数F-逻辑语言LF（X）是最小的和pα属于LF（X），和（ii）如果π属于FQ，对于某些Q<$S，然后SF模型，有明显的解释现在，对于每个序数α，都有一个将μLF-句子映射到LF-公式的转换tα这种转换定义如下：首先，我们通过transfinite归纳法，对任何L（X）-公式p，任何变量x∈X，和任何序数α，定义公式μα.p和ναx.p：µ0x.p：=0，μα+1x.p：=p[μαx.p/x]，μλx.p：=αλμαx.p，利用这些公式，ν0x.p：=T，να+1x.p：= p [ναx.p/x]，νλx.p：= α< λ ναx. p。tαp：=pforp∈{T，n}<$X，tα（p<$q）：=tαp<$tαqforn ∈{n，n}，tα（ηx.p）：=ηαx.tαpforη∈{μ，ν}，tα（π）：= π（Ftα）（π）。观察到tα将μLF-语句转换为无变量的LF-公式。可以证明，这些平移局部嵌入了μF以下意义：∞内部L∞，在(2) [[p]] M=[[tαp]] M，对任意F-模型M =（S，σ，V）和任意序数α> |S|+。然而，请注意，一般来说，（2）的余代数不动点逻辑不能嵌入无穷余代数逻辑中，如模态微演算所知我们的余代数不动点逻辑的一个重要性质是真Y. Venema/Electronic Notes in Theoretical Computer Science 106（2004）355371∈LEE∃∀是互模拟不变的。使用F-模型的互模拟的适当概念，这可以证明为任意μLF-公式，但在这里我们只陈述句子。命题4.14设S和SJ是两个F-余代数.则对任意双模拟Z<$S×SJ和任意两个点s∈S，SJ∈SJ且（s，SJ）∈Z，以及任意μLF-句p，S，sDpi S J，sJD p。证据利用Re-mark4.13的序开折和L-F-语句的真值是一个互模拟不变性质∞Q现在我们准备陈述最后一个基本的语义结果;由于篇幅有限，我们不得不省略（相当标准的）证明。命题4.15（范式）设F是集合上的R-标准内函子。那么每个公式p μF都等价于某个干净的、有保护的、具有相同深度的公式pJ。5博弈语义在这一节中，我们发展了我们的余代数不动点逻辑的语义的博弈论特征，将例如模态μ-演算的结果推广到一般的余代数框架。5.1评估游戏给定一个F-模型（S，σ，V）和一个共代数不动点公式q，我们将在有限二人图博弈中定义评价博弈=（S，σ，p定义5.1设F是集合上的R-标准内函子。给定一个F-模型M=（S，σ，V）和一个干净的余代数不动点公式q，我们首先定义了评价对策E=E（M，q