A graph class 𝒞 is monadically dependent if one cannot interpret all graphs in colored graphs from 𝒞 using a fixed first-order interpretation. We prove that monadically dependent classes can be exactly characterized by the following property, which we call flip-separability: for every r∈ℕ, ε>0, and every graph G∈𝒞 equipped with a weight function on vertices, one can apply a bounded (in terms of 𝒞,r,ε) number of flips (complementations of the adjacency relation on a subset of vertices) to G so that in the resulting graph, every radius-r ball contains at most an ε-fraction of the total weight. On the way to this result, we introduce a robust toolbox for working with various notions of local separations in monadically dependent classes.
现实世界中的人往往对未来回报有模糊的了解,对此量化是不可行的或可取的。 我们认为,语言具有不同的传达模糊信息的能力,在主观期望中起着重要但鲜为人知的角色。 从经验上讲,我们发现在他们的报告中,分析师在语言表达中包括有用的信息,而不是数字预测。 具体而言,分析师报告的文本语调具有预测误差和随后数字预测修订的预测能力,当分析师的语言模糊时,当不确定性更高时,当分析师更忙时,这种关系变得更加牢固。 总的来说,我们的理论和证据表明,一些有用的信息是模糊的,只能通过语言传达。
有效的强制技术允许人们证明在设置理论模型中,封闭系统T项类型(ι→ι)→ι的表示是一个连续函数(N→N)→N。 为此,通过逻辑关系定义和与设置理论语义相关的替代对话树语义。 在本文中,我们应用有效的强迫来表明系统T术语的对话树本身是系统T定义的,使用树的教会编码。
现实世界中的人往往对未来回报有模糊的了解,对此量化是不可行的或可取的。 我们认为,语言具有不同的传达模糊信息的能力,在主观期望中起着重要但鲜为人知的角色。 从经验上讲,我们发现在他们的报告中,分析师在语言表达中包括有用的信息,而不是数字预测。 具体而言,分析师报告的文本语调具有预测误差和随后数字预测修订的预测能力,当分析师的语言模糊时,当不确定性更高时,当分析师更忙时,这种关系变得更加牢固。 总的来说,我们的理论和证据表明,一些有用的信息是模糊的,只能通过语言传达。
双向模态mu-calculus是(标准)单向mu-calculus与反(向后看)模式的扩展。 对于这个逻辑,我们引入了两个新的序列式证明演算:一个非有根据的系统,承认无限的分支和一个使用注释的循环版本。 正如在双向模态逻辑的序列系统中常见的一样,我们的微积分具有分析剪切规则。 我们的方法与众不同的是使用所谓的微量原子,它有助于在证明理论设置中应用Vardi的双向自动机。 我们证明了这两个系统的健全性和完整性,随后使用循环演算来表明双向mu-calculus具有(本地)Craig插值属性,涉及命题和方式。 我们的证明使用Maehara方法的版本,以适应循环证明系统。 作为推论,我们证明双向mu-calculus也享有Beth的可定义属性。
有效的强制技术允许人们证明在设置理论模型中,封闭系统T项类型(ι→ι)→ι的表示是一个连续函数(N→N)→N。 为此,通过逻辑关系定义和与设置理论语义相关的替代对话树语义。 在本文中,我们应用有效的强迫来表明系统T术语的对话树本身是系统T定义的,使用树的教会编码。
对Z类不同组的亚移的研究,如Z^d,d≥2,近年来一直是深入研究的主题。 这些调查揭示了动力学和递归理论之间的显著联系。 关于这些系统动态的不同问题已经用递归理论术语回答。 在这项工作中,我们进一步探索了这种联系。 我们使用可计算分析框架来探索公制空间上有效的动态系统类别,并将这些系统与有限类型(SFT)在组上的子移位联系起来。 我们证明,一般公制空间上的每一个有效的动力系统都是拓扑尺寸为零的有效动力学系统的拓扑因素。 我们将这一结果与现有的模拟结果相结合,以获得作为SFTs因素的系统的新示例 我们还研究一种称为Medvedev度的组子移的共轭不变性。 这种不变性是算法性质的复杂性度量。 我们为任意有限生成组的子移位开发这些度的基本理论。 使用这些工具,我们能够对SFT和几个组上的其他子移类的这种不变值进行排序。 此外,我们建立了这些度与所有子移空间中隔离点的分布之间的联系。 在研究梅德韦杰夫亚移位度的激励下,我们还考虑了图形上的组的翻译类动作。 我们证明每个连接的、局部的有限和无限图形都承认Z的翻译,并且当图形有一两个端时,这个动作可以完全选择过渡。 这概括了 Seward 关于 Z 在有限生成的组上的翻译类操作的结果。
我们提出了两个看似不同的建设性有序指数定义,其中序曲被视为一个过渡性的,扩展的,有根据的顺序。 第一个定义是抽象的,使用序数的至上,并且完全由预期的方程驱动。 第二个更具体,基于减少列表,可以被视为Siepiński基于有限支持的函数的经典构造的建设性版本。 我们表明,我们的两种方法是等价的(无论何时提出问题都是有意义的),并使用这种等价物来证明指数的代数定律和可判定性。 我们的工作是在同源类型理论的框架内进行的,所有的结果都在证明助理Agda中正式化。
我们探索了合成域理论与与分配格子分类器相关的Grothendieck topoi之间的新联系。 特别是,合成域理论的所有公理(包括归纳定点对象和支配地位的链条完整性)都源于合成准一致性原理的可计数版本,该原理已成为合成代数几何,合成石二元性和合成范畴论统一的核心特征。 带有分布格子对象的topos中的准相干代数和亲和空格空间之间的二元性提供了一套新的技术,用于合成域结构的推理,并揭示了合成域理论的广泛类(更高)的舍法模型。
Guarded Monotone Strict NP (GMSNP) 通过守卫存在量化的任意实体谓词扩展 Monotone Monadic Strict NP (MMSNP)。 我们证明GMSNP的遏制问题是可决定的,从而解决了Bienvenu,十Cate,Lutz和Wolter的公开问题,后来由Bourhis和Lutz重述。 我们的证明还附带了2NEXPTIME对问题的复杂性的上限,这与Bourhis和Lutz对MMSNP的下限相匹配。 为了获得这些结果,我们显著改善了 GMSNP 模型理论特性的知识状态。 Bodirsky、Knäuer和Starke之前都表明,每个 GMSNP 句子都定义了 ω 分类结构的 CSP 的有限结合。 我们表明,这些结构可用于从GMSNP的遏制问题减少到测试称为重新着色的某些地图存在的简单问题,尽管在比GMSNP更通用的设置中; 仔细分析这个产量说是上限。 作为次要贡献,我们通过在这些结构的属性中添加有限形式的同质性来完善Bodirsky,Knäuer和Starke的构造,使逻辑适应未来的复杂性分类,使用为无限域CSP开发的技术进行查询评估。
假设没有多项式大小的布尔电路家族可以分解两个n位素数的所有产品的恒定部分,我们表明,边界算术理论PV_1,即使由锐利的选择方案BB(Σ^b_0)所证明,也不能证明每个数字都有一些素数除数。 根据完整性定理,根据这个假设,有一个PV_1的模型M,其中包含一个非标准的数字m,没有质数因子化。
许多一阶方程理论,如群论或布尔代数,可以通过比原始公理更小的一组公理呈现。 最近的研究表明,方程理论的同源方法为我们提供了获得公理数量的下限的不平等。 在本文中,我们将这一结果扩展到高阶方程理论。 更准确地说,我们考虑简单地键入lambda演算与产品和单位类型和研究lambda术语之间的方程集。 然后,我们定义了给定方程理论的同源组,并表明可以从同源组中计算方程数的下界。
交替均等自动机(APA)为模拟无限行为提供了强大的形式主义,并在正式验证中发挥着核心作用。 尽管它们被广泛使用,但APA背后的代数理论在很大程度上仍未被探索。 在最近的工作中,引入了一个非确定性有限自动机(NFA)的符号,以及通过右线性代数对其方程理论进行声音和完全的公理化。 在本文中,我们将这一行工作扩展到无限单词的设置。 我们提出了双倍化的语法,根据右线性晶格表达式为APA生成符号,并就其方程理论相对于ω-正则语言的标准语言模型提供了自然公理化。 这种公理化的设计是以定点逻辑理论为指导的;事实上,完整性因素通过线性时间μ微积分的完整性而干净。
我们为颞海格代数和时间Esakia空间的类别建立了Esakia二元性。 这包括反向等价的证明和一致性/过滤器/闭合通信。 然后,我们研究了两个关于相关空间/帧的“可达到性”概念,并在有限的情况下显示它们的等价性。 我们使用这些可到达的概念来同时给出简单和亚直接不可还原的时间海廷代数的格子理论和双重顺序拓扑特征。 最后,我们应用我们的二元性结果来证明时间海廷演算的关系和代数有限模型属性。 这与经过验证的特征相结合,使我们能够证明一个关系完整性结果,该结果将有限性和帧属性双重化到亚直接不可还原性,为我们提供了一类有限,易于理解的逻辑框架。
我们研究完全连接的馈向神经网络的损失景观的梯度流,这些神经网络具有常用的连续可微分激活函数,如Logistic,双曲切线,softplus或GeLU功能。 我们证明梯度流要么收敛到临界点,要么向无穷大分化,而损失收敛到渐近临界值。 此外,我们证明了阈值 ε>0 的存在,使得在最优水平以上初始化的任何梯度流的损失值收敛到它。 对于多项式目标函数和足够大的架构和数据集,我们证明最优损失值为零,只能无症状地实现。 从这个设置中,我们推断出我们的主要结果,即任何具有足够良好初始化的梯度流都会分化为无穷大。 我们的证明在很大程度上依赖于o-最小结构的几何形状。 我们用数值实验证实了这些理论发现,并将我们的调查扩展到现实世界的场景,在那里我们观察到类似的行为。
ω-regular语言是常规语言对无限单词设置的自然延伸。 同样,它们也被许多自动机模型所认可,其中最重要的一个是Alternating Parity Automata(APA),Büchi自动机的概括,它既对过渡(具有普遍性,也有存在分支)和接受条件(通过平价条件)表示。 在这项工作中,我们开发了一个循环证明系统,操作APA,由右线性格子表达式的代数符号表示。 这种语法使以前引入的右线性代数的语法加倍,其中包括非确定性有限自动机(NFA)的符号。 这种二元化在我们设计的证明系统中诱导对称性,晶格操作在序列的每一侧都双重表现。 我们的主要结果是ω语言包容性系统的健全性和完整性,充分利用了ω普通语言理论中的博学理论。
我们为一阶牧师的da Costa逻辑的三值扩展提供了一个粗略的语义集,我们在前一篇论文中研究了该逻辑。 语义遵循一阶经典逻辑的语义的通常模式。
关于无限树在描述性设置理论设置的几个笔记。
在使用除 De Morgan 基础(以及,或者,不是,和常数)以外的布尔运算符时,是否有可能编写明显较小的公式? 对于命题逻辑,Pratt给出了一个否定的答案:在一组运算符上的公式总是可以转化为与任何其他完整的运算符的等效公式,并且只有多项式的大小。 令人惊讶的是,对于模态逻辑,图景是不同的:我们表明,消除双implication仅以模态运算符的指数数发生的代价是可能的◊,因此公式大小的指数增长,即De Morgan基础及其由双implication的扩展在简洁性上有所不同。 此外,我们证明任何完整的布尔操作符在简洁性与德摩根的基础上或其扩展通过双implication同意。 更准确地说,这些结果是针对模态逻辑T(因此对于K)显示的。 我们补充它们表明模态逻辑S5的行为是命题逻辑:布尔运算符的选择对公式的大小没有重大影响。
有价值的约束满足问题(VCSP)构成了一大类计算优化问题。 最近显示,在有限域中,每个 VCSP 都是 P 或 NP 完整的,具体取决于已确认的成本函数。 在本文中,我们研究成本函数对可数的无限域,其自拟态形成寡态排列组。 我们的结果包括基于经典CSP的pp可构造性概括的硬度条件和基于分数多态性概念的多项时间牵引力条件。 然后,我们观察到,在数据库理论中研究的共体查询(UCQ)结合的弹性问题,在袋语义下,可能被视为我们考虑的VCSP的特殊情况。 我们获得了对发生率-鰰啶式UCQs的复杂性二分法,并举例使用我们的方法来确定在文献中被描述为一个开放问题的结列查询的复杂性。 我们推测,我们的硬度和牵引力条件与UCQ的弹性问题相匹配。 此外,我们获得了一个完整的二分法,用于双向常规路径查询的弹性问题,在包语义下。
极端图论中的许多结果可以表述为图同态密度中的某些多项式不等式。 在回答Lovász、Szegedy和Razborov、Hatami和Norine提出的基本问题时,证明在图同态密度中确定任意这种多项式不等式的有效性是不能决定的。 我们观察到,添加剂组合的许多结果也可以作为子集密度及其变体的多项式不等式配制。 基于哈塔米和诺林引入的技术,加上代数和图构造以及傅里叶分析,我们证明了类似的两个不可判定性定理,从而表明在添加剂组合中建立这样的多项式不等式在其完全通用性中本质上是困难的。
我们引入并研究中心类型，它们是 Eilenberg-Mac Lane 空间的推广。当一个类型与其自身自等价的单位分量等价时，该类型被称为中心类型。仅从中心性出发，我们通过带状类型的张量积构造一个无限的去循环，带状类型是中心类型的适当挠子概念。我们的构造是在同伦类型理论中进行的，因此在任何 ∞-拓扑中都成立。即使在解释为空间的 ∞-拓扑中，我们构建这些去循环的方法也是新的。在此过程中，我们进一步发展了同伦类型理论中 H-空间理论，包括它们与评估纤维和 Whitehead 积的关系。这些考虑使我们能够，例如，排除在 n > 0 时 2n-球上 H-空间结构的存在。我们还给出了 H-空间结构模空间的一个新的描述。利用这个描述，我们推广了 Arkowitz-Curjel 和 Copeland 针对计算该模空间的路径连通性的公式。作为应用，我们推导出 3-球上 H-空间结构的模空间为 Ω^6 𝕊^3。
我们探讨了“在非良序准序中寻找不良序列” (𝖡𝖲) 和 “在非良序线性序中寻找下降序列” (𝖣𝖲) 问题的 Weihrauch 程度。我们证明 𝖣𝖲 严格 Weihrauch 可约于 𝖡𝖲，纠正了我们在 [arXiv:2010.03840] 中的错误声明。这是通过分离它们各自的一阶部分来实现的。另一方面，我们表明 𝖡𝖲 和 𝖣𝖲 具有相同的有限和确定性部分，证实了 𝖡𝖲 和 𝖣𝖲 具有非常相似的统一计算强度。我们证明 König 引理 𝖪𝖫 和问题 𝗐𝖫𝗂𝗌𝗍_2^ℕ,≤ω (枚举给定的非空可数闭集 2^ℕ) 不可 Weihrauch 可约于 𝖣𝖲 或 𝖡𝖲，解决了 [arXiv:2010.03840] 中提出的两个主要未解决问题。我们还回答了 [arXiv:1804.10968] 中提出的关于“平行商”算子的存在性问题，并研究了 𝖡𝖲 和 𝖣𝖲 与一些已知问题商的性质。