递归域方程的解析与共代数方法和逻辑表示相关

271《理论计算机科学电子札记》44卷第1期（2001）网址：http://www.elsevier.nl/locate/entcs/volume44.html14页拓扑环境Dirk Pattinson德克·帕丁森1，2慕尼黑大学信息学院摘要众所周知，递归域方程的解Z，由一个终函子T给出，是终T-余代数。这就提出了一种共代数方法来获得Z的可观测性质的逻辑表示。本文考虑框架和（模态）逻辑的纤维化，通过一组谓词提升。我们讨论的条件，确保所得到的语言的表达能力（定义的公式确定的基础上的框架最终余代数）。框架，然后实例化的域的类别，我们建立这些条件的一个大类的局部连续endofunctors。这可以看作是abs1.tex这是以逻辑形式对阿布拉姆斯基的领域理论进行最终透视的第一步1介绍到目前为止，余代数已经被认为是基于状态的系统的模型，这些系统可以很自然地使用模态逻辑来指定。在集合和函数范畴上讨论余代数的（模态）逻辑有几种方法[9，11，15，17，18]。本文的目的是将这些方法推广到其他计算上感兴趣的范畴上的协余代数，域范畴就是最好的例子。这种扩展的动机是双重的。把余代数看作是变迁系统，我们想研究其变迁结构是程序的（指称语义）的系统。这就需要考虑域范畴上的闭函子的余代数。本工作的第二个动机是观察到，递归域方程的解Z，由一个内函子T给出，是最后的T-余代数（的载体取Scott-开子集1由DFG Graduiertenkolleg“Logik in der Informatik”部分资助的研究2电邮地址：pattinso@informatik.uni-muenchen.de2000年1月，出版社dbyElsevierScienceB。 V.操作访问和C CB Y-NC-ND许可证。PATTINSON272⊆∈∈L→O→∈→→→LPLPLOZ作为Z上的谓词，我们可以利用余代数模态逻辑的方法来获得Z的Scott-开子集的框架（Z）的基础集的句法表示。 为了获得这一代表性，因此，我们从X上的拓扑重建TX上的拓扑，给定任何域X。由于这可以对一大类域（连续的和更好的）进行，因此所得的表示不依赖于域是双有限的（与[2]相反）。所讨论的逻辑的解释是基于谓词提升。据作者与在loc中的阐述相反前引书(and随后的论文[10]），我们不将谓词提升与基于其句法结构的函子相关联。相反，采取了一种公理化的方法。也就是说，我们调查的谓词提升，这确保所产生的语言的表达能力的属性。这样做的优点是不限制先验假设下余代数的签名函子类，以及使我们能够根据结构性质进行论证，从而简化了证明。我们处理一个任意的基范畴C，它配备了一个偏序集的纤维化p：EC（或者替代地配备了一个函子P：Cop偏序集），并考虑闭函子T：C C的余代数。给 定 一个T-余代数（C，γ：C TC），取EC=p−1（C）（或者OP（C）在上述对应关系下）作为系统的性质（C，γ）。我们证明了T的每一组谓词提升都产生一个逻辑语言（）。这种方式产生的语言的解释被证明是稳定的余代数同态下，因此足够的余代数。我们关心的主要问题是以这种方式产生的语言的表达能力。我们考虑的表达性的概念受到Moss的余代数逻辑[16]的启发没有可用的元素，表达性的考虑是在拓扑集合中进行的，也就是说，我们假设每个元素CC上的纤维EC是一个框架（EC上的偏序表现得像拓扑）。通过离散拓扑将集内函子T：Set Set的终端余代数的载体Z看作拓扑空间，逻辑具有特征公式的性质转化为公式的表示集（wrt.最终余代数Z）是Z上离散拓扑的基。我们在一个抽象的背景下研究了这个概念，并给出了通过T的一组谓词提升而产生的语言的表达性的充分条件。该理论随后被实例化到范畴域上的内函子的余代数。我们表明，抽象的要求得到满足的一大类（局部连续）endofunctors。PATTINSON273→→→→→→→∈→∈→→2符号和标记给定一个任意范畴C，相对于C的谓词或性质的概念通常通过一个定态纤维化p表示：E C，其中纤维支持命题逻辑（的一部分）的解释.如果p：EC是纤维化，我们表示物体C上的纤维C by EC和由f诱导的重索引（或替换）函子：C D C byf：EDEC.请注意，重新索引函子在posetal设置中唯一确定。 我们将在下一章中关注三种不同类型的纤维p：E→C：谓词提升的概念被认为是偏序集的纤维化，也就是说，每个纤维EC是偏序集，重索引保持顺序。通过Grothendieck构造[5，8]，偏序集的纤维化p：E→C对应于函子P：Cop→偏序集。在研究通过一组谓词提升而产生的语言时，我们需要在纤维中添加额外的结构来解释命题连接词。因此，我们考虑晶格的纤维化。这些是偏序集的纤维p：E C，其中每个纤维都有有限的满足和连接，它们通过重新索引来保存。在这种情况下，我们解释的语言所产生的一组谓词提升和显示，他们是同态稳定的。通过Grothendieck，格的每个纤维化p：EC唯一对应于a函子P：CopLat，其值在格和连接保持映射和相交保持映射的范畴中。第三类纤维化是框架纤维化。这些都是晶格的纤维化，其中每一个纤维都有无限的满足分布在（有限）连接上（即。是一个帧），需要在重新索引时保留。可以很容易地看出，框架的纤维化对应于函子P：CopFrm，其中Frm是保持有限交和有限联的框架和映射的范畴。这将是审查逻辑表达能力的背景。3模态逻辑与谓词提升考虑任意基范畴上的定态纤维化p：E→CC. 直观地说，内函子T：C→C的谓词提升映射C∈C上的谓词（即，偏序集EC）的元素到TC上的谓词，服从自然性条件。从p：E→C传递到相应的函子P：Cop→Poset，我们得到以下定义：定义3.1（谓词提升）假设T：C → C是一个闭函子，P：Cop→偏序集。T的P-谓词提升是一个自然变换λ：P→P <$Top。通过从函子P：CopPoset传递到纤维化p：E，C的偏序集，我们得到以下，替代特征的fired函子PATTINSON274∈∈→→→→ →→→◦ →P ×P(see[8]，在那里它们被称为纤维化的态射，或[5]，第8.2节，在那里它们被称为carbohydrate函子）。命 题 3.2 （ 谓 词 提 升 是 纤 维 函 子 ） 假 设 T ： C C 和 纤 维 化 p ：E C 通 过Grothendieck构造对应于P：Cop偏序集。 那么，(i) T的P-同品种提升(ii) 函子L：E → E使得（L，T）：p → p是一个可解函子。证明假设λ：PPTop是自然的。 定义L：E E通过L（E）=λ（pE）（E）。 相反，如果（L，T）：p p是固定的，令λ（C）（E）=L（E），对于CC和EEC。这两种结构都以直接的方式转化为态射。✷我们给出一些谓词提升的例子例 3.3 （ i ） 假 设 C 有 回 调 且 幂 次 良 好 ， T ： C→C 保 持 幺 一 箭 头 。 将monosTm：TM→TC到由monicm：M→C表示的子对象的等价类扩展到T的S-谓词提升（其中S：Cop→Poset将对象C∈C映射到其子对象的集合，参见例如。[8]，第1.3节）。(ii) 如果p：E C是偏序集的双artesian纤维化，T：C C是多项式，那么T的逻辑谓词提升，如[7]中所考虑的，是定义3.1意义下的谓词提升。(iii) 设DDCPO是有向完全偏序范畴和Scott连续函数范畴的一个子范畴考虑函子O：Dop→偏序集，它将一个对象D∈D映射到它的斯科特拓扑O（D）。若D是Carnival闭的，且对某个D∈D，TX = XD，则指派<$X open <$→{f∈XD|f（d0）∈o}定义了T的一个O-谓词提升，对所有d0∈D.下一节建立了在赋予函子C op → Lat的范畴上，coal-gebras的逻辑与内函子的谓词提升之间的所需联系。3.1通过谓词提升的在模态逻辑的情况下解释wrt。在Kripke模型中，模态的解释和命题常量的解释都可以通过谓词提升而产生。由于命题常数集P上的Kripke模型是函子TX=（X）（P）的余代数，我们证明了余代数的一个逻辑，它被解释为：谓词提升，值得属性“模态”。模态逻辑和谓词提升之间的关系是下一个例子的目的，来自[13]。例3.4假设TX=P（X）× P（P），用命题常数的固定集合P建模克里普克模型，设2：Setop→Poset表示PATTINSON275→LPL对于T.反变幂集函子 函数[P]（X）：2 X→ 2 P（X）×P（P）定义为[P]（X）（x）={（y，p）∈ P（X）×P（P）|y<$x}是2-谓词提升给定T-余代数γ：C→ P（C）× P（P），相应的算子γ−1<$[P]：2 C→2 C是模态逻辑的<$-算子：的确，给定c<$C，我们得到γ−1<$[P]（c）={c∈C| <$CJ∈C. c→CJ=<$CJ∈c}，其中对于γ（c）=（c，p）<$cj∈ C，我们记为C→cj。另外，给定一个命题常数p∈P，则由[p∈P]（X）（x）={（c，p）∈ P（X）× P（C）|p∈p}是谓词提升。给定γ：C→ P（C）× P（P），则与[p∈P]相关联的（常数）算子γ−1<$[p∈P]：2C→ 2C产生了使p有效的状态集。更精确地说，给定任何子集c<$C，我们有γ−1<$[p∈P]（c）={c∈C|C|=p}，其中c|=p是γ（c）=（c，p）<$p∈p的简写。注意，谓词提升可以用来解释原子命题和模态。这使我们考虑逻辑，这是解释wrt。签名函子的一组谓词提升。为了也解释命题连接词，我们需要在命题纤维化p的纤维EC中的连接和会合：E C。对于一个更丰富的逻辑语言，人们也可以包括海廷蕴涵，如果posetalfibration支持它的解释。我们避免这样做，因为蕴涵是不需要获得的结果，关于表达的余代数模态逻辑。假设C有一个终端对象1∈C，P：Cop→Lat是一个函子（产生格的纤维化p：E→C），T：C→C是一个内函子。 给定T的P-谓词提升的集合PL，与PL相关联的语言L（PL）是包含以下项的公式的最小集合：• 作为原子命题的元素p∈P（1）• 对于每一对（φ，φ）公式，• 当λ∈ PL且φ∈ L（PL）时，给出了[ λ ] φ的公式.我们模糊了语法和语义之间的区别的水平上的propo- sitional常数，以避免符号开销有关的解释公式。注意，由于P（1）是一个格，语言（）包含真和假作为原子命题。给定一个T-余代数（C，γ：C→TC），公式φ∈L（PL）wrt. （C，γ）则作为一个谓词[[φ]]γ∈P（C）在载体上C∈C。归纳定义如下：• 对于p∈P（1），设[[p]]γ=P（！）（p）在哪里！表示到终端对象1∈C的唯一态射。• 在P（C）中，命题连接词通过连接和相遇来解释• 若φ∈L（PL）且λ∈PL，则[[λ]φ]γ=P（γ）<$λ（C）（[[φ]]γ）。关于通过谓词提升解释的逻辑，我们注意到的第一个性质是解释是同态稳定的。PATTINSON276→⊆→→×命题3.5（余代数同态下的稳定性）设P：Cop→Lat是函子且1 ∈C。如果PL是T：C → C的P-谓词提升的集合，则[[φ]]γ=P（f）（[[φ]]δ）对所有T-余代数态射f：（C，γ）→（D，δ）和所有公式φ ∈ L（PL）.对于命题连接词和原子命题来说，这个主张是直接的，因为P（f）保持（有限）连接和满足。给定一个自然变换λ：P→P<$Top∈PL，我们必须证 明 P （ f ） （ [[λ]φ]]δ ） =[[λ]φ]]γ ， 给 定 归 纳 假 设 [[φ]]γ=P （ f ）（[[φ]]δ）。这是通过计算P（f）（[[λ]φ]δ）=P（f）<$P（δ）<$λ（D）（[[φ]δ）=P（δf）<$λ（D）（[[φ]]δ）=P（Tf<$γ）<$λ（D）（[[φ]]δ）=P（γ）<$P（Tf）<$λ（D）（[[φ]]δ）=P（γ）<$λ（C）<$P（f）（[[φ]]δ）=P（γ）<$λ（C）（[φ]δ）=[λ]γ，利用f是同态的事实和λ的自然性。✷换句话说，解释是不变的。余代数态射当C=Set且P= 2：SetopLat是逆变幂集函子时，我们得到了双相似点（在Aczel和Mendler [3]的意义下）满足同一组公式的直接推论此外，当考虑子范畴DDCPO上的内函子T：DD的余代数时（如[19，20]中所示），该结果意味着（有序）双相似性意味着逻辑等价。4表现力这一节研究了由一组内函子T：C C的预提升所给出的逻辑的表达能力。我们在前一节中已经看到，公式的解释wrt。通过对φwrt的解释，可以得到任意余代数（C，γ）.终端余代数这一节的研究对象是终结余代数（的载体）上的谓词类，它可以用模态公式表示由于基数的原因，我们不能期望最终余代数的载体上的所有谓词都可以由基数原因的公式表示。例如，考虑函子TX=L X在集合范畴上。 众所周知（见[4]），最终余代数的载体是Z=LN，从自然数集合N到L的函数集合。如果L的基数大于1，则LN不可数，因此P（LN）不可数。怎么--PATTINSON277→→∈→{···|∈ S{LPLSPL然而，给定一个谓词提升的有限集合，我们只能表示Z的子集的可数集合。在这种情况下，有两种方法似乎是可行的：我们可以扩展语言，以适应更大基数的合取和析取，或者我们可以将注意力限制在这两种方法都需要从格的纤维化转移到纤维中具有“无限结构”的纤维化，以解释无限合取/析取。这使我们在后续中考虑框架的纤维化，最好的例子是拓扑空间，它有开子集作为纤维。我们不直接处理框架的纤维化，而是将它们表示为函子P：CopFrm，其中Frm表示在有限交和有限联接中保持的框架和映射的类别。一个框架L的子集B称为一个基，如果对于所有l∈L，我们有l ={lJ∈ B|lJ≤l}。 请注意，每个帧都有一个基础，也就是它的底层集合。一个子集称为L的子基，如果集合l1l kkN 11，...，Lk是L的一个基。显然L的每一个碱基也是一个底层。我们继续给出条件，这些条件确保公式的表示集wrt。最终余代数（Z，Z）构成Z上谓词框架的基。这将允许我们用逻辑的公式来表示终端组合上的用无限个析取来扩展逻辑，就产生了一种语言，在这种语言中，Z上的每一个谓词都有一个指称。为了获得具有这种性质的语言，需要两个不同的条件：谓词提升的集合必须是充分完备的（也就是说，我们可以在（）的公式中编码足够的信息）。第二个条件涉及签名函子T：C C和描述相对于对象CC的谓词的函子P：CopFrm之间的相互作用。由于我们通过逆极限构造来构造最终T-余代数，我们要求P将极限锥（在C中）映射到上极限（在Frm中），即极限上的谓词由逼近上的谓词确定。定义4.1（谓词提升的完备集假设P：Cop→从OP和T：C → C。我们称T完备的P-谓词提升的集合PL，如果对所有C∈C，{λ（o）|o ∈ B}λ∈PL是P（TC）的子基，只要B是P（C）的基。从逻辑上讲，这意味着我们可以通过P（C）的基、谓词提升和有限连词的集合来表示P（TC）的基的元素。关于谓词提升的完整集合的例子，我们请读者参考第5节，在那里更详细地研究了域范畴中的情况。PATTINSON278T！3∈→→→PLL PL→1JJJJJJ第二个要求是关于Pwrt的良好可解释性。T. 由于我们构造了终结T-余代数作为序列1，，！T1，T，！T212，T1···，记为（Tn1）n∈N，则需要该极限存在并被T保持.（Tn1）n∈N的极限上的谓词由逼近项Tn1上的谓词决定，这意味着（Tn1）n∈N的极限由Pop：C→Frmop保持.这是《定义4.2假设T：C C是闭函子且P：CopFrm.我们说T满足近似要求wrt。P，如果• C有一个终结对象1C，且极限L=Lim（Tn1）n∈N存在于C中，且• T和Pop都保持这个极限。虽然这些条件是相当技术性的，但它们存在于激发本研究的例子中，即域范畴上的局部连续内函子，我们将在下一节中建立它们给定一个函子满足近似要求的谓词提升的完备集，我们可以（最终）证明终结余代数上的每个定理4.3（ （假设P：CopFrm和T：C C满足近似要求。如果（Z，Z）是最终的T-余代数，则{[[φ]]}|φ∈L（PL）}是P（Z）的基，只要PL是T的P-谓词提升的完备集。我们推迟证明以陈述辅助证据引理4.4设D=（（On）n∈N，（fnm：On→Om）n≤m∈N）是一个图，Frm具有上极限余锥（O，（fn：O n→ O）n∈N）. 如果Bn是O n的基，a lln∈N，则n∈N{fn（b）|b∈Bn}是O.证明设x∈O. 因为O是Frm中D的共限锥的顶点，我们可以将x表示为X=i∈Ixi···xk（i）对于某个指标集I和xi∈n∈N{fn（o）|o∈O n}，其中i ∈ I且j ≤ k（i）。如果i∈On，也就是说，我们可以用On的基Bn的元素来逼近xi，对于某个子集Xi<$Bn，xi=Xi。 因为fn是一个框架同态对n∈N，O的分配律包含有✷使用上面的引理，我们准备好了定理4.3证明设（Z，（pn：Z→Tn1）n∈N）是序列（Tn1）n∈N的极限锥.由于T保持这个极限，XPATTINSON279DL∧DL→ D ∈ LL→ D≤：Z→TZ是final coalgebra。我们定义一个子集序列（Ln）n∈NL（PL）的子集的集合和序列（Dn）n∈N，其中Dn<$P（Tn1）如下：对于n = 0，设0=0= P（1）（注意P（1）的元素是原子命题）。假设0

下载后可阅读完整内容，剩余1页未读，立即下载