有限秩与变元逻辑的Pebbling余项及其在等秩变元同态保持定理下的研究

可在www.sciencedirect.com在线获取理论计算机科学电子笔记352（2020）191-209www.elsevier.com/locate/entcs有限秩与变元逻辑的Pebbling余项及其在等秩-变元同态保持定理托马斯·潘恩1牛津大学计算机科学系摘要在本文中，我们使用有界量化秩和变量计数（以及对偶树宽度和树深度）的共元公式来重新证明Rossman算一路上，我们给出了所需的comonads的阐述，显示它们的属性是如何关键词：Pebble游戏，Pebble Comonad，有限秩逻辑，有限变量逻辑，树深，树宽1介绍一阶句子可以通过quantierrank（量化器的嵌套深度）和variablecount（公式中使用的变量数量）来分级。这些在模型有限模型理论和描述复杂性中起着重要作用（参见[3]和[7]），代表了在计算期间绑定资源的想法。在一阶结构方面，与这些概念相对应的是分别被称为树深度和树宽度的参数，它们已经被广泛研究，主要是作为图参数，尽管它们也可以应用于一阶结构。后者是特别众所周知的，因为许多困难，以解决问题变得易于处理类的有界树宽度（最显着的结果也许是[ 4 ]中的Courcelle在图的一元二阶逻辑中，可以在有界树宽的图上在线性时间内判定）。文[1]中对卵石混合物的介绍，1电子邮件：thomas. cs.ox.ac.ukhttps://doi.org/10.1016/j.entcs.2020.09.0101571-0661/Crown版权所有© 2020由Elsevier B. V.出版这是CC BY许可下的开放获取文章（http://creativecommons.org/licenses/by/4.0/）。192T. Paine/Electronic Notes in Theoretical Computer Science 352（2020）191一阶结构和有界变量计数公式之间相互作用的语义解释。此外，通过对pebbling余代数的研究，给出了树宽参数的在第一节中，我们简要概述了量化器秩和变量计数的概述，以及它们与树宽度和树深度的在第二个例子中，我 们 将 pebbling comonad 和 [2] 中 的 Escherichfeucht-Frisse comonad （ 它 是pebbling comonad的类似物，但用于quantifier rank）合成为一个同时捕获quantifier rank和变量count的comonad，并且其余代数可以用于捕获树深度和树宽度。 这是在[1]和[2]中发现的comonads的一个小修改，以便继续第三部分的内容，尽管本文也新颖的是如何推广comonads来处理签名中的常数和自由变量。模型论中的保留定理是一个语义属性和一个一阶句子的句法限制之间的等价，然而其内容几乎总是在给定语义的情况下找到一个句法限制。例如，模型论的经典同态保持定理如下：定理1.1一个一阶句子在结构之间的同态下保持，当且仅当存在语义等价的正存在一阶句子。Rossman在[8]中对此进行了改进，他证明了可以保持公式的数量级：定理1.2（Rossman等秩同态保持定理）设φ是数量秩为n的公式。 然后它在一阶结构之间的同态下保持，当且仅当存在一个语义等价的正存在公式，其数量秩至多为n。在本文的第三部分中，我们遵循Abramsky此外，本发明还用于证明有界量化器秩的公式和用于证明有界量化器秩和变量计数的公式的comonads的明显一致性为Abramsky的简化推广提供了很好的动机猜想1.3（Abramsky的Equirank-Variable Preservation Conjecture）设φ是quantifier秩为n的公式，至多使用k个变量。然后它在同态下保持，当且仅当存在一个语义等价的正存在公式，其quantier秩至多为n，使用至多k个变量。反向蕴涵是明确的，直接的，所以蕴涵是第三节所讨论的.我们尝试通过替换用于验证有界量化器秩的公式的comonads和用于验证有界量化器秩和变量计数的公式的comonads，来对Equirank HPT的证明进行简单的翻译。这对于任意量化器秩n和变量计数都失败k，但在k≥n−2的情况下有效。我们包括一个讨论的证明未能翻译，并指出了一些结果，这将意味着T. Paine/Electronic Notes in Theoretical Computer Science 352（2020）191193氮钾一般情况下。1.1模型理论背景这是打算作为背景材料，所以讨论简短，与草图证明。[5]更多详情。设σ是一个有限的纯关系签名。我们让L（l）表示σ上的一阶公式，其中自由变量出现在x1，.，x l（并写作L：= L（0），即句子超过σ）。我们感兴趣的是L（1）的各种片段，在介绍中提到。设Ln，k（l）是L（l）的最多阶为n的片段，最多有l个变量。请注意，自由变量确实来自允许变量的总数，并且当限制变量计数时，重新绑定变量与不同的量化器对于完全表达是必要的（例如，在有向图中存在长度为n的行走可以用Ln，2中的一个句子来表达）。我们定义Ln（l）：=Ln，n（l）。可以很容易地检查出一个数量级为n的公式可以有效地使用最多n个变量，所以这在语义上捕获了所有数量级为n的公式（具有任何数量的变量），我们永远不需要考虑k > n的情况。我们也对存在正公式感兴趣，因为它们与同态有着密切的联系，同态是用{，，}作为唯一的连接词构造的。我们用一个上标+来修饰一个片段，以表示该片段的子集仅由存在正公式组成我们使用类似的上标需要注意的是，对于上述每一个片段，它的所有存在正公式都可以表示为本原正公式与它的析取。我们在这里立即指出一个非常重要的事实：引理1.4Ln，k（l）是有限的（直到公式等价）。这一点可以通过数量级上的归纳法来证明。这在很大程度上取决于假设σ是有限的和相关的。 作为一个相当明显的结果，L+（l），，则，n，k，n。我们还将σ与范畴Rσ联系起来，R σ的对象是一阶结构，也就是说，集合（称为结构的宇宙）配备有解释每个R∈σ。我们用同一个符号来表示宇宙和结构，这是对符号的滥用。这些结构之间的态射通常是在他们的宇宙之间建立地图，以保持对关系的解释。结构以通常的方式解释句子。我们还定义了一个范畴Rσ（l），它的态射是（A，a<$）型的，其中A∈Rσ，a<$∈Al，并且它的 态射是f：A→B∈Rσ的态射，使得f（ai）= bi，i =1，，l.来自Rσ（l）的结构可以用于通过使用元组a′来解释来自L（l）的m194T. Paine/Electronic Notes in Theoretical Computer Science 352（2020）191氮钾氮钾自由变量For（A，a<$），（B，<$b）∈Rσ（l）我们用e（A，a<$）→（B，<$b）表示态射f：（A，a<$）→（B，<$b）的存在性.如果A和B是有限的，这就等于对每一个φ∈L+（l），（A，a<$）|=φ=φ（B，<$b）|=φ。这促使了以下的翼可以被认为近似同态存在的定义定义1.5对于每个子空间∈L+（l），（A，a<$），Wewrit e（A，a <$）→n，k（B，<$b）|==（B，<$b）|=0。当（A，a <$）→n，k（B，<$b）且（B，<$b）→n，k（A，a <$）时，我们得到（A，a <$）4 n，k（B，<$b）. 我们用→n代替→n，n。注意，由于每个φ∈ L+（l）都可以写成公式的析取，从Ln，k<$（l）中，如果我们愿意，我们可以在上面的定义中量化Ln，k<$（l我们可以用类似的方法对初等等价进行定义1.6对于每一个ε∈Ln，k（l），（A，a<$），我们都可以构造e（A，a <$）<$n，k（B，<$b）|==（B，<$b）|=0。我们用n代替n，n。我们现在通过森林覆盖和k-可标记的森林覆盖来定义树的深度和树的宽度。分别对树深度和树宽度进行边界处理可以被认为是对量化器秩和变量计数进行边界处理的类似物，我们很快就会看到对于一个带根的森林（F，r′）（其中F是顶点集，r是根的集合），分支是从顶点到其根的唯一路径，森林的深度是在单个分支中出现的顶点的最大数量。定义1.7·A ∈ Rσ，G（A）的Gaifman图是一个无向简单图，其顶点集为A，如果A 1，a2同时出现在A的某个保护元组中，则a 1，a 2之间有一条边（也就是说，存在一个关系R∈σ和包含a 1，a 2的元组a<$∈RA）。• 图G的一个森林覆盖是同一顶点集上的一个分支森林（F，r′），使得只要G中有一条边a1，a2，它们就同时出现在某个分支中荷兰盾• 图G的一个k-标号森林覆盖器是一个森林覆盖器（F，r′），它的顶点c的标号为：F→ {1，. k}，使得只要G中有边a1，a2，并且a1是a2的祖先（也就是说，a1位于从a2到其根的唯一路径上），则对于从a1到a2的唯一路径上的任何a3，我们有c（a3）= c（a1）= a3=a1（或者换句话说，不再使用a1的标签在到a2的路径上，包括在a2处，只要G中存在边a1，a2）。定义1.8·An（n，k）−coverof（A，a<$）isk-labelledrootedforestcoverof深度G（A）至多n• A的一个（n，k）-覆盖是G（A）的k-标记有根森林覆盖，其深度至多为n+1，唯一根为a1，并且使得ai的唯一子是ai+1，T. Paine/Electronic Notes in Theoretical Computer Science 352（2020）191195我我我1LJJi= 1，.， l − 1（人们可以认为这是采取森林覆盖G（A）− {a1，...， al}，然后在顶部的路径中添加剩余的元素）。 为了方便起见，我们还将坚持1，...，所有L都在（n，k）-覆盖中具有不同的标号。• （A，a′）的 树 深 度 是最小的 n，使 得 对 于 k 个 树 存在（ A ， a ′ ） 的（n，k）-cover（如果存在的话）;或者，等价地，存在（n，n）-cov e r（因为对于高度为n的森林，最多只需要n个标签）。• （A，a<$）的树宽是最小的k，使得存在k标记的森林覆盖减1（减1是一种约定，因此树的树宽总是1）我们将主要关注具有（n，k）-覆盖的结构，作为结构的同时深度-宽度分解。在（n，k）-covers和quantier rank以及使用规范查询的变量数量之间存在明确的联系。定义1.9对于有限结构（A，a′），以及其单位a1，.， al，..， am（其中a<$=（a1，...，al）），我们定义它的正则查询y，φ（A，a<$），为：φ（A，a<$）（x<$）：=φx l+1，.， nxm{R（x1，.， xj）：R∈σ，（a1，.，aj）∈RA}规范查询的语义特征在于以下属性：引 理 1.10For （ A， a<$ ） ， （ B ， <$b） inRσ （ l ） ， （ where re （ A， a<$ ）isfinite），B|=φ（A，a<$）（A，a<$）→（B，<$b）证据 这可以通过注意到φ（A，a<$）在（B，<$b）中的见证与映射f：（A，a<$）→（B，<$b）之间的（稍微尖锐的）对应来证明。Q引理1.11如果（A，a<$）有（n，k）-c环，则φ（A，a<$）等价于一个公式φ∈ Ln，k∈（l）.证据直觉上，这是写一个关于结构的森林覆盖的句子，每个顶点对应一个量化器（或自由变量，在1，...，a l）。 在一个顶点a上，我们用变量xc（a）进行量化（回想c（a）是a的标签），并列出a及其标签没有被重用的祖先的所有原子命题。（n，k）-覆盖的结构确保我们不会错过任何原子命题。Q我们也可以将一个结构与一个给定的原始肯定句相关联，称为术语模型：定义1.12设φ∈ Ln，k∈（l）.为了便于标记，使用变量x j重写φ，其中变量x1，.，在φ中使用x k，上标j表示到目前为止x i被量化的次数（当x i出现自由时使用j = 0）。将C φ定义 为具有宇宙{c：x发生在n中}的结构，{c0，.， c0}（到确保我们对每个自由变量都有一个见证人，即使它们不满足任何关系。196T. Paine/Electronic Notes in Theoretical Computer Science 352（2020）191引物tions）区别元素（c0，...，c0），并且满足原子关系R（c j1，.，（c、j、m）1l i1im当且仅当R（x j1，...，x jm）发生在φ中。i1im引理1.13Forφ∈Ln，kpri m（l），（B，<$b）∈Rσ（l），Cφ→（B，<$b）≠（B，<$b）|=φ。是的。事实上，有一个共享的对应关系：{participateeswhitnessingφin（B，<$b）}{mapsf：Cφ→（B，<$b）}.Q引理1.14若φ∈ Ln，k∈（l），则C φ有（n，k）-覆盖。证据在森林覆盖中，使用量化器之间的直接作用域关系作为父关系，在φ中标记变量用于标记森林覆盖。Q引理1.15对于每个n，k，l，存在有限结构Fn，k，l的有限集<$Rσ（l），eachwitan（n，k）-c，前提是对于每个（A，a<$）∈Rσ（l），re存在（C，c<$）∈Fn，k，l使得（A，a<$）4n，k（C，c<$）。证据为了得到这样一个集合，选择有限个公式φ∈ Ln，k∈（l）来覆盖Ln，k∈（l），直到公式的等价，并取Fn ，k，l为这些公式的项模的集合。若（A，a<$）∈Rσ（l），则我们可以求出φ∈Ln，kprim（l），uch，φ：= {φ∈Ln，k（l）：（A，a′）|=φ}。 我们将证明Cφ4n，k（A，a′）.Q我们注意到，上面的引理依赖于签名σ的有限性，并且仅仅是选择等价集Ln，k<$（l）的有限个的代表的类似。在本文的其余部分中，我们用上述性质为每个n，k，l事实上，我们可以从结构的角度重新表述→n，k关系引理1.16For（A，a<$），（B，<$b）∈Rσ（l）（A，a<$）→n，k（B，<$b）当且仅当对每个（C，c<$）∈Rσ（l），其中an（n，k）-c在，（C，c<$）→（A，a<$）=n（C，c<$）→（B，<$b）.证据 我们在 一 个 方 向 上 使用规范查询，另一个是CφQ此外，我们可以通过以下引理重写（n，k）-保持猜想：引理1.17结构类M在→n，k下保持不变（也就是说：如果（A，a<$）∈M且（A，a<$）→n，k（B，<$b）则（B，<$b）∈M）当且仅当re是some+氮钾(l) 使得Mod（φ）= M。证据相反的方向是明确的。对于前向，关键是定义FJ：={（C，c<$）∈Fn，k，l：（C，c<$）∈M}，并设置φ={φ（C，c<$）：（C，c<$）∈FJ}. 可以很容易地证明φ满足所要求的性质。Q推论1.18在→n，k下公式<$∈ L保持当且仅当存在φ∈LT. Paine/Electronic Notes in Theoretical Computer Science 352（2020）191197氮钾某个φ ∈ L+（l）与它语义等价。198T. Paine/Electronic Notes in Theoretical Computer Science 352（2020）191通过上面的引理，我们现在可以陈述（n，k）-保持猜想的结构版本：猜想1.19任何在n，k和→下保持的结构类M在→n，k下也保持.这个版本类似于在[ 8 ]中证明的，也是我们将关注的。（n，k）-保持猜想将从这个设置M = Mod（k）得出，对于给定的在→下保持的k。在上面的猜想中，设n等于n的数量级，k等于变量的个数，然后应用引理，得到所需的结果。2游戏Comonads在这里，我们涵盖了稍后需要的游戏Comonads，我们将通过使用→ n，k的递归特征来激发它。这些将同时捕获→n，k和（n，k）-覆盖作为comonad的特征。这种类型的Comonads在[1]中首次介绍，并在[2]中进一步探索。我们给出了→ n，k的递归定义（在n上递归，对于固定的k）。我们称从A到B的部分态射是从A → B的部分映射，它是由部分映射的定义域诱导的A的子结构上的态射，并使用a<$[α/ai]来表示元组a<$，其中第i个尝试与α进行了交换定义2.1·（A，a<$）→0，k（B，<$b）：asignmentai从A到B的态射bi定义部分• 若n>0， l →bi定义从A到B的部分态射，且对每个α∈A，存在β∈B使得（A，a<$，α）→n−1 ， k（B，<$b，β）。• 若n>0， l=k，则then n（A，a<$）→n，k（B，<$b）：asign ntai<$→bi定义从A到B的部分态射，且对每个α ∈ Ai ∈ {1，.， l}，存在β ∈ B使得（A，a<$[α/ai]）→n−1，k（B，<$b[β/bi]）。我们在这里稍微滥用符号，使用相同的符号→n，k。可以用归纳法证明，f→ n，k的上述特征与已经证明的其他特征一致。我们也有一个递归的特征化的n，k：定义2.2·（A，a<$）<$0，k（B，<$b）： ai→bi定义了从A到B的部分同构。• 若n>0， l →bi定义了从A到B的部分同构，且对每个α∈A，存在β∈B使得（A，a<$，α）<$n−1 ，k（B，<$b，β），且对每个β∈B ，存在α∈A使得（A，a <$，α）<$n−1 ，k（B，<$b，β）。• 如果n>0， l=k，则 thenn（A，a<$）<$n，k（B，<$b）：同构，且对任意α∈A，存在β∈B使得T. Paine/Electronic Notes in Theoretical Computer Science 352（2020）191199→（A，a<$[α/ai]）<$n−1，k（B，<$b[β/bi]），并且对每一个β∈B，存在α∈A使得（A，a<$[α/ai]）<$n−1，k（B，<$b[β/bi]）.以上也可以被描述为玩家Spoiler和Duplicator之间的两个玩家游戏，通常被称为Escherichfeucht-Fraisse游戏（[6]）。在描述结构A和B之间→ n，k的博弈中，（n，k）-卵石博弈Spoiler有k个卵石，在n轮中的每一轮他都把一个卵石放在A的一个元素上（l< k情况），或者把一个现有的卵石从A的一个元素移到另一个元素上（l = k情况）。在每一轮中，复制者在B中做出同样的反应，他的目标是确保通过观察鹅卵石生成的部分地图是部分态射。 这是一个定理，复制者可以赢得（n，k）-卵石游戏，无论如何破坏者发挥当且仅当An，k B。结构（A，a<$）和（B，<$b）之间的（n，k）-卵石博弈是A和B之间的（n+1，k）卵石博弈，其中第一步已经固定（剧透者玩1，...，a 1，复制者响应b1，...，b l.）有一个类似的游戏和定理的n，k关系。我们坚持在两个游戏中，剧透必须放置所有的k卵石，然后才开始移动它们。这是一个等价的游戏（在这个意义上，复制者总是可以赢得一个，当且仅当他总是可以赢得另一个），如果我们允许剧透开始移动鹅卵石之前，他已经把所有的鹅卵石。（n，n）-博弈（没有鹅卵石的移动）通常被称为n轮Escherichfeucht-Fraisse博弈。这个游戏只包括Spoiler将鹅卵石放在结构A上，Duplicator用结构B中的元素进行响应（目前，我们只关注类别Rσ）。复制者只有在A→nB时才能赢得这场比赛。 为了简单起见，我们首先考虑l=定义2.3对于一个结构A，设EnA是长度不超过n的A元素的（非空）序列的集合，设A：EnA→A是给出序列最后一个元素的函数。在n轮Escherichfeucht-Fraisse博弈中，复制者的（确定性）策略恰好是函数f：EnA→B。 如果剧透播放 1， 2，... a n，Duplicator简单地播放f（[a1]），f（[a1，a2]），.，f（[a1，.，a n]）。这给出了映射f：EnA→B和复制者策略之间的精确我们将赋予EnA一个关系结构，使得如果映射f是态射，那么它就是一个获胜策略，但首先我们将考虑一般（n，k）-卵石博弈的策略定义2.4对于一个结构A，设Pn，kA是A× {1，...，k}，长度最多为n，使得第二个坐标在序列的前k个条目内不重复（即，如果s∈Pn ， kA，并且i∈{1，.，k}，则i在s）的前k个条目中作为第二坐标至多出现一次。再一次（稍微滥用符号），令A →A：Pn ，kA→A表示序列最后一个元素的第一个坐标（即从A开始的条目）与上面类似，复制者在（n，k）-卵石博弈中的策略恰好是函数f：Pn，kA→B。由于必须跟踪鹅卵石可以移动的事实，这种情况稍微复杂一些。在这种情况下，f（[（a1，i1），...，（a j，i j）]）表示复制器将在a的第j轮中播放的内容200T. Paine/Electronic Notes in Theoretical Computer Science 352（2020）191游戏中，在第m轮，剧透放置（或移动）卵石im到一个m。我们现在赋予我们的集合以关系结构，并给出一些关于我们为什么这样做的直觉。对于s1，s2序列，s1和s2表示s1是s2的前缀，s1和s2表示s1和s2是s2和s1的前缀。对于s∈Pn，kA，我们将其最后一个元素的第二个坐标称为pebble指数。定义2.5对于A∈ Rσ，R∈σ：• 对于EnA：（s1，...，s j）∈ REnA当且仅当：(i)（第A条第1款），.... <$A（sj））∈ RA.(ii) 对于每个i1，i2∈ {1，.，j}，我们有s i1 s i2。• 对于Pn，kA：（s1，...，sj）∈RPn，kA当且仅当：(i)（第A条第1款），.... <$A（sj））∈ RA.(ii) 对于每个i1，i2∈ {1，.，j}，我们有s i1 s i2。(iii) 对于每个i1，i2∈ {1，.，j}，如果s i1<$s i2，则s i 1的卵石指数不作为s j中的第二坐标出现，其中s i2 = s i1sJ。我们可以理解EnA（或Pn，kA）上关系的这些定义，简单地作为对态射f：EnA→B施加条件的一种方式。第一个条件帮助我们确保态射f：EnA→B包含来自{a1，.，a j}到{f（[a1]），...，f（[a1，.，a j]）}，如在n轮Eschericht-Fraisse游戏中所要求的。第二个条件确保我们没有要求太多的态射f：EnA→B;如果s1s2，那么它们不能代表同一个游戏中发生的情况，因此它们之间应该没有关系。对于Pn，k回想一下，对于序列s1，f（s1）告诉我们，当Spoiler刚刚将s1的pebble指数（我说pebble）移动到f（s1）时，复制器应该如何响应。如果s1和s2，并且s1的卵石指数在s2中再次出现（在s1之后），这告诉我们卵石i已经移动，因此f（[s1]）和f（[s2]）之间不需要有任何关系这是一个草图证明以下定理：定理2.6对于A，B∈ Rσ，存在一个双射：• 在n轮Escherichfeucht-Fraisse游戏中， A到b• 态射f：EnA→ B。或者，在更一般的情况下，存在以下两种情况之间的双射• （n，k）-pebble博弈中Spoiler从A到B的获胜策略• 态射f：Pn，kA→ B.在讨论了（n，k）-覆盖与Pn，kA的关系之后，我们将不给出详细的证明，而是稍后证明下面稍微弱一点的结果（因为我们将使用它）。定理2.7对于Rσ中的A，B：• A →nB当且仅当En A → BT. Paine/Electronic Notes in Theoretical Computer Science 352（2020）191201R• A→n，k B当且仅当Pn，k A→ B现在我们展示赋值A→Pn，kA的范畴性质。注意，En在形状上类似于集合范畴上的（非空）列表comonad，促使我们做出以下定义：定义2.8通过函数的逐点应用，我们将En转化为函子。另一方面， 对于A，B∈Rσ，f：A→B，Enf（[a1，...， aj]）：=[f（a1），.，f（aj）]]。同样，我们通过逐点应用而不接触，将Pn，k转化为函子卵石指数，所以f（[（a1，i1），...， （a j，i j）]）：=[（f（a1），i1），.， （f（a j），i j）]。和前面一样，我们滥用符号，对函子En和Pn，k使用相同的δ。定义2.9对于A∈ Rσ，递归地（在序列的长度上）定义δ：EnA→EnEnA• δA（[a]）：=[[a]]• δA（s[a]）：=δ（s）[s[a]]换句话说，δ A（[a1，.， a j]）=[[a1]，[a1，a2]，...， [a1，.， a j]]，[a1，...，a j]。与前面类似，我们给出了Pn，k的类似定义，保持卵石指数固定。• δA（[（a，i）]：=[（[（a，i）]，i）]• δA（s[（a，i）]：=δ（s）A[（s[（a，i）]，i）]上述定义是根据以下定理做出的：定理2.10（En，n，δ）和（Pn，k，n，δ）是余单子。通过与集合范畴上的标准列表comonad相比较，我们将得到所有必要的图都是可交换的。唯一需要验证的是，我们所定义的一切确实是Rσ中的态射，这很容易从我们的定义中得出。现在我们把它推广到范畴σ（l）。如上所述，由结构（A，a<$）和（B，<$b）组成的（n，k）-博弈就是这样一个（n，k+l）博弈，其中我们有一个固定的破坏者和复制者的第一步。因此，我们做出如下定义：定义2.11For（A，a<$）∈Rσ（l）：• En（A，a<$）是En+1A的诱导子结构，在子集{s∈En+1A：s<$[a1，.，al]}。我们认为它是Rσ（l）中的一个结构，ple（[a1]，[a1，a2]，.，[a1，.， a 1]）。• Pn，k是Pn+1，kA在子集{s∈Pn+1，kA：s<$[（a1，1），.，（al，l）]}。我们认为它是Rσ（l）中的一个结构，通过区分元组（[（a1 ，1）]，[（a1 ，1），（a2，2）]，.，[（a1，1），.， （a l，l）]）。我们（懒洋洋地）重新使用ε和δ来表示由我们以前的ε和δ映射的限制给出的明显的自然变换，并且通过限制类似地定义En和Pn，k在映射上的作用（实际上，我们甚至在不同的上下文中重新使用En和Pn ，k;希望这里不会发生混淆）。202T. Paine/Electronic Notes in Theoretical Computer Science 352（2020）191这个定义正如人们所希望的那样：引理2.12（En，n，δ）和（Pn，k，n，δ）是Rσ（l）上的余单子。引理2.13Rσ（l）中的For（A，a<$），（B，<$b）：• En（A，a<$）→（B，<$b）当且仅当（A，a<$）→n（B，<$b）。• Pn，k（A，a<$）→n，k（B，<$b）当且仅当（A，a<$）→n，k（B，<$b）。我们现在可以看到这些comonads如何给我们树深度和树宽度的新特征（通过（n，k）-covers），如[1]和[2]中所证明的。定理2.14：• C oalgebra r作为一个结构（A，a′）作为一个单子En.• 对于深度不超过n的（A，a′），以下两者之间存在一一对应关系• C oalgebra r作为一个结构（A，a′）作为一个同态Pn，k.• （n，k）-（A，a′）的c个遍历。证据一旦仔细地拆开（n，k）-覆盖的定义，我们将看到以下对应关系：(i) 森林在顶点集A上，以路径 a1，...，a l深度至多n+1个ParticipSet映射（A，a<$）→En（A，a<$）（分别代表可区别元素），使余代数图可交换.(ii) 深度至多为n的（A，a<$）的剩余代数（A，a<$）→En（A，a<$）(iii) （A，a<$）参与余代数（A，a<$）→Pn，kA的（n，k）-算子现在来看看细节：(i) 请注意，树的数据可以通过指定每个顶点到其根的唯一路径来给出。这个数据当然可以表示为函数F：A→En+1A。当然，并非所有这种类型的函数都描述以路径a1，..，阿湖函数为以路径a1，...，a l是精确的，F限制于函数（A，a<$）→En（A，a<$）（最前面的起点是路径a1，.， al），δ（F（a））=a对于每个a∈A（即到a的唯一路径以a结束），δ（F（a））= F（F（a））对于每个a∈A（如果一些b位于唯一路径a上的路径上，则F（b）是F（a）的以b结束的唯一前缀）。我们已经内联地写出了定义余代数的交换图，因此我们有对应关系（i）。(ii) 现在假设F满足（i）中的性质。F是态射当且仅当，对于每个元组b1，.，bj，且R∈σ，（b1，.， bj）∈R（A，a<$）=<$（F（b1），.， F（bj））∈REn（A，a<$）.当（F（b1）），.，.时，结果为真（F（bj）））∈R（A，a<$）且，T. Paine/Electronic Notes in Theoretical Computer Science 352（2020）191203对于b1，...， bj，F（b）<$F（bJ）. 由于第一个条件由（i）中关于F的假设满足，所以我们只需要检查第二个条件。我们重申如下：只要G（A）中有一条边b，bJ（回忆G（A）是A的Gaifman图，两个顶点之间有一条边，如果和通常， 所述 RE 是 相同 的（ B1 ，...， bj ）包含b ，bJ和关系R∈σ，使得（b1，.， b_j）∈R_A）有一个v e F（b）<$F（b_J）. 由于F（b）描述了从b到它的根的唯一路径，我们有F（b）<$F（bJ），当且仅当b和bJ位于同一分支上。综上所述，我们有F是态射当且仅当只要G（A）中有边b，BJ，则b和BJ与由F描述的森林位于同一分支上，即当且仅当F描述f（A，a′）的森林。这就完成了通信（二）。(iii) 对于（A，a<$）在共单子En上的余代数F，我们可以很容易地看出将F转化为Pn，kA的映射所需的数据与F所描述的森林覆盖的k -标号函数之间的对应关系.这是一个简单的检查，我们将得到一个态射，当且仅当标签将F描述的森林覆盖变成一个（n，k）-覆盖。Q我们陈述下面的直接推论：推论2.15形式Pn，k（A，a<$）（对于某些（A，a<$）∈Rσ（l））的一个环结构有δA提供的一个余代数，因此总有一个（n，k）-覆盖.这个定理告诉我们，（n，k）-覆盖的范畴就是群Pn，k的Eilenberg- Moore范畴.它还提供了2.7的证明：定理2.16（2.7的重述）Rσ（1）中的F（A，a<$），（B，<$b）：• （A，a<$）→n（B，<$b）当且仅当En（A，a<$）→（B，<$b）。• （A，a<$）→n，k（B，<$b）当且仅当Pn，k（A，a<$）→（B，<$b）。证据 我们只是证明了第二个陈述，使用组合特征-n，k。¯Sup pose（A，a<$）→n ， k（B ，b）. Since<$Pn ， k （A，a<$）hasan（n，k）-cover，andPn，k（A，a<$）→A，则n有Pn，k（A，a′）→（B，b）。N满足Pn，k（A，a<$）→（B，<$b）. 设C为（n，k）-c，且（C，c′）→（A，a′）. 由于（C，c<$）h是一个（n，k）-代数，所以它有一个余代数，并且hus（C，c<$）→Pn，k（C，c<$）. 通过函式y，Pn，k（C，c<$）→Pn，k（A，a<$），并将其中的b与假设放在一起，我们得到（C，c<$）→（B，<$b）.Q3保存定理现在我们要进一步证明第一节末尾所讲的内容（即一个在→下闭的类M和在→n，k下闭的类M）。我们的证明将基本上暴露罗斯曼证明思想是著名的伴随结构方法。也就是说，给定Rσ中的A，我们希望找到A，Pn，kA满足：204T. Paine/Electronic Notes in Theoretical Computer Science 352（2020）191（i）A→A（二）（三）其他事项An，kPn，kAPn，kA→Pn，kA然后证明将遵循，给定A∈M和B∈ Rσ，使得A→n，kB，遵循以下图表（使用M的闭包性质，我们可以获得B∈M）：An，kPn，kAAPn，kA B事实上，我们会找到比这更多性质的结构，但我们将其作为澄清论点的策略。我们的目标是沿着4 n，k关系建立nn，k关系，直接推广[ 8 ]中所谓的n-可扩性。考虑一对A4n，kB.由→ n，k的递归定义，对于任何b∈B，存在某个a ∈ A使得（B，b）→n−1，k（A，a）。 如果我们的目标是保持构建同构，我们可能会发现a∈A具有（A，a）4n−1，k（B，b）的性质，因为这将确保{a}<$和{b}之间的部分同构。我也可以这么做任何b∈B（当然是相对于B的某个元组b），反之亦然，则我们会有An，kB. 我们在下面更正式地说明这一点：定义3.1A∈ Rσ是（n，k）-可扩的，如果对每个：• 0

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